mcrl2::data::detail::RewriterProver Class Reference

#include <with_prover.h>

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

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
	RewriterProver (const data_specification &data_spec, mcrl2::data::rewriter::strategy strat, const used_data_equation_selector &equations_selector)
virtual	~RewriterProver ()
rewrite_strategy	getStrategy ()
	Get rewriter strategy that is used.
void	rewrite (data_expression &result, const data_expression &t, substitution_type &sigma)
	Rewrite an mCRL2 data term.
data_expression	rewrite (const data_expression &t, substitution_type &sigma)
	Rewrite an mCRL2 data term.
void	thread_initialise ()
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 ()

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

Protected Member Functions
	RewriterProver (const RewriterProver &other)=delete
	RewriterProver (const RewriterProver &rewr, BDD_Prover prover_obj_)
std::shared_ptr< Rewriter >	clone ()
	Clone a rewriter.
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)

Additional Inherited Members
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 24 of file with_prover.h.

Member Typedef Documentation

substitution_type

typedef Rewriter::substitution_type mcrl2::data::detail::RewriterProver::substitution_type

Definition at line 29 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 32 of file with_prover.h.

~RewriterProver()

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

inlinevirtual

Definition at line 40 of file with_prover.h.

RewriterProver() [2/3]

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

protecteddelete

RewriterProver() [3/3]

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

inlineprotected

Definition at line 102 of file with_prover.h.

Member Function Documentation

clone()

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

inlineprotectedvirtual

Clone a rewriter.

Returns

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

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

Definition at line 110 of file with_prover.h.

getStrategy()

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

inlinevirtual

Get rewriter strategy that is used.

Returns

Used rewriter strategy.

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

Definition at line 43 of file with_prover.h.

rewrite() [1/2]

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

inlinevirtual

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

rewrite() [2/2]

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

inlinevirtual

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

thread_initialise()

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

inlinevirtual

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

Definition at line 90 of file with_prover.h.

Member Data Documentation

prover_obj

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

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