# HG changeset patch # User blanchet # Date 1277216609 -7200 # Node ID 7587b6e6345444b1cdd53d4d3962b6f7dcfcea3b # Parent 5ff37037fbeccec86ac9890b10342d82a1c7284a thread original theorem along with CNF theorem, as a step toward killing the Skolem cache diff -r 5ff37037fbec -r 7587b6e63454 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Jun 22 14:48:46 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Jun 22 16:23:29 2010 +0200 @@ -8,7 +8,8 @@ signature ATP_MANAGER = sig - type name_pool = Sledgehammer_HOL_Clause.name_pool + type name_pool = Sledgehammer_FOL_Clause.name_pool + type cnf_thm = Sledgehammer_Fact_Preprocessor.cnf_thm type relevance_override = Sledgehammer_Fact_Filter.relevance_override type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command type params = @@ -31,8 +32,8 @@ {subgoal: int, goal: Proof.context * (thm list * thm), relevance_override: relevance_override, - axiom_clauses: (thm * (string * int)) list option, - filtered_clauses: (thm * (string * int)) list option} + axiom_clauses: cnf_thm list option, + filtered_clauses: cnf_thm list option} datatype failure = Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError @@ -46,7 +47,7 @@ proof: string, internal_thm_names: string Vector.vector, conjecture_shape: int list list, - filtered_clauses: (thm * (string * int)) list} + filtered_clauses: cnf_thm list} type prover = params -> minimize_command -> Time.time -> problem -> prover_result @@ -91,8 +92,8 @@ {subgoal: int, goal: Proof.context * (thm list * thm), relevance_override: relevance_override, - axiom_clauses: (thm * (string * int)) list option, - filtered_clauses: (thm * (string * int)) list option}; + axiom_clauses: cnf_thm list option, + filtered_clauses: cnf_thm list option} datatype failure = Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass | @@ -108,7 +109,7 @@ proof: string, internal_thm_names: string Vector.vector, conjecture_shape: int list list, - filtered_clauses: (thm * (string * int)) list}; + filtered_clauses: cnf_thm list} type prover = params -> minimize_command -> Time.time -> problem -> prover_result diff -r 5ff37037fbec -r 7587b6e63454 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Jun 22 14:48:46 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Jun 22 16:23:29 2010 +0200 @@ -5,11 +5,10 @@ signature SLEDGEHAMMER_FACT_FILTER = sig + type cnf_thm = Sledgehammer_Fact_Preprocessor.cnf_thm type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause type arity_clause = Sledgehammer_FOL_Clause.arity_clause - type axiom_name = Sledgehammer_HOL_Clause.axiom_name type hol_clause = Sledgehammer_HOL_Clause.hol_clause - type hol_clause_id = Sledgehammer_HOL_Clause.hol_clause_id type relevance_override = {add: Facts.ref list, @@ -24,14 +23,12 @@ val is_quasi_fol_term : theory -> term -> bool val relevant_facts : bool -> bool -> real -> real -> bool -> int -> bool -> relevance_override - -> Proof.context * (thm list * 'a) -> thm list - -> (thm * (string * int)) list + -> Proof.context * (thm list * 'a) -> thm list -> cnf_thm list val prepare_clauses : - bool -> thm list -> (thm * (axiom_name * hol_clause_id)) list - -> (thm * (axiom_name * hol_clause_id)) list -> theory - -> axiom_name vector - * (hol_clause list * hol_clause list * hol_clause list * - hol_clause list * classrel_clause list * arity_clause list) + bool -> thm list -> cnf_thm list -> cnf_thm list -> theory + -> string vector + * (hol_clause list * hol_clause list * hol_clause list + * hol_clause list * classrel_clause list * arity_clause list) end; structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER = @@ -234,13 +231,13 @@ | _ => false end; -type annotd_cls = (thm * (string * int)) * ((string * const_typ list) list); +type annotated_clause = cnf_thm * ((string * const_typ list) list) (*For a reverse sort, putting the largest values first.*) -fun compare_pairs ((_,w1),(_,w2)) = Real.compare (w2,w1); +fun compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1) (*Limit the number of new clauses, to prevent runaway acceptance.*) -fun take_best max_new (newpairs : (annotd_cls*real) list) = +fun take_best max_new (newpairs : (annotated_clause * real) list) = let val nnew = length newpairs in if nnew <= max_new then (map #1 newpairs, []) @@ -252,7 +249,7 @@ ", exceeds the limit of " ^ Int.toString (max_new))); trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted)))); trace_msg (fn () => "Actually passed: " ^ - space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted)); + space_implode ", " (map (fn (((_,((name,_), _)),_),_) => name) accepted)); (map #1 accepted, map #1 (List.drop (cls, max_new))) end @@ -286,7 +283,8 @@ (more_rejects @ rejects) end | relevant (newrels, rejects) - ((ax as (clsthm as (thm, (name, n)), consts_typs)) :: axs) = + ((ax as (clsthm as (thm, ((name, n), _)), consts_typs)) :: + axs) = let 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 @@ -309,7 +307,7 @@ fun relevance_filter ctxt relevance_threshold relevance_convergence defs_relevant max_new theory_relevant relevance_override - thy axioms goals = + thy (axioms : cnf_thm list) goals = if relevance_threshold > 0.0 then let val const_tab = List.foldl (count_axiom_consts theory_relevant thy) diff -r 5ff37037fbec -r 7587b6e63454 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Tue Jun 22 14:48:46 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Tue Jun 22 16:23:29 2010 +0200 @@ -7,6 +7,7 @@ signature SLEDGEHAMMER_FACT_PREPROCESSOR = sig + type cnf_thm = thm * ((string * int) * thm) val chained_prefix: string val trace: bool Unsynchronized.ref val trace_msg: (unit -> string) -> unit @@ -18,8 +19,7 @@ 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 -> (thm * (string * int)) list + val cnf_rules_pairs : theory -> (string * thm) list -> cnf_thm list val saturate_skolem_cache: theory -> theory option val auto_saturate_skolem_cache: bool Unsynchronized.ref (* for emergency use where the Skolem cache causes problems *) @@ -35,6 +35,8 @@ open Sledgehammer_FOL_Clause +type cnf_thm = thm * ((string * int) * thm) + (* Used to label theorems chained into the goal. *) val chained_prefix = "Sledgehammer.chained_" @@ -153,10 +155,11 @@ val cT = Ts ---> T (* FIXME: use "skolem_type_and_args" *) val id = skolem_name s (Unsynchronized.inc skolem_count) s' val c = Free (id, cT) - val rhs = list_abs_free (map dest_Free args, - HOLogic.choice_const T $ body) - |> inline ? mk_skolem_id - (*Forms a lambda-abstraction over the formal parameters*) + (* Forms a lambda-abstraction over the formal parameters *) + val rhs = + list_abs_free (map dest_Free args, + HOLogic.choice_const T $ body) + |> inline ? mk_skolem_id val def = Logic.mk_equals (c, rhs) val comb = list_comb (if inline then rhs else c, args) in dec_sko (subst_bound (comb, p)) (def :: defs) end @@ -446,20 +449,20 @@ (**** Translate a set of theorems into CNF ****) -fun pair_name_cls _ (_, []) = [] - | pair_name_cls k (n, cls::clss) = (cls, (n,k)) :: pair_name_cls (k+1) (n, clss) - (*The combination of rev and tail recursion preserves the original order*) fun cnf_rules_pairs thy = let - fun aux pairs [] = pairs - | aux pairs ((name, th) :: ths) = + fun do_one _ [] = [] + | do_one ((name, k), th) (cls :: clss) = + (cls, ((name, k), th)) :: do_one ((name, k + 1), th) clss + fun do_all pairs [] = pairs + | do_all pairs ((name, th) :: ths) = let - val new_pairs = pair_name_cls 0 (name, cnf_axiom thy th) + val new_pairs = do_one ((name, 0), th) (cnf_axiom thy th) handle THM _ => [] | CLAUSE _ => [] - in aux (new_pairs @ pairs) ths end - in aux [] o rev end + in do_all (new_pairs @ pairs) ths end + in do_all [] o rev end (**** Convert all facts of the theory into FOL or HOL clauses ****) diff -r 5ff37037fbec -r 7587b6e63454 src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Tue Jun 22 14:48:46 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Tue Jun 22 16:23:29 2010 +0200 @@ -37,7 +37,6 @@ val pool_map : ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b val nice_name : name -> name_pool option -> string * name_pool option datatype kind = Axiom | Conjecture - type axiom_name = string datatype fol_type = TyVar of name | TyFree of name | @@ -53,9 +52,9 @@ TConsLit of class * string * string list | TVarLit of class * string datatype arity_clause = ArityClause of - {axiom_name: axiom_name, conclLit: arLit, premLits: arLit list} + {axiom_name: string, conclLit: arLit, premLits: arLit list} datatype classrel_clause = ClassrelClause of - {axiom_name: axiom_name, subclass: class, superclass: class} + {axiom_name: string, subclass: class, superclass: class} val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list val tptp_sign: bool -> string -> string @@ -259,8 +258,6 @@ datatype kind = Axiom | Conjecture; -type axiom_name = string; - (**** Isabelle FOL clauses ****) datatype fol_type = @@ -308,9 +305,7 @@ | TVarLit of class * string; datatype arity_clause = - ArityClause of {axiom_name: axiom_name, - conclLit: arLit, - premLits: arLit list}; + ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list} fun gen_TVars 0 = [] @@ -334,9 +329,7 @@ (**** Isabelle class relations ****) datatype classrel_clause = - ClassrelClause of {axiom_name: axiom_name, - subclass: class, - superclass: class}; + ClassrelClause of {axiom_name: string, subclass: class, superclass: class} (*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*) fun class_pairs _ [] _ = [] @@ -437,7 +430,8 @@ let val tvar = "(T)" in tptp_clause [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)] end; -fun tptp_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) = +fun tptp_classrel_clause (ClassrelClause {axiom_name, subclass, superclass, + ...}) = tptp_cnf axiom_name "axiom" (tptp_classrelLits subclass superclass) end; diff -r 5ff37037fbec -r 7587b6e63454 src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Tue Jun 22 14:48:46 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Tue Jun 22 16:23:29 2010 +0200 @@ -7,15 +7,14 @@ signature SLEDGEHAMMER_HOL_CLAUSE = sig + type cnf_thm = Sledgehammer_Fact_Preprocessor.cnf_thm type name = Sledgehammer_FOL_Clause.name type name_pool = Sledgehammer_FOL_Clause.name_pool type kind = Sledgehammer_FOL_Clause.kind type fol_type = Sledgehammer_FOL_Clause.fol_type type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause type arity_clause = Sledgehammer_FOL_Clause.arity_clause - type axiom_name = string type polarity = bool - type hol_clause_id = int datatype combterm = CombConst of name * fol_type * fol_type list (* Const and Free *) | @@ -23,8 +22,8 @@ CombApp of combterm * combterm datatype literal = Literal of polarity * combterm datatype hol_clause = - HOLClause of {clause_id: hol_clause_id, axiom_name: axiom_name, th: thm, - kind: kind, literals: literal list, ctypes_sorts: typ list} + HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind, + literals: literal list, ctypes_sorts: typ list} val type_of_combterm : combterm -> fol_type val strip_combterm_comb : combterm -> combterm * combterm list @@ -33,13 +32,10 @@ int -> (string * term) list -> term -> (string * term) list * term exception TRIVIAL val make_conjecture_clauses : theory -> thm list -> hol_clause list - val make_axiom_clauses : - theory -> (thm * (axiom_name * hol_clause_id)) list - -> (axiom_name * hol_clause) list + val make_axiom_clauses : theory -> cnf_thm list -> (string * hol_clause) list val type_wrapper_name : string val get_helper_clauses : - theory -> bool -> bool -> hol_clause list - -> (thm * (axiom_name * hol_clause_id)) list -> hol_clause list + theory -> bool -> bool -> hol_clause list -> cnf_thm list -> hol_clause list val write_tptp_file : bool -> bool -> bool -> Path.T -> hol_clause list * hol_clause list * hol_clause list * hol_clause list * classrel_clause list * arity_clause list -> name_pool option * int @@ -65,9 +61,7 @@ (* data types for typed combinator expressions *) (******************************************************) -type axiom_name = string; -type polarity = bool; -type hol_clause_id = int; +type polarity = bool datatype combterm = CombConst of name * fol_type * fol_type list (* Const and Free *) | @@ -77,8 +71,8 @@ datatype literal = Literal of polarity * combterm; datatype hol_clause = - HOLClause of {clause_id: hol_clause_id, axiom_name: axiom_name, th: thm, - kind: kind, literals: literal list, ctypes_sorts: typ list}; + HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind, + literals: literal list, ctypes_sorts: typ list} (*********************************************************************) @@ -212,7 +206,7 @@ kind = kind, literals = lits, ctypes_sorts = ctypes_sorts}) end -fun add_axiom_clause thy (th, (name, id)) (skolem_somes, clss) = +fun add_axiom_clause thy (th, ((name, id), _ : thm)) (skolem_somes, clss) = let val (skolem_somes, cls) = make_clause thy (id, name, Axiom, th) skolem_somes in (skolem_somes, clss |> not (isTaut cls) ? cons (name, cls)) end @@ -364,7 +358,7 @@ fun count_clause (HOLClause {literals, ...}) = fold count_literal literals -val raw_cnf_rules_pairs = map (fn (name, thm) => (thm, (name, 0))) +val raw_cnf_rules_pairs = map (fn (name, thm) => (thm, ((name, 0), thm))) fun cnf_helper_thms thy raw = map (`Thm.get_name_hint) #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)