1. 26 Sep, 2016 2 commits
  2. 22 Sep, 2016 2 commits
  3. 21 Sep, 2016 1 commit
  4. 19 Sep, 2016 1 commit
    • Sylvain Dailler's avatar
      Keeping keep_on_simp labels during wp generation. · 64b1fda4
      Sylvain Dailler authored
      We changed t_map_simp, track_values and the eval_match transformation
      in order to prevent them from removing terms whose head has label
       keep_on_simp. Note that simplification inside those terms is
      still possible.
      * src/core/term.ml
      (t_map_simp): Adding the case when f has label keep_on_simp.
      * src/transform/eval_match.ml
      (eval_match): Adding keep_on_simp as a stop label.
      * src/whyml/mlw_wp.ml
      (track_values): Stopping on keep_on_simp label.
  5. 16 Sep, 2016 1 commit
  6. 15 Sep, 2016 2 commits
  7. 14 Sep, 2016 6 commits
  8. 09 Sep, 2016 4 commits
  9. 06 Sep, 2016 3 commits
    • 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
      * 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
    • Guillaume Melquiond's avatar
      Merge branch 'bugfix/v0.87' · 219c8bb3
      Guillaume Melquiond authored
    • Martin Clochard's avatar
  10. 02 Sep, 2016 2 commits
    • 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.
    • Guillaume Melquiond's avatar
  11. 01 Sep, 2016 3 commits
  12. 31 Aug, 2016 4 commits
  13. 30 Aug, 2016 2 commits
    • Sylvain Dailler's avatar
      P530-020 counterex - Disallow printing of value not introduced · 76c67c9c
      Sylvain Dailler authored
      I introduced bug with last counterexample commit. This was due to
      querying counterexample value of variables that were not introduced. This
      commits introduce a container that save introduced variables and check if
      they should be taken as counterex.
      * src/transform/intro_vc_vars_counterexmp.ml
      (do_intro): Adding vc_var which contains all variables that we can safely
      print as counterexamples.
      (remove_positive_foralls): Adding vc_var and introduce variables in vc_var
      when quantified over.
      (intros): Adding vc_var.
      (do_intro_vc_vars_counterexmp): Adding vc_var.
      Change-Id: Ic6bf732f1e50241a42df8e097f52aa46dd473bd2
    • Sylvain Dailler's avatar
      P530-020 counterex - Printing quantified variables · 27b053f3
      Sylvain Dailler authored
      We changed the prepare_for_counterexamples transformation to allow
      printing of quantified expressions, remove duplications of printed
      examples and adding an incomplete function to print universally
      quantified variables that are positive but not at head of the term.
      * src/transform/intro_projections_counterexmp.ml
      (intro_const_equal_to_term): Generating of the preid for a counterex.
      * src/transform/intro_projections_counterexmp.mli
      (val_intro_const_equal_to_term): Changing signature.
      * src/transform/intro_vc_vars_counterexmp.ml
      (Hprid): Adding a container for preids.
      (do_intro): Adding cases for generation of counterexample in the Tvar
      case, factorising the construction of vc_constant in a function
      new_counter_example_variable. Adding argument vc_map to avoid
      duplication of vc_constants
      (new_counter_example_variable): Adding a check to avoid duplication of
      (remove_positive_foralls): New experimental incomplete function that aims
      at introducting foralls even when they are under a construct.
      "H /\ forall i. P(i)" becomes "i as premisse and H /\ P(i)".
      (intros): Added calls to do_intro and removed optimizations.
      (do_intro_vc_vars_counterexmp): Concatenate results of intros and
      do_intros and create the prop goal.
      * src/transform/introduction.ml
      (stop_intro): Removed stop_intro.
      * src/transform/prepare_for_counterexmp.ml
      (prepare_for_counterexmp2): Removed call to introduce_premisses.
      Change-Id: I836ae9e69b887247eb64196705cc7ad32ba36825
  14. 26 Aug, 2016 6 commits
  15. 24 Aug, 2016 1 commit