This fixes invariant computation for a program symbol whose signature
contains a new tuple symbol. The early call of flush_tuples will miss
the tuple symbols inside specifications, but these do not participate
in invariant computation, and are not a worry. We still have to use
add_pdecl_with_tuples to catch them, though.

this heuristic does not show any real benefit in our tests.
Most of the time we are better off with per-function annotations.

in a series of tests on available examples, lightweight polymorphism
encoding techniques combined with a more agressive generation of
monomorphic instances (via Discriminate) show better results than
our earlier defaults.

In the same commit:
- remove Encoding_explicit (unsound), Encoding_decoexp (too naive),
  and Encoding_instantiate (subsumed by Discriminate)
- rename Encoding_decorate to Encoding_tags_full and Encoding_guard
  to Encoding_guards_full
- move Encoding_guards_full specific functions from Libencoding to
  Encoding_guards_full
- do not apply type protection in "encoding_tptp" and remove
  Protect_finite which is not needed anymore.