1.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Nov 23 21:54:03 2010 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Nov 23 22:37:16 2010 +0100
     1.3 @@ -26,7 +26,7 @@
     1.4    type 'a proof = 'a uniform_formula step list
     1.5  
     1.6    val strip_spaces : (char -> bool) -> string -> string
     1.7 -  val string_for_failure : failure -> string
     1.8 +  val string_for_failure : string -> failure -> string
     1.9    val extract_important_message : string -> string
    1.10    val extract_known_failure :
    1.11      (failure * string) list -> string -> failure option
    1.12 @@ -75,13 +75,15 @@
    1.13    " appears to be missing. You will need to install it if you want to run \
    1.14    \ATPs remotely."
    1.15  
    1.16 -fun string_for_failure Unprovable = "The ATP problem is unprovable."
    1.17 -  | string_for_failure IncompleteUnprovable =
    1.18 -    "The ATP cannot prove the problem."
    1.19 -  | string_for_failure CantConnect = "Can't connect to remote server."
    1.20 -  | string_for_failure TimedOut = "Timed out."
    1.21 -  | string_for_failure OutOfResources = "The ATP ran out of resources."
    1.22 -  | string_for_failure SpassTooOld =
    1.23 +fun string_for_failure prover Unprovable =
    1.24 +    "The " ^ prover ^ " problem is unprovable."
    1.25 +  | string_for_failure prover IncompleteUnprovable =
    1.26 +    "The " ^ prover ^ " cannot prove the problem."
    1.27 +  | string_for_failure _ CantConnect = "Cannot connect to remote server."
    1.28 +  | string_for_failure _ TimedOut = "Timed out."
    1.29 +  | string_for_failure prover OutOfResources =
    1.30 +    "The " ^ prover ^ " ran out of resources."
    1.31 +  | string_for_failure _ SpassTooOld =
    1.32      "Isabelle requires a more recent version of SPASS with support for the \
    1.33      \TPTP syntax. To install it, download and extract the package \
    1.34      \\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \
    1.35 @@ -90,21 +92,24 @@
    1.36                 (Path.variable "ISABELLE_HOME_USER" ::
    1.37                  map Path.basic ["etc", "components"])))) ^
    1.38      " on a line of its own."
    1.39 -  | string_for_failure VampireTooOld =
    1.40 +  | string_for_failure _ VampireTooOld =
    1.41      "Isabelle requires a more recent version of Vampire. To install it, follow \
    1.42      \the instructions from the Sledgehammer manual (\"isabelle doc\
    1.43      \ sledgehammer\")."
    1.44 -  | string_for_failure NoPerl = "Perl" ^ missing_message_tail
    1.45 -  | string_for_failure NoLibwwwPerl =
    1.46 +  | string_for_failure _ NoPerl = "Perl" ^ missing_message_tail
    1.47 +  | string_for_failure _ NoLibwwwPerl =
    1.48      "The Perl module \"libwww-perl\"" ^ missing_message_tail
    1.49 -  | string_for_failure MalformedInput =
    1.50 -    "The ATP problem is malformed. Please report this to the Isabelle \
    1.51 +  | string_for_failure prover MalformedInput =
    1.52 +    "The " ^ prover ^ " problem is malformed. Please report this to the Isabelle \
    1.53      \developers."
    1.54 -  | string_for_failure MalformedOutput = "The ATP output is malformed."
    1.55 -  | string_for_failure Interrupted = "The ATP was interrupted."
    1.56 -  | string_for_failure Crashed = "The ATP crashed."
    1.57 -  | string_for_failure InternalError = "An internal ATP error occurred."
    1.58 -  | string_for_failure UnknownError = "An unknown ATP error occurred."
    1.59 +  | string_for_failure prover MalformedOutput =
    1.60 +    "The " ^ prover ^ " output is malformed."
    1.61 +  | string_for_failure prover Interrupted = "The " ^ prover ^ " was interrupted."
    1.62 +  | string_for_failure prover Crashed = "The " ^ prover ^ " crashed."
    1.63 +  | string_for_failure prover InternalError =
    1.64 +    "An internal " ^ prover ^ " error occurred."
    1.65 +  | string_for_failure prover UnknownError =
    1.66 +    "An unknown " ^ prover ^ " error occurred."
    1.67  
    1.68  fun extract_delimited (begin_delim, end_delim) output =
    1.69    output |> first_field begin_delim |> the |> snd

     2.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Nov 23 21:54:03 2010 +0100
     2.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Nov 23 22:37:16 2010 +0100
     2.3 @@ -186,7 +186,7 @@
     2.4      (output, 0) => split_lines output
     2.5    | (output, _) =>
     2.6      error (case extract_known_failure known_perl_failures output of
     2.7 -             SOME failure => string_for_failure failure
     2.8 +             SOME failure => string_for_failure "ATP" failure
     2.9             | NONE => perhaps (try (unsuffix "\n")) output ^ ".")
    2.10  
    2.11  fun find_system name [] systems = find_first (String.isPrefix name) systems

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Nov 23 21:54:03 2010 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Nov 23 22:37:16 2010 +0100
     3.3 @@ -403,21 +403,25 @@
     3.4                     important_message
     3.5                   else
     3.6                     ""))
     3.7 -      | SOME failure => (string_for_failure failure, [])
     3.8 +      | SOME failure => (string_for_failure "ATP" failure, [])
     3.9    in
    3.10      {outcome = outcome, message = message, used_facts = used_facts,
    3.11       run_time_in_msecs = msecs}
    3.12    end
    3.13  
    3.14 -(* "SMT_Failure.Abnormal_Termination" carries the solver's return code.
    3.15 -   Return codes 1 to 127 are application-specific, whereas (at least on
    3.16 -   Unix) 128 to 255 are reserved for signals (e.g., SIGSEGV) and other
    3.17 -   system codes. *)
    3.18 +(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until
    3.19 +   these are sorted out properly in the SMT module, we have to interpret these
    3.20 +   ourselves. *)
    3.21 +
    3.22 +val z3_malformed_input_codes = [103, 110]
    3.23 +val sigsegv_code = 139
    3.24  
    3.25  fun failure_from_smt_failure (SMT_Failure.Counterexample _) = Unprovable
    3.26    | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
    3.27    | failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) =
    3.28 -    if code >= 128 then Crashed else IncompleteUnprovable
    3.29 +    if member (op =) z3_malformed_input_codes code then MalformedInput
    3.30 +    else if code = sigsegv_code then Crashed
    3.31 +    else IncompleteUnprovable
    3.32    | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
    3.33    | failure_from_smt_failure _ = UnknownError
    3.34  
    3.35 @@ -522,6 +526,7 @@
    3.36      val smt_fact = Option.map (apsnd (Thm.transfer thy)) o try dest_Untranslated
    3.37      val {outcome, used_facts, run_time_in_msecs} =
    3.38        smt_filter_loop params remote state subgoal (map_filter smt_fact facts)
    3.39 +    val outcome = outcome |> Option.map failure_from_smt_failure
    3.40      val message =
    3.41        case outcome of
    3.42          NONE =>
    3.43 @@ -535,15 +540,7 @@
    3.44                              command_call method (map (fst o fst) used_facts)) ^
    3.45            minimize_line minimize_command (map (fst o fst) used_facts)
    3.46          end
    3.47 -      | SOME SMT_Failure.Time_Out => "Timed out."
    3.48 -      | SOME (SMT_Failure.Abnormal_Termination code) =>
    3.49 -        "The SMT solver terminated abnormally with exit code " ^
    3.50 -        string_of_int code ^ "."
    3.51 -      | SOME (SMT_Failure.Counterexample _) => "The SMT problem is unprovable."
    3.52 -      | SOME SMT_Failure.Out_Of_Memory => "The SMT solver ran out of memory."
    3.53 -      | SOME failure =>
    3.54 -        SMT_Failure.string_of_failure ctxt failure
    3.55 -    val outcome = outcome |> Option.map failure_from_smt_failure (* FIXME *)
    3.56 +      | SOME failure => string_for_failure "SMT solver" failure
    3.57    in
    3.58      {outcome = outcome, used_facts = map fst used_facts,
    3.59       run_time_in_msecs = run_time_in_msecs, message = message}