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

Visitor that implements the pbes-abstract algorithm. More...

#include <abstract.h>

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

Public Types

using super = pbes_expression_builder< pbes_abstract_builder >
 
- Public Types inherited from mcrl2::pbes_system::add_pbes_expressions< Builder, Derived >
using super = Builder< Derived >
 

Public Member Functions

 pbes_abstract_builder (const std::vector< data::variable > &selected_variables, bool value_true)
 
bool is_bound (const data::variable &v) const
 Returns true if the m_quantifier_stack contains a given data variable.
 
void push_variables (const data::variable_list &variables)
 Adds a sequence of variables to the quantifier stack.
 
void pop_variables ()
 Removes the last added sequence of variables from the quantifier stack.
 
template<class T >
void apply (T &result, const data::data_expression &d)
 Visit data_expression node.
 
template<class T >
void apply (T &result, const forall &x)
 Visit forall node.
 
template<class T >
void apply (T &result, const exists &x)
 Visit exists node.
 
- 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)
 

Public Attributes

std::vector< data::variable_list > m_quantifier_stack
 
const std::vector< data::variable > m_selected_variables
 
const data::data_expression m_value
 

Detailed Description

Visitor that implements the pbes-abstract algorithm.

Definition at line 28 of file abstract.h.

Member Typedef Documentation

◆ super

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

Definition at line 30 of file abstract.h.

Constructor & Destructor Documentation

◆ pbes_abstract_builder()

mcrl2::pbes_system::detail::pbes_abstract_builder::pbes_abstract_builder ( const std::vector< data::variable > &  selected_variables,
bool  value_true 
)
inline

Definition at line 37 of file abstract.h.

Member Function Documentation

◆ apply() [1/3]

template<class T >
void mcrl2::pbes_system::detail::pbes_abstract_builder::apply ( T &  result,
const data::data_expression &  d 
)
inline

Visit data_expression node.

Definition at line 72 of file abstract.h.

◆ apply() [2/3]

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

Visit exists node.

Definition at line 103 of file abstract.h.

◆ apply() [3/3]

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

Visit forall node.

Definition at line 92 of file abstract.h.

◆ is_bound()

bool mcrl2::pbes_system::detail::pbes_abstract_builder::is_bound ( const data::variable &  v) const
inline

Returns true if the m_quantifier_stack contains a given data variable.

Definition at line 43 of file abstract.h.

◆ pop_variables()

void mcrl2::pbes_system::detail::pbes_abstract_builder::pop_variables ( )
inline

Removes the last added sequence of variables from the quantifier stack.

Definition at line 65 of file abstract.h.

◆ push_variables()

void mcrl2::pbes_system::detail::pbes_abstract_builder::push_variables ( const data::variable_list &  variables)
inline

Adds a sequence of variables to the quantifier stack.

Definition at line 59 of file abstract.h.

Member Data Documentation

◆ m_quantifier_stack

std::vector<data::variable_list> mcrl2::pbes_system::detail::pbes_abstract_builder::m_quantifier_stack

Definition at line 33 of file abstract.h.

◆ m_selected_variables

const std::vector<data::variable> mcrl2::pbes_system::detail::pbes_abstract_builder::m_selected_variables

Definition at line 34 of file abstract.h.

◆ m_value

const data::data_expression mcrl2::pbes_system::detail::pbes_abstract_builder::m_value

Definition at line 35 of file abstract.h.

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