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()

Public member functions

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.

rewriter(const rewriter &r) = default

Constructor.

Parameters:

  • r a rewriter.

rewriter(const data_specification &d = rewriter::default_specification(), const strategy s = jitty)

Constructor.

Parameters:

  • d A data specification

  • s A rewriter strategy.

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()