1. 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
  2. 26 Aug, 2016 5 commits
  3. 19 Aug, 2016 1 commit
  4. 17 Aug, 2016 1 commit
  5. 26 Jul, 2016 4 commits
  6. 25 Jul, 2016 3 commits
  7. 21 Jul, 2016 1 commit
  8. 19 Jul, 2016 1 commit
    • Johannes Kanig's avatar
      Allow to keep unmatched theories · 4c744eba
      Johannes Kanig authored
      When Why3 is run on a file where some theories have been suppressed, it
      will delete the corresponding theories from the session file.  We now
      add an option keep_unmatched_theories to Session.update_session, which
      keeps all theories. In this commit, this option is always disabled.
      This is useful for SPARK, which sometimes only generates part of the
      Why3 file for efficiency reasons, but doesn't want the session file to
      be damaged because of that.
      * session.ml
      (import_transf): new functions to copy a session tree from an old
        session file
      (merge_file): keep old theories when keep_unmatched_theories is true
      * session_scheduler.ml
      (update_session): pass keep_unmatched_theories
      * why3session_lib.ml
      (read_update_session): pass keep_unmatched_theories
  9. 11 Jul, 2016 1 commit
  10. 05 Jul, 2016 3 commits
  11. 04 Jul, 2016 3 commits
  12. 02 Jul, 2016 1 commit
  13. 01 Jul, 2016 4 commits
  14. 10 Jun, 2016 4 commits
  15. 03 Jun, 2016 1 commit
  16. 24 May, 2016 1 commit
  17. 20 May, 2016 3 commits
  18. 18 May, 2016 1 commit