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 expression_type

typedef for super::expression_type

type super

typedef for Substitution

type variable_type

typedef for super::variable_type

Protected attributes

std::set<variable_type> m_scratch_set
std::multiset<variable_type> m_variables_in_rhs

Public member functions

void clear()

Clear substitutions.


Default constructor.

bool occurs_in_a_rhs(const variable_type &v)

Indicates whether a variable occurs in some rhs of this substitution.


  • v The variable for which occurrence in a rhs is checked.
assignment operator[](variable_type const &v)

Assigment operator.


  • v The variable to which the assignment is carried out.
const std::multiset<variable> &variables_in_rhs()

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