mcrl2::data::rewriter

Include file:

#include "mcrl2/data/rewriter.h
class mcrl2::data::rewriter

Rewriter that operates on data expressions.

As long as normalisation of sorts remains necessary, the data specification object used for construction must exist during the lifetime of the rewriter object.

Public types

type mcrl2::data::rewriter::substitution_type

typedef for basic_rewriter< data_expression >::substitution_type

Protected static member functions

static const data_specification &default_specification()

Default specification used if no specification is specified at construction.

static substitution_type &empty_substitution()

Protected member functions

rewriter(const std::shared_ptr<detail::Rewriter> &r)

Constructor for internal use.

Parameters:

  • r A rewriter

Public member functions

rewriter clone()

Create a clone of the rewriter in which the underlying rewriter is copied, and not passed as a shared pointer.

This is useful when the rewriter is used in different parallel processes. One rewriter can only be used sequentially.

Returns: A rewriter, with a copy of the underlying jitty, jittyc or jittyp rewriting engine.

data_expression operator()(const data_expression &d) const

Rewrites a data expression.

Parameters:

  • d A data expression.

Returns: The normal form of d.

data_expression operator()(const data_expression &d, const SubstitutionFunction &sigma) const

Rewrites the data expression d, and on the fly applies a substitution function. to data variables.

Parameters:

  • d A data expression.
  • sigma A substitution function.

Returns: The normal form of the term.

data_expression operator()(const data_expression &d, substitution_type &sigma) const

Rewrites the data expression d, and on the fly applies a substitution function to data variables.

Parameters:

  • d A data expression.
  • sigma A substitution function.

Returns: The normal form of the term.

void operator()(data_expression &result, const data_expression &d, const SubstitutionFunction &sigma) const

Rewrites the data expression d, and on the fly applies a substitution function. to data variables.

Parameters:

  • result The normal form of the term is placed in result.
  • d A data expression.
  • sigma A substitution function.
void operator()(data_expression &result, const data_expression &d, substitution_type &sigma) const

Rewrites the data expression d, and on the fly applies a substitution function to data variables.

Parameters:

  • result The normal form of the term is put in resul is put in result
  • d A data expression.
  • sigma A substitutionA. function
rewriter(const data_specification &d, const EquationSelector &selector, const strategy s = jitty)

Constructor.

Parameters:

  • d A data specification
  • selector A component that selects the equations that are converted to rewrite rules
  • s A rewriter strategy.
rewriter(const data_specification &d = rewriter::default_specification(), const strategy s = jitty)

Constructor.

Parameters:

  • d A data specification
  • s A rewriter strategy.
rewriter(const rewriter &r) = default

Constructor.

Parameters:

  • r a rewriter.
void thread_initialise()

Initialises this rewriter with thread dependent information.

This function sets a pointer to the m_busy_flag and m_forbidden_flag of this. process, such that rewriter can access these faster than via the general thread. local mechanism. It is expected that this is not needed when compilers become. faster, and should be removed in due time.

~rewriter()