mcrl2::data::fourier_motzkin_sigma Struct Reference

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

#include <fourier_motzkin.h>

Public Member Functions
	fourier_motzkin_sigma (const rewriter &rewr_)
data_expression	operator() (const data_expression &d) const

Static Public Attributes
static constexpr bool	is_identity_substitution = false

Protected Member Functions
data_expression	apply (const abstraction &d, bool negate) const

Protected Attributes
rewriter	rewr

Detailed Description

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.

Author

Thomas Neele

Definition at line 314 of file fourier_motzkin.h.

Constructor & Destructor Documentation

fourier_motzkin_sigma()

mcrl2::data::fourier_motzkin_sigma::fourier_motzkin_sigma ( const rewriter &  rewr_ )

inline

Definition at line 343 of file fourier_motzkin.h.

Member Function Documentation

apply()

data_expression mcrl2::data::fourier_motzkin_sigma::apply ( const abstraction &  d, bool  negate  ) const

inlineprotected

Definition at line 320 of file fourier_motzkin.h.

operator()()

data_expression mcrl2::data::fourier_motzkin_sigma::operator() ( const data_expression &  d ) const

inline

Definition at line 347 of file fourier_motzkin.h.

Member Data Documentation

is_identity_substitution

constexpr bool mcrl2::data::fourier_motzkin_sigma::is_identity_substitution = false

staticconstexpr

Definition at line 341 of file fourier_motzkin.h.

rewr

rewriter mcrl2::data::fourier_motzkin_sigma::rewr

protected

Definition at line 318 of file fourier_motzkin.h.

---

The documentation for this struct was generated from the following file:

• data/include/mcrl2/data/fourier_motzkin.h