1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Wed Mar 17 18:16:31 2010 +0100
1.3 @@ -0,0 +1,531 @@
1.4 +(* Title: HOL/Tools/res_hol_clause.ML
1.5 + Author: Jia Meng, NICTA
1.6 +
1.7 +FOL clauses translated from HOL formulae.
1.8 +*)
1.9 +
1.10 +signature RES_HOL_CLAUSE =
1.11 +sig
1.12 + val ext: thm
1.13 + val comb_I: thm
1.14 + val comb_K: thm
1.15 + val comb_B: thm
1.16 + val comb_C: thm
1.17 + val comb_S: thm
1.18 + val minimize_applies: bool
1.19 + type axiom_name = string
1.20 + type polarity = bool
1.21 + type clause_id = int
1.22 + datatype combterm =
1.23 + CombConst of string * Res_Clause.fol_type * Res_Clause.fol_type list (*Const and Free*)
1.24 + | CombVar of string * Res_Clause.fol_type
1.25 + | CombApp of combterm * combterm
1.26 + datatype literal = Literal of polarity * combterm
1.27 + datatype clause = Clause of {clause_id: clause_id, axiom_name: axiom_name, th: thm,
1.28 + kind: Res_Clause.kind,literals: literal list, ctypes_sorts: typ list}
1.29 + val type_of_combterm: combterm -> Res_Clause.fol_type
1.30 + val strip_comb: combterm -> combterm * combterm list
1.31 + val literals_of_term: theory -> term -> literal list * typ list
1.32 + exception TOO_TRIVIAL
1.33 + val make_conjecture_clauses: bool -> theory -> thm list -> clause list
1.34 + val make_axiom_clauses: bool ->
1.35 + theory ->
1.36 + (thm * (axiom_name * clause_id)) list -> (axiom_name * clause) list
1.37 + val get_helper_clauses: bool ->
1.38 + theory ->
1.39 + bool ->
1.40 + clause list * (thm * (axiom_name * clause_id)) list * string list ->
1.41 + clause list
1.42 + val tptp_write_file: bool -> Path.T ->
1.43 + clause list * clause list * clause list * clause list *
1.44 + Res_Clause.classrelClause list * Res_Clause.arityClause list ->
1.45 + int * int
1.46 + val dfg_write_file: bool -> Path.T ->
1.47 + clause list * clause list * clause list * clause list *
1.48 + Res_Clause.classrelClause list * Res_Clause.arityClause list ->
1.49 + int * int
1.50 +end
1.51 +
1.52 +structure Res_HOL_Clause: RES_HOL_CLAUSE =
1.53 +struct
1.54 +
1.55 +structure RC = Res_Clause; (* FIXME avoid structure alias *)
1.56 +
1.57 +(* theorems for combinators and function extensionality *)
1.58 +val ext = thm "HOL.ext";
1.59 +val comb_I = thm "ATP_Linkup.COMBI_def";
1.60 +val comb_K = thm "ATP_Linkup.COMBK_def";
1.61 +val comb_B = thm "ATP_Linkup.COMBB_def";
1.62 +val comb_C = thm "ATP_Linkup.COMBC_def";
1.63 +val comb_S = thm "ATP_Linkup.COMBS_def";
1.64 +val fequal_imp_equal = thm "ATP_Linkup.fequal_imp_equal";
1.65 +val equal_imp_fequal = thm "ATP_Linkup.equal_imp_fequal";
1.66 +
1.67 +
1.68 +(* Parameter t_full below indicates that full type information is to be
1.69 +exported *)
1.70 +
1.71 +(*If true, each function will be directly applied to as many arguments as possible, avoiding
1.72 + use of the "apply" operator. Use of hBOOL is also minimized.*)
1.73 +val minimize_applies = true;
1.74 +
1.75 +fun min_arity_of const_min_arity c = the_default 0 (Symtab.lookup const_min_arity c);
1.76 +
1.77 +(*True if the constant ever appears outside of the top-level position in literals.
1.78 + If false, the constant always receives all of its arguments and is used as a predicate.*)
1.79 +fun needs_hBOOL const_needs_hBOOL c =
1.80 + not minimize_applies orelse
1.81 + the_default false (Symtab.lookup const_needs_hBOOL c);
1.82 +
1.83 +
1.84 +(******************************************************)
1.85 +(* data types for typed combinator expressions *)
1.86 +(******************************************************)
1.87 +
1.88 +type axiom_name = string;
1.89 +type polarity = bool;
1.90 +type clause_id = int;
1.91 +
1.92 +datatype combterm = CombConst of string * RC.fol_type * RC.fol_type list (*Const and Free*)
1.93 + | CombVar of string * RC.fol_type
1.94 + | CombApp of combterm * combterm
1.95 +
1.96 +datatype literal = Literal of polarity * combterm;
1.97 +
1.98 +datatype clause =
1.99 + Clause of {clause_id: clause_id,
1.100 + axiom_name: axiom_name,
1.101 + th: thm,
1.102 + kind: RC.kind,
1.103 + literals: literal list,
1.104 + ctypes_sorts: typ list};
1.105 +
1.106 +
1.107 +(*********************************************************************)
1.108 +(* convert a clause with type Term.term to a clause with type clause *)
1.109 +(*********************************************************************)
1.110 +
1.111 +fun isFalse (Literal(pol, CombConst(c,_,_))) =
1.112 + (pol andalso c = "c_False") orelse
1.113 + (not pol andalso c = "c_True")
1.114 + | isFalse _ = false;
1.115 +
1.116 +fun isTrue (Literal (pol, CombConst(c,_,_))) =
1.117 + (pol andalso c = "c_True") orelse
1.118 + (not pol andalso c = "c_False")
1.119 + | isTrue _ = false;
1.120 +
1.121 +fun isTaut (Clause {literals,...}) = exists isTrue literals;
1.122 +
1.123 +fun type_of dfg (Type (a, Ts)) =
1.124 + let val (folTypes,ts) = types_of dfg Ts
1.125 + in (RC.Comp(RC.make_fixed_type_const dfg a, folTypes), ts) end
1.126 + | type_of _ (tp as TFree (a, _)) =
1.127 + (RC.AtomF (RC.make_fixed_type_var a), [tp])
1.128 + | type_of _ (tp as TVar (v, _)) =
1.129 + (RC.AtomV (RC.make_schematic_type_var v), [tp])
1.130 +and types_of dfg Ts =
1.131 + let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
1.132 + in (folTyps, RC.union_all ts) end;
1.133 +
1.134 +(* same as above, but no gathering of sort information *)
1.135 +fun simp_type_of dfg (Type (a, Ts)) =
1.136 + RC.Comp(RC.make_fixed_type_const dfg a, map (simp_type_of dfg) Ts)
1.137 + | simp_type_of _ (TFree (a, _)) = RC.AtomF(RC.make_fixed_type_var a)
1.138 + | simp_type_of _ (TVar (v, _)) = RC.AtomV(RC.make_schematic_type_var v);
1.139 +
1.140 +
1.141 +fun const_type_of dfg thy (c,t) =
1.142 + let val (tp,ts) = type_of dfg t
1.143 + in (tp, ts, map (simp_type_of dfg) (Sign.const_typargs thy (c,t))) end;
1.144 +
1.145 +(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
1.146 +fun combterm_of dfg thy (Const(c,t)) =
1.147 + let val (tp,ts,tvar_list) = const_type_of dfg thy (c,t)
1.148 + val c' = CombConst(RC.make_fixed_const dfg c, tp, tvar_list)
1.149 + in (c',ts) end
1.150 + | combterm_of dfg _ (Free(v,t)) =
1.151 + let val (tp,ts) = type_of dfg t
1.152 + val v' = CombConst(RC.make_fixed_var v, tp, [])
1.153 + in (v',ts) end
1.154 + | combterm_of dfg _ (Var(v,t)) =
1.155 + let val (tp,ts) = type_of dfg t
1.156 + val v' = CombVar(RC.make_schematic_var v,tp)
1.157 + in (v',ts) end
1.158 + | combterm_of dfg thy (P $ Q) =
1.159 + let val (P',tsP) = combterm_of dfg thy P
1.160 + val (Q',tsQ) = combterm_of dfg thy Q
1.161 + in (CombApp(P',Q'), union (op =) tsP tsQ) end
1.162 + | combterm_of _ _ (t as Abs _) = raise RC.CLAUSE ("HOL CLAUSE", t);
1.163 +
1.164 +fun predicate_of dfg thy ((Const("Not",_) $ P), polarity) = predicate_of dfg thy (P, not polarity)
1.165 + | predicate_of dfg thy (t,polarity) = (combterm_of dfg thy (Envir.eta_contract t), polarity);
1.166 +
1.167 +fun literals_of_term1 dfg thy args (Const("Trueprop",_) $ P) = literals_of_term1 dfg thy args P
1.168 + | literals_of_term1 dfg thy args (Const("op |",_) $ P $ Q) =
1.169 + literals_of_term1 dfg thy (literals_of_term1 dfg thy args P) Q
1.170 + | literals_of_term1 dfg thy (lits,ts) P =
1.171 + let val ((pred,ts'),pol) = predicate_of dfg thy (P,true)
1.172 + in
1.173 + (Literal(pol,pred)::lits, union (op =) ts ts')
1.174 + end;
1.175 +
1.176 +fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P;
1.177 +val literals_of_term = literals_of_term_dfg false;
1.178 +
1.179 +(* Problem too trivial for resolution (empty clause) *)
1.180 +exception TOO_TRIVIAL;
1.181 +
1.182 +(* making axiom and conjecture clauses *)
1.183 +fun make_clause dfg thy (clause_id,axiom_name,kind,th) =
1.184 + let val (lits,ctypes_sorts) = literals_of_term_dfg dfg thy (prop_of th)
1.185 + in
1.186 + if forall isFalse lits
1.187 + then raise TOO_TRIVIAL
1.188 + else
1.189 + Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, kind = kind,
1.190 + literals = lits, ctypes_sorts = ctypes_sorts}
1.191 + end;
1.192 +
1.193 +
1.194 +fun add_axiom_clause dfg thy ((th,(name,id)), pairs) =
1.195 + let val cls = make_clause dfg thy (id, name, RC.Axiom, th)
1.196 + in
1.197 + if isTaut cls then pairs else (name,cls)::pairs
1.198 + end;
1.199 +
1.200 +fun make_axiom_clauses dfg thy = List.foldl (add_axiom_clause dfg thy) [];
1.201 +
1.202 +fun make_conjecture_clauses_aux _ _ _ [] = []
1.203 + | make_conjecture_clauses_aux dfg thy n (th::ths) =
1.204 + make_clause dfg thy (n,"conjecture", RC.Conjecture, th) ::
1.205 + make_conjecture_clauses_aux dfg thy (n+1) ths;
1.206 +
1.207 +fun make_conjecture_clauses dfg thy = make_conjecture_clauses_aux dfg thy 0;
1.208 +
1.209 +
1.210 +(**********************************************************************)
1.211 +(* convert clause into ATP specific formats: *)
1.212 +(* TPTP used by Vampire and E *)
1.213 +(* DFG used by SPASS *)
1.214 +(**********************************************************************)
1.215 +
1.216 +(*Result of a function type; no need to check that the argument type matches.*)
1.217 +fun result_type (RC.Comp ("tc_fun", [_, tp2])) = tp2
1.218 + | result_type _ = error "result_type"
1.219 +
1.220 +fun type_of_combterm (CombConst (_, tp, _)) = tp
1.221 + | type_of_combterm (CombVar (_, tp)) = tp
1.222 + | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1);
1.223 +
1.224 +(*gets the head of a combinator application, along with the list of arguments*)
1.225 +fun strip_comb u =
1.226 + let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
1.227 + | stripc x = x
1.228 + in stripc(u,[]) end;
1.229 +
1.230 +val type_wrapper = "ti";
1.231 +
1.232 +fun head_needs_hBOOL const_needs_hBOOL (CombConst(c,_,_)) = needs_hBOOL const_needs_hBOOL c
1.233 + | head_needs_hBOOL _ _ = true;
1.234 +
1.235 +fun wrap_type t_full (s, tp) =
1.236 + if t_full then
1.237 + type_wrapper ^ RC.paren_pack [s, RC.string_of_fol_type tp]
1.238 + else s;
1.239 +
1.240 +fun apply ss = "hAPP" ^ RC.paren_pack ss;
1.241 +
1.242 +fun rev_apply (v, []) = v
1.243 + | rev_apply (v, arg::args) = apply [rev_apply (v, args), arg];
1.244 +
1.245 +fun string_apply (v, args) = rev_apply (v, rev args);
1.246 +
1.247 +(*Apply an operator to the argument strings, using either the "apply" operator or
1.248 + direct function application.*)
1.249 +fun string_of_applic t_full cma (CombConst (c, _, tvars), args) =
1.250 + let val c = if c = "equal" then "c_fequal" else c
1.251 + val nargs = min_arity_of cma c
1.252 + val args1 = List.take(args, nargs)
1.253 + handle Subscript => error ("string_of_applic: " ^ c ^ " has arity " ^
1.254 + Int.toString nargs ^ " but is applied to " ^
1.255 + space_implode ", " args)
1.256 + val args2 = List.drop(args, nargs)
1.257 + val targs = if not t_full then map RC.string_of_fol_type tvars
1.258 + else []
1.259 + in
1.260 + string_apply (c ^ RC.paren_pack (args1@targs), args2)
1.261 + end
1.262 + | string_of_applic _ _ (CombVar (v, _), args) = string_apply (v, args)
1.263 + | string_of_applic _ _ _ = error "string_of_applic";
1.264 +
1.265 +fun wrap_type_if t_full cnh (head, s, tp) =
1.266 + if head_needs_hBOOL cnh head then wrap_type t_full (s, tp) else s;
1.267 +
1.268 +fun string_of_combterm (params as (t_full, cma, cnh)) t =
1.269 + let val (head, args) = strip_comb t
1.270 + in wrap_type_if t_full cnh (head,
1.271 + string_of_applic t_full cma (head, map (string_of_combterm (params)) args),
1.272 + type_of_combterm t)
1.273 + end;
1.274 +
1.275 +(*Boolean-valued terms are here converted to literals.*)
1.276 +fun boolify params t =
1.277 + "hBOOL" ^ RC.paren_pack [string_of_combterm params t];
1.278 +
1.279 +fun string_of_predicate (params as (_,_,cnh)) t =
1.280 + case t of
1.281 + (CombApp(CombApp(CombConst("equal",_,_), t1), t2)) =>
1.282 + (*DFG only: new TPTP prefers infix equality*)
1.283 + ("equal" ^ RC.paren_pack [string_of_combterm params t1, string_of_combterm params t2])
1.284 + | _ =>
1.285 + case #1 (strip_comb t) of
1.286 + CombConst(c,_,_) => if needs_hBOOL cnh c then boolify params t else string_of_combterm params t
1.287 + | _ => boolify params t;
1.288 +
1.289 +
1.290 +(*** tptp format ***)
1.291 +
1.292 +fun tptp_of_equality params pol (t1,t2) =
1.293 + let val eqop = if pol then " = " else " != "
1.294 + in string_of_combterm params t1 ^ eqop ^ string_of_combterm params t2 end;
1.295 +
1.296 +fun tptp_literal params (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) =
1.297 + tptp_of_equality params pol (t1,t2)
1.298 + | tptp_literal params (Literal(pol,pred)) =
1.299 + RC.tptp_sign pol (string_of_predicate params pred);
1.300 +
1.301 +(*Given a clause, returns its literals paired with a list of literals concerning TFrees;
1.302 + the latter should only occur in conjecture clauses.*)
1.303 +fun tptp_type_lits params pos (Clause{literals, ctypes_sorts, ...}) =
1.304 + (map (tptp_literal params) literals,
1.305 + map (RC.tptp_of_typeLit pos) (RC.add_typs ctypes_sorts));
1.306 +
1.307 +fun clause2tptp params (cls as Clause {axiom_name, clause_id, kind, ...}) =
1.308 + let val (lits,tylits) = tptp_type_lits params (kind = RC.Conjecture) cls
1.309 + in
1.310 + (RC.gen_tptp_cls(clause_id,axiom_name,kind,lits,tylits), tylits)
1.311 + end;
1.312 +
1.313 +
1.314 +(*** dfg format ***)
1.315 +
1.316 +fun dfg_literal params (Literal(pol,pred)) = RC.dfg_sign pol (string_of_predicate params pred);
1.317 +
1.318 +fun dfg_type_lits params pos (Clause{literals, ctypes_sorts, ...}) =
1.319 + (map (dfg_literal params) literals,
1.320 + map (RC.dfg_of_typeLit pos) (RC.add_typs ctypes_sorts));
1.321 +
1.322 +fun get_uvars (CombConst _) vars = vars
1.323 + | get_uvars (CombVar(v,_)) vars = (v::vars)
1.324 + | get_uvars (CombApp(P,Q)) vars = get_uvars P (get_uvars Q vars);
1.325 +
1.326 +fun get_uvars_l (Literal(_,c)) = get_uvars c [];
1.327 +
1.328 +fun dfg_vars (Clause {literals,...}) = RC.union_all (map get_uvars_l literals);
1.329 +
1.330 +fun clause2dfg params (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
1.331 + let val (lits,tylits) = dfg_type_lits params (kind = RC.Conjecture) cls
1.332 + val vars = dfg_vars cls
1.333 + val tvars = RC.get_tvar_strs ctypes_sorts
1.334 + in
1.335 + (RC.gen_dfg_cls(clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits)
1.336 + end;
1.337 +
1.338 +
1.339 +(** For DFG format: accumulate function and predicate declarations **)
1.340 +
1.341 +fun addtypes tvars tab = List.foldl RC.add_foltype_funcs tab tvars;
1.342 +
1.343 +fun add_decls (t_full, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) =
1.344 + if c = "equal" then (addtypes tvars funcs, preds)
1.345 + else
1.346 + let val arity = min_arity_of cma c
1.347 + val ntys = if not t_full then length tvars else 0
1.348 + val addit = Symtab.update(c, arity+ntys)
1.349 + in
1.350 + if needs_hBOOL cnh c then (addtypes tvars (addit funcs), preds)
1.351 + else (addtypes tvars funcs, addit preds)
1.352 + end
1.353 + | add_decls _ (CombVar(_,ctp), (funcs,preds)) =
1.354 + (RC.add_foltype_funcs (ctp,funcs), preds)
1.355 + | add_decls params (CombApp(P,Q),decls) = add_decls params (P,add_decls params (Q,decls));
1.356 +
1.357 +fun add_literal_decls params (Literal(_,c), decls) = add_decls params (c,decls);
1.358 +
1.359 +fun add_clause_decls params (Clause {literals, ...}, decls) =
1.360 + List.foldl (add_literal_decls params) decls literals
1.361 + handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
1.362 +
1.363 +fun decls_of_clauses params clauses arity_clauses =
1.364 + let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) RC.init_functab)
1.365 + val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty
1.366 + val (functab,predtab) = (List.foldl (add_clause_decls params) (init_functab, init_predtab) clauses)
1.367 + in
1.368 + (Symtab.dest (List.foldl RC.add_arityClause_funcs functab arity_clauses),
1.369 + Symtab.dest predtab)
1.370 + end;
1.371 +
1.372 +fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) =
1.373 + List.foldl RC.add_type_sort_preds preds ctypes_sorts
1.374 + handle Symtab.DUP a => error ("predicate " ^ a ^ " has multiple arities")
1.375 +
1.376 +(*Higher-order clauses have only the predicates hBOOL and type classes.*)
1.377 +fun preds_of_clauses clauses clsrel_clauses arity_clauses =
1.378 + Symtab.dest
1.379 + (List.foldl RC.add_classrelClause_preds
1.380 + (List.foldl RC.add_arityClause_preds
1.381 + (List.foldl add_clause_preds Symtab.empty clauses)
1.382 + arity_clauses)
1.383 + clsrel_clauses)
1.384 +
1.385 +
1.386 +(**********************************************************************)
1.387 +(* write clauses to files *)
1.388 +(**********************************************************************)
1.389 +
1.390 +val init_counters =
1.391 + Symtab.make [("c_COMBI", 0), ("c_COMBK", 0),
1.392 + ("c_COMBB", 0), ("c_COMBC", 0),
1.393 + ("c_COMBS", 0)];
1.394 +
1.395 +fun count_combterm (CombConst (c, _, _), ct) =
1.396 + (case Symtab.lookup ct c of NONE => ct (*no counter*)
1.397 + | SOME n => Symtab.update (c,n+1) ct)
1.398 + | count_combterm (CombVar _, ct) = ct
1.399 + | count_combterm (CombApp(t1,t2), ct) = count_combterm(t1, count_combterm(t2, ct));
1.400 +
1.401 +fun count_literal (Literal(_,t), ct) = count_combterm(t,ct);
1.402 +
1.403 +fun count_clause (Clause{literals,...}, ct) = List.foldl count_literal ct literals;
1.404 +
1.405 +fun count_user_clause user_lemmas (Clause{axiom_name,literals,...}, ct) =
1.406 + if axiom_name mem_string user_lemmas then List.foldl count_literal ct literals
1.407 + else ct;
1.408 +
1.409 +fun cnf_helper_thms thy =
1.410 + Res_Axioms.cnf_rules_pairs thy o map Res_Axioms.pairname
1.411 +
1.412 +fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) =
1.413 + if isFO then [] (*first-order*)
1.414 + else
1.415 + let
1.416 + val axclauses = map #2 (make_axiom_clauses dfg thy axcls)
1.417 + val ct0 = List.foldl count_clause init_counters conjectures
1.418 + val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses
1.419 + fun needed c = the (Symtab.lookup ct c) > 0
1.420 + val IK = if needed "c_COMBI" orelse needed "c_COMBK"
1.421 + then cnf_helper_thms thy [comb_I,comb_K]
1.422 + else []
1.423 + val BC = if needed "c_COMBB" orelse needed "c_COMBC"
1.424 + then cnf_helper_thms thy [comb_B,comb_C]
1.425 + else []
1.426 + val S = if needed "c_COMBS"
1.427 + then cnf_helper_thms thy [comb_S]
1.428 + else []
1.429 + val other = cnf_helper_thms thy [fequal_imp_equal,equal_imp_fequal]
1.430 + in
1.431 + map #2 (make_axiom_clauses dfg thy (other @ IK @ BC @ S))
1.432 + end;
1.433 +
1.434 +(*Find the minimal arity of each function mentioned in the term. Also, note which uses
1.435 + are not at top level, to see if hBOOL is needed.*)
1.436 +fun count_constants_term toplev t (const_min_arity, const_needs_hBOOL) =
1.437 + let val (head, args) = strip_comb t
1.438 + val n = length args
1.439 + val (const_min_arity, const_needs_hBOOL) = fold (count_constants_term false) args (const_min_arity, const_needs_hBOOL)
1.440 + in
1.441 + case head of
1.442 + CombConst (a,_,_) => (*predicate or function version of "equal"?*)
1.443 + let val a = if a="equal" andalso not toplev then "c_fequal" else a
1.444 + val const_min_arity = Symtab.map_default (a, n) (Integer.min n) const_min_arity
1.445 + in
1.446 + if toplev then (const_min_arity, const_needs_hBOOL)
1.447 + else (const_min_arity, Symtab.update (a,true) (const_needs_hBOOL))
1.448 + end
1.449 + | _ => (const_min_arity, const_needs_hBOOL)
1.450 + end;
1.451 +
1.452 +(*A literal is a top-level term*)
1.453 +fun count_constants_lit (Literal (_,t)) (const_min_arity, const_needs_hBOOL) =
1.454 + count_constants_term true t (const_min_arity, const_needs_hBOOL);
1.455 +
1.456 +fun count_constants_clause (Clause{literals,...}) (const_min_arity, const_needs_hBOOL) =
1.457 + fold count_constants_lit literals (const_min_arity, const_needs_hBOOL);
1.458 +
1.459 +fun display_arity const_needs_hBOOL (c,n) =
1.460 + Res_Axioms.trace_msg (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
1.461 + (if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else ""));
1.462 +
1.463 +fun count_constants (conjectures, _, extra_clauses, helper_clauses, _, _) =
1.464 + if minimize_applies then
1.465 + let val (const_min_arity, const_needs_hBOOL) =
1.466 + fold count_constants_clause conjectures (Symtab.empty, Symtab.empty)
1.467 + |> fold count_constants_clause extra_clauses
1.468 + |> fold count_constants_clause helper_clauses
1.469 + val _ = List.app (display_arity const_needs_hBOOL) (Symtab.dest (const_min_arity))
1.470 + in (const_min_arity, const_needs_hBOOL) end
1.471 + else (Symtab.empty, Symtab.empty);
1.472 +
1.473 +(* tptp format *)
1.474 +
1.475 +fun tptp_write_file t_full file clauses =
1.476 + let
1.477 + val (conjectures, axclauses, _, helper_clauses,
1.478 + classrel_clauses, arity_clauses) = clauses
1.479 + val (cma, cnh) = count_constants clauses
1.480 + val params = (t_full, cma, cnh)
1.481 + val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
1.482 + val tfree_clss = map RC.tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
1.483 + val _ =
1.484 + File.write_list file (
1.485 + map (#1 o (clause2tptp params)) axclauses @
1.486 + tfree_clss @
1.487 + tptp_clss @
1.488 + map RC.tptp_classrelClause classrel_clauses @
1.489 + map RC.tptp_arity_clause arity_clauses @
1.490 + map (#1 o (clause2tptp params)) helper_clauses)
1.491 + in (length axclauses + 1, length tfree_clss + length tptp_clss)
1.492 + end;
1.493 +
1.494 +
1.495 +(* dfg format *)
1.496 +
1.497 +fun dfg_write_file t_full file clauses =
1.498 + let
1.499 + val (conjectures, axclauses, _, helper_clauses,
1.500 + classrel_clauses, arity_clauses) = clauses
1.501 + val (cma, cnh) = count_constants clauses
1.502 + val params = (t_full, cma, cnh)
1.503 + val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures)
1.504 + and probname = Path.implode (Path.base file)
1.505 + val axstrs = map (#1 o (clause2dfg params)) axclauses
1.506 + val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss)
1.507 + val helper_clauses_strs = map (#1 o (clause2dfg params)) helper_clauses
1.508 + val (funcs,cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
1.509 + and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
1.510 + val _ =
1.511 + File.write_list file (
1.512 + RC.string_of_start probname ::
1.513 + RC.string_of_descrip probname ::
1.514 + RC.string_of_symbols (RC.string_of_funcs funcs)
1.515 + (RC.string_of_preds (cl_preds @ ty_preds)) ::
1.516 + "list_of_clauses(axioms,cnf).\n" ::
1.517 + axstrs @
1.518 + map RC.dfg_classrelClause classrel_clauses @
1.519 + map RC.dfg_arity_clause arity_clauses @
1.520 + helper_clauses_strs @
1.521 + ["end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"] @
1.522 + tfree_clss @
1.523 + dfg_clss @
1.524 + ["end_of_list.\n\n",
1.525 + (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
1.526 + "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n",
1.527 + "end_problem.\n"])
1.528 +
1.529 + in (length axclauses + length classrel_clauses + length arity_clauses +
1.530 + length helper_clauses + 1, length tfree_clss + length dfg_clss)
1.531 + end;
1.532 +
1.533 +end;
1.534 +