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

#include <constelm.h>

Inheritance diagram for mcrl2::pres_system::detail::edge_condition_traverser:
mcrl2::pres_system::pres_expression_traverser< edge_condition_traverser > mcrl2::pres_system::add_traverser_pres_expressions< Traverser, Derived >

Public Types

typedef pres_expression_traverser< edge_condition_traverser > super
 
typedef edge_traverser_stack_elem stack_elem
 
typedef stack_elem::edge_map edge_map
 
typedef std::list< detail::quantified_variable > qvar_list
 
- Public Types inherited from mcrl2::pres_system::add_traverser_pres_expressions< Traverser, Derived >
typedef Traverser< Derived > super
 

Public Member Functions

void push (const stack_elem &x)
 
stack_elem & top ()
 
const stack_elem & top () const
 
stack_elem pop ()
 
void merge_conditions (stack_elem &ec1, bool negate1, stack_elem &ec2, bool negate2, stack_elem &ec, bool is_conjunctive)
 
void enter (const minus &)
 
void enter (const and_ &)
 
void enter (const or_ &)
 
void enter (const imp &)
 
void enter (const infimum &x)
 
void enter (const supremum &x)
 
void enter (const sum &x)
 
void leave (const data::data_expression &x)
 
void leave (const minus &)
 
void leave (const and_ &)
 
void leave (const or_ &)
 
void leave (const imp &)
 
void leave (const infimum &x)
 
void leave (const supremum &x)
 
void leave (const sum &)
 
void leave (const propositional_variable_instantiation &x)
 
const edge_map & result () const
 
- Public Member Functions inherited from mcrl2::pres_system::add_traverser_pres_expressions< Traverser, Derived >
void apply (const pres_system::pres_equation &x)
 
void apply (const pres_system::pres &x)
 
void apply (const pres_system::propositional_variable_instantiation &x)
 
void apply (const pres_system::minus &x)
 
void apply (const pres_system::and_ &x)
 
void apply (const pres_system::or_ &x)
 
void apply (const pres_system::imp &x)
 
void apply (const pres_system::plus &x)
 
void apply (const pres_system::const_multiply &x)
 
void apply (const pres_system::const_multiply_alt &x)
 
void apply (const pres_system::infimum &x)
 
void apply (const pres_system::supremum &x)
 
void apply (const pres_system::sum &x)
 
void apply (const pres_system::eqinf &x)
 
void apply (const pres_system::eqninf &x)
 
void apply (const pres_system::condsm &x)
 
void apply (const pres_system::condeq &x)
 
void apply (const pres_system::pres_expression &x)
 

Public Attributes

std::vector< stack_elem > condition_fv_stack
 
std::list< pres_expression > quantified_context
 

Detailed Description

Definition at line 131 of file constelm.h.

Member Typedef Documentation

◆ edge_map

typedef stack_elem::edge_map mcrl2::pres_system::detail::edge_condition_traverser::edge_map

Definition at line 139 of file constelm.h.

◆ qvar_list

typedef std::list<detail::quantified_variable> mcrl2::pres_system::detail::edge_condition_traverser::qvar_list

Definition at line 140 of file constelm.h.

◆ stack_elem

typedef edge_traverser_stack_elem mcrl2::pres_system::detail::edge_condition_traverser::stack_elem

Definition at line 138 of file constelm.h.

◆ super

typedef pres_expression_traverser<edge_condition_traverser> mcrl2::pres_system::detail::edge_condition_traverser::super

Definition at line 133 of file constelm.h.

Member Function Documentation

◆ enter() [1/7]

void mcrl2::pres_system::detail::edge_condition_traverser::enter ( const and_ &  )
inline

Definition at line 197 of file constelm.h.

◆ enter() [2/7]

void mcrl2::pres_system::detail::edge_condition_traverser::enter ( const imp &  )
inline

Definition at line 207 of file constelm.h.

◆ enter() [3/7]

void mcrl2::pres_system::detail::edge_condition_traverser::enter ( const infimum &  x)
inline

Definition at line 212 of file constelm.h.

◆ enter() [4/7]

void mcrl2::pres_system::detail::edge_condition_traverser::enter ( const minus &  )
inline

Definition at line 192 of file constelm.h.

◆ enter() [5/7]

void mcrl2::pres_system::detail::edge_condition_traverser::enter ( const or_ &  )
inline

Definition at line 202 of file constelm.h.

◆ enter() [6/7]

void mcrl2::pres_system::detail::edge_condition_traverser::enter ( const sum &  x)
inline

Definition at line 222 of file constelm.h.

◆ enter() [7/7]

void mcrl2::pres_system::detail::edge_condition_traverser::enter ( const supremum &  x)
inline

Definition at line 217 of file constelm.h.

◆ leave() [1/9]

void mcrl2::pres_system::detail::edge_condition_traverser::leave ( const and_ &  )
inline

Definition at line 241 of file constelm.h.

◆ leave() [2/9]

void mcrl2::pres_system::detail::edge_condition_traverser::leave ( const data::data_expression &  x)
inline

Definition at line 228 of file constelm.h.

◆ leave() [3/9]

void mcrl2::pres_system::detail::edge_condition_traverser::leave ( const imp &  )
inline

Definition at line 272 of file constelm.h.

◆ leave() [4/9]

void mcrl2::pres_system::detail::edge_condition_traverser::leave ( const infimum &  x)
inline

Definition at line 288 of file constelm.h.

◆ leave() [5/9]

void mcrl2::pres_system::detail::edge_condition_traverser::leave ( const minus &  )
inline

Definition at line 236 of file constelm.h.

◆ leave() [6/9]

void mcrl2::pres_system::detail::edge_condition_traverser::leave ( const or_ &  )
inline

Definition at line 256 of file constelm.h.

◆ leave() [7/9]

void mcrl2::pres_system::detail::edge_condition_traverser::leave ( const propositional_variable_instantiation &  x)
inline

Definition at line 370 of file constelm.h.

◆ leave() [8/9]

void mcrl2::pres_system::detail::edge_condition_traverser::leave ( const sum &  )
inline

Definition at line 365 of file constelm.h.

◆ leave() [9/9]

void mcrl2::pres_system::detail::edge_condition_traverser::leave ( const supremum &  x)
inline

Definition at line 327 of file constelm.h.

◆ merge_conditions()

void mcrl2::pres_system::detail::edge_condition_traverser::merge_conditions ( stack_elem &  ec1,
bool  negate1,
stack_elem &  ec2,
bool  negate2,
stack_elem &  ec,
bool  is_conjunctive 
)
inline

Definition at line 168 of file constelm.h.

◆ pop()

stack_elem mcrl2::pres_system::detail::edge_condition_traverser::pop ( )
inline

Definition at line 160 of file constelm.h.

◆ push()

void mcrl2::pres_system::detail::edge_condition_traverser::push ( const stack_elem &  x)
inline

Definition at line 145 of file constelm.h.

◆ result()

const edge_map & mcrl2::pres_system::detail::edge_condition_traverser::result ( ) const
inline

Definition at line 393 of file constelm.h.

◆ top() [1/2]

stack_elem & mcrl2::pres_system::detail::edge_condition_traverser::top ( )
inline

Definition at line 150 of file constelm.h.

◆ top() [2/2]

const stack_elem & mcrl2::pres_system::detail::edge_condition_traverser::top ( ) const
inline

Definition at line 155 of file constelm.h.

Member Data Documentation

◆ condition_fv_stack

std::vector<stack_elem> mcrl2::pres_system::detail::edge_condition_traverser::condition_fv_stack

Definition at line 142 of file constelm.h.

◆ quantified_context

std::list<pres_expression> mcrl2::pres_system::detail::edge_condition_traverser::quantified_context

Definition at line 143 of file constelm.h.

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