* src/ltlvisit/nenoform.cc, src/ltlvisit/lunabbrev.cc,
src/ltlvisit/simpfg.cc, src/ltlvisit/tunabbrev.cc: Do not recurse
if the formula properties indicate that it is already in the right
form.

* src/ltlast/unop.cc (NegClosure): Reset is.not_marked.
* src/ltlvisit/mark.hh,
src/ltlvisit/mark.cc (has_mark_visitor, has_mark): Remove.
* src/tgbaalgos/ltl2tgba_fm.cc: Use f->is_marked() instead
of has_mark(f).

They are too slow.

* src/ltlast/formula.hh (opkind, kind, kind_): Use an enum
to indicate the actual kind of the formula.  This way we can
check the kind of a formula without relying on dynamic_cast.
* src/ltlast/atomic_prop.cc, src/ltlast/automatop.cc,
src/ltlast/binop.cc, src/ltlast/bunop.cc, src/ltlast/constant.cc,
src/ltlast/multop.cc, src/ltlast/refformula.cc,
src/ltlast/refformula.hh, src/ltlast/unop.cc: Adjust constructors.
* src/ltlvisit/basicreduce.cc, src/ltlvisit/mark.cc,
src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc,
src/ltlvisit/tostring.cc: Replace all dynamic_cast by a
call to kind() followed by a static_cast.

* src/ltlast/formula.hh (formula::accepts_eword): New method.
(formula::is.accepting_eword): New flag.
* src/ltlast/formula.cc (print_formula_props): Display the new
property.
* src/ltlast/atomic_prop.cc, src/ltlast/automatop.cc,
src/ltlast/binop.cc, src/ltlast/bunop.cc, src/ltlast/constant.cc,
src/ltlast/multop.cc, src/ltlast/unop.cc: Update
is.accepting_eword as appropriate.
* src/ltltest/consterm.cc, src/tgbaalgos/ltl2tgba_fm.cc: Adjust to
use accepts_eword().
* src/ltlvisit/consterm.cc, src/ltlvisit/consterm.hh: Delete.
* src/ltlvisit/Makefile.am: Remove these files.

This bitfield is easily updated as the formulae are constructed.
Doing so avoids many AST recursions to compute these properties
individually.  This patch removes the eventual_universal_visitor,
as well as the kind_of() function.

* src/ltlast/formula.hh (is_boolean, is_sugar_free_boolean,
is_in_nenoform, is_X_free, is_sugar_free_ltl,
is_ltl_formula, is_eltl_formula, is_psl_formula, is_eventual,
is_universal, is_marked): New methods to query formula
properties in constant time.
(get_props, ltl_prop): A method and structure for
implementation as a field bit in an unsigned, for fast
computation.
(print_formula_props): New function.
* src/ltlast/formula.cc (print_formula_props): Implement it.
* src/ltlast/atomic_prop.cc, src/ltlast/binop.cc,
src/ltlast/bunop.cc, src/ltlast/constant.cc, src/ltlast/multop.cc,
src/ltlast/unop.cc, src/ltlast/automatop.cc: Compute the
properties as instances are constructed.
* src/ltlparse/ltlparse.yy: Update to use is_boolean() instead
of kind_of().
* src/ltltest/kind.cc: Update to use print_formula_props().
* src/ltltest/kind.test: Adjust to test eventual and universal
properties.
* src/ltlvisit/kind.cc, src/ltlvisit/kind.hh: Delete these files.
* src/ltlvisit/Makefile.am: Remove kind.hh and kind.cc.
* src/ltlvisit/reduce.cc (recurse_eu, eventual_universal_visitor):
Remove, no longer needed.
(reduce_visitor, is_eventual, is_universal): Adjust to
use formula::is_eventual(), and formula::is_universal().
* src/ltlvisit/reduce.hh (is_eventual, is_universal): Declare as
deprecated.

* src/ltlast/binop.cc (binop::instance): Simplify fUf, fRf, fWf,
and fRF.
* src/ltlast/binop.hh: Document it.
* src/ltltest/equals.test: Add new tests for 'Exp U Exp'
and 'Exp R Exp', and all missing tests for W and M.

* src/ltlast/unop.hh, src/ltlast/unop.cc: Replace the
simplification by an assert.

The new rewriting are (Exp => Exp) = 1, (Exp <=> Exp) == 1,
and (Exp ^ Exp) == 0.

* src/ltlast/binop.hh: Fix documentation.
* src/ltlast/binop.cc: Fix implementation.
* src/ltltest/equals.test: More tests.
* src/tgbatest/emptchk.test: Remove a useless test.

* src/ltlparse/ltlscan.ll: Handle p=0Wq=1 and p=0Mq=1 in
the same way as we did for
* src/ltltest/parse.test: More tests.

* src/ltlparse/ltlscan.ll (OP_SQBKT_SEP): Accept ":" and "to"
in addition to ".." and ",".
(OP_UNBOUNDED): Recognize "$" for the rule below.
* src/ltlparse/ltlparse.yy: Accept [OP1:$] as a synonym
for [OP1:], for people used to SVA's syntax.
* src/ltltest/equals.test: Test these syntaxes.

* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_trad_visitor): Take a
"negated" parameter and use it.

* src/ltlvisit/consterm.cc: Stop the recursion on [->] and [=].

* src/ltlast/bunop.hh: Declare bunop::Goto
* src/ltlast/bunop.cc: Handle it.
* src/ltlparse/ltlparse.yy,
src/ltlparse/ltlscan.ll: Add rules for [->min..max].
* src/tgbaalgos/ltl2tgba_fm.cc: Handle bunop::Goto in
the translation.
* src/ltltest/equals.test: Test trivial identities.
* src/tgbatest/ltl2tgba.test: Test two more formulae using [->].

* src/ltlast/bunop.cc: Implement this rewriting.
* src/ltlast/bunop.hh: Document it.
* src/ltltest/equals.test: Test it.

* src/ltlast/bunop.hh: Declare bunop::Equal
* src/ltlast/bunop.cc: Handle it.
* src/ltlparse/ltlparse.yy,
src/ltlparse/ltlscan.ll: Add rules for [=min..max].
* src/tgbaalgos/ltl2tgba_fm.cc: Handle bunop::Equal in
the translation.
* src/ltltest/equals.test: Test trivial identities
for [=min..max].
* src/tgbatest/ltl2tgba.test: Add new formulae to test.

* src/ltlast/unop.cc: Simplify ![*0] as 1[+].
* src/ltlast/unop.hh: Document it.

* src/ltlvisit/kind.hh, src/ltlvisit/kind.cc: New files.
* src/ltlvisit/Makefile.am: Add them.
* src/ltltest/kind.test, src/ltltest/kind.cc: New files.
* src/ltltest/Makefile.am: Add them.

* src/ltlast/bunop.cc (bunop::format): Output [*1..] as [+].
* src/ltlvisit/tostring.cc: Output "a*" as "a[*]" for consistency.
* src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Recognize [+].
* src/ltltest/tostring.test, src/ltltest/equals.test,
src/tgbatest/ltl2tgba.test: More tests.

* src/ltlast/bunop.hh, src/ltlast/bunop.cc: New files for
bounded unary operators.
* src/ltlast/Makefile.am, src/ltlast/allnodes.hh: Add them.
* src/ltlast/predecl.hh (bunop): Declare.
* src/ltlast/unop.hh, src/ltlast/unop.cc (Star): Remove
declaration of Star and associated code.
* src/ltlast/visitor.hh: Add visit(bunop* node) methods.
* src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Add parse
rules for LTL.  This required passing the parse_error list
to the lexer, so it can report scanning errors when it reads
a number that does not fit in an unsigned int.
* src/ltlparse/parsedecl.hh (YY_DECL): Take error_list
as third argument.
* src/ltltest/consterm.test, src/ltltest/tostring.test,
src/ltltest/equals.test, src/tgbatest/ltl2tgba.test: More tests.
* src/ltlvisit/basicreduce.cc, src/ltlvisit/clone.cc,
src/ltlvisit/clone.hh, src/ltlvisit/consterm.cc,
src/ltlvisit/dotty.cc, src/ltlvisit/mark.cc,
src/ltlvisit/nenoform.cc, src/ltlvisit/postfix.cc,
src/ltlvisit/postfix.hh, src/ltlvisit/reduce.cc,
src/ltlvisit/syntimpl.cc, src/ltlvisit/tostring.cc,
src/ltlvisit/tunabbrev.cc, src/tgba/formula2bdd.cc,
src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2taa.cc,
src/tgbaalgos/ltl2tgba_lacim.cc: Adjust syntax to use
"bunop::Star" instead of "unop::Star".
* src/tgbaalgos/ltl2tgba_fm.cc: Likewise, but also adjust
the code to handle the bounds of the operator.

* src/ltlvisit/tostring.cc: Use braces for unary operators in
Star.
* src/ltltest/tostring.test: Add some PSL formulae, it cannot
hurt.

* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_trad_visitor::visit): Fix
the "deterministic case" of []->, and merge it with the
non-deterministic case.

* src/ltlparse/ltlparse.yy: Recognize "*" as "1*".
* src/ltlvisit/tostring.cc: Abbreviate "1*" as "*".
* src/tgbatest/ltl2tgba.test: Use the new syntax.

* src/ltlparse/ltlscan.ll: Recognize "[]=>" (a.k.a "|=>") and "<>=>".
* src/ltlparse/ltlparse.yy: Support them by rewriting them using
"[]->" and "<>->".
* src/tgbatest/ltl2tgba.test: More tests.

* src/ltlparse/ltlparse.yy (rationalexp): Recognize "OP_NOT
booleanatom".
* src/ltlvisit/consterm.cc, src/tgbaalgos/ltl2tgba_fm.cc: Adjust.
* src/tgbatest/ltl2tgba.test: Add one test.

* src/ltlast/multop.cc, src/ltlast/multop.hh: Declare AndNML
operator.
* src/ltlparse/ltlscan.ll: Distinguish "&" and "&&".
* src/ltlparse/ltlparse.yy: Handle them both as "And" for LTL
formula, use AndNML or And for rational expressions.
* src/ltlvisit/tostring.cc: Adjust to distinguish "&" and "&&" in
rational expressions. Also use {braces} to group rational
expressions.
* src/tgbaalgos/ltl2tgba_fm.cc
(ratexp_trad_visitor::ratexp_trad_visitor): Remove the possibility
to select the empty_word should act like true, and fix the rules
for Closure and NegClosure to rely on constant_term instead.
(ratexp_trad_visitor::visit) Adjust the And translation to also
support AndNML.
(ratexp_trad_visitor::recurse_and_concat): Introduce this new
method to simplify some calls to recurse(f, to_concat_).
* src/tgbatest/ltl2tgba.test: Add more test cases.
* src/ltlvisit/basicreduce.cc, src/ltlvisit/consterm.cc,
src/ltlvisit/contain.cc, src/ltlvisit/mark.cc,
src/ltlvisit/nenoform.cc, src/ltlvisit/syntimpl.cc,
src/tgba/formula2bdd.cc, src/tgbaalgos/eltl2tgba_lacim.cc,
src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_lacim.cc: Add
missing cases in switches.

* src/ltlparse/ltlparse.yy (parenthesedsubformula): Extract these
rules from...
(subformula): ... here, and use it to recognize "{SERE}(formula)".
* src/ltlparse/ltlscan.ll: Recognize "|->" as "[]->".
* src/ltltest/equals.test: Test these two new syntaxes.

* src/ltlparse/ltlscan.ll: Recognize [*] as *, and use
[*0] instead of #e for the empty word.
* src/ltlast/binop.cc, src/ltlast/constant.cc,
src/ltlast/multop.cc, src/ltlast/multop.hh, src/ltlast/unop.cc,
src/ltlast/unop.hh, src/ltltest/consterm.test,
src/ltltest/equals.test: Adjust all occurrences of #e to [*0].
* src/tgbatest/ltl2tgba.test: Also use [*].

* src/ltlparse/ltlparse.yy (rationalexp): Allow bracedrationalexp.
* src/ltltest/consterm.test, src/tgbatest/ltl2tgba.test: Add more
tests.

* src/ltlast/unop.hh, src/ltlast/unop.cc: Introduce Closure and
NegClosure operators.
* src/ltlparse/ltlparse.yy: Recognize {foo} as a Closure.
* src/ltlvisit/mark.cc: Consider NegClosure as a marked operator.
* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_trad_visitor): Add option to
select whether the empty_word should act like true (for {SERE}
and {!SERE}) or false (for {SERE}<>->Exp or {SERE}[]->Exp).
(ltl_trad_visitor): Translate Closure and NegClosure.
* src/tgbatest/ltl2tgba.test: Add more tests.
* src/ltlvisit/basicreduce.cc, src/ltlvisit/consterm.cc,
src/ltlvisit/nenoform.cc, src/ltlvisit/reduce.cc,
src/ltlvisit/syntimpl.cc, src/ltlvisit/tostring.cc,
src/ltlvisit/tunabbrev.cc, src/tgba/formula2bdd.cc,
src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2tgba_lacim.cc,
src/tgbaalgos/ltl2taa.cc: Straightforward update to support or
assert on these new operators.

* src/tgbaalgos/ltl2tgba_fm.cc (ltl_trad_visitor::visit): Honor
exprop_ while handling the binop::UConcat case.

* wrap/python/tests/ltlsimple.py: Adjust.

* src/tgbaalgos/ltl2tgba_fm.cc (ltl_trad_visitor): Take
an exprop argument, and use it while translation <>-> operators.
* src/tgbatest/ltl2tgba.test (check_psl): Use -x too.

* src/ltlast/multop.hh (multop::type::Fusion): New operator.
* src/ltlast/multop.cc: Handle it.
* src/ltlparse/ltlparse.yy: Declare OP_FUSION and add grammar
rules.
* src/ltlparse/ltlscan.ll: Recognize ":" as OP_FUSION.
* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_trad_visitor::visit):
Add translation rule for multop::Fusion.
* src/tgbatest/ltl2tgba.test: Add more tests.
* src/ltlvisit/basicreduce.cc, src/ltlvisit/consterm.cc,
src/ltlvisit/contain.cc, src/ltlvisit/mark.cc,
src/ltlvisit/nenoform.cc, src/ltlvisit/syntimpl.cc,
src/ltlvisit/tostring.cc, src/tgba/formula2bdd.cc,
src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2taa.cc,
src/tgbaalgos/ltl2tgba_lacim.cc: Handle multop::Fusion in switches.

For instance "(a+#e);(b+#e);(c*)" does.

* src/ltlvisit/consterm.cc: Fix handling of Concat operator.
* src/ltltest/consterm.test: Add more tests.

* src/tgbaalgos/ltl2tgba_fm.cc: Implement translation for
recently introduced operators.
* src/tgbatest/ltl2tgba.test: Add some PSL tests.

* src/ltlvisit/mark.cc, src/ltlvisit/mark.hh: New files.
* src/ltlvisit/Makefile.am: Add mark.hh and mark.cc.

* src/ltlast/binop.cc, src/ltlast/binop.hh: Introduce
EConcatMarked ("<>+>").
* src/ltlvisit/basicreduce.cc, src/ltlvisit/consterm.cc,
src/ltlvisit/lunabbrev.cc, src/ltlvisit/nenoform.cc,
src/ltlvisit/reduce.cc, src/ltlvisit/simpfg.cc,
src/ltlvisit/syntimpl.cc, src/ltlvisit/tostring.cc,
src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/eltl2tgba_lacim.cc,
src/tgbaalgos/ltl2tgba_lacim.cc, src/tgba/formula2bdd.cc,
src/tgba/formula2bdd.cc: Deal with it if possible or ignore
it.

* src/ltlast/multop.cc: Handle it.

* src/ltlast/binop.cc: Add simplification rules.