mcrl2::data::detail::Rewriter Class Reference

Rewriter interface class. More...

#include <rewrite.h>

Inheritance diagram for mcrl2::data::detail::Rewriter:

Public Types
typedef mutable_indexed_substitution	substitution_type

Public Member Functions
	Rewriter (const data_specification &data_spec, const used_data_equation_selector &eq_selector)
	Constructor. Do not use directly; use createRewriter() function instead.
virtual	~Rewriter ()
	Destructor.
data::enumerator_identifier_generator &	identifier_generator ()
	The fresh name generator of the rewriter.
virtual rewrite_strategy	getStrategy ()=0
	Get rewriter strategy that is used.
virtual data_expression	rewrite (const data_expression &term, substitution_type &sigma)=0
	Rewrite an mCRL2 data term.
virtual void	rewrite (data_expression &result, const data_expression &term, substitution_type &sigma)=0
	Rewrite an mCRL2 data term.
data_expression	operator() (const data_expression &term, substitution_type &sigma)
	Provide the rewriter with a () operator, such that it can also rewrite terms using this operator.
virtual std::shared_ptr< detail::Rewriter >	clone ()=0
	Clone a rewriter.
void	existential_quantifier_enumeration (data_expression &result, const abstraction &t, substitution_type &sigma)
void	existential_quantifier_enumeration (data_expression &result, const variable_list &vl, const data_expression &t1, const bool t1_is_normal_form, substitution_type &sigma)
void	universal_quantifier_enumeration (data_expression &result, const abstraction &t, substitution_type &sigma)
void	universal_quantifier_enumeration (data_expression &result, const variable_list &vl, const data_expression &t1, const bool t1_is_normal_form, substitution_type &sigma)
data_expression	existential_quantifier_enumeration (const abstraction &t, substitution_type &sigma)
data_expression	existential_quantifier_enumeration (const variable_list &vl, const data_expression &t1, const bool t1_is_normal_form, substitution_type &sigma)
data_expression	universal_quantifier_enumeration (const abstraction &t, substitution_type &sigma)
data_expression	universal_quantifier_enumeration (const variable_list &vl, const data_expression &t1, const bool t1_is_normal_form, substitution_type &sigma)
void	rewrite_where (data_expression &result, const where_clause &term, substitution_type &sigma)
data_expression	rewrite_where (const where_clause &term, substitution_type &sigma)
void	rewrite_single_lambda (data_expression &result, const variable_list &vl, const data_expression &body, const bool body_in_normal_form, substitution_type &sigma)
data_expression	rewrite_single_lambda (const variable_list &vl, const data_expression &body, const bool body_in_normal_form, substitution_type &sigma)
void	rewrite_lambda_application (data_expression &result, const data_expression &t, substitution_type &sigma)
	Rewrite t, assuming that the headsymbol of t, which can be nested, is a lambda term.
data_expression	rewrite_lambda_application (const data_expression &t, substitution_type &sigma)
void	rewrite_lambda_application (data_expression &result, const abstraction &lambda_term, const application &t, substitution_type &sigma)
virtual void	thread_initialise ()

Public Attributes
used_data_equation_selector	data_equation_selector

Protected Member Functions
Rewriter &	operator= (const Rewriter &other)=default
	The copy assignment operator is protected. Public copying is not allowed.
	Rewriter (const Rewriter &other)=default
	The copy constructor operator is protected. Public copying is not allowed.
void	quantifier_enumeration (data_expression &result, const variable_list &vl, const data_expression &t1, const bool t1_is_normal_form, substitution_type &sigma, const binder_type &binder, data_expression(*lazy_op)(const data_expression &, const data_expression &), const data_expression &identity_element, const data_expression &absorbing_element)

Protected Attributes
enumerator_identifier_generator	m_generator
mcrl2::data::data_specification	m_data_specification_for_enumeration

Detailed Description

Rewriter interface class.

This is the interface class for the rewriters. To create a specific rewriter, use createRewriter.

Simple use of the rewriter would be as follow (with t a term in the mCRL2 internal format):

Rewriter *r = createRewriter(equations);
t = r->rewrite(t);
delete r;

Definition at line 41 of file rewrite.h.

Member Typedef Documentation

substitution_type

typedef mutable_indexed_substitution mcrl2::data::detail::Rewriter::substitution_type

Definition at line 55 of file rewrite.h.

Constructor & Destructor Documentation

Rewriter() [1/2]

mcrl2::data::detail::Rewriter::Rewriter ( const Rewriter &  other )

protecteddefault

The copy constructor operator is protected. Public copying is not allowed.

Rewriter() [2/2]

mcrl2::data::detail::Rewriter::Rewriter ( const data_specification &  data_spec, const used_data_equation_selector &  eq_selector  )

inline

Constructor. Do not use directly; use createRewriter() function instead.

See also

createRewriter()

Definition at line 63 of file rewrite.h.

~Rewriter()

virtual mcrl2::data::detail::Rewriter::~Rewriter ( )

inlinevirtual

Destructor.

Definition at line 70 of file rewrite.h.

Member Function Documentation

clone()

virtual std::shared_ptr< detail::Rewriter > mcrl2::data::detail::Rewriter::clone ( )

pure virtual

Clone a rewriter.

Returns

A (pointer to a) a clone of the rewriter.

Implemented in mcrl2::data::detail::RewriterJitty, and mcrl2::data::detail::RewriterProver.

existential_quantifier_enumeration() [1/4]

data_expression mcrl2::data::detail::Rewriter::existential_quantifier_enumeration ( const abstraction &  t, substitution_type &  sigma  )

inline

Definition at line 142 of file rewrite.h.

existential_quantifier_enumeration() [2/4]

data_expression mcrl2::data::detail::Rewriter::existential_quantifier_enumeration ( const variable_list &  vl, const data_expression &  t1, const bool  t1_is_normal_form, substitution_type &  sigma  )

inline

Definition at line 150 of file rewrite.h.

existential_quantifier_enumeration() [3/4]

void mcrl2::data::detail::Rewriter::existential_quantifier_enumeration	(	data_expression &	result,
		const abstraction &	t,
		substitution_type &	sigma
	)

Definition at line 334 of file rewrite.cpp.

existential_quantifier_enumeration() [4/4]

void mcrl2::data::detail::Rewriter::existential_quantifier_enumeration	(	data_expression &	result,
		const variable_list &	vl,
		const data_expression &	t1,
		const bool	t1_is_normal_form,
		substitution_type &	sigma
	)

Definition at line 350 of file rewrite.cpp.

getStrategy()

virtual rewrite_strategy mcrl2::data::detail::Rewriter::getStrategy ( )

pure virtual

Get rewriter strategy that is used.

Returns

Used rewriter strategy.

Implemented in mcrl2::data::detail::RewriterJitty, and mcrl2::data::detail::RewriterProver.

identifier_generator()

data::enumerator_identifier_generator & mcrl2::data::detail::Rewriter::identifier_generator ( )

inline

The fresh name generator of the rewriter.

Definition at line 75 of file rewrite.h.

operator()()

data_expression mcrl2::data::detail::Rewriter::operator() ( const data_expression &  term, substitution_type &  sigma  )

inline

Provide the rewriter with a () operator, such that it can also rewrite terms using this operator.

Definition at line 105 of file rewrite.h.

operator=()

Rewriter & mcrl2::data::detail::Rewriter::operator= ( const Rewriter &  other )

protecteddefault

The copy assignment operator is protected. Public copying is not allowed.

quantifier_enumeration()

void mcrl2::data::detail::Rewriter::quantifier_enumeration ( data_expression &  result, const variable_list &  vl, const data_expression &  t1, const bool  t1_is_normal_form, substitution_type &  sigma, const binder_type &  binder, data_expression(*)(const data_expression &, const data_expression &)  lazy_op, const data_expression &  identity_element, const data_expression &  absorbing_element  )

protected

Definition at line 386 of file rewrite.cpp.

rewrite() [1/2]

virtual data_expression mcrl2::data::detail::Rewriter::rewrite ( const data_expression &  term, substitution_type &  sigma  )

pure virtual

Rewrite an mCRL2 data term.

Parameters

Term	The term to be rewritten. This term should be a data_term

Returns

The normal form of Term.

Implemented in mcrl2::data::detail::RewriterProver, and mcrl2::data::detail::RewriterJitty.

rewrite() [2/2]

virtual void mcrl2::data::detail::Rewriter::rewrite ( data_expression &  result, const data_expression &  term, substitution_type &  sigma  )

pure virtual

Rewrite an mCRL2 data term.

Parameters

Term	The term to be rewritten. This term should be a data_term

Returns

The normal form of Term.

Implemented in mcrl2::data::detail::RewriterProver, and mcrl2::data::detail::RewriterJitty.

rewrite_lambda_application() [1/3]

data_expression mcrl2::data::detail::Rewriter::rewrite_lambda_application	(	const data_expression &	t,
		substitution_type &	sigma
	)

Definition at line 241 of file rewrite.cpp.

rewrite_lambda_application() [2/3]

void mcrl2::data::detail::Rewriter::rewrite_lambda_application	(	data_expression &	result,
		const abstraction &	lambda_term,
		const application &	t,
		substitution_type &	sigma
	)

Definition at line 256 of file rewrite.cpp.

rewrite_lambda_application() [3/3]

void mcrl2::data::detail::Rewriter::rewrite_lambda_application	(	data_expression &	result,
		const data_expression &	t,
		substitution_type &	sigma
	)

Rewrite t, assuming that the headsymbol of t, which can be nested, is a lambda term.

Definition at line 214 of file rewrite.cpp.

rewrite_single_lambda() [1/2]

data_expression mcrl2::data::detail::Rewriter::rewrite_single_lambda ( const variable_list &  vl, const data_expression &  body, const bool  body_in_normal_form, substitution_type &  sigma  )

inline

Definition at line 201 of file rewrite.h.

rewrite_single_lambda() [2/2]

void mcrl2::data::detail::Rewriter::rewrite_single_lambda	(	data_expression &	result,
		const variable_list &	vl,
		const data_expression &	body,
		const bool	body_in_normal_form,
		substitution_type &	sigma
	)

Definition at line 109 of file rewrite.cpp.

rewrite_where() [1/2]

data_expression mcrl2::data::detail::Rewriter::rewrite_where	(	const where_clause &	term,
		substitution_type &	sigma
	)

Definition at line 61 of file rewrite.cpp.

rewrite_where() [2/2]

void mcrl2::data::detail::Rewriter::rewrite_where	(	data_expression &	result,
		const where_clause &	term,
		substitution_type &	sigma
	)

Definition at line 70 of file rewrite.cpp.

thread_initialise()

virtual void mcrl2::data::detail::Rewriter::thread_initialise ( )

inlinevirtual

Reimplemented in mcrl2::data::detail::RewriterJitty, and mcrl2::data::detail::RewriterProver.

Definition at line 228 of file rewrite.h.

universal_quantifier_enumeration() [1/4]

data_expression mcrl2::data::detail::Rewriter::universal_quantifier_enumeration ( const abstraction &  t, substitution_type &  sigma  )

inline

Definition at line 161 of file rewrite.h.

universal_quantifier_enumeration() [2/4]

data_expression mcrl2::data::detail::Rewriter::universal_quantifier_enumeration ( const variable_list &  vl, const data_expression &  t1, const bool  t1_is_normal_form, substitution_type &  sigma  )

inline

Definition at line 170 of file rewrite.h.

universal_quantifier_enumeration() [3/4]

void mcrl2::data::detail::Rewriter::universal_quantifier_enumeration	(	data_expression &	result,
		const abstraction &	t,
		substitution_type &	sigma
	)

Definition at line 362 of file rewrite.cpp.

universal_quantifier_enumeration() [4/4]

void mcrl2::data::detail::Rewriter::universal_quantifier_enumeration	(	data_expression &	result,
		const variable_list &	vl,
		const data_expression &	t1,
		const bool	t1_is_normal_form,
		substitution_type &	sigma
	)

Definition at line 375 of file rewrite.cpp.

Member Data Documentation

data_equation_selector

used_data_equation_selector mcrl2::data::detail::Rewriter::data_equation_selector

Definition at line 57 of file rewrite.h.

m_data_specification_for_enumeration

mcrl2::data::data_specification mcrl2::data::detail::Rewriter::m_data_specification_for_enumeration

protected

Definition at line 234 of file rewrite.h.

m_generator

enumerator_identifier_generator mcrl2::data::detail::Rewriter::m_generator

protected

Definition at line 44 of file rewrite.h.

---

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

• data/include/mcrl2/data/detail/rewrite.h
• data/source/detail/rewrite/rewrite.cpp