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