--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Apr 23 13:16:50 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Apr 23 15:48:34 2010 +0200
@@ -1,5 +1,6 @@
(* Title: HOL/Tools/ATP_Manager/atp_minimal.ML
Author: Philipp Meyer, TU Muenchen
+ Author: Jasmin Blanchette, TU Muenchen
Minimization of theorem list for Metis using automatic theorem provers.
*)
@@ -35,34 +36,16 @@
in aux s end
-(* failure check and producing answer *)
-
-datatype outcome = Success | Failure | Timeout | Error
-
-val string_of_outcome =
- fn Success => "Success"
- | Failure => "Failure"
- | Timeout => "Timeout"
- | Error => "Error"
+(* wrapper for calling external prover *)
-(* FIXME: move to "atp_wrapper.ML" *)
-val failure_strings =
- [("SPASS beiseite: Ran out of time.", Timeout),
- ("Timeout", Timeout),
- ("time limit exceeded", Timeout),
- ("# Cannot determine problem status within resource limit", Timeout),
- ("Error", Error)]
-
-fun outcome_of_result (result as {success, output, ...} : prover_result) =
- if success then
- Success
- else case get_first (fn (s, outcome) =>
- if String.isSubstring s output then SOME outcome
- else NONE) failure_strings of
- SOME outcome => outcome
- | NONE => Failure
-
-(* wrapper for calling external prover *)
+fun string_for_failure Unprovable = "Unprovable."
+ | string_for_failure TimedOut = "Timed out."
+ | string_for_failure OutOfResources = "Failed."
+ | string_for_failure OldSpass = "Error."
+ | string_for_failure MalformedOutput = "Error."
+ | string_for_failure UnknownError = "Failed."
+fun string_for_outcome NONE = "Success."
+ | string_for_outcome (SOME failure) = string_for_failure failure
fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover
timeout subgoal state filtered_clauses name_thms_pairs =
@@ -79,8 +62,8 @@
axiom_clauses = SOME axclauses,
filtered_clauses = SOME (the_default axclauses filtered_clauses)}
in
- `outcome_of_result (prover params (K "") timeout problem)
- |>> tap (priority o string_of_outcome)
+ prover params (K "") timeout problem
+ |> tap (priority o string_for_outcome o #outcome)
end
(* minimalization of thms *)
@@ -98,7 +81,7 @@
sledgehammer_test_theorems params prover minimize_timeout i state
fun test_thms filtered thms =
case test_thms_fun filtered thms of
- (Success, result) => SOME result
+ (result as {outcome = NONE, ...}) => SOME result
| _ => NONE
val {context = ctxt, facts, goal} = Proof.goal state;
@@ -106,7 +89,7 @@
in
(* try prove first to check result and get used theorems *)
(case test_thms_fun NONE name_thms_pairs of
- (Success, result as {internal_thm_names, filtered_clauses, ...}) =>
+ result as {outcome = NONE, internal_thm_names, filtered_clauses, ...} =>
let
val used = internal_thm_names |> Vector.foldr (op ::) []
|> sort_distinct string_ord
@@ -126,17 +109,17 @@
proof_text isar_proof debug modulus sorts ctxt
(K "", proof, internal_thm_names, goal, i) |> fst)
end
- | (Timeout, _) =>
+ | {outcome = SOME TimedOut, ...} =>
(NONE, "Timeout: You can increase the time limit using the \"timeout\" \
\option (e.g., \"timeout = " ^
string_of_int (10 + msecs div 1000) ^ " s\").")
- | (Error, {message, ...}) => (NONE, "ATP error: " ^ message)
- | (Failure, _) =>
+ | {outcome = SOME UnknownError, ...} =>
(* Failure sometimes mean timeout, unfortunately. *)
(NONE, "Failure: No proof was found with the current time limit. You \
\can increase the time limit using the \"timeout\" \
\option (e.g., \"timeout = " ^
- string_of_int (10 + msecs div 1000) ^ " s\")."))
+ string_of_int (10 + msecs div 1000) ^ " s\").")
+ | {message, ...} => (NONE, "ATP error: " ^ message))
handle Sledgehammer_HOL_Clause.TRIVIAL =>
(SOME [], metis_line i n [])
| ERROR msg => (NONE, "Error: " ^ msg)