--- 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
--- 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
--- 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
--- 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
--- 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,