mcrl2/pbes/replace.h

Include file:

#include "mcrl2/pbes/replace.h"

add your file description here.

Functions

void mcrl2::pbes_system::replace_all_variables(T &x, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
T mcrl2::pbes_system::replace_all_variables(const T &x, const Substitution &sigma, typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type * = nullptr)
void mcrl2::pbes_system::replace_data_expressions(T &x, const Substitution &sigma, bool innermost, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
T mcrl2::pbes_system::replace_data_expressions(const T &x, const Substitution &sigma, bool innermost, typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type * = nullptr)
void mcrl2::pbes_system::replace_free_variables(T &x, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

Applies the substitution sigma to x.

Pre: { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }

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

Applies the substitution sigma to x.

Pre: { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }

void mcrl2::pbes_system::replace_free_variables(T &x, const Substitution &sigma, const VariableContainer &bound_variables, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables.

Pre: { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }

T mcrl2::pbes_system::replace_free_variables(const T &x, const Substitution &sigma, const VariableContainer &bound_variables, typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type * = nullptr)

Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables.

Pre: { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }

void mcrl2::pbes_system::replace_pbes_expressions(T &x, const Substitution &sigma, bool innermost=true, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=0)
T mcrl2::pbes_system::replace_pbes_expressions(const T &x, const Substitution &sigma, bool innermost = true, typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type * = nullptr)
void mcrl2::pbes_system::replace_propositional_variables(T &x, const Substitution &sigma, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

Applies a propositional variable substitution.

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

Applies a propositional variable substitution.

void mcrl2::pbes_system::replace_sort_expressions(T &x, const Substitution &sigma, bool innermost, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
T mcrl2::pbes_system::replace_sort_expressions(const T &x, const Substitution &sigma, bool innermost, typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type * = nullptr)
void mcrl2::pbes_system::replace_variables(T &x, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
T mcrl2::pbes_system::replace_variables(const T &x, const Substitution &sigma, typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type * = nullptr)
void mcrl2::pbes_system::replace_variables_capture_avoiding(T &x, Substitution &sigma, const VariableContainer &sigma_variables, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

Applies sigma as a capture avoiding substitution to x.

Parameters:

  • x The object to which the subsitution is applied.
  • sigma A mutable substitution.
  • sigma_variables a container of variables.

Pre: { sigma_variables must contain the free variables appearing in the right hand side of sigma }.

T mcrl2::pbes_system::replace_variables_capture_avoiding(const T &x, Substitution &sigma, const VariableContainer &sigma_variables, typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type * = nullptr)

Applies sigma as a capture avoiding substitution to x.

Parameters:

  • x The object to which the substiution is applied.
  • sigma A mutable substitution.
  • sigma_variables a container of variables.

Pre: { sigma_variables must contain the free variables appearing in the right hand side of sigma }.

void mcrl2::pbes_system::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::pbes_system::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.