command for steps different from regular command

share/provers-detection-data.conf

@@ -7,8 +7,10 @@ version_switch = "-version"
 version_regexp = "\\([0-9.]+\\(-dev\\|~beta.prv\\)?\\)"
 version_ok  = "0.99.1"
 version_ok  = "0.95.2"
-command = "%l/why3-cpulimit %t %m -s %e -timelimit %t %f"
-command_steps = "%l/why3-cpulimit %t %m -s %e -steps-bound %S %f"
+# %T means timelimit+1
+command = "%l/why3-cpulimit %T %m -s %e -timelimit %t %f"
+# %U means 2*timelimit+1
+command_steps = "%l/why3-cpulimit %U %m -s %e -steps-bound %S %f"
 driver = "drivers/alt_ergo.drv"
 editor = "altgr-ergo"
 
@@ -22,27 +24,11 @@ version_regexp = "\\([0-9.]+\\(-dev\\)?\\)"
 version_old = "0.95.1"
 version_old = "0.95"
 command = "%l/why3-cpulimit %T %m -s %e -timelimit %t %f"
+# Alt-Ergo print steps but do not have an option to pass them for replay
+command_steps = "%l/why3-cpulimit %T %m -s %e -timelimit %t %f"
 driver = "drivers/alt_ergo.drv"
 editor = "altgr-ergo"
 
-# [ATP alt-ergo-model]
-# name = "Alt-Ergo"
-# alternative = "models"
-# exec = "alt-ergo"
-# exec = "alt-ergo-0.95.3"
-# exec = "alt-ergo-0.95.2"
-# exec = "alt-ergo-0.95.1"
-# exec = "alt-ergo-0.95"
-# exec = "alt-ergo-0.95-dev"
-# version_switch = "-version"
-# version_regexp = "\\([0-9.]+\\(-dev\\)?\\)"
-# version_ok  = "0.95.1"
-# version_old = "0.95"
-# version_old = "0.95-dev"
-# command = "%l/why3-cpulimit %T %m -s %e -timelimit %t -model %f"
-# driver = "drivers/alt_ergo_model.drv"
-# editor = "altgr-ergo"
-
 [ATP alt-ergo]
 name = "Alt-Ergo"
 exec = "alt-ergo"
@@ -51,6 +37,8 @@ version_switch = "-version"
 version_regexp = "\\([0-9.]+\\)"
 version_old = "0.94"
 command = "%l/why3-cpulimit %t %m -s %e %f"
+# Alt-Ergo print steps but do not have an option to pass them for replay
+command_steps = "%l/why3-cpulimit %t %m -s %e %f"
 driver = "drivers/alt_ergo_0.94.drv"
 editor = "altgr-ergo"
 
@@ -87,34 +75,20 @@ version_old = "0.8"
 command = "%l/why3-cpulimit %t %m -s %e %f"
 driver = "drivers/alt_ergo_0.92.drv"
 
-# CVC4 version 1.5-prerelease
-[ATP cvc4]
-name = "CVC4"
-exec = "cvc4"
-exec = "cvc4-1.5-prerelease"
-version_switch = "--version"
-version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
-version_ok  = "1.5-prerelease"
-driver = "drivers/cvc4.drv"
-# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
-# to try: --inst-when=full-last-call
-command = "%l/why3-cpulimit %T %m -s %e --stats --tlimit-per=%t000 --lang=smt2 %f"
-command_steps = "%l/why3-cpulimit %T %m -s %e --stats --rlimit=%S --lang=smt2 %f"
-
-# CVC4 version 1.4
+# CVC4 version >= 1.4
 [ATP cvc4]
 name = "CVC4"
 exec = "cvc4"
 exec = "cvc4-1.4"
+exec = "cvc4-1.5-prerelease"
 version_switch = "--version"
 version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
 version_ok  = "1.4"
 driver = "drivers/cvc4_14.drv"
 # --random-seed=42 is not needed as soon as --random-freq=0.0 by default
 # to try: --inst-when=full-last-call
-# --rlimit=%S : cvc4 1.4 DOES NOT accept -1 as argument
-# cvc4 .14 does not print steps used in --stats anyway
 command = "%l/why3-cpulimit %T %m -s %e --tlimit-per=%t000 --lang=smt2 %f"
+command_steps = "%l/why3-cpulimit %U %m -s %e --rlimit=%S --lang=smt2 %f"
 
 # CVC4 version 1.0 to 1.3
 [ATP cvc4]
@@ -168,7 +142,6 @@ version_switch = "-version"
 version_regexp = "This is CVC3 version \\([^ \n]+\\)"
 version_old = "2.2"
 version_old = "2.1"
-# we pass time 0 to why3-cpulimit to avoid race
 command = "%l/why3-cpulimit %T %m -s %e  -seed 42 -timeout %t %f"
 driver = "drivers/cvc3.drv"
 
@@ -211,7 +184,6 @@ version_old = "1.7"
 version_old = "1.6"
 version_old = "1.5"
 version_old = "1.4"
-# we pass time 0 to why3-cpulimit to avoid race
 command = "%l/why3-cpulimit %T %m -s %e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f"
 driver = "drivers/eprover.drv"
 
@@ -303,7 +275,6 @@ exec = "vampire"
 exec = "vampire-0.6"
 version_switch = "--version"
 version_regexp = "Vampire \\([0-9.]+\\)"
-# we pass time 0 to why3-cpulimit to avoid race
 command = "%l/why3-cpulimit %T %m -s %e -t %t"
 driver = "drivers/vampire.drv"
 version_ok = "0.6"

src/driver/call_provers.ml

@@ -122,9 +122,12 @@ let print_prover_status fmt = function
   | Unix.WSIGNALED n -> fprintf fmt "killed by signal %d" n
   | Unix.WEXITED n -> fprintf fmt "exited with status %d" n
 
+let print_steps fmt s =
+  if s >= 0 then fprintf fmt ", %d steps)" s
+
 let print_prover_result fmt
-  {pr_answer=ans; pr_status=status; pr_output=out; pr_time=t} =
-  fprintf fmt "%a (%.2fs)" print_prover_answer ans t;
+  {pr_answer=ans; pr_status=status; pr_output=out; pr_time=t; pr_steps=s} =
+  fprintf fmt "%a (%.2fs%a)" print_prover_answer ans t print_steps s;
   if ans == HighFailure then
     fprintf fmt "@\nProver exit status: %a@\nProver output:@\n%s@."
       print_prover_status status out

src/driver/whyconf.ml

@@ -714,7 +714,7 @@ let merge_config config filename =
   { config with main = main; provers = provers; strategies = strategies;
     prover_shortcuts = shortcuts; editors = editors }
 
-let debug = Debug.register_info_flag "whyconf"
+let _debug = Debug.register_info_flag "whyconf"
   ~desc:"Print@ debugging@ messages@ about@ whyconf."
 
 let save_config config =

src/mlw/dexpr.ml

@@ -1149,6 +1149,7 @@ and expr_fun ~keep_loc uloc env pvl dsp de =
 
 (*
 let val_decl ?(keep_loc=true) (id,_,_,_,_,_ as vald) =
+  ignore keep_loc;
   reunify_regions ();
   Loc.try2 ?loc:id.pre_loc val_decl env_empty vald
 *)

src/session/session_scheduler.ml

@@ -445,20 +445,22 @@ let fuzzy_proof_time nres ores =
     Done { res' with Call_provers.pr_time = told }
   | _, _ -> nres
 
+let dummy_limits = (0,0,0)
+
 (** run_external_proof_v3 doesn't modify existing proof attempt, it can just
     create new one by find_prover *)
 let run_external_proof_v3 eS eT a callback =
   match find_prover eS a with
   | None ->
-    callback a a.proof_prover 0 None Starting;
+    callback a a.proof_prover dummy_limits None Starting;
     (* nothing to do *)
-    callback a a.proof_prover 0 None MissingProver
+    callback a a.proof_prover dummy_limits None MissingProver
   | Some(ap,npc,a) ->
-    callback a ap 0 None Starting;
+    callback a ap dummy_limits None Starting;
     if a.proof_edited_as = None &&
        npc.prover_config.Whyconf.interactive
     then begin
-      callback a ap 0 None (MissingFile "unedited")
+      callback a ap dummy_limits None (MissingFile "unedited")
     end else begin
       let previous_result = a.proof_state in
       let timelimit, memlimit = adapt_limits a in
@@ -474,7 +476,7 @@ let run_external_proof_v3 eS eT a callback =
       let command = Whyconf.get_complete_command npc.prover_config stepslimit in
       let cb result =
         let result = fuzzy_proof_time result previous_result in
-        callback a ap timelimit
+        callback a ap (timelimit,memlimit,stepslimit)
           (match previous_result with Done res -> Some res | _ -> None)
           (StatusChange result) in
       try
@@ -492,13 +494,13 @@ let run_external_proof_v3 eS eT a callback =
           eT
           (goal_task_or_recover eS a.proof_parent)
       with NoFile f ->
-        callback a ap 0 None (MissingFile f)
+        callback a ap dummy_limits None (MissingFile f)
     end
 
 (** run_external_proof_v2 modify the session according to the current state *)
 let run_external_proof_v2 eS eT a callback =
   let previous_res = ref (a.proof_state,a.proof_obsolete) in
-  let callback a ap timelimit previous state =
+  let callback a ap limits previous state =
     begin match state with
     | Starting -> previous_res := (a.proof_state,a.proof_obsolete)
     | MissingFile _ ->
@@ -516,7 +518,7 @@ let run_external_proof_v2 eS eT a callback =
       end
     | _ -> ()
     end;
-    callback a ap timelimit previous state
+    callback a ap limits previous state
   in
   run_external_proof_v3 eS eT a callback
 
@@ -681,29 +683,29 @@ type report =
   | Edited_file_absent of string
   | No_former_result of Call_provers.prover_result
 
-let push_report report (g,p,t,r) =
-  (g.goal_name,p,t,r)::report
+let push_report report (g,p,limits,r) =
+  (g.goal_name,p,limits,r)::report
 
 let check_external_proof eS eT todo a =
-  let callback a ap tl old s =
+  let callback a ap limits old s =
     let g = a.proof_parent in
     match s with
     | Starting ->
       Todo.start todo
     | MissingFile f ->
-      Todo._done todo (g, ap, tl, Edited_file_absent f)
+      Todo._done todo (g, ap, limits, Edited_file_absent f)
     | MissingProver ->
-      Todo._done todo (g, ap, tl, Prover_not_installed)
+      Todo._done todo (g, ap, limits, Prover_not_installed)
     | StatusChange (Scheduled | Running) -> ()
     | StatusChange (Interrupted | Unedited | JustEdited) -> assert false
     | StatusChange (InternalFailure e) ->
-      Todo._done todo (g, ap, tl, CallFailed e)
+      Todo._done todo (g, ap, limits, CallFailed e)
     | StatusChange (Done res) ->
       let r =
         match old with
         | None -> No_former_result res
         | Some old -> Result (res, old) in
-      Todo._done todo (g, ap, tl, r) in
+      Todo._done todo (g, ap, limits, r) in
   run_external_proof_v2 eS eT a callback
 
 let rec goal_iter_proof_attempt_with_release ~release f g =

src/session/session_scheduler.mli

@@ -159,10 +159,10 @@ module Make(O: OBSERVER) : sig
   val run_external_proof_v3 :
     O.key Session.env_session -> t -> O.key Session.proof_attempt ->
     (O.key Session.proof_attempt -> Whyconf.prover ->
-     int -> Call_provers.prover_result option -> run_external_status -> unit) ->
+     int * int * int -> Call_provers.prover_result option -> run_external_status -> unit) ->
     unit
   (** [run_external_proof_v3 env_session sched pa callback] the
-      callback is applied with [callback pa p timelimit old_result
+      callback is applied with [callback pa p limits old_result
       status]. run_external_proof_v3 don't change the existing proof
       attempt just can add new by O.uninstalled_prover. Be aware since
       the session is not modified there is no test to see if the
@@ -255,24 +255,24 @@ module Make(O: OBSERVER) : sig
     O.key env_session -> t ->
     obsolete_only:bool ->
     context_unproved_goals_only:bool -> O.key any -> unit
-    (** [replay es sched ~obsolete_only ~context_unproved_goals_only a]
-        reruns proofs under [a]
-        if [obsolete_only] is set then does not rerun non-obsolete proofs
-        if [context_unproved_goals_only] is set then don't rerun proofs
-        already 'valid' (FIXME: its the opposite, no?)
-    *)
+  (** [replay es sched ~obsolete_only ~context_unproved_goals_only
+        a] reruns proofs under [a] if [obsolete_only] is set then does
+        not rerun non-obsolete proofs if [context_unproved_goals_only]
+        is set then only rerun proofs whose previous answer was
+        'valid' *)
 
   val check_all:
     ?release:bool -> (** Can all the goals be released at the end? def: false *)
     ?filter:(O.key proof_attempt -> bool) ->
     O.key env_session -> t ->
-    callback:((Ident.ident * Whyconf.prover * int * report) list -> unit) ->
+    callback:((Ident.ident * Whyconf.prover * (int * int * int) * report) list -> unit) ->
     unit
-    (** [check_all session callback] reruns all the proofs of the
+  (** [check_all session callback] reruns all the proofs of the
         session, and reports for all proofs the current result and the
-        new one (does not change the session state) When finished,
-        calls the callback with the reports which are 4-uples (goal
-        name, prover, timelimit, report) *)
+        new one (does not change the session state). When finished,
+        calls the callback with the reports which are 4-uples [(goal
+        name, prover, limits, report)] where [limits] is a triple
+        [(timelimit, memlimit, stepslimit)] *)
 
   val play_all :
     O.key env_session -> t -> callback:(unit-> unit) ->

src/tools/why3replay.ml

@@ -242,14 +242,14 @@ let print_statistics files =
   List.iter print_file (List.rev files)
 
 
-let print_report (g,p,t,r) =
+let print_report (g,p,(t,m,s),r) =
   printf "   goal '%s', prover '%a': " g.Ident.id_string Whyconf.print_prover p;
   match r with
   | M.Result(new_res,old_res) ->
     (* begin match !opt_smoke with *)
     (*   | Session.SD_None -> *)
-        printf "%a instead of %a (timelimit=%d)@."
-          print_result new_res print_result old_res t
+        printf "%a instead of %a (timelimit=%d, memlimit=%d, stepslimit=%d)@."
+          print_result new_res print_result old_res t m s
     (*   | _ -> *)
     (*     printf "Smoke detected!!!@." *)
     (* end *)