#include <rewrite.h>

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

Public Types
using	substitution_type = mutable_indexed_substitution<>

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 ()=default
	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, bool t1_is_normal_form=false)

void	existential_quantifier_enumeration (data_expression &result, const variable_list &vl, const data_expression &t1, substitution_type &sigma, bool t1_is_normal_form=false)

void	universal_quantifier_enumeration (data_expression &result, const abstraction &t, substitution_type &sigma, bool t1_is_normal_form=false)

void	universal_quantifier_enumeration (data_expression &result, const variable_list &vl, const data_expression &t1, substitution_type &sigma, bool t1_is_normal_form=false)

void	rewrite_where (data_expression &result, const where_clause &term, substitution_type &sigma)

void	rewrite_single_lambda (data_expression &result, const variable_list &vl, const data_expression &body, substitution_type &sigma, bool body_in_normal_form)

void	rewrite_lambda_application (data_expression &result, const data_expression &t, substitution_type &sigma, bool arguments_are_in_normal_form=false)
	Rewrite t, assuming that the headsymbol of t, which can be nested, is a lambda term.

void	rewrite_lambda_application (data_expression &result, const abstraction &lambda_term, const application &t, substitution_type &sigma, bool arguments_are_in_normal_form=false)

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, 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 follows (with t a term in the mCRL2 internal format):

std::shared_ptr<Rewriter> r = createRewriter(equations);

t = r->rewrite(t);

mcrl2::data::detail::createRewriter

std::shared_ptr< detail::Rewriter > createRewriter(const data_specification &DataSpec, const used_data_equation_selector &equations_selector, rewrite_strategy Strategy=jitty)

Create a rewriter.

Definition rewrite.cpp:498

Definition at line 38 of file rewrite.h.

Member Typedef Documentation

◆ substitution_type

using mcrl2::data::detail::Rewriter::substitution_type = mutable_indexed_substitution<>

Definition at line 52 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 60 of file rewrite.h.

◆ ~Rewriter()

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

virtualdefault

Destructor.

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/2]

void mcrl2::data::detail::Rewriter::existential_quantifier_enumeration	(	data_expression &	result,
		const abstraction &	t,
		substitution_type &	sigma,
		bool	t1_is_normal_form = `false`
	)

Definition at line 319 of file rewrite.cpp.

◆ existential_quantifier_enumeration() [2/2]

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

Definition at line 336 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 70 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 100 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,
		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 373 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/2]

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

Definition at line 230 of file rewrite.cpp.

◆ rewrite_lambda_application() [2/2]

void mcrl2::data::detail::Rewriter::rewrite_lambda_application	(	data_expression &	result,
		const data_expression &	t,
		substitution_type &	sigma,
		bool	arguments_are_in_normal_form = `false`
	)

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

Definition at line 205 of file rewrite.cpp.

◆ rewrite_single_lambda()

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

Definition at line 100 of file rewrite.cpp.

◆ rewrite_where()

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

Definition at line 61 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 163 of file rewrite.h.

◆ universal_quantifier_enumeration() [1/2]

void mcrl2::data::detail::Rewriter::universal_quantifier_enumeration	(	data_expression &	result,
		const abstraction &	t,
		substitution_type &	sigma,
		bool	t1_is_normal_form = `false`
	)

Definition at line 348 of file rewrite.cpp.

◆ universal_quantifier_enumeration() [2/2]

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

Definition at line 362 of file rewrite.cpp.

Member Data Documentation

◆ data_equation_selector

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

Definition at line 54 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 169 of file rewrite.h.

◆ m_generator

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

protected

Definition at line 41 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

Public Types

Public Member Functions

Public Attributes

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ substitution_type

Constructor & Destructor Documentation

◆ Rewriter() [1/2]

◆ Rewriter() [2/2]

◆ ~Rewriter()

Member Function Documentation

◆ clone()

◆ existential_quantifier_enumeration() [1/2]

◆ existential_quantifier_enumeration() [2/2]

◆ getStrategy()

◆ identifier_generator()

◆ operator()()

◆ operator=()

◆ quantifier_enumeration()

◆ rewrite() [1/2]

◆ rewrite() [2/2]

◆ rewrite_lambda_application() [1/2]

◆ rewrite_lambda_application() [2/2]

◆ rewrite_single_lambda()

◆ rewrite_where()

◆ thread_initialise()

◆ universal_quantifier_enumeration() [1/2]

◆ universal_quantifier_enumeration() [2/2]

Member Data Documentation

◆ data_equation_selector

◆ m_data_specification_for_enumeration

◆ m_generator