Call_prover, time : simpler format to parse time :

"%h:%m:%s:%i" (i for mIlliseconds)

Spass does'nt give cputime but wallclock.
eprover doesn't always give time. so use cpulimit_time for them.

add %b for the memlimit in bytes

drivers/alt_ergo.drv

@@ -9,7 +9,7 @@ valid "Valid"
 invalid "Invalid"
 unknown "I don't know" "Unknown"
 fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
-time "Valid (\\(.*\\))" "0:0:\\1"
+time "Valid (%s)"
 
 (* À discuter *)
 transformation "simplify_recursive_definition"

drivers/cvc3.drv

@@ -7,7 +7,7 @@ filename "%f-%t-%g.smt"
 
 valid "unsat"
 unknown "\\bunknown\\b\\|\\bsat\\b" "Unknown"
-time "cpulimit_time : \\([0-9]+.[0-9]*\\) s" "0:0:\\1"
+time "cpulimit_time : %s s"
 
 (* À discuter *)
 transformation "simplify_recursive_definition"

drivers/simplify.drv

@@ -7,7 +7,7 @@ filename "%f-%t-%g.sx"
 
 valid "\\bValid\\b"
 unknown "\\bInvalid\\b" "Unknown"
-time "cpulimit_time : \\([0-9]+.[0-9]*\\) s" "0:0:\\1"
+time "cpulimit_time : %s s"
 
 transformation "simplify_recursive_definition"
 transformation "inline_trivial"

drivers/tptp.drv

@@ -10,8 +10,9 @@ timeout "Resource limit exceeded"
 timeout "CPU time limit exceeded"
 unknown "No Proof Found"            "Unknown"
 fail    "Failure.*"                   "\"\\0\""
-time    "\\([0-9]+:[0-9]+:[0-9]+.[0-9]*\\) on the problem" "\\1"
-time    "Total time[ ]*: \\([0-9]+.[0-9]*\\) s" "0:0:\\1"
+time "cpulimit_time : %s s"
+(* time    "%h:%m:%s on the problem" *)
+(* time    "Total time[ ]*: %s s" *)
 
 
 (* to be improved *)

drivers/z3.drv

@@ -7,7 +7,8 @@ filename "%f-%t-%g.smt"
 
 valid "^unsat"
 unknown "^\\(unknown\\|sat\\|Fail\\)" "Unknown"
-time "cpulimit_time : \\([0-9]+.[0-9]*\\) s" "0:0:\\1"
+time "cpulimit_time : %s s"
+
 
 (* À discuter *)
 transformation "simplify_recursive_definition"

share/provers-detection-data.conf

@@ -40,7 +40,7 @@ name = "Eprover"
 exec = "eprover"
 version_switch = "--version"
 version_regexp = "E \\([^\n]+\\)"
-command = "why3-cpulimit 0 %m %e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f 2>&1"
+command = "why3-cpulimit_time 0 %m %e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f 2>&1"
 driver = "drivers/tptp.drv"
 
 [ATP gappa]
@@ -75,7 +75,7 @@ name = "Spass"
 exec = "SPASS"
 version_switch = "-TPTP || true"
 version_regexp = "SPASS V \\([^ \n\t]+\\)"
-command = "why3-cpulimit 0 %m %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f 2>&1"
+command = "why3-cpulimit_time 0 %m %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f 2>&1"
 driver = "drivers/tptp.drv"
 
 [ATP verit]

src/driver/call_provers.ml

@@ -20,6 +20,54 @@
 open Format
 open Sysutil
 
+(** time regexp "%h:%m:%s" *)
+type timeunit =
+  | Hour
+  | Min
+  | Sec
+  | Msec
+
+type regexptime = {
+  re : Str.regexp;
+  group : timeunit array; (*ieme corresponds to the group i + 1*)
+}
+
+let regexptime s =
+  let cmd_regexp = Str.regexp "%\\(.\\)" in
+  let nb = ref 0 in
+  let l = ref [] in
+  let add_unit x = l := (!nb,x) :: !l; incr nb; "\\([0-9]+.?[0-9]*\\)" in
+  let replace s = match Str.matched_group 1 s with
+    | "%" -> "%"
+    | "h" -> add_unit Hour
+    | "m" -> add_unit Min
+    | "s" -> add_unit Sec
+    | "i" -> add_unit Msec
+    | _ -> failwith "unknown format specifier, use %%h, %%m, %%s, %%i"
+  in
+  let s = Str.global_substitute cmd_regexp replace s in
+  let group = Array.make !nb Hour in
+  List.iter (fun (i,u) -> group.(i) <- u) !l;
+  { re = Str.regexp s; group = group}
+
+let rec grep_time out = function
+  | [] -> None
+  | re :: l ->
+    begin try
+            ignore (Str.search_forward re.re out 0);
+            let t = ref 0. in
+            Array.iteri (fun i u ->
+              let v = float_of_string (Str.matched_group (succ i) out) in
+              match u with
+                | Hour -> t := !t +. v *. 3600.
+                | Min  -> t := !t +. v *. 60.
+                | Sec  -> t := !t +. v
+                | Msec -> t := !t +. v /. 1000.) re.group;
+            Some !t
+      with _ -> grep_time out l end
+
+(** *)
+
 type prover_answer =
   | Valid
   | Invalid
@@ -59,16 +107,6 @@ let rec grep out l = match l with
         | HighFailure -> assert false
       with Not_found -> grep out l end
 
-let rec grep_time out = function
-  | [] -> None
-  | (re,pa) :: l ->
-    begin try
-            ignore (Str.search_forward re out 0);
-            let stime = (Str.replace_matched pa out) in
-            Some (Scanf.sscanf stime "%f:%f:%f"
-                    (fun h m s -> h *. 3600. +. m *. 60. +. s))
-      with _ -> grep_time out l end
-
 
 let debug = Debug.register_flag "call_prover"
 
@@ -103,7 +141,8 @@ let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
     | "f" -> on_stdin := false; file
     | "t" -> on_timelimit := true; string_of_int timelimit
     | "m" -> string_of_int memlimit
-    | _ -> failwith "unknown format specifier, use %%f, %%t or %%m"
+    | "b" -> string_of_int (memlimit * 1024)
+    | _ -> failwith "unknown format specifier, use %%f, %%t, %%m or %%b"
   in
   let cmd = Str.global_substitute cmd_regexp (replace "") command in
   let on_stdin = !on_stdin in
@@ -133,7 +172,7 @@ let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
       let time = Util.default_option time (grep_time out regexpstime) in
       let ans = match ans with
         | HighFailure when !on_timelimit && timelimit > 0
-          && time >= (float timelimit -. 0.1) -> Timeout
+          && time >= (0.9 *. float timelimit) -> Timeout
         | _ -> ans
       in
       { pr_answer = ans;

src/driver/call_provers.mli

@@ -56,6 +56,11 @@ val debug : Debug.flag
     If set [call_on_buffer] prints on stderr the commandline called
     and the output of the prover. *)
 
+(** time parser *)
+type regexptime
+val regexptime : string -> regexptime
+(** *)
+
 type post_prover_call = unit -> prover_result
 (** Thread-unsafe closure that processes a prover's output
     and returns the final result. Once again: this closure
@@ -70,7 +75,7 @@ val call_on_buffer :
   ?timelimit  : int ->
   ?memlimit   : int ->
   regexps     : (Str.regexp * prover_answer) list ->
-  regexpstime : (Str.regexp * string) list ->
+  regexpstime : regexptime list ->
   exitcodes   : (int * prover_answer) list ->
   filename    : string ->
   Buffer.t -> bare_prover_call

src/driver/driver.ml

@@ -42,7 +42,7 @@ type driver = {
   drv_meta        : (theory * Stdecl.t) Mid.t;
   drv_meta_cl     : (theory * Stdecl.t) Mid.t;
   drv_regexps     : (Str.regexp * prover_answer) list;
-  drv_regexpstime : (Str.regexp * string) list;
+  drv_regexpstime : Call_provers.regexptime list;
   drv_exitcodes   : (int * prover_answer) list;
 }
 
@@ -90,7 +90,7 @@ let load_driver = let driver_tag = ref (-1) in fun env file ->
     | RegexpTimeout s -> add_to_list regexps (Str.regexp s, Timeout)
     | RegexpUnknown (s,t) -> add_to_list regexps (Str.regexp s, Unknown t)
     | RegexpFailure (s,t) -> add_to_list regexps (Str.regexp s, Failure t)
-    | RegexpTime (r,s) -> add_to_list regexpstime (Str.regexp r,s)
+    | RegexpTime r -> add_to_list regexpstime (Call_provers.regexptime r)
     | ExitCodeValid s -> add_to_list exitcodes (s, Valid)
     | ExitCodeInvalid s -> add_to_list exitcodes (s, Invalid)
     | ExitCodeTimeout s -> add_to_list exitcodes (s, Timeout)

src/driver/driver_ast.ml

@@ -50,7 +50,7 @@ type global =
   | RegexpTimeout of string
   | RegexpUnknown of string * string
   | RegexpFailure of string * string
-  | RegexpTime of string * string
+  | RegexpTime of string
   | ExitCodeValid of int
   | ExitCodeInvalid of int
   | ExitCodeTimeout of int

src/driver/driver_parser.mly

@@ -57,7 +57,7 @@ global:
 | VALID STRING { RegexpValid $2 }
 | INVALID STRING { RegexpInvalid $2 }
 | TIMEOUT STRING { RegexpTimeout $2 }
-| TIME STRING STRING  { RegexpTime ($2,$3) }
+| TIME STRING  { RegexpTime ($2) }
 | UNKNOWN STRING STRING { RegexpUnknown ($2, $3) }
 | FAIL STRING STRING { RegexpFailure ($2, $3) }
 | VALID INTEGER { ExitCodeValid $2 }