# HG changeset patch
# User immler@in.tum.de
# Date 1244041001 -7200
# Node ID d8537ba165b52d8e3866b916e23a74d1652c4b4a
# Parent  9f2ca03ae7b7425c27ae7586c085861c20c95c7e
split preparing clauses and writing problemfile;
included results of count_constants in return-type of prover;
optionally pass counted constants to prover;
removed unused external_prover from signature

diff -r 9f2ca03ae7b7 -r d8537ba165b5 src/HOL/Tools/atp_manager.ML
--- a/src/HOL/Tools/atp_manager.ML	Wed Jun 03 07:12:57 2009 -0700
+++ b/src/HOL/Tools/atp_manager.ML	Wed Jun 03 16:56:41 2009 +0200
@@ -19,8 +19,10 @@
   val kill: unit -> unit
   val info: unit -> unit
   val messages: int option -> unit
-  type prover = int -> (thm * (string * int)) list option -> string -> int ->
-    Proof.context * (thm list * thm) -> bool * string * string * string vector
+  type prover = int -> (thm * (string * int)) list option ->
+    (int Symtab.table * bool Symtab.table) option -> string -> int ->
+    Proof.context * (thm list * thm) ->
+    bool * string * string * string vector * (int Symtab.table * bool Symtab.table)
   val add_prover: string -> prover -> theory -> theory
   val print_provers: theory -> unit
   val get_prover: string -> theory -> prover option
@@ -289,8 +291,10 @@
 
 (* named provers *)
 
-type prover = int -> (thm * (string * int)) list option -> string -> int ->
-  Proof.context * (thm list * thm) -> bool * string * string * string vector
+type prover = int -> (thm * (string * int)) list option ->
+  (int Symtab.table * bool Symtab.table) option -> string -> int ->
+  Proof.context * (thm list * thm) ->
+  bool * string * string * string vector * (int Symtab.table * bool Symtab.table)
 
 fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
 
@@ -330,8 +334,8 @@
           let
             val _ = register birthtime deadtime (Thread.self (), desc)
             val result =
-              let val (success, message, _, _) =
-                prover (get_timeout ()) NONE name i (Proof.get_goal proof_state)
+              let val (success, message, _, _, _) =
+                prover (get_timeout ()) NONE NONE name i (Proof.get_goal proof_state)
               in (success, message) end
               handle ResHolClause.TOO_TRIVIAL
                 => (true, "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
diff -r 9f2ca03ae7b7 -r d8537ba165b5 src/HOL/Tools/atp_minimal.ML
--- a/src/HOL/Tools/atp_minimal.ML	Wed Jun 03 07:12:57 2009 -0700
+++ b/src/HOL/Tools/atp_minimal.ML	Wed Jun 03 16:56:41 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) =
+fun produce_answer (success, message, result_string, thm_name_vec, const_counts) =
   if success then
-    (Success (Vector.foldr op:: [] thm_name_vec), result_string)
+    (Success (Vector.foldr op:: [] thm_name_vec, const_counts), 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 name_thms_pairs =
+fun sh_test_thms prover prover_name time_limit subgoalno state counts name_thms_pairs =
   let
     val _ = println ("Testing " ^ (length_string name_thms_pairs) ^ " theorems... ")
     val name_thm_pairs =
@@ -108,7 +108,8 @@
     val _ = debug_fn (fn () => print_names name_thm_pairs)
     val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
     val (result, proof) =
-      produce_answer (prover time_limit (SOME axclauses) prover_name subgoalno (Proof.get_goal state))
+      produce_answer
+        (prover time_limit (SOME axclauses) counts prover_name subgoalno (Proof.get_goal state))
     val _ = println (string_of_result result)
     val _ = debug proof
   in
@@ -126,11 +127,11 @@
     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 thms = case test_thms_fun thms of (Success _, _) => true | _ => false
+    fun test_thms counts thms = case test_thms_fun counts thms of (Success _, _) => true | _ => false
   in
     (* try prove first to check result and get used theorems *)
-    (case test_thms_fun name_thms_pairs of
-      (Success used, _) =>
+    (case test_thms_fun NONE name_thms_pairs of
+      (Success (used, const_counts), _) =>
         let
           val ordered_used = order_unique used
           val to_use =
@@ -138,7 +139,7 @@
               filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
             else
               name_thms_pairs
-          val min_thms = minimal test_thms to_use
+          val min_thms = (minimal (test_thms (SOME const_counts)) 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)
diff -r 9f2ca03ae7b7 -r d8537ba165b5 src/HOL/Tools/atp_wrapper.ML
--- a/src/HOL/Tools/atp_wrapper.ML	Wed Jun 03 07:12:57 2009 -0700
+++ b/src/HOL/Tools/atp_wrapper.ML	Wed Jun 03 16:56:41 2009 +0200
@@ -8,12 +8,6 @@
 sig
   val destdir: string ref
   val problem_name: string ref
-  val external_prover:
-    (unit -> (thm * (string * int)) list) ->
-    (Path.T -> thm -> int -> (thm * (string * int)) list -> theory -> string vector) ->
-    Path.T * string -> (string -> string option) ->
-    (string -> string * string vector * Proof.context * thm * int -> string) ->
-    AtpManager.prover
   val tptp_prover_opts_full: int -> bool -> bool -> Path.T * string -> AtpManager.prover
   val tptp_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover
   val tptp_prover: Path.T * string -> AtpManager.prover
@@ -46,8 +40,8 @@
 
 (* basic template *)
 
-fun external_prover relevance_filter write_problem_file (cmd, args) find_failure produce_answer
-  timeout axiom_clauses name subgoalno goal =
+fun external_prover relevance_filter preparer writer (cmd, args) find_failure produce_answer
+  timeout axiom_clauses const_counts name subgoalno goal =
   let
     (* path to unique problem file *)
     val destdir' = ! destdir
@@ -66,8 +60,24 @@
     val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths
     val probfile = prob_pathname subgoalno
     val fname = File.platform_path probfile
-    val the_ax_clauses = case axiom_clauses of NONE => relevance_filter () | SOME axcls => axcls
-    val thm_names = write_problem_file probfile th subgoalno the_ax_clauses thy
+    val goal_cls = #1 (ResAxioms.neg_conjecture_clauses th subgoalno)
+      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_axiom_clauses =
+      case axiom_clauses of
+          NONE => relevance_filter goal goal_cls
+        | SOME axcls => axcls
+    val (thm_names, clauses) = preparer goal_cls 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 (relevance_filter goal goal_cls) thy)
+          )
+      | SOME ccs => ccs
+    val _ = writer fname the_const_counts clauses
     val cmdline =
       if File.exists cmd then "exec " ^ File.shell_path cmd ^ " " ^ args
       else error ("Bad executable: " ^ Path.implode cmd)
@@ -92,7 +102,7 @@
       if rc <> 0
       then Output.debug (fn () => "Sledgehammer exited with return code " ^ string_of_int rc ^ ":\n" ^ proof)
       else ()
-  in (success, message, proof, thm_names) end;
+  in (success, message, proof, thm_names, the_const_counts) end;
 
 
 
@@ -100,14 +110,15 @@
 
 (* generic TPTP-based provers *)
 
-fun tptp_prover_opts_full max_new theory_const full command timeout ax_clauses name n goal =
+fun tptp_prover_opts_full max_new theory_const full command timeout ax_clauses ccs name n goal =
   external_prover
-    (fn () => ResAtp.get_relevant max_new theory_const goal n)
-    (ResAtp.write_problem_file false)
-    command
-    ResReconstruct.find_failure
-    (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp)
-    timeout ax_clauses name n goal;
+  (ResAtp.get_relevant max_new theory_const)
+  (ResAtp.prepare_clauses false)
+  (ResHolClause.tptp_write_file)
+  command
+  ResReconstruct.find_failure
+  (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp)
+  timeout ax_clauses ccs name n goal;
 
 (*arbitrary ATP with TPTP input/output and problemfile as last argument*)
 fun tptp_prover_opts max_new theory_const =
@@ -164,14 +175,15 @@
 
 (* SPASS *)
 
-fun spass_opts max_new theory_const timeout ax_clauses name n goal = external_prover
-  (fn () => ResAtp.get_relevant max_new theory_const goal n)
-  (ResAtp.write_problem_file true)
+fun spass_opts max_new theory_const timeout ax_clauses ccs name n goal = external_prover
+  (ResAtp.get_relevant max_new theory_const)
+  (ResAtp.prepare_clauses true)
+  ResHolClause.dfg_write_file
   (Path.explode "$SPASS_HOME/SPASS",
     "-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 name n goal;
+  timeout ax_clauses ccs name n goal;
 
 val spass = spass_opts 40 true;
 
diff -r 9f2ca03ae7b7 -r d8537ba165b5 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Wed Jun 03 07:12:57 2009 -0700
+++ b/src/HOL/Tools/res_atp.ML	Wed Jun 03 16:56:41 2009 +0200
@@ -6,10 +6,12 @@
   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 : int -> bool -> Proof.context * (thm list * thm) -> int
-    -> (thm * (string * int)) list
-  val write_problem_file : bool -> Path.T -> thm -> int -> (thm * (string * int)) list -> theory
-    -> string vector
+  val get_relevant : int -> bool -> Proof.context * (thm list * 'a) -> thm list ->
+    (thm * (string * int)) list
+  val prepare_clauses : bool -> thm 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)
 end;
 
 structure ResAtp: RES_ATP =
@@ -516,12 +518,9 @@
     | Fol => true
     | Hol => false
 
-fun get_relevant max_new theory_const (ctxt, (chain_ths, th)) n =
+fun get_relevant max_new theory_const (ctxt, (chain_ths, th)) goal_cls =
   let
     val thy = ProofContext.theory_of ctxt
-    val goal_cls = #1 (ResAxioms.neg_conjecture_clauses th n)
-                   handle THM ("assume: variables", _, _) =>
-                     error "Sledgehammer: Goal contains type variables (TVars)"
     val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt chain_ths
     val included_cls = included_thms |> ResAxioms.cnf_rules_pairs thy |> make_unique
                                      |> restrict_to_logic thy (isFO thy goal_cls)
@@ -532,15 +531,9 @@
     white_cls @ relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
   end;
 
-(* Write out problem file *)
-fun write_problem_file dfg probfile goal n axcls thy =
-  let val writer = if dfg then ResHolClause.dfg_write_file else ResHolClause.tptp_write_file
-    val fname = File.platform_path probfile
-    val axcls = make_unique axcls
-    val goal_cls = #1 (ResAxioms.neg_conjecture_clauses goal n)
-                   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
+(* prepare and count clauses before writing *)
+fun prepare_clauses dfg goal_cls axcls thy =
+  let
     val ccls = subtract_cls goal_cls axcls
     val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls
     val ccltms = map prop_of ccls
@@ -549,13 +542,13 @@
     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 (supers',arity_clauses) = ResClause.make_arity_clauses_dfg dfg thy tycons supers
     val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
-    val clnames = writer thy (isFO thy goal_cls) ccls fname (axcls,classrel_clauses,arity_clauses) []
   in
-    Vector.fromList clnames
-  end;
+    (Vector.fromList clnames, (conjectures, axiom_clauses, helper_clauses, classrel_clauses, arity_clauses))
+  end
 
 end;
 
-
diff -r 9f2ca03ae7b7 -r d8537ba165b5 src/HOL/Tools/res_hol_clause.ML
--- a/src/HOL/Tools/res_hol_clause.ML	Wed Jun 03 07:12:57 2009 -0700
+++ b/src/HOL/Tools/res_hol_clause.ML	Wed Jun 03 16:56:41 2009 +0200
@@ -23,15 +23,19 @@
     | CombVar of string * ResClause.fol_type
     | CombApp of combterm * combterm
   datatype literal = Literal of polarity * combterm
+  datatype clause = Clause of {clause_id: clause_id, axiom_name: axiom_name, th: thm,
+                    kind: ResClause.kind,literals: literal list, ctypes_sorts: typ list}
   val strip_comb: combterm -> combterm * combterm list
   val literals_of_term: theory -> term -> literal list * typ list
   exception TOO_TRIVIAL
-  val tptp_write_file: theory -> bool -> thm list -> string ->
-    (thm * (axiom_name * clause_id)) list * ResClause.classrelClause list *
-      ResClause.arityClause list -> string list -> axiom_name list
-  val dfg_write_file: theory -> bool -> thm list -> string ->
-    (thm * (axiom_name * clause_id)) list * ResClause.classrelClause list *
-      ResClause.arityClause list -> string list -> axiom_name list
+  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 ->
+    clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit
+  val dfg_write_file: string -> int Symtab.table * bool Symtab.table ->
+    clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit
 end
 
 structure ResHolClause: RES_HOL_CLAUSE =
@@ -294,7 +298,7 @@
       (map (tptp_literal cma cnh) literals, 
        map (RC.tptp_of_typeLit pos) (RC.add_typs ctypes_sorts));
 
-fun clause2tptp cma cnh (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
+fun clause2tptp (cma, cnh) (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
   let val (lits,tylits) = tptp_type_lits cma cnh (kind = RC.Conjecture) cls
   in
       (RC.gen_tptp_cls(clause_id,axiom_name,kind,lits,tylits), tylits)
@@ -317,7 +321,7 @@
 
 fun dfg_vars (Clause {literals,...}) = RC.union_all (map get_uvars_l literals);
 
-fun clause2dfg cma cnh (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
+fun clause2dfg (cma, cnh) (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
   let val (lits,tylits) = dfg_type_lits cma cnh (kind = RC.Conjecture) cls
       val vars = dfg_vars cls
       val tvars = RC.get_tvar_strs ctypes_sorts
@@ -350,7 +354,7 @@
     List.foldl (add_literal_decls cma cnh) decls literals
     handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
 
-fun decls_of_clauses cma cnh clauses arity_clauses =
+fun decls_of_clauses (cma, cnh) clauses arity_clauses =
   let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) RC.init_functab)
       val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty
       val (functab,predtab) = (List.foldl (add_clause_decls cma cnh) (init_functab, init_predtab) clauses)
@@ -448,7 +452,7 @@
   Output.debug (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
                 (if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else ""));
 
-fun count_constants (conjectures, axclauses, helper_clauses) =
+fun count_constants (conjectures, axclauses, helper_clauses, _, _) =
   if minimize_applies then
      let val (const_min_arity, const_needs_hBOOL) =
           fold count_constants_clause conjectures (Symtab.empty, Symtab.empty)
@@ -460,64 +464,63 @@
 
 (* tptp format *)
 
+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
+
 (* write TPTP format to a single file *)
-fun tptp_write_file thy isFO thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas =
-    let val _ = Output.debug (fn () => ("Preparing to write the TPTP file " ^ filename))
-        val conjectures = make_conjecture_clauses false thy thms
-        val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses false thy ax_tuples)
-        val helper_clauses = get_helper_clauses false thy isFO (conjectures, axclauses, user_lemmas)
-        val (const_min_arity, const_needs_hBOOL) = count_constants (conjectures, axclauses, helper_clauses);
-        val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp const_min_arity const_needs_hBOOL) conjectures)
-        val tfree_clss = map RC.tptp_tfree_clause (List.foldl (op union_string) [] tfree_litss)
-        val out = TextIO.openOut filename
-    in
-        List.app (curry TextIO.output out o #1 o (clause2tptp const_min_arity const_needs_hBOOL)) axclauses;
-        RC.writeln_strs out tfree_clss;
-        RC.writeln_strs out tptp_clss;
-        List.app (curry TextIO.output out o RC.tptp_classrelClause) classrel_clauses;
-        List.app (curry TextIO.output out o RC.tptp_arity_clause) arity_clauses;
-        List.app (curry TextIO.output out o #1 o (clause2tptp const_min_arity const_needs_hBOOL)) helper_clauses;
-        TextIO.closeOut out;
-        clnames
-    end;
+fun tptp_write_file filename const_counts (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) =
+  let
+    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
+  in
+    List.app (curry TextIO.output out o #1 o (clause2tptp const_counts)) axclauses;
+    RC.writeln_strs out tfree_clss;
+    RC.writeln_strs out tptp_clss;
+    List.app (curry TextIO.output out o RC.tptp_classrelClause) classrel_clauses;
+    List.app (curry TextIO.output out o RC.tptp_arity_clause) arity_clauses;
+    List.app (curry TextIO.output out o #1 o (clause2tptp const_counts)) helper_clauses;
+    TextIO.closeOut out
+  end;
 
 
 (* dfg format *)
 
-fun dfg_write_file thy isFO thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas =
-    let val _ = Output.debug (fn () => ("Preparing to write the DFG file " ^ filename))
-        val conjectures = make_conjecture_clauses true thy thms
-        val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses true thy ax_tuples)
-        val helper_clauses = get_helper_clauses true thy isFO (conjectures, axclauses, user_lemmas)
-        val (const_min_arity, const_needs_hBOOL) = count_constants (conjectures, axclauses, helper_clauses);
-        val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg const_min_arity const_needs_hBOOL) conjectures)
-        and probname = Path.implode (Path.base (Path.explode filename))
-        val axstrs = map (#1 o (clause2dfg const_min_arity const_needs_hBOOL)) axclauses
-        val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss)
-        val out = TextIO.openOut filename
-        val helper_clauses_strs = map (#1 o (clause2dfg const_min_arity const_needs_hBOOL)) helper_clauses
-        val (funcs,cl_preds) = decls_of_clauses const_min_arity const_needs_hBOOL (helper_clauses @ conjectures @ axclauses) arity_clauses
-        and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
-    in
-        TextIO.output (out, RC.string_of_start probname);
-        TextIO.output (out, RC.string_of_descrip probname);
-        TextIO.output (out, RC.string_of_symbols
-                              (RC.string_of_funcs funcs)
-                              (RC.string_of_preds (cl_preds @ ty_preds)));
-        TextIO.output (out, "list_of_clauses(axioms,cnf).\n");
-        RC.writeln_strs out axstrs;
-        List.app (curry TextIO.output out o RC.dfg_classrelClause) classrel_clauses;
-        List.app (curry TextIO.output out o RC.dfg_arity_clause) arity_clauses;
-        RC.writeln_strs out helper_clauses_strs;
-        TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n");
-        RC.writeln_strs out tfree_clss;
-        RC.writeln_strs out dfg_clss;
-        TextIO.output (out, "end_of_list.\n\n");
-        (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
-        TextIO.output (out, "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n");
-        TextIO.output (out, "end_problem.\n");
-        TextIO.closeOut out;
-        clnames
-    end;
+fun dfg_write_file filename const_counts (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) =
+  let
+    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
+    val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss)
+    val out = TextIO.openOut filename
+    val helper_clauses_strs = map (#1 o (clause2dfg const_counts)) helper_clauses
+    val (funcs,cl_preds) = decls_of_clauses const_counts (helper_clauses @ conjectures @ axclauses) arity_clauses
+    and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
+  in
+    TextIO.output (out, RC.string_of_start probname);
+    TextIO.output (out, RC.string_of_descrip probname);
+    TextIO.output (out, RC.string_of_symbols
+                          (RC.string_of_funcs funcs)
+                          (RC.string_of_preds (cl_preds @ ty_preds)));
+    TextIO.output (out, "list_of_clauses(axioms,cnf).\n");
+    RC.writeln_strs out axstrs;
+    List.app (curry TextIO.output out o RC.dfg_classrelClause) classrel_clauses;
+    List.app (curry TextIO.output out o RC.dfg_arity_clause) arity_clauses;
+    RC.writeln_strs out helper_clauses_strs;
+    TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n");
+    RC.writeln_strs out tfree_clss;
+    RC.writeln_strs out dfg_clss;
+    TextIO.output (out, "end_of_list.\n\n");
+    (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
+    TextIO.output (out, "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n");
+    TextIO.output (out, "end_problem.\n");
+    TextIO.closeOut out
+  end;
 
 end