# HG changeset patch # User blanchet # Date 1287752547 -7200 # Node ID 658a37c80b5308b2d132d434d8a03cb90dc9122c # Parent bdb890782d4acba0c5363c1c176e30c11603d8e9 generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different) diff -r bdb890782d4a -r 658a37c80b53 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Oct 22 14:47:43 2010 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Oct 22 15:02:27 2010 +0200 @@ -352,13 +352,15 @@ [("timeout", Int.toString timeout ^ " s")] val default_max_relevant = Sledgehammer.default_max_relevant_for_prover thy prover_name + val irrelevant_consts = + Sledgehammer.irrelevant_consts_for_prover prover_name val relevance_fudge = Sledgehammer.relevance_fudge_for_prover prover_name val relevance_override = {add = [], del = [], only = false} val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i val axioms = Sledgehammer_Filter.relevant_facts ctxt full_types relevance_thresholds - (the_default default_max_relevant max_relevant) relevance_fudge - relevance_override chained_ths hyp_ts concl_t + (the_default default_max_relevant max_relevant) irrelevant_consts + relevance_fudge relevance_override chained_ths hyp_ts concl_t val problem = {state = st', goal = goal, subgoal = i, subgoal_count = Sledgehammer_Util.subgoal_count st, diff -r bdb890782d4a -r 658a37c80b53 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Oct 22 14:47:43 2010 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Oct 22 15:02:27 2010 +0200 @@ -107,9 +107,12 @@ SOME proofs => let val {context = ctxt, facts, goal} = Proof.goal pre + val irrelevant_consts = + Sledgehammer.irrelevant_consts_for_prover prover_name val relevance_fudge = extract_relevance_fudge args (Sledgehammer.relevance_fudge_for_prover prover_name) + val relevance_override = {add = [], del = [], only = false} val {relevance_thresholds, full_types, max_relevant, ...} = Sledgehammer_Isar.default_params ctxt args val subgoal = 1 @@ -117,8 +120,9 @@ val facts = Sledgehammer_Filter.relevant_facts ctxt full_types relevance_thresholds - (the_default default_max_relevant max_relevant) relevance_fudge - {add = [], del = [], only = false} facts hyp_ts concl_t + (the_default default_max_relevant max_relevant) + irrelevant_consts relevance_fudge relevance_override facts hyp_ts + concl_t |> map (fst o fst) val (found_facts, lost_facts) = List.concat proofs |> sort_distinct string_ord diff -r bdb890782d4a -r 658a37c80b53 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 22 14:47:43 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 22 15:02:27 2010 +0200 @@ -52,6 +52,7 @@ val smtN : string val default_max_relevant_for_prover : theory -> string -> int + val irrelevant_consts_for_prover : string -> string list val relevance_fudge_for_prover : string -> relevance_fudge val dest_dir : string Config.T val problem_prefix : string Config.T @@ -98,6 +99,16 @@ if is_smt_prover name then smt_default_max_relevant else #default_max_relevant (get_atp thy name) +(* These are typically simplified away by "Meson.presimplify". Equality is + handled specially via "fequal". *) +val atp_irrelevant_consts = + [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let}, + @{const_name HOL.eq}] +val smt_irrelevant_consts = atp_irrelevant_consts (* FIXME *) + +fun irrelevant_consts_for_prover name = + if is_smt_prover name then smt_irrelevant_consts else atp_irrelevant_consts + (* FUDGE *) val atp_relevance_fudge = {worse_irrel_freq = 100.0, @@ -118,25 +129,25 @@ threshold_divisor = 2.0, ridiculous_threshold = 0.1} -(* FUDGE *) +(* FUDGE (FIXME) *) val smt_relevance_fudge = - {worse_irrel_freq = 100.0, - higher_order_irrel_weight = 1.05, - abs_rel_weight = 0.5, - abs_irrel_weight = 2.0, - skolem_irrel_weight = 0.75, - theory_const_rel_weight = 0.5, - theory_const_irrel_weight = 0.25, - intro_bonus = 0.15, - elim_bonus = 0.15, - simp_bonus = 0.15, - local_bonus = 0.55, - assum_bonus = 1.05, - chained_bonus = 1.5, - max_imperfect = 11.5, - max_imperfect_exp = 1.0, - threshold_divisor = 2.0, - ridiculous_threshold = 0.1} + {worse_irrel_freq = #worse_irrel_freq atp_relevance_fudge, + higher_order_irrel_weight = #higher_order_irrel_weight atp_relevance_fudge, + abs_rel_weight = #abs_rel_weight atp_relevance_fudge, + abs_irrel_weight = #abs_irrel_weight atp_relevance_fudge, + skolem_irrel_weight = #skolem_irrel_weight atp_relevance_fudge, + theory_const_rel_weight = #theory_const_rel_weight atp_relevance_fudge, + theory_const_irrel_weight = #theory_const_irrel_weight atp_relevance_fudge, + intro_bonus = #intro_bonus atp_relevance_fudge, + elim_bonus = #elim_bonus atp_relevance_fudge, + simp_bonus = #simp_bonus atp_relevance_fudge, + local_bonus = #local_bonus atp_relevance_fudge, + assum_bonus = #assum_bonus atp_relevance_fudge, + chained_bonus = #chained_bonus atp_relevance_fudge, + max_imperfect = #max_imperfect atp_relevance_fudge, + max_imperfect_exp = #max_imperfect_exp atp_relevance_fudge, + threshold_divisor = #threshold_divisor atp_relevance_fudge, + ridiculous_threshold = #ridiculous_threshold atp_relevance_fudge} fun relevance_fudge_for_prover name = if is_smt_prover name then smt_relevance_fudge else atp_relevance_fudge @@ -485,8 +496,8 @@ val _ = () |> not blocking ? kill_provers val _ = if auto then () else priority "Sledgehammering..." val (smts, atps) = provers |> List.partition is_smt_prover - fun run_provers full_types relevance_fudge maybe_prepare provers - (res as (success, state)) = + fun run_provers full_types irrelevant_consts relevance_fudge maybe_prepare + provers (res as (success, state)) = if success orelse null provers then res else @@ -500,8 +511,8 @@ |> auto ? (fn n => n div auto_max_relevant_divisor) val axioms = relevant_facts ctxt full_types relevance_thresholds - max_max_relevant relevance_fudge relevance_override - chained_ths hyp_ts concl_t + max_max_relevant irrelevant_consts relevance_fudge + relevance_override chained_ths hyp_ts concl_t |> map maybe_prepare val problem = {state = state, goal = goal, subgoal = i, subgoal_count = n, @@ -517,9 +528,12 @@ (run_prover problem) |> exists fst |> rpair state end - val run_atps = run_provers full_types atp_relevance_fudge - (Prepared o prepare_axiom ctxt) atps - val run_smts = run_provers true smt_relevance_fudge Unprepared smts + val run_atps = + run_provers full_types atp_irrelevant_consts atp_relevance_fudge + (Prepared o prepare_axiom ctxt) atps + val run_smts = + run_provers true smt_irrelevant_consts smt_relevance_fudge Unprepared + smts fun run_atps_and_smt_solvers () = [run_atps, run_smts] |> Par_List.map (fn f => f (false, state) |> K ()) in diff -r bdb890782d4a -r 658a37c80b53 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Fri Oct 22 14:47:43 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Fri Oct 22 15:02:27 2010 +0200 @@ -38,8 +38,8 @@ Proof.context -> unit Symtab.table -> thm list -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list val relevant_facts : - Proof.context -> bool -> real * real -> int -> relevance_fudge - -> relevance_override -> thm list -> term list -> term + Proof.context -> bool -> real * real -> int -> string list + -> relevance_fudge -> relevance_override -> thm list -> term list -> term -> ((string * locality) * thm) list end; @@ -175,16 +175,10 @@ fun string_for_hyper_pconst (s, ps) = s ^ "{" ^ commas (map string_for_ptype ps) ^ "}" -(* These are typically simplified away by "Meson.presimplify". Equality is - handled specially via "fequal". *) -val boring_consts = - [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let}, - @{const_name HOL.eq}] - (* Add a pconstant to the table, but a [] entry means a standard connective, which we ignore.*) -fun add_pconst_to_table also_skolem (c, p) = - if member (op =) boring_consts c orelse +fun add_pconst_to_table irrelevant_consts also_skolem (c, p) = + if member (op =) irrelevant_consts c orelse (not also_skolem andalso String.isPrefix skolem_prefix c) then I else @@ -192,14 +186,15 @@ fun is_formula_type T = (T = HOLogic.boolT orelse T = propT) -fun pconsts_in_terms thy also_skolems pos ts = +fun pconsts_in_terms thy irrelevant_consts also_skolems pos ts = let val flip = Option.map not (* We include free variables, as well as constants, to handle locales. For each quantifiers that must necessarily be skolemized by the ATP, we introduce a fresh constant to simulate the effect of Skolemization. *) fun do_const const (s, T) ts = - add_pconst_to_table also_skolems (rich_pconst thy const (s, T) ts) + add_pconst_to_table irrelevant_consts also_skolems + (rich_pconst thy const (s, T) ts) #> fold do_term ts and do_term t = case strip_comb t of @@ -207,13 +202,14 @@ | (Free x, ts) => do_const false x ts | (Abs (_, T, t'), ts) => (null ts - ? add_pconst_to_table true (abs_name, PType (order_of_type T + 1, []))) + ? add_pconst_to_table irrelevant_consts true + (abs_name, PType (order_of_type T + 1, []))) #> fold do_term (t' :: ts) | (_, ts) => fold do_term ts fun do_quantifier will_surely_be_skolemized abs_T body_t = do_formula pos body_t #> (if also_skolems andalso will_surely_be_skolemized then - add_pconst_to_table true + add_pconst_to_table irrelevant_consts true (gensym skolem_prefix, PType (order_of_type abs_T, [])) else I) @@ -395,11 +391,12 @@ in if Real.isFinite res then res else 0.0 end *) -fun pconsts_in_axiom thy t = +fun pconsts_in_axiom thy irrelevant_consts t = Symtab.fold (fn (s, pss) => fold (cons o pair s) pss) - (pconsts_in_terms thy true (SOME true) [t]) [] -fun pair_consts_axiom thy fudge axiom = - case axiom |> snd |> theory_const_prop_of fudge |> pconsts_in_axiom thy of + (pconsts_in_terms thy irrelevant_consts true (SOME true) [t]) [] +fun pair_consts_axiom thy irrelevant_consts fudge axiom = + case axiom |> snd |> theory_const_prop_of fudge + |> pconsts_in_axiom thy irrelevant_consts of [] => NONE | consts => SOME ((axiom, consts), NONE) @@ -429,23 +426,23 @@ (accepts, more_rejects @ rejects) end -fun if_empty_replace_with_locality thy axioms loc tab = +fun if_empty_replace_with_locality thy irrelevant_consts axioms loc tab = if Symtab.is_empty tab then - pconsts_in_terms thy false (SOME false) + pconsts_in_terms thy irrelevant_consts false (SOME false) (map_filter (fn ((_, loc'), th) => if loc' = loc then SOME (prop_of th) else NONE) axioms) else tab -fun relevance_filter ctxt threshold0 decay max_relevant +fun relevance_filter ctxt threshold0 decay max_relevant irrelevant_consts (fudge as {threshold_divisor, ridiculous_threshold, ...}) ({add, del, ...} : relevance_override) axioms goal_ts = let val thy = ProofContext.theory_of ctxt val const_tab = fold (count_axiom_consts thy fudge) axioms Symtab.empty val goal_const_tab = - pconsts_in_terms thy false (SOME false) goal_ts - |> fold (if_empty_replace_with_locality thy axioms) + pconsts_in_terms thy irrelevant_consts false (SOME false) goal_ts + |> fold (if_empty_replace_with_locality thy irrelevant_consts axioms) [Chained, Assum, Local] val add_ths = Attrib.eval_thms ctxt add val del_ths = Attrib.eval_thms ctxt del @@ -473,7 +470,8 @@ take_most_relevant max_relevant remaining_max fudge candidates val rel_const_tab' = rel_const_tab - |> fold (add_pconst_to_table false) (maps (snd o fst) accepts) + |> fold (add_pconst_to_table irrelevant_consts false) + (maps (snd o fst) accepts) fun is_dirty (c, _) = Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c val (hopeful_rejects, hopeless_rejects) = @@ -536,7 +534,7 @@ end in axioms |> filter_out (member Thm.eq_thm del_ths o snd) - |> map_filter (pair_consts_axiom thy fudge) + |> map_filter (pair_consts_axiom thy irrelevant_consts fudge) |> iter 0 max_relevant threshold0 goal_const_tab [] |> tap (fn res => trace_msg (fn () => "Total relevant: " ^ Int.toString (length res))) @@ -787,7 +785,8 @@ | NONE => "" end), let val t = prop_of th in - if is_chained th then Chained + if is_chained th then + Chained else if global then if Termtab.defined intros t then Intro else if Termtab.defined elims t then Elim @@ -814,8 +813,9 @@ (* ATP invocation methods setup *) (***************************************************************) -fun relevant_facts ctxt full_types (threshold0, threshold1) max_relevant fudge - (override as {add, only, ...}) chained_ths hyp_ts concl_t = +fun relevant_facts ctxt full_types (threshold0, threshold1) max_relevant + irrelevant_consts fudge (override as {add, only, ...}) + chained_ths hyp_ts concl_t = let val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0), 1.0 / Real.fromInt (max_relevant + 1)) @@ -838,8 +838,8 @@ max_relevant = 0 then [] else - relevance_filter ctxt threshold0 decay max_relevant fudge override axioms - (concl_t :: hyp_ts)) + relevance_filter ctxt threshold0 decay max_relevant irrelevant_consts + fudge override axioms (concl_t :: hyp_ts)) |> map (apfst (apfst (fn f => f ()))) end