mcrl2::pbes_system::one_point_rule_rewriter Class Reference

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

#include <one_point_rule_rewriter.h>

Public Types
using	term_type = pbes_expression
	The term type.
using	variable_type = data::variable
	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 134 of file one_point_rule_rewriter.h.

Member Typedef Documentation

term_type

using mcrl2::pbes_system::one_point_rule_rewriter::term_type = pbes_expression

The term type.

Definition at line 138 of file one_point_rule_rewriter.h.

variable_type

using mcrl2::pbes_system::one_point_rule_rewriter::variable_type = data::variable

The variable type.

Definition at line 141 of file one_point_rule_rewriter.h.

Member Function Documentation

operator()()

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

inline

Rewrites a pbes expression.

Parameters

x

A term

Returns

The rewrite result.

Definition at line 146 of file one_point_rule_rewriter.h.

---

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

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