generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
--- 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,
--- 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
--- 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
--- 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