mcrl2::data::enumerator_list_element_with_substitution¶
Include file:
#include "mcrl2/data/enumerator.h
-
class
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.
Public types¶
-
type
mcrl2::data::enumerator_list_element_with_substitution::expression_type¶ typedef for
Expression
Protected attributes¶
-
data::data_expression_list
mcrl2::data::enumerator_list_element_with_substitution::m_expressions¶
-
data::variable_list
mcrl2::data::enumerator_list_element_with_substitution::m_variables¶
Public member functions¶
-
void
add_assignments(const VariableList &v, MutableSubstitution &result, const Rewriter &rewriter) const¶ Adds the assignments that correspond with this element to the substitution result.
-
data::data_expression_list
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])
-
void
remove_assignments(const VariableList &v, MutableSubstitution &result) const¶ Removes the assignments corresponding with this element from the substitution result.
