1. 12 Nov, 2017 1 commit
    • Guillaume Melquiond's avatar
      Detect whether coqtop.byte is present. · 4ff1dd2a
      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.
      4ff1dd2a
  2. 19 Oct, 2017 1 commit
  3. 30 Sep, 2017 1 commit
  4. 29 Sep, 2017 1 commit
  5. 26 Sep, 2017 3 commits
  6. 08 Sep, 2017 1 commit
  7. 24 Aug, 2017 1 commit
  8. 17 Aug, 2017 1 commit
  9. 19 Apr, 2017 1 commit
  10. 12 Apr, 2017 3 commits
    • Sylvain Dailler's avatar
      Q217-025 Printer to smt2: convert bool term inside type to bv · a303ae72
      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
      a303ae72
    • Sylvain Dailler's avatar
      Q217-025 Use get-model instead of get-values for CE · 1f6da25d
      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
      1f6da25d
    • MARCHE Claude's avatar
      update header for year 2017 · 216f2ecd
      MARCHE Claude authored
      216f2ecd
  11. 11 Apr, 2017 2 commits
  12. 05 Apr, 2017 1 commit
  13. 09 Mar, 2017 1 commit
  14. 06 Mar, 2017 1 commit
  15. 28 Feb, 2017 1 commit
    • Clément Fumex's avatar
      Add the ability to · f0547868
      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.
      f0547868
  16. 29 Jan, 2017 1 commit
  17. 25 Jan, 2017 1 commit
    • Clément Fumex's avatar
      + remove unused constant half · 5a44ec01
      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
      5a44ec01
  18. 11 Jan, 2017 1 commit
  19. 05 Jan, 2017 1 commit
    • Clément Fumex's avatar
      + remove a few wrong axioms · 9a94aeb8
      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)
      9a94aeb8
  20. 03 Jan, 2017 4 commits
  21. 08 Dec, 2016 1 commit
  22. 07 Dec, 2016 1 commit
  23. 20 Oct, 2016 1 commit
  24. 09 Sep, 2016 1 commit
  25. 06 Sep, 2016 1 commit
    • Sylvain Dailler's avatar
      Why3 altergo counterex - Allowing values to be printed for Altergo · a5d0aa0b
      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
      a5d0aa0b
  26. 02 Sep, 2016 1 commit
  27. 17 Aug, 2016 1 commit
  28. 25 Jul, 2016 1 commit
  29. 05 Jul, 2016 4 commits