capture out-of-memory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver run-time: return NONE instead of ~1

--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Tue Oct 26 17:35:49 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Tue Oct 26 17:35:51 2010 +0200
@@ -64,9 +64,12 @@
 fun z3_on_last_line solver_name lines =
   let
     fun junk l =
-      String.isPrefix "WARNING" l orelse
-      String.isPrefix "ERROR" l orelse
-      forall Symbol.is_ascii_blank (Symbol.explode l)
+      if String.isPrefix "WARNING: Out of allocated virtual memory" l
+      then raise SMT_Solver.SMT SMT_Solver.Out_Of_Memory
+      else
+        String.isPrefix "WARNING" l orelse
+        String.isPrefix "ERROR" l orelse
+        forall Symbol.is_ascii_blank (Symbol.explode l)
   in
     the_default ("", []) (try (swap o split_last) (filter_out junk lines))
     |>> outcome_of "unsat" "sat" "unknown" solver_name

--- a/src/HOL/Tools/SMT/smt_solver.ML	Tue Oct 26 17:35:49 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Tue Oct 26 17:35:51 2010 +0200
@@ -9,8 +9,9 @@
   datatype failure =
     Counterexample of bool * term list |
     Time_Out |
+    Out_Of_Memory |
     Other_Failure of string
-  val string_of_failure: Proof.context -> failure -> string
+  val string_of_failure: Proof.context -> string -> failure -> string
   exception SMT of failure
 
   type interface = {
@@ -57,7 +58,8 @@
 
   (*filter*)
   val smt_filter: bool -> Time.time -> Proof.state -> ('a * thm) list -> int ->
-    {outcome: failure option, used_facts: 'a list, run_time_in_msecs: int}
+    {outcome: failure option, used_facts: 'a list,
+    run_time_in_msecs: int option}
 
   (*tactic*)
   val smt_tac': bool -> Proof.context -> thm list -> int -> Tactical.tactic
@@ -74,9 +76,10 @@
 datatype failure =
   Counterexample of bool * term list |
   Time_Out |
+  Out_Of_Memory |
   Other_Failure of string
 
-fun string_of_failure ctxt (Counterexample (real, ex)) =
+fun string_of_failure ctxt _ (Counterexample (real, ex)) =
       let
         val msg = (if real then "C" else "Potential c") ^ "ounterexample found"
       in
@@ -84,8 +87,9 @@
         else Pretty.string_of (Pretty.big_list (msg ^ ":")
           (map (Syntax.pretty_term ctxt) ex))
       end
-  | string_of_failure _ Time_Out = "Time out."
-  | string_of_failure _ (Other_Failure msg) = msg
+  | string_of_failure _ name Time_Out = name ^ " timed out."
+  | string_of_failure _ name Out_Of_Memory = name ^ " ran out of memory."
+  | string_of_failure _ _ (Other_Failure msg) = msg
 
 exception SMT of failure
 
@@ -431,9 +435,9 @@
     split_list xrules
     ||> distinct (op =) o fst o smt_solver rm ctxt o append irs o map_index I
     |-> map_filter o try o nth
-    |> (fn xs => {outcome=NONE, used_facts=xs, run_time_in_msecs= ~1})
+    |> (fn xs => {outcome=NONE, used_facts=xs, run_time_in_msecs=NONE})
   end
-  handle SMT fail => {outcome=SOME fail, used_facts=[], run_time_in_msecs= ~1}
+  handle SMT fail => {outcome=SOME fail, used_facts=[], run_time_in_msecs=NONE}
   (* FIXME: measure runtime *)
 
 
@@ -446,7 +450,8 @@
   THEN' SUBPROOF (fn {context=cx, prems, ...} =>
     let
       fun solve () = snd (smt_solver NONE cx (map (pair ~1) (rules @ prems)))
-      val trace = trace_msg cx (prefix "SMT: " o string_of_failure cx)
+      val name = solver_name_of (Context.Proof cx)
+      val trace = trace_msg cx (prefix "SMT: " o string_of_failure cx name)
     in
       (if pass_exns then SOME (solve ())
        else (SOME (solve ()) handle SMT fail => (trace fail; NONE)))

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Oct 26 17:35:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Oct 26 17:35:51 2010 +0200
@@ -426,11 +426,12 @@
                           command_call smtN (map fst used_facts)) ^
         minimize_line minimize_command (map fst used_facts)
       | SOME (failure as SMT_Solver.Other_Failure _) =>
-        SMT_Solver.string_of_failure ctxt failure
+        SMT_Solver.string_of_failure ctxt
+          (SMT_Solver.solver_name_of (Context.Proof ctxt)) failure
       | SOME _ => string_for_failure (the outcome')
   in
     {outcome = outcome', used_axioms = used_facts,
-     run_time_in_msecs = SOME run_time_in_msecs, message = message}
+     run_time_in_msecs = run_time_in_msecs, message = message}
   end
 
 fun get_prover ctxt auto name =