mCRL2
Loading...
Searching...
No Matches
mcrl2::data::rewriter Class Reference

Rewriter that operates on data expressions. More...

#include <rewriter.h>

Inheritance diagram for mcrl2::data::rewriter:
mcrl2::data::basic_rewriter< data_expression > mcrl2::data::detail::BDD_Prover

Public Types

typedef basic_rewriter< data_expression >::substitution_type substitution_type
 
- Public Types inherited from mcrl2::data::basic_rewriter< data_expression >
typedef data::mutable_indexed_substitution substitution_type
 The type for the substitution that is used internally.
 
typedef data_expression term_type
 The type for expressions manipulated by the rewriter.
 
typedef rewrite_strategy strategy
 The rewrite strategies of the rewriter.
 

Public Member Functions

 rewriter (const rewriter &r)=default
 Constructor.
 
 rewriter (const data_specification &d=rewriter::default_specification(), const strategy s=jitty)
 Constructor.
 
template<typename EquationSelector >
 rewriter (const data_specification &d, const EquationSelector &selector, const strategy s=jitty)
 Constructor.
 
rewriter clone ()
 Create a clone of the rewriter in which the underlying rewriter is copied, and not passed as a shared pointer.
 
void thread_initialise ()
 Initialises this rewriter with thread dependent information.
 
data_expression operator() (const data_expression &d) const
 Rewrites a data expression.
 
template<typename SubstitutionFunction >
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.
 
template<typename SubstitutionFunction >
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.
 
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.
 
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.
 
 ~rewriter ()
 

Protected Member Functions

 rewriter (const std::shared_ptr< detail::Rewriter > &r)
 Constructor for internal use.
 
- Protected Member Functions inherited from mcrl2::data::basic_rewriter< data_expression >
 basic_rewriter (const std::shared_ptr< detail::Rewriter > &r)
 Constructor.
 
 basic_rewriter (const basic_rewriter &other)=default
 Copy Constructor.
 
 basic_rewriter (const data_specification &d, const strategy s=jitty)
 Constructor.
 
 basic_rewriter (const data_specification &d, const used_data_equation_selector &equation_selector, const strategy s=jitty)
 Constructor.
 
basic_rewriteroperator= (const basic_rewriter &other)=default
 Assignment operator.
 

Static Protected Member Functions

static substitution_typeempty_substitution ()
 
static const data_specificationdefault_specification ()
 Default specification used if no specification is specified at construction.
 

Additional Inherited Members

- Protected Attributes inherited from mcrl2::data::basic_rewriter< data_expression >
std::shared_ptr< detail::Rewriterm_rewriter
 The wrapped Rewriter.
 

Detailed Description

Rewriter that operates on data expressions.

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

Definition at line 80 of file rewriter.h.

Member Typedef Documentation

◆ substitution_type

Definition at line 114 of file rewriter.h.

Constructor & Destructor Documentation

◆ rewriter() [1/4]

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

Constructor for internal use.

Parameters
[in]rA rewriter

Definition at line 105 of file rewriter.h.

◆ rewriter() [2/4]

mcrl2::data::rewriter::rewriter ( const rewriter r)
default

Constructor.

Parameters
[in]ra rewriter.

◆ rewriter() [3/4]

mcrl2::data::rewriter::rewriter ( const data_specification d = rewriter::default_specification(),
const strategy  s = jitty 
)
inlineexplicit

Constructor.

Parameters
[in]dA data specification
[in]sA rewriter strategy.

Definition at line 123 of file rewriter.h.

◆ rewriter() [4/4]

template<typename EquationSelector >
mcrl2::data::rewriter::rewriter ( const data_specification d,
const EquationSelector &  selector,
const strategy  s = jitty 
)
inline

Constructor.

Parameters
[in]dA data specification
[in]selectorA component that selects the equations that are converted to rewrite rules
[in]sA rewriter strategy.

Definition at line 132 of file rewriter.h.

◆ ~rewriter()

mcrl2::data::rewriter::~rewriter ( )
inline

Definition at line 232 of file rewriter.h.

Member Function Documentation

◆ clone()

rewriter mcrl2::data::rewriter::clone ( )
inline

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.

Definition at line 140 of file rewriter.h.

◆ default_specification()

static const data_specification & mcrl2::data::rewriter::default_specification ( )
inlinestaticprotected

Default specification used if no specification is specified at construction.

Definition at line 97 of file rewriter.h.

◆ empty_substitution()

static substitution_type & mcrl2::data::rewriter::empty_substitution ( )
inlinestaticprotected

Definition at line 84 of file rewriter.h.

◆ operator()() [1/5]

data_expression mcrl2::data::rewriter::operator() ( const data_expression d) const
inline

Rewrites a data expression.

Parameters
[in]dA data expression.
Returns
The normal form of d.

Definition at line 158 of file rewriter.h.

◆ operator()() [2/5]

template<typename SubstitutionFunction >
data_expression mcrl2::data::rewriter::operator() ( const data_expression d,
const SubstitutionFunction &  sigma 
) const
inline

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

Parameters
[in]dA data expression.
[in]sigmaA substitution function.
Returns
The normal form of the term.

Definition at line 169 of file rewriter.h.

◆ operator()() [3/5]

data_expression mcrl2::data::rewriter::operator() ( const data_expression d,
substitution_type sigma 
) const
inline

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

Parameters
[in]dA data expression.
[in]sigmaA substitution function.
Returns
The normal form of the term.

Definition at line 204 of file rewriter.h.

◆ operator()() [4/5]

template<typename SubstitutionFunction >
void mcrl2::data::rewriter::operator() ( data_expression result,
const data_expression d,
const SubstitutionFunction &  sigma 
) const
inline

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

Parameters
[out]resultThe normal form of the term is placed in result.
[in]dA data expression.
[in]sigmaA substitution function.

Definition at line 186 of file rewriter.h.

◆ operator()() [5/5]

void mcrl2::data::rewriter::operator() ( data_expression result,
const data_expression d,
substitution_type sigma 
) const
inline

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

Parameters
[out]resultThe normal form of the term is put in resul is put in result
[in]dA data expression.
[in]sigmaA substitutionA. function

Definition at line 218 of file rewriter.h.

◆ thread_initialise()

void mcrl2::data::rewriter::thread_initialise ( )
inline

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.

Definition at line 150 of file rewriter.h.


The documentation for this class was generated from the following file: