use results of relevance-filter to determine additional clauses;
(needed for minimize to be able to prove the same problems as sledgehammer)

--- a/src/HOL/Tools/atp_manager.ML	Mon Jun 22 17:07:08 2009 +0200
+++ b/src/HOL/Tools/atp_manager.ML	Mon Jun 22 17:07:09 2009 +0200
@@ -20,9 +20,9 @@
   val info: unit -> unit
   val messages: int option -> unit
   type prover = int -> (thm * (string * int)) list option ->
-    (int Symtab.table * bool Symtab.table) option -> string -> int ->
+    (thm * (string * int)) list option -> string -> int ->
     Proof.context * (thm list * thm) ->
-    bool * string * string * string vector * (int Symtab.table * bool Symtab.table)
+    bool * string * string * string vector * (thm * (string * int)) list
   val add_prover: string -> prover -> theory -> theory
   val print_provers: theory -> unit
   val get_prover: string -> theory -> prover option
@@ -292,9 +292,9 @@
 (* named provers *)
 
 type prover = int -> (thm * (string * int)) list option ->
-  (int Symtab.table * bool Symtab.table) option -> string -> int ->
+  (thm * (string * int)) list option -> string -> int ->
   Proof.context * (thm list * thm) ->
-  bool * string * string * string vector * (int Symtab.table * bool Symtab.table)
+  bool * string * string * string vector * (thm * (string * int)) list
 
 fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
 

--- a/src/HOL/Tools/atp_minimal.ML	Mon Jun 22 17:07:08 2009 +0200
+++ b/src/HOL/Tools/atp_minimal.ML	Mon Jun 22 17:07:09 2009 +0200
@@ -83,9 +83,9 @@
    ("# Cannot determine problem status within resource limit", Timeout),
    ("Error", Error)]
 
-fun produce_answer (success, message, result_string, thm_name_vec, const_counts) =
+fun produce_answer (success, message, result_string, thm_name_vec, filtered) =
   if success then
-    (Success (Vector.foldr op:: [] thm_name_vec, const_counts), result_string)
+    (Success (Vector.foldr op:: [] thm_name_vec, filtered), result_string)
   else
     let
       val failure = failure_strings |> get_first (fn (s, t) =>
@@ -100,7 +100,7 @@
 
 (* wrapper for calling external prover *)
 
-fun sh_test_thms prover prover_name time_limit subgoalno state counts name_thms_pairs =
+fun sh_test_thms prover prover_name time_limit subgoalno state filtered name_thms_pairs =
   let
     val _ = println ("Testing " ^ (length_string name_thms_pairs) ^ " theorems... ")
     val name_thm_pairs =
@@ -109,7 +109,7 @@
     val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
     val (result, proof) =
       produce_answer
-        (prover time_limit (SOME axclauses) counts prover_name subgoalno (Proof.get_goal state))
+        (prover time_limit (SOME axclauses) filtered prover_name subgoalno (Proof.get_goal state))
     val _ = println (string_of_result result)
     val _ = debug proof
   in
@@ -127,11 +127,12 @@
     val _ = debug_fn (fn () => app (fn (n, tl) =>
         (debug n; app (fn t => debug ("  " ^ Display.string_of_thm t)) tl)) name_thms_pairs)
     val test_thms_fun = sh_test_thms prover prover_name time_limit 1 state
-    fun test_thms counts thms = case test_thms_fun counts thms of (Success _, _) => true | _ => false
+    fun test_thms filtered thms =
+      case test_thms_fun filtered thms of (Success _, _) => true | _ => false
   in
     (* try prove first to check result and get used theorems *)
     (case test_thms_fun NONE name_thms_pairs of
-      (Success (used, const_counts), _) =>
+      (Success (used, filtered), _) =>
         let
           val ordered_used = order_unique used
           val to_use =
@@ -139,7 +140,7 @@
               filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
             else
               name_thms_pairs
-          val min_thms = (minimal (test_thms (SOME const_counts)) to_use)
+          val min_thms = (minimal (test_thms (SOME filtered)) to_use)
           val min_names = order_unique (map fst min_thms)
           val _ = println ("Minimal " ^ (length_string min_thms) ^ " theorems")
           val _ = debug_fn (fn () => print_names min_thms)

--- a/src/HOL/Tools/atp_wrapper.ML	Mon Jun 22 17:07:08 2009 +0200
+++ b/src/HOL/Tools/atp_wrapper.ML	Mon Jun 22 17:07:09 2009 +0200
@@ -41,7 +41,7 @@
 (* basic template *)
 
 fun external_prover relevance_filter preparer writer (cmd, args) find_failure produce_answer
-  timeout axiom_clauses const_counts name subgoalno goal =
+  timeout axiom_clauses filtered_clauses name subgoalno goal =
   let
     (* path to unique problem file *)
     val destdir' = ! destdir
@@ -62,24 +62,20 @@
       handle THM ("assume: variables", _, _) =>
         error "Sledgehammer: Goal contains type variables (TVars)"
     val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) goal_cls
+    val the_filtered_clauses =
+      case filtered_clauses of
+          NONE => relevance_filter goal goal_cls
+        | SOME fcls => fcls
     val the_axiom_clauses =
       case axiom_clauses of
-          NONE => relevance_filter goal goal_cls
+          NONE => the_filtered_clauses
         | SOME axcls => axcls
-    val (thm_names, clauses) = preparer goal_cls chain_ths the_axiom_clauses thy
-    val the_const_counts = case const_counts of
-      NONE =>
-        ResHolClause.count_constants(
-          case axiom_clauses of
-            NONE => clauses
-            | SOME axcls => #2(preparer goal_cls chain_ths (relevance_filter goal goal_cls) thy)
-          )
-      | SOME ccs => ccs
+    val (thm_names, clauses) = preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy
 
     (* write out problem file and call prover *)
     val probfile = prob_pathname subgoalno
     val fname = File.platform_path probfile
-    val _ = writer fname the_const_counts clauses
+    val _ = writer fname clauses
     val cmdline =
       if File.exists cmd then "exec " ^ File.shell_path cmd ^ " " ^ args
       else error ("Bad executable: " ^ Path.implode cmd)
@@ -101,7 +97,7 @@
       else if rc <> 0 then "External prover failed: " ^ proof
       else "Try this command: " ^ produce_answer name (proof, thm_names, ctxt, th, subgoalno)
     val _ = Output.debug (fn () => "Sledgehammer response (rc = " ^ string_of_int rc ^ "):\n" ^ proof)
-  in (success, message, proof, thm_names, the_const_counts) end;
+  in (success, message, proof, thm_names, the_filtered_clauses) end;
 
 
 
@@ -109,7 +105,7 @@
 
 (* generic TPTP-based provers *)
 
-fun tptp_prover_opts_full max_new theory_const full command timeout ax_clauses ccs name n goal =
+fun tptp_prover_opts_full max_new theory_const full command timeout ax_clauses fcls name n goal =
   external_prover
   (ResAtp.get_relevant max_new theory_const)
   (ResAtp.prepare_clauses false)
@@ -117,7 +113,7 @@
   command
   ResReconstruct.find_failure
   (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp)
-  timeout ax_clauses ccs name n goal;
+  timeout ax_clauses fcls name n goal;
 
 (*arbitrary ATP with TPTP input/output and problemfile as last argument*)
 fun tptp_prover_opts max_new theory_const =
@@ -174,7 +170,7 @@
 
 (* SPASS *)
 
-fun spass_opts max_new theory_const timeout ax_clauses ccs name n goal = external_prover
+fun spass_opts max_new theory_const timeout ax_clauses fcls name n goal = external_prover
   (ResAtp.get_relevant max_new theory_const)
   (ResAtp.prepare_clauses true)
   ResHolClause.dfg_write_file
@@ -182,7 +178,7 @@
     "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout)
   ResReconstruct.find_failure
   ResReconstruct.lemma_list_dfg
-  timeout ax_clauses ccs name n goal;
+  timeout ax_clauses fcls name n goal;
 
 val spass = spass_opts 40 true;
 

--- a/src/HOL/Tools/res_atp.ML	Mon Jun 22 17:07:08 2009 +0200
+++ b/src/HOL/Tools/res_atp.ML	Mon Jun 22 17:07:09 2009 +0200
@@ -9,6 +9,7 @@
   val get_relevant : int -> bool -> Proof.context * (thm list * 'a) -> thm list ->
     (thm * (string * int)) list
   val prepare_clauses : bool -> thm list -> thm list ->
+    (thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list ->
     (thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list -> theory ->
     ResHolClause.axiom_name vector * (ResHolClause.clause list * ResHolClause.clause list *
     ResHolClause.clause list * ResClause.classrelClause list * ResClause.arityClause list)
@@ -526,26 +527,30 @@
     relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
   end;
 
-(* prepare for passing to writer *)
-fun prepare_clauses dfg goal_cls chain_ths axcls thy =
+(* prepare for passing to writer,
+   create additional clauses based on the information from extra_cls *)
+fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy =
   let
-    val white_thms = filter check_named (map ResAxioms.pairname (if null chain_ths then whitelist else chain_ths))
+    val white_thms =
+      filter check_named (map ResAxioms.pairname (if null chain_ths then whitelist else chain_ths))
     val white_cls = ResAxioms.cnf_rules_pairs thy white_thms
-    val axcls = white_cls @ axcls
-    val ccls = subtract_cls goal_cls axcls
+    val extra_cls = white_cls @ extra_cls
+    val ccls = subtract_cls goal_cls extra_cls
     val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls
     val ccltms = map prop_of ccls
-    and axtms = map (prop_of o #1) axcls
+    and axtms = map (prop_of o #1) extra_cls
     val subs = tfree_classes_of_terms ccltms
     and supers = tvar_classes_of_terms axtms
     and tycons = type_consts_of_terms thy (ccltms@axtms)
     (*TFrees in conjecture clauses; TVars in axiom clauses*)
-    val (clnames, (conjectures, axiom_clauses, helper_clauses)) =
-      ResHolClause.prepare_clauses dfg thy (isFO thy goal_cls) ccls axcls []
+    val conjectures = ResHolClause.make_conjecture_clauses dfg thy ccls
+    val (clnames,axiom_clauses) = ListPair.unzip (ResHolClause.make_axiom_clauses dfg thy axcls)
+    val helper_clauses = ResHolClause.get_helper_clauses dfg thy (isFO thy goal_cls) (conjectures, extra_cls, [])
     val (supers',arity_clauses) = ResClause.make_arity_clauses_dfg dfg thy tycons supers
     val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
   in
-    (Vector.fromList clnames, (conjectures, axiom_clauses, helper_clauses, classrel_clauses, arity_clauses))
+    (Vector.fromList clnames,
+      (conjectures, axiom_clauses, helper_clauses, classrel_clauses, arity_clauses))
   end
 
 end;

--- a/src/HOL/Tools/res_hol_clause.ML	Mon Jun 22 17:07:08 2009 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML	Mon Jun 22 17:07:09 2009 +0200
@@ -28,13 +28,18 @@
   val strip_comb: combterm -> combterm * combterm list
   val literals_of_term: theory -> term -> literal list * typ list
   exception TOO_TRIVIAL
-  val count_constants: clause list * clause list * clause list * 'a * 'b ->
-    int Symtab.table * bool Symtab.table
-  val prepare_clauses: bool -> theory -> bool -> thm list -> (thm * (axiom_name * clause_id)) list ->
-    string list -> axiom_name list * (clause list * clause list * clause list)
-  val tptp_write_file: string -> int Symtab.table * bool Symtab.table ->
+  val make_conjecture_clauses:  bool -> theory -> thm list -> clause list (* dfg thy ccls *)
+  val make_axiom_clauses: bool ->
+       theory ->
+       (thm * (axiom_name * clause_id)) list -> (axiom_name * clause) list (* dfg thy axcls *)
+  val get_helper_clauses: bool ->
+       theory ->
+       bool ->
+       clause list * (thm * (axiom_name * clause_id)) list * string list ->
+       clause list
+  val tptp_write_file: string ->
     clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit
-  val dfg_write_file: string -> int Symtab.table * bool Symtab.table ->
+  val dfg_write_file: string -> 
     clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit
 end
 
@@ -403,10 +408,12 @@
 fun cnf_helper_thms thy =
   ResAxioms.cnf_rules_pairs thy o map ResAxioms.pairname
 
-fun get_helper_clauses dfg thy isFO (conjectures, axclauses, user_lemmas) =
+fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) =
   if isFO then []  (*first-order*)
   else
-    let val ct0 = List.foldl count_clause init_counters conjectures
+    let
+        val axclauses = map #2 (make_axiom_clauses dfg thy axcls)
+        val ct0 = List.foldl count_clause init_counters conjectures
         val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses
         fun needed c = valOf (Symtab.lookup ct c) > 0
         val IK = if needed "c_COMBI" orelse needed "c_COMBK"
@@ -462,20 +469,12 @@
      in (const_min_arity, const_needs_hBOOL) end
   else (Symtab.empty, Symtab.empty);
 
-
-fun prepare_clauses dfg thy isFO thms ax_tuples user_lemmas =
-  let
-    val conjectures = make_conjecture_clauses dfg thy thms
-    val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses dfg thy ax_tuples)
-    val helper_clauses = get_helper_clauses dfg thy isFO (conjectures, axclauses, user_lemmas)
-  in
-    (clnames, (conjectures, axclauses, helper_clauses))
-  end
-
 (* tptp format *)
 
-fun tptp_write_file filename const_counts (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) =
+fun tptp_write_file filename clauses =
   let
+    val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses
+    val const_counts = count_constants clauses
     val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp const_counts) conjectures)
     val tfree_clss = map RC.tptp_tfree_clause (List.foldl (op union_string) [] tfree_litss)
     val out = TextIO.openOut filename
@@ -492,8 +491,10 @@
 
 (* dfg format *)
 
-fun dfg_write_file filename const_counts (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) =
+fun dfg_write_file filename clauses =
   let
+    val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses
+    val const_counts = count_constants clauses
     val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg const_counts) conjectures)
     and probname = Path.implode (Path.base (Path.explode filename))
     val axstrs = map (#1 o (clause2dfg const_counts)) axclauses