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 mcrl2::data::mutable_indexed_substitution::substitution_type

typedef for atermpp::utilities::unordered_map< 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::result_type

typedef for expression_type

type mcrl2::data::mutable_indexed_substitution::variable_type

typedef for VariableType

Type of variables.

Protected attributes

substitution_type 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.

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 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:

• v The variable to which the subsitution is applied.
• target The target into which the substitution is stored.

void 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:

• v The variable to which the subsitution is applied.
• target The target into which the substitution is stored.

void clear()

Clear substitutions.

mutable_indexed_substitution<VariableType, ExpressionType> 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.

bool 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)

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

Application operator; applies substitution to v.

Parameters:

• v The variable to which the subsitution is applied.

Returns: The value to which v is mapped, or v itself if v is not mapped to a value.

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_type> &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.