mcrl2/data/fourier_motzkin.h

Include file:

#include "mcrl2/data/fourier_motzkin.h"

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

Classes

  • mcrl2::data::fourier_motzkin_sigma

Functions

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.

Deliver a data_expression e_out and a set of variables vars_out such that exists vars_in.e_in is equivalent to exists vars_out.e_out. If the resulting list of inequalities is inconsistent, then [false] is returned.

Parameters:

  • e_in An input data_expression of sort Bool.

  • vars_in A container with variables. Supports iterating over these variables.

  • e_out The output data expression of sort Bool.

  • vars_out A list of variables to store resulting variables. Initially empty.

  • r A rewriter.

Post: exists vars_out.e_out == exists vars_in.e_in.