1. 10 May, 2016 1 commit
    • Johannes Kanig's avatar
      P509-017 fix incorrect time limits · 34f472e9
      Johannes Kanig authored
      The adaptation of time limits was incorrect, and could transform "0" (no
      time limit) to "1" (second).
      
      * call_provers.ml
      (adapt_limit): do nothing when no time limit was present
      34f472e9
  2. 20 Apr, 2016 1 commit
    • Andrei Paskevich's avatar
      Call_provers: simplify API · 8159c0d7
      Andrei Paskevich authored
      Call_provers:
      
      - drop closures "pre_prover_call" and "post_prover_call". They were
        intended to be used for synchronous interaction with provers from
        multiple threads. This is now responsibility of the proof server:
        (a) any Call_prover.call_on_[file|buffer] submits the proof task
            immediately to the server;
        (b) all proof results are handled in the working Why3 thread.
      
      - Call_provers.query_call returns a tri-state "prover_update" type
        which can be one of: "ProverStarted" (returned after the proof
        server informs Why3 that a prover was started), "ProverFinished"
        (returned after the proof server returns the prover result), and
        "NoUpdates" (returned when the proof server has not sent any new
        updates concerning the proof task in question).
      
          IMPORTANT: query_call does not maintain the state of a given
        prover call. In a normal use case, "ProverFinished" is returned
        _exactly_ once, and "ProverStarted" _at_most_ once (never for
        an editor call or when rapidly overwritten by "ProverFinished").
      
          TODO: extend the proof server protocol and implementation to
        send "ProverStarted" events back to Why3.
      8159c0d7
  3. 15 Apr, 2016 2 commits
  4. 14 Apr, 2016 6 commits
  5. 12 Apr, 2016 2 commits
  6. 11 Apr, 2016 1 commit
  7. 10 Apr, 2016 1 commit
  8. 05 Apr, 2016 1 commit
  9. 25 Mar, 2016 1 commit
    • Johannes Kanig's avatar
      replace prover spawning by connection to why3server · 69b8ed31
      Johannes Kanig authored
      * previous implementations of call_on_file and call_on_buffer are
        removed, and now directly use the prove_file_server function
      * now, both blocking and nonblocking reading is supported on the socket
      * wait_on_call and query_call are implemented by blocking and
        nonblocking read, together with a result buffer, if results for other
        prover runs are returned
      * logging of the server is now optional
      69b8ed31
  10. 19 Mar, 2016 1 commit
  11. 17 Mar, 2016 2 commits
  12. 15 Mar, 2016 3 commits
  13. 14 Mar, 2016 1 commit
  14. 10 Mar, 2016 1 commit
  15. 08 Mar, 2016 2 commits
  16. 17 Nov, 2015 2 commits
    • David Hauzar's avatar
      6b21ff73
    • David Hauzar's avatar
      Query cvc4 for reason of answer unknown and use it for counterexamples. · 5c3038bf
      David Hauzar authored
      When resource limit is hit, cvc4 outputs useless counterexample. Query
      cvc4 for the reason of answer unknown and use the answer to decide
      whether resource limit was hit. If it was hit, do not display the
      counterexample.
      
      * src/driver/call_provers.{ml|mli}
      (parse_prover_run): If the prover answers unknown, get the information
      about the reason of this answer.
      
      * src/printer/smtv2.ml
      (print_prop_decl): Query solver for the reason of answer unknown.
      
      * src/driver/driver.ml
      (load_driver): Initialize Unknown with no information about the reason
      of answer unknown.
      
      * src/session/session.ml
      (load_result): Initialize Unknown with no information about the reason
      of answer unknown.
      
      * src/session/session_scheduler.ml
      (schedule_proof_attempt)
      (edit_proof): Initialize Unknown with no information about the reason
      of answer unknown.
      
      * src/why3session/why3session_lib.ml
      (filter_spec): Initialize Unknown with no information about the reason
      of answer unknown.
      5c3038bf
  17. 26 Jul, 2015 1 commit
  18. 22 Jul, 2015 1 commit
  19. 16 Jul, 2015 2 commits
    • David Hauzar's avatar
      7573c8b4
    • David Hauzar's avatar
      Adding information about the line that corresponds to the VC check · 68b3134d
      David Hauzar authored
      to the counter-example model.
      
      This line must be marked with the label "model_vc".
      If VC line is postcondition, it can be marked with the label
      "model_func" or "model_func:func_name". Terms corresponding to
      old values of arguments will be marked with @old, term corresponding
      to the function result will be marked with @result or
      func_name@result if func_name was given.
      
      Pretty printing of model element names in counter-example.
      Possibility to print differently model elements corresponding to
      function result, old values of function arguments and other model
      elements.
      68b3134d
  20. 03 Jun, 2015 1 commit
  21. 26 May, 2015 1 commit
  22. 23 May, 2015 1 commit
  23. 13 May, 2015 2 commits
  24. 15 Apr, 2015 1 commit
  25. 23 Mar, 2015 1 commit
  26. 21 Mar, 2015 1 commit