mcrl2::data::linear_inequality¶
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¶
-
detail::comparison_t
comparison() const¶
-
data_expression
get_factor_for_a_variable(const variable &x)¶
-
linear_inequality
invert(const rewriter &r)¶
-
const detail::lhs_t &
lhs() const
-
detail::lhs_t::const_iterator
lhs_begin() const¶
-
detail::lhs_t::const_iterator
lhs_end() const¶
-
linear_inequality()¶ 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.
Parameters:
- 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)¶ constructor.
-
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)¶ constructor.
-
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.
