#include <jitty.h>

Inheritance diagram for mcrl2::data::detail::RewriterJitty:

Public Types
typedef Rewriter::substitution_type	substitution_type

Public Types inherited from mcrl2::data::detail::Rewriter
typedef mutable_indexed_substitution	substitution_type

Public Member Functions
	RewriterJitty (const data_specification &data_spec, const used_data_equation_selector &)

	RewriterJitty (const RewriterJitty &other)=default

RewriterJitty &	operator= (const RewriterJitty &other)=delete

virtual	~RewriterJitty ()

rewrite_strategy	getStrategy ()
	Get rewriter strategy that is used.

data_expression	rewrite (const data_expression &term, substitution_type &sigma)
	Rewrite an mCRL2 data term.

void	rewrite (data_expression &result, const data_expression &term, substitution_type &sigma)
	Rewrite an mCRL2 data term.

std::shared_ptr< detail::Rewriter >	clone ()
	Clone a rewriter.

const function_symbol &	this_term_is_in_normal_form ()

Public Member Functions inherited from mcrl2::data::detail::Rewriter
	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 ()

Protected Member Functions
template<class ITERATOR >
void	apply_cpp_code_to_higher_order_term (data_expression &result, const application &t, const std::function< void(data_expression &, const data_expression &)> rewrite_cpp_code, ITERATOR begin, ITERATOR end, substitution_type &sigma)

void	rewrite_aux (data_expression &result, const data_expression &term, substitution_type &sigma)
	Rewrite a term with a given substitution and put the rewritten term in result.

void	rewrite_aux_function_symbol (data_expression &result, const function_symbol &op, const application &term, substitution_type &sigma)

void	rewrite_aux_const_function_symbol (data_expression &result, const function_symbol &op, substitution_type &sigma)

void	make_jitty_strat_sufficiently_larger (const std::size_t i)
	Auxiliary function to take care that the array jitty_strat is sufficiently large to access element i.

strategy	create_a_cpp_function_based_strategy (const function_symbol &f, const data_specification &data_spec)

strategy	create_a_rewriting_based_strategy (const function_symbol &f, const data_equation_list &rules1)

strategy	create_strategy (const function_symbol &f, const data_equation_list &rules1, const data_specification &data_spec)

void	rebuild_strategy (const data_specification &data_spec, const mcrl2::data::used_data_equation_selector &equation_selector)

data_expression	remove_normal_form_function (const data_expression &t)

void	subst_values (data_expression &result, const jitty_assignments_for_a_rewrite_rule &assignments, const data_expression &t, data::enumerator_identifier_generator &generator)

void	thread_initialise ()

Protected Member Functions inherited from mcrl2::data::detail::Rewriter
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
function_symbol	this_term_is_in_normal_form_symbol

bool	rewriting_in_progress

class rewrite_stack	m_rewrite_stack

std::vector< data_expression >	rhs_for_constants_cache

std::map< function_symbol, data_equation_list >	jitty_eqns

std::vector< strategy >	jitty_strat

atermpp::detail::thread_aterm_pool *	m_thread_aterm_pool

Protected Attributes inherited from mcrl2::data::detail::Rewriter
enumerator_identifier_generator	m_generator

mcrl2::data::data_specification	m_data_specification_for_enumeration

Friends
class	jitty_argument_rewriter

Additional Inherited Members
Public Attributes inherited from mcrl2::data::detail::Rewriter
used_data_equation_selector	data_equation_selector

Detailed Description

Definition at line 49 of file jitty.h.

Member Typedef Documentation

◆ substitution_type

typedef Rewriter::substitution_type mcrl2::data::detail::RewriterJitty::substitution_type

Definition at line 54 of file jitty.h.

Constructor & Destructor Documentation

◆ RewriterJitty() [1/2]

mcrl2::data::detail::RewriterJitty::RewriterJitty	(	const data_specification &	data_spec,
		const used_data_equation_selector &	equation_selector
	)

Definition at line 166 of file jitty.cpp.

◆ RewriterJitty() [2/2]

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

default

◆ ~RewriterJitty()

mcrl2::data::detail::RewriterJitty::~RewriterJitty ( )

virtual

Definition at line 206 of file jitty.cpp.

Member Function Documentation

◆ apply_cpp_code_to_higher_order_term()

template<class ITERATOR >

void mcrl2::data::detail::RewriterJitty::apply_cpp_code_to_higher_order_term	(	data_expression &	result,
		const application &	t,
		const std::function< void(data_expression &, const data_expression &)>	rewrite_cpp_code,
		ITERATOR	begin,
		ITERATOR	end,
		substitution_type &	sigma
	)

protected

Definition at line 404 of file jitty.cpp.

◆ clone()

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

inlinevirtual

Clone a rewriter.

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

Implements mcrl2::data::detail::Rewriter.

Definition at line 72 of file jitty.h.

◆ create_a_cpp_function_based_strategy()

strategy mcrl2::data::detail::RewriterJitty::create_a_cpp_function_based_strategy	(	const function_symbol &	f,
		const data_specification &	data_spec
	)

protected

Definition at line 222 of file strategy.cpp.

◆ create_a_rewriting_based_strategy()

strategy mcrl2::data::detail::RewriterJitty::create_a_rewriting_based_strategy	(	const function_symbol &	f,
		const data_equation_list &	rules1
	)

protected

Definition at line 46 of file strategy.cpp.

◆ create_strategy()

strategy mcrl2::data::detail::RewriterJitty::create_strategy	(	const function_symbol &	f,
		const data_equation_list &	rules1,
		const data_specification &	data_spec
	)

protected

Definition at line 242 of file strategy.cpp.

◆ getStrategy()

rewrite_strategy mcrl2::data::detail::RewriterJitty::getStrategy ( )

virtual

Get rewriter strategy that is used.

Returns: Used rewriter strategy.

Implements mcrl2::data::detail::Rewriter.

Definition at line 917 of file jitty.cpp.

◆ make_jitty_strat_sufficiently_larger()

void mcrl2::data::detail::RewriterJitty::make_jitty_strat_sufficiently_larger ( const std::size_t i )

protected

Auxiliary function to take care that the array jitty_strat is sufficiently large to access element i.

Definition at line 136 of file jitty.cpp.

◆ operator=()

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

delete

◆ rebuild_strategy()

void mcrl2::data::detail::RewriterJitty::rebuild_strategy	(	const data_specification &	data_spec,
		const mcrl2::data::used_data_equation_selector &	equation_selector
	)

protected

Definition at line 144 of file jitty.cpp.

◆ remove_normal_form_function()

data_expression mcrl2::data::detail::RewriterJitty::remove_normal_form_function ( const data_expression & t )

protected

Definition at line 38 of file jitty.cpp.

◆ rewrite() [1/2]

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

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.

Implements mcrl2::data::detail::Rewriter.

Definition at line 907 of file jitty.cpp.

◆ rewrite() [2/2]

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

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.

Implements mcrl2::data::detail::Rewriter.

Definition at line 870 of file jitty.cpp.

◆ rewrite_aux()

void mcrl2::data::detail::RewriterJitty::rewrite_aux	(	data_expression &	result,
		const data_expression &	term,
		substitution_type &	sigma
	)

protected

Rewrite a term with a given substitution and put the rewritten term in result.

Definition at line 433 of file jitty.cpp.

◆ rewrite_aux_const_function_symbol()

void mcrl2::data::detail::RewriterJitty::rewrite_aux_const_function_symbol	(	data_expression &	result,
		const function_symbol &	op,
		substitution_type &	sigma
	)

protected

Definition at line 794 of file jitty.cpp.

◆ rewrite_aux_function_symbol()

void mcrl2::data::detail::RewriterJitty::rewrite_aux_function_symbol	(	data_expression &	result,
		const function_symbol &	op,
		const application &	term,
		substitution_type &	sigma
	)

protected

Definition at line 569 of file jitty.cpp.

◆ subst_values()

void mcrl2::data::detail::RewriterJitty::subst_values	(	data_expression &	result,
		const jitty_assignments_for_a_rewrite_rule &	assignments,
		const data_expression &	t,
		data::enumerator_identifier_generator &	generator
	)

protected

Definition at line 210 of file jitty.cpp.

◆ this_term_is_in_normal_form()

const function_symbol & mcrl2::data::detail::RewriterJitty::this_term_is_in_normal_form ( )

inline

Definition at line 77 of file jitty.h.

◆ thread_initialise()

void mcrl2::data::detail::RewriterJitty::thread_initialise ( )

inlineprotectedvirtual

Reimplemented from mcrl2::data::detail::Rewriter.

Definition at line 138 of file jitty.h.

Friends And Related Symbol Documentation

◆ jitty_argument_rewriter

friend class jitty_argument_rewriter

friend

Definition at line 52 of file jitty.h.

Member Data Documentation

◆ jitty_eqns

std::map< function_symbol, data_equation_list > mcrl2::data::detail::RewriterJitty::jitty_eqns

protected

Definition at line 93 of file jitty.h.

◆ jitty_strat

std::vector<strategy> mcrl2::data::detail::RewriterJitty::jitty_strat

protected

Definition at line 94 of file jitty.h.

◆ m_rewrite_stack

class rewrite_stack mcrl2::data::detail::RewriterJitty::m_rewrite_stack

protected

Definition at line 90 of file jitty.h.

◆ m_thread_aterm_pool

atermpp::detail::thread_aterm_pool* mcrl2::data::detail::RewriterJitty::m_thread_aterm_pool

protected

Definition at line 96 of file jitty.h.

◆ rewriting_in_progress

bool mcrl2::data::detail::RewriterJitty::rewriting_in_progress

protected

Definition at line 88 of file jitty.h.

◆ rhs_for_constants_cache

std::vector<data_expression> mcrl2::data::detail::RewriterJitty::rhs_for_constants_cache

protected

Definition at line 92 of file jitty.h.

◆ this_term_is_in_normal_form_symbol

function_symbol mcrl2::data::detail::RewriterJitty::this_term_is_in_normal_form_symbol

protected

Definition at line 87 of file jitty.h.

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

data/include/mcrl2/data/detail/rewrite/jitty.h
data/source/detail/rewrite/jitty.cpp
data/source/detail/rewrite/strategy.cpp

Public Types

Public Member Functions

Protected Member Functions

Protected Attributes

Friends

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ substitution_type

Constructor & Destructor Documentation

◆ RewriterJitty() [1/2]

◆ RewriterJitty() [2/2]

◆ ~RewriterJitty()

Member Function Documentation

◆ apply_cpp_code_to_higher_order_term()

◆ clone()

◆ create_a_cpp_function_based_strategy()

◆ create_a_rewriting_based_strategy()

◆ create_strategy()

◆ getStrategy()

◆ make_jitty_strat_sufficiently_larger()

◆ operator=()

◆ rebuild_strategy()

◆ remove_normal_form_function()

◆ rewrite() [1/2]

◆ rewrite() [2/2]

◆ rewrite_aux()

◆ rewrite_aux_const_function_symbol()

◆ rewrite_aux_function_symbol()

◆ subst_values()

◆ this_term_is_in_normal_form()

◆ thread_initialise()

Friends And Related Symbol Documentation

◆ jitty_argument_rewriter

Member Data Documentation

◆ jitty_eqns

◆ jitty_strat

◆ m_rewrite_stack

◆ m_thread_aterm_pool

◆ rewriting_in_progress

◆ rhs_for_constants_cache

◆ this_term_is_in_normal_form_symbol