Include file:
#include "mcrl2/modal_formula/replace_capture_avoiding_with_an_identifier_generator.h"
add your file description here.
mcrl2::state_formulas::detail::add_capture_avoiding_replacement_with_an_identifier_generator
mcrl2::regular_formulas::detail::add_capture_avoiding_replacement_with_an_identifier_generator
mcrl2::action_formulas::detail::add_capture_avoiding_replacement_with_an_identifier_generator
mcrl2::action_formulas::
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.
mcrl2::action_formulas::
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.
mcrl2::regular_formulas::
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.
mcrl2::regular_formulas::
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.
mcrl2::regular_formulas::detail::
make_add_capture_avoiding_replacement_with_an_identifier_generator
(Substitution &sigma, IdentifierGenerator &id_generator)¶mcrl2::state_formulas::
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.
mcrl2::state_formulas::
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.