|
spot 2.13
|
Rewrite or simplify f in various ways. More...
#include <spot/tl/simplify.hh>
Public Member Functions | |
| tl_simplifier (const bdd_dict_ptr &dict=make_bdd_dict()) | |
| tl_simplifier (const tl_simplifier_options &opt, bdd_dict_ptr dict=make_bdd_dict()) | |
| formula | simplify (formula f) |
| tl_simplifier_options & | options () |
| formula | negative_normal_form (formula f, bool negated=false) |
| bool | syntactic_implication (formula f, formula g) |
| Syntactic implication. More... | |
| bool | syntactic_implication_neg (formula f, formula g, bool right) |
| Syntactic implication with one negated argument. More... | |
| bool | are_equivalent (formula f, formula g) |
| check whether two formulae are equivalent. More... | |
| bool | implication (formula f, formula g) |
| Check whether f implies g. More... | |
| bdd | as_bdd (formula f) |
| Convert a Boolean formula as a BDD. More... | |
| void | clear_as_bdd_cache () |
| Clear the as_bdd() cache. More... | |
| void | clear_caches () |
| Clear all caches. More... | |
| bdd_dict_ptr | get_dict () const |
| Return the bdd_dict used. More... | |
| formula | star_normal_form (formula f) |
| Cached version of spot::star_normal_form(). More... | |
| formula | boolean_to_isop (formula f) |
| Rewrite a Boolean formula f into as an irredundant sum of product. More... | |
| void | print_stats (std::ostream &os) const |
| Dump statistics about the caches. More... | |
Rewrite or simplify f in various ways.
check whether two formulae are equivalent.
This costly check performs up to four translations, two products, and two emptiness checks.
| bdd spot::tl_simplifier::as_bdd | ( | formula | f | ) |
Convert a Boolean formula as a BDD.
If you plan to use this method, be sure to pass a bdd_dict to the constructor.
Rewrite a Boolean formula f into as an irredundant sum of product.
This uses a cache, so it is OK to call this with identical arguments.
| void spot::tl_simplifier::clear_as_bdd_cache | ( | ) |
Clear the as_bdd() cache.
Calling this function is recommended before running other algorithms that create BDD variables in a more natural order. For instance ltl_to_tgba_fm() will usually be more efficient if the BDD variables for atomic propositions have not been ordered before hand.
This also clears the language containment cache.
| void spot::tl_simplifier::clear_caches | ( | ) |
Clear all caches.
This empties all the cache used by the simplifier.
| bdd_dict_ptr spot::tl_simplifier::get_dict | ( | ) | const |
Return the bdd_dict used.
Check whether f implies g.
This operation is costlier than syntactic_implication() because it requires two translation, one product and one emptiness check.
Build the negative normal form of formula f. All negations of the formula are pushed in front of the atomic propositions. Operators <=>, =>, xor are all removed (calling spot::unabbreviate for those is not needed).
| f | The formula to normalize. |
| negated | If true, return the negative normal form of !f |
| tl_simplifier_options & spot::tl_simplifier::options | ( | ) |
The simplifier options.
Those should can still be changed before the first formula is simplified.
| void spot::tl_simplifier::print_stats | ( | std::ostream & | os | ) | const |
Dump statistics about the caches.
Simplify the formula f (using options supplied to the constructor).
Cached version of spot::star_normal_form().
Syntactic implication.
Returns whether f syntactically implies g.
This is adapted from the rules of Somenzi and Bloem. [54]
Syntactic implication with one negated argument.
If right is true, this method returns whether f implies !g. If right is false, this returns whether !f implies g.
1.9.4