--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Jul 27 15:28:23 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Jul 27 17:04:09 2010 +0200
@@ -315,13 +315,13 @@
(case hard_timeout of
NONE => I
| SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
- val ({outcome, message, relevant_thm_names,
+ val ({outcome, message, used_thm_names,
atp_run_time_in_msecs = time_atp, ...}: ATP_Manager.prover_result,
time_isa) = time_limit (Mirabelle.cpu_time
(prover params (K "") (Time.fromSeconds timeout))) problem
in
case outcome of
- NONE => (message, SH_OK (time_isa, time_atp, relevant_thm_names))
+ NONE => (message, SH_OK (time_isa, time_atp, used_thm_names))
| SOME _ => (message, SH_FAIL (time_isa, time_atp))
end
handle ERROR msg => ("error: " ^ msg, SH_ERROR)
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Jul 27 15:28:23 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Jul 27 17:04:09 2010 +0200
@@ -38,7 +38,7 @@
{outcome: failure option,
message: string,
pool: string Symtab.table,
- relevant_thm_names: string list,
+ used_thm_names: string list,
atp_run_time_in_msecs: int,
output: string,
proof: string,
@@ -107,7 +107,7 @@
{outcome: failure option,
message: string,
pool: string Symtab.table,
- relevant_thm_names: string list,
+ used_thm_names: string list,
atp_run_time_in_msecs: int,
output: string,
proof: string,
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jul 27 15:28:23 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jul 27 17:04:09 2010 +0200
@@ -493,7 +493,7 @@
repair_conjecture_shape_and_theorem_names output conjecture_shape
internal_thm_names
- val (message, relevant_thm_names) =
+ val (message, used_thm_names) =
case outcome of
NONE =>
proof_text isar_proof
@@ -503,7 +503,7 @@
| SOME failure => (string_for_failure failure ^ "\n", [])
in
{outcome = outcome, message = message, pool = pool,
- relevant_thm_names = relevant_thm_names, atp_run_time_in_msecs = msecs,
+ used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs,
output = output, proof = proof, internal_thm_names = internal_thm_names,
conjecture_shape = conjecture_shape,
filtered_clauses = the_filtered_clauses}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Tue Jul 27 15:28:23 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Tue Jul 27 17:04:09 2010 +0200
@@ -23,18 +23,6 @@
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."
@@ -52,8 +40,15 @@
let
val thy = Proof.theory_of state
val num_theorems = length name_thms_pairs
- val _ = priority ("Testing " ^ string_of_int num_theorems ^
- " theorem" ^ plural_s num_theorems ^ "...")
+ val _ =
+ priority ("Testing " ^ string_of_int num_theorems ^
+ " theorem" ^ plural_s num_theorems ^
+ (if num_theorems > 0 then
+ ": " ^ space_implode " "
+ (name_thms_pairs
+ |> map fst |> sort_distinct string_ord)
+ else
+ "") ^ "...")
val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
val {context = ctxt, facts, goal} = Proof.goal state
val problem =
@@ -69,6 +64,17 @@
(* minimalization of thms *)
+fun filter_used_facts used = filter (member (op =) used o fst)
+
+fun sublinear_minimize _ [] p = p
+ | sublinear_minimize test (x :: xs) (seen, result) =
+ case test (xs @ seen) of
+ result as {outcome = NONE, proof, used_thm_names, ...}
+ : prover_result =>
+ sublinear_minimize test (filter_used_facts used_thm_names xs)
+ (filter_used_facts used_thm_names seen, result)
+ | _ => sublinear_minimize test xs (x :: seen, result)
+
fun minimize_theorems (params as {debug, atps, full_types, minimize_timeout,
isar_proof, isar_shrink_factor, ...})
i n state name_thms_pairs =
@@ -81,50 +87,39 @@
val _ =
priority ("Sledgehammer minimizer: ATP " ^ quote (the_single atps) ^
" with a time limit of " ^ string_of_int msecs ^ " ms.")
- val test_thms_fun =
+ val test_facts =
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, goal, ...} = Proof.goal state;
in
(* try prove first to check result and get used theorems *)
- (case test_thms_fun NONE name_thms_pairs of
- result as {outcome = NONE, pool, internal_thm_names, conjecture_shape,
- 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, _) => 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 m = length min_thms
- val _ = priority (cat_lines
- ["Minimized: " ^ string_of_int m ^ " theorem" ^ plural_s m] ^ ".")
- in
- (SOME min_thms,
- proof_text isar_proof
- (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
- (full_types, 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))
+ (case test_facts NONE name_thms_pairs of
+ result as {outcome = NONE, pool, proof, used_thm_names,
+ conjecture_shape, filtered_clauses, ...} =>
+ let
+ val (min_thms, {proof, internal_thm_names, ...}) =
+ sublinear_minimize (test_facts (SOME filtered_clauses))
+ (filter_used_facts used_thm_names name_thms_pairs)
+ ([], result)
+ val m = length min_thms
+ val _ = priority (cat_lines
+ ["Minimized: " ^ string_of_int m ^ " theorem" ^ plural_s m] ^ ".")
+ in
+ (SOME min_thms,
+ proof_text isar_proof
+ (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
+ (full_types, 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 ERROR msg => (NONE, "Error: " ^ msg)
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Jul 27 15:28:23 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Jul 27 17:04:09 2010 +0200
@@ -562,17 +562,18 @@
val unprefix_chained = perhaps (try (unprefix chained_prefix))
+fun used_facts thm_names =
+ extract_formula_numbers_in_atp_proof
+ #> filter (is_axiom_clause_number thm_names)
+ #> map (fn i => Vector.sub (thm_names, i - 1))
+ #> List.partition (String.isPrefix chained_prefix)
+ #>> map (unprefix chained_prefix)
+ #> pairself (sort_distinct string_ord)
+
fun metis_proof_text (full_types, minimize_command, atp_proof, thm_names, goal,
i) =
let
- val raw_lemmas =
- atp_proof |> extract_formula_numbers_in_atp_proof
- |> filter (is_axiom_clause_number thm_names)
- |> map (fn i => Vector.sub (thm_names, i - 1))
- val (chained_lemmas, other_lemmas) =
- raw_lemmas |> List.partition (String.isPrefix chained_prefix)
- |>> map (unprefix chained_prefix)
- |> pairself (sort_distinct string_ord)
+ val (chained_lemmas, other_lemmas) = used_facts thm_names atp_proof
val lemmas = other_lemmas @ chained_lemmas
val n = Logic.count_prems (prop_of goal)
in