- 07 Dec, 2017 1 commit
-
-
Guillaume Melquiond authored
-
- 12 Nov, 2017 1 commit
-
-
Guillaume Melquiond authored
It is needed for compiling the Coq tactic Why3.vo file when native compilation is disabled. This commit also avoid a potential race condition when Why3.vo was compiled with both the native and bytecode compilers.
-
- 19 Oct, 2017 1 commit
-
-
Guillaume Melquiond authored
-
- 30 Sep, 2017 1 commit
-
-
Guillaume Melquiond authored
-
- 29 Sep, 2017 1 commit
-
-
Guillaume Melquiond authored
-
- 26 Sep, 2017 3 commits
-
-
Guillaume Melquiond authored
-
Guillaume Melquiond authored
-
Guillaume Melquiond authored
-
- 08 Sep, 2017 1 commit
-
-
Stefan Berghofer authored
-
- 24 Aug, 2017 1 commit
-
-
Guillaume Melquiond authored
-
- 17 Aug, 2017 1 commit
-
-
Sylvain Dailler authored
Change prelude to AUFBVDTNIRA and removed smt-libv2-cvc-ce.drv
-
- 19 Apr, 2017 1 commit
-
-
Jean-Christophe Filliâtre authored
-
- 12 Apr, 2017 3 commits
-
-
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
-
- 11 Apr, 2017 2 commits
-
-
MARCHE Claude authored
Good thing, there is no more any version-specific Coq realizations
-
MARCHE Claude authored
-
- 05 Apr, 2017 1 commit
-
-
MARCHE Claude authored
-
- 09 Mar, 2017 1 commit
-
-
Clément Fumex authored
-
- 06 Mar, 2017 1 commit
-
-
Andrei Paskevich authored
-
- 28 Feb, 2017 1 commit
-
-
Clément Fumex authored
* 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.
-
- 29 Jan, 2017 1 commit
-
-
Jean-Christophe Filliâtre authored
for teaching purposes only limited to a microscopic fragment of Python for the moment
-
- 25 Jan, 2017 1 commit
-
-
Clément Fumex authored
+ 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
-
- 11 Jan, 2017 1 commit
-
-
Guillaume Melquiond authored
-
- 05 Jan, 2017 1 commit
-
-
Clément Fumex authored
+ simplify some others + add a realization of real.Truncate + add a, almost complete, realization (missing fma related axioms + some non-axiomatized definitions)
-
- 03 Jan, 2017 4 commits
-
-
MARCHE Claude authored
-
Stefan Berghofer authored
-
MARCHE Claude authored
-
Guillaume Melquiond authored
-
- 08 Dec, 2016 1 commit
-
-
Kim Nguyen authored
-
- 07 Dec, 2016 1 commit
-
-
Kim Nguyen authored
[trywhy3] Allow one to compile trywhy3 with debugging information and source map file by passing DEBUGJS=yes to make.
-
- 20 Oct, 2016 1 commit
-
-
Andrei Paskevich authored
-
- 09 Sep, 2016 1 commit
-
-
Jean-Christophe Filliâtre authored
now correctly updates the examples contained in sub-directories
-
- 06 Sep, 2016 1 commit
-
-
Sylvain Dailler authored
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
-
- 02 Sep, 2016 1 commit
-
-
Guillaume Melquiond authored
-
- 17 Aug, 2016 1 commit
-
-
Guillaume Melquiond authored
-
- 25 Jul, 2016 1 commit
-
-
MARCHE Claude authored
-
- 05 Jul, 2016 3 commits
-
-
Guillaume Melquiond authored
-
Guillaume Melquiond authored
-
Guillaume Melquiond authored
-