Include file:

#include "mcrl2/data/linear_inequalities.h
class mcrl2::data::linear_inequality

Protected static member functions

static void parse_and_store_expression(const data_expression &e, detail::map_based_lhs_t &new_lhs, data_expression &new_rhs, const rewriter &r, const bool negate = false, const data_expression &factor = real_one())

Public member functions

void add_variables(std::set<variable> &variable_set) const
detail::comparison_t comparison() const
data_expression get_factor_for_a_variable(const variable &x)
linear_inequality invert(const rewriter &r)
bool is_false(const rewriter &r) const
bool is_true(const rewriter &r) const
const detail::lhs_t &lhs() const
detail::lhs_t::const_iterator lhs_begin() const
detail::lhs_t::const_iterator lhs_end() const

Constructor yielding an inconsistent inequality.

linear_inequality(const data_expression &e, const rewriter &r)

Constructor that constructs a linear inequality out of a data expression.

The data expression e is expected to have the form lhs op rhs where op is one of <=,<,==,>,>= and lhs and rhs satisfy the syntax t ::= x | c*t | t*c | t+t | t-t | -t where x is a variable and c is a real constant.


  • e Contains the expression to become a linear inequality.
  • r A rewriter used to evaluate the expression.
linear_inequality(const data_expression &lhs, const data_expression &rhs, const detail::comparison_t comparison, const rewriter &r, const bool negate = false)


linear_inequality(const detail::lhs_t &lhs, const data_expression &r, detail::comparison_t t)

Basic constructor.

linear_inequality(const detail::lhs_t &lhs, const data_expression &rhs, detail::comparison_t comparison, const rewriter &r)


const data_expression &rhs() const
data_expression transform_to_data_expression() const
bool typical_pair(data_expression &lhs_expression, data_expression &rhs_expression, detail::comparison_t &comparison_operator, const rewriter &r) const

Return this inequality as a typical pair of terms of the form <x1+c2 x2+…+cn xn, d> where c2,…,cn, d are real constants.

Returns: The return value indicates whether the left and right hand side have been negated when yielding the typical pair.