• Alexandre Duret-Lutz's avatar
    Move the remaining reduce() logic into ltl_simplifier. · c0085a8f
    Alexandre Duret-Lutz authored
    * src/ltlvisit/simplify.hh
    (ltl_simplifier::negative_normal_form): Allow logical
    unabbreviations during the NNF pass.
    * src/ltlvisit/simplify.cc
    (ltl_simplifier::negative_normal_form)
    (negative_normal_form_visitor): Adjust.
    (ltl_simplifier::simplify): Request unabbreviations.
    * src/ltlvisit/reduce.cc (reduce): Remove most
    of the code, leaving only a call ltl_simplifier
    and some wrapper code to convert options.
    * src/ltltest/reduccmp.test: Add more test cases.
    c0085a8f
reduccmp.test 6.39 KB