spot  2.11.6
Public Member Functions | List of all members
spot::tl_simplifier Class Reference

Rewrite or simplify f in various ways. More...

#include <spot/tl/simplify.hh>

Collaboration diagram for spot::tl_simplifier:

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_optionsoptions ()
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...

Detailed Description

Rewrite or simplify f in various ways.

Member Function Documentation

◆ are_equivalent()

bool spot::tl_simplifier::are_equivalent ( formula  f,
formula  g 

check whether two formulae are equivalent.

This costly check performs up to four translations, two products, and two emptiness checks.

◆ as_bdd()

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.

◆ boolean_to_isop()

formula spot::tl_simplifier::boolean_to_isop ( formula  f)

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.

◆ clear_as_bdd_cache()

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.

◆ clear_caches()

void spot::tl_simplifier::clear_caches ( )

Clear all caches.

This empties all the cache used by the simplifier.

◆ get_dict()

bdd_dict_ptr spot::tl_simplifier::get_dict ( ) const

Return the bdd_dict used.

◆ implication()

bool spot::tl_simplifier::implication ( formula  f,
formula  g 

Check whether f implies g.

This operation is costlier than syntactic_implication() because it requires two translation, one product and one emptiness check.

◆ negative_normal_form()

formula spot::tl_simplifier::negative_normal_form ( formula  f,
bool  negated = false 

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).

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

◆ options()

tl_simplifier_options& spot::tl_simplifier::options ( )

The simplifier options.

Those should can still be changed before the first formula is simplified.

◆ print_stats()

void spot::tl_simplifier::print_stats ( std::ostream &  os) const

Dump statistics about the caches.

◆ simplify()

formula spot::tl_simplifier::simplify ( formula  f)

Simplify the formula f (using options supplied to the constructor).

◆ star_normal_form()

formula spot::tl_simplifier::star_normal_form ( formula  f)

Cached version of spot::star_normal_form().

◆ syntactic_implication()

bool spot::tl_simplifier::syntactic_implication ( formula  f,
formula  g 

Syntactic implication.

Returns whether f syntactically implies g.

This is adapted from the rules of Somenzi and Bloem. [51]

◆ syntactic_implication_neg()

bool spot::tl_simplifier::syntactic_implication_neg ( formula  f,
formula  g,
bool  right 

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.

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

Please direct any question, comment, or bug report to the Spot mailing list at
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.1