-
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