Contains functions to apply Fourier-Motzkin on linear inequalities and data expressions. More...

Classes
struct	mcrl2::data::fourier_motzkin_sigma
	A unary function that can be used in combination with replace_data_expressions to eliminate real numbers from all quantifiers in an expression. It is adviced to first push the quantifiers inside and apply the one point rule, since that reduces the time spent on the Fourier-Motzkin procedure for large expression. Apply this function innermost first if the expresion contains nested quantifiers. More...

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.

Functions
template<class Data_variable_iterator >
void	mcrl2::data::fourier_motzkin (const std::vector< linear_inequality > &inequalities_in, Data_variable_iterator variables_begin, Data_variable_iterator variables_end, std::vector< linear_inequality > &resulting_inequalities, const rewriter &r)

void	mcrl2::data::fourier_motzkin (const data_expression &e_in, const variable_list &vars_in, data_expression &e_out, variable_list &vars_out, const rewriter &r)
	Eliminate variables from a data expression using Gauss elimination and Fourier-Motzkin elimination.

Detailed Description

Contains functions to apply Fourier-Motzkin on linear inequalities and data expressions.

Definition in file fourier_motzkin.h.

Classes