mCRL2
Loading...
Searching...
No Matches
mcrl2::data::detail::Rewriter Class Referenceabstract

Rewriter interface class. More...

#include <rewrite.h>

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

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_generatoridentifier_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::Rewriterclone ()=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.
 
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

Rewriteroperator= (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;
Rewriter interface class.
Definition rewrite.h:42
virtual data_expression rewrite(const data_expression &term, substitution_type &sigma)=0
Rewrite an mCRL2 data term.
std::shared_ptr< detail::Rewriter > createRewriter(const data_specification &DataSpec, const used_data_equation_selector &equations_selector, const rewrite_strategy Strategy=jitty)
Create a rewriter.
Definition rewrite.cpp:504

Definition at line 41 of file rewrite.h.

Member Typedef Documentation

◆ substitution_type

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 325 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 341 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 377 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
TermThe 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
TermThe 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 
)

Definition at line 247 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 
)

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 224 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 353 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 366 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 230 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: