# HG changeset patch # User blanchet # Date 1381360657 -7200 # Node ID d80743f28fec7c8cb5c74be1f61e2aac83e2fd44 # Parent 5d077ce92d003680710ce2486aba8be0ea6e193f simplify fudge factor code diff -r 5d077ce92d00 -r d80743f28fec src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Oct 09 17:21:28 2013 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Thu Oct 10 01:17:37 2013 +0200 @@ -110,18 +110,15 @@ SOME proofs => let val {context = ctxt, facts = chained_ths, goal} = Proof.goal pre - val prover = AList.lookup (op =) args "prover" - |> the_default default_prover + val prover = AList.lookup (op =) args "prover" |> the_default default_prover val params as {max_facts, slice, ...} = Sledgehammer_Isar.default_params ctxt args val default_max_facts = Sledgehammer_Provers.default_max_facts_of_prover ctxt slice prover val is_appropriate_prop = - Sledgehammer_Provers.is_appropriate_prop_of_prover ctxt - default_prover + Sledgehammer_Provers.is_appropriate_prop_of_prover ctxt default_prover val relevance_fudge = - extract_relevance_fudge args - (Sledgehammer_Provers.relevance_fudge_of_prover ctxt prover) + extract_relevance_fudge args Sledgehammer_MePo.default_relevance_fudge val subgoal = 1 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal subgoal ctxt val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover @@ -133,8 +130,7 @@ hyp_ts concl_t |> filter (is_appropriate_prop o prop_of o snd) |> Sledgehammer_MePo.mepo_suggested_facts ctxt params - default_prover (the_default default_max_facts max_facts) - (SOME relevance_fudge) hyp_ts concl_t + (the_default default_max_facts max_facts) (SOME relevance_fudge) hyp_ts concl_t |> map (fst o fst) val (found_facts, lost_facts) = flat proofs |> sort_distinct string_ord diff -r 5d077ce92d00 -r d80743f28fec src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Wed Oct 09 17:21:28 2013 +0200 +++ b/src/HOL/TPTP/mash_export.ML Thu Oct 10 01:17:37 2013 +0200 @@ -245,8 +245,7 @@ val suggs = old_facts |> linearize ? filter_accessible_from th - |> Sledgehammer_MePo.mepo_suggested_facts ctxt params prover - max_suggs NONE hyp_ts concl_t + |> Sledgehammer_MePo.mepo_suggested_facts ctxt params max_suggs NONE hyp_ts concl_t |> map (nickname_of_thm o snd) in encode_str name ^ ": " ^ encode_strs suggs ^ "\n" end end diff -r 5d077ce92d00 -r d80743f28fec src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Oct 09 17:21:28 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Oct 10 01:17:37 2013 +0200 @@ -11,7 +11,6 @@ type fact = Sledgehammer_Fact.fact type fact_override = Sledgehammer_Fact.fact_override type params = Sledgehammer_Provers.params - type relevance_fudge = Sledgehammer_Provers.relevance_fudge type prover_result = Sledgehammer_Provers.prover_result val trace : bool Config.T @@ -776,9 +775,8 @@ | NONE => accum (* shouldn't happen *) val facts = facts - |> mepo_suggested_facts ctxt params prover - (max_facts |> the_default prover_default_max_facts) NONE hyp_ts - concl_t + |> mepo_suggested_facts ctxt params (max_facts |> the_default prover_default_max_facts) NONE + hyp_ts concl_t |> fold (add_isar_dep facts) isar_deps |> map nickify in @@ -1329,7 +1327,7 @@ (accepts |> filter_out in_add)) |> take max_facts fun mepo () = - (mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts concl_t facts + (mepo_suggested_facts ctxt params max_facts NONE hyp_ts concl_t facts |> weight_facts_steeply, []) fun mash () = mash_suggested_facts ctxt params prover (generous_max_facts max_facts) hyp_ts concl_t facts diff -r 5d077ce92d00 -r d80743f28fec src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Wed Oct 09 17:21:28 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Thu Oct 10 01:17:37 2013 +0200 @@ -11,13 +11,33 @@ type raw_fact = Sledgehammer_Fact.raw_fact type fact = Sledgehammer_Fact.fact type params = Sledgehammer_Provers.params - type relevance_fudge = Sledgehammer_Provers.relevance_fudge + + type relevance_fudge = + {local_const_multiplier : real, + worse_irrel_freq : real, + higher_order_irrel_weight : real, + abs_rel_weight : real, + abs_irrel_weight : real, + theory_const_rel_weight : real, + theory_const_irrel_weight : real, + chained_const_irrel_weight : real, + intro_bonus : real, + elim_bonus : real, + simp_bonus : real, + local_bonus : real, + assum_bonus : real, + chained_bonus : real, + max_imperfect : real, + max_imperfect_exp : real, + threshold_divisor : real, + ridiculous_threshold : real} val trace : bool Config.T val pseudo_abs_name : string + val default_relevance_fudge : relevance_fudge val mepo_suggested_facts : - Proof.context -> params -> string -> int -> relevance_fudge option - -> term list -> term -> raw_fact list -> fact list + Proof.context -> params -> int -> relevance_fudge option -> term list -> term -> + raw_fact list -> fact list end; structure Sledgehammer_MePo : SLEDGEHAMMER_MEPO = @@ -36,6 +56,47 @@ val pseudo_abs_name = sledgehammer_prefix ^ "abs" val theory_const_suffix = Long_Name.separator ^ " 1" +type relevance_fudge = + {local_const_multiplier : real, + worse_irrel_freq : real, + higher_order_irrel_weight : real, + abs_rel_weight : real, + abs_irrel_weight : real, + theory_const_rel_weight : real, + theory_const_irrel_weight : real, + chained_const_irrel_weight : real, + intro_bonus : real, + elim_bonus : real, + simp_bonus : real, + local_bonus : real, + assum_bonus : real, + chained_bonus : real, + max_imperfect : real, + max_imperfect_exp : real, + threshold_divisor : real, + ridiculous_threshold : real} + +(* FUDGE *) +val default_relevance_fudge = + {local_const_multiplier = 1.5, + worse_irrel_freq = 100.0, + higher_order_irrel_weight = 1.05, + abs_rel_weight = 0.5, + abs_irrel_weight = 2.0, + theory_const_rel_weight = 0.5, + theory_const_irrel_weight = 0.25, + chained_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} + fun order_of_type (Type (@{type_name fun}, [T1, T2])) = Int.max (order_of_type T1 + 1, order_of_type T2) | order_of_type (Type (_, Ts)) = fold (Integer.max o order_of_type) Ts 0 @@ -497,15 +558,11 @@ "Total relevant: " ^ string_of_int (length accepts))) end -fun mepo_suggested_facts ctxt - ({fact_thresholds = (thres0, thres1), ...} : params) prover - max_facts fudge hyp_ts concl_t facts = +fun mepo_suggested_facts ctxt ({fact_thresholds = (thres0, thres1), ...} : params) max_facts fudge + hyp_ts concl_t facts = let val thy = Proof_Context.theory_of ctxt - val fudge = - case fudge of - SOME fudge => fudge - | NONE => Sledgehammer_Provers.relevance_fudge_of_prover ctxt prover + val fudge = fudge |> the_default default_relevance_fudge val decay = Math.pow ((1.0 - thres1) / (1.0 - thres0), 1.0 / Real.fromInt (max_facts + 1)) in diff -r 5d077ce92d00 -r d80743f28fec src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Oct 09 17:21:28 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Oct 10 01:17:37 2013 +0200 @@ -44,26 +44,6 @@ preplay_timeout : Time.time option, expect : string} - type relevance_fudge = - {local_const_multiplier : real, - worse_irrel_freq : real, - higher_order_irrel_weight : real, - abs_rel_weight : real, - abs_irrel_weight : real, - theory_const_rel_weight : real, - theory_const_irrel_weight : real, - chained_const_irrel_weight : real, - intro_bonus : real, - elim_bonus : real, - simp_bonus : real, - local_bonus : real, - assum_bonus : real, - chained_bonus : real, - max_imperfect : real, - max_imperfect_exp : real, - threshold_divisor : real, - ridiculous_threshold : real} - type prover_problem = {state : Proof.state, goal : thm, @@ -119,9 +99,6 @@ val default_max_facts_of_prover : Proof.context -> bool -> string -> int val is_unit_equality : term -> bool val is_appropriate_prop_of_prover : Proof.context -> string -> term -> bool - val atp_relevance_fudge : relevance_fudge - val smt_relevance_fudge : relevance_fudge - val relevance_fudge_of_prover : Proof.context -> string -> relevance_fudge val weight_smt_fact : Proof.context -> int -> ((string * stature) * thm) * int -> (string * stature) * (int option * thm) @@ -263,51 +240,6 @@ fun is_appropriate_prop_of_prover ctxt name = if is_unit_equational_atp ctxt name then is_unit_equality else K true -(* FUDGE *) -val atp_relevance_fudge = - {local_const_multiplier = 1.5, - worse_irrel_freq = 100.0, - higher_order_irrel_weight = 1.05, - abs_rel_weight = 0.5, - abs_irrel_weight = 2.0, - theory_const_rel_weight = 0.5, - theory_const_irrel_weight = 0.25, - chained_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} - -(* FUDGE (FIXME) *) -val smt_relevance_fudge = - {local_const_multiplier = #local_const_multiplier atp_relevance_fudge, - 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, - theory_const_rel_weight = #theory_const_rel_weight atp_relevance_fudge, - theory_const_irrel_weight = #theory_const_irrel_weight atp_relevance_fudge, - chained_const_irrel_weight = #chained_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_of_prover ctxt name = - if is_smt_prover ctxt name then smt_relevance_fudge else atp_relevance_fudge - fun supported_provers ctxt = let val thy = Proof_Context.theory_of ctxt @@ -354,26 +286,6 @@ preplay_timeout : Time.time option, expect : string} -type relevance_fudge = - {local_const_multiplier : real, - worse_irrel_freq : real, - higher_order_irrel_weight : real, - abs_rel_weight : real, - abs_irrel_weight : real, - theory_const_rel_weight : real, - theory_const_irrel_weight : real, - chained_const_irrel_weight : real, - intro_bonus : real, - elim_bonus : real, - simp_bonus : real, - local_bonus : real, - assum_bonus : real, - chained_bonus : real, - max_imperfect : real, - max_imperfect_exp : real, - threshold_divisor : real, - ridiculous_threshold : real} - type prover_problem = {state : Proof.state, goal : thm,