-
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