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

using term_type = pbes_expression
 
using variable_type = data::variable
 

Public Member Functions

 enumerate_quantifiers_rewriter (const data::rewriter &R, const data::data_specification &dataspec, const enumerate_quantifiers_mode enum_mode=enumerate_quantifiers_mode::expand_infinite_sorts_and_use_data_rewriter)
 
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
 
template<typename MutableSubstitution , typename PbesSubstitution >
pbes_expression operator() (const pbes_expression &x, MutableSubstitution &sigma, const PbesSubstitution &sigma_pbes) const
 
template<typename MutableSubstitution , typename PbesSubstitution >
void operator() (pbes_expression &result, const pbes_expression &x, MutableSubstitution &sigma, const PbesSubstitution &sigma_pbes) 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.
 
enumerate_quantifiers_mode m_enum_mode
 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 336 of file enumerate_quantifiers_rewriter.h.

Member Typedef Documentation

◆ term_type

using mcrl2::pbes_system::enumerate_quantifiers_rewriter::term_type = pbes_expression

Definition at line 351 of file enumerate_quantifiers_rewriter.h.

◆ variable_type

using mcrl2::pbes_system::enumerate_quantifiers_rewriter::variable_type = data::variable

Definition at line 352 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,
const enumerate_quantifiers_mode  enum_mode = enumerate_quantifiers_mode::expand_infinite_sorts_and_use_data_rewriter 
)
inline

Definition at line 354 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 414 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 422 of file enumerate_quantifiers_rewriter.h.

◆ operator()() [1/5]

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

Definition at line 362 of file enumerate_quantifiers_rewriter.h.

◆ operator()() [2/5]

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

Definition at line 371 of file enumerate_quantifiers_rewriter.h.

◆ operator()() [3/5]

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

Definition at line 385 of file enumerate_quantifiers_rewriter.h.

◆ operator()() [4/5]

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 379 of file enumerate_quantifiers_rewriter.h.

◆ operator()() [5/5]

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

Definition at line 402 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 432 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 343 of file enumerate_quantifiers_rewriter.h.

◆ m_enum_mode

enumerate_quantifiers_mode mcrl2::pbes_system::enumerate_quantifiers_rewriter::m_enum_mode
protected

If true, quantifier variables of infinite sort are enumerated.

Definition at line 346 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 348 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 340 of file enumerate_quantifiers_rewriter.h.

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