* src/tgbaalgos/ltl2tgba_fm.cc (translate_ratexp): Replace
a dynamic cast by a call to kind().

* doc/tl/tl.tex: Document the rules.
* src/ltlvisit/simplify.cc (simplify_visitor): Implement them.
* src/ltltest/reduccmp.test: Test them.

* src/ltlvisit/simplify.cc (simplify_visitor): Do it.
* src/ltltest/reduccmp.test: Add a test.
* doc/tl/tl.tex: Document it.
* src/ltlast/multop.cc: Fix the computation of is.accepting_eword
for Fusion.  The Fusion operator never accepts [*0].

* src/ltlvisit/simplify.cc (simplify_visitor): Do it.
* src/ltltest/reduccmp.test: Add more tests.
* doc/tl/tl.tex: Document it.

* doc/tl/Makefile.am: Rewrite using latexmk instead of texi2dvi.
Also define the SpotVersion when calling latexmk, not in tl.tex.
* doc/tl/tl.tex: Assume SpotVersion is defined outside the file.

* src/ltlvisit/mark.hh, src/ltlvisit/mark.cc (mark_concat_ops,
simplify_mark): Rewrite these two functions as methods of
(mark_tools): this new class.
* src/ltlast/binop.cc, src/ltlast/unop.cc: Adjust computation
of not_marked to ignore marked operators that are not at
the top-level.  I.e., something like X(!{a}) is not marked.
* src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::mt): New
instance of mark_tools.
(formula_canonizer::translate) Adjust calls to
mark_concat_ops() and simplify_mark().

* src/ltlast/binop.cc, src/ltlast/binop.hh: Here.
* doc/tl/tl.tex, src/ltltest/equals.test: Adjust.

* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_to_dfa::translate): Do not
translate a subformula if we have already proved it useless in
a previous rational expression.
* src/tgbatest/ltl2tgba.test: Add an example, although that
test does not ensure the subformula is ignored early in the
translation.  I.e., it would still work without the patch.

* src/kernel.h (PAIR, TRIPLE): Redefine these hash functions
using something that is simpler to compute.

* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_to_dfa::translate,
ltl_to_tgba_fm): Do not convert labels as Boolean formulas before
creating transitions.  Use the bdd directly, and register the used
transitions later.

* src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::ltl_to_bdd):
Use boolean_to_bdd()

We used to cache it only for formulas used as states.

* src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::ltl_to_bdd): New method.
(ltl_trad_visitor::recurse): Use ltl_to_bdd().
(formula_canonizer): Likewise.
(ltl_to_tgba_fm): Adjust.

* src/ltlast/unop.cc: Perform the simplification.
* src/ltlast/unop.hh, doc/tl/tl.tex: Document it.
* src/ltltest/equals.test: Adjust test cases.

* src/tgbaalgos/minimize.cc (minimize_obligation): Do not check
the output of minimize_wdba if the input formula is a syntactic
obligation.

* doc/tl/Makefile.am, doc/tl/tl.tex, doc/tl/tl.bib: New files.
* doc/Makefile.am (SUBDIRS): Recurse into tl/.
* configure.ac: Output doc/tl/Makefile
* README: Describe doc/tl/.

This fixes a bug where {(a&!a)[=2]} was translated either into an
universal automaton (with simplification turned off) or in an
empty automaton (with simplification turned on).

* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_to_dfa::translate): Trim
the automaton.
(ratexp_to_dfa::succ, ratexp_to_dfa::get_label): Deal with trimed
states.
(ltl_trad_visitor::visit(unop::Closure)): Likewise.
* src/tgbatest/ltl2tgba.test, src/ltltest/reduccmp.test: New test
cases.

This is especially important when translating the Closure
operators, because normally we should only keep the satisfiable
formulae (i.e. co-accessible states), which seems hard to check on
the fly.  After this patch we need to teach
ratexp_to_dfa::translate() how to trim (and then minimize) the DFA
to prune those useless (non co-accessible) states.

* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_to_dfa): New class.
(translate_dict::transdfa): New member.
(ltl_trad_visitor::visit(unop::Closure)): Use transdfa.

* src/ltlvisit/simplify.cc (syntactic_implication_aux): Refine
rules to deal with pure eventualities and purely universal
properties.
* src/ltltest/reduccmp.test: Add tests.

* 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 (inf_left_recurse_visitor,
inf_right_recurse_visitor): Remove.
(syntactic_implication, syntactic_implication_aux): Rewrite all
rules for syntactic implication.
(syntactic_implication_neg): Simplify.

* src/ltlvisit/randomltl.cc (bunop_bounded_builder,
bunop_bool_bounded_builder): Set the maximum value
to 3 instead of 4, to speed up the test suite.

* src/ltlvisit/contain.cc
(language_containment_checker::contained,
language_containment_checker::neg_contained,
language_containment_checker::contained_neg): Detect
cases where both formulae are equal.

* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_trad_visitor::visit): Fix
the translation of the Goto operator.
(ratexp_trad_visitor::next_to_concat): More comments.
* src/ltltest/reduccmp.test: Add a test case.

* src/tgbaalgos/ltl2tgba_fm.cc (trace_ltl_bdd):
Declare as unused.

* 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.

* src/ltlast/binop.cc: a M b is eventual if both a and b are
eventual, or if b == 1.  a W b is universal if both a and b
are universal or if b == 0.
* src/ltltest/kind.test: New test case.

* src/ltlvisit/simplify.cc (syntactic_implication): Here.

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/contain.hh (reduce_tau03): Mark as deprecated.
* src/tgbaalgos/ltl2tgba_fm.cc, src/tgbatest/ltl2tgba.cc,
src/ltltest/equals.cc: Do not include ltlvisit/contain.hh, since
it's not used.

* src/ltlvisit/basicreduce.cc, src/ltlvisit/basicreduce.hh: Delete.
* src/ltlvisit/Makefile.am: Remove them.

* src/ltlvisit/reduce.hh: Mark the file as obsolete.
(reduce): Declare this function as obsolete.
* src/ltlvisit/reduce.cc: Define SKIP_DEPRECATED_WARNING
so we can include reduce.hh.
* src/sanity/includes.test: Also use SKIP_DEPRECATED_WARNING
when compiling headers.
* iface/dve2/dve2check.cc,
src/ltltest/equals.cc, src/ltltest/randltl.cc,
src/ltltest/reduc.cc, src/tgbaalgos/ltl2tgba_fm.hh,
src/tgbaalgos/ltl2tgba_fm.cc, src/tgbatest/randtgba.cc,
wrap/python/ajax/spot.in, wrap/python/spot.i: Adjust
to use ltl_simplifier.
* src/tgbatest/ltl2tgba.cc: Adjust to use ltl_simplifier,
and replace -fr1...-fr7 options by a single -fr option.
* src/tgbatest/spotlbtt.test: Adjust -fr flags accordingly.
* src/tgbatest/reductgba.cc: Do not include reduce.hh.

* 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 (simplify_visitor): Fix it,
and leave the trace code.

* src/ltlvisit/simplify.cc (ltl_simplifier::simplify):
Convert in negative normal form if needed.
* src/ltlvisit/reduce.cc (reduce): Do not call
negative_normal_form().

* 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.

* src/ltlvisit/simplify.cc (ltl_simplifier): Adjust
code.
* src/ltltest/reduccmp.test: Add some test cases.

* src/ltlvisit/simplify.cc (ltl_simplifier): Add more rewritings
for formulae that are both universal and eventual.
* src/ltltest/reduccmp.test: Add six more cases.