more precise/correct SMT error handling

--- a/src/HOL/Tools/ATP/atp_proof.ML	Fri Dec 17 00:11:06 2010 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Fri Dec 17 00:27:40 2010 +0100
@@ -14,8 +14,8 @@
   datatype failure =
     Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
     OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl |
-    MalformedInput | MalformedOutput | Interrupted | Crashed | InternalError |
-    UnknownError
+    NoRealZ3 | MalformedInput | MalformedOutput | Interrupted | Crashed |
+    InternalError | UnknownError
 
   type step_name = string * string option
 
@@ -47,8 +47,9 @@
 
 datatype failure =
   Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
-  SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl | MalformedInput |
-  MalformedOutput | Interrupted | Crashed | InternalError | UnknownError
+  SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl | NoRealZ3 |
+  MalformedInput | MalformedOutput | Interrupted | Crashed | InternalError |
+  UnknownError
 
 fun strip_spaces_in_list _ [] = []
   | strip_spaces_in_list _ [c1] = if Char.isSpace c1 then [] else [str c1]
@@ -99,6 +100,8 @@
   | string_for_failure prover NoPerl = "Perl" ^ missing_message_tail prover
   | string_for_failure prover NoLibwwwPerl =
     "The Perl module \"libwww-perl\"" ^ missing_message_tail prover
+  | string_for_failure prover NoRealZ3 =
+    "The environment variable \"Z3_REAL_SOLVER\" must be set to Z3's full path."
   | string_for_failure prover MalformedInput =
     "The " ^ prover ^ " problem is malformed. Please report this to the \
     \Isabelle developers."

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Dec 17 00:11:06 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Dec 17 00:27:40 2010 +0100
@@ -51,7 +51,7 @@
   type prover = params -> minimize_command -> prover_problem -> prover_result
 
   (* for experimentation purposes -- do not use in production code *)
-  val smt_max_iter : int Unsynchronized.ref
+  val smt_max_iters : int Unsynchronized.ref
   val smt_iter_fact_frac : real Unsynchronized.ref
   val smt_iter_time_frac : real Unsynchronized.ref
   val smt_iter_min_msecs : int Unsynchronized.ref
@@ -431,32 +431,40 @@
 (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until
    these are sorted out properly in the SMT module, we have to interpret these
    ourselves. *)
+val perl_failures =
+  [(127, NoPerl)]
 val remote_smt_failures =
   [(22, CantConnect),
    (2, NoLibwwwPerl)]
+val z3_wrapper_failures =
+  [(10, NoRealZ3),
+   (11, InternalError),
+   (12, InternalError),
+   (13, InternalError)]
 val z3_failures =
   [(103, MalformedInput),
-   (110, MalformedInput),
-   (127, NoPerl)] (* can occur with "z3_wrapper", written in Perl *)
+   (110, MalformedInput)]
 val unix_failures =
   [(139, Crashed)]
+val smt_failures =
+  perl_failures @ remote_smt_failures @ z3_wrapper_failures @ z3_failures @
+  unix_failures
 
 val internal_error_prefix = "Internal error: "
 
-fun failure_from_smt_failure _ (SMT_Failure.Counterexample _) = Unprovable
-  | failure_from_smt_failure _ SMT_Failure.Time_Out = TimedOut
-  | failure_from_smt_failure remote (SMT_Failure.Abnormal_Termination code) =
-    (case AList.lookup (op =) (z3_failures @ unix_failures
-                               |> remote ? append remote_smt_failures) code of
+fun failure_from_smt_failure (SMT_Failure.Counterexample _) = Unprovable
+  | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
+  | failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) =
+    (case AList.lookup (op =) smt_failures code of
        SOME failure => failure
      | NONE => UnknownError)
-  | failure_from_smt_failure _ SMT_Failure.Out_Of_Memory = OutOfResources
-  | failure_from_smt_failure _ (SMT_Failure.Other_Failure msg) =
+  | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
+  | failure_from_smt_failure (SMT_Failure.Other_Failure msg) =
     if String.isPrefix internal_error_prefix msg then InternalError
     else UnknownError
 
 (* FUDGE *)
-val smt_max_iter = Unsynchronized.ref 8
+val smt_max_iters = Unsynchronized.ref 8
 val smt_iter_fact_frac = Unsynchronized.ref 0.5
 val smt_iter_time_frac = Unsynchronized.ref 0.5
 val smt_iter_min_msecs = Unsynchronized.ref 5000
@@ -470,7 +478,7 @@
         val timer = Timer.startRealTimer ()
         val ms = timeout |> Time.toMilliseconds
         val iter_timeout =
-          if iter_num < !smt_max_iter then
+          if iter_num < !smt_max_iters then
             Int.min (ms,
                 Int.max (!smt_iter_min_msecs,
                     Real.ceil (!smt_iter_time_frac * Real.fromInt ms)))
@@ -525,7 +533,7 @@
           | SOME (SMT_Failure.Other_Failure _) => true
         val timeout = Time.- (timeout, Timer.checkRealTimer timer)
       in
-        if too_many_facts_perhaps andalso iter_num < !smt_max_iter andalso
+        if too_many_facts_perhaps andalso iter_num < !smt_max_iters andalso
            num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then
           let
             val n = Real.ceil (!smt_iter_fact_frac * Real.fromInt num_facts)
@@ -603,7 +611,7 @@
     val {outcome, used_facts, run_time_in_msecs} =
       smt_filter_loop params remote state subgoal facts
     val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts)
-    val outcome = outcome |> Option.map (failure_from_smt_failure remote)
+    val outcome = outcome |> Option.map failure_from_smt_failure
     val message =
       case outcome of
         NONE =>