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

#include <quantifier_propagate.h>

Inheritance diagram for mcrl2::pbes_system::detail::quantifier_propagate_builder:
mcrl2::pbes_system::pbes_expression_builder< quantifier_propagate_builder > mcrl2::pbes_system::add_pbes_expressions< Builder, Derived >

Public Types

using super = pbes_expression_builder< quantifier_propagate_builder >
 
using equation_map_t = std::map< core::identifier_string, pbes_equation >
 
- Public Types inherited from mcrl2::pbes_system::add_pbes_expressions< Builder, Derived >
using super = Builder< Derived >
 

Public Member Functions

 quantifier_propagate_builder (std::list< std::pair< core::identifier_string, pbes_equation > > &new_eqns, data::set_identifier_generator &ig, const equation_map_t &eq_idx)
 
pbes_expression apply_quantifier (bool is_forall, const data::variable_list &vars, const pbes_expression &body)
 
template<class T >
void apply (T &result, const forall &x)
 
template<class T >
void apply (T &result, const exists &x)
 
void enter (const and_ &)
 
void enter (const or_ &)
 
void enter (const imp &)
 
void enter (const not_ &)
 
template<class T >
void apply (T &result, const propositional_variable_instantiation &X_e)
 
- Public Member Functions inherited from mcrl2::pbes_system::add_pbes_expressions< Builder, Derived >
void update (pbes_system::pbes_equation &x)
 
void update (pbes_system::pbes &x)
 
template<class T >
void apply (T &result, const pbes_system::propositional_variable_instantiation &x)
 
template<class T >
void apply (T &result, const pbes_system::not_ &x)
 
template<class T >
void apply (T &result, const pbes_system::and_ &x)
 
template<class T >
void apply (T &result, const pbes_system::or_ &x)
 
template<class T >
void apply (T &result, const pbes_system::imp &x)
 
template<class T >
void apply (T &result, const pbes_system::forall &x)
 
template<class T >
void apply (T &result, const pbes_system::exists &x)
 
template<class T >
void apply (T &result, const pbes_system::pbes_expression &x)
 

Private Member Functions

std::list< quantifier > make_quantifier_list (const std::list< pbes_expression > &ctx) const
 
pbes_equation find_equation (const propositional_variable_instantiation &X_e)
 

Private Attributes

std::list< std::pair< core::identifier_string, pbes_equation > > & m_new_equations
 
const equation_map_t & m_eqn_map
 
data::set_identifier_generator & id_gen
 
std::list< pbes_expression > quantified_context
 

Detailed Description

Definition at line 104 of file quantifier_propagate.h.

Member Typedef Documentation

◆ equation_map_t

using mcrl2::pbes_system::detail::quantifier_propagate_builder::equation_map_t = std::map<core::identifier_string, pbes_equation>

Definition at line 108 of file quantifier_propagate.h.

◆ super

using mcrl2::pbes_system::detail::quantifier_propagate_builder::super = pbes_expression_builder<quantifier_propagate_builder>

Definition at line 107 of file quantifier_propagate.h.

Constructor & Destructor Documentation

◆ quantifier_propagate_builder()

mcrl2::pbes_system::detail::quantifier_propagate_builder::quantifier_propagate_builder ( std::list< std::pair< core::identifier_string, pbes_equation > > &  new_eqns,
data::set_identifier_generator &  ig,
const equation_map_t &  eq_idx 
)
inline

Definition at line 147 of file quantifier_propagate.h.

Member Function Documentation

◆ apply() [1/3]

template<class T >
void mcrl2::pbes_system::detail::quantifier_propagate_builder::apply ( T &  result,
const exists &  x 
)
inline

Definition at line 194 of file quantifier_propagate.h.

◆ apply() [2/3]

template<class T >
void mcrl2::pbes_system::detail::quantifier_propagate_builder::apply ( T &  result,
const forall &  x 
)
inline

Definition at line 188 of file quantifier_propagate.h.

◆ apply() [3/3]

template<class T >
void mcrl2::pbes_system::detail::quantifier_propagate_builder::apply ( T &  result,
const propositional_variable_instantiation &  X_e 
)
inline

Definition at line 220 of file quantifier_propagate.h.

◆ apply_quantifier()

pbes_expression mcrl2::pbes_system::detail::quantifier_propagate_builder::apply_quantifier ( bool  is_forall,
const data::variable_list &  vars,
const pbes_expression &  body 
)
inline

Definition at line 155 of file quantifier_propagate.h.

◆ enter() [1/4]

void mcrl2::pbes_system::detail::quantifier_propagate_builder::enter ( const and_ &  )
inline

Definition at line 199 of file quantifier_propagate.h.

◆ enter() [2/4]

void mcrl2::pbes_system::detail::quantifier_propagate_builder::enter ( const imp &  )
inline

Definition at line 209 of file quantifier_propagate.h.

◆ enter() [3/4]

void mcrl2::pbes_system::detail::quantifier_propagate_builder::enter ( const not_ &  )
inline

Definition at line 214 of file quantifier_propagate.h.

◆ enter() [4/4]

void mcrl2::pbes_system::detail::quantifier_propagate_builder::enter ( const or_ &  )
inline

Definition at line 204 of file quantifier_propagate.h.

◆ find_equation()

pbes_equation mcrl2::pbes_system::detail::quantifier_propagate_builder::find_equation ( const propositional_variable_instantiation &  X_e)
inlineprivate

Definition at line 141 of file quantifier_propagate.h.

◆ make_quantifier_list()

std::list< quantifier > mcrl2::pbes_system::detail::quantifier_propagate_builder::make_quantifier_list ( const std::list< pbes_expression > &  ctx) const
inlineprivate

Definition at line 119 of file quantifier_propagate.h.

Member Data Documentation

◆ id_gen

data::set_identifier_generator& mcrl2::pbes_system::detail::quantifier_propagate_builder::id_gen
private

Definition at line 115 of file quantifier_propagate.h.

◆ m_eqn_map

const equation_map_t& mcrl2::pbes_system::detail::quantifier_propagate_builder::m_eqn_map
private

Definition at line 114 of file quantifier_propagate.h.

◆ m_new_equations

std::list<std::pair<core::identifier_string, pbes_equation> >& mcrl2::pbes_system::detail::quantifier_propagate_builder::m_new_equations
private

Definition at line 113 of file quantifier_propagate.h.

◆ quantified_context

std::list<pbes_expression> mcrl2::pbes_system::detail::quantifier_propagate_builder::quantified_context
private

Definition at line 117 of file quantifier_propagate.h.

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