GitLab

This allows to have one line less in transformations.

- bring driver syntax closer to that of theories
- some simple API improvements

Since its already incorrect no encoding for simplify, and also no trigger because its buggy inside simplify

- everything is converted to the new shiny way of doing things.
  Well, everything except Gappa, which seems very unifinished anyway,
  and Encoding_instantiate, which is too complex and would like to 
  update it with François.

Also, I commented a little piece of exception reporting in manager/,
will see it with Claude.

THIS IS STILL A WORK IN PROGRESS!
Please inform me about any bugs, ugly APIs, and proposed corrections.

All the non-implemented things, mentioned in the previous commit
message are still in the TODO list and will be done soon.

- dependent transformations (ones that depend on cloning history
  and/or metaproperties) have now the same type Trans.trans and
  can be registered via Trans, too.
- load_driver accumulates appropriate tdecls to be appended to
  tasks before transformation/printing.

At this moment, we have almost everything in place and are ready
to remove Register module (subsumed by Trans and Printer in core/)
and Prover module (its functions will move to Driver), and convert
all printers and transformations to use the new infrastructure. 

Not implemented yet:
- appending driver-imposed tdecls to tasks - when and where?
- metas-options - what is the best way to implement them?
- syntax/typing for metas in theories and drivers.

- introduce a new Theory.tdecl "Meta" to be used for tags
- simplify cloning procedure, get rid of the th_clone field
- when a goal proposition is discarded during cloning, 
  it's still keeped in the theory as a "skip proposition",
  this is needed to preserve/clone every local identifier.
  Skip propositions are eliminated during task formation.
- get rid of a separate Task.tdecl type
- reorganize the Task.task_hd record:
  * use/clone history is cached in a theory-keyed map;
  * meta-properties are cached in a tagname-keyed map.
  This is done to simplify the fine-grained configuration
  of transformations.

alt-ergo : trigger pas sur l'égalité

traitemant des triggers dans encoding decorate (des cas pathologiques peuvent aboutir a des quantifications non totales

corrected bug in tptp parser (associativity)

code is still quite ugly, and more testing is required

added eprover to solvers
refactoring and cleaning in tptp printer

tptp output now manages 0-arity functors,
and lowercase functor names

The printer exists but is not yet usable.

printer : print_prelude inside printers instead of prover.ml. Required for smt which has its own prelude.