(so that we can use it with 'why3 execute')

For every check, we now print the "check_tree" into the JSON output.
This is basically a dump of the session tree, just in a different
format.

* json.ml
new json datatype and new function "print_json" to print it

Change-Id: I0b28ac181793af4d160abc58c2634b3cbcac9b94

Parsing reference was forgotten in commit for Q217-025. This solves the
problem with a new token MK_ANYTHING.

* src/driver/parse_smtv2_model_lexer.mll
(parse): Added lexing for all remaining mk*___ record constructs.

* src/driver/parse_smtv2_model_parser.mly
(smt_term): An smt_term can be a reference to a smt_term. It means it can
be (Mk_anything smt_term).

Change-Id: Ib529fee83d16d09266e526ca5fb3c65526addff5

Added a counter for constructors. We print a new functions to redefine
constructors only if there is a need.

* src/printer/smtv2_cvc_ce.ml
(print_constructor_decl): Added counter.
(print_data_decl): Added counter.
(print_saved_constructors): Print only if number of constructors in the
list is greater than counter.

Change-Id: Iad0f29caac961644dcbf4137341abd76c01e1090

Do not print (get-info :reason-unknown) on smt2 output. Previously,
detection of end of model and beginning of statistics was done by using
the reason. We now detect a single parenthesis on a line: every cvc4 model
ends with this (we assume statistics does not contain a line beginning
with a closing parenthesis). As a side effect, we also find
more counterexamples.

* src/driver/parse_smtv2_model.ml
(parse): Revert changes that were detecting Abort trap.

* src/driver/parse_smtv2_model_parser.mly
(output): Revert changes to allow absence of parenthesis at the end. Also
removed parsing on results given by the reason. Now match on ).

* src/printer/smtv2_cvc_ce.ml
(print_prop_decl): Remove (get-info :reason-unknown).

* src/printer/smtv2.ml
(print_prop_decl): Remove get-info for coherence.

Change-Id: Ifbd7b2b9ce499f8aaa020f58375d784793990965

This patch allows parsing model including the error message raised by cvc4
on mac.

* src/driver/parse_smtv2_model.ml
(parse): Allow parsing of specific error message "Abort trap".
(output): Allow parsing when last parenthesis is missing which is the case
when the bug is occuring.

Change-Id: I80d7276d37916e09ba4bb28478ac9a7427789771

Change-Id: Id165717756375db150031589740470cc1e08b8ac

This commit solves a CVC4 limitation on boolean inside datatypes for CE.
It converts them to bv by adding a new printer. This commit is a hack and
it will be reverted when the bug is solved in CVC4.

* Makefile.in
(Makefile): Added new printer.
* drivers/smtv-libv2_cvc_ce.drv:
(printer): new printer used is smtv2_cvc_ce
* src/driver/parse_smtv2_model_lexer.mll
(parse): Changed the way constructor of datatype are detected.
* src/printer/smtv2_cvc_ce.ml
(print_constructors): Projections to bool are changed to projections
to bitvectors. Duplicate projections are generated which returns bool and
are used in the rest of smtv2 generated.

Change-Id: Ib2eba92aa788938b0bec30f8c156e9b235896881

This commit allows parsing of the result of get-model from smtsolvers.
It changes the communication between why3 and Spark for CE to communicate
records and array as JSON values.

 * src/core/model_parser.ml
(model_value): Adding boolean and record type to model values.
(print_*): Changed printing functions to print arrays and records as JSON
values not as strings.

 * src/driver/collect_data_model.ml
(get_variables_*): collect all internal variables of a term and put them
into a map.
(add_all_cvc): Add all cvc4 variables in the model to a global map.
(add_vars_to_table): Add values of variables that can be deduced from ITE
 to the table.
(corres_else_element): Take the definitions of functions to_rep/of_rep
and extract the values of internal CVC variables from it.
(refine_*): Recursively replace internal variables in a term with values
taken from the table.
(convert_*): Convert to type model_value from model_parser.ml.
(create_list): Combine the following to get a list of model_value from
the parsing of the model.

* src/driver/parse_smtv2_model.ml
(parse): Changed the detected end of model.

* src/driver/parse_smtv2_model_lexer.mll
(rule): Added tokens related to model definitions and SPARK definitions of
records, discriminants and ref.

* src/driver/parse_smtv2_model_parser.mly
(output): Changed the parser so that it can parse a model as returned by
Cvc4 or z3.

* src/driver/smt2_model_defs.ml
(print_*): Added printing functions for terms.
(make_local*): Changes the AST of terms to differentiate smtsolver
internal variables, user-defined variables and local variables.
(subst*): Removes the local let bindings introduced by z3.
(build_record_discr): Put definitions of discriminants inside the record
definition.

 * src/printer/smtv2.ml
(print_logic_decl): Removed get-values and added get-model.

* src/transform/intro_projections_counterexmp.ml
(intro_const_equal_to_term): Only allow projections for attributes first,
last and field projections. Necessary when the field of a record is
itself on array on which we want to get First and Last.

* src/transform/intro_vc_vars_counterexmp.ml
(do_intro): Some definitions moved to intro_projections_counterexmp.ml.

Change-Id: Ib77fb66a2f7c53a9f54cfc300c8984e1fcec8087

Good thing, there is no more any version-specific Coq realizations

forgot to add .mli file to commit

Change-Id: I28d89aa1f85ff5a3e19a495babcdd707545607f4

We set the error mode in the why3 server. This has two effects:
- disable pop-ups in case of crashes of why3server;
- inherit this setting to all spawned prover processes.

* server-win.c
(main): call SetErrorMode

Change-Id: I93862d51aebe1d4639ab1d463c08366f79375a7a

The extmap.ml file was taken (and extended) from ocaml 3.12 and has not
been updated since. Since then, ocaml map.ml has evolved and contains
some space optimizations.

The commit contains more changes than strictly needed. The objective is
to be as close as possible to map.ml from ocaml 4.04. After this patch,
the 'diff' wrt. map.ml  contains almost exclusively additions, and no
other changes.

Change-Id: I3e31f6068562e5e1c48f8426efc9ce4e2f5b6010