# HG changeset patch # User smolkas # Date 1360878562 -3600 # Node ID 76d68444cd590b30d961ebf9543e8ae7b176c9ab # Parent 1edc2cc25f1988d914ed4a7fbbc31bd551b27e67 renamed sledgehammer_shrink to sledgehammer_compress diff -r 1edc2cc25f19 -r 76d68444cd59 src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Thu Feb 14 22:49:22 2013 +0100 +++ b/src/Doc/Sledgehammer/document/root.tex Thu Feb 14 22:49:22 2013 +0100 @@ -369,7 +369,7 @@ \item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies that Isar proofs should be generated, instead of one-liner \textit{metis} or \textit{smt} proofs. The length of the Isar proofs can be controlled by setting -\textit{isar\_shrink} (\S\ref{output-format}). +\textit{isar\_compress} (\S\ref{output-format}). \item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the provers' time limit. It is set to 30 seconds, but since Sledgehammer runs @@ -508,7 +508,7 @@ is highly experimental. Work on a new implementation has begun. There is a large body of research into transforming resolution proofs into natural deduction proofs (such as Isar proofs), which we hope to leverage. In the meantime, a workaround is to -set the \textit{isar\_shrink} option (\S\ref{output-format}) to a larger +set the \textit{isar\_compress} option (\S\ref{output-format}) to a larger value or to try several provers and keep the nicest-looking proof. \point{How can I tell whether a suggested proof is sound?} @@ -1302,7 +1302,7 @@ fails; however, they are usually faster and sometimes more robust than \textit{metis} proofs. -\opdefault{isar\_shrink}{int}{\upshape 10} +\opdefault{isar\_compress}{int}{\upshape 10} Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs} is enabled. A value of $n$ indicates that each Isar proof step should correspond to a group of up to $n$ consecutive proof steps in the ATP proof. diff -r 1edc2cc25f19 -r 76d68444cd59 src/HOL/Metis_Examples/Big_O.thy --- a/src/HOL/Metis_Examples/Big_O.thy Thu Feb 14 22:49:22 2013 +0100 +++ b/src/HOL/Metis_Examples/Big_O.thy Thu Feb 14 22:49:22 2013 +0100 @@ -29,7 +29,7 @@ (*** Now various verions with an increasing shrink factor ***) -sledgehammer_params [isar_proofs, isar_shrink = 1] +sledgehammer_params [isar_proofs, isar_compress = 1] lemma "(\c\'a\linordered_idom. @@ -60,7 +60,7 @@ thus "\h x\ \ \c\ * \f x\" by (metis F4) qed -sledgehammer_params [isar_proofs, isar_shrink = 2] +sledgehammer_params [isar_proofs, isar_compress = 2] lemma "(\c\'a\linordered_idom. @@ -83,7 +83,7 @@ thus "\h x\ \ \c\ * \f x\" by (metis F2) qed -sledgehammer_params [isar_proofs, isar_shrink = 3] +sledgehammer_params [isar_proofs, isar_compress = 3] lemma "(\c\'a\linordered_idom. @@ -103,7 +103,7 @@ thus "\h x\ \ \c\ * \f x\" by (metis A1 abs_ge_zero) qed -sledgehammer_params [isar_proofs, isar_shrink = 4] +sledgehammer_params [isar_proofs, isar_compress = 4] lemma "(\c\'a\linordered_idom. @@ -123,7 +123,7 @@ thus "\h x\ \ \c\ * \f x\" by (metis abs_mult) qed -sledgehammer_params [isar_proofs, isar_shrink = 1] +sledgehammer_params [isar_proofs, isar_compress = 1] lemma bigo_alt_def: "O(f) = {h. \c. (0 < c \ (\x. abs (h x) <= c * abs (f x)))}" by (auto simp add: bigo_def bigo_pos_const) diff -r 1edc2cc25f19 -r 76d68444cd59 src/HOL/Metis_Examples/Sets.thy --- a/src/HOL/Metis_Examples/Sets.thy Thu Feb 14 22:49:22 2013 +0100 +++ b/src/HOL/Metis_Examples/Sets.thy Thu Feb 14 22:49:22 2013 +0100 @@ -21,7 +21,7 @@ lemma "P(n::nat) ==> ~P(0) ==> n ~= 0" by metis -sledgehammer_params [isar_proofs, isar_shrink = 1] +sledgehammer_params [isar_proofs, isar_compress = 1] (*multiple versions of this example*) lemma (*equal_union: *) @@ -70,7 +70,7 @@ ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by metis qed -sledgehammer_params [isar_proofs, isar_shrink = 2] +sledgehammer_params [isar_proofs, isar_compress = 2] lemma (*equal_union: *) "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" @@ -107,7 +107,7 @@ ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by metis qed -sledgehammer_params [isar_proofs, isar_shrink = 3] +sledgehammer_params [isar_proofs, isar_compress = 3] lemma (*equal_union: *) "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" @@ -124,7 +124,7 @@ ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis Un_commute Un_upper2) qed -sledgehammer_params [isar_proofs, isar_shrink = 4] +sledgehammer_params [isar_proofs, isar_compress = 4] lemma (*equal_union: *) "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" @@ -140,7 +140,7 @@ ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis Un_subset_iff Un_upper2) qed -sledgehammer_params [isar_proofs, isar_shrink = 1] +sledgehammer_params [isar_proofs, isar_compress = 1] lemma (*equal_union: *) "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" diff -r 1edc2cc25f19 -r 76d68444cd59 src/HOL/Metis_Examples/Trans_Closure.thy --- a/src/HOL/Metis_Examples/Trans_Closure.thy Thu Feb 14 22:49:22 2013 +0100 +++ b/src/HOL/Metis_Examples/Trans_Closure.thy Thu Feb 14 22:49:22 2013 +0100 @@ -44,7 +44,7 @@ lemma "\f c = Intg x; \y. f b = Intg y \ y \ x; (a, b) \ R\<^sup>*; (b,c) \ R\<^sup>*\ \ \c. (b, c) \ R \ (a, c) \ R\<^sup>*" -(* sledgehammer [isar_proofs, isar_shrink = 2] *) +(* sledgehammer [isar_proofs, isar_compress = 2] *) proof - assume A1: "f c = Intg x" assume A2: "\y. f b = Intg y \ y \ x" diff -r 1edc2cc25f19 -r 76d68444cd59 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Thu Feb 14 22:49:22 2013 +0100 +++ b/src/HOL/Sledgehammer.thy Thu Feb 14 22:49:22 2013 +0100 @@ -17,7 +17,7 @@ ML_file "Tools/Sledgehammer/sledgehammer_proof.ML" ML_file "Tools/Sledgehammer/sledgehammer_annotate.ML" ML_file "Tools/Sledgehammer/sledgehammer_preplay.ML" -ML_file "Tools/Sledgehammer/sledgehammer_shrink.ML" +ML_file "Tools/Sledgehammer/sledgehammer_compress.ML" ML_file "Tools/Sledgehammer/sledgehammer_reconstruct.ML" ML_file "Tools/Sledgehammer/sledgehammer_provers.ML" ML_file "Tools/Sledgehammer/sledgehammer_minimize.ML" diff -r 1edc2cc25f19 -r 76d68444cd59 src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Thu Feb 14 22:49:22 2013 +0100 @@ -0,0 +1,252 @@ +(* Title: HOL/Tools/Sledgehammer/sledgehammer_compress.ML + Author: Jasmin Blanchette, TU Muenchen + Author: Steffen Juilf Smolka, TU Muenchen + +Compression of reconstructed isar proofs. +*) + +signature SLEDGEHAMMER_COMPRESS = +sig + type isar_step = Sledgehammer_Proof.isar_step + type preplay_time = Sledgehammer_Preplay.preplay_time + val compress_proof : + bool -> Proof.context -> string -> string -> bool -> Time.time option + -> real -> isar_step list -> isar_step list * (bool * preplay_time) +end + +structure Sledgehammer_Compress : SLEDGEHAMMER_COMPRESS = +struct + +open Sledgehammer_Util +open Sledgehammer_Proof +open Sledgehammer_Preplay + +(* Parameters *) +val merge_timeout_slack = 1.2 + +(* Data structures, orders *) +val label_ord = prod_ord int_ord fast_string_ord o pairself swap +structure Label_Table = Table( + type key = label + val ord = label_ord) + +(* clean vector interface *) +fun get i v = Vector.sub (v, i) +fun replace x i v = Vector.update (v, i, x) +fun update f i v = replace (get i v |> f) i v +fun v_map_index f v = Vector.foldr (op::) nil v |> map_index f |> Vector.fromList +fun v_fold_index f v s = + Vector.foldl (fn (x, (i, s)) => (i+1, f (i, x) s)) (0, s) v |> snd + +(* Queue interface to table *) +fun pop tab key = + let val v = hd (Inttab.lookup_list tab key) in + (v, Inttab.remove_list (op =) (key, v) tab) + end +fun pop_max tab = pop tab (the (Inttab.max_key tab)) +fun add_list tab xs = fold (Inttab.insert_list (op =)) xs tab + +(* Main function for compresing proofs *) +fun compress_proof debug ctxt type_enc lam_trans preplay preplay_timeout + isar_compress proof = + let + (* 60 seconds seems like a good interpreation of "no timeout" *) + val preplay_timeout = preplay_timeout |> the_default (seconds 60.0) + + (* handle metis preplay fail *) + local + open Unsynchronized + val metis_fail = ref false + in + fun handle_metis_fail try_metis () = + try_metis () handle exn => + (if Exn.is_interrupt exn orelse debug then reraise exn + else metis_fail := true; some_preplay_time) + fun get_time lazy_time = + if !metis_fail andalso not (Lazy.is_finished lazy_time) + then some_preplay_time + else Lazy.force lazy_time + val metis_fail = fn () => !metis_fail + end + + (* compress proof on top level - do not compress case splits *) + fun compress_top_level on_top_level ctxt proof = + let + (* proof vector *) + val proof_vect = proof |> map SOME |> Vector.fromList + val n = Vector.length proof_vect + val n_metis = metis_steps_top_level proof + val target_n_metis = Real.fromInt n_metis / isar_compress |> Real.round + + (* table for mapping from (top-level-)label to proof position *) + fun update_table (i, Assume (l, _)) = Label_Table.update_new (l, i) + | update_table (i, Obtain (_, _, l, _, _)) = Label_Table.update_new (l, i) + | update_table (i, Prove (_, l, _, _)) = Label_Table.update_new (l, i) + | update_table _ = I + val label_index_table = fold_index update_table proof Label_Table.empty + val lookup_indices = map_filter (Label_Table.lookup label_index_table) + + (* proof references *) + fun refs (Obtain (_, _, _, _, By_Metis (lfs, _))) = lookup_indices lfs + | refs (Prove (_, _, _, By_Metis (lfs, _))) = lookup_indices lfs + | refs (Prove (_, _, _, Case_Split (cases, (lfs, _)))) = + lookup_indices lfs @ maps (maps refs) cases + | refs (Prove (_, _, _, Subblock proof)) = maps refs proof + | refs _ = [] + val refed_by_vect = + Vector.tabulate (n, (fn _ => [])) + |> fold_index (fn (i, step) => fold (update (cons i)) (refs step)) proof + |> Vector.map rev (* after rev, indices are sorted in ascending order *) + + (* candidates for elimination, use table as priority queue (greedy + algorithm) *) + fun add_if_cand proof_vect (i, [j]) = + (case (the (get i proof_vect), the (get j proof_vect)) of + (Prove (_, _, t, By_Metis _), Prove (_, _, _, By_Metis _)) => + cons (Term.size_of_term t, i) + | (Prove (_, _, t, By_Metis _), Obtain (_, _, _, _, By_Metis _)) => + cons (Term.size_of_term t, i) + | _ => I) + | add_if_cand _ _ = I + val cand_tab = + v_fold_index (add_if_cand proof_vect) refed_by_vect [] + |> Inttab.make_list + + (* cache metis preplay times in lazy time vector *) + val metis_time = + v_map_index + (if not preplay then K (zero_preplay_time) #> Lazy.value + else + apsnd the (* step *) + #> apfst (fn i => try (get (i-1) #> the) proof_vect) (* succedent *) + #> try_metis debug type_enc lam_trans ctxt preplay_timeout + #> handle_metis_fail + #> Lazy.lazy) + proof_vect + + fun sum_up_time lazy_time_vector = + Vector.foldl + (apfst get_time #> uncurry add_preplay_time) + zero_preplay_time lazy_time_vector + + (* Merging *) + fun merge (Prove (_, label1, _, By_Metis (lfs1, gfs1))) step2 = + let + val (step_constructor, lfs2, gfs2) = + (case step2 of + (Prove (qs2, label2, t, By_Metis (lfs2, gfs2))) => + (fn by => Prove (qs2, label2, t, by), lfs2, gfs2) + | (Obtain (qs2, xs, label2, t, By_Metis (lfs2, gfs2))) => + (fn by => Obtain (qs2, xs, label2, t, by), lfs2, gfs2) + | _ => error "sledgehammer_compress: unmergeable Isar steps" ) + val lfs = remove (op =) label1 lfs2 |> union (op =) lfs1 + val gfs = union (op =) gfs1 gfs2 + in step_constructor (By_Metis (lfs, gfs)) end + | merge _ _ = error "sledgehammer_compress: unmergeable Isar steps" + + fun try_merge metis_time (s1, i) (s2, j) = + if not preplay then (merge s1 s2 |> SOME, metis_time) + else + (case get i metis_time |> Lazy.force of + (true, _) => (NONE, metis_time) + | (_, t1) => + (case get j metis_time |> Lazy.force of + (true, _) => (NONE, metis_time) + | (_, t2) => + let + val s12 = merge s1 s2 + val timeout = time_mult merge_timeout_slack (Time.+(t1, t2)) + in + case try_metis_quietly debug type_enc lam_trans ctxt timeout + (NONE, s12) () of + (true, _) => (NONE, metis_time) + | exact_time => + (SOME s12, metis_time + |> replace (zero_preplay_time |> Lazy.value) i + |> replace (Lazy.value exact_time) j) + + end)) + + fun merge_steps metis_time proof_vect refed_by cand_tab n' n_metis' = + if Inttab.is_empty cand_tab + orelse n_metis' <= target_n_metis + orelse (on_top_level andalso n'<3) + then + (Vector.foldr + (fn (NONE, proof) => proof | (SOME s, proof) => s :: proof) + [] proof_vect, + sum_up_time metis_time) + else + let + val (i, cand_tab) = pop_max cand_tab + val j = get i refed_by |> the_single + val s1 = get i proof_vect |> the + val s2 = get j proof_vect |> the + in + case try_merge metis_time (s1, i) (s2, j) of + (NONE, metis_time) => + merge_steps metis_time proof_vect refed_by cand_tab n' n_metis' + | (s, metis_time) => + let + val refs = refs s1 + val refed_by = refed_by |> fold + (update (Ord_List.remove int_ord i #> Ord_List.insert int_ord j)) refs + val new_candidates = + fold (add_if_cand proof_vect) + (map (fn i => (i, get i refed_by)) refs) [] + val cand_tab = add_list cand_tab new_candidates + val proof_vect = proof_vect |> replace NONE i |> replace s j + in + merge_steps metis_time proof_vect refed_by cand_tab (n' - 1) + (n_metis' - 1) + end + end + in + merge_steps metis_time proof_vect refed_by_vect cand_tab n n_metis + end + + fun do_proof on_top_level ctxt proof = + let + (* Enrich context with top-level facts *) + val thy = Proof_Context.theory_of ctxt + (* TODO: add Skolem variables to context? *) + fun enrich_with_fact l t = + Proof_Context.put_thms false + (string_for_label l, SOME [Skip_Proof.make_thm thy t]) + fun enrich_with_step (Assume (l, t)) = enrich_with_fact l t + | enrich_with_step (Obtain (_, _, l, t, _)) = enrich_with_fact l t + | enrich_with_step (Prove (_, l, t, _)) = enrich_with_fact l t + | enrich_with_step _ = I + val rich_ctxt = fold enrich_with_step proof ctxt + + (* compress subproofs (case_splits and subblocks) and top-levl *) + val ((proof, top_level_time), lower_level_time) = + proof |> do_subproof rich_ctxt + |>> compress_top_level on_top_level rich_ctxt + in + (proof, add_preplay_time lower_level_time top_level_time) + end + + and do_subproof ctxt proof = + let + fun compress_each_and_collect_time compress candidates = + let fun f_m cand time = compress cand ||> add_preplay_time time + in fold_map f_m candidates zero_preplay_time end + val compress_subproof = + compress_each_and_collect_time (do_proof false ctxt) + fun compress (Prove (qs, l, t, Case_Split (cases, facts))) = + let val (cases, time) = compress_subproof cases + in (Prove (qs, l, t, Case_Split (cases, facts)), time) end + | compress (Prove (qs, l, t, Subblock proof)) = + let val ([proof], time) = compress_subproof [proof] + in (Prove (qs, l, t, Subblock proof), time) end + | compress step = (step, zero_preplay_time) + in + compress_each_and_collect_time compress proof + end + in + do_proof true ctxt proof + |> apsnd (pair (metis_fail ())) + end + +end diff -r 1edc2cc25f19 -r 76d68444cd59 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Feb 14 22:49:22 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Feb 14 22:49:22 2013 +0100 @@ -95,7 +95,7 @@ ("max_mono_iters", "smart"), ("max_new_mono_instances", "smart"), ("isar_proofs", "false"), - ("isar_shrink", "10"), + ("isar_compress", "10"), ("slice", "true"), ("minimize", "smart"), ("preplay_timeout", "3")] @@ -119,7 +119,7 @@ val params_for_minimize = ["debug", "verbose", "overlord", "type_enc", "strict", "lam_trans", "uncurried_aliases", "max_mono_iters", "max_new_mono_instances", - "learn", "isar_proofs", "isar_shrink", "timeout", "preplay_timeout"] + "learn", "isar_proofs", "isar_compress", "timeout", "preplay_timeout"] val property_dependent_params = ["provers", "timeout"] @@ -314,7 +314,7 @@ val max_new_mono_instances = lookup_option lookup_int "max_new_mono_instances" val isar_proofs = lookup_bool "isar_proofs" - val isar_shrink = Real.max (1.0, lookup_real "isar_shrink") + val isar_compress = Real.max (1.0, lookup_real "isar_compress") val slice = mode <> Auto_Try andalso lookup_bool "slice" val minimize = if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize" @@ -330,7 +330,7 @@ learn = learn, fact_filter = fact_filter, max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, - isar_shrink = isar_shrink, slice = slice, minimize = minimize, + isar_compress = isar_compress, slice = slice, minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} end diff -r 1edc2cc25f19 -r 76d68444cd59 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Feb 14 22:49:22 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Feb 14 22:49:22 2013 +0100 @@ -54,7 +54,7 @@ fun test_facts ({debug, verbose, overlord, provers, max_mono_iters, max_new_mono_instances, type_enc, strict, lam_trans, - uncurried_aliases, isar_proofs, isar_shrink, + uncurried_aliases, isar_proofs, isar_compress, preplay_timeout, ...} : params) silent (prover : prover) timeout i n state facts = let @@ -76,7 +76,7 @@ learn = false, fact_filter = NONE, max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, - isar_proofs = isar_proofs, isar_shrink = isar_shrink, + isar_proofs = isar_proofs, isar_compress = isar_compress, slice = false, minimize = SOME false, timeout = timeout, preplay_timeout = preplay_timeout, expect = ""} val problem = @@ -243,7 +243,7 @@ ({debug, verbose, overlord, blocking, provers, type_enc, strict, lam_trans, uncurried_aliases, learn, fact_filter, max_facts, fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proofs, - isar_shrink, slice, minimize, timeout, preplay_timeout, expect} + isar_compress, slice, minimize, timeout, preplay_timeout, expect} : params) = let fun lookup_override name default_value = @@ -261,7 +261,7 @@ learn = learn, fact_filter = fact_filter, max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, - isar_shrink = isar_shrink, slice = slice, minimize = minimize, + isar_compress = isar_compress, slice = slice, minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} end diff -r 1edc2cc25f19 -r 76d68444cd59 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu Feb 14 22:49:22 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu Feb 14 22:49:22 2013 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/Tools/Sledgehammer/sledgehammer_shrink.ML +(* Title: HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Author: Jasmin Blanchette, TU Muenchen Author: Steffen Juilf Smolka, TU Muenchen diff -r 1edc2cc25f19 -r 76d68444cd59 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Feb 14 22:49:22 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Feb 14 22:49:22 2013 +0100 @@ -35,7 +35,7 @@ max_mono_iters : int option, max_new_mono_instances : int option, isar_proofs : bool, - isar_shrink : real, + isar_compress : real, slice : bool, minimize : bool option, timeout : Time.time option, @@ -322,7 +322,7 @@ max_mono_iters : int option, max_new_mono_instances : int option, isar_proofs : bool, - isar_shrink : real, + isar_compress : real, slice : bool, minimize : bool option, timeout : Time.time option, @@ -635,7 +635,7 @@ best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config) (params as {debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, fact_filter, max_facts, max_mono_iters, - max_new_mono_instances, isar_proofs, isar_shrink, + max_new_mono_instances, isar_proofs, isar_compress, slice, timeout, preplay_timeout, ...}) minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) = @@ -898,7 +898,7 @@ else () val isar_params = - (debug, verbose, preplay_timeout, isar_shrink, + (debug, verbose, preplay_timeout, isar_compress, pool, fact_names, sym_tab, atp_proof, goal) val one_line_params = (preplay, proof_banner mode name, used_facts, diff -r 1edc2cc25f19 -r 76d68444cd59 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Feb 14 22:49:22 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Feb 14 22:49:22 2013 +0100 @@ -54,7 +54,7 @@ open Sledgehammer_Util open Sledgehammer_Proof open Sledgehammer_Annotate -open Sledgehammer_Shrink +open Sledgehammer_Compress structure String_Redirect = ATP_Proof_Redirect( type key = step_name @@ -639,7 +639,7 @@ * (string * stature) list vector * int Symtab.table * string proof * thm fun isar_proof_text ctxt isar_proofs - (debug, verbose, preplay_timeout, isar_shrink, pool, fact_names, sym_tab, + (debug, verbose, preplay_timeout, isar_compress, pool, fact_names, sym_tab, atp_proof, goal) (one_line_params as (_, _, _, _, subgoal, subgoal_count)) = let @@ -757,12 +757,12 @@ |> redirect_graph axioms tainted bot |> map (isar_step_of_direct_inf true) |> append assms - |> (if not preplay andalso isar_shrink <= 1.0 then + |> (if not preplay andalso isar_compress <= 1.0 then rpair (false, (true, seconds 0.0)) else - shrink_proof debug ctxt type_enc lam_trans preplay + compress_proof debug ctxt type_enc lam_trans preplay preplay_timeout - (if isar_proofs then isar_shrink else 1000.0)) + (if isar_proofs then isar_compress else 1000.0)) (* |>> reorder_proof_to_minimize_jumps (* ? *) *) |>> chain_direct_proof |>> kill_useless_labels_in_proof diff -r 1edc2cc25f19 -r 76d68444cd59 src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Thu Feb 14 22:49:22 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,252 +0,0 @@ -(* Title: HOL/Tools/Sledgehammer/sledgehammer_shrink.ML - Author: Jasmin Blanchette, TU Muenchen - Author: Steffen Juilf Smolka, TU Muenchen - -Shrinking of reconstructed isar proofs. -*) - -signature SLEDGEHAMMER_SHRINK = -sig - type isar_step = Sledgehammer_Proof.isar_step - type preplay_time = Sledgehammer_Preplay.preplay_time - val shrink_proof : - bool -> Proof.context -> string -> string -> bool -> Time.time option - -> real -> isar_step list -> isar_step list * (bool * preplay_time) -end - -structure Sledgehammer_Shrink : SLEDGEHAMMER_SHRINK = -struct - -open Sledgehammer_Util -open Sledgehammer_Proof -open Sledgehammer_Preplay - -(* Parameters *) -val merge_timeout_slack = 1.2 - -(* Data structures, orders *) -val label_ord = prod_ord int_ord fast_string_ord o pairself swap -structure Label_Table = Table( - type key = label - val ord = label_ord) - -(* clean vector interface *) -fun get i v = Vector.sub (v, i) -fun replace x i v = Vector.update (v, i, x) -fun update f i v = replace (get i v |> f) i v -fun v_map_index f v = Vector.foldr (op::) nil v |> map_index f |> Vector.fromList -fun v_fold_index f v s = - Vector.foldl (fn (x, (i, s)) => (i+1, f (i, x) s)) (0, s) v |> snd - -(* Queue interface to table *) -fun pop tab key = - let val v = hd (Inttab.lookup_list tab key) in - (v, Inttab.remove_list (op =) (key, v) tab) - end -fun pop_max tab = pop tab (the (Inttab.max_key tab)) -fun add_list tab xs = fold (Inttab.insert_list (op =)) xs tab - -(* Main function for shrinking proofs *) -fun shrink_proof debug ctxt type_enc lam_trans preplay preplay_timeout - isar_shrink proof = - let - (* 60 seconds seems like a good interpreation of "no timeout" *) - val preplay_timeout = preplay_timeout |> the_default (seconds 60.0) - - (* handle metis preplay fail *) - local - open Unsynchronized - val metis_fail = ref false - in - fun handle_metis_fail try_metis () = - try_metis () handle exn => - (if Exn.is_interrupt exn orelse debug then reraise exn - else metis_fail := true; some_preplay_time) - fun get_time lazy_time = - if !metis_fail andalso not (Lazy.is_finished lazy_time) - then some_preplay_time - else Lazy.force lazy_time - val metis_fail = fn () => !metis_fail - end - - (* Shrink proof on top level - do not shrink case splits *) - fun shrink_top_level on_top_level ctxt proof = - let - (* proof vector *) - val proof_vect = proof |> map SOME |> Vector.fromList - val n = Vector.length proof_vect - val n_metis = metis_steps_top_level proof - val target_n_metis = Real.fromInt n_metis / isar_shrink |> Real.round - - (* table for mapping from (top-level-)label to proof position *) - fun update_table (i, Assume (l, _)) = Label_Table.update_new (l, i) - | update_table (i, Obtain (_, _, l, _, _)) = Label_Table.update_new (l, i) - | update_table (i, Prove (_, l, _, _)) = Label_Table.update_new (l, i) - | update_table _ = I - val label_index_table = fold_index update_table proof Label_Table.empty - val lookup_indices = map_filter (Label_Table.lookup label_index_table) - - (* proof references *) - fun refs (Obtain (_, _, _, _, By_Metis (lfs, _))) = lookup_indices lfs - | refs (Prove (_, _, _, By_Metis (lfs, _))) = lookup_indices lfs - | refs (Prove (_, _, _, Case_Split (cases, (lfs, _)))) = - lookup_indices lfs @ maps (maps refs) cases - | refs (Prove (_, _, _, Subblock proof)) = maps refs proof - | refs _ = [] - val refed_by_vect = - Vector.tabulate (n, (fn _ => [])) - |> fold_index (fn (i, step) => fold (update (cons i)) (refs step)) proof - |> Vector.map rev (* after rev, indices are sorted in ascending order *) - - (* candidates for elimination, use table as priority queue (greedy - algorithm) *) - fun add_if_cand proof_vect (i, [j]) = - (case (the (get i proof_vect), the (get j proof_vect)) of - (Prove (_, _, t, By_Metis _), Prove (_, _, _, By_Metis _)) => - cons (Term.size_of_term t, i) - | (Prove (_, _, t, By_Metis _), Obtain (_, _, _, _, By_Metis _)) => - cons (Term.size_of_term t, i) - | _ => I) - | add_if_cand _ _ = I - val cand_tab = - v_fold_index (add_if_cand proof_vect) refed_by_vect [] - |> Inttab.make_list - - (* cache metis preplay times in lazy time vector *) - val metis_time = - v_map_index - (if not preplay then K (zero_preplay_time) #> Lazy.value - else - apsnd the (* step *) - #> apfst (fn i => try (get (i-1) #> the) proof_vect) (* succedent *) - #> try_metis debug type_enc lam_trans ctxt preplay_timeout - #> handle_metis_fail - #> Lazy.lazy) - proof_vect - - fun sum_up_time lazy_time_vector = - Vector.foldl - (apfst get_time #> uncurry add_preplay_time) - zero_preplay_time lazy_time_vector - - (* Merging *) - fun merge (Prove (_, label1, _, By_Metis (lfs1, gfs1))) step2 = - let - val (step_constructor, lfs2, gfs2) = - (case step2 of - (Prove (qs2, label2, t, By_Metis (lfs2, gfs2))) => - (fn by => Prove (qs2, label2, t, by), lfs2, gfs2) - | (Obtain (qs2, xs, label2, t, By_Metis (lfs2, gfs2))) => - (fn by => Obtain (qs2, xs, label2, t, by), lfs2, gfs2) - | _ => error "sledgehammer_shrink: unmergeable Isar steps" ) - val lfs = remove (op =) label1 lfs2 |> union (op =) lfs1 - val gfs = union (op =) gfs1 gfs2 - in step_constructor (By_Metis (lfs, gfs)) end - | merge _ _ = error "sledgehammer_shrink: unmergeable Isar steps" - - fun try_merge metis_time (s1, i) (s2, j) = - if not preplay then (merge s1 s2 |> SOME, metis_time) - else - (case get i metis_time |> Lazy.force of - (true, _) => (NONE, metis_time) - | (_, t1) => - (case get j metis_time |> Lazy.force of - (true, _) => (NONE, metis_time) - | (_, t2) => - let - val s12 = merge s1 s2 - val timeout = time_mult merge_timeout_slack (Time.+(t1, t2)) - in - case try_metis_quietly debug type_enc lam_trans ctxt timeout - (NONE, s12) () of - (true, _) => (NONE, metis_time) - | exact_time => - (SOME s12, metis_time - |> replace (zero_preplay_time |> Lazy.value) i - |> replace (Lazy.value exact_time) j) - - end)) - - fun merge_steps metis_time proof_vect refed_by cand_tab n' n_metis' = - if Inttab.is_empty cand_tab - orelse n_metis' <= target_n_metis - orelse (on_top_level andalso n'<3) - then - (Vector.foldr - (fn (NONE, proof) => proof | (SOME s, proof) => s :: proof) - [] proof_vect, - sum_up_time metis_time) - else - let - val (i, cand_tab) = pop_max cand_tab - val j = get i refed_by |> the_single - val s1 = get i proof_vect |> the - val s2 = get j proof_vect |> the - in - case try_merge metis_time (s1, i) (s2, j) of - (NONE, metis_time) => - merge_steps metis_time proof_vect refed_by cand_tab n' n_metis' - | (s, metis_time) => - let - val refs = refs s1 - val refed_by = refed_by |> fold - (update (Ord_List.remove int_ord i #> Ord_List.insert int_ord j)) refs - val new_candidates = - fold (add_if_cand proof_vect) - (map (fn i => (i, get i refed_by)) refs) [] - val cand_tab = add_list cand_tab new_candidates - val proof_vect = proof_vect |> replace NONE i |> replace s j - in - merge_steps metis_time proof_vect refed_by cand_tab (n' - 1) - (n_metis' - 1) - end - end - in - merge_steps metis_time proof_vect refed_by_vect cand_tab n n_metis - end - - fun do_proof on_top_level ctxt proof = - let - (* Enrich context with top-level facts *) - val thy = Proof_Context.theory_of ctxt - (* TODO: add Skolem variables to context? *) - fun enrich_with_fact l t = - Proof_Context.put_thms false - (string_for_label l, SOME [Skip_Proof.make_thm thy t]) - fun enrich_with_step (Assume (l, t)) = enrich_with_fact l t - | enrich_with_step (Obtain (_, _, l, t, _)) = enrich_with_fact l t - | enrich_with_step (Prove (_, l, t, _)) = enrich_with_fact l t - | enrich_with_step _ = I - val rich_ctxt = fold enrich_with_step proof ctxt - - (* Shrink subproofs (case_splits and subblocks) and top-levl *) - val ((proof, top_level_time), lower_level_time) = - proof |> do_subproof rich_ctxt - |>> shrink_top_level on_top_level rich_ctxt - in - (proof, add_preplay_time lower_level_time top_level_time) - end - - and do_subproof ctxt proof = - let - fun shrink_each_and_collect_time shrink candidates = - let fun f_m cand time = shrink cand ||> add_preplay_time time - in fold_map f_m candidates zero_preplay_time end - val shrink_subproof = - shrink_each_and_collect_time (do_proof false ctxt) - fun shrink (Prove (qs, l, t, Case_Split (cases, facts))) = - let val (cases, time) = shrink_subproof cases - in (Prove (qs, l, t, Case_Split (cases, facts)), time) end - | shrink (Prove (qs, l, t, Subblock proof)) = - let val ([proof], time) = shrink_subproof [proof] - in (Prove (qs, l, t, Subblock proof), time) end - | shrink step = (step, zero_preplay_time) - in - shrink_each_and_collect_time shrink proof - end - in - do_proof true ctxt proof - |> apsnd (pair (metis_fail ())) - end - -end