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_)
const data_expression	operator() (const data_expression &d) const

Protected Member Functions
const 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 316 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()

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

inlineprotected

Definition at line 322 of file fourier_motzkin.h.

operator()()

const 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

rewr

rewriter mcrl2::data::fourier_motzkin_sigma::rewr

protected

Definition at line 320 of file fourier_motzkin.h.

---

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

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