# HG changeset patch # User blanchet # Date 1342593843 -7200 # Node ID 255c6e1fd5051f21ce4b4b021381a36144b942b3 # Parent 61acb731b4a2602c2eed363cb87a96c399aa256e rationalize relevance filter, slowing moving code from Iter to MaSh diff -r 61acb731b4a2 -r 255c6e1fd505 src/HOL/IsaMakefile --- 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 \ diff -r 61acb731b4a2 -r 255c6e1fd505 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.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, diff -r 61acb731b4a2 -r 255c6e1fd505 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- 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) = diff -r 61acb731b4a2 -r 255c6e1fd505 src/HOL/Sledgehammer.thy --- 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 diff -r 61acb731b4a2 -r 255c6e1fd505 src/HOL/TPTP/sledgehammer_tactics.ML --- 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} diff -r 61acb731b4a2 -r 255c6e1fd505 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- 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; diff -r 61acb731b4a2 -r 255c6e1fd505 src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML --- 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 ()))) diff -r 61acb731b4a2 -r 255c6e1fd505 src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML --- 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; diff -r 61acb731b4a2 -r 255c6e1fd505 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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) diff -r 61acb731b4a2 -r 255c6e1fd505 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- 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))