1. 04 Mar, 2019 1 commit
  2. 18 Feb, 2019 1 commit
    • Guillaume Melquiond's avatar
      Rework numerical constants. · d3d7c7ac
      Guillaume Melquiond authored
      Main changes are:
      - Real constants now offer a normalized representation usable for internal
        computations.
      - Constants are no longer stored in textual form.
      d3d7c7ac
  3. 11 Feb, 2019 1 commit
  4. 01 Feb, 2019 1 commit
  5. 30 Jan, 2019 1 commit
  6. 22 Oct, 2018 2 commits
  7. 16 Oct, 2018 1 commit
  8. 22 Jun, 2018 1 commit
  9. 17 May, 2018 1 commit
  10. 12 Mar, 2018 1 commit
    • Sylvain Dailler's avatar
      Change the way counterexamples are parsed · 3ea32678
      Sylvain Dailler authored
      The way records are recognized during model parsing is changed:
      we previously recognized records during parsing by looking at the name of
      the variable returned by the prover (mk_r mk__rep etc).
      Now, we collect the names of constructor of records (recognized using
      their id_string beginning with "mk ") during the printing of the smt2
      files. So, after parsing of the model, we can match the name of an
      application with a previously collected constructor: we can recreate
      the record.
      
      The same can be done for all algebraic datatype.
      
      This change also solve the problem of parsing in ce-bench.
      3ea32678
  11. 16 Feb, 2018 1 commit
  12. 11 Jan, 2018 1 commit
  13. 22 Sep, 2017 1 commit
  14. 05 Jul, 2017 2 commits
  15. 10 Jun, 2017 2 commits
  16. 09 Jun, 2017 1 commit
  17. 03 May, 2017 1 commit
  18. 12 Apr, 2017 1 commit
  19. 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
  20. 23 Nov, 2016 1 commit
    • Sylvain Dailler's avatar
      Add a name_table in proof_node. · e0d6b38d
      Sylvain Dailler authored
      Add a name_table in printer_args.
      Put the definition of name_table in task.ml.
      Build_name_tables only called once in proof_node creation.
      Modified the rest accordingly.
      e0d6b38d
  21. 26 Oct, 2016 1 commit
  22. 02 Sep, 2016 1 commit
    • Sylvain Dailler's avatar
      Why3 counterex: Changing the way counterex value are get from prover. · 86ebcd21
      Sylvain Dailler authored
      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.
      86ebcd21
  23. 10 Jun, 2016 1 commit
  24. 15 Mar, 2016 3 commits
  25. 11 Sep, 2015 1 commit
  26. 22 Jul, 2015 2 commits
  27. 15 Jul, 2015 1 commit
  28. 03 Jun, 2015 1 commit
  29. 26 May, 2015 1 commit
  30. 20 Mar, 2015 1 commit
  31. 19 Mar, 2015 1 commit
  32. 04 Mar, 2015 1 commit
  33. 03 Mar, 2015 1 commit
  34. 25 Feb, 2015 1 commit