# HG changeset patch # User blanchet # Date 1275899850 -7200 # Node ID 4c8642087c6367c88862228bba4c46cda3a292f9 # Parent c333da19fe6707eaf57fea39933fed0429388f41# Parent 3d7058e24b7a5ab95bc1d4f1bba8cec15304c66e merged diff -r c333da19fe67 -r 4c8642087c63 src/HOL/Tools/ATP_Manager/atp_systems.ML --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Sun Jun 06 18:47:29 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Mon Jun 07 10:37:30 2010 +0200 @@ -239,14 +239,14 @@ fun generic_tptp_prover (name, {home_var, executable, arguments, proof_delims, known_failures, max_axiom_clauses, prefers_theory_relevant}) - (params as {debug, overlord, respect_no_atp, relevance_threshold, - relevance_convergence, theory_relevant, defs_relevant, - isar_proof, ...}) + (params as {debug, overlord, full_types, respect_no_atp, + relevance_threshold, relevance_convergence, theory_relevant, + defs_relevant, isar_proof, ...}) minimize_command timeout = generic_prover overlord - (get_relevant_facts respect_no_atp relevance_threshold - relevance_convergence defs_relevant max_axiom_clauses - (the_default prefers_theory_relevant theory_relevant)) + (relevant_facts full_types respect_no_atp relevance_threshold + relevance_convergence defs_relevant max_axiom_clauses + (the_default prefers_theory_relevant theory_relevant)) (prepare_clauses false) (write_tptp_file (debug andalso overlord)) home_var executable (arguments timeout) proof_delims known_failures name params @@ -276,7 +276,7 @@ known_failures = [(Unprovable, "Satisfiability detected"), (Unprovable, "UNPROVABLE"), - (OutOfResources, "CANNOT PROVE"), + (Unprovable, "CANNOT PROVE"), (OutOfResources, "Refutation not found")], max_axiom_clauses = 60, prefers_theory_relevant = false} @@ -314,13 +314,13 @@ fun generic_dfg_prover (name, {home_var, executable, arguments, proof_delims, known_failures, max_axiom_clauses, prefers_theory_relevant}) - (params as {overlord, respect_no_atp, relevance_threshold, + (params as {overlord, full_types, respect_no_atp, relevance_threshold, relevance_convergence, theory_relevant, defs_relevant, ...}) minimize_command timeout = generic_prover overlord - (get_relevant_facts respect_no_atp relevance_threshold - relevance_convergence defs_relevant max_axiom_clauses - (the_default prefers_theory_relevant theory_relevant)) + (relevant_facts full_types respect_no_atp relevance_threshold + relevance_convergence defs_relevant max_axiom_clauses + (the_default prefers_theory_relevant theory_relevant)) (prepare_clauses true) write_dfg_file home_var executable (arguments timeout) proof_delims known_failures name params minimize_command diff -r c333da19fe67 -r 4c8642087c63 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Sun Jun 06 18:47:29 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Jun 07 10:37:30 2010 +0200 @@ -16,11 +16,13 @@ del: Facts.ref list, only: bool} + val name_thms_pair_from_ref : + Proof.context -> thm list -> Facts.ref -> string * thm list val tvar_classes_of_terms : term list -> string list val tfree_classes_of_terms : term list -> string list val type_consts_of_terms : theory -> term list -> string list - val get_relevant_facts : - bool -> real -> real -> bool -> int -> bool -> relevance_override + val relevant_facts : + bool -> bool -> real -> real -> bool -> int -> bool -> relevance_override -> Proof.context * (thm list * 'a) -> thm list -> (thm * (string * int)) list val prepare_clauses : @@ -253,36 +255,41 @@ end end; +fun cnf_for_facts ctxt = + let val thy = ProofContext.theory_of ctxt in + maps (maps (cnf_axiom thy) o ProofContext.get_fact ctxt) + end + fun relevant_clauses ctxt relevance_convergence defs_relevant max_new - (relevance_override as {add, del, only}) thy ctab = + (relevance_override as {add, del, ...}) ctab = let - val thms_for_facts = - maps (maps (cnf_axiom thy) o ProofContext.get_fact ctxt) - val add_thms = thms_for_facts add - val del_thms = thms_for_facts del - fun iter p rel_consts = + val thy = ProofContext.theory_of ctxt + val add_thms = cnf_for_facts ctxt add + val del_thms = cnf_for_facts ctxt del + fun iter threshold rel_consts = let fun relevant ([], _) [] = [] (* Nothing added this iteration *) - | relevant (newpairs,rejects) [] = + | relevant (newpairs, rejects) [] = let val (newrels, more_rejects) = take_best max_new newpairs val new_consts = maps #2 newrels val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts - val newp = p + (1.0 - p) / relevance_convergence + val threshold = + threshold + (1.0 - threshold) / relevance_convergence in trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels)); - map #1 newrels @ iter newp rel_consts' (more_rejects @ rejects) + map #1 newrels @ iter threshold rel_consts' + (more_rejects @ rejects) end | relevant (newrels, rejects) ((ax as (clsthm as (thm, (name, n)), consts_typs)) :: axs) = let - val weight = if member Thm.eq_thm del_thms thm then 0.0 - else if member Thm.eq_thm add_thms thm then 1.0 - else if only then 0.0 + val weight = if member Thm.eq_thm add_thms thm then 1.0 + else if member Thm.eq_thm del_thms thm then 0.0 else clause_weight ctab rel_consts consts_typs in - if p <= weight orelse + if weight >= threshold orelse (defs_relevant andalso defines thy (#1 clsthm) rel_consts) then (trace_msg (fn () => name ^ " clause " ^ Int.toString n ^ " passes: " ^ Real.toString weight); @@ -291,8 +298,8 @@ relevant (newrels, ax :: rejects) axs end in - trace_msg (fn () => "relevant_clauses, current pass mark: " ^ - Real.toString p); + trace_msg (fn () => "relevant_clauses, current threshold: " ^ + Real.toString threshold); relevant ([], []) end in iter end @@ -310,7 +317,7 @@ commas (Symtab.keys goal_const_tab)) val relevant = relevant_clauses ctxt relevance_convergence defs_relevant max_new - relevance_override thy const_tab relevance_threshold + relevance_override const_tab relevance_threshold goal_const_tab (map (pair_consts_typs_axiom theory_relevant thy) axioms) @@ -352,7 +359,7 @@ fun subtract_cls ax_clauses = filter_out (Termtab.defined (mk_clause_table ax_clauses) o prop_of) -fun all_valid_thms respect_no_atp ctxt chained_ths = +fun all_name_thms_pairs respect_no_atp ctxt chained_ths = let val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt); val local_facts = ProofContext.facts_of ctxt; @@ -369,7 +376,7 @@ val name1 = Facts.extern facts name; val name2 = Name_Space.extern full_space name; - val ths = filter_out bad_for_atp ths0; + val ths = filter_out is_theorem_bad_for_atps ths0; in if Facts.is_concealed facts name orelse (respect_no_atp andalso is_package_def name) then @@ -398,26 +405,32 @@ (* The single-name theorems go after the multiple-name ones, so that single names are preferred when both are available. *) -fun name_thm_pairs respect_no_atp ctxt chained_ths = +fun name_thm_pairs respect_no_atp ctxt name_thms_pairs = let - val (mults, singles) = - List.partition is_multi (all_valid_thms respect_no_atp ctxt chained_ths) + val (mults, singles) = List.partition is_multi name_thms_pairs val ps = [] |> fold add_single_names singles |> fold add_multi_names mults in ps |> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) end; -fun check_named ("", th) = - (warning ("No name for theorem " ^ Display.string_of_thm_without_context th); false) - | check_named _ = true; +fun is_named ("", th) = + (warning ("No name for theorem " ^ + Display.string_of_thm_without_context th); false) + | is_named _ = true +fun checked_name_thm_pairs respect_no_atp ctxt = + name_thm_pairs respect_no_atp ctxt + #> tap (fn ps => trace_msg + (fn () => ("Considering " ^ Int.toString (length ps) ^ + " theorems"))) + #> filter is_named -fun get_all_lemmas respect_no_atp ctxt chained_ths = - let val included_thms = - tap (fn ths => trace_msg - (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems"))) - (name_thm_pairs respect_no_atp ctxt chained_ths) - in - filter check_named included_thms - end; +fun name_thms_pair_from_ref ctxt chained_ths xref = + let + val ths = ProofContext.get_fact ctxt xref + val name = Facts.string_of_ref xref + |> forall (member Thm.eq_thm chained_ths) ths + ? prefix chained_prefix + in (name, ths) end + (***************************************************************) (* Type Classes Present in the Axiom or Conjecture Clauses *) @@ -463,26 +476,29 @@ fun restrict_to_logic thy true cls = filter (Meson.is_fol_term thy o prop_of o fst) cls | restrict_to_logic thy false cls = cls; -(**** Predicates to detect unwanted clauses (prolific or likely to cause unsoundness) ****) +(**** Predicates to detect unwanted clauses (prolific or likely to cause + unsoundness) ****) (** Too general means, positive equality literal with a variable X as one operand, when X does not occur properly in the other operand. This rules out clearly inconsistent clauses such as V=a|V=b, though it by no means guarantees soundness. **) -fun occurs ix = - let fun occ(Var (jx,_)) = (ix=jx) - | occ(t1$t2) = occ t1 orelse occ t2 - | occ(Abs(_,_,t)) = occ t - | occ _ = false - in occ end; +fun var_occurs_in_term ix = + let + fun aux (Var (jx, _)) = (ix = jx) + | aux (t1 $ t2) = aux t1 orelse aux t2 + | aux (Abs (_, _, t)) = aux t + | aux _ = false + in aux end -fun is_recordtype T = not (null (Record.dest_recTs T)); +fun is_record_type T = not (null (Record.dest_recTs T)) (*Unwanted equalities include (1) those between a variable that does not properly occur in the second operand, (2) those between a variable and a record, since these seem to be prolific "cases" thms *) -fun too_general_eqterms (Var (ix,T), t) = not (occurs ix t) orelse is_recordtype T +fun too_general_eqterms (Var (ix,T), t) = + not (var_occurs_in_term ix t) orelse is_record_type T | too_general_eqterms _ = false; fun too_general_equality (Const (@{const_name "op ="}, _) $ x $ y) = @@ -492,40 +508,56 @@ fun has_typed_var tycons = exists_subterm (fn Var (_, Type (a, _)) => member (op =) tycons a | _ => false); -(*Clauses are forbidden to contain variables of these types. The typical reason is that - they lead to unsoundness. Note that "unit" satisfies numerous equations like ?X=(). - The resulting clause will have no type constraint, yielding false proofs. Even "bool" - leads to many unsound proofs, though (obviously) only for higher-order problems.*) -val unwanted_types = [@{type_name unit}, @{type_name bool}]; +(* Clauses are forbidden to contain variables of these types. The typical reason + is that they lead to unsoundness. Note that "unit" satisfies numerous + equations like "?x = ()". The resulting clause will have no type constraint, + yielding false proofs. Even "bool" leads to many unsound proofs, though only + for higher-order problems. *) +val dangerous_types = [@{type_name unit}, @{type_name bool}]; -fun unwanted t = - t = @{prop True} orelse has_typed_var unwanted_types t orelse - forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t)); +(* Clauses containing variables of type "unit" or "bool" or of the form + "?x = A | ?x = B | ?x = C" are likely to lead to unsound proofs if types are + omitted. *) +fun is_dangerous_term _ @{prop True} = true + | is_dangerous_term full_types t = + not full_types andalso + (has_typed_var dangerous_types t orelse + forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t))) -(*Clauses containing variables of type "unit" or "bool" are unlikely to be useful and - likely to lead to unsound proofs.*) -fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls; +fun is_dangerous_theorem full_types add_thms thm = + not (member Thm.eq_thm add_thms thm) andalso + is_dangerous_term full_types (prop_of thm) + +fun remove_dangerous_clauses full_types add_thms = + filter_out (is_dangerous_theorem full_types add_thms o fst) fun is_first_order thy = forall (Meson.is_fol_term thy) o map prop_of -fun get_relevant_facts respect_no_atp relevance_threshold relevance_convergence - defs_relevant max_new theory_relevant - (relevance_override as {add, only, ...}) - (ctxt, (chained_ths, _)) goal_cls = +fun relevant_facts full_types respect_no_atp relevance_threshold + relevance_convergence defs_relevant max_new theory_relevant + (relevance_override as {add, del, only}) + (ctxt, (chained_ths, _)) goal_cls = if (only andalso null add) orelse relevance_threshold > 1.0 then [] else let val thy = ProofContext.theory_of ctxt + val add_thms = cnf_for_facts ctxt add + val has_override = not (null add) orelse not (null del) val is_FO = is_first_order thy goal_cls - val included_cls = get_all_lemmas respect_no_atp ctxt chained_ths - |> cnf_rules_pairs thy |> make_unique + val axioms = + checked_name_thm_pairs respect_no_atp ctxt + (if only then map (name_thms_pair_from_ref ctxt chained_ths) add + else all_name_thms_pairs respect_no_atp ctxt chained_ths) + |> cnf_rules_pairs thy + |> not has_override ? make_unique |> restrict_to_logic thy is_FO - |> remove_unwanted_clauses + |> not only ? remove_dangerous_clauses full_types add_thms in relevance_filter ctxt relevance_threshold relevance_convergence defs_relevant max_new theory_relevant relevance_override - thy included_cls (map prop_of goal_cls) + thy axioms (map prop_of goal_cls) + |> has_override ? make_unique end (* prepare for passing to writer, diff -r c333da19fe67 -r 4c8642087c63 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sun Jun 06 18:47:29 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Mon Jun 07 10:37:30 2010 +0200 @@ -14,11 +14,12 @@ val skolem_infix: string val cnf_axiom: theory -> thm -> thm list val multi_base_blacklist: string list - val bad_for_atp: thm -> bool + val is_theorem_bad_for_atps: thm -> bool val type_has_topsort: typ -> bool - val cnf_rules_pairs: theory -> (string * thm) list -> (thm * (string * int)) list - val suppress_endtheory: bool Unsynchronized.ref - (*for emergency use where endtheory causes problems*) + val cnf_rules_pairs: + theory -> (string * thm) list -> (thm * (string * int)) list + val use_skolem_cache: bool Unsynchronized.ref + (* for emergency use where the Skolem cache causes problems *) val strip_subgoal : thm -> int -> (string * typ) list * term list * term val neg_clausify: thm -> thm list val neg_conjecture_clauses: @@ -86,9 +87,9 @@ val rhs_consts = fold_aterms (fn Const c => insert (op =) c | _ => I) rhs [] in fold (#2 #> Term.fold_atyps add_new_TFrees) rhs_consts [] end; -(*Traverse a theorem, declaring Skolem function definitions. String s is the suggested - prefix for the Skolem constant.*) -fun declare_skofuns s th = +(* Traverse a theorem, declaring Skolem function definitions. String "s" is the + suggested prefix for the Skolem constants. *) +fun declare_skolem_funs s th thy = let val nref = Unsynchronized.ref 0 (* FIXME ??? *) fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs (s', T, p))) (axs, thy) = @@ -103,13 +104,13 @@ val cT = extraTs ---> Ts ---> T val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp) (*Forms a lambda-abstraction over the formal parameters*) - val (c, thy') = + val (c, thy) = Sign.declare_const ((Binding.conceal (Binding.name cname), cT), NoSyn) thy val cdef = cname ^ "_def" - val ((_, ax), thy'') = - Thm.add_def true false (Binding.name cdef, Logic.mk_equals (c, rhs)) thy' + val ((_, ax), thy) = + Thm.add_def true false (Binding.name cdef, Logic.mk_equals (c, rhs)) thy val ax' = Drule.export_without_context ax - in dec_sko (subst_bound (list_comb (c, args), p)) (ax' :: axs, thy'') end + in dec_sko (subst_bound (list_comb (c, args), p)) (ax' :: axs, thy) end | dec_sko (Const (@{const_name All}, _) $ (Abs (a, T, p))) thx = (*Universal quant: insert a free variable into body and continue*) let val fname = Name.variant (OldTerm.add_term_names (p, [])) a @@ -117,11 +118,11 @@ | dec_sko (@{const "op &"} $ p $ q) thx = dec_sko q (dec_sko p thx) | dec_sko (@{const "op |"} $ p $ q) thx = dec_sko q (dec_sko p thx) | dec_sko (@{const Trueprop} $ p) thx = dec_sko p thx - | dec_sko t thx = thx (*Do nothing otherwise*) - in fn thy => dec_sko (Thm.prop_of th) ([], thy) end; + | dec_sko t thx = thx + in dec_sko (prop_of th) ([], thy) end (*Traverse a theorem, accumulating Skolem function definitions.*) -fun assume_skofuns s th = +fun assume_skolem_funs s th = let val sko_count = Unsynchronized.ref 0 (* FIXME ??? *) fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs (s', T, p))) defs = (*Existential: declare a Skolem function, then insert into body and continue*) @@ -135,9 +136,7 @@ HOLogic.choice_const T $ xtp) (*Forms a lambda-abstraction over the formal parameters*) val def = Logic.mk_equals (c, rhs) - in dec_sko (subst_bound (list_comb(c,args), p)) - (def :: defs) - end + in dec_sko (subst_bound (list_comb(c,args), p)) (def :: defs) end | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) defs = (*Universal quant: insert a free variable into body and continue*) let val fname = Name.variant (OldTerm.add_term_names (p,[])) a @@ -219,41 +218,44 @@ val crator = cterm_of thy rator val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B} val (_,rhs) = Thm.dest_equals (cprop_of abs_B') - in - Thm.transitive abs_B' (Conv.arg_conv abstract rhs) - end + in Thm.transitive abs_B' (Conv.arg_conv abstract rhs) end else makeK() - | _ => error "abstract: Bad term" + | _ => raise Fail "abstract: Bad term" end; -(*Traverse a theorem, declaring abstraction function definitions. String s is the suggested - prefix for the constants.*) -fun combinators_aux ct = - if lambda_free (term_of ct) then Thm.reflexive ct +(* Traverse a theorem, remplacing lambda-abstractions with combinators. *) +fun do_introduce_combinators ct = + if lambda_free (term_of ct) then + Thm.reflexive ct + else case term_of ct of + Abs _ => + let + val (cv, cta) = Thm.dest_abs NONE ct + val (v, _) = dest_Free (term_of cv) + val u_th = do_introduce_combinators cta + val cu = Thm.rhs_of u_th + val comb_eq = abstract (Thm.cabs cv cu) + in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end + | _ $ _ => + let val (ct1, ct2) = Thm.dest_comb ct in + Thm.combination (do_introduce_combinators ct1) + (do_introduce_combinators ct2) + end + +fun introduce_combinators th = + if lambda_free (prop_of th) then + th else - case term_of ct of - Abs _ => - let val (cv, cta) = Thm.dest_abs NONE ct - val (v, _) = dest_Free (term_of cv) - val u_th = combinators_aux cta - val cu = Thm.rhs_of u_th - val comb_eq = abstract (Thm.cabs cv cu) - in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end - | _ $ _ => - let val (ct1, ct2) = Thm.dest_comb ct - in Thm.combination (combinators_aux ct1) (combinators_aux ct2) end; - -fun combinators th = - if lambda_free (prop_of th) then th - else - let val th = Drule.eta_contraction_rule th - val eqth = combinators_aux (cprop_of th) - in Thm.equal_elim eqth th end - handle THM (msg,_,_) => - (warning (cat_lines - ["Error in the combinator translation of " ^ Display.string_of_thm_without_context th, - " Exception message: " ^ msg]); - TrueI); (*A type variable of sort {} will cause make abstraction fail.*) + let + val th = Drule.eta_contraction_rule th + val eqth = do_introduce_combinators (cprop_of th) + in Thm.equal_elim eqth th end + handle THM (msg, _, _) => + (warning ("Error in the combinator translation of " ^ + Display.string_of_thm_without_context th ^ + "\nException message: " ^ msg ^ "."); + (* A type variable of sort "{}" will make abstraction fail. *) + TrueI) (*cterms are used throughout for efficiency*) val cTrueprop = Thm.cterm_of @{theory HOL} HOLogic.Trueprop; @@ -302,37 +304,43 @@ (*Generate Skolem functions for a theorem supplied in nnf*) fun assume_skolem_of_def s th = - map (skolem_of_def o Thm.assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th); + map (skolem_of_def o Thm.assume o cterm_of (theory_of_thm th)) + (assume_skolem_funs s th) -(*** Blacklisting (FIXME: duplicated in "Sledgehammer_Fact_Filter"?) ***) +(*** Blacklisting (more in "Sledgehammer_Fact_Filter") ***) -val max_lambda_nesting = 3; +val max_lambda_nesting = 3 -fun excessive_lambdas (f$t, k) = excessive_lambdas (f,k) orelse excessive_lambdas (t,k) - | excessive_lambdas (Abs(_,_,t), k) = k=0 orelse excessive_lambdas (t,k-1) - | excessive_lambdas _ = false; +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); +fun is_formula_type T = (T = HOLogic.boolT orelse T = propT) -(*Don't count nested lambdas at the level of formulas, as they are quantifiers*) -fun excessive_lambdas_fm Ts (Abs(_,T,t)) = excessive_lambdas_fm (T::Ts) t - | excessive_lambdas_fm Ts t = - if is_formula_type (fastype_of1 (Ts, t)) - then exists (excessive_lambdas_fm Ts) (#2 (strip_comb t)) - else excessive_lambdas (t, max_lambda_nesting); +(* 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; +(* 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 apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1) + | apply_depth (Abs (_, _, t)) = apply_depth t + | apply_depth _ = 0 -fun too_complex t = - apply_depth t > max_apply_depth orelse - Meson.too_many_clauses NONE t orelse - excessive_lambdas_fm [] t; +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 @@ -340,10 +348,11 @@ a <> @{const_name "=="}) | _ => false; -fun bad_for_atp th = - too_complex (prop_of th) - orelse exists_type type_has_topsort (prop_of th) - orelse is_strange_thm th; +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" *) val multi_base_blacklist = @@ -356,14 +365,21 @@ (*Skolemize a named theorem, with Skolem functions as additional premises.*) fun skolem_thm (s, th) = - if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse bad_for_atp th then [] + if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse + is_theorem_bad_for_atps th then + [] else let val ctxt0 = Variable.global_thm_context th - val (nnfth, ctxt1) = to_nnf th ctxt0 - val (cnfs, ctxt2) = Meson.make_cnf (assume_skolem_of_def s nnfth) nnfth ctxt1 - in cnfs |> map combinators |> Variable.export ctxt2 ctxt0 |> Meson.finish_cnf end - handle THM _ => []; + val (nnfth, ctxt) = to_nnf th ctxt0 + val defs = assume_skolem_of_def s nnfth + val (cnfs, ctxt) = Meson.make_cnf defs nnfth ctxt + in + cnfs |> map introduce_combinators + |> Variable.export ctxt ctxt0 + |> Meson.finish_cnf + end + handle THM _ => [] (*The cache prevents repeated clausification of a theorem, and also repeated declaration of Skolem functions.*) @@ -413,19 +429,19 @@ fun skolem_def (name, th) thy = let val ctxt0 = Variable.global_thm_context th in - (case try (to_nnf th) ctxt0 of + case try (to_nnf th) ctxt0 of NONE => (NONE, thy) - | SOME (nnfth, ctxt1) => - let val (defs, thy') = declare_skofuns (flatten_name name) nnfth thy - in (SOME (th, ctxt0, ctxt1, nnfth, defs), thy') end) + | SOME (nnfth, ctxt) => + let val (defs, thy') = declare_skolem_funs (flatten_name name) nnfth thy + in (SOME (th, ctxt0, ctxt, nnfth, defs), thy') end end; -fun skolem_cnfs (th, ctxt0, ctxt1, nnfth, defs) = +fun skolem_cnfs (th, ctxt0, ctxt, nnfth, defs) = let - val (cnfs, ctxt2) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt1; + val (cnfs, ctxt) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt; val cnfs' = cnfs - |> map combinators - |> Variable.export ctxt2 ctxt0 + |> map introduce_combinators + |> Variable.export ctxt ctxt0 |> Meson.finish_cnf |> map Thm.close_derivation; in (th, cnfs') end; @@ -441,8 +457,10 @@ val new_thms = (new_facts, []) |-> fold (fn (name, ths) => if member (op =) multi_base_blacklist (Long_Name.base_name name) then I else fold_index (fn (i, th) => - if bad_for_atp th orelse is_some (lookup_cache thy th) then I - else cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths); + if is_theorem_bad_for_atps th orelse is_some (lookup_cache thy th) then + I + else + cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths) in if null new_facts then NONE else @@ -457,11 +475,10 @@ end; -val suppress_endtheory = Unsynchronized.ref false +val use_skolem_cache = Unsynchronized.ref true fun clause_cache_endtheory thy = - if ! suppress_endtheory then NONE - else saturate_skolem_cache thy; + if !use_skolem_cache then saturate_skolem_cache thy else NONE (*The cache can be kept smaller by inspecting the prop of each thm. Can ignore all that are @@ -481,7 +498,10 @@ EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt] val neg_clausify = - single #> Meson.make_clauses_unsorted #> map combinators #> Meson.finish_cnf + single + #> Meson.make_clauses_unsorted + #> map introduce_combinators + #> Meson.finish_cnf fun neg_conjecture_clauses ctxt st0 n = let @@ -509,7 +529,7 @@ (** setup **) val setup = - perhaps saturate_skolem_cache #> - Theory.at_end clause_cache_endtheory; + perhaps saturate_skolem_cache + #> Theory.at_end clause_cache_endtheory end; diff -r c333da19fe67 -r 4c8642087c63 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun Jun 06 18:47:29 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jun 07 10:37:30 2010 +0200 @@ -19,6 +19,7 @@ struct open Sledgehammer_Util +open Sledgehammer_Fact_Filter open Sledgehammer_Fact_Preprocessor open ATP_Manager open ATP_Systems @@ -238,19 +239,12 @@ state) atps in () end -fun minimize override_params i frefs state = +fun minimize override_params i refs state = let val thy = Proof.theory_of state val ctxt = Proof.context_of state val chained_ths = #facts (Proof.goal state) - fun theorems_from_ref ctxt fref = - let - val ths = ProofContext.get_fact ctxt fref - val name = Facts.string_of_ref fref - |> forall (member Thm.eq_thm chained_ths) ths - ? prefix chained_prefix - in (name, ths) end - val name_thms_pairs = map (theorems_from_ref ctxt) frefs + val name_thms_pairs = map (name_thms_pair_from_ref ctxt chained_ths) refs in case subgoal_count state of 0 => priority "No subgoal!"