mcrl2::pbes_system::data2pbes_rewriter Class Reference

A rewriter that applies one point rule quantifier elimination to a PBES. More...

#include <data2pbes_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 applies one point rule quantifier elimination to a PBES.

Definition at line 147 of file data2pbes_rewriter.h.

Member Typedef Documentation

term_type

typedef pbes_expression mcrl2::pbes_system::data2pbes_rewriter::term_type

The term type.

Definition at line 151 of file data2pbes_rewriter.h.

variable_type

typedef data::variable mcrl2::pbes_system::data2pbes_rewriter::variable_type

The variable type.

Definition at line 154 of file data2pbes_rewriter.h.

Member Function Documentation

operator()()

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

inline

Rewrites a pbes expression.

Parameters

x

A term

Returns

The rewrite result.

Definition at line 159 of file data2pbes_rewriter.h.

---

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

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