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 expression_type

typedef for Expression

Protected attributes

data::data_expression_list m_expressions
data::variable_list 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.