mcrl2::pbes_system::detail::normalize_and_or_builder< Derived > Struct Template Reference

#include <normalize_and_or.h>

Inheritance diagram for mcrl2::pbes_system::detail::normalize_and_or_builder< Derived >:

Public Types
typedef pbes_expression_builder< Derived >	super
Public Types inherited from mcrl2::pbes_system::add_pbes_expressions< pbes_system::pbes_expression_builder_base, Derived >
typedef pbes_system::pbes_expression_builder_base< Derived >	super

Public Member Functions
std::multiset< pbes_expression >	split_or (const pbes_expression &expr)
	Splits a disjunction into a sequence of operands Given a pbes expression of the form p1 || p2 || .... || pn, this will yield a set of the form { p1, p2, ..., pn }, assuming that pi does not have a || as main function symbol.
std::multiset< pbes_expression >	split_and (const pbes_expression &expr)
	Splits a conjunction into a sequence of operands Given a pbes expression of the form p1 && p2 && .... && pn, this will yield a set of the form { p1, p2, ..., pn }, assuming that pi does not have a && as main function symbol.
pbes_expression	normalize (const pbes_expression &x)
template<class T >
void	apply (T &result, const data::data_expression &x)
template<class T >
void	apply (T &result, const pbes_expression &x)
Public Member Functions inherited from mcrl2::pbes_system::add_pbes_expressions< pbes_system::pbes_expression_builder_base, Derived >
void	update (pbes_system::pbes_equation &x)
void	update (pbes_system::pbes &x)
void	apply (T &result, const pbes_system::propositional_variable_instantiation &x)
void	apply (T &result, const pbes_system::not_ &x)
void	apply (T &result, const pbes_system::and_ &x)
void	apply (T &result, const pbes_system::or_ &x)
void	apply (T &result, const pbes_system::imp &x)
void	apply (T &result, const pbes_system::forall &x)
void	apply (T &result, const pbes_system::exists &x)
void	apply (T &result, const pbes_system::pbes_expression &x)

Detailed Description

template<typename Derived>
struct mcrl2::pbes_system::detail::normalize_and_or_builder< Derived >

Definition at line 29 of file normalize_and_or.h.

Member Typedef Documentation

super

template<typename Derived >

typedef pbes_expression_builder<Derived> mcrl2::pbes_system::detail::normalize_and_or_builder< Derived >::super

Definition at line 31 of file normalize_and_or.h.

Member Function Documentation

apply() [1/2]

template<typename Derived >

template<class T >

void mcrl2::pbes_system::detail::normalize_and_or_builder< Derived >::apply ( T &  result, const data::data_expression &  x  )

inline

Definition at line 82 of file normalize_and_or.h.

apply() [2/2]

template<typename Derived >

template<class T >

void mcrl2::pbes_system::detail::normalize_and_or_builder< Derived >::apply ( T &  result, const pbes_expression &  x  )

inline

Definition at line 88 of file normalize_and_or.h.

normalize()

template<typename Derived >

pbes_expression mcrl2::pbes_system::detail::normalize_and_or_builder< Derived >::normalize ( const pbes_expression &  x )

inline

Definition at line 65 of file normalize_and_or.h.

split_and()

template<typename Derived >

std::multiset< pbes_expression > mcrl2::pbes_system::detail::normalize_and_or_builder< Derived >::split_and ( const pbes_expression &  expr )

inline

Splits a conjunction into a sequence of operands Given a pbes expression of the form p1 && p2 && .... && pn, this will yield a set of the form { p1, p2, ..., pn }, assuming that pi does not have a && as main function symbol.

Parameters

expr	A PBES expression

Returns

A sequence of operands

Definition at line 57 of file normalize_and_or.h.

split_or()

template<typename Derived >

std::multiset< pbes_expression > mcrl2::pbes_system::detail::normalize_and_or_builder< Derived >::split_or ( const pbes_expression &  expr )

inline

Splits a disjunction into a sequence of operands Given a pbes expression of the form p1 || p2 || .... || pn, this will yield a set of the form { p1, p2, ..., pn }, assuming that pi does not have a || as main function symbol.

Parameters

expr	A PBES expression

Returns

A sequence of operands

Definition at line 43 of file normalize_and_or.h.

---

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

• pbes/include/mcrl2/pbes/detail/normalize_and_or.h