Applies the PFNF rewriter to a PBES expression. More...

#include <pfnf_traverser.h>

Inheritance diagram for mcrl2::pbes_system::detail::pfnf_traverser:

Public Types
typedef pbes_expression_traverser< pfnf_traverser >	super

Public Types inherited from mcrl2::pbes_system::add_traverser_pbes_expressions< Traverser, Derived >
typedef Traverser< Derived >	super

Public Member Functions
void	resolve_name_clashes (pfnf_traverser_expression &left, pfnf_traverser_expression &right)

pbes_expression	make_and (const pfnf_traverser_expression &left, const pfnf_traverser_expression &right) const

pbes_expression	make_or (const pfnf_traverser_expression &left, const pfnf_traverser_expression &right) const

pbes_expression	make_not (const pfnf_traverser_expression &x) const

pbes_expression	evaluate () const
	Returns the top element of the expression stack converted to a pbes expression.

void	print_expression (const pfnf_traverser_expression &expr) const
	Prints an expression.

void	print (const std::string &msg="") const
	Prints the expression stack.

void	enter (const data::data_expression &x)

void	enter (const not_ &)

void	leave (const and_ &)

void	leave (const or_ &)

void	enter (const imp &)

void	enter (const forall &x)

void	leave (const forall &)

void	enter (const exists &x)

void	leave (const exists &)

void	enter (const propositional_variable_instantiation &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::vector< pfnf_traverser_expression >	expression_stack
	A stack containing expressions in PFNF format.

std::vector< data::variable_list >	quantifier_stack
	A stack containing quantifier variables.

Detailed Description

Applies the PFNF rewriter to a PBES expression.

Definition at line 179 of file pfnf_traverser.h.

Member Typedef Documentation

◆ super

typedef pbes_expression_traverser<pfnf_traverser> mcrl2::pbes_system::detail::pfnf_traverser::super

Definition at line 181 of file pfnf_traverser.h.

Member Function Documentation

◆ enter() [1/6]

void mcrl2::pbes_system::detail::pfnf_traverser::enter ( const data::data_expression & x )

inline

Definition at line 352 of file pfnf_traverser.h.

◆ enter() [2/6]

void mcrl2::pbes_system::detail::pfnf_traverser::enter ( const exists & x )

inline

Definition at line 441 of file pfnf_traverser.h.

◆ enter() [3/6]

void mcrl2::pbes_system::detail::pfnf_traverser::enter ( const forall & x )

inline

Definition at line 429 of file pfnf_traverser.h.

◆ enter() [4/6]

void mcrl2::pbes_system::detail::pfnf_traverser::enter ( const imp & )

inline

Definition at line 424 of file pfnf_traverser.h.

◆ enter() [5/6]

void mcrl2::pbes_system::detail::pfnf_traverser::enter ( const not_ & )

inline

Definition at line 357 of file pfnf_traverser.h.

◆ enter() [6/6]

void mcrl2::pbes_system::detail::pfnf_traverser::enter ( const propositional_variable_instantiation & x )

inline

Definition at line 453 of file pfnf_traverser.h.

◆ evaluate()

pbes_expression mcrl2::pbes_system::detail::pfnf_traverser::evaluate ( ) const

inline

Returns the top element of the expression stack converted to a pbes expression.

Returns: The top element of the expression stack converted to a pbes expression.

Definition at line 270 of file pfnf_traverser.h.

◆ leave() [1/4]

void mcrl2::pbes_system::detail::pfnf_traverser::leave ( const and_ & )

inline

Definition at line 362 of file pfnf_traverser.h.

◆ leave() [2/4]

void mcrl2::pbes_system::detail::pfnf_traverser::leave ( const exists & )

inline

Definition at line 446 of file pfnf_traverser.h.

◆ leave() [3/4]

void mcrl2::pbes_system::detail::pfnf_traverser::leave ( const forall & )

inline

Definition at line 434 of file pfnf_traverser.h.

◆ leave() [4/4]

void mcrl2::pbes_system::detail::pfnf_traverser::leave ( const or_ & )

inline

Definition at line 377 of file pfnf_traverser.h.

◆ make_and()

pbes_expression mcrl2::pbes_system::detail::pfnf_traverser::make_and	(	const pfnf_traverser_expression &	left,
		const pfnf_traverser_expression &	right
	)		const

inline

Definition at line 241 of file pfnf_traverser.h.

◆ make_not()

pbes_expression mcrl2::pbes_system::detail::pfnf_traverser::make_not ( const pfnf_traverser_expression & x ) const

inline

Definition at line 255 of file pfnf_traverser.h.

◆ make_or()

pbes_expression mcrl2::pbes_system::detail::pfnf_traverser::make_or	(	const pfnf_traverser_expression &	left,
		const pfnf_traverser_expression &	right
	)		const

inline

Definition at line 248 of file pfnf_traverser.h.

◆ print()

void mcrl2::pbes_system::detail::pfnf_traverser::print ( const std::string & msg = "" ) const

inline

Prints the expression stack.

Parameters

msg A string

Definition at line 342 of file pfnf_traverser.h.

◆ print_expression()

void mcrl2::pbes_system::detail::pfnf_traverser::print_expression ( const pfnf_traverser_expression & expr ) const

inline

Prints an expression.

Parameters

expr	An expression

Definition at line 305 of file pfnf_traverser.h.

◆ resolve_name_clashes()

void mcrl2::pbes_system::detail::pfnf_traverser::resolve_name_clashes	(	pfnf_traverser_expression &	left,
		pfnf_traverser_expression &	right
	)

inline

Definition at line 188 of file pfnf_traverser.h.

Member Data Documentation

◆ expression_stack

std::vector<pfnf_traverser_expression> mcrl2::pbes_system::detail::pfnf_traverser::expression_stack

A stack containing expressions in PFNF format.

Definition at line 263 of file pfnf_traverser.h.

◆ quantifier_stack

std::vector<data::variable_list> mcrl2::pbes_system::detail::pfnf_traverser::quantifier_stack

A stack containing quantifier variables.

Definition at line 266 of file pfnf_traverser.h.

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

pbes/include/mcrl2/pbes/detail/pfnf_traverser.h

Public Types

Public Member Functions

Public Attributes

Detailed Description

Member Typedef Documentation

◆ super

Member Function Documentation

◆ enter() [1/6]

◆ enter() [2/6]

◆ enter() [3/6]

◆ enter() [4/6]

◆ enter() [5/6]

◆ enter() [6/6]

◆ evaluate()

◆ leave() [1/4]

◆ leave() [2/4]

◆ leave() [3/4]

◆ leave() [4/4]

◆ make_and()

◆ make_not()

◆ make_or()

◆ print()

◆ print_expression()

◆ resolve_name_clashes()

Member Data Documentation

◆ expression_stack

◆ quantifier_stack