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.
mcrl2::data::mutable_indexed_substitution::
substitution_type
¶typedef for atermpp::utilities::unordered_map< VariableType, ExpressionType >
mcrl2::data::mutable_indexed_substitution::
argument_type
¶typedef for variable_type
mcrl2::data::mutable_indexed_substitution::
expression_type
¶typedef for ExpressionType
Type of expressions.
mcrl2::data::mutable_indexed_substitution::
result_type
¶typedef for expression_type
mcrl2::data::mutable_indexed_substitution::
variable_type
¶typedef for VariableType
Type of variables.
mcrl2::data::mutable_indexed_substitution::
m_substitution
¶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.
mcrl2::data::mutable_indexed_substitution::
m_variables_in_rhs
¶mcrl2::data::mutable_indexed_substitution::
m_variables_in_rhs_set_is_defined
¶apply
(const variable_type &v, expression_type &target, std::atomic<bool> *busy_flag, std::atomic<bool> *forbidden_flag, std::size_t *lock_depth)¶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.
Parameters:
apply
(const variable_type &v, ResultType &target)¶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.
Parameters:
clear
()Clear substitutions.
clone
()¶Create a clone of the rewriter in which the underlying rewriter is copied, and not passed as a shared pointer.
This is useful when the rewriter is used in different parallel processes. One rewriter can only be used sequentially.
Returns: A rewriter, with a copy of the underlying jitty, jittyc or jittyp rewriting engine.
empty
()¶Returns true if the substitution is empty.
mutable_indexed_substitution
()¶Default constructor.
mutable_indexed_substitution
(const substitution_type &substitution, const bool variables_in_rhs_set_is_defined, const std::multiset<variable_type> &variables_in_rhs)¶operator()
(const variable_type &v) const¶Application operator; applies substitution to v.
Parameters:
Returns: The value to which v is mapped, or v itself if v is not mapped to a value.
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!
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.
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.