GitLab

- put abstract types and aliases in Dtype of tysymbol
- put (recursive) algebraic types in Ddata of (ts,constr list) list
- put abstract function/predicate symbols in Dparam of lsymbol
- put defined logic symbols in Dlogic of (ls,ls_definition) list

also, remove all customization from the Z3 3.x section in prover detection.
I find it morally wrong to chase magic options of a closed-source program.
We should add an option for a prover only when we have clear understanding
of what it does and good reasons to believe that it is useful in our case.

but not use it by default, because of bad caching of smt_encoding
transformations. Because of this, new function symbols appear again
and again, and since we don't forget function symbols in trans-based
printers, we obtain names like at234.

also, introduce in Printer the p-printing transformations

Prover capabilities are now represented by a record enumerating each case and which syntax to use then.
This fixes output of nondecimal integers to provers (bug #12981).

TODO: check whether some provers support more than just decimal representations.

Rename as little as possible and keep the API.
Make all the necessary checks in Term and Decl.
Remove the duplicate code in Term but keep it elsewhere.
We will factorize the code as we go, without rush.

encoding_sort   : identity on meta lsymbol without definition
                  undefined symbol are defined before using them...

courses  WP_registerStudent : 0.53 s -> 0.03!!

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

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

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