Rewriter that operates on data expressions. More...

#include <rewriter.h>

Inheritance diagram for mcrl2::data::rewriter:

Public Types
using	substitution_type = basic_rewriter< data_expression >::substitution_type

Public Types inherited from mcrl2::data::basic_rewriter< data_expression >
using	substitution_type = data::mutable_indexed_substitution<>
	The type for the substitution that is used internally.

using	term_type = data_expression
	The type for expressions manipulated by the rewriter.

using	strategy = rewrite_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=rewrite_strategy::jitty)
	Constructor.

template<typename EquationSelector >
	rewriter (const data_specification &d, const EquationSelector &selector, const strategy s=rewrite_strategy::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.

void	operator() (data_expression &result, const data_expression &d) const
	Rewrites a data expression.

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

Public Member Functions inherited from mcrl2::data::basic_rewriter< data_expression >
const data::enumerator_identifier_generator &	identifier_generator () const
	Expose the identifier generator present in m_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=rewrite_strategy::jitty)
	Constructor.

	basic_rewriter (const data_specification &d, const used_data_equation_selector &equation_selector, const strategy s=rewrite_strategy::jitty)
	Constructor.

basic_rewriter &	operator= (const basic_rewriter &other)=default
	Assignment operator.

Static Protected Member Functions
static substitution_type &	empty_substitution ()

static const data_specification &	default_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::Rewriter >	m_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 83 of file rewriter.h.

Member Typedef Documentation

◆ substitution_type

using mcrl2::data::rewriter::substitution_type = basic_rewriter<data_expression>::substitution_type

Definition at line 117 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] r A rewriter

Definition at line 108 of file rewriter.h.

◆ rewriter() [2/4]

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

default

Constructor.

Parameters

[in] r a rewriter.

◆ rewriter() [3/4]

mcrl2::data::rewriter::rewriter	(	const data_specification &	d = `rewriter::default_specification()`,
		const strategy	s = `rewrite_strategy::jitty`
	)

inlineexplicit

Constructor.

Parameters

[in]	d	A data specification
[in]	s	A rewriter strategy.

Definition at line 126 of file rewriter.h.

◆ rewriter() [4/4]

template<typename EquationSelector >

mcrl2::data::rewriter::rewriter	(	const data_specification &	d,
		const EquationSelector &	selector,
		const strategy	s = `rewrite_strategy::jitty`
	)

inline

Constructor.

Parameters

[in]	d	A data specification
[in]	selector	A component that selects the equations that are converted to rewrite rules
[in]	s	A rewriter strategy.

Definition at line 135 of file rewriter.h.

◆ ~rewriter()

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

inline

Definition at line 239 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 143 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 100 of file rewriter.h.

◆ empty_substitution()

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

inlinestaticprotected

Definition at line 87 of file rewriter.h.

◆ operator()() [1/6]

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

inline

Rewrites a data expression.

Parameters

[in] d A data expression.

Returns: The normal form of d.

Definition at line 161 of file rewriter.h.

◆ operator()() [2/6]

template<IsSubstitution 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]	d	A data expression.
[in]	sigma	A substitution function.

Returns: The normal form of the term.

Definition at line 180 of file rewriter.h.

◆ operator()() [3/6]

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]	d	A data expression.
[in]	sigma	A substitution function.

Returns: The normal form of the term.

Definition at line 211 of file rewriter.h.

◆ operator()() [4/6]

void mcrl2::data::rewriter::operator()	(	data_expression &	result,
		const data_expression &	d
	)		const

inline

Rewrites a data expression.

Parameters

[in] d A data expression.

Returns: The normal form of d.

Definition at line 169 of file rewriter.h.

◆ operator()() [5/6]

template<IsSubstitution 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]	result	The normal form of the term is placed in result.
[in]	d	A data expression.
[in]	sigma	A substitution function.

Definition at line 193 of file rewriter.h.

◆ operator()() [6/6]

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]	result	The normal form of the term is put in resul is put in result
[in]	d	A data expression.
[in]	sigma	A substitutionA. function

Definition at line 225 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 153 of file rewriter.h.

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

data/include/mcrl2/data/rewriter.h

Public Types

Public Member Functions

Protected Member Functions

Static Protected Member Functions

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ substitution_type

Constructor & Destructor Documentation

◆ rewriter() [1/4]

◆ rewriter() [2/4]

◆ rewriter() [3/4]

◆ rewriter() [4/4]

◆ ~rewriter()

Member Function Documentation

◆ clone()

◆ default_specification()

◆ empty_substitution()

◆ operator()() [1/6]

◆ operator()() [2/6]

◆ operator()() [3/6]

◆ operator()() [4/6]

◆ operator()() [5/6]

◆ operator()() [6/6]

◆ thread_initialise()