(contributed by David Hauzar) Parsing of steps

It is now done by a different mechanism than parsing of time:
timeregexp is not any more used for parsing of steps, stepsregexp is
used instead.

drivers/alt_ergo_bare.drv

@@ -13,8 +13,10 @@ timeout "Steps limit reached"
 outofmemory "Fatal error: out of memory"
 outofmemory "Fatal error: exception Stack_overflow"
 fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
-time "Valid (%s) (%S)"
-time "Valid (%s) (%S steps)"
+time "Valid (%s)"
+time "Valid (%s)"
+steps "Valid (\\([0-9]+.?[0-9]*\\)) (\\([0-9]+.?[0-9]*\\))" 2
+steps "Valid (\\([0-9]+.?[0-9]*\\)) (\\([0-9]+.?[0-9]*\\) steps)" 2
 time "why3cpulimit time : %s s"
 
 (* À discuter *)

drivers/cvc4_bare.drv

@@ -8,13 +8,9 @@ prelude "(set-logic AUFBVNIRA)"
 
 import "smt-libv2.drv"
 
-(* regexp for steps should match things like
+(* regexp for steps *)
+steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
 
-smt::SmtEngine::resourceUnitsUsed, 1041
-
-but not in the same line as the "valid" answer
-
-*)
 
 (* CVC4 division seems to be neither the Euclidean one, nor the Computer one *)
 (*

share/provers-detection-data.conf

@@ -86,19 +86,32 @@ version_old = "0.8"
 command = "%l/why3-cpulimit %t %m -s %e %f"
 driver = "drivers/alt_ergo_0.92.drv"
 
-# CVC4 version 1.4 and 1.5-prerelease
+# CVC4 version 1.5-prerelease
 [ATP cvc4]
 name = "CVC4"
 exec = "cvc4"
 exec = "cvc4-1.5-prerelease"
-exec = "cvc4-1.4"
 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 --rlimit=%S --lang=smt2 %f"
+
+# CVC4 version 1.4
+[ATP cvc4]
+name = "CVC4"
+exec = "cvc4"
+exec = "cvc4-1.4"
+version_switch = "--version"
+version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
 version_ok  = "1.4"
 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 
+# 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"
 
 # CVC4 version 1.0 to 1.3

src/driver/call_provers.ml

@@ -11,19 +11,27 @@
 
 open Format
 
+let debug = Debug.register_info_flag "call_prover"
+  ~desc:"Print@ debugging@ messages@ about@ prover@ calls@ \
+         and@ keep@ temporary@ files."
+
 (** time regexp "%h:%m:%s" *)
 type timeunit =
   | Hour
   | Min
   | Sec
   | Msec
-  | Step
 
 type timeregexp = {
   re    : Str.regexp;
   group : timeunit array; (* i-th corresponds to the group i+1 *)
 }
 
+type stepsregexp = {
+  steps_re        : Str.regexp;
+  steps_group_num : int; (* the number of matched group which corresponds to the number of steps *)
+}
+
 let timeregexp s =
   let cmd_regexp = Str.regexp "%\\(.\\)" in
   let nb = ref 0 in
@@ -35,7 +43,6 @@ let timeregexp s =
     | "m" -> add_unit Min
     | "s" -> add_unit Sec
     | "i" -> add_unit Msec
-    | "S" -> add_unit Step
     | _ -> failwith "unknown format specifier, use %%h, %%m, %%s, %%i, %%S"
   in
   let s = Str.global_substitute cmd_regexp replace s in
@@ -49,17 +56,29 @@ let rec grep_time out = function
     begin try
             ignore (Str.search_forward re.re out 0);
             let t = ref 0. in
-	    let s = ref (-1) in
             Array.iteri (fun i u ->
               let v = Str.matched_group (succ i) out in
               match u with
                 | Hour -> t := !t +. float_of_string v *. 3600.
                 | Min  -> t := !t +. float_of_string v *. 60.
                 | Sec  -> t := !t +. float_of_string v
-                | Msec -> t := !t +. float_of_string v /. 1000.
-		| Step -> s := int_of_string v ) re.group;
-            Some( !t, !s )
-      with _ -> grep_time out l end
+                | Msec -> t := !t +. float_of_string v /. 1000. ) re.group;
+            Some( !t )
+      with _ -> grep_time out l
+    end
+
+let stepsregexp s_re s_group_num =
+  {steps_re = (Str.regexp s_re); steps_group_num = s_group_num}
+
+let rec grep_steps out = function
+  | [] -> None
+  | re :: l ->
+    begin try
+	    ignore (Str.search_forward re.steps_re out 0);
+	    let v = Str.matched_group (re.steps_group_num) out in
+	    Some(int_of_string v)
+      with _ -> grep_steps out l
+    end
 
 (** *)
 
@@ -83,6 +102,7 @@ type prover_result = {
 type prover_result_parser = {
   prp_regexps     : (Str.regexp * prover_answer) list;
   prp_timeregexps : timeregexp list;
+  prp_stepsregexp : stepsregexp list;
   prp_exitcodes   : (int * prover_answer) list;
 }
 
@@ -122,11 +142,6 @@ let rec grep out l = match l with
         | HighFailure -> assert false
       with Not_found -> grep out l end
 
-
-let debug = Debug.register_info_flag "call_prover"
-  ~desc:"Print@ debugging@ messages@ about@ prover@ calls@ \
-         and@ keep@ temporary@ files."
-
 type post_prover_call = unit -> prover_result
 
 type prover_call = {
@@ -152,8 +167,8 @@ let parse_prover_run res_parser time out ret on_timelimit timelimit =
          with Not_found -> grep out res_parser.prp_regexps)
   in
   Debug.dprintf debug "Call_provers: prover output:@\n%s@." out;
-  let time,steps = Opt.get_def (time,-1) (grep_time out res_parser.prp_timeregexps) in
-  (* TODO: separate grep for time and for steps into different regexps *)
+  let time = Opt.get_def (time) (grep_time out res_parser.prp_timeregexps) in
+  let steps = Opt.get_def (-1) (grep_steps out res_parser.prp_stepsregexp) in
   let ans = match ans with
     | Unknown _ | HighFailure when on_timelimit && timelimit > 0
       && time >= (0.9 *. float timelimit) -> Timeout

src/driver/call_provers.mli

@@ -57,13 +57,21 @@ val debug : Debug.flag
 type timeregexp
 (** The type of precompiled regular expressions for time parsing *)
 
+type stepsregexp
+(** The type of precompiled regular expressions for parsing of steps *)
+
 val timeregexp : string -> timeregexp
 (** Converts a regular expression with special markers '%h','%m',
     '%s','%i' (for milliseconds) into a value of type [timeregexp] *)
 
+val stepsregexp : string -> int -> stepsregexp
+(** stepsregexp s n creates a regular expression for matching number of steps.
+s is regular expression, n is a group number with steps information *)
+
 type prover_result_parser = {
   prp_regexps     : (Str.regexp * prover_answer) list;
   prp_timeregexps : timeregexp list;
+  prp_stepsregexp : stepsregexp list;
   prp_exitcodes   : (int * prover_answer) list;
 }
 

src/driver/driver.ml

@@ -75,6 +75,7 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
   let printer   = ref None in
   let transform = ref [] in
   let timeregexps = ref [] in
+  let stepsregexps = ref [] in
   let blacklist = Queue.create () in
 
   let set_or_raise loc r v error = match !r with
@@ -91,6 +92,7 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
     | RegexpUnknown (s,t) -> add_to_list regexps (Str.regexp s, Unknown t)
     | RegexpFailure (s,t) -> add_to_list regexps (Str.regexp s, Failure t)
     | TimeRegexp r -> add_to_list timeregexps (Call_provers.timeregexp r)
+    | StepRegexp (r,ns) -> add_to_list stepsregexps (Call_provers.stepsregexp r ns)
     | ExitCodeValid s -> add_to_list exitcodes (s, Valid)
     | ExitCodeInvalid s -> add_to_list exitcodes (s, Invalid)
     | ExitCodeTimeout s -> add_to_list exitcodes (s, Timeout)
@@ -197,6 +199,7 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
       {
       prp_regexps     = List.rev !regexps;
       prp_timeregexps = List.rev !timeregexps;
+      prp_stepsregexp = List.rev !stepsregexps;
       prp_exitcodes   = List.rev !exitcodes;
     };
     drv_tag         = !driver_tag;

src/driver/driver_ast.ml

@@ -60,6 +60,7 @@ type global =
   | RegexpUnknown of string * string
   | RegexpFailure of string * string
   | TimeRegexp of string
+  | StepRegexp of string * int
   | ExitCodeValid of int
   | ExitCodeInvalid of int
   | ExitCodeTimeout of int

src/driver/driver_lexer.mll

@@ -31,6 +31,7 @@
         "meta", META;
         "prelude", PRELUDE;
         "printer", PRINTER;
+	"steps", STEPS;
         "valid", VALID;
         "invalid", INVALID;
         "timeout", TIMEOUT;

src/driver/driver_parser.mly

@@ -23,7 +23,7 @@
 %token <string> OPERATOR
 %token <string> INPUT (* never reaches the parser *)
 %token THEORY END SYNTAX REMOVE META PRELUDE PRINTER
-%token VALID INVALID TIMEOUT OUTOFMEMORY UNKNOWN FAIL TIME
+%token VALID INVALID TIMEOUT OUTOFMEMORY UNKNOWN FAIL TIME STEPS
 %token UNDERSCORE LEFTPAR RIGHTPAR DOT QUOTE EOF
 %token BLACKLIST
 %token MODULE EXCEPTION VAL CONVERTER
@@ -56,6 +56,7 @@ global:
 | TIMEOUT STRING { RegexpTimeout $2 }
 | OUTOFMEMORY STRING { RegexpOutOfMemory $2 }
 | TIME STRING  { TimeRegexp $2 }
+| STEPS STRING INTEGER { StepRegexp ($2, $3) }
 | UNKNOWN STRING STRING { RegexpUnknown ($2, $3) }
 | FAIL STRING STRING { RegexpFailure ($2, $3) }
 | VALID INTEGER { ExitCodeValid $2 }
@@ -106,20 +107,21 @@ qualid_:
 | ident DOT qualid_  { ($1 :: $3) }
 
 ident:
-| IDENT     { $1 }
-| SYNTAX    { "syntax" }
-| REMOVE    { "remove" }
-| PRELUDE   { "prelude" }
-| BLACKLIST { "blacklist" }
-| PRINTER   { "printer" }
-| VALID     { "valid" }
-| INVALID   { "invalid" }
-| TIMEOUT   { "timeout" }
-| UNKNOWN   { "unknown" }
-| FAIL      { "fail" }
-| FILENAME  { "filename" }
-| TRANSFORM { "transformation" }
-| PLUGIN    { "plugin" }
+| IDENT        { $1 }
+| SYNTAX       { "syntax" }
+| REMOVE       { "remove" }
+| PRELUDE      { "prelude" }
+| BLACKLIST    { "blacklist" }
+| PRINTER      { "printer" }
+| STEPS        { "steps" }
+| VALID        { "valid" }
+| INVALID      { "invalid" }
+| TIMEOUT      { "timeout" }
+| UNKNOWN      { "unknown" }
+| FAIL         { "fail" }
+| FILENAME     { "filename" }
+| TRANSFORM    { "transformation" }
+| PLUGIN       { "plugin" }
 
 ident_rich:
 | ident                     { $1 }

src/session/session_scheduler.ml

@@ -292,7 +292,8 @@ let schedule_edition t command filename callback =
   let res_parser =
     { Call_provers.prp_exitcodes = [(0,Call_provers.Unknown "")];
       Call_provers.prp_regexps = [];
-      Call_provers.prp_timeregexps = []
+      Call_provers.prp_timeregexps = [];
+      Call_provers.prp_stepsregexp = [];
     } in
   let precall =
     Call_provers.call_on_file ~command ~res_parser ~redirect:false filename in