GitLab

This patch also simplifies the specification of the floating-point
equality.

Adding "I don't know" as a correct keyword for provers return (inside
counterexamples).
Updating scripts because of move from hoare_logic to WP_revisited.

* src/driver/parse_smtv2_model.ml
(parse): Adding I dont know as a keyword.

* bench/bench
Changing to WP_revisited.

* examples/bench.sh
Changing to WP_revisited.

* examples/regtests.sh
Changing to WP_revisited.

now correctly updates the examples contained in sub-directories

simplifies the gallery update

add exception handler for int_of_string failure and raise the correct
exception here

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

This commit solve a problem raised by Mohamed Iguernlala. If provers give
more values than asked, the results of counterex becomes inconsistent.

We changed the way corresponding terms are associated to counterex value.
Now we have a map containing the term corresponding to a counterex asked to
a prover.

* src/core/model_parser.ml
(construct_name): Takes a string and create a model_name.
(build_model_rec): Changed to use term_map which allow a name of asked
counterex to correspond to the term asked.

* src/core/printer.ml
(printer_mapping): Changed type of queried_terms to store correspondance
between names and terms.
(printer_args): Changed initial value of queried_terms accordingly.

* src/core/smtv2.ml
(print_info_model): This function now returns the map of names to terms.
(print_prop_decl): Changed variable model_list accordingly.

I introduced bug with last counterexample commit. This was due to
querying counterexample value of variables that were not introduced. This
commits introduce a container that save introduced variables and check if
they should be taken as counterex.

* src/transform/intro_vc_vars_counterexmp.ml
(do_intro): Adding vc_var which contains all variables that we can safely
print as counterexamples.
(remove_positive_foralls): Adding vc_var and introduce variables in vc_var
when quantified over.
(intros): Adding vc_var.
(do_intro_vc_vars_counterexmp): Adding vc_var.

Change-Id: Ic6bf732f1e50241a42df8e097f52aa46dd473bd2

We changed the prepare_for_counterexamples transformation to allow
printing of quantified expressions, remove duplications of printed
examples and adding an incomplete function to print universally
quantified variables that are positive but not at head of the term.

* src/transform/intro_projections_counterexmp.ml
(intro_const_equal_to_term): Generating of the preid for a counterex.

* src/transform/intro_projections_counterexmp.mli
(val_intro_const_equal_to_term): Changing signature.

* src/transform/intro_vc_vars_counterexmp.ml
(Hprid): Adding a container for preids.
(do_intro): Adding cases for generation of counterexample in the Tvar
case, factorising the construction of vc_constant in a function
new_counter_example_variable. Adding argument vc_map to avoid
duplication of vc_constants
(new_counter_example_variable): Adding a check to avoid duplication of
vc_constant.
(remove_positive_foralls): New experimental incomplete function that aims
at introducting foralls even when they are under a construct.
"H /\ forall i. P(i)" becomes "i as premisse and H /\ P(i)".
(intros): Added calls to do_intro and removed optimizations.
(do_intro_vc_vars_counterexmp): Concatenate results of intros and
do_intros and create the prop goal.

* src/transform/introduction.ml
(stop_intro): Removed stop_intro.

* src/transform/prepare_for_counterexmp.ml
(prepare_for_counterexmp2): Removed call to introduce_premisses.

Change-Id: I836ae9e69b887247eb64196705cc7ad32ba36825

The sum of two positive (resp. negative) FP numbers should always be
positive (resp. negative), even when the result is zero.

This commit also cleans a bit some other parts of the specification of FP
operations.