Include file:

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

Generic substitution function.

This substitution assumes a function variable -> std::size_t, that, for each variable gives a unique index. The substitutions are stored internally as a vector, mapping std::size_t to expression. Provided that, given a variable, its index can be computed in O(1) time, insertion is O(1) amortized, and lookup is O(1). Memory required is O(n) where n is the largest index used. This substitution can maintain the variables occurring in the rhs of expressions. If it is requested that whether a variable occurs in a rhs, the substitution automatically maintains these variables. This requires time O(n log n) per rhs, where n is the size of the rhs.

Protected types

type mcrl2::data::mutable_indexed_substitution::substitution_type

typedef for std::pair< VariableType, ExpressionType >

Public types

type mcrl2::data::mutable_indexed_substitution::argument_type

typedef for variable_type

type mcrl2::data::mutable_indexed_substitution::expression_type

typedef for ExpressionType

Type of expressions.

type mcrl2::data::mutable_indexed_substitution::variable_type

typedef for VariableType

Type of variables.

Protected attributes

std::vector<substitution_type> mcrl2::data::mutable_indexed_substitution::m_container

Internal storage for substitutions. Required to be a container with random access through [] operator. It is essential to store the variable also in the container, as it might be that this variable is not used anywhere although it has a valid assignment. This happens for instance when the assignment is already parsed, while the expression to which it needs to be applied must still be parsed.

std::stack<std::size_t> mcrl2::data::mutable_indexed_substitution::m_free_positions
std::vector<std::size_t> mcrl2::data::mutable_indexed_substitution::m_index_table
std::multiset<variable> mcrl2::data::mutable_indexed_substitution::m_variables_in_rhs
bool mcrl2::data::mutable_indexed_substitution::m_variables_in_rhs_set_is_defined

Public member functions

void clear()

Clear substitutions.

bool empty()

Returns true if the substitution is empty.


Default constructor.

const expression_type operator()(const variable_type &v) const

Application operator; applies substitution to v.

This must deliver an expression, and not a reference to an expression, as the expressions are stored in a vector that can be resized and moved.

bool operator==(const Substitution&) const

Compare substitutions.

assignment operator[](variable_type const &v)

Index operator.

bool size()

Returns the number of assigned variables in the substitution.

std::string to_string() const

string representation of the substitution. N.B. This is an expensive operation!

bool variable_occurs_in_a_rhs(const variable &v)

Checks whether a variable v occurs in one of the rhs’s of the current substitution.

Returns: A boolean indicating whether v occurs in sigma(x) for some variable x.

const std::multiset<variable> &variables_occurring_in_right_hand_sides() const

Provides a multiset containing the variables in the rhs.

Returns: A multiset with variables in the right hand side.