--- a/src/HOL/IsaMakefile Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/IsaMakefile Wed Jul 18 08:44:03 2012 +0200
@@ -372,7 +372,6 @@
Tools/semiring_normalizer.ML \
Tools/Sledgehammer/async_manager.ML \
Tools/Sledgehammer/sledgehammer_fact.ML \
- Tools/Sledgehammer/sledgehammer_filter.ML \
Tools/Sledgehammer/sledgehammer_filter_iter.ML \
Tools/Sledgehammer/sledgehammer_filter_mash.ML \
Tools/Sledgehammer/sledgehammer_minimize.ML \
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Jul 18 08:44:03 2012 +0200
@@ -423,7 +423,7 @@
term_order |> the_default I)
#> (Option.map (Config.put ATP_Systems.force_sos)
force_sos |> the_default I))
- val params as {relevance_thresholds, max_relevant, slice, ...} =
+ val params as {max_relevant, slice, ...} =
Sledgehammer_Isar.default_params ctxt
([("verbose", "true"),
("type_enc", type_enc),
@@ -442,11 +442,6 @@
prover_name
val is_appropriate_prop =
Sledgehammer_Provers.is_appropriate_prop_for_prover ctxt prover_name
- val is_built_in_const =
- Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name
- val relevance_fudge =
- Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name
- val relevance_override = {add = [], del = [], only = false}
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
val time_limit =
(case hard_timeout of
@@ -465,13 +460,13 @@
else raise Fail "inappropriate"
val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover_name
val facts =
- Sledgehammer_Fact.nearly_all_facts ctxt ho_atp relevance_override
- chained_ths hyp_ts concl_t
+ Sledgehammer_Fact.nearly_all_facts ctxt ho_atp
+ Sledgehammer_Fact.no_relevance_override chained_ths hyp_ts concl_t
|> filter (is_appropriate_prop o prop_of o snd)
- |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
+ |> Sledgehammer_Filter_MaSh.relevant_facts ctxt params prover_name
(the_default default_max_relevant max_relevant)
- is_built_in_const relevance_fudge relevance_override
- chained_ths hyp_ts concl_t
+ Sledgehammer_Fact.no_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 Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Jul 18 08:44:03 2012 +0200
@@ -113,7 +113,7 @@
val {context = ctxt, facts = chained_ths, goal} = Proof.goal pre
val prover = AList.lookup (op =) args "prover"
|> the_default default_prover
- val {relevance_thresholds, max_relevant, slice, ...} =
+ val params as {max_relevant, slice, ...} =
Sledgehammer_Isar.default_params ctxt args
val default_max_relevant =
Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice
@@ -121,22 +121,19 @@
val is_appropriate_prop =
Sledgehammer_Provers.is_appropriate_prop_for_prover ctxt
default_prover
- val is_built_in_const =
- Sledgehammer_Provers.is_built_in_const_for_prover ctxt default_prover
val relevance_fudge =
extract_relevance_fudge args
(Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover)
- val relevance_override = {add = [], del = [], only = false}
val subgoal = 1
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal subgoal
val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
val facts =
- Sledgehammer_Fact.nearly_all_facts ctxt ho_atp relevance_override
- chained_ths hyp_ts concl_t
+ Sledgehammer_Fact.nearly_all_facts ctxt ho_atp
+ Sledgehammer_Fact.no_relevance_override chained_ths hyp_ts concl_t
|> filter (is_appropriate_prop o prop_of o snd)
- |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
- (the_default default_max_relevant max_relevant)
- is_built_in_const relevance_fudge relevance_override
+ |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
+ default_prover (the_default default_max_relevant max_relevant)
+ (SOME relevance_fudge) Sledgehammer_Fact.no_relevance_override
chained_ths hyp_ts concl_t
|> map (fst o fst)
val (found_facts, lost_facts) =
--- a/src/HOL/Sledgehammer.thy Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Sledgehammer.thy Wed Jul 18 08:44:03 2012 +0200
@@ -12,11 +12,10 @@
uses "Tools/Sledgehammer/async_manager.ML"
"Tools/Sledgehammer/sledgehammer_util.ML"
"Tools/Sledgehammer/sledgehammer_fact.ML"
- "Tools/Sledgehammer/sledgehammer_filter_iter.ML"
"Tools/Sledgehammer/sledgehammer_provers.ML"
"Tools/Sledgehammer/sledgehammer_minimize.ML"
+ "Tools/Sledgehammer/sledgehammer_filter_iter.ML"
"Tools/Sledgehammer/sledgehammer_filter_mash.ML"
- "Tools/Sledgehammer/sledgehammer_filter.ML"
"Tools/Sledgehammer/sledgehammer_run.ML"
"Tools/Sledgehammer/sledgehammer_isar.ML"
begin
--- a/src/HOL/TPTP/sledgehammer_tactics.ML Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/TPTP/sledgehammer_tactics.ML Wed Jul 18 08:44:03 2012 +0200
@@ -26,24 +26,20 @@
let
val mode = Sledgehammer_Provers.Normal
val chained_ths = [] (* a tactic has no chained ths *)
- val params as {provers, relevance_thresholds, max_relevant, slice, ...} =
+ val params as {provers, max_relevant, slice, ...} =
Sledgehammer_Isar.default_params ctxt override_params
val name = hd provers
val prover = Sledgehammer_Provers.get_prover ctxt mode name
val default_max_relevant =
Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice name
- val is_built_in_const =
- Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
- val relevance_fudge =
- Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
val facts =
Sledgehammer_Fact.nearly_all_facts ctxt ho_atp relevance_override
chained_ths hyp_ts concl_t
- |> Sledgehammer_Filter_MaSh.relevant_facts ctxt relevance_thresholds
- (the_default default_max_relevant max_relevant) is_built_in_const
- relevance_fudge relevance_override chained_ths hyp_ts concl_t
+ |> Sledgehammer_Filter_MaSh.relevant_facts ctxt params name
+ (the_default default_max_relevant max_relevant) relevance_override
+ chained_ths hyp_ts concl_t
val problem =
{state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
facts = map Sledgehammer_Provers.Untranslated_Fact facts}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Jul 18 08:44:03 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_filter.ML
- Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
- Author: Jasmin Blanchette, TU Muenchen
-
-Sledgehammer's hybrid relevance filter.
-*)
-
-signature SLEDGEHAMMER_FILTER =
-sig
- type stature = ATP_Problem_Generate.stature
- type relevance_fudge = Sledgehammer_Filter_Iter.relevance_fudge
- type relevance_override = Sledgehammer_Filter_Iter.relevance_override
-
- val relevant_facts :
- Proof.context -> real * real -> int
- -> (string * typ -> term list -> bool * term list) -> relevance_fudge
- -> relevance_override -> thm list -> term list -> term
- -> (((unit -> string) * stature) * thm) list
- -> ((string * stature) * thm) list
-end;
-
-structure Sledgehammer_Filter : SLEDGEHAMMER_FILTER =
-struct
-
-open Sledgehammer_Filter_Iter
-
-val relevant_facts = iterative_relevant_facts
-
-end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML Wed Jul 18 08:44:03 2012 +0200
@@ -9,27 +9,8 @@
sig
type stature = ATP_Problem_Generate.stature
type relevance_override = Sledgehammer_Fact.relevance_override
-
- type relevance_fudge =
- {local_const_multiplier : real,
- 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,
- 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 params = Sledgehammer_Provers.params
+ type relevance_fudge = Sledgehammer_Provers.relevance_fudge
val trace : bool Config.T
val pseudo_abs_name : string
@@ -38,8 +19,7 @@
theory -> (string * typ -> term list -> bool * term list) -> term
-> string list
val iterative_relevant_facts :
- Proof.context -> real * real -> int
- -> (string * typ -> term list -> bool * term list) -> relevance_fudge
+ Proof.context -> params -> string -> int -> relevance_fudge option
-> relevance_override -> thm list -> term list -> term
-> (((unit -> string) * stature) * thm) list
-> ((string * stature) * thm) list
@@ -50,32 +30,12 @@
open ATP_Problem_Generate
open Sledgehammer_Fact
+open Sledgehammer_Provers
val trace =
Attrib.setup_config_bool @{binding sledgehammer_filter_trace} (K false)
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
-type relevance_fudge =
- {local_const_multiplier : real,
- 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,
- 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 sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
val pseudo_abs_name = sledgehammer_prefix ^ "abs"
val pseudo_skolem_prefix = sledgehammer_prefix ^ "sko"
@@ -436,9 +396,9 @@
facts are included. *)
val special_fact_index = 75
-fun relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
+fun relevance_filter ctxt thres0 decay max_relevant is_built_in_const
(fudge as {threshold_divisor, ridiculous_threshold, ...})
- ({add, del, ...} : relevance_override) facts chained_ts hyp_ts concl_t =
+ ({del, ...} : relevance_override) facts chained_ts hyp_ts concl_t =
let
val thy = Proof_Context.theory_of ctxt
val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty
@@ -450,16 +410,15 @@
|> (fn tab => if Symtab.is_empty tab then chained_const_tab else tab)
|> fold (if_empty_replace_with_scope thy is_built_in_const facts)
[Chained, Assum, Local]
- val add_ths = Attrib.eval_thms ctxt add
val del_ths = Attrib.eval_thms ctxt del
val facts = facts |> filter_out (member Thm.eq_thm_prop del_ths o snd)
- fun iter j remaining_max threshold rel_const_tab hopeless hopeful =
+ fun iter j remaining_max thres rel_const_tab hopeless hopeful =
let
fun relevant [] _ [] =
(* Nothing has been added this iteration. *)
- if j = 0 andalso threshold >= ridiculous_threshold then
+ if j = 0 andalso thres >= ridiculous_threshold then
(* First iteration? Try again. *)
- iter 0 max_relevant (threshold / threshold_divisor) rel_const_tab
+ iter 0 max_relevant (thres / threshold_divisor) rel_const_tab
hopeless hopeful
else
[]
@@ -484,8 +443,8 @@
|> map (fn (ax as (_, consts), old_weight) =>
(ax, if exists is_dirty consts then NONE
else SOME old_weight)))
- val threshold =
- 1.0 - (1.0 - threshold)
+ val thres =
+ 1.0 - (1.0 - thres)
* Math.pow (decay, Real.fromInt (length accepts))
val remaining_max = remaining_max - length accepts
in
@@ -497,7 +456,7 @@
(if remaining_max = 0 then
[]
else
- iter (j + 1) remaining_max threshold rel_const_tab'
+ iter (j + 1) remaining_max thres rel_const_tab'
hopeless_rejects hopeful_rejects)
end
| relevant candidates rejects
@@ -510,7 +469,7 @@
| NONE => fact_weight fudge stature const_tab rel_const_tab
chained_const_tab fact_consts
in
- if weight >= threshold then
+ if weight >= thres then
relevant ((ax, weight) :: candidates) rejects hopeful
else
relevant candidates ((ax, weight) :: rejects) hopeful
@@ -518,16 +477,12 @@
in
trace_msg ctxt (fn () =>
"ITERATION " ^ string_of_int j ^ ": current threshold: " ^
- Real.toString threshold ^ ", constants: " ^
+ Real.toString thres ^ ", constants: " ^
commas (rel_const_tab |> Symtab.dest
|> filter (curry (op <>) [] o snd)
|> map string_for_hyper_pconst));
relevant [] [] hopeful
end
- fun prepend_facts ths accepts =
- ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
- (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
- |> take max_relevant
fun uses_const s t =
fold_aterms (curry (fn (Const (s', _), false) => s' = s | (_, b) => b)) t
false
@@ -552,30 +507,34 @@
|> insert_into_facts accepts
in
facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)
- |> iter 0 max_relevant threshold0 goal_const_tab []
- |> not (null add_ths) ? prepend_facts add_ths
+ |> iter 0 max_relevant thres0 goal_const_tab []
|> insert_special_facts
|> tap (fn accepts => trace_msg ctxt (fn () =>
"Total relevant: " ^ string_of_int (length accepts)))
end
-fun iterative_relevant_facts ctxt (threshold0, threshold1) max_relevant
- is_built_in_const fudge (override as {only, ...})
- chained_ths hyp_ts concl_t facts =
+fun iterative_relevant_facts ctxt
+ ({relevance_thresholds = (thres0, thres1), ...} : params) prover
+ max_relevant fudge override chained_ths hyp_ts concl_t facts =
let
val thy = Proof_Context.theory_of ctxt
- val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
+ val is_built_in_const =
+ Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover
+ val fudge =
+ case fudge of
+ SOME fudge => fudge
+ | NONE => Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover
+ val decay = Math.pow ((1.0 - thres1) / (1.0 - thres0),
1.0 / Real.fromInt (max_relevant + 1))
in
trace_msg ctxt (fn () => "Considering " ^ string_of_int (length facts) ^
" facts");
- (if only orelse threshold1 < 0.0 then
+ (if thres1 < 0.0 then
facts
- else if threshold0 > 1.0 orelse threshold0 > threshold1 orelse
- max_relevant = 0 then
+ else if thres0 > 1.0 orelse thres0 > thres1 then
[]
else
- relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
+ relevance_filter ctxt thres0 decay max_relevant is_built_in_const
fudge override facts (chained_ths |> map prop_of) hyp_ts
(concl_t |> theory_constify fudge (Context.theory_name thy)))
|> map (apfst (apfst (fn f => f ())))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:03 2012 +0200
@@ -9,6 +9,8 @@
type status = ATP_Problem_Generate.status
type stature = ATP_Problem_Generate.stature
type params = Sledgehammer_Provers.params
+ type relevance_override = Sledgehammer_Fact.relevance_override
+ type relevance_fudge = Sledgehammer_Provers.relevance_fudge
type prover_result = Sledgehammer_Provers.prover_result
val fact_name_of : string -> string
@@ -36,10 +38,16 @@
Proof.context -> params -> theory -> bool -> string -> unit
val reset : unit -> unit
- val can_suggest : unit -> bool
+ val can_suggest_facts : unit -> bool
+(* ### val suggest_facts : ... *)
val can_learn_thy : theory -> bool
val learn_thy : theory -> real -> unit
val learn_proof : theory -> term -> thm list -> unit
+
+ val relevant_facts :
+ Proof.context -> params -> string -> int -> relevance_override -> thm list
+ -> term list -> term -> (((unit -> string) * stature) * thm) list
+ -> ((string * stature) * thm) list
end;
structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH =
@@ -247,20 +255,10 @@
fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init
-fun iter_facts ctxt ({provers, relevance_thresholds, ...} : params) max_relevant
- goal =
- let
- val prover_name = hd provers
- val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
- val is_built_in_const =
- Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name
- val relevance_fudge =
- Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name
- val relevance_override = {add = [], del = [], only = false}
- in
- iterative_relevant_facts ctxt relevance_thresholds max_relevant
- is_built_in_const relevance_fudge
- relevance_override [] hyp_ts concl_t
+fun iter_facts ctxt (params as {provers, ...}) max_relevant goal =
+ let val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 in
+ iterative_relevant_facts ctxt params (hd provers) max_relevant NONE
+ no_relevance_override [] hyp_ts concl_t
end
fun run_prover ctxt (params as {provers, ...}) facts goal =
@@ -377,7 +375,7 @@
fun reset () =
()
-fun can_suggest () =
+fun can_suggest_facts () =
true
fun can_learn_thy thy =
@@ -386,7 +384,27 @@
fun learn_thy thy timeout =
()
-fun learn_proof theory t thms =
+fun learn_proof thy t thms =
()
+fun relevant_facts ctxt params prover max_relevant
+ (override as {add, only, ...}) chained_ths hyp_ts concl_t
+ facts =
+ if only then
+ facts |> map (apfst (apfst (fn f => f ()))) (* ###*)
+ else if max_relevant <= 0 then
+ []
+ else
+ let
+ val add_ths = Attrib.eval_thms ctxt add
+ fun prepend_facts ths facts =
+ ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
+ (facts |> filter_out (member Thm.eq_thm_prop ths o snd)))
+ |> take max_relevant
+ in
+ iterative_relevant_facts ctxt params prover max_relevant NONE override
+ chained_ths hyp_ts concl_t facts
+ |> not (null add_ths) ? prepend_facts add_ths
+ end
+
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jul 18 08:44:03 2012 +0200
@@ -14,7 +14,6 @@
type reconstructor = ATP_Proof_Reconstruct.reconstructor
type play = ATP_Proof_Reconstruct.play
type minimize_command = ATP_Proof_Reconstruct.minimize_command
- type relevance_fudge = Sledgehammer_Filter_Iter.relevance_fudge
datatype mode = Auto_Try | Try | Normal | Auto_Minimize | Minimize
@@ -40,6 +39,27 @@
preplay_timeout: Time.time,
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,
+ skolem_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}
+
datatype prover_fact =
Untranslated_Fact of (string * stature) * thm |
SMT_Weighted_Fact of (string * stature) * (int option * thm)
@@ -124,7 +144,7 @@
open ATP_Proof_Reconstruct
open Metis_Tactic
open Sledgehammer_Util
-open Sledgehammer_Filter_Iter
+
(** The Sledgehammer **)
@@ -281,6 +301,7 @@
fun running_provers () = Async_Manager.running_threads das_tool "prover"
val messages = Async_Manager.thread_messages das_tool "prover"
+
(** problems, results, ATPs, etc. **)
type params =
@@ -305,6 +326,27 @@
preplay_timeout: Time.time,
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,
+ skolem_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}
+
datatype prover_fact =
Untranslated_Fact of (string * stature) * thm |
SMT_Weighted_Fact of (string * stature) * (int option * thm)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Jul 18 08:44:03 2012 +0200
@@ -9,7 +9,7 @@
signature SLEDGEHAMMER_RUN =
sig
type minimize_command = ATP_Proof_Reconstruct.minimize_command
- type relevance_override = Sledgehammer_Filter.relevance_override
+ type relevance_override = Sledgehammer_Fact.relevance_override
type mode = Sledgehammer_Provers.mode
type params = Sledgehammer_Provers.params
@@ -33,7 +33,7 @@
open Sledgehammer_Fact
open Sledgehammer_Provers
open Sledgehammer_Minimize
-open Sledgehammer_Filter
+open Sledgehammer_Filter_MaSh
val someN = "some"
val noneN = "none"
@@ -156,8 +156,7 @@
val auto_try_max_relevant_divisor = 2 (* FUDGE *)
fun run_sledgehammer (params as {debug, verbose, blocking, provers,
- relevance_thresholds, max_relevant, slice,
- ...})
+ max_relevant, slice, ...})
mode i (relevance_override as {only, ...}) minimize_command state =
if null provers then
error "No prover is set."
@@ -208,7 +207,7 @@
(launch problem #> fst)
|> max_outcome_code |> rpair state
end
- fun get_facts label is_appropriate_prop relevance_fudge provers =
+ fun get_facts label is_appropriate_prop provers =
let
val max_max_relevant =
case max_relevant of
@@ -219,16 +218,13 @@
provers
|> mode = Auto_Try
? (fn n => n div auto_try_max_relevant_divisor)
- val is_built_in_const =
- is_built_in_const_for_prover ctxt (hd provers)
in
facts
|> (case is_appropriate_prop of
SOME is_app => filter (is_app o prop_of o snd)
| NONE => I)
- |> relevant_facts ctxt relevance_thresholds max_max_relevant
- is_built_in_const relevance_fudge relevance_override
- chained_ths hyp_ts concl_t
+ |> relevant_facts ctxt params (hd provers) max_max_relevant
+ relevance_override chained_ths hyp_ts concl_t
|> tap (fn facts =>
if debug then
label ^ plural_s (length provers) ^ ": " ^
@@ -255,15 +251,14 @@
();
accum)
else
- launch_provers state
- (get_facts label is_appropriate_prop atp_relevance_fudge o K atps)
- (K (Untranslated_Fact o fst)) atps
+ launch_provers state (get_facts label is_appropriate_prop o K atps)
+ (K (Untranslated_Fact o fst)) atps
fun launch_smts accum =
if null smts then
accum
else
let
- val facts = get_facts "SMT solver" NONE smt_relevance_fudge smts
+ val facts = get_facts "SMT solver" NONE smts
val weight = SMT_Weighted_Fact oo weight_smt_fact ctxt
in
smts |> map (`(class_of_smt_solver ctxt))