#include <with_prover.h>

Inheritance diagram for mcrl2::data::detail::RewriterProver:

Public Types
using	substitution_type = Rewriter::substitution_type

Public Types inherited from mcrl2::data::detail::Rewriter
using	substitution_type = mutable_indexed_substitution<>

Public Member Functions
	RewriterProver (const data_specification &data_spec, mcrl2::data::rewriter::strategy strat, const used_data_equation_selector &equations_selector)

	~RewriterProver () override=default

rewrite_strategy	getStrategy () override
	Get rewriter strategy that is used.

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

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

void	thread_initialise () override

	RewriterProver (const RewriterProver &other)=delete

	RewriterProver (const RewriterProver &rewr, BDD_Prover prover_obj_)

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

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 ()=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
BDD_Prover	prover_obj

Public Attributes inherited from mcrl2::data::detail::Rewriter
used_data_equation_selector	data_equation_selector

Additional Inherited Members
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, 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 inherited from mcrl2::data::detail::Rewriter
enumerator_identifier_generator	m_generator

mcrl2::data::data_specification	m_data_specification_for_enumeration

Detailed Description

Definition at line 20 of file with_prover.h.

Member Typedef Documentation

◆ substitution_type

using mcrl2::data::detail::RewriterProver::substitution_type = Rewriter::substitution_type

Definition at line 25 of file with_prover.h.

Constructor & Destructor Documentation

◆ RewriterProver() [1/3]

mcrl2::data::detail::RewriterProver::RewriterProver	(	const data_specification &	data_spec,
		mcrl2::data::rewriter::strategy	strat,
		const used_data_equation_selector &	equations_selector
	)

inline

Definition at line 28 of file with_prover.h.

◆ ~RewriterProver()

mcrl2::data::detail::RewriterProver::~RewriterProver ( )

overridedefault

◆ RewriterProver() [2/3]

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

delete

◆ RewriterProver() [3/3]

mcrl2::data::detail::RewriterProver::RewriterProver	(	const RewriterProver &	rewr,
		BDD_Prover	prover_obj_
	)

inline

Definition at line 88 of file with_prover.h.

Member Function Documentation

◆ clone()

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

inlineoverridevirtual

Clone a rewriter.

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

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

Definition at line 96 of file with_prover.h.

◆ getStrategy()

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

inlineoverridevirtual

Get rewriter strategy that is used.

Returns: Used rewriter strategy.

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

Definition at line 38 of file with_prover.h.

◆ rewrite() [1/2]

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

inlineoverridevirtual

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 68 of file with_prover.h.

◆ rewrite() [2/2]

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

inlineoverridevirtual

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 53 of file with_prover.h.

◆ thread_initialise()

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

inlineoverridevirtual

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

Definition at line 75 of file with_prover.h.

Member Data Documentation

◆ prover_obj

BDD_Prover mcrl2::data::detail::RewriterProver::prover_obj

Definition at line 23 of file with_prover.h.

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

data/include/mcrl2/data/detail/rewrite/with_prover.h

Public Types

Public Member Functions

Public Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ substitution_type

Constructor & Destructor Documentation

◆ RewriterProver() [1/3]

◆ ~RewriterProver()

◆ RewriterProver() [2/3]

◆ RewriterProver() [3/3]

Member Function Documentation

◆ clone()

◆ getStrategy()

◆ rewrite() [1/2]

◆ rewrite() [2/2]

◆ thread_initialise()

Member Data Documentation

◆ prover_obj