Doing so will release all BDD variables used by automata created for
syntactic implication. This way the main translation will create
acceptance variables again in a more natural order, which will help
the degeneralization (until we get a better degeneralization).
* src/ltlvisit/contain.cc, src/ltlvisit/contain.hh
(language_containment_checker::clear): New method to clear the
containment cache.
* src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh
(clear_as_bdd_cache): Also call language_containment_checker::clear.
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.
* src/ltlvisit/snf.cc, src/ltlvisit/snf.hh: New files.
* src/ltlvisit/Makefile.am: Distribute them.
* src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh: Call snf(f) for
all f[*].
* src/ltltest/reduccmp.test: Test it.
* doc/tl/tl.tex, doc/tl/tl.bib: Document it.
* src/ltlvisit/simplify.hh (ltl_simplifier_options): New option
reduce_size_stricly.
* src/ltlvisit/simplify.cc (simplify_visitor): Implement these
rules.
* src/ltltest/reduc.cc: Check with reduce_size_strictly unset or
set, but only use the latter result to check sizes.
* src/ltltest/reduccmp.test: Test them.
* doc/tl/tl.tex: Document them.
* 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.
* src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh
(are_equivalent): Export this function from the cache.
* src/ltltest/reduc.cc, src/ltltest/equals.cc: Use
are_equivalent() to check that the reductions are legitimate.
So that we can latter use some combined optimizations.
* src/ltlvisit/simplify.hh, src/ltlvisit/simplify.cc: Integrate
the code from syntimpl.cc
* src/ltlvisit/syntimpl.hh, src/ltlvisit/syntimpl.cc: Delete. All
code has been moved above.
* src/ltlvisit/Makefile.am: Adjust.
* src/ltltest/syntimpl.cc: Adjust code.
* src/ltlvisit/simplify.hh, src/ltlvisit/simplify.cc
(ltl_simplify::negative_normal_form): Remove the third
parameter and always rewrite XOR, =>, and <=>. This avoid
problems with the cache, that could have been populated with
a different value for this third parameter.
* src/ltltest/reduc.cc, src/tgbaalgos/ltl2tgba_fm.cc: Adjust
calls to negative_normal_form().
* src/ltltest/nenoform.test: Adjust tests.
* 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.
* src/ltlvisit/simplify.cc: Integrate the tau03
containment rules.
* src/ltlvisit/simplify.hh: Add options to select simplifications.
* src/ltlvisit/reduce.cc (reduce): Do not call reduce_tau03().
* src/ltlvisit/contain.cc (reduce_tau03_visitor): Remove.
(reduce_tau03): Implement it using ltl_simplifier.
It is limited to negative_normal_form_visitor for now.
* src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh: New files.
* src/ltlvisit/Makefile.am: Add them.
* src/ltlvisit/nenoform.cc, src/ltlvisit/nenoform.hh: Rewrite
using ltl_simplifier.
