move blacklisting completely out of the clausifier;
the only reason it was in the clausifier as well was the Skolem cache
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Tue Jun 29 09:26:56 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Tue Jun 29 10:25:53 2010 +0200
@@ -8,9 +8,6 @@
signature CLAUSIFIER =
sig
val cnf_axiom: theory -> thm -> thm list
- val multi_base_blacklist: string list
- val is_theorem_bad_for_atps: thm -> bool
- val type_has_topsort: typ -> bool
val cnf_rules_pairs :
theory -> (string * thm) list -> ((string * int) * thm) list
val neg_clausify: thm -> thm list
@@ -21,12 +18,6 @@
structure Clausifier : CLAUSIFIER =
struct
-val type_has_topsort = Term.exists_subtype
- (fn TFree (_, []) => true
- | TVar (_, []) => true
- | _ => false);
-
-
(**** Transformation of Elimination Rules into First-Order Formulas****)
val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
@@ -237,77 +228,20 @@
|> Meson.make_nnf ctxt
in (th3, ctxt) end;
-(*** Blacklisting (more in "Sledgehammer_Fact_Filter") ***)
-
-val max_lambda_nesting = 3
-
-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
-
-fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
-
-(* 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 is_formula_type (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 max apply depth of any "metis" call in "Metis_Examples" (on 31-10-2007)
- was 11. *)
-val max_apply_depth = 15
-
-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_formula_too_complex t =
- apply_depth t > max_apply_depth orelse Meson.too_many_clauses NONE t orelse
- formula_has_too_many_lambdas [] t
-
-fun is_strange_thm th =
- case head_of (concl_of th) of
- Const (a, _) => (a <> @{const_name Trueprop} andalso
- a <> @{const_name "=="})
- | _ => false;
-
-fun is_theorem_bad_for_atps thm =
- let val t = prop_of thm in
- is_formula_too_complex t orelse exists_type type_has_topsort t orelse
- is_strange_thm thm
- end
-
-(* FIXME: put other record thms here, or declare as "no_atp" *)
-(* FIXME: move to "Sledgehammer_Fact_Filter" *)
-val multi_base_blacklist =
- ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits",
- "split_asm", "cases", "ext_cases"];
-
(*Skolemize a named theorem, with Skolem functions as additional premises.*)
fun skolemize_theorem thy th =
- if member (op =) multi_base_blacklist
- (Long_Name.base_name (Thm.get_name_hint th)) orelse
- is_theorem_bad_for_atps th then
- []
- else
- let
- val ctxt0 = Variable.global_thm_context th
- val (nnfth, ctxt) = to_nnf th ctxt0
- val sko_ths = map (skolem_theorem_of_def thy) (assume_skolem_funs nnfth)
- val (cnfs, ctxt) = Meson.make_cnf sko_ths nnfth ctxt
- in
- cnfs |> map introduce_combinators
- |> Variable.export ctxt ctxt0
- |> Meson.finish_cnf
- |> map Thm.close_derivation
- end
- handle THM _ => []
+ let
+ val ctxt0 = Variable.global_thm_context th
+ val (nnfth, ctxt) = to_nnf th ctxt0
+ val sko_ths = map (skolem_theorem_of_def thy) (assume_skolem_funs nnfth)
+ val (cnfs, ctxt) = Meson.make_cnf sko_ths nnfth ctxt
+ in
+ cnfs |> map introduce_combinators
+ |> Variable.export ctxt ctxt0
+ |> Meson.finish_cnf
+ |> map Thm.close_derivation
+ end
+ handle THM _ => []
(* Convert Isabelle theorems into axiom clauses. *)
(* FIXME: is transfer necessary? *)
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Jun 29 09:26:56 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Jun 29 10:25:53 2010 +0200
@@ -779,11 +779,14 @@
raise METIS ("FOL_SOLVE", ""))
end;
+val type_has_top_sort =
+ exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
+
fun generic_metis_tac mode ctxt ths i st0 =
let val _ = trace_msg (fn () =>
"Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
in
- if exists_type type_has_topsort (prop_of st0) then
+ if exists_type type_has_top_sort (prop_of st0) then
(warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
else
(Meson.MESON (maps neg_clausify)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Jun 29 09:26:56 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Jun 29 10:25:53 2010 +0200
@@ -393,8 +393,60 @@
fun make_unique xs =
Termtab.fold (cons o snd) (make_clause_table xs) []
+(* FIXME: put other record thms here, or declare as "no_atp" *)
+val multi_base_blacklist =
+ ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits",
+ "split_asm", "cases", "ext_cases"]
+
+val max_lambda_nesting = 3
+
+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
+
+fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
+
+(* 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 is_formula_type (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 max apply depth of any "metis" call in "Metis_Examples" (on 31-10-2007)
+ was 11. *)
+val max_apply_depth = 15
+
+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_formula_too_complex t =
+ apply_depth t > max_apply_depth orelse Meson.too_many_clauses NONE t orelse
+ formula_has_too_many_lambdas [] t
+
val exists_sledgehammer_const =
- exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s) o prop_of
+ exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
+
+fun is_strange_thm th =
+ case head_of (concl_of th) of
+ Const (a, _) => (a <> @{const_name Trueprop} andalso
+ a <> @{const_name "=="})
+ | _ => false
+
+val type_has_top_sort =
+ exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
+
+fun is_theorem_bad_for_atps thm =
+ let val t = prop_of thm in
+ is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
+ exists_sledgehammer_const t orelse is_strange_thm thm
+ end
fun all_name_thms_pairs ctxt chained_ths =
let
@@ -407,8 +459,7 @@
(facts, []) |-> Facts.fold_static (fn (name, ths0) =>
if Facts.is_concealed facts name orelse
(respect_no_atp andalso is_package_def name) orelse
- member (op =) Clausifier.multi_base_blacklist
- (Long_Name.base_name name) then
+ member (op =) multi_base_blacklist (Long_Name.base_name name) then
I
else
let
@@ -419,8 +470,7 @@
val name1 = Facts.extern facts name;
val name2 = Name_Space.extern full_space name;
- val ths = filter_out (Clausifier.is_theorem_bad_for_atps orf
- exists_sledgehammer_const) ths0
+ val ths = filter_out is_theorem_bad_for_atps ths0
in
case find_first check_thms [name1, name2, name] of
NONE => I