# HG changeset patch # User blanchet # Date 1381325974 -7200 # Node ID b13f6731f873fdd89ee58c0482748a4327735564 # Parent 40366d99fa39b87413a82bf78705033e56c5227b 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) diff -r 40366d99fa39 -r b13f6731f873 src/HOL/TPTP/mash_export.ML --- 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 diff -r 40366d99fa39 -r b13f6731f873 src/HOL/Tools/ATP/atp_problem_generate.ML --- 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 = diff -r 40366d99fa39 -r b13f6731f873 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- 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 diff -r 40366d99fa39 -r b13f6731f873 src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML --- 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 diff -r 40366d99fa39 -r b13f6731f873 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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