--- 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."
--- 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; }
--- 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} =