--- a/src/Doc/Sledgehammer/document/root.tex Wed Sep 11 11:34:27 2013 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Wed Sep 11 11:38:07 2013 +0200
@@ -1098,7 +1098,7 @@
are potentially generated. Whether monomorphization takes place depends on the
type encoding used. If the option is set to \textit{smart}, it is set to a value
that was empirically found to be appropriate for the prover. For most provers,
-this value is 200.
+this value is 100.
\nopagebreak
{\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
--- a/src/HOL/Tools/ATP/atp_systems.ML Wed Sep 11 11:34:27 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Sep 11 11:38:07 2013 +0200
@@ -91,7 +91,7 @@
(* ATP configuration *)
val default_max_mono_iters = 3 (* FUDGE *)
-val default_max_new_mono_instances = 200 (* FUDGE *)
+val default_max_new_mono_instances = 100 (* FUDGE *)
type slice_spec = (int * string) * atp_format * string * string * bool
@@ -225,7 +225,7 @@
(* FUDGE *)
K [(1.0, (((60, ""), agsyhol_thf0, "mono_native_higher", keep_lamsN, false), ""))],
best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
- best_max_new_mono_instances = default_max_new_mono_instances div 2 (* FUDGE *)}
+ best_max_new_mono_instances = default_max_new_mono_instances}
val agsyhol = (agsyholN, fn () => agsyhol_config)
@@ -480,7 +480,7 @@
(* FUDGE *)
K [(1.0, (((40, ""), leo2_thf0, "mono_native_higher", keep_lamsN, false), ""))],
best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
- best_max_new_mono_instances = default_max_new_mono_instances div 2 (* FUDGE *)}
+ best_max_new_mono_instances = default_max_new_mono_instances}
val leo2 = (leo2N, fn () => leo2_config)
@@ -502,7 +502,7 @@
(* FUDGE *)
K [(1.0, (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), ""))],
best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
- best_max_new_mono_instances = default_max_new_mono_instances div 2 (* FUDGE *)}
+ best_max_new_mono_instances = default_max_new_mono_instances}
val satallax = (satallaxN, fn () => satallax_config)
@@ -609,7 +609,7 @@
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I),
best_max_mono_iters = default_max_mono_iters,
- best_max_new_mono_instances = default_max_new_mono_instances}
+ best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
val vampire = (vampireN, fn () => vampire_config)
@@ -633,7 +633,7 @@
(0.125, (((62, mashN), z3_tff0, "mono_native", combsN, false), "")),
(0.125, (((31, meshN), z3_tff0, "mono_native", combsN, false), ""))],
best_max_mono_iters = default_max_mono_iters,
- best_max_new_mono_instances = default_max_new_mono_instances}
+ best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
val z3_tptp = (z3_tptpN, fn () => z3_tptp_config)
--- a/src/HOL/Tools/ATP/atp_util.ML Wed Sep 11 11:34:27 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML Wed Sep 11 11:38:07 2013 +0200
@@ -7,8 +7,9 @@
signature ATP_UTIL =
sig
val timestamp : unit -> string
+ val hashw : word * word -> word
+ val hashw_string : string * word -> word
val hash_string : string -> int
- val hash_term : term -> int
val chunk_list : int -> 'a list -> 'a list list
val stringN_of_int : int -> int -> string
val strip_spaces : bool -> (char -> bool) -> string -> string
@@ -63,13 +64,7 @@
fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)
fun hashw_string (s : string, w) = CharVector.foldl hashw_char w s
-fun hashw_term (t1 $ t2) = hashw (hashw_term t1, hashw_term t2)
- | hashw_term (Const (s, _)) = hashw_string (s, 0w0)
- | hashw_term (Free (s, _)) = hashw_string (s, 0w0)
- | hashw_term _ = 0w0
-
fun hash_string s = Word.toInt (hashw_string (s, 0w0))
-val hash_term = Word.toInt o hashw_term
fun chunk_list _ [] = []
| chunk_list k xs =
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Wed Sep 11 11:34:27 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Wed Sep 11 11:38:07 2013 +0200
@@ -299,6 +299,11 @@
if maybe_quote s = s then pretty else Pretty.enum "" "\"" "\"" [pretty]
end
-val hash_term = ATP_Util.hash_term
+fun hashw_term (t1 $ t2) = ATP_Util.hashw (hashw_term t1, hashw_term t2)
+ | hashw_term (Const (s, _)) = ATP_Util.hashw_string (s, 0w0)
+ | hashw_term (Free (s, _)) = ATP_Util.hashw_string (s, 0w0)
+ | hashw_term _ = 0w0
+
+val hash_term = Word.toInt o hashw_term
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Sep 11 11:34:27 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Sep 11 11:38:07 2013 +0200
@@ -18,7 +18,6 @@
del : (Facts.ref * Attrib.src list) list,
only : bool}
- val ignore_no_atp : bool Config.T
val instantiate_inducts : bool Config.T
val no_fact_override : fact_override
val fact_of_ref :
@@ -33,7 +32,6 @@
val maybe_instantiate_inducts :
Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
-> (((unit -> string) * 'a) * thm) list
- val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
val fact_of_raw_fact : raw_fact -> fact
val all_facts :
Proof.context -> bool -> bool -> unit Symtab.table -> thm list -> thm list
@@ -59,9 +57,7 @@
del : (Facts.ref * Attrib.src list) list,
only : bool}
-(* experimental features *)
-val ignore_no_atp =
- Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false)
+(* experimental feature *)
val instantiate_inducts =
Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false)
@@ -106,15 +102,49 @@
body_type T = @{typ bool}
| _ => false)
+fun normalize_vars t =
+ let
+ fun normT (Type (s, Ts)) = fold_map normT Ts #>> curry Type s
+ | normT (TVar (z as (_, S))) =
+ (fn ((knownT, nT), accum) =>
+ case find_index (equal z) knownT of
+ ~1 => (TVar ((Name.uu, nT), S), ((z :: knownT, nT + 1), accum))
+ | j => (TVar ((Name.uu, nT - j - 1), S), ((knownT, nT), accum)))
+ | normT (T as TFree _) = pair T
+ fun norm (t $ u) = norm t ##>> norm u #>> op $
+ | norm (Const (s, T)) = normT T #>> curry Const s
+ | norm (Var (z as (_, T))) =
+ normT T
+ #> (fn (T, (accumT, (known, n))) =>
+ case find_index (equal z) known of
+ ~1 => (Var ((Name.uu, n), T), (accumT, (z :: known, n + 1)))
+ | j => (Var ((Name.uu, n - j - 1), T), (accumT, (known, n))))
+ | norm (Abs (_, T, t)) =
+ norm t ##>> normT T #>> (fn (t, T) => Abs (Name.uu, T, t))
+ | norm (Bound j) = pair (Bound j)
+ | norm (Free (s, T)) = normT T #>> curry Free s
+ in fst (norm t (([], 0), ([], 0))) end
+
fun status_of_thm css name th =
- (* FIXME: use structured name *)
- if (String.isSubstring ".induct" name orelse
- String.isSubstring ".inducts" name) andalso
- may_be_induction (prop_of th) then
- Induction
- else case Termtab.lookup css (prop_of th) of
- SOME status => status
- | NONE => General
+ let val t = normalize_vars (prop_of th) in
+ (* FIXME: use structured name *)
+ if String.isSubstring ".induct" name andalso may_be_induction t then
+ Induction
+ else case Termtab.lookup css t of
+ SOME status => status
+ | NONE =>
+ let val concl = Logic.strip_imp_concl t in
+ case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl of
+ SOME lrhss =>
+ let
+ val prems = Logic.strip_imp_prems t
+ val t' = Logic.list_implies (prems, Logic.mk_equals lrhss)
+ in
+ Termtab.lookup css t' |> the_default General
+ end
+ | NONE => General
+ end
+ end
fun stature_of_thm global assms chained css name th =
(scope_of_thm global assms chained th, status_of_thm css name th)
@@ -161,36 +191,6 @@
append ["induct", "inducts"]
|> map (prefix Long_Name.separator)
-val max_lambda_nesting = 5 (*only applies if not ho_atp*)
-
-fun term_has_too_many_lambdas max (t1 $ t2) =
- exists (term_has_too_many_lambdas max) [t1, t2]
- | term_has_too_many_lambdas max (Abs (_, _, t)) =
- max = 0 orelse term_has_too_many_lambdas (max - 1) t
- | term_has_too_many_lambdas _ _ = false
-
-(* Don't count nested lambdas at the level of formulas, since they are
- quantifiers. *)
-fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
- formula_has_too_many_lambdas (T :: Ts) t
- | formula_has_too_many_lambdas Ts t =
- if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then
- exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
- else
- term_has_too_many_lambdas max_lambda_nesting t
-
-(* The maximum apply depth of any "metis" call in "Metis_Examples" (on
- 2007-10-31) was 11. *)
-val max_apply_depth = 18
-
-fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
- | apply_depth (Abs (_, _, t)) = apply_depth t
- | apply_depth _ = 0
-
-fun is_too_complex ho_atp t =
- apply_depth t > max_apply_depth orelse
- (not ho_atp andalso formula_has_too_many_lambdas [] t)
-
(* FIXME: Ad hoc list *)
val technical_prefixes =
["ATP", "Code_Evaluation", "Datatype", "Enum", "Lazy_Sequence",
@@ -199,51 +199,66 @@
"Random_Sequence", "Sledgehammer", "SMT"]
|> map (suffix Long_Name.separator)
-fun has_technical_prefix s =
+fun is_technical_const (s, _) =
exists (fn pref => String.isPrefix pref s) technical_prefixes
-val exists_technical_const = exists_Const (has_technical_prefix o fst)
(* FIXME: make more reliable *)
-val exists_low_level_class_const =
- exists_Const (fn (s, _) =>
- s = @{const_name equal_class.equal} orelse
- String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s)
+val sep_class_sep = Long_Name.separator ^ "class" ^ Long_Name.separator
+fun is_low_level_class_const (s, _) =
+ s = @{const_name equal_class.equal} orelse String.isSubstring sep_class_sep s
+
+val sep_that = Long_Name.separator ^ Obtain.thatN
fun is_that_fact th =
- String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th)
+ String.isSuffix sep_that (Thm.get_name_hint th)
andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
| _ => false) (prop_of th)
+datatype interest = Deal_Breaker | Interesting | Boring
+
+fun combine_interests Deal_Breaker _ = Deal_Breaker
+ | combine_interests _ Deal_Breaker = Deal_Breaker
+ | combine_interests Interesting _ = Interesting
+ | combine_interests _ Interesting = Interesting
+ | combine_interests Boring Boring = Boring
+
fun is_likely_tautology_too_meta_or_too_technical th =
let
fun is_interesting_subterm (Const (s, _)) =
not (member (op =) atp_widely_irrelevant_consts s)
| is_interesting_subterm (Free _) = true
| is_interesting_subterm _ = false
- fun is_boring_bool t =
- not (exists_subterm is_interesting_subterm t) orelse
- exists_type (exists_subtype (curry (op =) @{typ prop})) t
- fun is_boring_prop _ (@{const Trueprop} $ t) = is_boring_bool t
- | is_boring_prop Ts (@{const "==>"} $ t $ u) =
- is_boring_prop Ts t andalso is_boring_prop Ts u
- | is_boring_prop Ts (Const (@{const_name all}, _) $ Abs (_, T, t)) =
- is_boring_prop (T :: Ts) t
- | is_boring_prop Ts ((t as Const (@{const_name all}, _)) $ u) =
- is_boring_prop Ts (t $ eta_expand Ts u 1)
- | is_boring_prop _ (Const (@{const_name "=="}, _) $ t $ u) =
- is_boring_bool t andalso is_boring_bool u
- | is_boring_prop _ _ = true
+ fun interest_of_bool t =
+ if exists_Const (is_technical_const orf is_low_level_class_const) t then
+ Deal_Breaker
+ else if exists_type (exists_subtype (curry (op =) @{typ prop})) t orelse
+ not (exists_subterm is_interesting_subterm t) then
+ Boring
+ else
+ Interesting
+ fun interest_of_prop _ (@{const Trueprop} $ t) = interest_of_bool t
+ | interest_of_prop Ts (@{const "==>"} $ t $ u) =
+ combine_interests (interest_of_prop Ts t) (interest_of_prop Ts u)
+ | interest_of_prop Ts (Const (@{const_name all}, _) $ Abs (_, T, t)) =
+ interest_of_prop (T :: Ts) t
+ | interest_of_prop Ts ((t as Const (@{const_name all}, _)) $ u) =
+ interest_of_prop Ts (t $ eta_expand Ts u 1)
+ | interest_of_prop _ (Const (@{const_name "=="}, _) $ t $ u) =
+ combine_interests (interest_of_bool t) (interest_of_bool u)
+ | interest_of_prop _ _ = Deal_Breaker
val t = prop_of th
in
- (is_boring_prop [] (prop_of th) andalso
+ (interest_of_prop [] t <> Interesting andalso
not (Thm.eq_thm_prop (@{thm ext}, th))) orelse
- exists_type type_has_top_sort t orelse exists_technical_const t orelse
- exists_low_level_class_const t orelse is_that_fact th
+ is_that_fact th
end
-fun is_blacklisted_or_something ctxt ho_atp name =
- (not (Config.get ctxt ignore_no_atp) andalso is_package_def name) orelse
- exists (fn s => String.isSuffix s name) (multi_base_blacklist ctxt ho_atp)
+fun is_blacklisted_or_something ctxt ho_atp =
+ let
+ val blist = multi_base_blacklist ctxt ho_atp
+ fun is_blisted name =
+ is_package_def name orelse exists (fn s => String.isSuffix s name) blist
+ in is_blisted end
fun hackish_string_of_term ctxt =
with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces
@@ -272,48 +287,45 @@
fun backquote_term ctxt = close_form #> hackish_string_of_term ctxt #> backquote
fun backquote_thm ctxt = backquote_term ctxt o prop_of
+(* gracefully handle huge background theories *)
+val max_simps_for_clasimpset = 10000
+
fun clasimpset_rule_table_of ctxt =
- let
- val thy = Proof_Context.theory_of ctxt
- val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy
- fun add stature normalizers get_th =
- fold (fn rule =>
- let
- val th = rule |> get_th
- val t =
- th |> Thm.maxidx_of th > 0 ? zero_var_indexes |> prop_of
- in
- fold (fn normalize => Termtab.update (normalize t, stature))
- (I :: normalizers)
- end)
- val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} =
- ctxt |> claset_of |> Classical.rep_cs
- val intros = Item_Net.content safeIs @ Item_Net.content hazIs
+ let val simps = ctxt |> simpset_of |> dest_ss |> #simps in
+ if length simps >= max_simps_for_clasimpset then
+ Termtab.empty
+ else
+ let
+ fun add stature th =
+ Termtab.update (normalize_vars (prop_of th), stature)
+ val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} =
+ ctxt |> claset_of |> Classical.rep_cs
+ val intros = Item_Net.content safeIs @ Item_Net.content hazIs
(* Add once it is used:
- val elims =
- Item_Net.content safeEs @ Item_Net.content hazEs
- |> map Classical.classical_rule
+ val elims =
+ Item_Net.content safeEs @ Item_Net.content hazEs
+ |> map Classical.classical_rule
*)
- val simps = ctxt |> simpset_of |> dest_ss |> #simps
- val specs = ctxt |> Spec_Rules.get
- val (rec_defs, nonrec_defs) =
- specs |> filter (curry (op =) Spec_Rules.Equational o fst)
- |> maps (snd o snd)
- |> filter_out (member Thm.eq_thm_prop risky_defs)
- |> List.partition (is_rec_def o prop_of)
- val spec_intros =
- specs |> filter (member (op =) [Spec_Rules.Inductive,
- Spec_Rules.Co_Inductive] o fst)
- |> maps (snd o snd)
- in
- Termtab.empty |> add Simp [atomize] snd simps
- |> add Rec_Def [] I rec_defs
- |> add Non_Rec_Def [] I nonrec_defs
+ val specs = ctxt |> Spec_Rules.get
+ val (rec_defs, nonrec_defs) =
+ specs |> filter (curry (op =) Spec_Rules.Equational o fst)
+ |> maps (snd o snd)
+ |> filter_out (member Thm.eq_thm_prop risky_defs)
+ |> List.partition (is_rec_def o prop_of)
+ val spec_intros =
+ specs |> filter (member (op =) [Spec_Rules.Inductive,
+ Spec_Rules.Co_Inductive] o fst)
+ |> maps (snd o snd)
+ in
+ Termtab.empty |> fold (add Simp o snd) simps
+ |> fold (add Rec_Def) rec_defs
+ |> fold (add Non_Rec_Def) nonrec_defs
(* Add once it is used:
- |> add Elim [] I elims
+ |> fold (add Elim) elims
*)
- |> add Intro [] I intros
- |> add Inductive [] I spec_intros
+ |> fold (add Intro) intros
+ |> fold (add Inductive) spec_intros
+ end
end
fun normalize_eq (t as @{const Trueprop}
@@ -326,7 +338,7 @@
else HOLogic.mk_Trueprop (HOLogic.mk_not (t0 $ t2 $ t1))
| normalize_eq t = t
-val normalize_eq_etc = normalize_eq o Term_Subst.zero_var_indexes
+val normalize_eq_vars = normalize_eq #> normalize_vars
fun if_thm_before th th' =
if Theory.subthy (pairself Thm.theory_of_thm (th, th')) then th else th'
@@ -341,7 +353,8 @@
fun build_name_tables name_of facts =
let
- fun cons_thm (_, th) = Termtab.cons_list (normalize_eq_etc (prop_of th), th)
+ fun cons_thm (_, th) =
+ Termtab.cons_list (normalize_eq_vars (prop_of th), th)
fun add_plain canon alias =
Symtab.update (Thm.get_name_hint alias,
name_of (if_thm_before canon alias))
@@ -353,10 +366,17 @@
val inclass_name_tab = Symtab.fold add_inclass plain_name_tab Symtab.empty
in (plain_name_tab, inclass_name_tab) end
-fun uniquify facts =
- Termtab.fold (cons o snd)
- (fold (Termtab.default o `(normalize_eq_etc o prop_of o snd)) facts
- Termtab.empty) []
+fun keyed_distinct key_of xs =
+ let val tab = fold (Termtab.default o `key_of) xs Termtab.empty in
+ Termtab.fold (cons o snd) tab []
+ end
+
+fun hashed_keyed_distinct hash_of key_of xs =
+ let
+ val ys = map (`hash_of) xs
+ val sorted_ys = sort (int_ord o pairself fst) ys
+ val grouped_ys = AList.coalesce (op =) sorted_ys
+ in maps (keyed_distinct key_of o snd) grouped_ys end
fun struct_induct_rule_on th =
case Logic.strip_horn (prop_of th) of
@@ -415,9 +435,6 @@
else
I
-fun maybe_filter_no_atps ctxt =
- not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
-
fun fact_of_raw_fact ((name, stature), th) = ((name (), stature), th)
fun all_facts ctxt generous ho_atp reserved add_ths chained css =
@@ -435,14 +452,13 @@
|> filter is_good_unnamed_local |> map (pair "" o single)
val full_space =
Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
+ val is_blacklisted_or_something = is_blacklisted_or_something ctxt ho_atp
fun add_facts global foldx facts =
foldx (fn (name0, ths) =>
if name0 <> "" andalso
forall (not o member Thm.eq_thm_prop add_ths) ths andalso
(Facts.is_concealed facts name0 orelse
- not (can (Proof_Context.get_thms ctxt) name0) orelse
- (not generous andalso
- is_blacklisted_or_something ctxt ho_atp name0)) then
+ (not generous andalso is_blacklisted_or_something name0)) then
I
else
let
@@ -457,9 +473,7 @@
#> fold_rev (fn th => fn (j, accum) =>
(j - 1,
if not (member Thm.eq_thm_prop add_ths th) andalso
- (is_likely_tautology_too_meta_or_too_technical th orelse
- (not generous andalso
- is_too_complex ho_atp (prop_of th))) then
+ is_likely_tautology_too_meta_or_too_technical th then
accum
else
let
@@ -506,9 +520,10 @@
else
let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
all_facts ctxt false ho_atp reserved add chained css
- |> filter_out (member Thm.eq_thm_prop del o snd)
- |> maybe_filter_no_atps ctxt
- |> uniquify
+ |> filter_out
+ ((member Thm.eq_thm_prop del orf No_ATPs.member ctxt) o snd)
+ |> hashed_keyed_distinct (size_of_term o prop_of o snd)
+ (normalize_eq_vars o prop_of o snd)
end)
|> maybe_instantiate_inducts ctxt hyp_ts concl_t
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Wed Sep 11 11:34:27 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Wed Sep 11 11:38:07 2013 +0200
@@ -311,8 +311,8 @@
s = pseudo_abs_name orelse String.isPrefix pseudo_skolem_prefix s orelse
String.isSuffix theory_const_suffix s
-fun fact_weight fudge stature const_tab rel_const_tab rel_const_iter_tab
- chained_const_tab fact_consts =
+fun fact_weight fudge stature const_tab rel_const_tab chained_const_tab
+ fact_consts =
case fact_consts |> List.partition (pconst_hyper_mem I rel_const_tab)
||> filter_out (pconst_hyper_mem swap rel_const_tab) of
([], _) => 0.0
@@ -407,16 +407,14 @@
|> (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 goal_const_iter_tab = goal_const_tab |> Symtab.map (K (K ~1))
- fun iter j remaining_max thres rel_const_tab rel_const_iter_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 thres >= ridiculous_threshold then
(* First iteration? Try again. *)
iter 0 max_facts (thres / threshold_divisor) rel_const_tab
- rel_const_iter_tab hopeless hopeful
+ hopeless hopeful
else
[]
| relevant candidates rejects [] =
@@ -426,9 +424,6 @@
val sps = maps (snd o fst) accepts;
val rel_const_tab' =
rel_const_tab |> fold (add_pconst_to_table false) sps
- val rel_const_iter_tab' =
- rel_const_iter_tab
- |> fold (fn (s, _) => Symtab.default (s, j)) sps
fun is_dirty (s, _) =
Symtab.lookup rel_const_tab' s <> Symtab.lookup rel_const_tab s
val (hopeful_rejects, hopeless_rejects) =
@@ -457,7 +452,7 @@
[]
else
iter (j + 1) remaining_max thres rel_const_tab'
- rel_const_iter_tab' hopeless_rejects hopeful_rejects)
+ hopeless_rejects hopeful_rejects)
end
| relevant candidates rejects
(((ax as (((_, stature), _), fact_consts)), cached_weight)
@@ -468,7 +463,7 @@
SOME w => w
| NONE =>
fact_weight fudge stature const_tab rel_const_tab
- rel_const_iter_tab chained_const_tab fact_consts
+ chained_const_tab fact_consts
in
if weight >= thres then
relevant ((ax, weight) :: candidates) rejects hopeful
@@ -509,7 +504,7 @@
|> insert_into_facts accepts
in
facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)
- |> iter 0 max_facts thres0 goal_const_tab goal_const_iter_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)))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Sep 11 11:34:27 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Sep 11 11:38:07 2013 +0200
@@ -252,6 +252,9 @@
fun is_appropriate_prop_of_prover ctxt name =
if is_unit_equational_atp ctxt name then is_unit_equality else K true
+val atp_irrelevant_const_tab =
+ Symtab.make (map (rpair ()) atp_irrelevant_consts)
+
fun is_built_in_const_of_prover ctxt name =
if is_smt_prover ctxt name then
let val ctxt = ctxt |> select_smt_solver name in
@@ -264,7 +267,7 @@
(false, ts)
end
else
- fn (s, _) => fn ts => (member (op =) atp_irrelevant_consts s, ts)
+ fn (s, _) => fn ts => (Symtab.defined atp_irrelevant_const_tab s, ts)
(* FUDGE *)
val atp_relevance_fudge =
@@ -1122,7 +1125,7 @@
(if show_filter then " " ^ quote fact_filter else "") ^
" fact" ^ plural_s num_facts
val _ =
- if verbose andalso is_some outcome then
+ if debug then
quote name ^ " invoked with " ^
num_of_facts fact_filter num_facts ^ ": " ^
string_of_failure (failure_of_smt_failure (the outcome)) ^