split preparing clauses and writing problemfile;
authorimmler@in.tum.de
Wed Jun 03 16:56:41 2009 +0200 (2009-06-03)
changeset 31409d8537ba165b5
parent 31408 9f2ca03ae7b7
child 31410 c231efe693ce
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
src/HOL/Tools/atp_manager.ML
src/HOL/Tools/atp_minimal.ML
src/HOL/Tools/atp_wrapper.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_hol_clause.ML
     1.1 --- a/src/HOL/Tools/atp_manager.ML	Wed Jun 03 07:12:57 2009 -0700
     1.2 +++ b/src/HOL/Tools/atp_manager.ML	Wed Jun 03 16:56:41 2009 +0200
     1.3 @@ -19,8 +19,10 @@
     1.4    val kill: unit -> unit
     1.5    val info: unit -> unit
     1.6    val messages: int option -> unit
     1.7 -  type prover = int -> (thm * (string * int)) list option -> string -> int ->
     1.8 -    Proof.context * (thm list * thm) -> bool * string * string * string vector
     1.9 +  type prover = int -> (thm * (string * int)) list option ->
    1.10 +    (int Symtab.table * bool Symtab.table) option -> string -> int ->
    1.11 +    Proof.context * (thm list * thm) ->
    1.12 +    bool * string * string * string vector * (int Symtab.table * bool Symtab.table)
    1.13    val add_prover: string -> prover -> theory -> theory
    1.14    val print_provers: theory -> unit
    1.15    val get_prover: string -> theory -> prover option
    1.16 @@ -289,8 +291,10 @@
    1.17  
    1.18  (* named provers *)
    1.19  
    1.20 -type prover = int -> (thm * (string * int)) list option -> string -> int ->
    1.21 -  Proof.context * (thm list * thm) -> bool * string * string * string vector
    1.22 +type prover = int -> (thm * (string * int)) list option ->
    1.23 +  (int Symtab.table * bool Symtab.table) option -> string -> int ->
    1.24 +  Proof.context * (thm list * thm) ->
    1.25 +  bool * string * string * string vector * (int Symtab.table * bool Symtab.table)
    1.26  
    1.27  fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
    1.28  
    1.29 @@ -330,8 +334,8 @@
    1.30            let
    1.31              val _ = register birthtime deadtime (Thread.self (), desc)
    1.32              val result =
    1.33 -              let val (success, message, _, _) =
    1.34 -                prover (get_timeout ()) NONE name i (Proof.get_goal proof_state)
    1.35 +              let val (success, message, _, _, _) =
    1.36 +                prover (get_timeout ()) NONE NONE name i (Proof.get_goal proof_state)
    1.37                in (success, message) end
    1.38                handle ResHolClause.TOO_TRIVIAL
    1.39                  => (true, "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
     2.1 --- a/src/HOL/Tools/atp_minimal.ML	Wed Jun 03 07:12:57 2009 -0700
     2.2 +++ b/src/HOL/Tools/atp_minimal.ML	Wed Jun 03 16:56:41 2009 +0200
     2.3 @@ -83,9 +83,9 @@
     2.4     ("# Cannot determine problem status within resource limit", Timeout),
     2.5     ("Error", Error)]
     2.6  
     2.7 -fun produce_answer (success, message, result_string, thm_name_vec) =
     2.8 +fun produce_answer (success, message, result_string, thm_name_vec, const_counts) =
     2.9    if success then
    2.10 -    (Success (Vector.foldr op:: [] thm_name_vec), result_string)
    2.11 +    (Success (Vector.foldr op:: [] thm_name_vec, const_counts), result_string)
    2.12    else
    2.13      let
    2.14        val failure = failure_strings |> get_first (fn (s, t) =>
    2.15 @@ -100,7 +100,7 @@
    2.16  
    2.17  (* wrapper for calling external prover *)
    2.18  
    2.19 -fun sh_test_thms prover prover_name time_limit subgoalno state name_thms_pairs =
    2.20 +fun sh_test_thms prover prover_name time_limit subgoalno state counts name_thms_pairs =
    2.21    let
    2.22      val _ = println ("Testing " ^ (length_string name_thms_pairs) ^ " theorems... ")
    2.23      val name_thm_pairs =
    2.24 @@ -108,7 +108,8 @@
    2.25      val _ = debug_fn (fn () => print_names name_thm_pairs)
    2.26      val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
    2.27      val (result, proof) =
    2.28 -      produce_answer (prover time_limit (SOME axclauses) prover_name subgoalno (Proof.get_goal state))
    2.29 +      produce_answer
    2.30 +        (prover time_limit (SOME axclauses) counts prover_name subgoalno (Proof.get_goal state))
    2.31      val _ = println (string_of_result result)
    2.32      val _ = debug proof
    2.33    in
    2.34 @@ -126,11 +127,11 @@
    2.35      val _ = debug_fn (fn () => app (fn (n, tl) =>
    2.36          (debug n; app (fn t => debug ("  " ^ Display.string_of_thm t)) tl)) name_thms_pairs)
    2.37      val test_thms_fun = sh_test_thms prover prover_name time_limit 1 state
    2.38 -    fun test_thms thms = case test_thms_fun thms of (Success _, _) => true | _ => false
    2.39 +    fun test_thms counts thms = case test_thms_fun counts thms of (Success _, _) => true | _ => false
    2.40    in
    2.41      (* try prove first to check result and get used theorems *)
    2.42 -    (case test_thms_fun name_thms_pairs of
    2.43 -      (Success used, _) =>
    2.44 +    (case test_thms_fun NONE name_thms_pairs of
    2.45 +      (Success (used, const_counts), _) =>
    2.46          let
    2.47            val ordered_used = order_unique used
    2.48            val to_use =
    2.49 @@ -138,7 +139,7 @@
    2.50                filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
    2.51              else
    2.52                name_thms_pairs
    2.53 -          val min_thms = minimal test_thms to_use
    2.54 +          val min_thms = (minimal (test_thms (SOME const_counts)) to_use)
    2.55            val min_names = order_unique (map fst min_thms)
    2.56            val _ = println ("Minimal " ^ (length_string min_thms) ^ " theorems")
    2.57            val _ = debug_fn (fn () => print_names min_thms)
     3.1 --- a/src/HOL/Tools/atp_wrapper.ML	Wed Jun 03 07:12:57 2009 -0700
     3.2 +++ b/src/HOL/Tools/atp_wrapper.ML	Wed Jun 03 16:56:41 2009 +0200
     3.3 @@ -8,12 +8,6 @@
     3.4  sig
     3.5    val destdir: string ref
     3.6    val problem_name: string ref
     3.7 -  val external_prover:
     3.8 -    (unit -> (thm * (string * int)) list) ->
     3.9 -    (Path.T -> thm -> int -> (thm * (string * int)) list -> theory -> string vector) ->
    3.10 -    Path.T * string -> (string -> string option) ->
    3.11 -    (string -> string * string vector * Proof.context * thm * int -> string) ->
    3.12 -    AtpManager.prover
    3.13    val tptp_prover_opts_full: int -> bool -> bool -> Path.T * string -> AtpManager.prover
    3.14    val tptp_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover
    3.15    val tptp_prover: Path.T * string -> AtpManager.prover
    3.16 @@ -46,8 +40,8 @@
    3.17  
    3.18  (* basic template *)
    3.19  
    3.20 -fun external_prover relevance_filter write_problem_file (cmd, args) find_failure produce_answer
    3.21 -  timeout axiom_clauses name subgoalno goal =
    3.22 +fun external_prover relevance_filter preparer writer (cmd, args) find_failure produce_answer
    3.23 +  timeout axiom_clauses const_counts name subgoalno goal =
    3.24    let
    3.25      (* path to unique problem file *)
    3.26      val destdir' = ! destdir
    3.27 @@ -66,8 +60,24 @@
    3.28      val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths
    3.29      val probfile = prob_pathname subgoalno
    3.30      val fname = File.platform_path probfile
    3.31 -    val the_ax_clauses = case axiom_clauses of NONE => relevance_filter () | SOME axcls => axcls
    3.32 -    val thm_names = write_problem_file probfile th subgoalno the_ax_clauses thy
    3.33 +    val goal_cls = #1 (ResAxioms.neg_conjecture_clauses th subgoalno)
    3.34 +      handle THM ("assume: variables", _, _) =>
    3.35 +        error "Sledgehammer: Goal contains type variables (TVars)"
    3.36 +    val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) goal_cls
    3.37 +    val the_axiom_clauses =
    3.38 +      case axiom_clauses of
    3.39 +          NONE => relevance_filter goal goal_cls
    3.40 +        | SOME axcls => axcls
    3.41 +    val (thm_names, clauses) = preparer goal_cls the_axiom_clauses thy
    3.42 +    val the_const_counts = case const_counts of
    3.43 +      NONE =>
    3.44 +        ResHolClause.count_constants(
    3.45 +          case axiom_clauses of
    3.46 +            NONE => clauses
    3.47 +            | SOME axcls => #2(preparer goal_cls (relevance_filter goal goal_cls) thy)
    3.48 +          )
    3.49 +      | SOME ccs => ccs
    3.50 +    val _ = writer fname the_const_counts clauses
    3.51      val cmdline =
    3.52        if File.exists cmd then "exec " ^ File.shell_path cmd ^ " " ^ args
    3.53        else error ("Bad executable: " ^ Path.implode cmd)
    3.54 @@ -92,7 +102,7 @@
    3.55        if rc <> 0
    3.56        then Output.debug (fn () => "Sledgehammer exited with return code " ^ string_of_int rc ^ ":\n" ^ proof)
    3.57        else ()
    3.58 -  in (success, message, proof, thm_names) end;
    3.59 +  in (success, message, proof, thm_names, the_const_counts) end;
    3.60  
    3.61  
    3.62  
    3.63 @@ -100,14 +110,15 @@
    3.64  
    3.65  (* generic TPTP-based provers *)
    3.66  
    3.67 -fun tptp_prover_opts_full max_new theory_const full command timeout ax_clauses name n goal =
    3.68 +fun tptp_prover_opts_full max_new theory_const full command timeout ax_clauses ccs name n goal =
    3.69    external_prover
    3.70 -    (fn () => ResAtp.get_relevant max_new theory_const goal n)
    3.71 -    (ResAtp.write_problem_file false)
    3.72 -    command
    3.73 -    ResReconstruct.find_failure
    3.74 -    (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp)
    3.75 -    timeout ax_clauses name n goal;
    3.76 +  (ResAtp.get_relevant max_new theory_const)
    3.77 +  (ResAtp.prepare_clauses false)
    3.78 +  (ResHolClause.tptp_write_file)
    3.79 +  command
    3.80 +  ResReconstruct.find_failure
    3.81 +  (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp)
    3.82 +  timeout ax_clauses ccs name n goal;
    3.83  
    3.84  (*arbitrary ATP with TPTP input/output and problemfile as last argument*)
    3.85  fun tptp_prover_opts max_new theory_const =
    3.86 @@ -164,14 +175,15 @@
    3.87  
    3.88  (* SPASS *)
    3.89  
    3.90 -fun spass_opts max_new theory_const timeout ax_clauses name n goal = external_prover
    3.91 -  (fn () => ResAtp.get_relevant max_new theory_const goal n)
    3.92 -  (ResAtp.write_problem_file true)
    3.93 +fun spass_opts max_new theory_const timeout ax_clauses ccs name n goal = external_prover
    3.94 +  (ResAtp.get_relevant max_new theory_const)
    3.95 +  (ResAtp.prepare_clauses true)
    3.96 +  ResHolClause.dfg_write_file
    3.97    (Path.explode "$SPASS_HOME/SPASS",
    3.98      "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout)
    3.99    ResReconstruct.find_failure
   3.100    ResReconstruct.lemma_list_dfg
   3.101 -  timeout ax_clauses name n goal;
   3.102 +  timeout ax_clauses ccs name n goal;
   3.103  
   3.104  val spass = spass_opts 40 true;
   3.105  
     4.1 --- a/src/HOL/Tools/res_atp.ML	Wed Jun 03 07:12:57 2009 -0700
     4.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Jun 03 16:56:41 2009 +0200
     4.3 @@ -6,10 +6,12 @@
     4.4    val tvar_classes_of_terms : term list -> string list
     4.5    val tfree_classes_of_terms : term list -> string list
     4.6    val type_consts_of_terms : theory -> term list -> string list
     4.7 -  val get_relevant : int -> bool -> Proof.context * (thm list * thm) -> int
     4.8 -    -> (thm * (string * int)) list
     4.9 -  val write_problem_file : bool -> Path.T -> thm -> int -> (thm * (string * int)) list -> theory
    4.10 -    -> string vector
    4.11 +  val get_relevant : int -> bool -> Proof.context * (thm list * 'a) -> thm list ->
    4.12 +    (thm * (string * int)) list
    4.13 +  val prepare_clauses : bool -> thm list ->
    4.14 +    (thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list -> theory ->
    4.15 +    ResHolClause.axiom_name vector * (ResHolClause.clause list * ResHolClause.clause list *
    4.16 +    ResHolClause.clause list * ResClause.classrelClause list * ResClause.arityClause list)
    4.17  end;
    4.18  
    4.19  structure ResAtp: RES_ATP =
    4.20 @@ -516,12 +518,9 @@
    4.21      | Fol => true
    4.22      | Hol => false
    4.23  
    4.24 -fun get_relevant max_new theory_const (ctxt, (chain_ths, th)) n =
    4.25 +fun get_relevant max_new theory_const (ctxt, (chain_ths, th)) goal_cls =
    4.26    let
    4.27      val thy = ProofContext.theory_of ctxt
    4.28 -    val goal_cls = #1 (ResAxioms.neg_conjecture_clauses th n)
    4.29 -                   handle THM ("assume: variables", _, _) =>
    4.30 -                     error "Sledgehammer: Goal contains type variables (TVars)"
    4.31      val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt chain_ths
    4.32      val included_cls = included_thms |> ResAxioms.cnf_rules_pairs thy |> make_unique
    4.33                                       |> restrict_to_logic thy (isFO thy goal_cls)
    4.34 @@ -532,15 +531,9 @@
    4.35      white_cls @ relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
    4.36    end;
    4.37  
    4.38 -(* Write out problem file *)
    4.39 -fun write_problem_file dfg probfile goal n axcls thy =
    4.40 -  let val writer = if dfg then ResHolClause.dfg_write_file else ResHolClause.tptp_write_file
    4.41 -    val fname = File.platform_path probfile
    4.42 -    val axcls = make_unique axcls
    4.43 -    val goal_cls = #1 (ResAxioms.neg_conjecture_clauses goal n)
    4.44 -                   handle THM ("assume: variables", _, _) =>
    4.45 -                     error "Sledgehammer: Goal contains type variables (TVars)"
    4.46 -    val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) goal_cls
    4.47 +(* prepare and count clauses before writing *)
    4.48 +fun prepare_clauses dfg goal_cls axcls thy =
    4.49 +  let
    4.50      val ccls = subtract_cls goal_cls axcls
    4.51      val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls
    4.52      val ccltms = map prop_of ccls
    4.53 @@ -549,13 +542,13 @@
    4.54      and supers = tvar_classes_of_terms axtms
    4.55      and tycons = type_consts_of_terms thy (ccltms@axtms)
    4.56      (*TFrees in conjecture clauses; TVars in axiom clauses*)
    4.57 +    val (clnames, (conjectures, axiom_clauses, helper_clauses)) =
    4.58 +      ResHolClause.prepare_clauses dfg thy (isFO thy goal_cls) ccls axcls []
    4.59      val (supers',arity_clauses) = ResClause.make_arity_clauses_dfg dfg thy tycons supers
    4.60      val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
    4.61 -    val clnames = writer thy (isFO thy goal_cls) ccls fname (axcls,classrel_clauses,arity_clauses) []
    4.62    in
    4.63 -    Vector.fromList clnames
    4.64 -  end;
    4.65 +    (Vector.fromList clnames, (conjectures, axiom_clauses, helper_clauses, classrel_clauses, arity_clauses))
    4.66 +  end
    4.67  
    4.68  end;
    4.69  
    4.70 -
     5.1 --- a/src/HOL/Tools/res_hol_clause.ML	Wed Jun 03 07:12:57 2009 -0700
     5.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Wed Jun 03 16:56:41 2009 +0200
     5.3 @@ -23,15 +23,19 @@
     5.4      | CombVar of string * ResClause.fol_type
     5.5      | CombApp of combterm * combterm
     5.6    datatype literal = Literal of polarity * combterm
     5.7 +  datatype clause = Clause of {clause_id: clause_id, axiom_name: axiom_name, th: thm,
     5.8 +                    kind: ResClause.kind,literals: literal list, ctypes_sorts: typ list}
     5.9    val strip_comb: combterm -> combterm * combterm list
    5.10    val literals_of_term: theory -> term -> literal list * typ list
    5.11    exception TOO_TRIVIAL
    5.12 -  val tptp_write_file: theory -> bool -> thm list -> string ->
    5.13 -    (thm * (axiom_name * clause_id)) list * ResClause.classrelClause list *
    5.14 -      ResClause.arityClause list -> string list -> axiom_name list
    5.15 -  val dfg_write_file: theory -> bool -> thm list -> string ->
    5.16 -    (thm * (axiom_name * clause_id)) list * ResClause.classrelClause list *
    5.17 -      ResClause.arityClause list -> string list -> axiom_name list
    5.18 +  val count_constants: clause list * clause list * clause list * 'a * 'b ->
    5.19 +    int Symtab.table * bool Symtab.table
    5.20 +  val prepare_clauses: bool -> theory -> bool -> thm list -> (thm * (axiom_name * clause_id)) list ->
    5.21 +    string list -> axiom_name list * (clause list * clause list * clause list)
    5.22 +  val tptp_write_file: string -> int Symtab.table * bool Symtab.table ->
    5.23 +    clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit
    5.24 +  val dfg_write_file: string -> int Symtab.table * bool Symtab.table ->
    5.25 +    clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit
    5.26  end
    5.27  
    5.28  structure ResHolClause: RES_HOL_CLAUSE =
    5.29 @@ -294,7 +298,7 @@
    5.30        (map (tptp_literal cma cnh) literals, 
    5.31         map (RC.tptp_of_typeLit pos) (RC.add_typs ctypes_sorts));
    5.32  
    5.33 -fun clause2tptp cma cnh (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
    5.34 +fun clause2tptp (cma, cnh) (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
    5.35    let val (lits,tylits) = tptp_type_lits cma cnh (kind = RC.Conjecture) cls
    5.36    in
    5.37        (RC.gen_tptp_cls(clause_id,axiom_name,kind,lits,tylits), tylits)
    5.38 @@ -317,7 +321,7 @@
    5.39  
    5.40  fun dfg_vars (Clause {literals,...}) = RC.union_all (map get_uvars_l literals);
    5.41  
    5.42 -fun clause2dfg cma cnh (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
    5.43 +fun clause2dfg (cma, cnh) (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
    5.44    let val (lits,tylits) = dfg_type_lits cma cnh (kind = RC.Conjecture) cls
    5.45        val vars = dfg_vars cls
    5.46        val tvars = RC.get_tvar_strs ctypes_sorts
    5.47 @@ -350,7 +354,7 @@
    5.48      List.foldl (add_literal_decls cma cnh) decls literals
    5.49      handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
    5.50  
    5.51 -fun decls_of_clauses cma cnh clauses arity_clauses =
    5.52 +fun decls_of_clauses (cma, cnh) clauses arity_clauses =
    5.53    let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) RC.init_functab)
    5.54        val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty
    5.55        val (functab,predtab) = (List.foldl (add_clause_decls cma cnh) (init_functab, init_predtab) clauses)
    5.56 @@ -448,7 +452,7 @@
    5.57    Output.debug (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
    5.58                  (if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else ""));
    5.59  
    5.60 -fun count_constants (conjectures, axclauses, helper_clauses) =
    5.61 +fun count_constants (conjectures, axclauses, helper_clauses, _, _) =
    5.62    if minimize_applies then
    5.63       let val (const_min_arity, const_needs_hBOOL) =
    5.64            fold count_constants_clause conjectures (Symtab.empty, Symtab.empty)
    5.65 @@ -460,64 +464,63 @@
    5.66  
    5.67  (* tptp format *)
    5.68  
    5.69 +fun prepare_clauses dfg thy isFO thms ax_tuples user_lemmas =
    5.70 +  let
    5.71 +    val conjectures = make_conjecture_clauses dfg thy thms
    5.72 +    val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses dfg thy ax_tuples)
    5.73 +    val helper_clauses = get_helper_clauses dfg thy isFO (conjectures, axclauses, user_lemmas)
    5.74 +  in
    5.75 +    (clnames, (conjectures, axclauses, helper_clauses))
    5.76 +  end
    5.77 +
    5.78  (* write TPTP format to a single file *)
    5.79 -fun tptp_write_file thy isFO thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas =
    5.80 -    let val _ = Output.debug (fn () => ("Preparing to write the TPTP file " ^ filename))
    5.81 -        val conjectures = make_conjecture_clauses false thy thms
    5.82 -        val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses false thy ax_tuples)
    5.83 -        val helper_clauses = get_helper_clauses false thy isFO (conjectures, axclauses, user_lemmas)
    5.84 -        val (const_min_arity, const_needs_hBOOL) = count_constants (conjectures, axclauses, helper_clauses);
    5.85 -        val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp const_min_arity const_needs_hBOOL) conjectures)
    5.86 -        val tfree_clss = map RC.tptp_tfree_clause (List.foldl (op union_string) [] tfree_litss)
    5.87 -        val out = TextIO.openOut filename
    5.88 -    in
    5.89 -        List.app (curry TextIO.output out o #1 o (clause2tptp const_min_arity const_needs_hBOOL)) axclauses;
    5.90 -        RC.writeln_strs out tfree_clss;
    5.91 -        RC.writeln_strs out tptp_clss;
    5.92 -        List.app (curry TextIO.output out o RC.tptp_classrelClause) classrel_clauses;
    5.93 -        List.app (curry TextIO.output out o RC.tptp_arity_clause) arity_clauses;
    5.94 -        List.app (curry TextIO.output out o #1 o (clause2tptp const_min_arity const_needs_hBOOL)) helper_clauses;
    5.95 -        TextIO.closeOut out;
    5.96 -        clnames
    5.97 -    end;
    5.98 +fun tptp_write_file filename const_counts (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) =
    5.99 +  let
   5.100 +    val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp const_counts) conjectures)
   5.101 +    val tfree_clss = map RC.tptp_tfree_clause (List.foldl (op union_string) [] tfree_litss)
   5.102 +    val out = TextIO.openOut filename
   5.103 +  in
   5.104 +    List.app (curry TextIO.output out o #1 o (clause2tptp const_counts)) axclauses;
   5.105 +    RC.writeln_strs out tfree_clss;
   5.106 +    RC.writeln_strs out tptp_clss;
   5.107 +    List.app (curry TextIO.output out o RC.tptp_classrelClause) classrel_clauses;
   5.108 +    List.app (curry TextIO.output out o RC.tptp_arity_clause) arity_clauses;
   5.109 +    List.app (curry TextIO.output out o #1 o (clause2tptp const_counts)) helper_clauses;
   5.110 +    TextIO.closeOut out
   5.111 +  end;
   5.112  
   5.113  
   5.114  (* dfg format *)
   5.115  
   5.116 -fun dfg_write_file thy isFO thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas =
   5.117 -    let val _ = Output.debug (fn () => ("Preparing to write the DFG file " ^ filename))
   5.118 -        val conjectures = make_conjecture_clauses true thy thms
   5.119 -        val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses true thy ax_tuples)
   5.120 -        val helper_clauses = get_helper_clauses true thy isFO (conjectures, axclauses, user_lemmas)
   5.121 -        val (const_min_arity, const_needs_hBOOL) = count_constants (conjectures, axclauses, helper_clauses);
   5.122 -        val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg const_min_arity const_needs_hBOOL) conjectures)
   5.123 -        and probname = Path.implode (Path.base (Path.explode filename))
   5.124 -        val axstrs = map (#1 o (clause2dfg const_min_arity const_needs_hBOOL)) axclauses
   5.125 -        val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss)
   5.126 -        val out = TextIO.openOut filename
   5.127 -        val helper_clauses_strs = map (#1 o (clause2dfg const_min_arity const_needs_hBOOL)) helper_clauses
   5.128 -        val (funcs,cl_preds) = decls_of_clauses const_min_arity const_needs_hBOOL (helper_clauses @ conjectures @ axclauses) arity_clauses
   5.129 -        and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
   5.130 -    in
   5.131 -        TextIO.output (out, RC.string_of_start probname);
   5.132 -        TextIO.output (out, RC.string_of_descrip probname);
   5.133 -        TextIO.output (out, RC.string_of_symbols
   5.134 -                              (RC.string_of_funcs funcs)
   5.135 -                              (RC.string_of_preds (cl_preds @ ty_preds)));
   5.136 -        TextIO.output (out, "list_of_clauses(axioms,cnf).\n");
   5.137 -        RC.writeln_strs out axstrs;
   5.138 -        List.app (curry TextIO.output out o RC.dfg_classrelClause) classrel_clauses;
   5.139 -        List.app (curry TextIO.output out o RC.dfg_arity_clause) arity_clauses;
   5.140 -        RC.writeln_strs out helper_clauses_strs;
   5.141 -        TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n");
   5.142 -        RC.writeln_strs out tfree_clss;
   5.143 -        RC.writeln_strs out dfg_clss;
   5.144 -        TextIO.output (out, "end_of_list.\n\n");
   5.145 -        (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
   5.146 -        TextIO.output (out, "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n");
   5.147 -        TextIO.output (out, "end_problem.\n");
   5.148 -        TextIO.closeOut out;
   5.149 -        clnames
   5.150 -    end;
   5.151 +fun dfg_write_file filename const_counts (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) =
   5.152 +  let
   5.153 +    val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg const_counts) conjectures)
   5.154 +    and probname = Path.implode (Path.base (Path.explode filename))
   5.155 +    val axstrs = map (#1 o (clause2dfg const_counts)) axclauses
   5.156 +    val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss)
   5.157 +    val out = TextIO.openOut filename
   5.158 +    val helper_clauses_strs = map (#1 o (clause2dfg const_counts)) helper_clauses
   5.159 +    val (funcs,cl_preds) = decls_of_clauses const_counts (helper_clauses @ conjectures @ axclauses) arity_clauses
   5.160 +    and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
   5.161 +  in
   5.162 +    TextIO.output (out, RC.string_of_start probname);
   5.163 +    TextIO.output (out, RC.string_of_descrip probname);
   5.164 +    TextIO.output (out, RC.string_of_symbols
   5.165 +                          (RC.string_of_funcs funcs)
   5.166 +                          (RC.string_of_preds (cl_preds @ ty_preds)));
   5.167 +    TextIO.output (out, "list_of_clauses(axioms,cnf).\n");
   5.168 +    RC.writeln_strs out axstrs;
   5.169 +    List.app (curry TextIO.output out o RC.dfg_classrelClause) classrel_clauses;
   5.170 +    List.app (curry TextIO.output out o RC.dfg_arity_clause) arity_clauses;
   5.171 +    RC.writeln_strs out helper_clauses_strs;
   5.172 +    TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n");
   5.173 +    RC.writeln_strs out tfree_clss;
   5.174 +    RC.writeln_strs out dfg_clss;
   5.175 +    TextIO.output (out, "end_of_list.\n\n");
   5.176 +    (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
   5.177 +    TextIO.output (out, "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n");
   5.178 +    TextIO.output (out, "end_problem.\n");
   5.179 +    TextIO.closeOut out
   5.180 +  end;
   5.181  
   5.182  end