- 12 Jun, 2017 6 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
- 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)
-
- 08 Jun, 2017 1 commit
-
-
MARCHE Claude authored
-
- 24 May, 2017 1 commit
-
-
MARCHE Claude authored
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
-
- 22 May, 2017 1 commit
-
-
MARCHE Claude authored
The underlying Monoid does not need to be commutative, and is indeed not in example fibonacci.mlw
-
- 19 May, 2017 3 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
- 16 May, 2017 1 commit
-
-
MARCHE Claude authored
-
- 15 May, 2017 1 commit
-
-
Guillaume Melquiond authored
-
- 12 May, 2017 1 commit
-
-
MARCHE Claude authored
-
- 10 May, 2017 2 commits
-
-
MARCHE Claude authored
-
François Bobot authored
-
- 05 May, 2017 1 commit
-
-
Mário Pereira authored
-
- 27 Apr, 2017 1 commit
-
-
Martin Clochard authored
-
- 20 Apr, 2017 3 commits
-
-
Jean-Christophe Filliâtre authored
(so that we can use it with 'why3 execute')
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
- 19 Apr, 2017 1 commit
-
-
Jean-Christophe Filliâtre authored
-
- 13 Apr, 2017 2 commits
-
-
Guillaume Melquiond authored
-
Guillaume Melquiond authored
-
- 12 Apr, 2017 13 commits
-
-
MARCHE Claude authored
-
Sylvain Dailler authored
-
Johannes Kanig authored
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
-
Sylvain Dailler authored
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
-
Sylvain Dailler authored
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
-
Sylvain Dailler authored
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
-
Sylvain Dailler authored
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
-
Sylvain Dailler authored
Change-Id: Id165717756375db150031589740470cc1e08b8ac
-
Sylvain Dailler authored
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
-
Sylvain Dailler authored
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
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
- 11 Apr, 2017 2 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-