mcrl2::data::mutable_indexed_substitution

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 substitution_type

typedef for std::pair< VariableType, ExpressionType >

Public types

type expression_type

typedef for ExpressionType

Type of expressions.

type variable_type

typedef for VariableType

Type of variables.

Protected attributes

std::vector<substitution_type> 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> m_free_positions
std::vector<std::size_t> m_index_table
std::multiset<variable> m_variables_in_rhs
bool m_variables_in_rhs_set_is_defined

Public member functions

void clear()

Clear substitutions.

bool empty()

Returns true if the substitution is empty.

mutable_indexed_substitution()

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)

Provides a set of variables that occur in the right hand sides of the assignments.