mcrl2::pbes_system::bqnf_rewriter Class Reference

A rewriter that rewrites universal quantifiers over conjuncts in BQNF expressions to conjuncts over universal quantifiers. More...

#include <bqnf_rewriter.h>

Public Types
typedef pbes_equation	equation_type
	The equation type.
typedef pbes_expression	term_type
	The term type.

Public Member Functions
	bqnf_rewriter ()
	Constructor.
term_type	operator() (const term_type &t) const
	Rewrites a PBES expression in BQNF such that universal quantifier over conjuncts are replaced by conjuncts over universal quantifiers.
template<typename SubstitutionFunction >
term_type	operator() (const term_type &x, SubstitutionFunction sigma) const
	Rewrites a pbes expression.

Private Attributes
std::unique_ptr< pbes_system::detail::bqnf_visitor >	bqnf_checker
std::unique_ptr< pbes_system::detail::bqnf_quantifier_rewriter >	bqnf_quantifier_rewriter

Detailed Description

A rewriter that rewrites universal quantifiers over conjuncts in BQNF expressions to conjuncts over universal quantifiers.

Definition at line 23 of file bqnf_rewriter.h.

Member Typedef Documentation

equation_type

typedef pbes_equation mcrl2::pbes_system::bqnf_rewriter::equation_type

The equation type.

Definition at line 27 of file bqnf_rewriter.h.

term_type

typedef pbes_expression mcrl2::pbes_system::bqnf_rewriter::term_type

The term type.

Definition at line 29 of file bqnf_rewriter.h.

Constructor & Destructor Documentation

bqnf_rewriter()

mcrl2::pbes_system::bqnf_rewriter::bqnf_rewriter ( )

inline

Constructor.

Definition at line 32 of file bqnf_rewriter.h.

Member Function Documentation

operator()() [1/2]

term_type mcrl2::pbes_system::bqnf_rewriter::operator() ( const term_type &  t ) const

inline

Rewrites a PBES expression in BQNF such that universal quantifier over conjuncts are replaced by conjuncts over universal quantifiers.

Parameters

t

A term.

Returns

The expression resulting from the transformation.

Definition at line 41 of file bqnf_rewriter.h.

operator()() [2/2]

template<typename SubstitutionFunction >

term_type mcrl2::pbes_system::bqnf_rewriter::operator() ( const term_type &  x, SubstitutionFunction  sigma  ) const

inline

Rewrites a pbes expression.

Parameters

x	A term
sigma	A substitution function

Returns

The rewrite result.

Definition at line 62 of file bqnf_rewriter.h.

Member Data Documentation

bqnf_checker

std::unique_ptr<pbes_system::detail::bqnf_visitor> mcrl2::pbes_system::bqnf_rewriter::bqnf_checker

private

Definition at line 68 of file bqnf_rewriter.h.

bqnf_quantifier_rewriter

std::unique_ptr<pbes_system::detail::bqnf_quantifier_rewriter> mcrl2::pbes_system::bqnf_rewriter::bqnf_quantifier_rewriter

private

Definition at line 69 of file bqnf_rewriter.h.

---

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

• pbes/include/mcrl2/pbes/rewriters/bqnf_rewriter.h