Include file:
#include "mcrl2/data/substitutions/mutable_indexed_substitution.h
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.
expression_type
¶typedef for ExpressionType
Type of expressions.
variable_type
¶typedef for VariableType
Type of variables.
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.
m_free_positions
¶
m_index_table
¶
m_variables_in_rhs_set_is_defined
¶
clear
()¶Clear substitutions.
empty
()¶Returns true if the substitution is empty.
mutable_indexed_substitution
()¶Default constructor.
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.
operator==
(const Substitution&) const¶Compare substitutions.
operator[]
(variable_type const &v)¶Index operator.
size
()¶Returns the number of assigned variables in the substitution.
to_string
() const¶string representation of the substitution. N.B. This is an expensive operation!