mCRL2
Loading...
Searching...
No Matches
Public Types | Public Member Functions | Public Attributes | List of all members
mcrl2::pbes_system::detail::srf_and_traverser< allow_ce > Struct Template Reference

#include <srf_pbes.h>

Inheritance diagram for mcrl2::pbes_system::detail::srf_and_traverser< allow_ce >:
mcrl2::pbes_system::pbes_expression_traverser< srf_and_traverser< allow_ce > > mcrl2::pbes_system::add_traverser_pbes_expressions< Traverser, Derived >

Public Types

using super = pbes_expression_traverser< srf_and_traverser >
 
- Public Types inherited from mcrl2::pbes_system::add_traverser_pbes_expressions< Traverser, Derived >
using super = Traverser< Derived >
 

Public Member Functions

bool is_simple_expression_cached (const pbes_expression &p, const bool b)
 
 srf_and_traverser (std::deque< pbes_equation > &equations_, const pbes_equation &eqn_, const data::variable_list &V_, data::set_identifier_generator &id_generator_, const core::identifier_string &X_true_, const core::identifier_string &X_false_, std::vector< pre_srf_equation< allow_ce > > &result_, bool merge_simple_expressions)
 
void apply (const or_ &x)
 
void apply (const and_ &x)
 
void apply (const forall &x)
 
void apply (const exists &x)
 
void apply (const propositional_variable_instantiation &x)
 
void apply (const pbes_expression &x)
 
void apply (const not_ &x)
 
void apply (const imp &x)
 
- Public Member Functions inherited from mcrl2::pbes_system::add_traverser_pbes_expressions< Traverser, Derived >
void apply (const pbes_system::pbes_equation &x)
 
void apply (const pbes_system::pbes &x)
 
void apply (const pbes_system::propositional_variable_instantiation &x)
 
void apply (const pbes_system::not_ &x)
 
void apply (const pbes_system::and_ &x)
 
void apply (const pbes_system::or_ &x)
 
void apply (const pbes_system::imp &x)
 
void apply (const pbes_system::forall &x)
 
void apply (const pbes_system::exists &x)
 
void apply (const pbes_system::pbes_expression &x)
 

Public Attributes

std::deque< pbes_equation > & equations
 
const pbes_equation & eqn
 
const data::variable_list & V
 
data::set_identifier_generator & id_generator
 
const core::identifier_string & X_true
 
const core::identifier_string & X_false
 
std::vector< pre_srf_equation< allow_ce > > & result
 
std::vector< pre_srf_summand< allow_ce > > summands
 
std::map< pbes_expression, bool > m_is_simple_expression_cache_true
 is_simple_expression is called often. Therefore, we add a cached variant.
 
std::map< pbes_expression, bool > m_is_simple_expression_cache_false
 
bool m_merge_simple_expressions = false
 

Detailed Description

template<bool allow_ce>
struct mcrl2::pbes_system::detail::srf_and_traverser< allow_ce >

Definition at line 522 of file srf_pbes.h.

Member Typedef Documentation

◆ super

template<bool allow_ce>
using mcrl2::pbes_system::detail::srf_and_traverser< allow_ce >::super = pbes_expression_traverser<srf_and_traverser>

Definition at line 524 of file srf_pbes.h.

Constructor & Destructor Documentation

◆ srf_and_traverser()

template<bool allow_ce>
mcrl2::pbes_system::detail::srf_and_traverser< allow_ce >::srf_and_traverser ( std::deque< pbes_equation > &  equations_,
const pbes_equation &  eqn_,
const data::variable_list &  V_,
data::set_identifier_generator &  id_generator_,
const core::identifier_string &  X_true_,
const core::identifier_string &  X_false_,
std::vector< pre_srf_equation< allow_ce > > &  result_,
bool  merge_simple_expressions 
)
inline

Definition at line 567 of file srf_pbes.h.

Member Function Documentation

◆ apply() [1/8]

template<bool allow_ce>
void mcrl2::pbes_system::detail::srf_and_traverser< allow_ce >::apply ( const and_ &  x)
inline

Definition at line 617 of file srf_pbes.h.

◆ apply() [2/8]

template<bool allow_ce>
void mcrl2::pbes_system::detail::srf_and_traverser< allow_ce >::apply ( const exists &  x)
inline

Definition at line 692 of file srf_pbes.h.

◆ apply() [3/8]

template<bool allow_ce>
void mcrl2::pbes_system::detail::srf_and_traverser< allow_ce >::apply ( const forall &  x)
inline

Definition at line 674 of file srf_pbes.h.

◆ apply() [4/8]

template<bool allow_ce>
void mcrl2::pbes_system::detail::srf_and_traverser< allow_ce >::apply ( const imp &  x)
inline

Definition at line 730 of file srf_pbes.h.

◆ apply() [5/8]

template<bool allow_ce>
void mcrl2::pbes_system::detail::srf_and_traverser< allow_ce >::apply ( const not_ &  x)
inline

Definition at line 726 of file srf_pbes.h.

◆ apply() [6/8]

template<bool allow_ce>
void mcrl2::pbes_system::detail::srf_and_traverser< allow_ce >::apply ( const or_ &  x)
inline

Definition at line 585 of file srf_pbes.h.

◆ apply() [7/8]

template<bool allow_ce>
void mcrl2::pbes_system::detail::srf_and_traverser< allow_ce >::apply ( const pbes_expression &  x)
inline

Definition at line 712 of file srf_pbes.h.

◆ apply() [8/8]

template<bool allow_ce>
void mcrl2::pbes_system::detail::srf_and_traverser< allow_ce >::apply ( const propositional_variable_instantiation &  x)
inline

Definition at line 706 of file srf_pbes.h.

◆ is_simple_expression_cached()

template<bool allow_ce>
bool mcrl2::pbes_system::detail::srf_and_traverser< allow_ce >::is_simple_expression_cached ( const pbes_expression &  p,
const bool  b 
)
inline

Definition at line 554 of file srf_pbes.h.

Member Data Documentation

◆ eqn

template<bool allow_ce>
const pbes_equation& mcrl2::pbes_system::detail::srf_and_traverser< allow_ce >::eqn

Definition at line 533 of file srf_pbes.h.

◆ equations

template<bool allow_ce>
std::deque<pbes_equation>& mcrl2::pbes_system::detail::srf_and_traverser< allow_ce >::equations

Definition at line 530 of file srf_pbes.h.

◆ id_generator

template<bool allow_ce>
data::set_identifier_generator& mcrl2::pbes_system::detail::srf_and_traverser< allow_ce >::id_generator

Definition at line 538 of file srf_pbes.h.

◆ m_is_simple_expression_cache_false

template<bool allow_ce>
std::map<pbes_expression, bool> mcrl2::pbes_system::detail::srf_and_traverser< allow_ce >::m_is_simple_expression_cache_false

Definition at line 552 of file srf_pbes.h.

◆ m_is_simple_expression_cache_true

template<bool allow_ce>
std::map<pbes_expression, bool> mcrl2::pbes_system::detail::srf_and_traverser< allow_ce >::m_is_simple_expression_cache_true

is_simple_expression is called often. Therefore, we add a cached variant.

Definition at line 551 of file srf_pbes.h.

◆ m_merge_simple_expressions

template<bool allow_ce>
bool mcrl2::pbes_system::detail::srf_and_traverser< allow_ce >::m_merge_simple_expressions = false

If true do not introduce a new PBES equation for simple expressions, and instead add them to every summand separately.

Definition at line 565 of file srf_pbes.h.

◆ result

template<bool allow_ce>
std::vector<pre_srf_equation<allow_ce> >& mcrl2::pbes_system::detail::srf_and_traverser< allow_ce >::result

Definition at line 545 of file srf_pbes.h.

◆ summands

template<bool allow_ce>
std::vector<pre_srf_summand<allow_ce> > mcrl2::pbes_system::detail::srf_and_traverser< allow_ce >::summands

Definition at line 548 of file srf_pbes.h.

◆ V

template<bool allow_ce>
const data::variable_list& mcrl2::pbes_system::detail::srf_and_traverser< allow_ce >::V

Definition at line 535 of file srf_pbes.h.

◆ X_false

template<bool allow_ce>
const core::identifier_string& mcrl2::pbes_system::detail::srf_and_traverser< allow_ce >::X_false

Definition at line 542 of file srf_pbes.h.

◆ X_true

template<bool allow_ce>
const core::identifier_string& mcrl2::pbes_system::detail::srf_and_traverser< allow_ce >::X_true

Definition at line 541 of file srf_pbes.h.

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