mcrl2::pbes_system::quantifiers_inside_rewriter Class Reference

A rewriter that pushes quantifiers inside in a PBES expression. More...

#include <quantifiers_inside_rewriter.h>

Public Types
typedef pbes_expression	term_type
	The term type.
typedef data::variable	variable_type
	The variable type.

Public Member Functions
pbes_expression	operator() (const pbes_expression &x) const
	Rewrites a pbes expression.

Detailed Description

A rewriter that pushes quantifiers inside in a PBES expression.

Definition at line 314 of file quantifiers_inside_rewriter.h.

Member Typedef Documentation

term_type

typedef pbes_expression mcrl2::pbes_system::quantifiers_inside_rewriter::term_type

The term type.

Definition at line 318 of file quantifiers_inside_rewriter.h.

variable_type

typedef data::variable mcrl2::pbes_system::quantifiers_inside_rewriter::variable_type

The variable type.

Definition at line 321 of file quantifiers_inside_rewriter.h.

Member Function Documentation

operator()()

pbes_expression mcrl2::pbes_system::quantifiers_inside_rewriter::operator() ( const pbes_expression &  x ) const

inline

Rewrites a pbes expression.

Parameters

x

A term

Returns

The rewrite result.

Definition at line 326 of file quantifiers_inside_rewriter.h.

---

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

• pbes/include/mcrl2/pbes/rewriters/quantifiers_inside_rewriter.h