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 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.

void remove_assignments(const VariableList &v, MutableSubstitution &result) const

Removes the assignments corresponding with this element from the substitution result.

void 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]).

void 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]).

data::enumerator_substitution sigma() const