--- 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)
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Apr 23 13:16:50 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Apr 23 15:48:34 2010 +0200
@@ -43,20 +43,20 @@
(* prover configuration *)
-val remotify = prefix "remote_"
-
type prover_config =
- {home: string,
- executable: string,
- arguments: Time.time -> string,
- proof_delims: (string * string) list,
- known_failures: (string list * string) list,
- max_new_clauses: int,
- prefers_theory_relevant: bool};
+ {home: string,
+ executable: string,
+ arguments: Time.time -> string,
+ proof_delims: (string * string) list,
+ known_failures: (failure * string) list,
+ max_new_clauses: int,
+ prefers_theory_relevant: bool};
(* basic template *)
+val remotify = prefix "remote_"
+
fun with_path cleanup after f path =
Exn.capture f path
|> tap (fn _ => cleanup path)
@@ -72,17 +72,30 @@
|> first_field end_delim |> the |> fst
| _ => ""
-fun extract_proof_or_failure proof_delims known_failures output =
- case map_filter
- (fn (patterns, message) =>
- if exists (fn p => String.isSubstring p output) patterns then
- SOME message
- else
- NONE) known_failures of
+fun extract_proof_and_outcome res_code proof_delims known_failures output =
+ case map_filter (fn (failure, pattern) =>
+ if String.isSubstring pattern output then SOME failure
+ else NONE) known_failures of
[] => (case extract_proof proof_delims output of
- "" => ("", "Error: The ATP output is malformed.")
- | proof => (proof, ""))
- | (message :: _) => ("", message)
+ "" => ("", SOME UnknownError)
+ | proof => if res_code = 0 then (proof, NONE)
+ else ("", SOME UnknownError))
+ | (failure :: _) => ("", SOME failure)
+
+fun string_for_failure Unprovable = "The ATP problem is unprovable."
+ | string_for_failure TimedOut = "Timed out."
+ | string_for_failure OutOfResources = "The ATP ran out of resources."
+ | string_for_failure OldSpass =
+ "Warning: Sledgehammer requires a more recent version of SPASS with \
+ \support for the TPTP syntax. To install it, download and untar the \
+ \package \"http://isabelle.in.tum.de/~blanchet/spass-3.7.tgz\" and add the \
+ \\"spass-3.7\" directory's full path to \"" ^
+ Path.implode (Path.expand (Path.appends
+ (Path.variable "ISABELLE_HOME_USER" ::
+ map Path.basic ["etc", "components"]))) ^
+ "\" on a line of its own."
+ | string_for_failure MalformedOutput = "Error: The ATP output is malformed."
+ | string_for_failure UnknownError = "Error: An unknown ATP error occurred."
fun generic_prover overlord get_facts prepare write_file home executable args
proof_delims known_failures name
@@ -176,23 +189,20 @@
else
"") ^ output)
- val (((output, atp_run_time_in_msecs), rc), _) =
+ val (((output, atp_run_time_in_msecs), res_code), _) =
with_path cleanup export run_on (prob_pathname subgoal);
(* Check for success and print out some information on failure. *)
- val (proof, failure) =
- extract_proof_or_failure proof_delims known_failures output
- val success = (rc = 0 andalso failure = "")
+ val (proof, outcome) =
+ extract_proof_and_outcome res_code proof_delims known_failures output
val (message, relevant_thm_names) =
- if success then
- proof_text isar_proof debug modulus sorts ctxt
- (minimize_command, proof, internal_thm_names, th, subgoal)
- else if failure <> "" then
- (failure ^ "\n", [])
- else
- ("Unknown ATP error: " ^ output ^ ".\n", [])
+ case outcome of
+ NONE => proof_text isar_proof debug modulus sorts ctxt
+ (minimize_command, proof, internal_thm_names, th,
+ subgoal)
+ | SOME failure => (string_for_failure failure ^ "\n", [])
in
- {success = success, message = message,
+ {outcome = outcome, message = message,
relevant_thm_names = relevant_thm_names,
atp_run_time_in_msecs = atp_run_time_in_msecs, output = output,
proof = proof, internal_thm_names = internal_thm_names,
@@ -237,10 +247,9 @@
proof_delims = [("=========== Refutation ==========",
"======= End of refutation =======")],
known_failures =
- [(["Satisfiability detected", "CANNOT PROVE"],
- "The ATP problem is unprovable."),
- (["Refutation not found"],
- "The ATP failed to determine the problem's status.")],
+ [(Unprovable, "Satisfiability detected"),
+ (OutOfResources, "CANNOT PROVE"),
+ (OutOfResources, "Refutation not found")],
max_new_clauses = 60,
prefers_theory_relevant = false}
val vampire = tptp_prover "vampire" vampire_config
@@ -259,12 +268,14 @@
string_of_int (generous_to_secs timeout)),
proof_delims = [tstp_proof_delims],
known_failures =
- [(["SZS status: Satisfiable", "SZS status Satisfiable"],
- "The ATP problem is unprovable."),
- (["SZS status: ResourceOut", "SZS status ResourceOut"],
- "The ATP ran out of resources."),
- (["# Cannot determine problem status"],
- "The ATP failed to determine the problem's status.")],
+ [(Unprovable, "SZS status: Satisfiable"),
+ (Unprovable, "SZS status Satisfiable"),
+ (TimedOut, "Failure: Resource limit exceeded (time)"),
+ (TimedOut, "time limit exceeded"),
+ (OutOfResources,
+ "# Cannot determine problem status within resource limit"),
+ (OutOfResources, "SZS status: ResourceOut"),
+ (OutOfResources, "SZS status ResourceOut")],
max_new_clauses = 100,
prefers_theory_relevant = false}
val e = tptp_prover "e" e_config
@@ -298,10 +309,9 @@
string_of_int (generous_to_secs timeout)),
proof_delims = [("Here is a proof", "Formulae used in the proof")],
known_failures =
- [(["SPASS beiseite: Completion found."], "The ATP problem is unprovable."),
- (["SPASS beiseite: Ran out of time."], "The ATP timed out."),
- (["SPASS beiseite: Maximal number of loops exceeded."],
- "The ATP hit its loop limit.")],
+ [(Unprovable, "SPASS beiseite: Completion found"),
+ (TimedOut, "SPASS beiseite: Ran out of time"),
+ (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded")],
max_new_clauses = 40,
prefers_theory_relevant = true}
val spass = dfg_prover "spass" spass_config
@@ -321,15 +331,8 @@
proof_delims = #proof_delims spass_config,
known_failures =
#known_failures spass_config @
- [(["unrecognized option `-TPTP'", "Unrecognized option TPTP"],
- "Warning: Sledgehammer requires a more recent version of SPASS with \
- \support for the TPTP syntax. To install it, download and untar the \
- \package \"http://isabelle.in.tum.de/~blanchet/spass-3.7.tgz\" and add \
- \the \"spass-3.7\" directory's full path to \"" ^
- Path.implode (Path.expand (Path.appends
- (Path.variable "ISABELLE_HOME_USER" ::
- map Path.basic ["etc", "components"]))) ^
- "\" on a line of its own.")],
+ [(OldSpass, "unrecognized option `-TPTP'"),
+ (OldSpass, "Unrecognized option TPTP")],
max_new_clauses = #max_new_clauses spass_config,
prefers_theory_relevant = #prefers_theory_relevant spass_config}
val spass_tptp = tptp_prover "spass_tptp" spass_tptp_config
@@ -339,14 +342,10 @@
val systems = Synchronized.var "atp_wrapper_systems" ([]: string list);
fun get_systems () =
- let
- val (answer, rc) = bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w"
- in
- if rc <> 0 then
- error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer)
- else
- split_lines answer
- end;
+ case bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w" of
+ (answer, 0) => split_lines answer
+ | (answer, _) =>
+ error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer)
fun refresh_systems_on_tptp () =
Synchronized.change systems (fn _ => get_systems ());
@@ -357,12 +356,13 @@
fun the_system prefix =
(case get_system prefix of
- NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP")
+ NONE => error ("System " ^ quote prefix ^
+ " not available at SystemOnTPTP.")
| SOME sys => sys);
val remote_known_failures =
- [(["Remote-script could not extract proof"],
- "Error: The remote ATP proof is ill-formed.")]
+ [(TimedOut, "says Timeout"),
+ (MalformedOutput, "Remote-script could not extract proof")]
fun remote_prover_config prover_prefix args
({proof_delims, known_failures, max_new_clauses,