# HG changeset patch # User blanchet # Date 1344943259 -7200 # Node ID 9152e66f98da8f786ee1ad0259feaa44133fd27a # Parent e653853365316bfc906a318b40bc5e86eca05765 be less aggressive at kicking out chained facts diff -r e65385336531 -r 9152e66f98da src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Aug 14 12:54:26 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Aug 14 13:20:59 2012 +0200 @@ -128,10 +128,11 @@ case test timeout (xs @ seen) of result as {outcome = NONE, used_facts, run_time, ...} : prover_result => - min (new_timeout timeout run_time) (filter_used_facts used_facts xs) - (filter_used_facts used_facts seen, result) + min (new_timeout timeout run_time) + (filter_used_facts true used_facts xs) + (filter_used_facts false used_facts seen, result) | _ => min timeout xs (x :: seen, result) - in min timeout xs ([], result) end + in min timeout (rev xs) ([], result) end fun binary_minimize test timeout result xs = let @@ -154,20 +155,21 @@ in case test timeout (sup @ l0) of result as {outcome = NONE, used_facts, ...} => - min depth result (filter_used_facts used_facts sup) - (filter_used_facts used_facts l0) + min depth result (filter_used_facts true used_facts sup) + (filter_used_facts true used_facts l0) | _ => case test timeout (sup @ r0) of result as {outcome = NONE, used_facts, ...} => - min depth result (filter_used_facts used_facts sup) - (filter_used_facts used_facts r0) + min depth result (filter_used_facts true used_facts sup) + (filter_used_facts true used_facts r0) | _ => let val (sup_r0, (l, result)) = min depth result (sup @ r0) l0 val (sup, r0) = - (sup, r0) |> pairself (filter_used_facts (map fst sup_r0)) + (sup, r0) + |> pairself (filter_used_facts true (map fst sup_r0)) val (sup_l, (r, result)) = min depth result (sup @ l) r0 - val sup = sup |> filter_used_facts (map fst sup_l) + val sup = sup |> filter_used_facts true (map fst sup_l) in (sup, (l @ r, result)) end end (* @@ -183,8 +185,6 @@ | p => p end -fun is_fact_chained ((_, (sc, _)), _) = sc = Chained - fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent i n state facts = let @@ -193,8 +193,9 @@ get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name fun test timeout = test_facts params silent prover timeout i n state val (chained, non_chained) = List.partition is_fact_chained facts - (* Push chained facts to the back, so that they are less likely to be kicked - out by the linear minimization algorithm. *) + (* Pull chained facts to the front, so that they are less likely to be + kicked out by the minimization algorithms (cf. "rev" in + "linear_minimize"). *) val facts = non_chained @ chained in (print silent (fn () => "Sledgehammer minimizer: " ^ @@ -202,7 +203,7 @@ case test timeout facts of result as {outcome = NONE, used_facts, run_time, ...} => let - val facts = filter_used_facts used_facts facts + val facts = filter_used_facts true used_facts facts val min = if length facts >= Config.get ctxt binary_min_facts then binary_minimize @@ -307,7 +308,7 @@ minimize_facts do_learn minimize_name params (mode <> Normal orelse not verbose) subgoal subgoal_count state - (filter_used_facts used_facts + (filter_used_facts true used_facts (map (apsnd single o untranslated_fact) facts)) |>> Option.map (map fst) else diff -r e65385336531 -r 9152e66f98da src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Aug 14 12:54:26 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Aug 14 13:20:59 2012 +0200 @@ -131,7 +131,10 @@ val kill_provers : unit -> unit val running_provers : unit -> unit val messages : int option -> unit - val filter_used_facts : ''a list -> (''a * 'b) list -> (''a * 'b) list + val is_fact_chained : (('a * stature) * 'b) -> bool + val filter_used_facts : + bool -> (''a * stature) list -> ((''a * stature) * 'b) list -> + ((''a * stature) * 'b) list val get_prover : Proof.context -> mode -> string -> prover end; @@ -483,7 +486,11 @@ #> (fn ctxt => tac_for_reconstructor reconstr ctxt ths)) |> timed_apply timeout -fun filter_used_facts used = filter (member (op =) used o fst) +fun is_fact_chained ((_, (sc, _)), _) = sc = Chained + +fun filter_used_facts keep_chained used = + filter ((member (op =) used o fst) orf + (if keep_chained then is_fact_chained else K false)) fun play_one_line_proof mode debug verbose timeout pairs state i preferred reconstrs = @@ -862,7 +869,8 @@ fn () => let val used_pairs = - facts |> map untranslated_fact |> filter_used_facts used_facts + facts |> map untranslated_fact + |> filter_used_facts false used_facts in play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal (hd reconstrs) reconstrs diff -r e65385336531 -r 9152e66f98da src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Aug 14 12:54:26 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Aug 14 13:20:59 2012 +0200 @@ -87,7 +87,7 @@ fun print_used_facts used_facts = tag_list 1 facts |> map (fn (j, fact) => fact |> untranslated_fact |> apsnd (K j)) - |> filter_used_facts used_facts + |> filter_used_facts false used_facts |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) |> commas |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^