spot
2.0.3
|
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... | |
formula spot::mark_tools::mark_concat_ops | ( | formula | f | ) |
#include <spot/tl/mark.hh>
Mark operators NegClosure and EConcat.
f | The 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.
f | The formula to normalize. |
negated | If 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).