GitLab

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

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

in preparation of command-line option --mono

Adding support in drivers for Zarith and the ocaml.mlw file

for teaching purposes only
limited to a microscopic fragment of Python for the moment

+ add predicate "exact_int"
+ add three axioms on of_int +/-/*
+ add some other axioms
+ guard the theory realization with a dependency to flocq in make file

+ simplify some others
+ add a realization of real.Truncate
+ add a, almost complete, realization (missing fma related axioms + some non-axiomatized definitions)

[trywhy3] Allow one to compile trywhy3 with debugging information and source map file by passing DEBUGJS=yes to make.

Dummy C printer added

Attempt to make it generic, using registered extraction functions

Compiles but not working yet