Include file:
#include "mcrl2/data/enumerator.h
mcrl2::data::
enumerator_list_element_with_substitution
¶An element for the todo list of the enumerator that collects the substitution corresponding to the expression phi.
mcrl2::data::enumerator_list_element_with_substitution::
expression_type
¶typedef for Expression
mcrl2::data::enumerator_list_element_with_substitution::
m_expressions
¶mcrl2::data::enumerator_list_element_with_substitution::
m_variables
¶add_assignments
(const VariableList &v, MutableSubstitution &result, const Rewriter &rewriter) const¶Adds the assignments that correspond with this element to the substitution result.
assign_expressions
(const VariableList &v, const Rewriter &rewriter) const¶Returns the right hand sides corresponding to the variables v.
Pre: variables in v must be contained in variables()
enumerator_list_element_with_substitution
() = default¶Default constructor.
enumerator_list_element_with_substitution
(const data::variable_list &v, const Expression &phi)¶Constructs the element (v, phi, [])
enumerator_list_element_with_substitution
(const data::variable_list &v, const Expression &phi, const enumerator_list_element_with_substitution<Expression> &elem)¶Constructs the element (v, phi, e.sigma[v := x])
enumerator_list_element_with_substitution
(const data::variable_list &v, const Expression &phi, const enumerator_list_element_with_substitution<Expression> &elem, const data::variable &d, const data::data_expression &e)¶Constructs the element (v, phi, e.sigma[v := x])
remove_assignments
(const VariableList &v, MutableSubstitution &result) const¶Removes the assignments corresponding with this element from the substitution result.