explicit prover result "steps limit exceeded"

+ fixed wrong step limit in one session

drivers/alt_ergo_common.drv

@@ -9,7 +9,7 @@ valid "Valid"
 invalid "Invalid"
 unknown "I don't know" ""
 timeout "Timeout"
-timeout "Steps limit reached"
+stepslimitexceeded "Steps limit reached"
 outofmemory "Fatal error: out of memory"
 outofmemory "Fatal error: exception Stack_overflow"
 fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"

drivers/cvc4.drv

@@ -27,7 +27,6 @@ transformation "encoding_smt"
 
 outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
 timeout "interrupted by timeout"
-steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
 
 
 (** Extra theories supported by CVC4 *)

drivers/cvc4_14.drv

@@ -35,14 +35,9 @@ transformation "encoding_smt_if_poly"
 
 outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
 timeout "interrupted by timeout"
+steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
+stepslimitexceeded "??"
 
-(* regexp for steps should match things like
-
-smt::SmtEngine::resourceUnitsUsed, 1041
-
-but not in the same line as the "valid" answer
-
-*)
 
 (** Extra theories supported by CVC4 *)
 

drivers/smt-libv2.drv

@@ -18,9 +18,9 @@ prelude "(set-logic AUFNIRA)"
 
 printer "smtv2"
 filename "%f-%t-%g.smt2"
-unknown "^\\(unknown\\|sat\\|Fail\\)" ""
+unknown "^\\(unknown\\|sat\\|Fail\\)$" ""
 time "why3cpulimit time : %s s"
-valid "^unsat"
+valid "^unsat$"
 
 
 theory BuiltIn

examples/vacid_0_red_black_trees/why3session.xml

@@ -135,8 +135,8 @@
  <goal name="almost_rbtree_rbtree_black">
  <proof prover="7" timelimit="10" memlimit="0"><result status="valid" time="0.01" steps="14"/></proof>
  </goal>
- <goal name="WP_parameter lbalance" expl="VC for lbalance">
- <transf name="split_goal_wp">
+ <goal name="WP_parameter lbalance" expl="VC for lbalance" expanded="true">
+ <transf name="split_goal_wp" expanded="true">
   <goal name="WP_parameter lbalance.1" expl="1. postcondition">
   <transf name="split_goal_wp">
    <goal name="WP_parameter lbalance.1.1" expl="1.">
@@ -713,8 +713,8 @@
    </goal>
   </transf>
   </goal>
-  <goal name="WP_parameter lbalance.11" expl="11. postcondition">
-  <proof prover="0"><result status="valid" time="0.71" steps="1172"/></proof>
+  <goal name="WP_parameter lbalance.11" expl="11. postcondition" expanded="true">
+  <proof prover="0"><result status="valid" time="1.20" steps="1173"/></proof>
   </goal>
   <goal name="WP_parameter lbalance.12" expl="12. postcondition">
   <proof prover="4"><result status="valid" time="0.04"/></proof>

share/images/icons.rc

@@ -9,12 +9,14 @@ unknown = "help32"
 invalid = "delete32"
 timeout = "clock32"
 outofmemory = "deletefile32"
+stepslimitexceeded = "cut32"
 failure = "bug32"
 valid_obs = "obsaccept32"
 unknown_obs = "obshelp32"
 invalid_obs = "obsdelete32"
 timeout_obs = "obsclock32"
 outofmemory_obs = "obsdeletefile32"
+stepslimitexceeded_obs = "cut32"
 failure_obs = "obsbug32"
 yes = "accept32"
 no = "delete32"
@@ -41,14 +43,16 @@ running = "control_play_blue"
 valid = "accept"
 unknown = "help"
 invalid = "exclamation"
-timeout = "timeline"
-outofmemory = "ddr_memory"
+timeout = "time_delete"
+outofmemory = "database_delete"
+stepslimitexceeded = "brick_delete"
 failure = "bomb"
 valid_obs = "bullet_green"
 unknown_obs = "bullet_blue"
 invalid_obs = "bullet_red"
-timeout_obs = "bullet_white"
-outofmemory_obs = "bullet_white"
+timeout_obs = "time_delete"
+outofmemory_obs = "database_delete"
+stepslimitexceeded_obs = "brick_delete"
 failure_obs = "bullet_black"
 yes = "accept"
 no = "delete"

share/provers-detection-data.conf

@@ -66,8 +66,8 @@ 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
-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"
+command = "%l/why3-cpulimit %T %m -s %e --stats --tlimit-per=%t000 --lang=smt2 %f"
+command_steps = "%l/why3-cpulimit %U %m -s %e --stats --rlimit=%S --lang=smt2 %f"
 
 # CVC4 version 1.0 to 1.3
 [ATP cvc4]

src/coq-tactic/why3tac.ml4

@@ -1289,6 +1289,7 @@ let why3tac ?(timelimit=timelimit) s gl =
       | Call_provers.Failure s -> error ("Failure: " ^ s)
       | Call_provers.Timeout -> error "Timeout"
       | OutOfMemory -> error "Out Of Memory"
+      | StepsLimitExceeded -> error "Steps Limit reached"
       | HighFailure ->
           error ("Prover failure\n" ^ res.pr_output ^ "\n")
   with

src/driver/call_provers.ml

@@ -87,6 +87,7 @@ type prover_answer =
   | Invalid
   | Timeout
   | OutOfMemory
+  | StepsLimitExceeded
   | Unknown of string
   | Failure of string
   | HighFailure
@@ -111,6 +112,7 @@ let print_prover_answer fmt = function
   | Invalid -> fprintf fmt "Invalid"
   | Timeout -> fprintf fmt "Timeout"
   | OutOfMemory -> fprintf fmt "Ouf Of Memory"
+  | StepsLimitExceeded -> fprintf fmt "Steps limit exceeded"
   | Unknown "" -> fprintf fmt "Unknown"
   | Failure "" -> fprintf fmt "Failure"
   | Unknown s -> fprintf fmt "Unknown (%s)" s
@@ -139,7 +141,7 @@ let rec grep out l = match l with
       begin try
         ignore (Str.search_forward re out 0);
         match pa with
-        | Valid | Invalid | Timeout | OutOfMemory -> pa
+        | Valid | Invalid | Timeout | OutOfMemory | StepsLimitExceeded -> pa
         | Unknown s -> Unknown (Str.replace_matched s out)
         | Failure s -> Failure (Str.replace_matched s out)
         | HighFailure -> assert false

src/driver/call_provers.mli

@@ -17,9 +17,11 @@ type prover_answer =
   | Invalid
       (** The task is invalid *)
   | Timeout
-      (** the task timeout, ie it takes more time than specified *)
+      (** the task timeouts, ie it takes more time than specified *)
   | OutOfMemory
-      (** the task timeout, ie it takes more time than specified *)
+      (** the task runs out of memory *)
+  | StepsLimitExceeded
+      (** the task required more steps than the limit provided *)
   | Unknown of string
       (** The prover can't determine if the task is valid *)
   | Failure of string

src/driver/driver.ml

@@ -89,14 +89,19 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
     | RegexpInvalid s -> add_to_list regexps (Str.regexp s, Invalid)
     | RegexpTimeout s -> add_to_list regexps (Str.regexp s, Timeout)
     | RegexpOutOfMemory s -> add_to_list regexps (Str.regexp s, OutOfMemory)
+    | RegexpStepsLimitExceeded s ->
+      add_to_list regexps (Str.regexp s, StepsLimitExceeded)
     | 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)
+    | 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)
     | ExitCodeOutOfMemory s -> add_to_list exitcodes (s, OutOfMemory)
+    | ExitCodeStepsLimitExceeded s ->
+      add_to_list exitcodes (s, StepsLimitExceeded)
     | ExitCodeUnknown (s,t) -> add_to_list exitcodes (s, Unknown t)
     | ExitCodeFailure (s,t) -> add_to_list exitcodes (s, Failure t)
     | Filename s -> set_or_raise loc filename s "filename"

src/driver/driver_ast.ml

@@ -57,6 +57,7 @@ type global =
   | RegexpInvalid of string
   | RegexpTimeout of string
   | RegexpOutOfMemory of string
+  | RegexpStepsLimitExceeded of string
   | RegexpUnknown of string * string
   | RegexpFailure of string * string
   | TimeRegexp of string
@@ -65,6 +66,7 @@ type global =
   | ExitCodeInvalid of int
   | ExitCodeTimeout of int
   | ExitCodeOutOfMemory of int
+  | ExitCodeStepsLimitExceeded of int
   | ExitCodeUnknown of int * string
   | ExitCodeFailure of int * string
   | Filename of string

src/driver/driver_lexer.mll

@@ -36,6 +36,7 @@
         "invalid", INVALID;
         "timeout", TIMEOUT;
         "outofmemory", OUTOFMEMORY;
+        "stepslimitexceeded", STEPSLIMITEXCEEDED;
         "time",    TIME;
         "unknown", UNKNOWN;
         "fail", FAIL;

src/driver/driver_parser.mly

@@ -23,7 +23,8 @@
 %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 STEPS
+%token VALID INVALID UNKNOWN FAIL
+%token TIMEOUT OUTOFMEMORY STEPSLIMITEXCEEDED TIME STEPS
 %token UNDERSCORE LEFTPAR RIGHTPAR DOT QUOTE EOF
 %token BLACKLIST
 %token MODULE EXCEPTION VAL CONVERTER
@@ -55,6 +56,7 @@ global:
 | INVALID STRING { RegexpInvalid $2 }
 | TIMEOUT STRING { RegexpTimeout $2 }
 | OUTOFMEMORY STRING { RegexpOutOfMemory $2 }
+| STEPSLIMITEXCEEDED STRING { RegexpStepsLimitExceeded $2 }
 | TIME STRING  { TimeRegexp $2 }
 | STEPS STRING INTEGER { StepRegexp ($2, $3) }
 | UNKNOWN STRING STRING { RegexpUnknown ($2, $3) }
@@ -62,6 +64,7 @@ global:
 | VALID INTEGER { ExitCodeValid $2 }
 | INVALID INTEGER { ExitCodeInvalid $2 }
 | TIMEOUT INTEGER { ExitCodeTimeout $2 }
+| STEPSLIMITEXCEEDED INTEGER { ExitCodeStepsLimitExceeded $2 }
 | UNKNOWN INTEGER STRING { ExitCodeUnknown ($2, $3) }
 | FAIL INTEGER STRING { ExitCodeFailure ($2, $3) }
 | FILENAME STRING { Filename $2 }

src/ide/gconfig.ml

@@ -265,12 +265,14 @@ let image_unknown = ref !image_default
 let image_invalid = ref !image_default
 let image_timeout = ref !image_default
 let image_outofmemory = ref !image_default
+let image_stepslimitexceeded = ref !image_default
 let image_failure = ref !image_default
 let image_valid_obs = ref !image_default
 let image_unknown_obs = ref !image_default
 let image_invalid_obs = ref !image_default
 let image_timeout_obs = ref !image_default
 let image_outofmemory_obs = ref !image_default
+let image_stepslimitexceeded_obs = ref !image_default
 let image_failure_obs = ref !image_default
 let image_yes = ref !image_default
 let image_no = ref !image_default
@@ -310,12 +312,14 @@ let iconname_unknown = ref ""
 let iconname_invalid = ref ""
 let iconname_timeout = ref ""
 let iconname_outofmemory = ref ""
+let iconname_stepslimitexceeded = ref ""
 let iconname_failure = ref ""
 let iconname_valid_obs = ref ""
 let iconname_unknown_obs = ref ""
 let iconname_invalid_obs = ref ""
 let iconname_timeout_obs = ref ""
 let iconname_outofmemory_obs = ref ""
+let iconname_stepslimitexceeded_obs = ref ""
 let iconname_failure_obs = ref ""
 let iconname_yes = ref ""
 let iconname_no = ref ""
@@ -354,12 +358,14 @@ let load_icon_names () =
   iconname_invalid := get_icon_name "invalid";
   iconname_timeout := get_icon_name "timeout";
   iconname_outofmemory := get_icon_name "outofmemory";
+  iconname_stepslimitexceeded := get_icon_name "stepslimitexceeded";
   iconname_failure := get_icon_name "failure";
   iconname_valid_obs := get_icon_name "valid_obs";
   iconname_unknown_obs := get_icon_name "unknown_obs";
   iconname_invalid_obs := get_icon_name "invalid_obs";
   iconname_timeout_obs := get_icon_name "timeout_obs";
   iconname_outofmemory_obs := get_icon_name "outofmemory_obs";
+  iconname_stepslimitexceeded_obs := get_icon_name "stepslimitexceeded_obs";
   iconname_failure_obs := get_icon_name "failure_obs";
   iconname_yes := get_icon_name "yes";
   iconname_no := get_icon_name "no";
@@ -387,12 +393,14 @@ let resize_images size =
   image_invalid := image ~size !iconname_invalid;
   image_timeout := image ~size !iconname_timeout;
   image_outofmemory := image ~size !iconname_outofmemory;
+  image_stepslimitexceeded := image ~size !iconname_stepslimitexceeded;
   image_failure := image ~size !iconname_failure;
   image_valid_obs := image ~size !iconname_valid_obs;
   image_unknown_obs := image ~size !iconname_unknown_obs;
   image_invalid_obs := image ~size !iconname_invalid_obs;
   image_timeout_obs := image ~size !iconname_timeout_obs;
   image_outofmemory_obs := image ~size !iconname_outofmemory_obs;
+  image_stepslimitexceeded_obs := image ~size !iconname_stepslimitexceeded_obs;
   image_failure_obs := image ~size !iconname_failure_obs;
   image_yes := image ~size !iconname_yes;
   image_no := image ~size !iconname_no;
@@ -458,6 +466,8 @@ let show_legend_window () =
   i "   External prover reached the time limit\n";
   ib image_outofmemory;
   i "   External prover ran out of memory\n";
+  ib image_stepslimitexceeded;
+  i "   External prover exceeded the steps limit\n";
   ib image_unknown;
   i "   External prover answer not conclusive\n";
   ib image_failure;

src/ide/gconfig.mli

@@ -82,12 +82,14 @@ val image_valid : GdkPixbuf.pixbuf ref
 val image_invalid : GdkPixbuf.pixbuf ref
 val image_timeout : GdkPixbuf.pixbuf ref
 val image_outofmemory : GdkPixbuf.pixbuf ref
+val image_stepslimitexceeded : GdkPixbuf.pixbuf ref
 val image_unknown : GdkPixbuf.pixbuf ref
 val image_failure : GdkPixbuf.pixbuf ref
 val image_valid_obs : GdkPixbuf.pixbuf ref
 val image_invalid_obs : GdkPixbuf.pixbuf ref
 val image_timeout_obs : GdkPixbuf.pixbuf ref
 val image_outofmemory_obs : GdkPixbuf.pixbuf ref
+val image_stepslimitexceeded_obs : GdkPixbuf.pixbuf ref
 val image_unknown_obs : GdkPixbuf.pixbuf ref
 val image_failure_obs : GdkPixbuf.pixbuf ref
 

src/ide/gmain.ml

@@ -415,6 +415,9 @@ let image_of_result ~obsolete result =
             if obsolete then !image_timeout_obs else !image_timeout
         | Call_provers.OutOfMemory ->
             if obsolete then !image_outofmemory_obs else !image_outofmemory
+        | Call_provers.StepsLimitExceeded ->
+            if obsolete then !image_stepslimitexceeded_obs
+            else !image_stepslimitexceeded
         | Call_provers.Unknown _ ->
             if obsolete then !image_unknown_obs else !image_unknown
         | Call_provers.Failure _ ->

src/session/session.ml

@@ -562,6 +562,7 @@ let save_result fmt r =
        | Call_provers.HighFailure -> "highfailure"
        | Call_provers.Timeout -> "timeout"
        | Call_provers.OutOfMemory -> "outofmemory"
+       | Call_provers.StepsLimitExceeded -> "stepslimitexceeded"
        | Call_provers.Invalid -> "invalid")
     r.Call_provers.pr_time
     (opt pp_print_int "steps") steps

src/session/session_scheduler.ml

@@ -415,6 +415,7 @@ let adapt_limits a =
       match r with
       | Call_provers.OutOfMemory -> increased_time, a.proof_memlimit
       | Call_provers.Timeout -> a.proof_timelimit, increased_mem
+      | Call_provers.StepsLimitExceeded
       | Call_provers.Valid
       | Call_provers.Unknown _
       | Call_provers.Invalid -> increased_time, increased_mem
@@ -596,66 +597,6 @@ let run_prover eS eT ~context_unproved_goals_only ~timelimit ~memlimit pr a =
       prover_on_goal_or_children eS eT
         ~context_unproved_goals_only ~timelimit ~memlimit pr m.metas_goal
 
-(**********************************)
-(* method: replay obsolete proofs *)
-(**********************************)
-
-(* in the default context, a proof should be replayed if
-   . it was successful or
-   . it was just edited
-*)
-let proof_should_be_replayed a =
-  match a.proof_state with
-    | Done { Call_provers.pr_answer = Call_provers.Valid }
-    | JustEdited -> true
-    | _ -> false
-
-let rec replay_on_goal_or_children eS eT
-    ~obsolete_only ~context_unproved_goals_only g =
-  iter_goal
-    (fun a ->
-       if not obsolete_only || a.proof_obsolete then
-         if not context_unproved_goals_only || proof_should_be_replayed a
-         then run_external_proof eS eT a)
-    (iter_transf
-       (replay_on_goal_or_children eS eT
-          ~obsolete_only ~context_unproved_goals_only)
-    )
-    (iter_metas
-       (replay_on_goal_or_children eS eT
-          ~obsolete_only ~context_unproved_goals_only)
-    )
-    g
-
-let replay eS eT ~obsolete_only ~context_unproved_goals_only a =
-  match a with
-    | Goal g ->
-        replay_on_goal_or_children eS eT
-          ~obsolete_only ~context_unproved_goals_only g
-    | Theory th ->
-        List.iter
-          (replay_on_goal_or_children eS eT
-             ~obsolete_only ~context_unproved_goals_only)
-          th.theory_goals
-    | File file ->
-        List.iter
-          (fun th ->
-             List.iter
-               (replay_on_goal_or_children eS eT
-                  ~obsolete_only ~context_unproved_goals_only)
-               th.theory_goals)
-          file.file_theories
-    | Proof_attempt a ->
-        replay_on_goal_or_children eS eT
-          ~obsolete_only ~context_unproved_goals_only a.proof_parent
-    | Transf tr ->
-        List.iter
-          (replay_on_goal_or_children eS eT
-             ~obsolete_only ~context_unproved_goals_only)
-          tr.transf_goals
-    | Metas m ->
-      replay_on_goal_or_children eS eT
-        ~obsolete_only ~context_unproved_goals_only m.metas_goal
 
 
 (***********************************)
@@ -735,6 +676,68 @@ let check_all ?(release=false) ?filter eS eT ~callback =
   Todo.stop todo
 
 
+(**********************************)
+(* method: replay obsolete proofs *)
+(**********************************)
+
+(* in the default context, a proof should be replayed if
+   . it was successful or
+   . it was just edited
+*)
+let proof_should_be_replayed a =
+  match a.proof_state with
+    | Done { Call_provers.pr_answer = Call_provers.Valid }
+    | JustEdited -> true
+    | _ -> false
+
+let rec replay_on_goal_or_children eS eT
+    ~obsolete_only ~context_unproved_goals_only g =
+  iter_goal
+    (fun a ->
+       if not obsolete_only || a.proof_obsolete then
+         if not context_unproved_goals_only || proof_should_be_replayed a
+         then run_external_proof eS eT a)
+    (iter_transf
+       (replay_on_goal_or_children eS eT
+          ~obsolete_only ~context_unproved_goals_only)
+    )
+    (iter_metas
+       (replay_on_goal_or_children eS eT
+          ~obsolete_only ~context_unproved_goals_only)
+    )
+    g
+
+let replay eS eT ~obsolete_only ~context_unproved_goals_only a =
+  match a with
+    | Goal g ->
+        replay_on_goal_or_children eS eT
+          ~obsolete_only ~context_unproved_goals_only g
+    | Theory th ->
+        List.iter
+          (replay_on_goal_or_children eS eT
+             ~obsolete_only ~context_unproved_goals_only)
+          th.theory_goals
+    | File file ->
+        List.iter
+          (fun th ->
+             List.iter
+               (replay_on_goal_or_children eS eT
+                  ~obsolete_only ~context_unproved_goals_only)
+               th.theory_goals)
+          file.file_theories
+    | Proof_attempt a ->
+        replay_on_goal_or_children eS eT
+          ~obsolete_only ~context_unproved_goals_only a.proof_parent
+    | Transf tr ->
+        List.iter
+          (replay_on_goal_or_children eS eT
+             ~obsolete_only ~context_unproved_goals_only)
+          tr.transf_goals
+    | Metas m ->
+      replay_on_goal_or_children eS eT
+        ~obsolete_only ~context_unproved_goals_only m.metas_goal
+
+
 (***********************************)
 (* play all                        *)
 (***********************************)

src/why3session/why3session_html.ml

@@ -138,6 +138,8 @@ let print_results fmt provers proofs =
 		| Call_provers.OutOfMemory ->
                   fprintf fmt "FF8000\">Out Of Memory (%dM)"
                     pr.S.proof_memlimit
+		| Call_provers.StepsLimitExceeded ->
+                  fprintf fmt "FF8000\">Steps limit exceeded"
 		| Call_provers.Unknown _ ->
                   fprintf fmt "FF8000\">%.2f" res.Call_provers.pr_time
 		| Call_provers.Failure _ ->

src/why3session/why3session_latex.ml

@@ -133,6 +133,8 @@ let print_result_prov proofs prov fmt=
                   fprintf fmt "& \\timeout{%ds} " pr.S.proof_timelimit
 		| Call_provers.OutOfMemory ->
                   fprintf fmt "& \\outofmemory{%dM} " pr.S.proof_memlimit
+		| Call_provers.StepsLimitExceeded ->
+                  fprintf fmt "& \\stepslimitexceeded "
 		| Call_provers.Unknown _ ->
                   fprintf fmt "& \\unknown{%.2f} " res.Call_provers.pr_time
 		| Call_provers.Failure _ ->