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])
mark
(std::stack<std::reference_wrapper<atermpp::detail::_aterm>> &todo) const¶The following function is needed to mark the aterms in this class, when elements of this class are used in an atermpp standard container. When garbage collection of aterms is taking place this function is called for all elements of this class in the atermpp container.
remove_assignments
(const VariableList &v, MutableSubstitution &result) const¶Removes the assignments corresponding with this element from the substitution result.
set
(const data::variable_list &v, const Expression &phi, const enumerator_list_element_with_substitution<Expression> &elem)¶Set the variable ands and the expression explicitly as the element (v, phi, e.sigma[v := x]).
set
(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)¶Set the variable ands and the expression explicitly as the element (v, phi, e.sigma[v := x]).