mcrl2::pbes_system::bqnf_rewriter

Include file:

#include "mcrl2/pbes/rewriters/bqnf_rewriter.h

class mcrl2::pbes_system::bqnf_rewriter

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

Public types

type mcrl2::pbes_system::bqnf_rewriter::equation_type

typedef for pbes_equation

The equation type.

type mcrl2::pbes_system::bqnf_rewriter::term_type

typedef for pbes_expression

The term type.

Private attributes

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

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

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.

Parameters:

• t A term.

Returns: The expression resulting from the transformation.

term_type operator()(const term_type &x, SubstitutionFunction sigma) const

Rewrites a pbes expression.

Parameters:

• x A term
• sigma A substitution function

Returns: The rewrite result.