# HG changeset patch # User blanchet # Date 1342593843 -7200 # Node ID 914ca082780450e2ce25cc251f313cfe5e80647d # Parent 7fcee834c7f57e76c412a5db83d741a8dc91e453 renamed Sledgehammer options diff -r 7fcee834c7f5 -r 914ca0827804 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 @@ -22,6 +22,7 @@ val reconstructorK = "reconstructor" (*=NAME: how to reconstruct proofs (ie. using metis/smt)*) val metis_ftK = "metis_ft" (*: apply metis with fully-typed encoding to the theorems found by sledgehammer*) +val max_factsK = "max_facts" (*=NUM: max. relevant clauses to use*) val max_relevantK = "max_relevant" (*=NUM: max. relevant clauses to use*) val max_callsK = "max_calls" (*=NUM: max. no. of calls to sledgehammer*) val preplay_timeoutK = "preplay_timeout" (*=TIME: timeout for finding reconstructed proof*) @@ -53,7 +54,7 @@ val uncurried_aliases_default = "smart" val type_enc_default = "smart" val strict_default = "false" -val max_relevant_default = "smart" +val max_facts_default = "smart" val slice_default = "true" val max_calls_default = "10000000" val trivial_default = "false" @@ -398,7 +399,7 @@ SH_FAIL of int * int | SH_ERROR -fun run_sh prover_name prover type_enc strict max_relevant slice lam_trans +fun run_sh prover_name prover type_enc strict max_facts slice lam_trans uncurried_aliases e_selection_heuristic term_order force_sos hard_timeout timeout preplay_timeout sh_minimizeLST max_new_mono_instancesLST max_mono_itersLST dir pos st = @@ -423,23 +424,22 @@ term_order |> the_default I) #> (Option.map (Config.put ATP_Systems.force_sos) force_sos |> the_default I)) - val params as {max_relevant, slice, ...} = + val params as {max_facts, slice, ...} = Sledgehammer_Isar.default_params ctxt ([("verbose", "true"), ("type_enc", type_enc), ("strict", strict), ("lam_trans", lam_trans |> the_default lam_trans_default), ("uncurried_aliases", uncurried_aliases |> the_default uncurried_aliases_default), - ("max_relevant", max_relevant), + ("max_facts", max_facts), ("slice", slice), ("timeout", string_of_int timeout), ("preplay_timeout", preplay_timeout)] |> sh_minimizeLST (*don't confuse the two minimization flags*) |> max_new_mono_instancesLST |> max_mono_itersLST) - val default_max_relevant = - Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice - prover_name + val default_max_facts = + Sledgehammer_Provers.default_max_facts_for_prover ctxt slice prover_name val is_appropriate_prop = Sledgehammer_Provers.is_appropriate_prop_for_prover ctxt prover_name val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i @@ -464,7 +464,7 @@ Sledgehammer_Fact.no_fact_override chained_ths hyp_ts concl_t |> filter (is_appropriate_prop o prop_of o snd) |> Sledgehammer_Filter_MaSh.relevant_facts ctxt params prover_name - (the_default default_max_relevant max_relevant) + (the_default default_max_facts max_facts) Sledgehammer_Fact.no_fact_override hyp_ts concl_t val problem = {state = st', goal = goal, subgoal = i, @@ -507,7 +507,12 @@ val (prover_name, prover) = get_prover (Proof.context_of st) args val type_enc = AList.lookup (op =) args type_encK |> the_default type_enc_default val strict = AList.lookup (op =) args strictK |> the_default strict_default - val max_relevant = AList.lookup (op =) args max_relevantK |> the_default max_relevant_default + val max_facts = + case AList.lookup (op =) args max_factsK of + SOME max => max + | NONE => case AList.lookup (op =) args max_relevantK of + SOME max => max + | NONE => max_facts_default val slice = AList.lookup (op =) args sliceK |> the_default slice_default val lam_trans = AList.lookup (op =) args lam_transK val uncurried_aliases = AList.lookup (op =) args uncurried_aliasesK @@ -527,7 +532,7 @@ val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK val hard_timeout = SOME (2 * timeout) val (msg, result) = - run_sh prover_name prover type_enc strict max_relevant slice lam_trans + run_sh prover_name prover type_enc strict max_facts slice lam_trans uncurried_aliases e_selection_heuristic term_order force_sos hard_timeout timeout preplay_timeout sh_minimizeLST max_new_mono_instancesLST max_mono_itersLST dir pos st @@ -611,7 +616,7 @@ fun override_params prover type_enc timeout = [("provers", prover), - ("max_relevant", "0"), + ("max_facts", "0"), ("type_enc", type_enc), ("strict", "true"), ("slice", "false"), diff -r 7fcee834c7f5 -r 914ca0827804 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,11 +113,10 @@ val {context = ctxt, facts = chained_ths, goal} = Proof.goal pre val prover = AList.lookup (op =) args "prover" |> the_default default_prover - val params as {max_relevant, slice, ...} = + val params as {max_facts, slice, ...} = Sledgehammer_Isar.default_params ctxt args - val default_max_relevant = - Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice - prover + val default_max_facts = + Sledgehammer_Provers.default_max_facts_for_prover ctxt slice prover val is_appropriate_prop = Sledgehammer_Provers.is_appropriate_prop_for_prover ctxt default_prover @@ -132,7 +131,7 @@ Sledgehammer_Fact.no_fact_override chained_ths hyp_ts concl_t |> filter (is_appropriate_prop o prop_of o snd) |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params - default_prover (the_default default_max_relevant max_relevant) + default_prover (the_default default_max_facts max_facts) (SOME relevance_fudge) hyp_ts concl_t |> map ((fn name => name ()) o fst o fst) val (found_facts, lost_facts) = diff -r 7fcee834c7f5 -r 914ca0827804 src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:03 2012 +0200 +++ b/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:03 2012 +0200 @@ -36,11 +36,11 @@ val mashN = "MaSh" val iter_mashN = "Iter+MaSh" -val max_relevant_slack = 2 +val max_facts_slack = 2 fun evaluate_mash_suggestions ctxt params thy file_name = let - val {provers, max_relevant, slice, type_enc, lam_trans, timeout, ...} = + val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = Sledgehammer_Isar.default_params ctxt [] val prover_name = hd provers val path = file_name |> Path.explode @@ -55,7 +55,7 @@ find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts fun sugg_facts hyp_ts concl_t facts = map_filter (find_sugg facts o of_fact_name) - #> take (max_relevant_slack * the max_relevant) + #> take (max_facts_slack * the max_facts) #> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t fun hybrid_facts fsp = let @@ -70,7 +70,7 @@ in union fact_eq fs1 fs2 |> map (`score_of) |> sort (int_ord o pairself fst) |> map snd - |> take (the max_relevant) + |> take (the max_facts) |> map (apfst (apfst K)) end fun with_index facts s = (find_index (curry (op =) s) facts + 1, s) @@ -84,20 +84,19 @@ |> sort (int_ord o pairself fst) |> map index_string |> space_implode " ") ^ - (if length facts < the max_relevant then + (if length facts < the max_facts then " (of " ^ string_of_int (length facts) ^ ")" else "") else "Failure: " ^ - (facts |> take (the max_relevant) - |> tag_list 1 + (facts |> take (the max_facts) |> tag_list 1 |> map index_string |> space_implode " ")) end fun prove ok heading facts goal = let - val facts = facts |> take (the max_relevant) + val facts = facts |> take (the max_facts) val res as {outcome, ...} = run_prover ctxt params facts goal val _ = if is_none outcome then ok := !ok + 1 else () in str_of_res heading facts res end @@ -115,8 +114,8 @@ val isa_facts = sugg_facts hyp_ts concl_t facts isa_deps val iter_facts = Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params - prover_name (max_relevant_slack * the max_relevant) NONE hyp_ts - concl_t facts + prover_name (max_facts_slack * the max_facts) NONE hyp_ts concl_t + facts val mash_facts = sugg_facts hyp_ts concl_t facts suggs val iter_mash_facts = hybrid_facts (iter_facts, mash_facts) val iter_s = prove iter_ok iterN iter_facts goal @@ -139,7 +138,7 @@ (100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)" val inst_inducts = Config.get ctxt Sledgehammer_Fact.instantiate_inducts val options = - [prover_name, string_of_int (the max_relevant) ^ " facts", + [prover_name, string_of_int (the max_facts) ^ " facts", "slice" |> not slice ? prefix "dont_", the_default "smart" type_enc, the_default "smart" lam_trans, ATP_Util.string_from_time timeout, "instantiate_inducts" |> not inst_inducts ? prefix "dont_"] diff -r 7fcee834c7f5 -r 914ca0827804 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 @@ -23,20 +23,20 @@ fun run_prover override_params fact_override i n ctxt goal = let val mode = Sledgehammer_Provers.Normal - val params as {provers, max_relevant, slice, ...} = + val params as {provers, max_facts, 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 default_max_facts = + Sledgehammer_Provers.default_max_facts_for_prover ctxt slice 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 fact_override [] hyp_ts concl_t |> Sledgehammer_Filter_MaSh.relevant_facts ctxt params name - (the_default default_max_relevant max_relevant) fact_override - hyp_ts concl_t + (the_default default_max_facts max_facts) fact_override hyp_ts + concl_t val problem = {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, facts = facts |> map (apfst (apfst (fn name => name ()))) diff -r 7fcee834c7f5 -r 914ca0827804 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 @@ -336,14 +336,14 @@ type annotated_thm = (((unit -> string) * stature) * thm) * (string * ptype) list -fun take_most_relevant ctxt max_relevant remaining_max +fun take_most_relevant ctxt max_facts remaining_max ({max_imperfect, max_imperfect_exp, ...} : relevance_fudge) (candidates : (annotated_thm * real) list) = let val max_imperfect = Real.ceil (Math.pow (max_imperfect, Math.pow (Real.fromInt remaining_max - / Real.fromInt max_relevant, max_imperfect_exp))) + / Real.fromInt max_facts, max_imperfect_exp))) val (perfect, imperfect) = candidates |> sort (Real.compare o swap o pairself snd) |> take_prefix (fn (_, w) => w > 0.99999) @@ -393,7 +393,7 @@ facts are included. *) val special_fact_index = 75 -fun relevance_filter ctxt thres0 decay max_relevant is_built_in_const +fun relevance_filter ctxt thres0 decay max_facts is_built_in_const (fudge as {threshold_divisor, ridiculous_threshold, ...}) facts hyp_ts concl_t = let @@ -416,15 +416,14 @@ (* Nothing has been added this iteration. *) if j = 0 andalso thres >= ridiculous_threshold then (* First iteration? Try again. *) - iter 0 max_relevant (thres / threshold_divisor) rel_const_tab + iter 0 max_facts (thres / threshold_divisor) rel_const_tab hopeless hopeful else [] | relevant candidates rejects [] = let val (accepts, more_rejects) = - take_most_relevant ctxt max_relevant remaining_max fudge - candidates + take_most_relevant ctxt max_facts remaining_max fudge candidates val rel_const_tab' = rel_const_tab |> fold (add_pconst_to_table false) (maps (snd o fst) accepts) @@ -495,7 +494,7 @@ val add = facts |> filter (member Thm.eq_thm_prop ths o snd) val (bef, after) = accepts |> filter_out (member Thm.eq_thm_prop ths o snd) - |> take (max_relevant - length add) + |> take (max_facts - length add) |> chop special_fact_index in bef @ add @ after end fun insert_special_facts accepts = @@ -505,15 +504,15 @@ |> insert_into_facts accepts in facts |> map_filter (pair_consts_fact thy is_built_in_const fudge) - |> iter 0 max_relevant thres0 goal_const_tab [] + |> iter 0 max_facts 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 - ({relevance_thresholds = (thres0, thres1), ...} : params) prover - max_relevant fudge hyp_ts concl_t facts = + ({fact_thresholds = (thres0, thres1), ...} : params) prover + max_facts fudge hyp_ts concl_t facts = let val thy = Proof_Context.theory_of ctxt val is_built_in_const = @@ -523,7 +522,7 @@ 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)) + 1.0 / Real.fromInt (max_facts + 1)) in trace_msg ctxt (fn () => "Considering " ^ string_of_int (length facts) ^ " facts"); @@ -532,8 +531,8 @@ else if thres0 > 1.0 orelse thres0 > thres1 then [] else - relevance_filter ctxt thres0 decay max_relevant is_built_in_const - fudge facts hyp_ts + relevance_filter ctxt thres0 decay max_facts is_built_in_const fudge + facts hyp_ts (concl_t |> theory_constify fudge (Context.theory_name thy))) end diff -r 7fcee834c7f5 -r 914ca0827804 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 @@ -313,7 +313,7 @@ in File.append path s end in List.app do_thm ths end -fun generate_atp_dependencies ctxt (params as {provers, max_relevant, ...}) thy +fun generate_atp_dependencies ctxt (params as {provers, max_facts, ...}) thy include_thy file_name = let val path = file_name |> Path.explode @@ -347,7 +347,7 @@ facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) val facts = facts |> iterative_relevant_facts ctxt params (hd provers) - (the max_relevant) NONE hyp_ts concl_t + (the max_facts) NONE hyp_ts concl_t |> fold (add_isa_dep facts) isa_deps |> map fix_name in @@ -378,11 +378,11 @@ fun learn_proof thy t ths = () -fun relevant_facts ctxt params prover max_relevant - ({add, only, ...} : fact_override) hyp_ts concl_t facts = +fun relevant_facts ctxt params prover max_facts + ({add, only, ...} : fact_override) hyp_ts concl_t facts = if only then facts - else if max_relevant <= 0 then + else if max_facts <= 0 then [] else let @@ -390,10 +390,11 @@ 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 + |> take max_facts in - iterative_relevant_facts ctxt params prover max_relevant NONE - hyp_ts concl_t facts + facts + |> iterative_relevant_facts ctxt params prover max_facts NONE hyp_ts + concl_t |> not (null add_ths) ? prepend_facts add_ths end diff -r 7fcee834c7f5 -r 914ca0827804 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 18 08:44:03 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 18 08:44:03 2012 +0200 @@ -82,8 +82,8 @@ ("strict", "false"), ("lam_trans", "smart"), ("uncurried_aliases", "smart"), - ("relevance_thresholds", "0.45 0.85"), - ("max_relevant", "smart"), + ("fact_thresholds", "0.45 0.85"), + ("max_facts", "smart"), ("max_mono_iters", "smart"), ("max_new_mono_instances", "smart"), ("isar_proof", "false"), @@ -93,7 +93,8 @@ ("preplay_timeout", "3")] val alias_params = - [("prover", ("provers", [])), + [("prover", ("provers", [])), (* legacy *) + ("max_relevant", ("max_facts", [])), (* legacy *) ("dont_preplay", ("preplay_timeout", ["0"]))] val negated_alias_params = [("no_debug", "debug"), @@ -288,8 +289,8 @@ val strict = mode = Auto_Try orelse lookup_bool "strict" val lam_trans = lookup_option lookup_string "lam_trans" val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases" - val relevance_thresholds = lookup_real_pair "relevance_thresholds" - val max_relevant = lookup_option lookup_int "max_relevant" + val fact_thresholds = lookup_real_pair "fact_thresholds" + val max_facts = lookup_option lookup_int "max_facts" val max_mono_iters = lookup_option lookup_int "max_mono_iters" val max_new_mono_instances = lookup_option lookup_int "max_new_mono_instances" @@ -308,7 +309,7 @@ {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking, provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, - relevance_thresholds = relevance_thresholds, max_relevant = max_relevant, + fact_thresholds = fact_thresholds, max_facts = max_facts, max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, slice = slice, @@ -405,12 +406,12 @@ val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) [] val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse_Spec.xthm) -val parse_relevance_chunk = +val parse_fact_override_chunk = (Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override) || (Args.del |-- Args.colon |-- parse_fact_refs >> del_fact_override) || (parse_fact_refs >> only_fact_override) val parse_fact_override = - Scan.optional (Args.parens (Scan.repeat parse_relevance_chunk + Scan.optional (Args.parens (Scan.repeat parse_fact_override_chunk >> merge_fact_overrides)) no_fact_override diff -r 7fcee834c7f5 -r 914ca0827804 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Jul 18 08:44:03 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Jul 18 08:44:03 2012 +0200 @@ -68,7 +68,7 @@ {debug = debug, verbose = verbose, overlord = overlord, blocking = true, provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, - relevance_thresholds = (1.01, 1.01), max_relevant = SOME (length facts), + fact_thresholds = (1.01, 1.01), max_facts = SOME (length facts), max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, slice = false, @@ -225,7 +225,7 @@ fun adjust_reconstructor_params override_params ({debug, verbose, overlord, blocking, provers, type_enc, strict, - lam_trans, uncurried_aliases, relevance_thresholds, max_relevant, + lam_trans, uncurried_aliases, fact_thresholds, max_facts, max_mono_iters, max_new_mono_instances, isar_proof, isar_shrink_factor, slice, minimize, timeout, preplay_timeout, expect} : params) = let @@ -241,7 +241,7 @@ {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking, provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, - max_relevant = max_relevant, relevance_thresholds = relevance_thresholds, + max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, slice = slice, @@ -304,8 +304,8 @@ case used_facts of SOME used_facts => (if debug andalso not (null used_facts) then - facts ~~ (0 upto length facts - 1) - |> map (fn (fact, j) => fact |> untranslated_fact |> apsnd (K j)) + tag_list 1 facts + |> map (fn (j, fact) => fact |> untranslated_fact |> apsnd (K j)) |> filter_used_facts used_facts |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) |> commas diff -r 7fcee834c7f5 -r 914ca0827804 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 @@ -27,8 +27,8 @@ strict: bool, lam_trans: string option, uncurried_aliases: bool option, - relevance_thresholds: real * real, - max_relevant: int option, + fact_thresholds: real * real, + max_facts: int option, max_mono_iters: int option, max_new_mono_instances: int option, isar_proof: bool, @@ -110,7 +110,7 @@ val is_unit_equational_atp : Proof.context -> string -> bool val is_prover_supported : Proof.context -> string -> bool val is_prover_installed : Proof.context -> string -> bool - val default_max_relevant_for_prover : Proof.context -> bool -> string -> int + val default_max_facts_for_prover : Proof.context -> bool -> string -> int val is_unit_equality : term -> bool val is_appropriate_prop_for_prover : Proof.context -> string -> term -> bool val is_built_in_const_for_prover : @@ -188,12 +188,12 @@ fun get_slices slice slices = (0 upto length slices - 1) ~~ slices |> not slice ? (List.last #> single) -val reconstructor_default_max_relevant = 20 +val reconstructor_default_max_facts = 20 -fun default_max_relevant_for_prover ctxt slice name = +fun default_max_facts_for_prover ctxt slice name = let val thy = Proof_Context.theory_of ctxt in if is_reconstructor name then - reconstructor_default_max_relevant + reconstructor_default_max_facts else if is_atp thy name then fold (Integer.max o #1 o fst o snd o snd o snd) (get_slices slice (#best_slices (get_atp thy name ()) ctxt)) 0 @@ -314,8 +314,8 @@ strict: bool, lam_trans: string option, uncurried_aliases: bool option, - relevance_thresholds: real * real, - max_relevant: int option, + fact_thresholds: real * real, + max_facts: int option, max_mono_iters: int option, max_new_mono_instances: int option, isar_proof: bool, @@ -629,7 +629,7 @@ prem_role, best_slices, best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config) (params as {debug, verbose, overlord, type_enc, strict, lam_trans, - uncurried_aliases, max_relevant, max_mono_iters, + uncurried_aliases, max_facts, max_mono_iters, max_new_mono_instances, isar_proof, isar_shrink_factor, slice, timeout, preplay_timeout, ...}) minimize_command @@ -711,13 +711,12 @@ end fun run_slice time_left (cache_key, cache_value) (slice, (time_frac, (complete, - (key as (best_max_relevant, format, best_type_enc, + (key as (best_max_facts, format, best_type_enc, best_lam_trans, best_uncurried_aliases), extra)))) = let val num_facts = - length facts |> is_none max_relevant - ? Integer.min best_max_relevant + length facts |> is_none max_facts ? Integer.min best_max_facts val soundness = if strict then Strict else Non_Strict val type_enc = type_enc |> choose_type_enc soundness best_type_enc format diff -r 7fcee834c7f5 -r 914ca0827804 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 @@ -62,7 +62,7 @@ (if blocking then "." else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))) -fun launch_prover (params as {debug, verbose, blocking, max_relevant, slice, +fun launch_prover (params as {debug, verbose, blocking, max_facts, slice, timeout, expect, ...}) mode minimize_command only {state, goal, subgoal, subgoal_count, facts} name = @@ -71,10 +71,9 @@ val hard_timeout = Time.+ (timeout, timeout) val birth_time = Time.now () val death_time = Time.+ (birth_time, hard_timeout) - val max_relevant = - max_relevant - |> the_default (default_max_relevant_for_prover ctxt slice name) - val num_facts = length facts |> not only ? Integer.min max_relevant + val max_facts = + max_facts |> the_default (default_max_facts_for_prover ctxt slice name) + val num_facts = length facts |> not only ? Integer.min max_facts fun desc () = prover_description ctxt params name num_facts subgoal subgoal_count goal val problem = @@ -153,10 +152,10 @@ ctxt |> select_smt_solver name |> SMT_Config.solver_class_of |> SMT_Utils.string_of_class -val auto_try_max_relevant_divisor = 2 (* FUDGE *) +val auto_try_max_facts_divisor = 2 (* FUDGE *) -fun run_sledgehammer (params as {debug, verbose, blocking, provers, - max_relevant, slice, ...}) +fun run_sledgehammer (params as {debug, verbose, blocking, provers, max_facts, + slice, ...}) mode i (fact_override as {only, ...}) minimize_command state = if null provers then error "No prover is set." @@ -207,22 +206,20 @@ end fun get_facts label is_appropriate_prop provers = let - val max_max_relevant = - case max_relevant of + val max_max_facts = + case max_facts of SOME n => n | NONE => - 0 |> fold (Integer.max - o default_max_relevant_for_prover ctxt slice) + 0 |> fold (Integer.max o default_max_facts_for_prover ctxt slice) provers - |> mode = Auto_Try - ? (fn n => n div auto_try_max_relevant_divisor) + |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor) in facts |> (case is_appropriate_prop of SOME is_app => filter (is_app o prop_of o snd) | NONE => I) - |> relevant_facts ctxt params (hd provers) max_max_relevant - fact_override hyp_ts concl_t + |> relevant_facts ctxt params (hd provers) max_max_facts fact_override + hyp_ts concl_t |> map (apfst (apfst (fn name => name ()))) |> tap (fn facts => if debug then