GitLab

The way records are recognized during model parsing is changed:
we previously recognized records during parsing by looking at the name of
the variable returned by the prover (mk_r mk__rep etc).
Now, we collect the names of constructor of records (recognized using
their id_string beginning with "mk ") during the printing of the smt2
files. So, after parsing of the model, we can match the name of an
application with a previously collected constructor: we can recreate
the record.

The same can be done for all algebraic datatype.

This change also solve the problem of parsing in ce-bench.

Formerly we only parsed elements of float values as decimals when they can
be hexadecimal.

* src/driver/parse_smtv2_model_lexer.mll
(float_num): Now takes hexadecimal number instead of decimal numbers.

Change-Id: Ie3c4e3452c7cb68af8767d2859bfbb4bb90e607e

This commit adds parsing for boolean expression and floating point value
which are returned by z3 on the last version. This adds floating point
values in the collected data and JSON printed data. This does not add
boolean expressions because it does not add information.
Also added transformation eliminate epsilon in driver for Z3 ce.

* drivers/z3_gnatprove_ce.drv
(eliminate_epsilon): Added transformation eliminate epsilon in driver for
counterex for z3.

* src/core/model_parser.ml
(float_type): Added a float_type and functions to send it as JSON data.

* src/driver/collect_data_model.ml
(convert_array_value): Explicit matching for error handling when adding
constructs.
(convert_float): Dummy conversion of float_type to avoid circular
dependency.

* src/driver/parse_smtv2_model_lexer.mll
(token): Adding z3 specific boolean expressions. Also adding a way to
parse all floating point value including those we don't want to print
because we need to parse them even if we don't want to print them.

* src/driver/parse_smtv2_model_parser.mly
(smt_term): Adding floating point value case which is handled in the lexer.
Added boolean_expression case.

* src/driver/smt2_model_defs.ml
(float_type): Adding a duplicated float_type for dependencies reasons.
(print_float): Debugging print of float_type.
(): Adding cases for float in remaining functions.

Change-Id: I5baee2880a9843f0fec61b1bf3edb2a2f3e54bd1

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

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

We added the generation of identifiers for counterex values inside the
printer of altergo.
Also added a file to factorize counterex printing functions that are used
for both altergo and smtv2.

* Makefile.in
(cntexmp_printer): Factorization file added to Makefile.

* src/driver/parse_smtv2_model_lexer.mll
(MODEL): Adding model keyword.

* src/driver/parse_smtv2_model_parser.mly
(output): Added parsing when keyword model is at beginning of the
 output of the prover.

* src/printer/alt_ergo.ml
Adding info mimicking smtv2.ml inside most printing functions for counterex
generation.

* src/printer/cntexmp_printer.ml
Common functions to alt_ergo.ml and smtv2.ml

* src/printer/smtv2.ml
Removed functions that are factorized into cntexmp_printer.ml

In a counterexample model returned by cvc4, values can be also of the form
"(mk_t__ref([0-9]*) (value))", while only the form "(mk_t__ref (value))"
was supported.

* src/driver/parse_smtv2_model_lexer.mll
MK_T__REF can be of the form "mk_t__ref([0-9]*)".

Enabling the transformation detect_polymorphism caused some variables be
of reference type and their values outputed in the form "mk_t__ref value".
This was not recognized by the counterexample model parser.

* src/driver/parse_smtv2_model_lexer.mll
Add new token corresponding to string "mk_t__ref"

* src/driver/parse_smtv2_model_parser.mly
Value can be also of the form "(mk_t__ref value)"

The value of bitvector can not fit into integer range (it can be, e.g,
9223372036854775881). Values of bitvectors are stored as strings and not
converted to integers.

Parsing bitvectors in the counterexample returned by the prover.