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.