spot  2.1.1
 All Classes Files Functions Variables Typedefs Enumerations Enumerator Friends Modules Pages
Classes | Functions
Rewriting Algorithms for Formulas

Classes

class  spot::tl_simplifier
 Rewrite or simplify f in various ways. More...
 
class  spot::unabbreviator
 Clone and rewrite a formula to remove specified operators logical operators. More...
 

Functions

formula spot::mark_tools::mark_concat_ops (formula f)
 Mark operators NegClosure and EConcat. More...
 
formula spot::negative_normal_form (formula f, bool negated=false)
 Build the negative normal form of f. More...
 
formula spot::relabel (formula f, relabeling_style style, relabeling_map *m=nullptr)
 Relabel the atomic propositions in a formula. More...
 
formula spot::relabel_bse (formula f, relabeling_style style, relabeling_map *m=nullptr)
 Relabel Boolean subexpressions in a formula using atomic propositions. More...
 
formula spot::unabbreviate (formula in, const char *opt=default_unabbrev_string)
 Clone and rewrite a formula to remove specified operators logical operators. More...
 

Detailed Description

Function Documentation

formula spot::mark_tools::mark_concat_ops ( formula  f)

#include <spot/tl/mark.hh>

Mark operators NegClosure and EConcat.

Parameters
fThe formula to rewrite.
formula spot::negative_normal_form ( formula  f,
bool  negated = false 
)

#include <spot/tl/nenoform.hh>

Build the negative normal form of f.

All negations of the formula are pushed in front of the atomic propositions.

Parameters
fThe formula to normalize.
negatedIf true, return the negative normal form of !f

Note that this will not remove abbreviated operators. If you want to remove abbreviations, call spot::unabbreviate first. (Calling this function after spot::negative_normal_form would likely produce a formula which is not in negative normal form.)

formula spot::relabel ( formula  f,
relabeling_style  style,
relabeling_map *  m = nullptr 
)

#include <spot/tl/relabel.hh>

Relabel the atomic propositions in a formula.

If m is non-null, it is filled with correspondence between the new names (keys) and the old names (values).

formula spot::relabel_bse ( formula  f,
relabeling_style  style,
relabeling_map *  m = nullptr 
)

#include <spot/tl/relabel.hh>

Relabel Boolean subexpressions in a formula using atomic propositions.

If m is non-null, it is filled with correspondence between the new names (keys) and the old names (values).

formula spot::unabbreviate ( formula  in,
const char *  opt = default_unabbrev_string 
)

#include <spot/tl/unabbrev.hh>

Clone and rewrite a formula to remove specified operators logical operators.

The set of operators to remove should be passed as a string which in which each letter denote an operator (using LBT's convention).


Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Tue Sep 20 2016 07:13:02 for spot by doxygen 1.8.8