--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Apr 23 16:59:48 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,128 +0,0 @@
-(* 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.
-*)
-
-signature ATP_MINIMAL =
-sig
- type params = ATP_Manager.params
- type prover = ATP_Manager.prover
- type prover_result = ATP_Manager.prover_result
-
- val minimize_theorems :
- params -> prover -> string -> int -> Proof.state -> (string * thm list) list
- -> (string * thm list) list option * string
-end;
-
-structure ATP_Minimal : ATP_MINIMAL =
-struct
-
-open Sledgehammer_Util
-open Sledgehammer_Fact_Preprocessor
-open Sledgehammer_Proof_Reconstruct
-open ATP_Manager
-
-(* Linear minimization algorithm *)
-
-fun linear_minimize test s =
- let
- fun aux [] p = p
- | aux (x :: xs) (needed, result) =
- case test (xs @ needed) of
- SOME result => aux xs (needed, result)
- | NONE => aux xs (x :: needed, result)
- in aux s end
-
-
-(* 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 =
- let
- val num_theorems = length name_thms_pairs
- val _ = priority ("Testing " ^ string_of_int num_theorems ^
- " theorem" ^ plural_s num_theorems ^ "...")
- val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
- val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
- val {context = ctxt, facts, goal} = Proof.goal state
- val problem =
- {subgoal = subgoal, goal = (ctxt, (facts, goal)),
- relevance_override = {add = [], del = [], only = false},
- axiom_clauses = SOME axclauses,
- filtered_clauses = SOME (the_default axclauses filtered_clauses)}
- in
- prover params (K "") timeout problem
- |> tap (priority o string_for_outcome o #outcome)
- end
-
-(* minimalization of thms *)
-
-fun minimize_theorems (params as {debug, minimize_timeout, isar_proof, modulus,
- sorts, ...})
- prover atp_name i state name_thms_pairs =
- let
- val msecs = Time.toMilliseconds minimize_timeout
- val n = length name_thms_pairs
- val _ =
- priority ("Sledgehammer minimizer: ATP " ^ quote atp_name ^
- " with a time limit of " ^ string_of_int msecs ^ " ms.")
- val test_thms_fun =
- sledgehammer_test_theorems params prover minimize_timeout i state
- fun test_thms filtered thms =
- case test_thms_fun filtered thms of
- (result as {outcome = NONE, ...}) => SOME result
- | _ => NONE
-
- val {context = ctxt, facts, goal} = Proof.goal state;
- val n = Logic.count_prems (prop_of goal)
- in
- (* try prove first to check result and get used theorems *)
- (case test_thms_fun NONE name_thms_pairs of
- result as {outcome = NONE, internal_thm_names, filtered_clauses, ...} =>
- let
- val used = internal_thm_names |> Vector.foldr (op ::) []
- |> sort_distinct string_ord
- val to_use =
- if length used < length name_thms_pairs then
- filter (fn (name1, _) => List.exists (curry (op =) name1) used)
- name_thms_pairs
- else name_thms_pairs
- val (min_thms, {proof, internal_thm_names, ...}) =
- linear_minimize (test_thms (SOME filtered_clauses)) to_use
- ([], result)
- val n = length min_thms
- val _ = priority (cat_lines
- ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ ".")
- in
- (SOME min_thms,
- proof_text isar_proof debug modulus sorts ctxt
- (K "", proof, internal_thm_names, goal, i) |> fst)
- end
- | {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\").")
- | {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\").")
- | {message, ...} => (NONE, "ATP error: " ^ message))
- handle Sledgehammer_HOL_Clause.TRIVIAL =>
- (SOME [], metis_line i n [])
- | ERROR msg => (NONE, "Error: " ^ msg)
- end
-
-end;