Skip to content
  • Alexandre Duret-Lutz's avatar
    Translate Boolean formulae as BDD using the ltl_simplifier cache. · 07e40e70
    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