- most important improvement : the explanation, used as first part
  of the shape was computed twice ! (at least)
- several improvements in the implementation, avoid using Format
  in particular (done also in checksum computations)
- possible further improvements:
    do not compute shapes if checksums are OK
       (they must be the same as in previous session)
    do not compute goal checksums if theory checksum is OK
       (they must be the same as in previous session)

If drivers in why3.conf are simple names like "alt_ergo", then the driver file
is search as <datadir>/drivers/alt_ergo.drv

This behavior is now the same as when a driver is given with option -D on the
command line for why3prove, why3replay or why3extract

Reminder: the datadir is either given as
1) the environment variable WHY3DATA
2) the field "datadir" of the [main] section of the
   why3 config file if exists
3) or by default the compile-time datadir

* declare range types and float types,
* use integer (resp. real) literals for those types through casting,
* specify how to print them in drivers.

Change in syntax
* use

  type t = < range 1 2 >   (* integers from 1 to 2 *)
  type t' = < float 4 12 > (* float with 4 bits in exponent and 12 in mantissa *)

  the two projections :
  t'int
  t''real

  and the predicate :
  t''isFinite

* Restrict the use of "'" in whyml:
  Users are not allowed to introduce names where a quote symbol
  is followed by a letter. Thus, the following identifiers are
  valid:

  t'
  toto'0''
  toto'_phi

  whereas toto'phi is not.

Note: we do not yet support negative numbers in range declaration
and casting of a literal.

  added in 9577acb9

When Why3 is run on a file where some theories have been suppressed, it
will delete the corresponding theories from the session file.  We now
add an option keep_unmatched_theories to Session.update_session, which
keeps all theories. In this commit, this option is always disabled.

This is useful for SPARK, which sometimes only generates part of the
Why3 file for efficiency reasons, but doesn't want the session file to
be damaged because of that.

* session.ml
(import_theory)
(import_goal)
(import_proof_attempt)
(import_transf): new functions to copy a session tree from an old
  session file
(merge_file): keep old theories when keep_unmatched_theories is true
* session_scheduler.ml
(update_session): pass keep_unmatched_theories
* why3session_lib.ml
(read_update_session): pass keep_unmatched_theories

When sessions are saved and then loaded from disk, goal identifiers are
properly qualified. This is not the case when goals are still in memory
due to reloading a file in the ide. So merging can get confused since
several goals potentially share the same base name.

makes API of Call_provers and Driver a bit simpler

When resource limit is hit, cvc4 outputs useless counterexample. Query
cvc4 for the reason of answer unknown and use the answer to decide
whether resource limit was hit. If it was hit, do not display the
counterexample.

* src/driver/call_provers.{ml|mli}
(parse_prover_run): If the prover answers unknown, get the information
about the reason of this answer.

* src/printer/smtv2.ml
(print_prop_decl): Query solver for the reason of answer unknown.

* src/driver/driver.ml
(load_driver): Initialize Unknown with no information about the reason
of answer unknown.

* src/session/session.ml
(load_result): Initialize Unknown with no information about the reason
of answer unknown.

* src/session/session_scheduler.ml
(schedule_proof_attempt)
(edit_proof): Initialize Unknown with no information about the reason
of answer unknown.

* src/why3session/why3session_lib.ml
(filter_spec): Initialize Unknown with no information about the reason
of answer unknown.

triggers VC in Model_parser.model and printing them.

It finished for why3prove but not finishedfor why3ide yet.

If these are set, the prover is asked for counter-example and if the counter-example is got, it is displayed.

Sessions may contain the status "stepslimitexceeded", but this was not
actually parsed by the session parser. Now fixed.

characters '. ", <, > and &

+ fixed wrong step limit in one session

Parsing a model returned by the solver -  added possibility to specify the parser of model in the driver.