--- 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"),
--- 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) =
--- 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_"]
--- 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 ())))
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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