mCRL2
Loading...
Searching...
No Matches
Public Types | Public Member Functions | Protected Attributes | List of all members
mcrl2::pbes_system::enumerate_quantifiers_rewriter Struct Reference

An attempt for improving the efficiency. More...

#include <enumerate_quantifiers_rewriter.h>

Public Types

typedef pbes_expression term_type
 
typedef data::variable variable_type
 

Public Member Functions

 enumerate_quantifiers_rewriter (const data::rewriter &R, const data::data_specification &dataspec, bool enumerate_infinite_sorts=true)
 
pbes_expression operator() (const pbes_expression &x) const
 
template<typename MutableSubstitution >
pbes_expression operator() (const pbes_expression &x, MutableSubstitution &sigma) const
 
template<typename MutableSubstitution >
void operator() (pbes_expression &result, const pbes_expression &x, MutableSubstitution &sigma) const
 
void clear_identifier_generator ()
 
enumerate_quantifiers_rewriter clone ()
 Create a clone of the rewriter in which the underlying rewriter is copied, and not passed as a shared pointer.
 
void thread_initialise ()
 Initialises this rewriter with thread dependent information.
 

Protected Attributes

data::rewriter m_rewriter
 A data rewriter.
 
data::data_specification m_dataspec
 A data specification.
 
bool m_enumerate_infinite_sorts
 If true, quantifier variables of infinite sort are enumerated.
 
data::enumerator_identifier_generator m_id_generator
 

Detailed Description

An attempt for improving the efficiency.

Definition at line 275 of file enumerate_quantifiers_rewriter.h.

Member Typedef Documentation

◆ term_type

typedef pbes_expression mcrl2::pbes_system::enumerate_quantifiers_rewriter::term_type

Definition at line 290 of file enumerate_quantifiers_rewriter.h.

◆ variable_type

typedef data::variable mcrl2::pbes_system::enumerate_quantifiers_rewriter::variable_type

Definition at line 291 of file enumerate_quantifiers_rewriter.h.

Constructor & Destructor Documentation

◆ enumerate_quantifiers_rewriter()

mcrl2::pbes_system::enumerate_quantifiers_rewriter::enumerate_quantifiers_rewriter ( const data::rewriter &  R,
const data::data_specification &  dataspec,
bool  enumerate_infinite_sorts = true 
)
inline

Definition at line 293 of file enumerate_quantifiers_rewriter.h.

Member Function Documentation

◆ clear_identifier_generator()

void mcrl2::pbes_system::enumerate_quantifiers_rewriter::clear_identifier_generator ( )
inline

Definition at line 319 of file enumerate_quantifiers_rewriter.h.

◆ clone()

enumerate_quantifiers_rewriter mcrl2::pbes_system::enumerate_quantifiers_rewriter::clone ( )
inline

Create a clone of the rewriter in which the underlying rewriter is copied, and not passed as a shared pointer.

This is useful when the rewriter is used in different parallel processes. One rewriter can only be used sequentially.

Returns
A rewriter, with a copy of the underlying jitty, jittyc or jittyp rewriting engine.

Definition at line 327 of file enumerate_quantifiers_rewriter.h.

◆ operator()() [1/3]

pbes_expression mcrl2::pbes_system::enumerate_quantifiers_rewriter::operator() ( const pbes_expression &  x) const
inline

Definition at line 297 of file enumerate_quantifiers_rewriter.h.

◆ operator()() [2/3]

template<typename MutableSubstitution >
pbes_expression mcrl2::pbes_system::enumerate_quantifiers_rewriter::operator() ( const pbes_expression &  x,
MutableSubstitution &  sigma 
) const
inline

Definition at line 306 of file enumerate_quantifiers_rewriter.h.

◆ operator()() [3/3]

template<typename MutableSubstitution >
void mcrl2::pbes_system::enumerate_quantifiers_rewriter::operator() ( pbes_expression &  result,
const pbes_expression &  x,
MutableSubstitution &  sigma 
) const
inline

Definition at line 314 of file enumerate_quantifiers_rewriter.h.

◆ thread_initialise()

void mcrl2::pbes_system::enumerate_quantifiers_rewriter::thread_initialise ( )
inline

Initialises this rewriter with thread dependent information.

This function sets a pointer to the m_busy_flag and m_forbidden_flag of this. process, such that rewriter can access these faster than via the general thread. local mechanism. It is expected that this is not needed when compilers become. faster, and should be removed in due time.

Definition at line 337 of file enumerate_quantifiers_rewriter.h.

Member Data Documentation

◆ m_dataspec

data::data_specification mcrl2::pbes_system::enumerate_quantifiers_rewriter::m_dataspec
protected

A data specification.

Definition at line 282 of file enumerate_quantifiers_rewriter.h.

◆ m_enumerate_infinite_sorts

bool mcrl2::pbes_system::enumerate_quantifiers_rewriter::m_enumerate_infinite_sorts
protected

If true, quantifier variables of infinite sort are enumerated.

Definition at line 285 of file enumerate_quantifiers_rewriter.h.

◆ m_id_generator

data::enumerator_identifier_generator mcrl2::pbes_system::enumerate_quantifiers_rewriter::m_id_generator
mutableprotected

Definition at line 287 of file enumerate_quantifiers_rewriter.h.

◆ m_rewriter

data::rewriter mcrl2::pbes_system::enumerate_quantifiers_rewriter::m_rewriter
protected

A data rewriter.

Definition at line 279 of file enumerate_quantifiers_rewriter.h.

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