• Alexandre Duret-Lutz's avatar
    Clean the as_bdd() cache after LTL simplification. · e5a86290
    Alexandre Duret-Lutz authored
    Syntactic implication checks may use as_bdd() to compare Boolean
    formulae.  By doing so, they register Boolean variables in an order
    that is usially detrimental to the LTL translator.  The new,
    clear_as_bdd_cache() function offers a mean to unregister these
    variables, so that the LTL translator will register them again in the
    a more natural way.
    
    * src/ltlvisit/simplify.hh, src/ltlvisit/simplify.cc
    (clear_as_bdd_cache): New function.
    * src/tgbatest/ltl2tgba.cc, wrap/python/ajax/spot.in: Call it.
    e5a86290
ltl2tgba.cc 38.8 KB