mcrl2::data::maintain_variables_in_rhs¶
Include file:
#include "mcrl2/data/substitutions/maintain_variables_in_rhs.h
-
class
mcrl2::data::maintain_variables_in_rhs¶ Wrapper that extends any substitution to a substitution maintaining the vars in its rhs.
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.
Public types¶
-
type
mcrl2::data::maintain_variables_in_rhs::expression_type¶ typedef for
super::expression_type
-
type
mcrl2::data::maintain_variables_in_rhs::super¶ typedef for
Substitution
-
type
mcrl2::data::maintain_variables_in_rhs::variable_type¶ typedef for
super::variable_type
Protected attributes¶
-
std::set<variable_type>
mcrl2::data::maintain_variables_in_rhs::m_scratch_set¶
-
std::multiset<variable_type>
mcrl2::data::maintain_variables_in_rhs::m_variables_in_rhs¶
Public member functions¶
-
void
clear() Clear substitutions.
-
maintain_variables_in_rhs()¶ Default constructor.
-
bool
occurs_in_a_rhs(const variable_type &v)¶ Indicates whether a variable occurs in some rhs of this substitution.
Parameters:
- v The variable for which occurrence in a rhs is checked.
-
assignment
operator[](variable_type const &v)¶ Assigment operator.
Parameters:
- v The variable to which the assignment is carried out.
