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. More...

Classes
class	mcrl2::data::detail::variable_with_a_rational_factor

class	mcrl2::data::detail::lhs_t

class	mcrl2::data::linear_inequality

class	mcrl2::data::detail::inequality_inconsistency_cache_base

class	mcrl2::data::detail::inequality_inconsistency_cache

class	mcrl2::data::detail::inequality_consistency_cache

Namespaces
namespace	mcrl2
	A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.

namespace	mcrl2::data
	Namespace for all data library functionality.

namespace	mcrl2::data::detail

Typedefs
typedef std::map< variable, data_expression >	mcrl2::data::detail::map_based_lhs_t

Enumerations
enum	mcrl2::data::detail::comparison_t { mcrl2::data::detail::less , mcrl2::data::detail::less_eq , mcrl2::data::detail::equal }

enum	mcrl2::data::detail::node_type { mcrl2::data::detail::true_end_node , mcrl2::data::detail::false_end_node , mcrl2::data::detail::intermediate_node }

Functions
data_expression &	mcrl2::data::real_zero ()

data_expression &	mcrl2::data::real_one ()

data_expression &	mcrl2::data::real_minus_one ()

data_expression	mcrl2::data::min (const data_expression &e1, const data_expression &e2, const rewriter &)

data_expression	mcrl2::data::max (const data_expression &e1, const data_expression &e2, const rewriter &)

bool	mcrl2::data::is_closed_real_number (const data_expression &e)

bool	mcrl2::data::is_negative (const data_expression &e, const rewriter &r)

bool	mcrl2::data::is_positive (const data_expression &e, const rewriter &r)

bool	mcrl2::data::is_zero (const data_expression &e)

application	mcrl2::data::real_times (const data_expression &arg0, const data_expression &arg1)

application	mcrl2::data::real_plus (const data_expression &arg0, const data_expression &arg1)

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)

application	mcrl2::data::real_negate (const data_expression &arg)

application	mcrl2::data::real_abs (const data_expression &arg)

data_expression	mcrl2::data::rewrite_with_memory (const data_expression &t, const rewriter &r)

std::string	mcrl2::data::pp (const linear_inequality &l)

template<class TYPE >
std::string	mcrl2::data::pp_vector (const TYPE &inequalities)
	Print the vector of inequalities to stderr in readable form.

std::string	mcrl2::data::detail::pp (const detail::lhs_t &lhs)

detail::comparison_t	mcrl2::data::detail::negate (const detail::comparison_t t)

std::string	mcrl2::data::detail::pp (const detail::comparison_t t)

atermpp::function_symbol	mcrl2::data::detail::f_variable_with_a_rational_factor ()

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::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)

bool	mcrl2::data::detail::is_well_formed (const lhs_t &lhs)

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::emplace_back_if_not_zero (std::vector< detail::variable_with_a_rational_factor > &r, const variable &v, const data_expression &f)

template<application Operation>
const lhs_t	mcrl2::data::detail::meta_operation_constant (const lhs_t &argument, const data_expression &v, const rewriter &r)

template<class OPERATION >
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::add (const data_expression &v, const lhs_t &argument, const rewriter &r)

const lhs_t	mcrl2::data::detail::subtract (const lhs_t &argument, const data_expression &v, const rewriter &r)

const lhs_t	mcrl2::data::detail::multiply (const lhs_t &argument, const data_expression &v, const rewriter &r)

const lhs_t	mcrl2::data::detail::divide (const lhs_t &argument, const data_expression &v, 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::subtract (const lhs_t &argument, const lhs_t &e, const rewriter &r)

atermpp::function_symbol	mcrl2::data::detail::linear_inequality_less ()

atermpp::function_symbol	mcrl2::data::detail::linear_inequality_less_equal ()

atermpp::function_symbol	mcrl2::data::detail::linear_inequality_equal ()

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,.

bool	mcrl2::data::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.

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)

template<class Variable_iterator >
std::set< variable >	mcrl2::data::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.

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.

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.

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)

Detailed Description

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.

Definition in file linear_inequalities.h.

Classes

Namespaces

Typedefs

Enumerations

Functions

Detailed Description