--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Oct 22 14:10:32 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Oct 22 14:47:43 2010 +0200
@@ -350,13 +350,14 @@
val params as {full_types, relevance_thresholds, max_relevant, ...} =
Sledgehammer_Isar.default_params ctxt
[("timeout", Int.toString timeout ^ " s")]
- val relevance_override = {add = [], del = [], only = false}
val default_max_relevant =
Sledgehammer.default_max_relevant_for_prover thy 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)
+ (the_default default_max_relevant max_relevant) relevance_fudge
relevance_override chained_ths hyp_ts concl_t
val problem =
{state = st', goal = goal, subgoal = i,
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Oct 22 14:10:32 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Oct 22 14:47:43 2010 +0200
@@ -5,26 +5,37 @@
structure Mirabelle_Sledgehammer_Filter : MIRABELLE_ACTION =
struct
-structure SF = Sledgehammer_Filter
+fun get args name default_value =
+ case AList.lookup (op =) args name of
+ SOME value => the (Real.fromString value)
+ | NONE => default_value
-val relevance_filter_args =
- [("worse_irrel_freq", SF.worse_irrel_freq),
- ("higher_order_irrel_weight", SF.higher_order_irrel_weight),
- ("abs_rel_weight", SF.abs_rel_weight),
- ("abs_irrel_weight", SF.abs_irrel_weight),
- ("skolem_irrel_weight", SF.skolem_irrel_weight),
- ("theory_const_rel_weight", SF.theory_const_rel_weight),
- ("theory_const_irrel_weight", SF.theory_const_irrel_weight),
- ("intro_bonus", SF.intro_bonus),
- ("elim_bonus", SF.elim_bonus),
- ("simp_bonus", SF.simp_bonus),
- ("local_bonus", SF.local_bonus),
- ("assum_bonus", SF.assum_bonus),
- ("chained_bonus", SF.chained_bonus),
- ("max_imperfect", SF.max_imperfect),
- ("max_imperfect_exp", SF.max_imperfect_exp),
- ("threshold_divisor", SF.threshold_divisor),
- ("ridiculous_threshold", SF.ridiculous_threshold)]
+fun extract_relevance_fudge args
+ {worse_irrel_freq, higher_order_irrel_weight, abs_rel_weight,
+ abs_irrel_weight, skolem_irrel_weight, theory_const_rel_weight,
+ theory_const_irrel_weight, intro_bonus, elim_bonus, simp_bonus,
+ local_bonus, assum_bonus, chained_bonus, max_imperfect,
+ max_imperfect_exp, threshold_divisor, ridiculous_threshold} =
+ {worse_irrel_freq = get args "worse_irrel_freq" worse_irrel_freq,
+ higher_order_irrel_weight =
+ get args "higher_order_irrel_weight" higher_order_irrel_weight,
+ abs_rel_weight = get args "abs_rel_weight" abs_rel_weight,
+ abs_irrel_weight = get args "abs_irrel_weight" abs_irrel_weight,
+ skolem_irrel_weight = get args "skolem_irrel_weight" skolem_irrel_weight,
+ theory_const_rel_weight =
+ get args "theory_const_rel_weight" theory_const_rel_weight,
+ theory_const_irrel_weight =
+ get args "theory_const_irrel_weight" theory_const_irrel_weight,
+ intro_bonus = get args "intro_bonus" intro_bonus,
+ elim_bonus = get args "elim_bonus" elim_bonus,
+ simp_bonus = get args "simp_bonus" simp_bonus,
+ local_bonus = get args "local_bonus" local_bonus,
+ assum_bonus = get args "assum_bonus" assum_bonus,
+ chained_bonus = get args "chained_bonus" chained_bonus,
+ max_imperfect = get args "max_imperfect" max_imperfect,
+ max_imperfect_exp = get args "max_imperfect_exp" max_imperfect_exp,
+ threshold_divisor = get args "threshold_divisor" threshold_divisor,
+ ridiculous_threshold = get args "ridiculous_threshold" ridiculous_threshold}
structure Prooftab =
Table(type key = int * int val ord = prod_ord int_ord int_ord);
@@ -85,6 +96,7 @@
()
val default_max_relevant = 300
+val prover_name = ATP_Systems.eN (* arbitrary ATP *)
fun with_index (i, s) = s ^ "@" ^ string_of_int i
@@ -95,21 +107,17 @@
SOME proofs =>
let
val {context = ctxt, facts, goal} = Proof.goal pre
- val args =
- args
- |> filter (fn (key, value) =>
- case AList.lookup (op =) relevance_filter_args key of
- SOME rf => (rf := the (Real.fromString value); false)
- | NONE => true)
-
+ val relevance_fudge =
+ extract_relevance_fudge args
+ (Sledgehammer.relevance_fudge_for_prover prover_name)
val {relevance_thresholds, full_types, max_relevant, ...} =
Sledgehammer_Isar.default_params ctxt args
val subgoal = 1
val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal
val facts =
- SF.relevant_facts ctxt full_types
+ Sledgehammer_Filter.relevant_facts ctxt full_types
relevance_thresholds
- (the_default default_max_relevant max_relevant)
+ (the_default default_max_relevant max_relevant) relevance_fudge
{add = [], del = [], only = false} facts hyp_ts concl_t
|> map (fst o fst)
val (found_facts, lost_facts) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 22 14:10:32 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 22 14:47:43 2010 +0200
@@ -10,6 +10,7 @@
sig
type failure = ATP_Systems.failure
type locality = Sledgehammer_Filter.locality
+ type relevance_fudge = Sledgehammer_Filter.relevance_fudge
type relevance_override = Sledgehammer_Filter.relevance_override
type prepared_formula = Sledgehammer_ATP_Translate.prepared_formula
type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
@@ -51,6 +52,7 @@
val smtN : string
val default_max_relevant_for_prover : theory -> string -> int
+ val relevance_fudge_for_prover : string -> relevance_fudge
val dest_dir : string Config.T
val problem_prefix : string Config.T
val measure_run_time : bool Config.T
@@ -87,13 +89,58 @@
val smtN = "smt"
val smt_prover_names = [smtN, remote_prefix ^ smtN]
+val is_smt_prover = member (op =) smt_prover_names
+
val smt_default_max_relevant = 300 (* FUDGE *)
val auto_max_relevant_divisor = 2 (* FUDGE *)
fun default_max_relevant_for_prover thy name =
- if member (op =) smt_prover_names name then smt_default_max_relevant
+ if is_smt_prover name then smt_default_max_relevant
else #default_max_relevant (get_atp thy name)
+(* FUDGE *)
+val atp_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}
+
+(* FUDGE *)
+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}
+
+fun relevance_fudge_for_prover name =
+ if is_smt_prover name then smt_relevance_fudge else atp_relevance_fudge
+
fun available_provers thy =
let
val (remote_provers, local_provers) =
@@ -364,10 +411,8 @@
end
fun get_prover thy auto name =
- if member (op =) smt_prover_names name then
- run_smt_solver (String.isPrefix remote_prefix)
- else
- run_atp auto name (get_atp thy name)
+ if is_smt_prover name then run_smt_solver (String.isPrefix remote_prefix)
+ else run_atp auto name (get_atp thy name)
fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...})
auto minimize_command
@@ -439,9 +484,9 @@
val (_, hyp_ts, concl_t) = strip_subgoal goal i
val _ = () |> not blocking ? kill_provers
val _ = if auto then () else priority "Sledgehammering..."
- val (smts, atps) =
- provers |> List.partition (member (op =) smt_prover_names)
- fun run_provers full_types maybe_prepare provers (res as (success, state)) =
+ val (smts, atps) = provers |> List.partition is_smt_prover
+ fun run_provers full_types relevance_fudge maybe_prepare provers
+ (res as (success, state)) =
if success orelse null provers then
res
else
@@ -455,8 +500,8 @@
|> auto ? (fn n => n div auto_max_relevant_divisor)
val axioms =
relevant_facts ctxt full_types relevance_thresholds
- max_max_relevant relevance_override chained_ths
- hyp_ts concl_t
+ max_max_relevant relevance_fudge relevance_override
+ chained_ths hyp_ts concl_t
|> map maybe_prepare
val problem =
{state = state, goal = goal, subgoal = i, subgoal_count = n,
@@ -472,8 +517,9 @@
(run_prover problem)
|> exists fst |> rpair state
end
- val run_atps = run_provers full_types (Prepared o prepare_axiom ctxt) atps
- val run_smts = run_provers true Unprepared smts
+ 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
fun run_atps_and_smt_solvers () =
[run_atps, run_smts] |> Par_List.map (fn f => f (false, state) |> K ())
in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Fri Oct 22 14:10:32 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Fri Oct 22 14:47:43 2010 +0200
@@ -9,35 +9,38 @@
sig
datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
+ type relevance_fudge =
+ {worse_irrel_freq : real,
+ higher_order_irrel_weight : real,
+ abs_rel_weight : real,
+ abs_irrel_weight : real,
+ skolem_irrel_weight : real,
+ theory_const_rel_weight : real,
+ theory_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 relevance_override =
- {add: (Facts.ref * Attrib.src list) list,
- del: (Facts.ref * Attrib.src list) list,
- only: bool}
+ {add : (Facts.ref * Attrib.src list) list,
+ del : (Facts.ref * Attrib.src list) list,
+ only : bool}
val trace : bool Unsynchronized.ref
- val worse_irrel_freq : real Unsynchronized.ref
- val higher_order_irrel_weight : real Unsynchronized.ref
- val abs_rel_weight : real Unsynchronized.ref
- val abs_irrel_weight : real Unsynchronized.ref
- val skolem_irrel_weight : real Unsynchronized.ref
- val theory_const_rel_weight : real Unsynchronized.ref
- val theory_const_irrel_weight : real Unsynchronized.ref
- val intro_bonus : real Unsynchronized.ref
- val elim_bonus : real Unsynchronized.ref
- val simp_bonus : real Unsynchronized.ref
- val local_bonus : real Unsynchronized.ref
- val assum_bonus : real Unsynchronized.ref
- val chained_bonus : real Unsynchronized.ref
- val max_imperfect : real Unsynchronized.ref
- val max_imperfect_exp : real Unsynchronized.ref
- val threshold_divisor : real Unsynchronized.ref
- val ridiculous_threshold : real Unsynchronized.ref
val name_thm_pairs_from_ref :
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_override
- -> thm list -> term list -> term -> ((string * locality) * thm) list
+ Proof.context -> bool -> real * real -> int -> relevance_fudge
+ -> relevance_override -> thm list -> term list -> term
+ -> ((string * locality) * thm) list
end;
structure Sledgehammer_Filter : SLEDGEHAMMER_FILTER =
@@ -52,31 +55,31 @@
val term_patterns = false
val respect_no_atp = true
-(* FUDGE *)
-val worse_irrel_freq = Unsynchronized.ref 100.0
-val higher_order_irrel_weight = Unsynchronized.ref 1.05
-val abs_rel_weight = Unsynchronized.ref 0.5
-val abs_irrel_weight = Unsynchronized.ref 2.0
-val skolem_irrel_weight = Unsynchronized.ref 0.75
-val theory_const_rel_weight = Unsynchronized.ref 0.5
-val theory_const_irrel_weight = Unsynchronized.ref 0.25
-val intro_bonus = Unsynchronized.ref 0.15
-val elim_bonus = Unsynchronized.ref 0.15
-val simp_bonus = Unsynchronized.ref 0.15
-val local_bonus = Unsynchronized.ref 0.55
-val assum_bonus = Unsynchronized.ref 1.05
-val chained_bonus = Unsynchronized.ref 1.5
-val max_imperfect = Unsynchronized.ref 11.5
-val max_imperfect_exp = Unsynchronized.ref 1.0
-val threshold_divisor = Unsynchronized.ref 2.0
-val ridiculous_threshold = Unsynchronized.ref 0.1
-
datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
+type relevance_fudge =
+ {worse_irrel_freq : real,
+ higher_order_irrel_weight : real,
+ abs_rel_weight : real,
+ abs_irrel_weight : real,
+ skolem_irrel_weight : real,
+ theory_const_rel_weight : real,
+ theory_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 relevance_override =
- {add: (Facts.ref * Attrib.src list) list,
- del: (Facts.ref * Attrib.src list) list,
- only: bool}
+ {add : (Facts.ref * Attrib.src list) list,
+ del : (Facts.ref * Attrib.src list) list,
+ only : bool}
val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
val abs_name = sledgehammer_prefix ^ "abs"
@@ -254,9 +257,11 @@
(*Inserts a dummy "constant" referring to the theory name, so that relevance
takes the given theory into account.*)
-fun theory_const_prop_of th =
- if exists (curry (op <) 0.0) [!theory_const_rel_weight,
- !theory_const_irrel_weight] then
+fun theory_const_prop_of ({theory_const_rel_weight,
+ theory_const_irrel_weight, ...} : relevance_fudge)
+ th =
+ if exists (curry (op <) 0.0) [theory_const_rel_weight,
+ theory_const_irrel_weight] then
let
val name = Context.theory_name (theory_of_thm th)
val t = Const (name ^ theory_const_suffix, @{typ bool})
@@ -282,7 +287,7 @@
structure PType_Tab = Table(type key = ptype val ord = ptype_ord)
-fun count_axiom_consts thy =
+fun count_axiom_consts thy fudge =
let
fun do_const const (s, T) ts =
(* Two-dimensional table update. Constant maps to types maps to count. *)
@@ -295,7 +300,7 @@
| (Free x, ts) => do_const false x ts
| (Abs (_, _, t'), ts) => fold do_term (t' :: ts)
| (_, ts) => fold do_term ts
- in do_term o theory_const_prop_of o snd end
+ in do_term o theory_const_prop_of fudge o snd end
(**** Actual Filtering Code ****)
@@ -322,11 +327,12 @@
very rare constants and very common ones -- the former because they can't
lead to the inclusion of too many new facts, and the latter because they are
so common as to be of little interest. *)
-fun irrel_weight_for order freq =
- let val (k, x) = !worse_irrel_freq |> `Real.ceil in
+fun irrel_weight_for ({worse_irrel_freq, higher_order_irrel_weight, ...}
+ : relevance_fudge) order freq =
+ let val (k, x) = worse_irrel_freq |> `Real.ceil in
(if freq < k then Math.ln (Real.fromInt (freq + 1)) / Math.ln x
else rel_weight_for order freq / rel_weight_for order k)
- * pow_int (!higher_order_irrel_weight) (order - 1)
+ * pow_int higher_order_irrel_weight (order - 1)
end
(* Computes a constant's weight, as determined by its frequency. *)
@@ -337,22 +343,25 @@
else if String.isSuffix theory_const_suffix s then theory_const_weight
else weight_for m (pconst_freq (match_ptype o f) const_tab c)
-fun rel_pconst_weight const_tab =
- generic_pconst_weight (!abs_rel_weight) 0.0 (!theory_const_rel_weight)
+fun rel_pconst_weight ({abs_rel_weight, theory_const_rel_weight, ...}
+ : relevance_fudge) const_tab =
+ generic_pconst_weight abs_rel_weight 0.0 theory_const_rel_weight
rel_weight_for I const_tab
-fun irrel_pconst_weight const_tab =
- generic_pconst_weight (!abs_irrel_weight) (!skolem_irrel_weight)
- (!theory_const_irrel_weight) irrel_weight_for swap const_tab
+fun irrel_pconst_weight (fudge as {abs_irrel_weight, skolem_irrel_weight,
+ theory_const_irrel_weight, ...}) const_tab =
+ generic_pconst_weight abs_irrel_weight skolem_irrel_weight
+ theory_const_irrel_weight (irrel_weight_for fudge) swap
+ const_tab
-fun locality_bonus General = 0.0
- | locality_bonus Intro = !intro_bonus
- | locality_bonus Elim = !elim_bonus
- | locality_bonus Simp = !simp_bonus
- | locality_bonus Local = !local_bonus
- | locality_bonus Assum = !assum_bonus
- | locality_bonus Chained = !chained_bonus
+fun locality_bonus (_ : relevance_fudge) General = 0.0
+ | locality_bonus {intro_bonus, ...} Intro = intro_bonus
+ | locality_bonus {elim_bonus, ...} Elim = elim_bonus
+ | locality_bonus {simp_bonus, ...} Simp = simp_bonus
+ | locality_bonus {local_bonus, ...} Local = local_bonus
+ | locality_bonus {assum_bonus, ...} Assum = assum_bonus
+ | locality_bonus {chained_bonus, ...} Chained = chained_bonus
-fun axiom_weight loc const_tab relevant_consts axiom_consts =
+fun axiom_weight fudge loc const_tab relevant_consts axiom_consts =
case axiom_consts |> List.partition (pconst_hyper_mem I relevant_consts)
||> filter_out (pconst_hyper_mem swap relevant_consts) of
([], _) => 0.0
@@ -360,15 +369,15 @@
let
val irrel = irrel |> filter_out (pconst_mem swap rel)
val rel_weight =
- 0.0 |> fold (curry (op +) o rel_pconst_weight const_tab) rel
+ 0.0 |> fold (curry (op +) o rel_pconst_weight fudge const_tab) rel
val irrel_weight =
- ~ (locality_bonus loc)
- |> fold (curry (op +) o irrel_pconst_weight const_tab) irrel
+ ~ (locality_bonus fudge loc)
+ |> fold (curry (op +) o irrel_pconst_weight fudge const_tab) irrel
val res = rel_weight / (rel_weight + irrel_weight)
in if Real.isFinite res then res else 0.0 end
(* FIXME: experiment
-fun debug_axiom_weight loc const_tab relevant_consts axiom_consts =
+fun debug_axiom_weight fudge loc const_tab relevant_consts axiom_consts =
case axiom_consts |> List.partition (pconst_hyper_mem I relevant_consts)
||> filter_out (pconst_hyper_mem swap relevant_consts) of
([], _) => 0.0
@@ -378,10 +387,10 @@
val rels_weight =
0.0 |> fold (curry (op +) o rel_pconst_weight const_tab) rel
val irrels_weight =
- ~ (locality_bonus loc)
- |> fold (curry (op +) o irrel_pconst_weight const_tab) irrel
+ ~ (locality_bonus fudge loc)
+ |> fold (curry (op +) o irrel_pconst_weight fudge const_tab) irrel
val _ = tracing (PolyML.makestring ("REL: ", map (`(rel_pconst_weight const_tab)) rel))
-val _ = tracing (PolyML.makestring ("IRREL: ", map (`(irrel_pconst_weight const_tab)) irrel))
+val _ = tracing (PolyML.makestring ("IRREL: ", map (`(irrel_pconst_weight fudge const_tab)) irrel))
val res = rels_weight / (rels_weight + irrels_weight)
in if Real.isFinite res then res else 0.0 end
*)
@@ -389,8 +398,8 @@
fun pconsts_in_axiom thy 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 axiom =
- case axiom |> snd |> theory_const_prop_of |> pconsts_in_axiom thy of
+fun pair_consts_axiom thy fudge axiom =
+ case axiom |> snd |> theory_const_prop_of fudge |> pconsts_in_axiom thy of
[] => NONE
| consts => SOME ((axiom, consts), NONE)
@@ -398,12 +407,13 @@
(((unit -> string) * locality) * thm) * (string * ptype) list
fun take_most_relevant max_relevant remaining_max
- (candidates : (annotated_thm * real) list) =
+ ({max_imperfect, max_imperfect_exp, ...} : relevance_fudge)
+ (candidates : (annotated_thm * real) list) =
let
val max_imperfect =
- Real.ceil (Math.pow (!max_imperfect,
+ Real.ceil (Math.pow (max_imperfect,
Math.pow (Real.fromInt remaining_max
- / Real.fromInt max_relevant, !max_imperfect_exp)))
+ / Real.fromInt max_relevant, max_imperfect_exp)))
val (perfect, imperfect) =
candidates |> sort (Real.compare o swap o pairself snd)
|> take_prefix (fn (_, w) => w > 0.99999)
@@ -428,10 +438,11 @@
tab
fun relevance_filter ctxt threshold0 decay max_relevant
- ({add, del, ...} : relevance_override) axioms goal_ts =
+ (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) axioms Symtab.empty
+ 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)
@@ -450,16 +461,16 @@
else NONE) rejects
fun relevant [] rejects [] =
(* Nothing has been added this iteration. *)
- if j = 0 andalso threshold >= !ridiculous_threshold then
+ if j = 0 andalso threshold >= ridiculous_threshold then
(* First iteration? Try again. *)
- iter 0 max_relevant (threshold / !threshold_divisor) rel_const_tab
+ iter 0 max_relevant (threshold / threshold_divisor) rel_const_tab
hopeless hopeful
else
game_over (rejects @ hopeless)
| relevant candidates rejects [] =
let
val (accepts, more_rejects) =
- take_most_relevant max_relevant remaining_max candidates
+ 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)
@@ -499,11 +510,12 @@
val weight =
case cached_weight of
SOME w => w
- | NONE => axiom_weight loc const_tab rel_const_tab axiom_consts
+ | NONE => axiom_weight fudge loc const_tab rel_const_tab
+ axiom_consts
(* FIXME: experiment
val name = fst (fst (fst ax)) ()
val _ = if String.isSubstring "positive_minus" name orelse String.isSubstring "not_exp_le_zero" name then
-tracing ("*** " ^ name ^ PolyML.makestring (debug_axiom_weight loc const_tab rel_const_tab axiom_consts))
+tracing ("*** " ^ name ^ PolyML.makestring (debug_axiom_weight fudge loc const_tab rel_const_tab axiom_consts))
else
()
*)
@@ -524,7 +536,7 @@
end
in
axioms |> filter_out (member Thm.eq_thm del_ths o snd)
- |> map_filter (pair_consts_axiom thy)
+ |> map_filter (pair_consts_axiom thy fudge)
|> iter 0 max_relevant threshold0 goal_const_tab []
|> tap (fn res => trace_msg (fn () =>
"Total relevant: " ^ Int.toString (length res)))
@@ -708,7 +720,9 @@
(Term.add_vars t [] |> sort_wrt (fst o fst))
|> fst
-fun all_name_thms_pairs ctxt reserved full_types add_ths chained_ths =
+fun all_name_thms_pairs ctxt reserved full_types
+ ({intro_bonus, elim_bonus, simp_bonus, ...} : relevance_fudge) add_ths
+ chained_ths =
let
val thy = ProofContext.theory_of ctxt
val global_facts = Global_Theory.facts_of thy
@@ -718,7 +732,7 @@
fun is_assum th = exists (fn ct => prop_of th aconv term_of ct) assms
val is_chained = member Thm.eq_thm chained_ths
val (intros, elims, simps) =
- if exists (curry (op <) 0.0) [!intro_bonus, !elim_bonus, !simp_bonus] then
+ if exists (curry (op <) 0.0) [intro_bonus, elim_bonus, simp_bonus] then
clasimpset_rules_of ctxt
else
(Termtab.empty, Termtab.empty, Termtab.empty)
@@ -800,9 +814,8 @@
(* ATP invocation methods setup *)
(***************************************************************)
-fun relevant_facts ctxt full_types (threshold0, threshold1) max_relevant
- (relevance_override as {add, only, ...}) chained_ths hyp_ts
- concl_t =
+fun relevant_facts ctxt full_types (threshold0, threshold1) max_relevant 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))
@@ -813,7 +826,7 @@
maps (map (fn ((name, loc), th) => ((K name, loc), (true, th)))
o name_thm_pairs_from_ref ctxt reserved chained_ths) add
else
- all_name_thms_pairs ctxt reserved full_types add_ths chained_ths)
+ all_name_thms_pairs ctxt reserved full_types fudge add_ths chained_ths)
|> name_thm_pairs ctxt (respect_no_atp andalso not only)
|> uniquify
in
@@ -825,8 +838,8 @@
max_relevant = 0 then
[]
else
- relevance_filter ctxt threshold0 decay max_relevant relevance_override
- axioms (concl_t :: hyp_ts))
+ relevance_filter ctxt threshold0 decay max_relevant fudge override axioms
+ (concl_t :: hyp_ts))
|> map (apfst (apfst (fn f => f ())))
end