# HG changeset patch # User blanchet # Date 1280243049 -7200 # Node ID b30c3c2e1030a9e464a8eb4db4fdeda2897c0129 # Parent 81c23d286f0c267a784c74f4e33c81a36d42546f implemented "sublinear" minimization algorithm diff -r 81c23d286f0c -r b30c3c2e1030 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- 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) diff -r 81c23d286f0c -r b30c3c2e1030 src/HOL/Tools/ATP_Manager/atp_manager.ML --- 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, diff -r 81c23d286f0c -r b30c3c2e1030 src/HOL/Tools/ATP_Manager/atp_systems.ML --- 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} diff -r 81c23d286f0c -r b30c3c2e1030 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML --- 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 diff -r 81c23d286f0c -r b30c3c2e1030 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- 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