Include file:

#include "mcrl2/bes/normal_forms.h
class mcrl2::bes::detail::standard_form_traverser

Traverser that implements the standard form normalization.

Public types

type mcrl2::bes::detail::standard_form_traverser::super

typedef for bes::boolean_expression_traverser< standard_form_traverser >

Public attributes

std::vector<boolean_equation> mcrl2::bes::detail::standard_form_traverser::m_equations

A vector containing generated equations.

std::vector<boolean_equation> mcrl2::bes::detail::standard_form_traverser::m_equations2

A vector containing generated equations with new variables.

std::vector<standard_form_pair> mcrl2::bes::detail::standard_form_traverser::m_expression_stack

A stack containing sub-terms.

boolean_expression mcrl2::bes::detail::standard_form_traverser::m_false

The expression corresponding to false.

utilities::number_postfix_generator mcrl2::bes::detail::standard_form_traverser::m_generator

For generating fresh variables.

bool mcrl2::bes::detail::standard_form_traverser::m_has_false

Is set to true if the value false is encountered in the BES.

bool mcrl2::bes::detail::standard_form_traverser::m_has_true

Is set to true if the value true is encountered in the BES.

std::string mcrl2::bes::detail::standard_form_traverser::m_name

The name of the variable of the current equation, with a trailing underscore added.

bool mcrl2::bes::detail::standard_form_traverser::m_recursive_form

If true, the result will be in standard recursive normal form, otherwise in standard form.

fixpoint_symbol mcrl2::bes::detail::standard_form_traverser::m_symbol

The fixpoint symbol of the current equation.

std::map<boolean_expression, boolean_variable> mcrl2::bes::detail::standard_form_traverser::m_table

Maps right hand sides of equations to their corresponding left hand side.

boolean_expression mcrl2::bes::detail::standard_form_traverser::m_true

The expression corresponding to true.

Public member functions

boolean_variable create_variable(const boolean_expression &expr, standard_form_type type, const std::string &hint)

Generates an equation var=expr for the expression expr (if it does not exist).

Returns: The variable var.

void enter(const boolean_equation &eq)

Enter an equation.

void enter(const boolean_equation_system &x)

Enter a boolean equation system.

void enter(const boolean_variable &x)

Enter boolean_variable node.


  • x A boolean variable.
void enter(const false_ &x)

Enter false node.


  • x A term
void enter(const true_ &x)

Enter true node.


  • x A term.
const std::vector<boolean_equation> &equations() const

Returns the generated equations.

boolean_variable fresh_variable(const std::string &hint)

Generates a fresh boolean variable.

void leave(const and_&)

Leave and node.

void leave(const boolean_equation &eq)

Leave an equation.

void leave(const boolean_equation_system&)

Leave a boolean equation system.

void leave(const imp&)

Leave imp node.

void leave(const not_&)

Leave not node.

void leave(const or_&)

Leave or node.

standard_form_pair pop()

Pops the stack and returns the popped element.

void push(const boolean_expression &first, standard_form_type second)

Pushes (first, second) on the stack.

boolean_expression result() const

Returns the top element of the expression stack, which is the result of the normalization.

standard_form_traverser(bool recursive_form = false)



  • recursive_form Determines whether or not the result will be in standard recursive normal form.