mcrl2::data::mutable_map_substitution

Include file:

#include "mcrl2/data/substitutions/mutable_map_substitution.h
class mcrl2::data::mutable_map_substitution

Generic substitution function. The substitution is stored as a mapping of variables to expressions. The substitution is mutable, meaning that substitutions to variables can be added and removed as follows:

  • mutable_map_substitution sigma;
  • mutable_map_substitution::variable_type v;
  • mutable_map_substitution::expression_type e;
  • sigma[v] = e; // add the assignment of e to v
  • sigma[v] = v; // remove the assignment to v

Public types

type mcrl2::data::mutable_map_substitution::argument_type

typedef for variable_type

type mcrl2::data::mutable_map_substitution::const_iterator

typedef for AssociativeContainer::const_iterator

type mcrl2::data::mutable_map_substitution::expression_type

typedef for AssociativeContainer::mapped_type

type mcrl2::data::mutable_map_substitution::iterator

typedef for AssociativeContainer::iterator

type mcrl2::data::mutable_map_substitution::result_type

typedef for expression_type

type mcrl2::data::mutable_map_substitution::variable_type

typedef for AssociativeContainer::key_type

Protected attributes

AssociativeContainer mcrl2::data::mutable_map_substitution::m_map

Public member functions

iterator begin()

Returns an iterator pointing to the beginning of the sequence of assignments TODO: should become protected.

const_iterator begin() const

Returns an iterator pointing to the beginning of the sequence of assignments TODO: should become protected.

void clear()

Resets the substitution by letting every variable yield itself. Cf. clear() of a map.

bool empty()

Returns true if the substitution is empty.

iterator end()

Returns an iterator pointing past the end of the sequence of assignments TODO: should become protected.

const_iterator end() const

Returns an iterator pointing past the end of the sequence of assignments TODO: should become protected.

iterator find(variable_type const &v)

Returns an iterator that references the expression associated with v or is equal to m_map.end()

const_iterator find(variable_type const &v) const

Returns an iterator that references the expression associated with v or is equal to m_map.end()

mutable_map_substitution() = default
mutable_map_substitution(const AssociativeContainer &m)
mutable_map_substitution(VariableContainer const &variables, ExpressionContainer const &expressions)
expression_type operator()(const variable_type &v) const
bool operator==(const Substitution&) const
assignment operator[](variable_type const &v)
std::string to_string() const