mCRL2
Loading...
Searching...
No Matches
mcrl2::pbes_system::pfnf_rewriter Class Reference

A rewriter that brings PBES expressions into PFNF normal form. More...

#include <pfnf_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.
 
template<typename SubstitutionFunction >
pbes_expression operator() (const pbes_expression &x, SubstitutionFunction sigma) const
 Rewrites a pbes expression.
 

Detailed Description

A rewriter that brings PBES expressions into PFNF normal form.

Definition at line 22 of file pfnf_rewriter.h.

Member Typedef Documentation

◆ term_type

The term type.

Definition at line 26 of file pfnf_rewriter.h.

◆ variable_type

The variable type.

Definition at line 29 of file pfnf_rewriter.h.

Member Function Documentation

◆ operator()() [1/2]

pbes_expression mcrl2::pbes_system::pfnf_rewriter::operator() ( const pbes_expression x) const
inline

Rewrites a pbes expression.

Parameters
xA term
Returns
The rewrite result.

Definition at line 34 of file pfnf_rewriter.h.

◆ operator()() [2/2]

template<typename SubstitutionFunction >
pbes_expression mcrl2::pbes_system::pfnf_rewriter::operator() ( const pbes_expression x,
SubstitutionFunction  sigma 
) const
inline

Rewrites a pbes expression.

Parameters
xA term
sigmaA substitution function
Returns
The rewrite result.

Definition at line 46 of file pfnf_rewriter.h.


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