use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
--- a/src/HOL/TPTP/mash_export.ML Wed Oct 09 10:47:43 2013 +0200
+++ b/src/HOL/TPTP/mash_export.ML Wed Oct 09 15:39:34 2013 +0200
@@ -72,7 +72,6 @@
fun generate_features ctxt prover thys file_name =
let
- val is_built_in_const = Sledgehammer_Provers.is_built_in_const_of_prover ctxt prover
val path = file_name |> Path.explode
val _ = File.write path ""
val facts = all_facts ctxt |> filter_out (has_thys thys o snd)
@@ -80,8 +79,7 @@
let
val name = nickname_of_thm th
val feats =
- features_of ctxt is_built_in_const (theory_of_thm th) 0 Symtab.empty stature [prop_of th]
- |> map fst
+ features_of ctxt (theory_of_thm th) 0 Symtab.empty stature [prop_of th] |> map fst
val s =
encode_str name ^ ": " ^ encode_strs (sort string_ord feats) ^ "\n"
in File.append path s end
@@ -150,7 +148,6 @@
fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys
linearize max_suggs file_name =
let
- val is_built_in_const = Sledgehammer_Provers.is_built_in_const_of_prover ctxt prover
val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
val path = file_name |> Path.explode
val facts = all_facts ctxt
@@ -165,8 +162,7 @@
val isar_deps = isar_dependencies_of name_tabs th
val do_query = not (is_bad_query ctxt ho_atp step j th isar_deps)
val goal_feats =
- features_of ctxt is_built_in_const (theory_of_thm th) (num_old_facts + j) const_tab
- stature [prop_of th]
+ features_of ctxt (theory_of_thm th) (num_old_facts + j) const_tab stature [prop_of th]
|> sort_wrt fst
val access_facts =
(if linearize then take (j - 1) new_facts
@@ -177,8 +173,7 @@
val parents = if linearize then prevs else parents
fun extra_features_of (((_, stature), th), weight) =
[prop_of th]
- |> features_of ctxt is_built_in_const (theory_of_thm th) (num_old_facts + j) const_tab
- stature
+ |> features_of ctxt (theory_of_thm th) (num_old_facts + j) const_tab stature
|> map (apsnd (fn r => weight * extra_feature_factor * r))
val query =
if do_query then
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Oct 09 10:47:43 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Oct 09 15:39:34 2013 +0200
@@ -91,6 +91,8 @@
val atp_logical_consts : string list
val atp_irrelevant_consts : string list
val atp_widely_irrelevant_consts : string list
+ val is_irrelevant_const : string -> bool
+ val is_widely_irrelevant_const : string -> bool
val atp_schematic_consts_of : term -> typ list Symtab.table
val is_type_enc_higher_order : type_enc -> bool
val is_type_enc_polymorphic : type_enc -> bool
@@ -405,19 +407,25 @@
(* These are ignored anyway by the relevance filter (unless they appear in
higher-order places) but not by the monomorphizer. *)
val atp_logical_consts =
- [@{const_name all}, @{const_name "==>"}, @{const_name "=="},
- @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
+ [@{const_name prop}, @{const_name Pure.conjunction}, @{const_name all}, @{const_name "==>"},
+ @{const_name "=="}, @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
@{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]
(* These are either simplified away by "Meson.presimplify" (most of the time) or
handled specially via "fFalse", "fTrue", ..., "fequal". *)
val atp_irrelevant_consts =
- [@{const_name False}, @{const_name True}, @{const_name Not},
- @{const_name conj}, @{const_name disj}, @{const_name implies},
- @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
+ [@{const_name False}, @{const_name True}, @{const_name Not}, @{const_name conj},
+ @{const_name disj}, @{const_name implies}, @{const_name HOL.eq}, @{const_name If},
+ @{const_name Let}]
val atp_widely_irrelevant_consts = atp_logical_consts @ atp_irrelevant_consts
+val atp_irrelevant_const_tab = Symtab.make (map (rpair ()) atp_irrelevant_consts)
+val atp_widely_irrelevant_const_tab = Symtab.make (map (rpair ()) atp_widely_irrelevant_consts)
+
+val is_irrelevant_const = Symtab.defined atp_irrelevant_const_tab
+val is_widely_irrelevant_const = Symtab.defined atp_widely_irrelevant_const_tab
+
fun add_schematic_const (x as (_, T)) =
Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x
val add_schematic_consts_of =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Oct 09 10:47:43 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Oct 09 15:39:34 2013 +0200
@@ -63,8 +63,8 @@
val run_prover_for_mash :
Proof.context -> params -> string -> fact list -> thm -> prover_result
val features_of :
- Proof.context -> (string * typ -> term list -> bool * term list) -> theory ->
- int -> int Symtab.table -> stature -> term list -> (string * real) list
+ Proof.context -> theory -> int -> int Symtab.table -> stature -> term list ->
+ (string * real) list
val trim_dependencies : string list -> string list option
val isar_dependencies_of :
string Symtab.table * string Symtab.table -> thm -> string list
@@ -514,20 +514,14 @@
val mess = mess |> map (apsnd (apfst (normalize_scores max_facts)))
fun score_in fact (global_weight, (sels, unks)) =
let
- fun score_at j =
- case try (nth sels) j of
- SOME (_, score) => SOME (global_weight * score)
- | NONE => NONE
+ val score_at = try (nth sels) #> Option.map (fn (_, score) => global_weight * score)
in
case find_index (curry fact_eq fact o fst) sels of
- ~1 => (case find_index (curry fact_eq fact) unks of
- ~1 => SOME 0.0
- | _ => NONE)
+ ~1 => if member fact_eq unks fact then NONE else SOME 0.0
| rank => score_at rank
end
fun weight_of fact = mess |> map_filter (score_in fact) |> scaled_avg
- val facts =
- fold (union fact_eq o map fst o take max_facts o fst o snd) mess []
+ val facts = fold (union fact_eq o map fst o take max_facts o fst o snd) mess []
in
facts |> map (`weight_of) |> sort (int_ord o swap o pairself fst)
|> map snd |> take max_facts
@@ -585,9 +579,6 @@
val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
-val logical_consts =
- [@{const_name prop}, @{const_name Pure.conjunction}] @ atp_logical_consts
-
val pat_tvar_prefix = "_"
val pat_var_prefix = "_"
@@ -608,15 +599,10 @@
val max_pat_breadth = 10 (* FUDGE *)
-fun term_features_of ctxt is_built_in_const thy_name num_facts const_tab term_max_depth
- type_max_depth ts =
+fun term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth ts =
let
val thy = Proof_Context.theory_of ctxt
- fun is_built_in (x as (s, _)) args =
- if member (op =) logical_consts s then (true, args)
- else is_built_in_const x args
-
val fixes = map snd (Variable.dest_fixes ctxt)
val classes = Sign.classes_of thy
@@ -660,11 +646,10 @@
let val count = Symtab.lookup const_tab s |> the_default 1 in
Real.fromInt num_facts / Real.fromInt count (* FUDGE *)
end)
- fun pattify_term _ _ 0 _ = []
- | pattify_term _ args _ (Const (x as (s, _))) =
- if fst (is_built_in x args) then []
- else [(massage_long_name s, weight_of_const s)]
- | pattify_term _ _ _ (Free (s, T)) =
+ fun pattify_term _ 0 _ = []
+ | pattify_term _ _ (Const (s, _)) =
+ if is_widely_irrelevant_const s then [] else [(massage_long_name s, weight_of_const s)]
+ | pattify_term _ _ (Free (s, T)) =
maybe_singleton_str pat_var_prefix (crude_str_of_typ T)
|> map (rpair 0.0)
|> (if member (op =) fixes s then
@@ -672,36 +657,31 @@
(thy_name ^ Long_Name.separator ^ s)))
else
I)
- | pattify_term _ _ _ (Var (_, T)) =
- maybe_singleton_str pat_var_prefix (crude_str_of_typ T)
- |> map (rpair 0.0)
- | pattify_term Ts _ _ (Bound j) =
- maybe_singleton_str pat_var_prefix (crude_str_of_typ (nth Ts j))
- |> map (rpair 0.0)
- | pattify_term Ts args depth (t $ u) =
+ | pattify_term _ _ (Var (_, T)) =
+ maybe_singleton_str pat_var_prefix (crude_str_of_typ T) |> map (rpair 0.0)
+ | pattify_term Ts _ (Bound j) =
+ maybe_singleton_str pat_var_prefix (crude_str_of_typ (nth Ts j)) |> map (rpair 0.0)
+ | pattify_term Ts depth (t $ u) =
let
- val ps = take max_pat_breadth (pattify_term Ts (u :: args) depth t)
- val qs =
- take max_pat_breadth (("", 0.0) :: pattify_term Ts [] (depth - 1) u)
+ val ps = take max_pat_breadth (pattify_term Ts depth t)
+ val qs = take max_pat_breadth (("", 0.0) :: pattify_term Ts (depth - 1) u)
in
map_product (fn ppw as (p, pw) =>
fn ("", _) => ppw
| (q, qw) => (p ^ "(" ^ q ^ ")", pw + qw)) ps qs
end
- | pattify_term _ _ _ _ = []
- fun add_term_pat Ts = union (eq_fst (op =)) oo pattify_term Ts []
+ | pattify_term _ _ _ = []
+ fun add_term_pat Ts = union (eq_fst (op =)) oo pattify_term Ts
fun add_term_pats _ 0 _ = I
| add_term_pats Ts depth t =
add_term_pat Ts depth t #> add_term_pats Ts (depth - 1) t
fun add_term Ts = add_term_pats Ts term_max_depth
fun add_subterms Ts t =
case strip_comb t of
- (Const (x as (_, T)), args) =>
- let val (built_in, args) = is_built_in x args in
- (not built_in ? add_term Ts t)
- #> add_subtypes T
- #> fold (add_subterms Ts) args
- end
+ (Const (s, T), args) =>
+ (not (is_widely_irrelevant_const s) ? add_term Ts t)
+ #> add_subtypes T
+ #> fold (add_subterms Ts) args
| (head, args) =>
(case head of
Free (_, T) => add_term Ts t #> add_subtypes T
@@ -715,11 +695,10 @@
val type_max_depth = 1
(* TODO: Generate type classes for types? *)
-fun features_of ctxt is_built_in_const thy num_facts const_tab (scope, _) ts =
+fun features_of ctxt thy num_facts const_tab (scope, _) ts =
let val thy_name = Context.theory_name thy in
thy_feature_of thy_name ::
- term_features_of ctxt is_built_in_const thy_name num_facts const_tab term_max_depth
- type_max_depth ts
+ term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth ts
|> scope <> Global ? cons local_feature
end
@@ -961,7 +940,6 @@
let
val thy = Proof_Context.theory_of ctxt
val thy_name = Context.theory_name thy
- val is_built_in_const = is_built_in_const_of_prover ctxt prover
val facts = facts |> sort (crude_thm_ord o pairself snd o swap)
val chained = facts |> filter (fn ((_, (scope, _)), _) => scope = Chained)
val num_facts = length facts
@@ -971,7 +949,7 @@
thy_name = Context.theory_name (theory_of_thm th)
fun chained_or_extra_features_of factor (((_, stature), th), weight) =
[prop_of th]
- |> features_of ctxt is_built_in_const (theory_of_thm th) num_facts const_tab stature
+ |> features_of ctxt (theory_of_thm th) num_facts const_tab stature
|> map (apsnd (fn r => weight * factor * r))
val (access_G, suggs) =
@@ -982,8 +960,7 @@
let
val parents = maximal_wrt_access_graph access_G facts
val goal_feats =
- features_of ctxt is_built_in_const thy num_facts const_tab (Local, General)
- (concl_t :: hyp_ts)
+ features_of ctxt thy num_facts const_tab (Local, General) (concl_t :: hyp_ts)
val chained_feats =
chained
|> map (rpair 1.0)
@@ -1052,10 +1029,7 @@
let
val thy = Proof_Context.theory_of ctxt
val name = freshish_name ()
- val feats =
- features_of ctxt (is_built_in_const_of_prover ctxt prover) thy 0 Symtab.empty
- (Local, General) [t]
- |> map fst
+ val feats = features_of ctxt thy 0 Symtab.empty (Local, General) [t] |> map fst
in
peek_state ctxt overlord (fn {access_G, ...} =>
let
@@ -1100,7 +1074,6 @@
""
else
let
- val is_built_in_const = is_built_in_const_of_prover ctxt prover
val name_tabs = build_name_tables nickname_of_thm facts
fun deps_of status th =
if no_dependencies_for_status status then
@@ -1155,9 +1128,7 @@
let
val name = nickname_of_thm th
val feats =
- features_of ctxt is_built_in_const (theory_of_thm th) 0 Symtab.empty stature
- [prop_of th]
- |> map fst
+ features_of ctxt (theory_of_thm th) 0 Symtab.empty stature [prop_of th] |> map fst
val deps = deps_of status th |> these
val n = n |> not (null deps) ? Integer.add 1
val learns = (name, parents, feats, deps) :: learns
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Wed Oct 09 10:47:43 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Wed Oct 09 15:39:34 2013 +0200
@@ -58,16 +58,6 @@
fun string_of_ptype (PType (_, ps)) = string_of_patternsT ps
(*Is the second type an instance of the first one?*)
-fun match_pattern (PVar, _) = true
- | match_pattern (_, PVar) = false
- | match_pattern (PApp (s, ps), PApp (t, qs)) =
- s = t andalso match_patterns (ps, qs)
-and match_patterns (_, []) = true
- | match_patterns ([], _) = false
- | match_patterns (p :: ps, q :: qs) =
- match_pattern (p, q) andalso match_patterns (ps, qs)
-
-(*Is the second type an instance of the first one?*)
fun match_patternT (TVar _, _) = true
| match_patternT (Type (s, ps), Type (t, qs)) =
s = t andalso match_patternsT (ps, qs)
@@ -116,21 +106,18 @@
val set_consts = [@{const_name Collect}, @{const_name Set.member}]
val set_thms = @{thms Collect_mem_eq mem_Collect_eq Collect_cong}
-fun add_pconsts_in_term thy is_built_in_const =
+fun add_pconsts_in_term thy =
let
- fun do_const const ext_arg (x as (s, _)) ts =
- let val (built_in, ts) = is_built_in_const x ts in
- if member (op =) set_consts s then
- fold (do_term ext_arg) ts
- else
- (not built_in
- ? add_pconst_to_table (rich_pconst thy const x))
- #> fold (do_term false) ts
- end
+ fun do_const const (x as (s, _)) ts =
+ if member (op =) set_consts s then
+ fold (do_term false) ts
+ else
+ (not (is_irrelevant_const s) ? add_pconst_to_table (rich_pconst thy const x))
+ #> fold (do_term false) ts
and do_term ext_arg t =
case strip_comb t of
- (Const x, ts) => do_const true ext_arg x ts
- | (Free x, ts) => do_const false ext_arg x ts
+ (Const x, ts) => do_const true x ts
+ | (Free x, ts) => do_const false x ts
| (Abs (_, T, t'), ts) =>
((null ts andalso not ext_arg)
(* Since lambdas on the right-hand side of equalities are usually
@@ -144,7 +131,7 @@
if T = HOLogic.boolT then do_formula else do_term ext_arg
and do_formula t =
case t of
- Const (@{const_name all}, _) $ Abs (_, T, t') => do_formula t'
+ Const (@{const_name all}, _) $ Abs (_, _, t') => do_formula t'
| @{const "==>"} $ t1 $ t2 => do_formula t1 #> do_formula t2
| Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
do_term_or_formula false T t1 #> do_term_or_formula true T t2
@@ -152,8 +139,8 @@
| @{const False} => I
| @{const True} => I
| @{const Not} $ t1 => do_formula t1
- | Const (@{const_name All}, _) $ Abs (_, T, t') => do_formula t'
- | Const (@{const_name Ex}, _) $ Abs (_, T, t') => do_formula t'
+ | Const (@{const_name All}, _) $ Abs (_, _, t') => do_formula t'
+ | Const (@{const_name Ex}, _) $ Abs (_, _, t') => do_formula t'
| @{const HOL.conj} $ t1 $ t2 => do_formula t1 #> do_formula t2
| @{const HOL.disj} $ t1 $ t2 => do_formula t1 #> do_formula t2
| @{const HOL.implies} $ t1 $ t2 => do_formula t1 #> do_formula t2
@@ -162,19 +149,19 @@
| Const (@{const_name If}, Type (_, [_, Type (_, [T, _])]))
$ t1 $ t2 $ t3 =>
do_formula t1 #> fold (do_term_or_formula false T) [t2, t3]
- | Const (@{const_name Ex1}, _) $ Abs (_, T, t') => do_formula t'
- | Const (@{const_name Ball}, _) $ t1 $ Abs (_, T, t') =>
+ | Const (@{const_name Ex1}, _) $ Abs (_, _, t') => do_formula t'
+ | Const (@{const_name Ball}, _) $ t1 $ Abs (_, _, t') =>
do_formula (t1 $ Bound ~1) #> do_formula t'
- | Const (@{const_name Bex}, _) $ t1 $ Abs (_, T, t') =>
+ | Const (@{const_name Bex}, _) $ t1 $ Abs (_, _, t') =>
do_formula (t1 $ Bound ~1) #> do_formula t'
| (t0 as Const (_, @{typ bool})) $ t1 =>
do_term false t0 #> do_formula t1 (* theory constant *)
| _ => do_term false t
in do_formula end
-fun pconsts_in_fact thy is_built_in_const t =
+fun pconsts_in_fact thy t =
Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
- (Symtab.empty |> add_pconsts_in_term thy is_built_in_const t) []
+ (Symtab.empty |> add_pconsts_in_term thy t) []
(* Inserts a dummy "constant" referring to the theory name, so that relevance
takes the given theory into account. *)
@@ -189,9 +176,9 @@
fun theory_const_prop_of fudge th =
theory_constify fudge (Context.theory_name (theory_of_thm th)) (prop_of th)
-fun pair_consts_fact thy is_built_in_const fudge fact =
+fun pair_consts_fact thy fudge fact =
case fact |> snd |> theory_const_prop_of fudge
- |> pconsts_in_fact thy is_built_in_const of
+ |> pconsts_in_fact thy of
[] => NONE
| consts => SOME ((fact, consts), NONE)
@@ -206,13 +193,11 @@
EQUAL => dict_ord patternT_ord (ps, qs)
| ord => ord)
| (TVar _, TVar _) => EQUAL
- | (TVar _, Type _) => LESS
- | (TVar _, TFree _) => LESS
+ | (TVar _, _) => LESS
| (Type _, TVar _) => GREATER
- | (TFree _, TVar _) => GREATER
| (Type _, TFree _) => LESS
- | (TFree _, Type _) => GREATER
| (TFree (s, _), TFree (t, _)) => fast_string_ord (s, t)
+ | (TFree _, _) => GREATER
fun ptype_ord (PType (m, ps), PType (n, qs)) =
(case dict_ord patternT_ord (ps, qs) of
EQUAL => int_ord (m, n)
@@ -357,23 +342,23 @@
(accepts, more_rejects @ rejects)
end
-fun if_empty_replace_with_scope thy is_built_in_const facts sc tab =
+fun if_empty_replace_with_scope thy facts sc tab =
if Symtab.is_empty tab then
Symtab.empty
- |> fold (add_pconsts_in_term thy is_built_in_const)
+ |> fold (add_pconsts_in_term thy)
(map_filter (fn ((_, (sc', _)), th) =>
if sc' = sc then SOME (prop_of th) else NONE) facts)
else
tab
-fun consider_arities is_built_in_const th =
+fun consider_arities th =
let
fun aux _ _ NONE = NONE
| aux t args (SOME tab) =
case t of
t1 $ t2 => SOME tab |> aux t1 (t2 :: args) |> aux t2 []
- | Const (x as (s, _)) =>
- (if is_built_in_const x args |> fst then
+ | Const (s, _) =>
+ (if is_widely_irrelevant_const s then
SOME tab
else case Symtab.lookup tab s of
NONE => SOME (Symtab.update (s, length args) tab)
@@ -382,9 +367,8 @@
in aux (prop_of th) [] end
(* FIXME: This is currently only useful for polymorphic type encodings. *)
-fun could_benefit_from_ext is_built_in_const facts =
- fold (consider_arities is_built_in_const o snd) facts (SOME Symtab.empty)
- |> is_none
+fun could_benefit_from_ext facts =
+ fold (consider_arities o snd) facts (SOME Symtab.empty) |> is_none
(* High enough so that it isn't wrongly considered as very relevant (e.g., for E
weights), but low enough so that it is unlikely to be truncated away if few
@@ -395,13 +379,12 @@
val really_hopeless_get_kicked_out_iter = 5 (* FUDGE *)
-fun relevance_filter ctxt thres0 decay max_facts is_built_in_const
- (fudge as {threshold_divisor, ridiculous_threshold, ...}) facts hyp_ts
- concl_t =
+fun relevance_filter ctxt thres0 decay max_facts
+ (fudge as {threshold_divisor, ridiculous_threshold, ...}) facts hyp_ts concl_t =
let
val thy = Proof_Context.theory_of ctxt
val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty
- val add_pconsts = add_pconsts_in_term thy is_built_in_const
+ val add_pconsts = add_pconsts_in_term thy
val chained_ts =
facts |> map_filter (fn ((_, (Chained, _)), th) => SOME (prop_of th)
| _ => NONE)
@@ -411,8 +394,7 @@
|> fold add_pconsts hyp_ts
|> add_pconsts concl_t
|> (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]
+ |> fold (if_empty_replace_with_scope thy facts) [Chained, Assum, Local]
fun iter j remaining_max thres rel_const_tab hopeless hopeful =
let
val hopeless =
@@ -509,11 +491,11 @@
in bef @ add @ after end
fun insert_special_facts accepts =
(* FIXME: get rid of "ext" here once it is treated as a helper *)
- [] |> could_benefit_from_ext is_built_in_const accepts ? cons @{thm ext}
+ [] |> could_benefit_from_ext accepts ? cons @{thm ext}
|> add_set_const_thms accepts
|> insert_into_facts accepts
in
- facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)
+ facts |> map_filter (pair_consts_fact thy fudge)
|> iter 0 max_facts thres0 goal_const_tab []
|> insert_special_facts
|> tap (fn accepts => trace_msg ctxt (fn () =>
@@ -525,8 +507,6 @@
max_facts fudge hyp_ts concl_t facts =
let
val thy = Proof_Context.theory_of ctxt
- val is_built_in_const =
- Sledgehammer_Provers.is_built_in_const_of_prover ctxt prover
val fudge =
case fudge of
SOME fudge => fudge
@@ -534,16 +514,14 @@
val decay = Math.pow ((1.0 - thres1) / (1.0 - thres0),
1.0 / Real.fromInt (max_facts + 1))
in
- trace_msg ctxt (fn () => "Considering " ^ string_of_int (length facts) ^
- " facts");
+ trace_msg ctxt (fn () => "Considering " ^ string_of_int (length facts) ^ " facts");
(if thres1 < 0.0 then
facts
else if thres0 > 1.0 orelse thres0 > thres1 then
[]
else
- relevance_filter ctxt thres0 decay max_facts is_built_in_const fudge
- facts hyp_ts
- (concl_t |> theory_constify fudge (Context.theory_name thy)))
+ relevance_filter ctxt thres0 decay max_facts fudge facts hyp_ts
+ (concl_t |> theory_constify fudge (Context.theory_name thy)))
|> map fact_of_raw_fact
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Oct 09 10:47:43 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Oct 09 15:39:34 2013 +0200
@@ -120,8 +120,6 @@
val default_max_facts_of_prover : Proof.context -> bool -> string -> int
val is_unit_equality : term -> bool
val is_appropriate_prop_of_prover : Proof.context -> string -> term -> bool
- val is_built_in_const_of_prover :
- Proof.context -> string -> string * typ -> term list -> bool * term list
val atp_relevance_fudge : relevance_fudge
val smt_relevance_fudge : relevance_fudge
val relevance_fudge_of_prover : Proof.context -> string -> relevance_fudge
@@ -275,23 +273,6 @@
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 andalso Config.get ctxt smt_builtin_facts then
- let val ctxt = ctxt |> select_smt_solver name in
- fn x => fn ts =>
- if SMT_Builtin.is_builtin_num_ext ctxt (list_comb (Const x, ts)) then
- (true, [])
- else if SMT_Builtin.is_builtin_fun_ext ctxt x ts then
- (true, ts)
- else
- (false, ts)
- end
- else
- fn (s, _) => fn ts => (Symtab.defined atp_irrelevant_const_tab s, ts)
-
(* FUDGE *)
val atp_relevance_fudge =
{local_const_multiplier = 1.5,
@@ -1028,10 +1009,8 @@
val is_boring_builtin_typ =
not o exists_subtype (member (op =) [@{typ nat}, @{typ int}, HOLogic.realT])
-fun smt_filter_loop name
- ({debug, verbose, overlord, max_mono_iters,
- max_new_mono_instances, timeout, slice, ...} : params)
- state goal i =
+fun smt_filter_loop name ({debug, overlord, max_mono_iters, max_new_mono_instances, timeout, slice,
+ ...} : params) state goal i =
let
fun repair_context ctxt =
ctxt |> select_smt_solver name