Include file:

#include "mcrl2/data/linear_inequalities.h"

Contains a class linear_inequality to represent mcrl2 data expressions that are linear equalities, or inequalities. Furthermore, it contains some operations on these linear inequalities, such as Fourier-Motzkin elimination.


void mcrl2::data::count_occurrences(const std::vector<linear_inequality> &inequalities, std::map<variable, std::size_t> &nr_positive_occurrences, std::map<variable, std::size_t> &nr_negative_occurrences, const rewriter &r)
std::set<variable> gauss_elimination(const std::vector<linear_inequality> &inequalities, std::vector<linear_inequality> &resulting_equalities, std::vector<linear_inequality> &resulting_inequalities, Variable_iterator variables_begin, Variable_iterator variables_end, const rewriter &r)

Try to eliminate variables from a system of inequalities using Gauss elimination.

For all variables yi in y1,...,yn indicated by variables_begin to variables_end, it attempted to find and equation among inequalities of the form yi==expression. All occurrences of yi in equalities are subsequently replaced by yi. If no equation of the form yi can be found, yi is added to the list of variables that is returned by this function. If the input contains an inconsistent inequality, resulting_equalities becomes empty, resulting_inequalities contains false and the returned list of variables is also empty. The resulting equalities and inequalities do not contain linear inequalites equivalent to true.


  • inequalities A list of inequalities over real numbers
  • resulting_equalities A list with the resulting equalities.
  • resulting_inequalities A list of the resulting inequalities
  • variables_begin An iterator indicating the beginning of the eliminatable variables.
  • variables_end An iterator indicating the end of the eliminatable variables.
  • r A rewriter.

Post: variables contains the list of variables that have not been eliminated

Returns: The variables that could not be removed by gauss elimination.

bool mcrl2::data::is_a_redundant_inequality(const std::vector<linear_inequality> &inequalities, const std::vector<linear_inequality>::iterator i, const rewriter &r)

Indicate whether an inequality from a set of inequalities is redundant.

Return whether the inequality referred to by i is inconsistent. It is expected that i refers to an equality in the vector inequalities. The vector inequalities might be changed within the procedure, but will be restored to its original value when this function terminates.


  • inequalities A list of inequalities
  • i An iterator pointing into inequalities.
  • r A rewriter

Returns: An indication whether the inequality referred to by i is inconsistent in the context of inequalities.

bool is_closed_real_number(const data_expression &e)
bool is_inconsistent(const std::vector<linear_inequality> &inequalities_in, const rewriter &r, const bool use_cache)

Determine whether a list of data expressions is inconsistent.

First it is checked whether false is among the input. If not, Fourier-Motzkin is applied to all variables in the inequalities. If the empty vector of equalities is the result, the input was consistent. Otherwise the resulting vector contains an inconsistent inequality. The implementation uses a feasible point detection algorithm as described by Bruno Dutertre and Leonardo de Moura. Integrating Simplex with DPLL(T). CSL Technical Report SRI-CSL-06-01, 2006.


  • inequalities_in A list of inequalities.
  • r A rewriter.
  • use_cache A boolean indicating whether results can be cahced.

Returns: true if the system of inequalities can be determined to be inconsistent, false otherwise.

bool is_negative(const data_expression &e, const rewriter &r)
bool is_positive(const data_expression &e, const rewriter &r)
bool is_zero(const data_expression &e)
data_expression max(const data_expression &e1, const data_expression &e2, const rewriter&)
data_expression min(const data_expression &e1, const data_expression &e2, const rewriter&)
static void mcrl2::data::pivot_and_update(const variable &xi, const variable &xj, const data_expression &v, const data_expression &v_delta_correction, std::map<variable, data_expression> &beta, std::map<variable, data_expression> &beta_delta_correction, std::set<variable> &basic_variables, std::map<variable, detail::lhs_t> &working_equalities, const rewriter &r)
std::string pp(const linear_inequality &l)
std::string pp_vector(const TYPE &inequalities)

Print the vector of inequalities to stderr in readable form.

application mcrl2::data::real_abs(const data_expression &arg)
application mcrl2::data::real_divides(const data_expression &arg0, const data_expression &arg1)
application mcrl2::data::real_minus(const data_expression &arg0, const data_expression &arg1)
data_expression &real_minus_one()
application mcrl2::data::real_negate(const data_expression &arg)
data_expression &real_one()
application mcrl2::data::real_plus(const data_expression &arg0, const data_expression &arg1)
application mcrl2::data::real_times(const data_expression &arg0, const data_expression &arg1)
data_expression &real_zero()
void mcrl2::data::remove_redundant_inequalities(const std::vector<linear_inequality> &inequalities, std::vector<linear_inequality> &resulting_inequalities, const rewriter &r)

Remove every redundant inequality from a vector of inequalities.

If inequalities is inconsistent, [false] is returned. Otherwise a list of inequalities is returned, from which no inequality can be removed without changing the vector of solutions of the inequalities. Redundancy of equalities is not checked, because this is quite expensive.


  • inequalities A list of inequalities
  • resulting_inequalities A list of inequalities to which the result is stored.
  • r A rewriter
data_expression rewrite_with_memory(const data_expression &t, const rewriter &r)
linear_inequality mcrl2::data::subtract(const linear_inequality &e1, const linear_inequality &e2, const data_expression &f1, const data_expression &f2, const rewriter &r)

Subtract the given equality, multiplied by f1/f2. The result is e1-(f1/f2)e2,.

Enumerated types

type comparison_t


  • less
  • less_eq
  • equal
type node_type


  • true_end_node
  • false_end_node
  • intermediate_node


type map_based_lhs_t

typedef for std::map< variable, data_expression >


const lhs_t mcrl2::data::detail::add(const data_expression &v, const lhs_t &argument, const rewriter &r)
const lhs_t mcrl2::data::detail::add(const lhs_t &argument, const lhs_t &e, const rewriter &r)
const lhs_t mcrl2::data::detail::divide(const lhs_t &argument, const data_expression &v, const rewriter &r)
void mcrl2::data::detail::emplace_back_if_not_zero(std::vector<detail::variable_with_a_rational_factor> &r, const variable &v, const data_expression &f)
atermpp::function_symbol mcrl2::data::detail::f_variable_with_a_rational_factor()
bool mcrl2::data::detail::is_well_formed(const lhs_t &lhs)
atermpp::function_symbol mcrl2::data::detail::linear_inequality_equal()
atermpp::function_symbol mcrl2::data::detail::linear_inequality_less()
atermpp::function_symbol mcrl2::data::detail::linear_inequality_less_equal()
const lhs_t mcrl2::data::detail::map_to_lhs_type(const map_based_lhs_t &lhs)
const lhs_t mcrl2::data::detail::map_to_lhs_type(const map_based_lhs_t &lhs, const data_expression &factor, const rewriter &r)
const lhs_t mcrl2::data::detail::meta_operation_constant(const lhs_t &argument, const data_expression &v, const rewriter &r)
lhs_t mcrl2::data::detail::meta_operation_lhs(const lhs_t &argument1, const lhs_t &argument2, OPERATION operation, const rewriter &r)
const lhs_t mcrl2::data::detail::multiply(const lhs_t &argument, const data_expression &v, const rewriter &r)
detail::comparison_t mcrl2::data::detail::negate(const detail::comparison_t t)
std::string pp(const detail::lhs_t &lhs)
std::string mcrl2::data::detail::pp(const detail::comparison_t t)
const lhs_t mcrl2::data::detail::remove_variable_and_divide(const lhs_t &lhs, const variable &v, const data_expression &f, const rewriter &r)
void mcrl2::data::detail::set_factor_for_a_variable(detail::map_based_lhs_t &new_lhs, const variable &x, const data_expression &e)
lhs_t mcrl2::data::detail::set_factor_for_a_variable(const lhs_t &lhs, const variable &x, const data_expression &e)
const lhs_t mcrl2::data::detail::subtract(const lhs_t &argument, const data_expression &v, const rewriter &r)
const lhs_t mcrl2::data::detail::subtract(const lhs_t &argument, const lhs_t &e, const rewriter &r)