drivers/call_prover : a regexp can be given to extract

from the prover output the time used by the prover.

An intermediate format "h:m:s" is used to accept more output
than only seconds.

drivers/alt_ergo.drv

@@ -9,6 +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"
 
 (* À discuter *)
 transformation "simplify_recursive_definition"

drivers/tptp.drv

@@ -10,6 +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"
+
 
 (* to be improved *)
 

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 --print-statistics -xAuto -tAuto --cpu-limit=%t --tstp-in %f 2>&1"
+command = "why3-cpulimit 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 -DocProof -TimeLimit=%t %f 2>&1"
+command = "why3-cpulimit 0 %m %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f 2>&1"
 driver = "drivers/tptp.drv"
 
 [ATP verit]

src/driver/call_provers.ml

@@ -59,6 +59,16 @@ 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"
 
@@ -84,7 +94,7 @@ type post_prover_call = unit -> prover_result
 type bare_prover_call = unit -> post_prover_call
 
 let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
-                   ~regexps ~exitcodes ~filename buffer =
+                   ~regexps ~regexpstime ~exitcodes ~filename buffer =
   let on_stdin = ref true in
   let on_timelimit = ref false in
   let cmd_regexp = Str.regexp "%\\(.\\)" in
@@ -120,9 +130,10 @@ let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
             Debug.dprintf debug "Call_provers: exited with status %d@." n;
             (try List.assoc n exitcodes with Not_found -> grep out regexps)
       in
+      let time = Util.default_option time (grep_time out regexpstime) in
       let ans = match ans with
         | HighFailure when !on_timelimit && timelimit > 0
-          && time >= (0.9 *. float timelimit) -> Timeout
+          && time >= (float timelimit -. 0.1) -> Timeout
         | _ -> ans
       in
       { pr_answer = ans;

src/driver/call_provers.mli

@@ -66,12 +66,13 @@ type bare_prover_call = unit -> post_prover_call
 (** Thread-safe closure that executes a prover on a task. *)
 
 val call_on_buffer :
-  command    : string ->
-  ?timelimit : int ->
-  ?memlimit  : int ->
-  regexps    : (Str.regexp * prover_answer) list ->
-  exitcodes  : (int * prover_answer) list ->
-  filename   : string ->
+  command     : string ->
+  ?timelimit  : int ->
+  ?memlimit   : int ->
+  regexps     : (Str.regexp * prover_answer) list ->
+  regexpstime : (Str.regexp * string) list ->
+  exitcodes   : (int * prover_answer) list ->
+  filename    : string ->
   Buffer.t -> bare_prover_call
 (** Call a prover on the task printed in the {!type: Buffer.t} given.
 
@@ -83,6 +84,11 @@ val call_on_buffer :
     the first field are substituted in the second field (\0,\1,...).
     The regexps are tested in the order of the list.
 
+    @param regexpstime : if the first field matches the prover output,
+    the second field is the time in the format "%f:%f:%f" (h:m:s)
+    after substitution of matching groups. Otherwise wallclock is
+    used. The regexps are tested in the order of the list.
+
     @param exitcodes : if the first field is the exit code, then
     the second field is the answer. Exit codes are tested in the order
     of the list and before the regexps.

src/driver/driver.ml

@@ -33,16 +33,17 @@ open Call_provers
 (** drivers *)
 
 type driver = {
-  drv_env       : Env.env;
-  drv_printer   : string option;
-  drv_filename  : string option;
-  drv_transform : string list;
-  drv_prelude   : prelude;
-  drv_thprelude : prelude_map;
-  drv_meta      : (theory * Stdecl.t) Mid.t;
-  drv_meta_cl   : (theory * Stdecl.t) Mid.t;
-  drv_regexps   : (Str.regexp * prover_answer) list;
-  drv_exitcodes : (int * prover_answer) list;
+  drv_env         : Env.env;
+  drv_printer     : string option;
+  drv_filename    : string option;
+  drv_transform   : string list;
+  drv_prelude     : prelude;
+  drv_thprelude   : prelude_map;
+  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_exitcodes   : (int * prover_answer) list;
 }
 
 (** parse a driver file *)
@@ -71,6 +72,7 @@ exception UnknownProp  of (string list * string list)
 let load_driver = let driver_tag = ref (-1) in fun env file ->
   let prelude   = ref [] in
   let regexps   = ref [] in
+  let regexpstime   = ref [] in
   let exitcodes = ref [] in
   let filename  = ref None in
   let printer   = ref None in
@@ -88,6 +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)
     | ExitCodeValid s -> add_to_list exitcodes (s, Valid)
     | ExitCodeInvalid s -> add_to_list exitcodes (s, Invalid)
     | ExitCodeTimeout s -> add_to_list exitcodes (s, Timeout)
@@ -159,16 +162,17 @@ let load_driver = let driver_tag = ref (-1) in fun env file ->
   transform := List.rev !transform;
   incr driver_tag;
   {
-    drv_env       = env;
-    drv_printer   = !printer;
-    drv_prelude   = !prelude;
-    drv_filename  = !filename;
-    drv_transform = !transform;
-    drv_thprelude = !thprelude;
-    drv_meta      = !meta;
-    drv_meta_cl   = !meta_cl;
-    drv_regexps   = List.rev !regexps;
-    drv_exitcodes = List.rev !exitcodes;
+    drv_env         = env;
+    drv_printer     = !printer;
+    drv_prelude     = !prelude;
+    drv_filename    = !filename;
+    drv_transform   = !transform;
+    drv_thprelude   = !thprelude;
+    drv_meta        = !meta;
+    drv_meta_cl     = !meta_cl;
+    drv_regexps     = List.rev !regexps;
+    drv_regexpstime = List.rev !regexpstime;
+    drv_exitcodes   = List.rev !exitcodes;
   }
 
 (** apply drivers *)
@@ -196,10 +200,12 @@ let file_of_task drv input_file theory_name task =
 
 let call_on_buffer ~command ?timelimit ?memlimit drv buffer =
   let regexps = drv.drv_regexps in
+  let regexpstime = drv.drv_regexpstime in
   let exitcodes = drv.drv_exitcodes in
   let filename = get_filename drv "" "" "" in
   Call_provers.call_on_buffer
-    ~command ?timelimit ?memlimit ~regexps ~exitcodes ~filename buffer
+    ~command ?timelimit ?memlimit ~regexps ~regexpstime
+    ~exitcodes ~filename buffer
 
 (** print'n'prove *)
 

src/driver/driver_ast.ml

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

src/driver/driver_lexer.mll

@@ -44,6 +44,7 @@
 	"valid", VALID;
 	"invalid", INVALID;
         "timeout", TIMEOUT;
+        "time",    TIME;
 	"unknown", UNKNOWN;
 	"fail", FAIL;
         "logic", LOGIC;

src/driver/driver_parser.mly

@@ -31,7 +31,7 @@
 %token <string> STRING
 %token <string> OPERATOR
 %token THEORY END SYNTAX REMOVE META PRELUDE PRINTER
-%token VALID INVALID TIMEOUT UNKNOWN FAIL
+%token VALID INVALID TIMEOUT UNKNOWN FAIL TIME
 %token UNDERSCORE LEFTPAR RIGHTPAR CLONED DOT EOF
 %token LOGIC TYPE PROP FILENAME TRANSFORM PLUGIN
 %token LEFTPAR_STAR_RIGHTPAR COMMA
@@ -57,6 +57,7 @@ global:
 | VALID STRING { RegexpValid $2 }
 | INVALID STRING { RegexpInvalid $2 }
 | TIMEOUT STRING { RegexpTimeout $2 }
+| TIME STRING STRING  { RegexpTime ($2,$3) }
 | UNKNOWN STRING STRING { RegexpUnknown ($2, $3) }
 | FAIL STRING STRING { RegexpFailure ($2, $3) }
 | VALID INTEGER { ExitCodeValid $2 }