thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
authorblanchet
Tue Jun 22 16:23:29 2010 +0200 (2010-06-22 ago)
changeset 375007587b6e63454
parent 37499 5ff37037fbec
child 37501 b5440c78ed3f
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
src/HOL/Tools/ATP_Manager/atp_manager.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Jun 22 14:48:46 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Jun 22 16:23:29 2010 +0200
     1.3 @@ -8,7 +8,8 @@
     1.4  
     1.5  signature ATP_MANAGER =
     1.6  sig
     1.7 -  type name_pool = Sledgehammer_HOL_Clause.name_pool
     1.8 +  type name_pool = Sledgehammer_FOL_Clause.name_pool
     1.9 +  type cnf_thm = Sledgehammer_Fact_Preprocessor.cnf_thm
    1.10    type relevance_override = Sledgehammer_Fact_Filter.relevance_override
    1.11    type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
    1.12    type params =
    1.13 @@ -31,8 +32,8 @@
    1.14      {subgoal: int,
    1.15       goal: Proof.context * (thm list * thm),
    1.16       relevance_override: relevance_override,
    1.17 -     axiom_clauses: (thm * (string * int)) list option,
    1.18 -     filtered_clauses: (thm * (string * int)) list option}
    1.19 +     axiom_clauses: cnf_thm list option,
    1.20 +     filtered_clauses: cnf_thm list option}
    1.21    datatype failure =
    1.22      Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
    1.23      MalformedInput | MalformedOutput | UnknownError
    1.24 @@ -46,7 +47,7 @@
    1.25       proof: string,
    1.26       internal_thm_names: string Vector.vector,
    1.27       conjecture_shape: int list list,
    1.28 -     filtered_clauses: (thm * (string * int)) list}
    1.29 +     filtered_clauses: cnf_thm list}
    1.30    type prover =
    1.31      params -> minimize_command -> Time.time -> problem -> prover_result
    1.32  
    1.33 @@ -91,8 +92,8 @@
    1.34    {subgoal: int,
    1.35     goal: Proof.context * (thm list * thm),
    1.36     relevance_override: relevance_override,
    1.37 -   axiom_clauses: (thm * (string * int)) list option,
    1.38 -   filtered_clauses: (thm * (string * int)) list option};
    1.39 +   axiom_clauses: cnf_thm list option,
    1.40 +   filtered_clauses: cnf_thm list option}
    1.41  
    1.42  datatype failure =
    1.43    Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
    1.44 @@ -108,7 +109,7 @@
    1.45     proof: string,
    1.46     internal_thm_names: string Vector.vector,
    1.47     conjecture_shape: int list list,
    1.48 -   filtered_clauses: (thm * (string * int)) list};
    1.49 +   filtered_clauses: cnf_thm list}
    1.50  
    1.51  type prover =
    1.52    params -> minimize_command -> Time.time -> problem -> prover_result
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Jun 22 14:48:46 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Jun 22 16:23:29 2010 +0200
     2.3 @@ -5,11 +5,10 @@
     2.4  
     2.5  signature SLEDGEHAMMER_FACT_FILTER =
     2.6  sig
     2.7 +  type cnf_thm = Sledgehammer_Fact_Preprocessor.cnf_thm
     2.8    type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
     2.9    type arity_clause = Sledgehammer_FOL_Clause.arity_clause
    2.10 -  type axiom_name = Sledgehammer_HOL_Clause.axiom_name
    2.11    type hol_clause = Sledgehammer_HOL_Clause.hol_clause
    2.12 -  type hol_clause_id = Sledgehammer_HOL_Clause.hol_clause_id
    2.13  
    2.14    type relevance_override =
    2.15      {add: Facts.ref list,
    2.16 @@ -24,14 +23,12 @@
    2.17    val is_quasi_fol_term : theory -> term -> bool
    2.18    val relevant_facts :
    2.19      bool -> bool -> real -> real -> bool -> int -> bool -> relevance_override
    2.20 -    -> Proof.context * (thm list * 'a) -> thm list
    2.21 -    -> (thm * (string * int)) list
    2.22 +    -> Proof.context * (thm list * 'a) -> thm list -> cnf_thm list
    2.23    val prepare_clauses :
    2.24 -    bool -> thm list -> (thm * (axiom_name * hol_clause_id)) list
    2.25 -    -> (thm * (axiom_name * hol_clause_id)) list -> theory
    2.26 -    -> axiom_name vector
    2.27 -       * (hol_clause list * hol_clause list * hol_clause list *
    2.28 -          hol_clause list * classrel_clause list * arity_clause list)
    2.29 +    bool -> thm list -> cnf_thm list -> cnf_thm list -> theory
    2.30 +    -> string vector
    2.31 +       * (hol_clause list * hol_clause list * hol_clause list
    2.32 +          * hol_clause list * classrel_clause list * arity_clause list)
    2.33  end;
    2.34  
    2.35  structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
    2.36 @@ -234,13 +231,13 @@
    2.37          | _ => false
    2.38      end;
    2.39  
    2.40 -type annotd_cls = (thm * (string * int)) * ((string * const_typ list) list);
    2.41 +type annotated_clause = cnf_thm * ((string * const_typ list) list)
    2.42         
    2.43  (*For a reverse sort, putting the largest values first.*)
    2.44 -fun compare_pairs ((_,w1),(_,w2)) = Real.compare (w2,w1);
    2.45 +fun compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1)
    2.46  
    2.47  (*Limit the number of new clauses, to prevent runaway acceptance.*)
    2.48 -fun take_best max_new (newpairs : (annotd_cls*real) list) =
    2.49 +fun take_best max_new (newpairs : (annotated_clause * real) list) =
    2.50    let val nnew = length newpairs
    2.51    in
    2.52      if nnew <= max_new then (map #1 newpairs, [])
    2.53 @@ -252,7 +249,7 @@
    2.54                         ", exceeds the limit of " ^ Int.toString (max_new)));
    2.55          trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
    2.56          trace_msg (fn () => "Actually passed: " ^
    2.57 -          space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted));
    2.58 +          space_implode ", " (map (fn (((_,((name,_), _)),_),_) => name) accepted));
    2.59  
    2.60          (map #1 accepted, map #1 (List.drop (cls, max_new)))
    2.61        end
    2.62 @@ -286,7 +283,8 @@
    2.63                    (more_rejects @ rejects)
    2.64              end
    2.65            | relevant (newrels, rejects)
    2.66 -                     ((ax as (clsthm as (thm, (name, n)), consts_typs)) :: axs) =
    2.67 +                     ((ax as (clsthm as (thm, ((name, n), _)), consts_typs)) ::
    2.68 +                      axs) =
    2.69              let
    2.70                val weight = if member Thm.eq_thm add_thms thm then 1.0
    2.71                             else if member Thm.eq_thm del_thms thm then 0.0
    2.72 @@ -309,7 +307,7 @@
    2.73          
    2.74  fun relevance_filter ctxt relevance_threshold relevance_convergence
    2.75                       defs_relevant max_new theory_relevant relevance_override
    2.76 -                     thy axioms goals = 
    2.77 +                     thy (axioms : cnf_thm list) goals = 
    2.78    if relevance_threshold > 0.0 then
    2.79      let
    2.80        val const_tab = List.foldl (count_axiom_consts theory_relevant thy)
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Tue Jun 22 14:48:46 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Tue Jun 22 16:23:29 2010 +0200
     3.3 @@ -7,6 +7,7 @@
     3.4  
     3.5  signature SLEDGEHAMMER_FACT_PREPROCESSOR =
     3.6  sig
     3.7 +  type cnf_thm = thm * ((string * int) * thm)
     3.8    val chained_prefix: string
     3.9    val trace: bool Unsynchronized.ref
    3.10    val trace_msg: (unit -> string) -> unit
    3.11 @@ -18,8 +19,7 @@
    3.12    val multi_base_blacklist: string list
    3.13    val is_theorem_bad_for_atps: thm -> bool
    3.14    val type_has_topsort: typ -> bool
    3.15 -  val cnf_rules_pairs:
    3.16 -    theory -> (string * thm) list -> (thm * (string * int)) list
    3.17 +  val cnf_rules_pairs : theory -> (string * thm) list -> cnf_thm list
    3.18    val saturate_skolem_cache: theory -> theory option
    3.19    val auto_saturate_skolem_cache: bool Unsynchronized.ref
    3.20      (* for emergency use where the Skolem cache causes problems *)
    3.21 @@ -35,6 +35,8 @@
    3.22  
    3.23  open Sledgehammer_FOL_Clause
    3.24  
    3.25 +type cnf_thm = thm * ((string * int) * thm)
    3.26 +
    3.27  (* Used to label theorems chained into the goal. *)
    3.28  val chained_prefix = "Sledgehammer.chained_"
    3.29  
    3.30 @@ -153,10 +155,11 @@
    3.31            val cT = Ts ---> T (* FIXME: use "skolem_type_and_args" *)
    3.32            val id = skolem_name s (Unsynchronized.inc skolem_count) s'
    3.33            val c = Free (id, cT)
    3.34 -          val rhs = list_abs_free (map dest_Free args,
    3.35 -                                   HOLogic.choice_const T $ body)
    3.36 -                    |> inline ? mk_skolem_id
    3.37 -                (*Forms a lambda-abstraction over the formal parameters*)
    3.38 +          (* Forms a lambda-abstraction over the formal parameters *)
    3.39 +          val rhs =
    3.40 +            list_abs_free (map dest_Free args,
    3.41 +                           HOLogic.choice_const T $ body)
    3.42 +            |> inline ? mk_skolem_id
    3.43            val def = Logic.mk_equals (c, rhs)
    3.44            val comb = list_comb (if inline then rhs else c, args)
    3.45          in dec_sko (subst_bound (comb, p)) (def :: defs) end
    3.46 @@ -446,20 +449,20 @@
    3.47  
    3.48  (**** Translate a set of theorems into CNF ****)
    3.49  
    3.50 -fun pair_name_cls _ (_, []) = []
    3.51 -  | pair_name_cls k (n, cls::clss) = (cls, (n,k)) :: pair_name_cls (k+1) (n, clss)
    3.52 -
    3.53  (*The combination of rev and tail recursion preserves the original order*)
    3.54  fun cnf_rules_pairs thy =
    3.55    let
    3.56 -    fun aux pairs [] = pairs
    3.57 -      | aux pairs ((name, th) :: ths) =
    3.58 +    fun do_one _ [] = []
    3.59 +      | do_one ((name, k), th) (cls :: clss) =
    3.60 +        (cls, ((name, k), th)) :: do_one ((name, k + 1), th) clss
    3.61 +    fun do_all pairs [] = pairs
    3.62 +      | do_all pairs ((name, th) :: ths) =
    3.63          let
    3.64 -          val new_pairs = pair_name_cls 0 (name, cnf_axiom thy th)
    3.65 +          val new_pairs = do_one ((name, 0), th) (cnf_axiom thy th)
    3.66                            handle THM _ => [] |
    3.67                                   CLAUSE _ => []
    3.68 -        in aux (new_pairs @ pairs) ths end
    3.69 -  in aux [] o rev end
    3.70 +        in do_all (new_pairs @ pairs) ths end
    3.71 +  in do_all [] o rev end
    3.72  
    3.73  
    3.74  (**** Convert all facts of the theory into FOL or HOL clauses ****)
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Tue Jun 22 14:48:46 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Tue Jun 22 16:23:29 2010 +0200
     4.3 @@ -37,7 +37,6 @@
     4.4    val pool_map : ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
     4.5    val nice_name : name -> name_pool option -> string * name_pool option
     4.6    datatype kind = Axiom | Conjecture
     4.7 -  type axiom_name = string
     4.8    datatype fol_type =
     4.9      TyVar of name |
    4.10      TyFree of name |
    4.11 @@ -53,9 +52,9 @@
    4.12        TConsLit of class * string * string list
    4.13      | TVarLit of class * string
    4.14    datatype arity_clause = ArityClause of
    4.15 -   {axiom_name: axiom_name, conclLit: arLit, premLits: arLit list}
    4.16 +   {axiom_name: string, conclLit: arLit, premLits: arLit list}
    4.17    datatype classrel_clause = ClassrelClause of
    4.18 -   {axiom_name: axiom_name, subclass: class, superclass: class}
    4.19 +   {axiom_name: string, subclass: class, superclass: class}
    4.20    val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list
    4.21    val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
    4.22    val tptp_sign: bool -> string -> string
    4.23 @@ -259,8 +258,6 @@
    4.24  
    4.25  datatype kind = Axiom | Conjecture;
    4.26  
    4.27 -type axiom_name = string;
    4.28 -
    4.29  (**** Isabelle FOL clauses ****)
    4.30  
    4.31  datatype fol_type =
    4.32 @@ -308,9 +305,7 @@
    4.33                 | TVarLit of class * string;
    4.34  
    4.35  datatype arity_clause =
    4.36 -         ArityClause of {axiom_name: axiom_name,
    4.37 -                         conclLit: arLit,
    4.38 -                         premLits: arLit list};
    4.39 +  ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list}
    4.40  
    4.41  
    4.42  fun gen_TVars 0 = []
    4.43 @@ -334,9 +329,7 @@
    4.44  (**** Isabelle class relations ****)
    4.45  
    4.46  datatype classrel_clause =
    4.47 -         ClassrelClause of {axiom_name: axiom_name,
    4.48 -                            subclass: class,
    4.49 -                            superclass: class};
    4.50 +  ClassrelClause of {axiom_name: string, subclass: class, superclass: class}
    4.51  
    4.52  (*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
    4.53  fun class_pairs _ [] _ = []
    4.54 @@ -437,7 +430,8 @@
    4.55    let val tvar = "(T)"
    4.56    in  tptp_clause [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)]  end;
    4.57  
    4.58 -fun tptp_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) =
    4.59 +fun tptp_classrel_clause (ClassrelClause {axiom_name, subclass, superclass,
    4.60 +                                          ...}) =
    4.61    tptp_cnf axiom_name "axiom" (tptp_classrelLits subclass superclass)
    4.62  
    4.63  end;
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Jun 22 14:48:46 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Jun 22 16:23:29 2010 +0200
     5.3 @@ -7,15 +7,14 @@
     5.4  
     5.5  signature SLEDGEHAMMER_HOL_CLAUSE =
     5.6  sig
     5.7 +  type cnf_thm = Sledgehammer_Fact_Preprocessor.cnf_thm
     5.8    type name = Sledgehammer_FOL_Clause.name
     5.9    type name_pool = Sledgehammer_FOL_Clause.name_pool
    5.10    type kind = Sledgehammer_FOL_Clause.kind
    5.11    type fol_type = Sledgehammer_FOL_Clause.fol_type
    5.12    type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
    5.13    type arity_clause = Sledgehammer_FOL_Clause.arity_clause
    5.14 -  type axiom_name = string
    5.15    type polarity = bool
    5.16 -  type hol_clause_id = int
    5.17  
    5.18    datatype combterm =
    5.19      CombConst of name * fol_type * fol_type list (* Const and Free *) |
    5.20 @@ -23,8 +22,8 @@
    5.21      CombApp of combterm * combterm
    5.22    datatype literal = Literal of polarity * combterm
    5.23    datatype hol_clause =
    5.24 -    HOLClause of {clause_id: hol_clause_id, axiom_name: axiom_name, th: thm,
    5.25 -                  kind: kind, literals: literal list, ctypes_sorts: typ list}
    5.26 +    HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
    5.27 +                  literals: literal list, ctypes_sorts: typ list}
    5.28  
    5.29    val type_of_combterm : combterm -> fol_type
    5.30    val strip_combterm_comb : combterm -> combterm * combterm list
    5.31 @@ -33,13 +32,10 @@
    5.32      int -> (string * term) list -> term -> (string * term) list * term
    5.33    exception TRIVIAL
    5.34    val make_conjecture_clauses : theory -> thm list -> hol_clause list
    5.35 -  val make_axiom_clauses :
    5.36 -    theory -> (thm * (axiom_name * hol_clause_id)) list
    5.37 -    -> (axiom_name * hol_clause) list
    5.38 +  val make_axiom_clauses : theory -> cnf_thm list -> (string * hol_clause) list
    5.39    val type_wrapper_name : string
    5.40    val get_helper_clauses :
    5.41 -    theory -> bool -> bool -> hol_clause list
    5.42 -    -> (thm * (axiom_name * hol_clause_id)) list -> hol_clause list
    5.43 +    theory -> bool -> bool -> hol_clause list -> cnf_thm list -> hol_clause list
    5.44    val write_tptp_file : bool -> bool -> bool -> Path.T ->
    5.45      hol_clause list * hol_clause list * hol_clause list * hol_clause list *
    5.46      classrel_clause list * arity_clause list -> name_pool option * int
    5.47 @@ -65,9 +61,7 @@
    5.48  (* data types for typed combinator expressions        *)
    5.49  (******************************************************)
    5.50  
    5.51 -type axiom_name = string;
    5.52 -type polarity = bool;
    5.53 -type hol_clause_id = int;
    5.54 +type polarity = bool
    5.55  
    5.56  datatype combterm =
    5.57    CombConst of name * fol_type * fol_type list (* Const and Free *) |
    5.58 @@ -77,8 +71,8 @@
    5.59  datatype literal = Literal of polarity * combterm;
    5.60  
    5.61  datatype hol_clause =
    5.62 -  HOLClause of {clause_id: hol_clause_id, axiom_name: axiom_name, th: thm,
    5.63 -                kind: kind, literals: literal list, ctypes_sorts: typ list};
    5.64 +  HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
    5.65 +                literals: literal list, ctypes_sorts: typ list}
    5.66  
    5.67  
    5.68  (*********************************************************************)
    5.69 @@ -212,7 +206,7 @@
    5.70                    kind = kind, literals = lits, ctypes_sorts = ctypes_sorts})
    5.71    end
    5.72  
    5.73 -fun add_axiom_clause thy (th, (name, id)) (skolem_somes, clss) =
    5.74 +fun add_axiom_clause thy (th, ((name, id), _ : thm)) (skolem_somes, clss) =
    5.75    let
    5.76      val (skolem_somes, cls) = make_clause thy (id, name, Axiom, th) skolem_somes
    5.77    in (skolem_somes, clss |> not (isTaut cls) ? cons (name, cls)) end
    5.78 @@ -364,7 +358,7 @@
    5.79  
    5.80  fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
    5.81  
    5.82 -val raw_cnf_rules_pairs = map (fn (name, thm) => (thm, (name, 0)))
    5.83 +val raw_cnf_rules_pairs = map (fn (name, thm) => (thm, ((name, 0), thm)))
    5.84  fun cnf_helper_thms thy raw =
    5.85    map (`Thm.get_name_hint)
    5.86    #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)