1. 06 Feb, 2018 1 commit
  2. 11 Jan, 2018 1 commit
  3. 26 Dec, 2017 3 commits
  4. 24 Dec, 2017 3 commits
  5. 11 Dec, 2017 3 commits
    • MARCHE Claude's avatar
      check realizations: generate them in a fresh temporary directory · f071fac7
      MARCHE Claude authored
      additional cosmetic changes
      f071fac7
    • MARCHE Claude's avatar
      cosmetic changes · 9a43c12a
      MARCHE Claude authored
      - do not erase Isabelle's XML files even in local mode
      
      - use realization*s* with an s everywhere
      9a43c12a
    • Sylvain Dailler's avatar
      Update configure and regtests / nightly-build so that realization are · 190492a8
      Sylvain Dailler authored
      generated again.
      
      * Makefile.in
      Realizations for isabelle are generated even if Isabelle is not installed.
      The .thy file are checked only if isabelle is installed. This allows us
      to treat it as with coq and be able to detect changes in realizations
      with a script.
      Dont erase xml generated file during clean.
      
      * configure.in
      Changed the configure to always generate a default isabelle version (set
      to 2017) for generation of the realization driver (needed even when no
      isablle support is given).
      
      * examples/regtests.sh
      Adding option --check-realization and --only-realization which add a test
      the compares the output of the new realization compared to the one
      recorded. It complains if they are different forcing the user to update the
      realization files.
      
      * lib/isabelle/*
      Adding xml files corresponding to generated realization for Isabelle. This
      allows for the abovementionned script to work even if Isabelle is not
      installed (which is the case for most people editing theories).
      
      * examples/nightly-bench.sh
      Add the option for realization check
      
      * misc/ci-bench
      Calls the test for realization
      
      Conflicts:
      	examples/regtests.sh
      190492a8
  6. 08 Dec, 2017 1 commit
  7. 07 Dec, 2017 2 commits
  8. 29 Nov, 2017 1 commit
  9. 27 Nov, 2017 1 commit
  10. 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
  11. 19 Oct, 2017 1 commit
  12. 30 Sep, 2017 1 commit
  13. 29 Sep, 2017 1 commit
  14. 26 Sep, 2017 3 commits
  15. 08 Sep, 2017 1 commit
  16. 24 Aug, 2017 1 commit
  17. 17 Aug, 2017 1 commit
  18. 19 Apr, 2017 1 commit
  19. 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
  20. 11 Apr, 2017 2 commits
  21. 05 Apr, 2017 1 commit
  22. 09 Mar, 2017 1 commit
  23. 06 Mar, 2017 1 commit
  24. 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
  25. 29 Jan, 2017 1 commit
  26. 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
  27. 11 Jan, 2017 1 commit
  28. 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