-
Alexandre Duret-Lutz authored
* src/ltlvisit/simplify.hh, src/ltlvisit/simplify.cc (ltl_simplifier::ltl_simplifier, ltl_simplifier::get_dict): Make it possible to supply and retrieve the dictionary used. (ltl_simplifier::as_bdd): New function, exported from the cache. * src/tgbaalgos/ltl2tgba_fm.cc (translate_dict): Store the ltl_simplifier object. (translate_dict::boolean_to_bdd): Call ltl_simplifier::as_bdd. (translate_ratexp): New wrapper around the ratexp_trad_visitor, calling boolean_to_bdd whenever possible. (ratexp_trad_visitor): Do not deal with negated formulae, there are necessarily Boolean and handled by translate_ratexp(). (ltl_visitor): Adjust to call translate_ratexp. (ltl_to_tgba_fm): Adjust passing of the ltl_simplifier to the translate_dict, and make sure everybody is using the same dictionary. * src/tgbatest/ltl2tgba.cc: Pass the dictionary to the ltl_simplifier.
07e40e70