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



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.


  • t A term.

Returns: The expression resulting from the transformation.

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

Rewrites a pbes expression.


  • x A term
  • sigma A substitution function

Returns: The rewrite result.