# HG changeset patch
# User blanchet
# Date 1290548236 -3600
# Node ID 5c316d1327d462ab5a4281d679fd3f79d4e4fd3a
# Parent  661e334d31f0758e2c6afcb835dcaf5d949300e2
more precise error handling for Z3;
refactored some of the error handling code shared by ATP and SMT

diff -r 661e334d31f0 -r 5c316d1327d4 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Nov 23 21:54:03 2010 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Nov 23 22:37:16 2010 +0100
@@ -26,7 +26,7 @@
   type 'a proof = 'a uniform_formula step list
 
   val strip_spaces : (char -> bool) -> string -> string
-  val string_for_failure : failure -> string
+  val string_for_failure : string -> failure -> string
   val extract_important_message : string -> string
   val extract_known_failure :
     (failure * string) list -> string -> failure option
@@ -75,13 +75,15 @@
   " appears to be missing. You will need to install it if you want to run \
   \ATPs remotely."
 
-fun string_for_failure Unprovable = "The ATP problem is unprovable."
-  | string_for_failure IncompleteUnprovable =
-    "The ATP cannot prove the problem."
-  | string_for_failure CantConnect = "Can't connect to remote server."
-  | string_for_failure TimedOut = "Timed out."
-  | string_for_failure OutOfResources = "The ATP ran out of resources."
-  | string_for_failure SpassTooOld =
+fun string_for_failure prover Unprovable =
+    "The " ^ prover ^ " problem is unprovable."
+  | string_for_failure prover IncompleteUnprovable =
+    "The " ^ prover ^ " cannot prove the problem."
+  | string_for_failure _ CantConnect = "Cannot connect to remote server."
+  | string_for_failure _ TimedOut = "Timed out."
+  | string_for_failure prover OutOfResources =
+    "The " ^ prover ^ " ran out of resources."
+  | string_for_failure _ SpassTooOld =
     "Isabelle requires a more recent version of SPASS with support for the \
     \TPTP syntax. To install it, download and extract the package \
     \\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \
@@ -90,21 +92,24 @@
                (Path.variable "ISABELLE_HOME_USER" ::
                 map Path.basic ["etc", "components"])))) ^
     " on a line of its own."
-  | string_for_failure VampireTooOld =
+  | string_for_failure _ VampireTooOld =
     "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 =
+  | string_for_failure _ NoPerl = "Perl" ^ missing_message_tail
+  | string_for_failure _ NoLibwwwPerl =
     "The Perl module \"libwww-perl\"" ^ missing_message_tail
-  | string_for_failure MalformedInput =
-    "The ATP problem is malformed. Please report this to the Isabelle \
+  | string_for_failure prover MalformedInput =
+    "The " ^ prover ^ " problem is malformed. Please report this to the Isabelle \
     \developers."
-  | string_for_failure MalformedOutput = "The ATP output is malformed."
-  | string_for_failure Interrupted = "The ATP was interrupted."
-  | string_for_failure Crashed = "The ATP crashed."
-  | string_for_failure InternalError = "An internal ATP error occurred."
-  | string_for_failure UnknownError = "An unknown ATP error occurred."
+  | string_for_failure prover MalformedOutput =
+    "The " ^ prover ^ " output is malformed."
+  | string_for_failure prover Interrupted = "The " ^ prover ^ " was interrupted."
+  | string_for_failure prover Crashed = "The " ^ prover ^ " crashed."
+  | string_for_failure prover InternalError =
+    "An internal " ^ prover ^ " error occurred."
+  | string_for_failure prover UnknownError =
+    "An unknown " ^ prover ^ " error occurred."
 
 fun extract_delimited (begin_delim, end_delim) output =
   output |> first_field begin_delim |> the |> snd
diff -r 661e334d31f0 -r 5c316d1327d4 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Nov 23 21:54:03 2010 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Nov 23 22:37:16 2010 +0100
@@ -186,7 +186,7 @@
     (output, 0) => split_lines output
   | (output, _) =>
     error (case extract_known_failure known_perl_failures output of
-             SOME failure => string_for_failure failure
+             SOME failure => string_for_failure "ATP" failure
            | NONE => perhaps (try (unsuffix "\n")) output ^ ".")
 
 fun find_system name [] systems = find_first (String.isPrefix name) systems
diff -r 661e334d31f0 -r 5c316d1327d4 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Nov 23 21:54:03 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Nov 23 22:37:16 2010 +0100
@@ -403,21 +403,25 @@
                    important_message
                  else
                    ""))
-      | SOME failure => (string_for_failure failure, [])
+      | SOME failure => (string_for_failure "ATP" failure, [])
   in
     {outcome = outcome, message = message, used_facts = used_facts,
      run_time_in_msecs = msecs}
   end
 
-(* "SMT_Failure.Abnormal_Termination" carries the solver's return code.
-   Return codes 1 to 127 are application-specific, whereas (at least on
-   Unix) 128 to 255 are reserved for signals (e.g., SIGSEGV) and other
-   system codes. *)
+(* "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
 
 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 code >= 128 then Crashed else IncompleteUnprovable
+    if member (op =) z3_malformed_input_codes code then MalformedInput
+    else if code = sigsegv_code then Crashed
+    else IncompleteUnprovable
   | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
   | failure_from_smt_failure _ = UnknownError
 
@@ -522,6 +526,7 @@
     val smt_fact = Option.map (apsnd (Thm.transfer thy)) o try dest_Untranslated
     val {outcome, used_facts, run_time_in_msecs} =
       smt_filter_loop params remote state subgoal (map_filter smt_fact facts)
+    val outcome = outcome |> Option.map failure_from_smt_failure
     val message =
       case outcome of
         NONE =>
@@ -535,15 +540,7 @@
                             command_call method (map (fst o fst) used_facts)) ^
           minimize_line minimize_command (map (fst o fst) used_facts)
         end
-      | SOME SMT_Failure.Time_Out => "Timed out."
-      | SOME (SMT_Failure.Abnormal_Termination code) =>
-        "The SMT solver terminated abnormally with exit code " ^
-        string_of_int code ^ "."
-      | SOME (SMT_Failure.Counterexample _) => "The SMT problem is unprovable."
-      | SOME SMT_Failure.Out_Of_Memory => "The SMT solver ran out of memory."
-      | SOME failure =>
-        SMT_Failure.string_of_failure ctxt failure
-    val outcome = outcome |> Option.map failure_from_smt_failure (* FIXME *)
+      | SOME failure => string_for_failure "SMT solver" failure
   in
     {outcome = outcome, used_facts = map fst used_facts,
      run_time_in_msecs = run_time_in_msecs, message = message}