mcrl2/lps/rewrite.h

Include file:

#include "mcrl2/lps/rewrite.h"

add your file description here.

Functions

void mcrl2::lps::one_point_rule_rewrite(T &x, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

Applies the one point rule rewriter to all embedded data expressions in an object x.

Parameters:

  • x an object containing data expressions
T mcrl2::lps::one_point_rule_rewrite(const T &x, typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type * = nullptr)

Applies the one point rule rewriter to all embedded data expressions in an object x.

Parameters:

  • x an object containing data expressions

Returns: the rewrite result

void mcrl2::lps::rewrite(T &x, Rewriter R, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

Rewrites all embedded expressions in an object x.

Parameters:

  • x an object containing expressions
  • R a rewriter
T mcrl2::lps::rewrite(const T &x, Rewriter R, typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type * = nullptr)

Rewrites all embedded expressions in an object x.

Parameters:

  • x an object containing expressions
  • R a rewriter

Returns: the rewrite result

void mcrl2::lps::rewrite(T &x, Rewriter R, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

Rewrites all embedded expressions in an object x, and applies a substitution to variables on the fly.

Parameters:

  • x an object containing expressions
  • R a rewriter
  • sigma a substitution
T mcrl2::lps::rewrite(const T &x, Rewriter R, const Substitution &sigma, typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type * = nullptr)

Rewrites all embedded expressions in an object x, and applies a substitution to variables on the fly.

Parameters:

  • x an object containing expressions
  • R a rewriter
  • sigma a substitution

Returns: the rewrite result