# HG changeset patch
# User blanchet
# Date 1290611715 -3600
# Node ID c7ba327eb58cffd7d3a045f2660159780c916f2a
# Parent  a3f37b3d303ada3ffcee4262942652bba5a4e588
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers

diff -r a3f37b3d303a -r c7ba327eb58c src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Nov 24 16:15:15 2010 +0100
@@ -71,9 +71,9 @@
 fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
 val strip_spaces_except_between_ident_chars = strip_spaces is_ident_char
 
-val missing_message_tail =
-  " appears to be missing. You will need to install it if you want to run \
-  \ATPs remotely."
+fun missing_message_tail prover =
+  " appears to be missing. You will need to install it if you want to run " ^
+  prover ^ "s remotely."
 
 fun string_for_failure prover Unprovable =
     "The " ^ prover ^ " problem is unprovable."
@@ -96,9 +96,9 @@
     "Isabelle requires a more recent version of Vampire. To install it, follow \
     \the instructions from the Sledgehammer manual (\"isabelle doc\
     \ sledgehammer\")."
-  | string_for_failure _ NoPerl = "Perl" ^ missing_message_tail
-  | string_for_failure _ NoLibwwwPerl =
-    "The Perl module \"libwww-perl\"" ^ missing_message_tail
+  | 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 MalformedInput =
     "The " ^ prover ^ " problem is malformed. Please report this to the Isabelle \
     \developers."
diff -r a3f37b3d303a -r c7ba327eb58c src/HOL/Tools/SMT/lib/scripts/remote_smt
--- a/src/HOL/Tools/SMT/lib/scripts/remote_smt	Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Tools/SMT/lib/scripts/remote_smt	Wed Nov 24 16:15:15 2010 +0100
@@ -26,6 +26,6 @@
   "Options" => join(" ", @options),
   "Problem" => [$problem_file] ],
   "Content_Type" => "form-data");
-if (not $response->is_success) { die "HTTP-Error: " . $response->message; }
+if (not $response->is_success) { die "HTTP error: " . $response->message; }
 else { print $response->content; }
 
diff -r a3f37b3d303a -r c7ba327eb58c src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Nov 24 16:15:15 2010 +0100
@@ -412,16 +412,23 @@
 (* "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 z3_malformed_input_codes = [103, 110]
-val sigsegv_code = 139
+val remote_smt_failures =
+  [(22, CantConnect),
+   (127, NoPerl),
+   (2, NoLibwwwPerl)]
+val z3_failures =
+  [(103, MalformedInput),
+   (110, MalformedInput)]
+val unix_failures =
+  [(139, Crashed)]
+val smt_failures = remote_smt_failures @ z3_failures @ unix_failures
 
 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) =
-    if member (op =) z3_malformed_input_codes code then MalformedInput
-    else if code = sigsegv_code then Crashed
-    else IncompleteUnprovable
+    (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 _ = UnknownError
 
@@ -521,7 +528,6 @@
       #> Config.put SMT_Config.verbose debug
       #> Config.put SMT_Config.monomorph_limit smt_monomorph_limit
     val state = state |> Proof.map_context repair_context
-    val ctxt = Proof.context_of state
     val thy = Proof.theory_of state
     val smt_fact = Option.map (apsnd (Thm.transfer thy)) o try dest_Untranslated
     val {outcome, used_facts, run_time_in_msecs} =