src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
author blanchet
Wed Mar 17 19:37:44 2010 +0100 (2010-03-17)
changeset 35827 f552152d7747
parent 35826 1590abc3d42a
child 35865 2f8fb5242799
permissions -rw-r--r--
renamed "ATP_Linkup" theory to "Sledgehammer"
     1 (*  Title:      HOL/Sledgehammer/sledgehammer_hol_clause.ML
     2     Author:     Jia Meng, NICTA
     3 
     4 FOL clauses translated from HOL formulae.
     5 *)
     6 
     7 signature SLEDGEHAMMER_HOL_CLAUSE =
     8 sig
     9   val ext: thm
    10   val comb_I: thm
    11   val comb_K: thm
    12   val comb_B: thm
    13   val comb_C: thm
    14   val comb_S: thm
    15   val minimize_applies: bool
    16   type axiom_name = string
    17   type polarity = bool
    18   type clause_id = int
    19   datatype combterm =
    20       CombConst of string * Sledgehammer_FOL_Clause.fol_type * Sledgehammer_FOL_Clause.fol_type list (*Const and Free*)
    21     | CombVar of string * Sledgehammer_FOL_Clause.fol_type
    22     | CombApp of combterm * combterm
    23   datatype literal = Literal of polarity * combterm
    24   datatype clause = Clause of {clause_id: clause_id, axiom_name: axiom_name, th: thm,
    25                     kind: Sledgehammer_FOL_Clause.kind,literals: literal list, ctypes_sorts: typ list}
    26   val type_of_combterm: combterm -> Sledgehammer_FOL_Clause.fol_type
    27   val strip_comb: combterm -> combterm * combterm list
    28   val literals_of_term: theory -> term -> literal list * typ list
    29   exception TOO_TRIVIAL
    30   val make_conjecture_clauses:  bool -> theory -> thm list -> clause list
    31   val make_axiom_clauses: bool ->
    32        theory ->
    33        (thm * (axiom_name * clause_id)) list -> (axiom_name * clause) list
    34   val get_helper_clauses: bool ->
    35        theory ->
    36        bool ->
    37        clause list * (thm * (axiom_name * clause_id)) list * string list ->
    38        clause list
    39   val tptp_write_file: bool -> Path.T ->
    40     clause list * clause list * clause list * clause list *
    41     Sledgehammer_FOL_Clause.classrelClause list * Sledgehammer_FOL_Clause.arityClause list ->
    42     int * int
    43   val dfg_write_file: bool -> Path.T ->
    44     clause list * clause list * clause list * clause list *
    45     Sledgehammer_FOL_Clause.classrelClause list * Sledgehammer_FOL_Clause.arityClause list ->
    46     int * int
    47 end
    48 
    49 structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
    50 struct
    51 
    52 structure SFC = Sledgehammer_FOL_Clause;
    53 
    54 (* theorems for combinators and function extensionality *)
    55 val ext = thm "HOL.ext";
    56 val comb_I = thm "Sledgehammer.COMBI_def";
    57 val comb_K = thm "Sledgehammer.COMBK_def";
    58 val comb_B = thm "Sledgehammer.COMBB_def";
    59 val comb_C = thm "Sledgehammer.COMBC_def";
    60 val comb_S = thm "Sledgehammer.COMBS_def";
    61 val fequal_imp_equal = thm "Sledgehammer.fequal_imp_equal";
    62 val equal_imp_fequal = thm "Sledgehammer.equal_imp_fequal";
    63 
    64 
    65 (* Parameter t_full below indicates that full type information is to be
    66 exported *)
    67 
    68 (*If true, each function will be directly applied to as many arguments as possible, avoiding
    69   use of the "apply" operator. Use of hBOOL is also minimized.*)
    70 val minimize_applies = true;
    71 
    72 fun min_arity_of const_min_arity c = the_default 0 (Symtab.lookup const_min_arity c);
    73 
    74 (*True if the constant ever appears outside of the top-level position in literals.
    75   If false, the constant always receives all of its arguments and is used as a predicate.*)
    76 fun needs_hBOOL const_needs_hBOOL c =
    77   not minimize_applies orelse
    78     the_default false (Symtab.lookup const_needs_hBOOL c);
    79 
    80 
    81 (******************************************************)
    82 (* data types for typed combinator expressions        *)
    83 (******************************************************)
    84 
    85 type axiom_name = string;
    86 type polarity = bool;
    87 type clause_id = int;
    88 
    89 datatype combterm = CombConst of string * SFC.fol_type * SFC.fol_type list (*Const and Free*)
    90                   | CombVar of string * SFC.fol_type
    91                   | CombApp of combterm * combterm
    92 
    93 datatype literal = Literal of polarity * combterm;
    94 
    95 datatype clause =
    96          Clause of {clause_id: clause_id,
    97                     axiom_name: axiom_name,
    98                     th: thm,
    99                     kind: SFC.kind,
   100                     literals: literal list,
   101                     ctypes_sorts: typ list};
   102 
   103 
   104 (*********************************************************************)
   105 (* convert a clause with type Term.term to a clause with type clause *)
   106 (*********************************************************************)
   107 
   108 fun isFalse (Literal(pol, CombConst(c,_,_))) =
   109       (pol andalso c = "c_False") orelse
   110       (not pol andalso c = "c_True")
   111   | isFalse _ = false;
   112 
   113 fun isTrue (Literal (pol, CombConst(c,_,_))) =
   114       (pol andalso c = "c_True") orelse
   115       (not pol andalso c = "c_False")
   116   | isTrue _ = false;
   117 
   118 fun isTaut (Clause {literals,...}) = exists isTrue literals;
   119 
   120 fun type_of dfg (Type (a, Ts)) =
   121       let val (folTypes,ts) = types_of dfg Ts
   122       in  (SFC.Comp(SFC.make_fixed_type_const dfg a, folTypes), ts)  end
   123   | type_of _ (tp as TFree (a, _)) =
   124       (SFC.AtomF (SFC.make_fixed_type_var a), [tp])
   125   | type_of _ (tp as TVar (v, _)) =
   126       (SFC.AtomV (SFC.make_schematic_type_var v), [tp])
   127 and types_of dfg Ts =
   128       let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
   129       in  (folTyps, SFC.union_all ts)  end;
   130 
   131 (* same as above, but no gathering of sort information *)
   132 fun simp_type_of dfg (Type (a, Ts)) =
   133       SFC.Comp(SFC.make_fixed_type_const dfg a, map (simp_type_of dfg) Ts)
   134   | simp_type_of _ (TFree (a, _)) = SFC.AtomF(SFC.make_fixed_type_var a)
   135   | simp_type_of _ (TVar (v, _)) = SFC.AtomV(SFC.make_schematic_type_var v);
   136 
   137 
   138 fun const_type_of dfg thy (c,t) =
   139       let val (tp,ts) = type_of dfg t
   140       in  (tp, ts, map (simp_type_of dfg) (Sign.const_typargs thy (c,t))) end;
   141 
   142 (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
   143 fun combterm_of dfg thy (Const(c,t)) =
   144       let val (tp,ts,tvar_list) = const_type_of dfg thy (c,t)
   145           val c' = CombConst(SFC.make_fixed_const dfg c, tp, tvar_list)
   146       in  (c',ts)  end
   147   | combterm_of dfg _ (Free(v,t)) =
   148       let val (tp,ts) = type_of dfg t
   149           val v' = CombConst(SFC.make_fixed_var v, tp, [])
   150       in  (v',ts)  end
   151   | combterm_of dfg _ (Var(v,t)) =
   152       let val (tp,ts) = type_of dfg t
   153           val v' = CombVar(SFC.make_schematic_var v,tp)
   154       in  (v',ts)  end
   155   | combterm_of dfg thy (P $ Q) =
   156       let val (P',tsP) = combterm_of dfg thy P
   157           val (Q',tsQ) = combterm_of dfg thy Q
   158       in  (CombApp(P',Q'), union (op =) tsP tsQ)  end
   159   | combterm_of _ _ (t as Abs _) = raise SFC.CLAUSE ("HOL CLAUSE", t);
   160 
   161 fun predicate_of dfg thy ((Const("Not",_) $ P), polarity) = predicate_of dfg thy (P, not polarity)
   162   | predicate_of dfg thy (t,polarity) = (combterm_of dfg thy (Envir.eta_contract t), polarity);
   163 
   164 fun literals_of_term1 dfg thy args (Const("Trueprop",_) $ P) = literals_of_term1 dfg thy args P
   165   | literals_of_term1 dfg thy args (Const("op |",_) $ P $ Q) =
   166       literals_of_term1 dfg thy (literals_of_term1 dfg thy args P) Q
   167   | literals_of_term1 dfg thy (lits,ts) P =
   168       let val ((pred,ts'),pol) = predicate_of dfg thy (P,true)
   169       in
   170           (Literal(pol,pred)::lits, union (op =) ts ts')
   171       end;
   172 
   173 fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P;
   174 val literals_of_term = literals_of_term_dfg false;
   175 
   176 (* Problem too trivial for resolution (empty clause) *)
   177 exception TOO_TRIVIAL;
   178 
   179 (* making axiom and conjecture clauses *)
   180 fun make_clause dfg thy (clause_id,axiom_name,kind,th) =
   181     let val (lits,ctypes_sorts) = literals_of_term_dfg dfg thy (prop_of th)
   182     in
   183         if forall isFalse lits
   184         then raise TOO_TRIVIAL
   185         else
   186             Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, kind = kind,
   187                     literals = lits, ctypes_sorts = ctypes_sorts}
   188     end;
   189 
   190 
   191 fun add_axiom_clause dfg thy ((th,(name,id)), pairs) =
   192   let val cls = make_clause dfg thy (id, name, SFC.Axiom, th)
   193   in
   194       if isTaut cls then pairs else (name,cls)::pairs
   195   end;
   196 
   197 fun make_axiom_clauses dfg thy = List.foldl (add_axiom_clause dfg thy) [];
   198 
   199 fun make_conjecture_clauses_aux _ _ _ [] = []
   200   | make_conjecture_clauses_aux dfg thy n (th::ths) =
   201       make_clause dfg thy (n,"conjecture", SFC.Conjecture, th) ::
   202       make_conjecture_clauses_aux dfg thy (n+1) ths;
   203 
   204 fun make_conjecture_clauses dfg thy = make_conjecture_clauses_aux dfg thy 0;
   205 
   206 
   207 (**********************************************************************)
   208 (* convert clause into ATP specific formats:                          *)
   209 (* TPTP used by Vampire and E                                         *)
   210 (* DFG used by SPASS                                                  *)
   211 (**********************************************************************)
   212 
   213 (*Result of a function type; no need to check that the argument type matches.*)
   214 fun result_type (SFC.Comp ("tc_fun", [_, tp2])) = tp2
   215   | result_type _ = error "result_type"
   216 
   217 fun type_of_combterm (CombConst (_, tp, _)) = tp
   218   | type_of_combterm (CombVar (_, tp)) = tp
   219   | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1);
   220 
   221 (*gets the head of a combinator application, along with the list of arguments*)
   222 fun strip_comb u =
   223     let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
   224         |   stripc  x =  x
   225     in  stripc(u,[])  end;
   226 
   227 val type_wrapper = "ti";
   228 
   229 fun head_needs_hBOOL const_needs_hBOOL (CombConst(c,_,_)) = needs_hBOOL const_needs_hBOOL c
   230   | head_needs_hBOOL _ _ = true;
   231 
   232 fun wrap_type t_full (s, tp) =
   233   if t_full then
   234       type_wrapper ^ SFC.paren_pack [s, SFC.string_of_fol_type tp]
   235   else s;
   236 
   237 fun apply ss = "hAPP" ^ SFC.paren_pack ss;
   238 
   239 fun rev_apply (v, []) = v
   240   | rev_apply (v, arg::args) = apply [rev_apply (v, args), arg];
   241 
   242 fun string_apply (v, args) = rev_apply (v, rev args);
   243 
   244 (*Apply an operator to the argument strings, using either the "apply" operator or
   245   direct function application.*)
   246 fun string_of_applic t_full cma (CombConst (c, _, tvars), args) =
   247       let val c = if c = "equal" then "c_fequal" else c
   248           val nargs = min_arity_of cma c
   249           val args1 = List.take(args, nargs)
   250             handle Subscript => error ("string_of_applic: " ^ c ^ " has arity " ^
   251                                          Int.toString nargs ^ " but is applied to " ^
   252                                          space_implode ", " args)
   253           val args2 = List.drop(args, nargs)
   254           val targs = if not t_full then map SFC.string_of_fol_type tvars
   255                       else []
   256       in
   257           string_apply (c ^ SFC.paren_pack (args1@targs), args2)
   258       end
   259   | string_of_applic _ _ (CombVar (v, _), args) = string_apply (v, args)
   260   | string_of_applic _ _ _ = error "string_of_applic";
   261 
   262 fun wrap_type_if t_full cnh (head, s, tp) =
   263   if head_needs_hBOOL cnh head then wrap_type t_full (s, tp) else s;
   264 
   265 fun string_of_combterm (params as (t_full, cma, cnh)) t =
   266   let val (head, args) = strip_comb t
   267   in  wrap_type_if t_full cnh (head,
   268                     string_of_applic t_full cma (head, map (string_of_combterm (params)) args),
   269                     type_of_combterm t)
   270   end;
   271 
   272 (*Boolean-valued terms are here converted to literals.*)
   273 fun boolify params t =
   274   "hBOOL" ^ SFC.paren_pack [string_of_combterm params t];
   275 
   276 fun string_of_predicate (params as (_,_,cnh)) t =
   277   case t of
   278       (CombApp(CombApp(CombConst("equal",_,_), t1), t2)) =>
   279           (*DFG only: new TPTP prefers infix equality*)
   280           ("equal" ^ SFC.paren_pack [string_of_combterm params t1, string_of_combterm params t2])
   281     | _ =>
   282           case #1 (strip_comb t) of
   283               CombConst(c,_,_) => if needs_hBOOL cnh c then boolify params t else string_of_combterm params t
   284             | _ => boolify params t;
   285 
   286 
   287 (*** tptp format ***)
   288 
   289 fun tptp_of_equality params pol (t1,t2) =
   290   let val eqop = if pol then " = " else " != "
   291   in  string_of_combterm params t1 ^ eqop ^ string_of_combterm params t2  end;
   292 
   293 fun tptp_literal params (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) =
   294       tptp_of_equality params pol (t1,t2)
   295   | tptp_literal params (Literal(pol,pred)) =
   296       SFC.tptp_sign pol (string_of_predicate params pred);
   297 
   298 (*Given a clause, returns its literals paired with a list of literals concerning TFrees;
   299   the latter should only occur in conjecture clauses.*)
   300 fun tptp_type_lits params pos (Clause{literals, ctypes_sorts, ...}) =
   301       (map (tptp_literal params) literals, 
   302        map (SFC.tptp_of_typeLit pos) (SFC.add_typs ctypes_sorts));
   303 
   304 fun clause2tptp params (cls as Clause {axiom_name, clause_id, kind, ...}) =
   305   let val (lits,tylits) = tptp_type_lits params (kind = SFC.Conjecture) cls
   306   in
   307       (SFC.gen_tptp_cls(clause_id,axiom_name,kind,lits,tylits), tylits)
   308   end;
   309 
   310 
   311 (*** dfg format ***)
   312 
   313 fun dfg_literal params (Literal(pol,pred)) = SFC.dfg_sign pol (string_of_predicate params pred);
   314 
   315 fun dfg_type_lits params pos (Clause{literals, ctypes_sorts, ...}) =
   316       (map (dfg_literal params) literals, 
   317        map (SFC.dfg_of_typeLit pos) (SFC.add_typs ctypes_sorts));
   318 
   319 fun get_uvars (CombConst _) vars = vars
   320   | get_uvars (CombVar(v,_)) vars = (v::vars)
   321   | get_uvars (CombApp(P,Q)) vars = get_uvars P (get_uvars Q vars);
   322 
   323 fun get_uvars_l (Literal(_,c)) = get_uvars c [];
   324 
   325 fun dfg_vars (Clause {literals,...}) = SFC.union_all (map get_uvars_l literals);
   326 
   327 fun clause2dfg params (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
   328   let val (lits,tylits) = dfg_type_lits params (kind = SFC.Conjecture) cls
   329       val vars = dfg_vars cls
   330       val tvars = SFC.get_tvar_strs ctypes_sorts
   331   in
   332       (SFC.gen_dfg_cls(clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits)
   333   end;
   334 
   335 
   336 (** For DFG format: accumulate function and predicate declarations **)
   337 
   338 fun addtypes tvars tab = List.foldl SFC.add_foltype_funcs tab tvars;
   339 
   340 fun add_decls (t_full, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) =
   341       if c = "equal" then (addtypes tvars funcs, preds)
   342       else
   343         let val arity = min_arity_of cma c
   344             val ntys = if not t_full then length tvars else 0
   345             val addit = Symtab.update(c, arity+ntys)
   346         in
   347             if needs_hBOOL cnh c then (addtypes tvars (addit funcs), preds)
   348             else (addtypes tvars funcs, addit preds)
   349         end
   350   | add_decls _ (CombVar(_,ctp), (funcs,preds)) =
   351       (SFC.add_foltype_funcs (ctp,funcs), preds)
   352   | add_decls params (CombApp(P,Q),decls) = add_decls params (P,add_decls params (Q,decls));
   353 
   354 fun add_literal_decls params (Literal(_,c), decls) = add_decls params (c,decls);
   355 
   356 fun add_clause_decls params (Clause {literals, ...}, decls) =
   357     List.foldl (add_literal_decls params) decls literals
   358     handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
   359 
   360 fun decls_of_clauses params clauses arity_clauses =
   361   let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) SFC.init_functab)
   362       val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty
   363       val (functab,predtab) = (List.foldl (add_clause_decls params) (init_functab, init_predtab) clauses)
   364   in
   365       (Symtab.dest (List.foldl SFC.add_arityClause_funcs functab arity_clauses),
   366        Symtab.dest predtab)
   367   end;
   368 
   369 fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) =
   370   List.foldl SFC.add_type_sort_preds preds ctypes_sorts
   371   handle Symtab.DUP a => error ("predicate " ^ a ^ " has multiple arities")
   372 
   373 (*Higher-order clauses have only the predicates hBOOL and type classes.*)
   374 fun preds_of_clauses clauses clsrel_clauses arity_clauses =
   375     Symtab.dest
   376         (List.foldl SFC.add_classrelClause_preds
   377                (List.foldl SFC.add_arityClause_preds
   378                       (List.foldl add_clause_preds Symtab.empty clauses)
   379                       arity_clauses)
   380                clsrel_clauses)
   381 
   382 
   383 (**********************************************************************)
   384 (* write clauses to files                                             *)
   385 (**********************************************************************)
   386 
   387 val init_counters =
   388     Symtab.make [("c_COMBI", 0), ("c_COMBK", 0),
   389                  ("c_COMBB", 0), ("c_COMBC", 0),
   390                  ("c_COMBS", 0)];
   391 
   392 fun count_combterm (CombConst (c, _, _), ct) =
   393      (case Symtab.lookup ct c of NONE => ct  (*no counter*)
   394                                | SOME n => Symtab.update (c,n+1) ct)
   395   | count_combterm (CombVar _, ct) = ct
   396   | count_combterm (CombApp(t1,t2), ct) = count_combterm(t1, count_combterm(t2, ct));
   397 
   398 fun count_literal (Literal(_,t), ct) = count_combterm(t,ct);
   399 
   400 fun count_clause (Clause{literals,...}, ct) = List.foldl count_literal ct literals;
   401 
   402 fun count_user_clause user_lemmas (Clause{axiom_name,literals,...}, ct) =
   403   if axiom_name mem_string user_lemmas then List.foldl count_literal ct literals
   404   else ct;
   405 
   406 fun cnf_helper_thms thy =
   407   Sledgehammer_Fact_Preprocessor.cnf_rules_pairs thy
   408   o map Sledgehammer_Fact_Preprocessor.pairname
   409 
   410 fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) =
   411   if isFO then []  (*first-order*)
   412   else
   413     let
   414         val axclauses = map #2 (make_axiom_clauses dfg thy axcls)
   415         val ct0 = List.foldl count_clause init_counters conjectures
   416         val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses
   417         fun needed c = the (Symtab.lookup ct c) > 0
   418         val IK = if needed "c_COMBI" orelse needed "c_COMBK"
   419                  then cnf_helper_thms thy [comb_I,comb_K]
   420                  else []
   421         val BC = if needed "c_COMBB" orelse needed "c_COMBC"
   422                  then cnf_helper_thms thy [comb_B,comb_C]
   423                  else []
   424         val S = if needed "c_COMBS"
   425                 then cnf_helper_thms thy [comb_S]
   426                 else []
   427         val other = cnf_helper_thms thy [fequal_imp_equal,equal_imp_fequal]
   428     in
   429         map #2 (make_axiom_clauses dfg thy (other @ IK @ BC @ S))
   430     end;
   431 
   432 (*Find the minimal arity of each function mentioned in the term. Also, note which uses
   433   are not at top level, to see if hBOOL is needed.*)
   434 fun count_constants_term toplev t (const_min_arity, const_needs_hBOOL) =
   435   let val (head, args) = strip_comb t
   436       val n = length args
   437       val (const_min_arity, const_needs_hBOOL) = fold (count_constants_term false) args (const_min_arity, const_needs_hBOOL)
   438   in
   439       case head of
   440           CombConst (a,_,_) => (*predicate or function version of "equal"?*)
   441             let val a = if a="equal" andalso not toplev then "c_fequal" else a
   442             val const_min_arity = Symtab.map_default (a, n) (Integer.min n) const_min_arity
   443             in
   444               if toplev then (const_min_arity, const_needs_hBOOL)
   445               else (const_min_arity, Symtab.update (a,true) (const_needs_hBOOL))
   446             end
   447         | _ => (const_min_arity, const_needs_hBOOL)
   448   end;
   449 
   450 (*A literal is a top-level term*)
   451 fun count_constants_lit (Literal (_,t)) (const_min_arity, const_needs_hBOOL) =
   452   count_constants_term true t (const_min_arity, const_needs_hBOOL);
   453 
   454 fun count_constants_clause (Clause{literals,...}) (const_min_arity, const_needs_hBOOL) =
   455   fold count_constants_lit literals (const_min_arity, const_needs_hBOOL);
   456 
   457 fun display_arity const_needs_hBOOL (c,n) =
   458   Sledgehammer_Fact_Preprocessor.trace_msg (fn () => "Constant: " ^ c ^
   459                 " arity:\t" ^ Int.toString n ^
   460                 (if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else ""));
   461 
   462 fun count_constants (conjectures, _, extra_clauses, helper_clauses, _, _) =
   463   if minimize_applies then
   464      let val (const_min_arity, const_needs_hBOOL) =
   465           fold count_constants_clause conjectures (Symtab.empty, Symtab.empty)
   466        |> fold count_constants_clause extra_clauses
   467        |> fold count_constants_clause helper_clauses
   468      val _ = List.app (display_arity const_needs_hBOOL) (Symtab.dest (const_min_arity))
   469      in (const_min_arity, const_needs_hBOOL) end
   470   else (Symtab.empty, Symtab.empty);
   471 
   472 (* tptp format *)
   473 
   474 fun tptp_write_file t_full file clauses =
   475   let
   476     val (conjectures, axclauses, _, helper_clauses,
   477       classrel_clauses, arity_clauses) = clauses
   478     val (cma, cnh) = count_constants clauses
   479     val params = (t_full, cma, cnh)
   480     val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
   481     val tfree_clss = map SFC.tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
   482     val _ =
   483       File.write_list file (
   484         map (#1 o (clause2tptp params)) axclauses @
   485         tfree_clss @
   486         tptp_clss @
   487         map SFC.tptp_classrelClause classrel_clauses @
   488         map SFC.tptp_arity_clause arity_clauses @
   489         map (#1 o (clause2tptp params)) helper_clauses)
   490     in (length axclauses + 1, length tfree_clss + length tptp_clss)
   491   end;
   492 
   493 
   494 (* dfg format *)
   495 
   496 fun dfg_write_file t_full file clauses =
   497   let
   498     val (conjectures, axclauses, _, helper_clauses,
   499       classrel_clauses, arity_clauses) = clauses
   500     val (cma, cnh) = count_constants clauses
   501     val params = (t_full, cma, cnh)
   502     val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures)
   503     and probname = Path.implode (Path.base file)
   504     val axstrs = map (#1 o (clause2dfg params)) axclauses
   505     val tfree_clss = map SFC.dfg_tfree_clause (SFC.union_all tfree_litss)
   506     val helper_clauses_strs = map (#1 o (clause2dfg params)) helper_clauses
   507     val (funcs,cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
   508     and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
   509     val _ =
   510       File.write_list file (
   511         SFC.string_of_start probname ::
   512         SFC.string_of_descrip probname ::
   513         SFC.string_of_symbols (SFC.string_of_funcs funcs)
   514           (SFC.string_of_preds (cl_preds @ ty_preds)) ::
   515         "list_of_clauses(axioms,cnf).\n" ::
   516         axstrs @
   517         map SFC.dfg_classrelClause classrel_clauses @
   518         map SFC.dfg_arity_clause arity_clauses @
   519         helper_clauses_strs @
   520         ["end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"] @
   521         tfree_clss @
   522         dfg_clss @
   523         ["end_of_list.\n\n",
   524         (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
   525          "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n",
   526          "end_problem.\n"])
   527 
   528     in (length axclauses + length classrel_clauses + length arity_clauses +
   529       length helper_clauses + 1, length tfree_clss + length dfg_clss)
   530   end;
   531 
   532 end;
   533