mcrl2::data::data_equation

Include file:

#include "mcrl2/data/data_equation.h
class mcrl2::data::data_equation

A data equation.

Public member functions

const data_expression &condition() const
data_equation()

Default constructor.

data_equation(const atermpp::aterm &term)

Constructor.

Parameters:

  • term A term
data_equation(const variable_list &variables, const data_expression &condition, const data_expression &lhs, const data_expression &rhs)

Constructor.

data_equation(const Container &variables, const data_expression &condition, const data_expression &lhs, const data_expression &rhs, typename atermpp::enable_if_container<Container, variable>::type * = nullptr)

Constructor.

data_equation(const data_equation&) noexcept = default

Move semantics.

data_equation(data_equation&&) noexcept = default
data_equation(const Container &variables, const data_expression &lhs, const data_expression &rhs, typename atermpp::enable_if_container<Container, variable>::type * = nullptr)

Constructor.

Parameters:

  • variables The free variables of the data_equation.
  • lhs The left hand side of the data_equation.
  • rhs The right hand side of the data_equation.

Post: this is the data equation representing the input, with condition true

data_equation(const data_expression &lhs, const data_expression &rhs)

Constructor.

Parameters:

  • lhs The left hand side of the data equation.
  • rhs The right hand side of the data equation.

Post: this is the data equations representing the input, without variables, and condition true

const data_expression &lhs() const
data_equation &operator=(const data_equation&) noexcept = default
data_equation &operator=(data_equation&&) noexcept = default
const data_expression &rhs() const
const variable_list &variables() const