# HG changeset patch
# User blanchet
# Date 1277740956 -7200
# Node ID fa57a87f92a0c527fbb37bb8939f5bb632f62143
# Parent  f73cd4069f6973c0eaea2793786421bea7797f6e
get rid of Skolem cache by performing CNF-conversion after fact selection

diff -r f73cd4069f69 -r fa57a87f92a0 src/HOL/Tools/Sledgehammer/clausifier.ML
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Jun 28 17:32:28 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Jun 28 18:02:36 2010 +0200
@@ -9,23 +9,14 @@
 sig
   type cnf_thm = thm * ((string * int) * thm)
 
-  val trace: bool Unsynchronized.ref
-  val skolem_theory_name: string
-  val skolem_prefix: string
-  val skolem_infix: string
-  val is_skolem_const_name: string -> bool
-  val num_type_args: theory -> string -> int
   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 -> cnf_thm list
-  val saturate_cache: theory -> theory option
-  val auto_saturate_cache: bool Unsynchronized.ref
   val neg_clausify: thm -> thm list
   val neg_conjecture_clauses:
     Proof.context -> thm -> int -> thm list list * (string * typ) list
-  val setup: theory -> theory
 end;
 
 structure Clausifier : CLAUSIFIER =
@@ -33,13 +24,6 @@
 
 type cnf_thm = thm * ((string * int) * thm)
 
-val trace = Unsynchronized.ref false;
-fun trace_msg msg = if !trace then tracing (msg ()) else ();
-
-val skolem_theory_name = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
-val skolem_prefix = "sko_"
-val skolem_infix = "$"
-
 val type_has_topsort = Term.exists_subtype
   (fn TFree (_, []) => true
     | TVar (_, []) => true
@@ -68,30 +52,6 @@
 
 (**** SKOLEMIZATION BY INFERENCE (lcp) ****)
 
-(*Keep the full complexity of the original name*)
-fun flatten_name s = space_implode "_X" (Long_Name.explode s);
-
-fun skolem_name thm_name j var_name =
-  skolem_prefix ^ thm_name ^ "_" ^ Int.toString j ^
-  skolem_infix ^ (if var_name = "" then "g" else flatten_name var_name)
-
-(* Hack: Could return false positives (e.g., a user happens to declare a
-   constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
-val is_skolem_const_name =
-  Long_Name.base_name
-  #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
-
-(* The number of type arguments of a constant, zero if it's monomorphic. For
-   (instances of) Skolem pseudoconstants, this information is encoded in the
-   constant name. *)
-fun num_type_args thy s =
-  if String.isPrefix skolem_theory_name s then
-    s |> unprefix skolem_theory_name
-      |> space_explode skolem_infix |> hd
-      |> space_explode "_" |> List.last |> Int.fromString |> the
-  else
-    (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
-
 fun mk_skolem_id t =
   let val T = fastype_of t in
     Const (@{const_name skolem_id}, T --> T) $ t
@@ -352,24 +312,9 @@
     end
     handle THM _ => []
 
-(*The cache prevents repeated clausification of a theorem, and also repeated declaration of
-  Skolem functions.*)
-structure ThmCache = Theory_Data
-(
-  type T = thm list Thmtab.table * unit Symtab.table;
-  val empty = (Thmtab.empty, Symtab.empty);
-  val extend = I;
-  fun merge ((cache1, seen1), (cache2, seen2)) : T =
-    (Thmtab.merge (K true) (cache1, cache2), Symtab.merge (K true) (seen1, seen2));
-);
-
 (* Convert Isabelle theorems into axiom clauses. *)
-fun cnf_axiom thy th0 =
-  let val th = Thm.transfer thy th0 in
-    case Thmtab.lookup (#1 (ThmCache.get thy)) th of
-      SOME cls => cls
-    | NONE => skolemize_theorem thy th
-  end
+(* FIXME: is transfer necessary? *)
+fun cnf_axiom thy = skolemize_theorem thy o Thm.transfer thy
 
 
 (**** Translate a set of theorems into CNF ****)
@@ -389,44 +334,6 @@
   in do_all [] o rev end
 
 
-(**** Convert all facts of the theory into FOL or HOL clauses ****)
-
-fun saturate_cache thy =
-  let
-    val (cache, seen) = ThmCache.get thy
-    val facts = PureThy.facts_of thy
-    val new_facts = (facts, []) |-> Facts.fold_static (fn (name, ths) =>
-      if Facts.is_concealed facts name orelse Symtab.defined seen name then I
-      else cons (name, ths))
-    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 is_theorem_bad_for_atps th orelse Thmtab.defined cache th then
-            I
-          else
-            cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths)
-    val entries =
-      Par_List.map (fn (_, th) => (th, skolemize_theorem thy th))
-                   (sort_distinct (Thm.thm_ord o pairself snd) new_thms)
-  in
-    if null entries then
-      NONE
-    else
-      thy |> ThmCache.map (fn p => p |>> fold Thmtab.update entries
-                                     ||> fold Symtab.update
-                                              (map (rpair () o #1) new_facts))
-          |> SOME
-  end
-
-(* For emergency use where the Skolem cache causes problems. *)
-val auto_saturate_cache = Unsynchronized.ref true
-
-fun conditionally_saturate_cache thy =
-  if !auto_saturate_cache then saturate_cache thy else NONE
-
-
 (*** Converting a subgoal into negated conjecture clauses. ***)
 
 fun neg_skolemize_tac ctxt =
@@ -447,10 +354,4 @@
   in (map neg_clausify prems, map (dest_Free o term_of o #2) params) end
 
 
-(** setup **)
-
-val setup =
-  perhaps conditionally_saturate_cache
-  #> Theory.at_end conditionally_saturate_cache
-
 end;
diff -r f73cd4069f69 -r fa57a87f92a0 src/HOL/Tools/Sledgehammer/meson_tactic.ML
--- a/src/HOL/Tools/Sledgehammer/meson_tactic.ML	Mon Jun 28 17:32:28 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/meson_tactic.ML	Mon Jun 28 18:02:36 2010 +0200
@@ -16,7 +16,7 @@
 
 (*Expand all new definitions of abstraction or Skolem functions in a proof state.*)
 fun is_absko (Const (@{const_name "=="}, _) $ Free (a, _) $ _) =
-    String.isPrefix Clausifier.skolem_prefix a
+(*  FIXME  String.isPrefix Clausifier.skolem_prefix a *) true
   | is_absko _ = false;
 
 fun is_okdef xs (Const (@{const_name "=="}, _) $ t $ _) =   (*Definition of Free, not in certain terms*)
diff -r f73cd4069f69 -r fa57a87f92a0 src/HOL/Tools/Sledgehammer/metis_clauses.ML
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Mon Jun 28 17:32:28 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Mon Jun 28 18:02:36 2010 +0200
@@ -57,6 +57,11 @@
   val make_fixed_const : string -> string
   val make_fixed_type_const : string -> string
   val make_type_class : string -> string
+  val skolem_theory_name: string
+  val skolem_prefix: string
+  val skolem_infix: string
+  val is_skolem_const_name: string -> bool
+  val num_type_args: theory -> string -> int
   val empty_name_pool : bool -> name_pool option
   val pool_map : ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
   val nice_name : name -> name_pool option -> string * name_pool option
@@ -209,6 +214,29 @@
 
 fun make_type_class clas = class_prefix ^ ascii_of clas;
 
+val skolem_theory_name = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
+val skolem_prefix = "sko_"
+val skolem_infix = "$"
+
+(*Keep the full complexity of the original name*)
+fun flatten_name s = space_implode "_X" (Long_Name.explode s);
+
+(* Hack: Could return false positives (e.g., a user happens to declare a
+   constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
+val is_skolem_const_name =
+  Long_Name.base_name
+  #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
+
+(* The number of type arguments of a constant, zero if it's monomorphic. For
+   (instances of) Skolem pseudoconstants, this information is encoded in the
+   constant name. *)
+fun num_type_args thy s =
+  if String.isPrefix skolem_theory_name s then
+    s |> unprefix skolem_theory_name
+      |> space_explode skolem_infix |> hd
+      |> space_explode "_" |> List.last |> Int.fromString |> the
+  else
+    (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
 
 (**** name pool ****)