mcrl2/data/replace_capture_avoiding_with_an_identifier_generator.h

Include file:

#include "mcrl2/data/replace_capture_avoiding_with_an_identifier_generator.h"

add your file description here.

Classes

Functions

void mcrl2::data::replace_variables_capture_avoiding_with_an_identifier_generator(T &x, Substitution &sigma, IdentifierGenerator &id_generator, typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type * = nullptr)

Applies sigma as a capture avoiding substitution to x using an identifier generator.

This substitution function is much faster than replace_variables_capture_avoiding, but it requires an identifier generator that generates strings for fresh variables. These strings must be unique in the sense that they have not been used for other variables.

Parameters:

  • x The object to which the subsitution is applied.

  • sigma A mutable substitution of which it can efficiently be checked whether a variable occurs in its right hand side. The class maintain_variables_in_rhs is useful for this purpose.

  • id_generator A generator that generates unique strings, not yet used as variable names.

T mcrl2::data::replace_variables_capture_avoiding_with_an_identifier_generator(const T &x, Substitution &sigma, IdentifierGenerator &id_generator, typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type * = nullptr)

Applies sigma as a capture avoiding substitution to x using an identifier generator..

This substitution function is much faster than replace_variables_capture_avoiding, but it requires an identifier generator that generates strings for fresh variables. These strings must be unique in the sense that they have not been used for other variables.

Parameters:

  • x The object to which the substiution is applied.

  • sigma A mutable substitution of which it can efficiently be checked whether a variable occurs in its right hand side. The class maintain_variables_in_rhs is useful for this purpose.

  • id_generator A generator that generates unique strings, not yet used as variable names.

Returns: The result is the term x to which sigma has been applied.

Functions

replace_capture_avoiding_variables_builder_with_an_identifier_generator<Builder, Binder, Substitution, IdentifierGenerator> mcrl2::data::detail::apply_replace_capture_avoiding_variables_builder_with_an_identifier_generator(Substitution &sigma, IdentifierGenerator &id_generator)
data::variable mcrl2::data::detail::update_substitution(Substitution &sigma, const data::variable &v, const std::multiset<data::variable> &V, IdentifierGenerator &id_generator)
VariableContainer mcrl2::data::detail::update_substitution(Substitution &sigma, const VariableContainer &v, const std::multiset<data::variable> &V, IdentifierGenerator &id_generator)