--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Mon Apr 26 21:18:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Mon Apr 26 21:20:43 2010 +0200
@@ -38,10 +38,10 @@
hol_clause list
val write_tptp_file : bool -> bool -> bool -> Path.T ->
hol_clause list * hol_clause list * hol_clause list * hol_clause list *
- classrel_clause list * arity_clause list -> name_pool option
+ classrel_clause list * arity_clause list -> name_pool option * int
val write_dfg_file : bool -> bool -> Path.T ->
hol_clause list * hol_clause list * hol_clause list * hol_clause list *
- classrel_clause list * arity_clause list -> name_pool option
+ classrel_clause list * arity_clause list -> name_pool option * int
end
structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
@@ -56,7 +56,7 @@
If "explicit_apply" is false, each function will be directly applied to as
many arguments as possible, avoiding use of the "apply" operator. Use of
- hBOOL is also minimized.
+ "hBOOL" is also minimized.
*)
fun min_arity_of const_min_arity c = the_default 0 (Symtab.lookup const_min_arity c);
@@ -518,17 +518,19 @@
val arity_clss = map tptp_arity_clause arity_clauses
val (helper_clss, pool) = pool_map (apfst fst oo tptp_clause params)
helper_clauses pool
+ val conjecture_offset =
+ length ax_clss + length classrel_clss + length arity_clss
+ + length helper_clss
val _ =
File.write_list file
(header () ::
section "Relevant fact" ax_clss @
+ section "Class relationship" classrel_clss @
+ section "Arity declaration" arity_clss @
section "Helper fact" helper_clss @
- section "Type variable" tfree_clss @
section "Conjecture" conjecture_clss @
- section "Class relationship" classrel_clss @
- section "Arity declaration" arity_clss)
- in pool end
-
+ section "Type variable" tfree_clss)
+ in (pool, conjecture_offset) end
(* DFG format *)
@@ -551,6 +553,9 @@
pool_map (apfst fst oo dfg_clause params) helper_clauses pool
val (funcs, cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
+ val conjecture_offset =
+ length axclauses + length classrel_clauses + length arity_clauses
+ + length helper_clauses
val _ =
File.write_list file
(header () ::
@@ -564,10 +569,10 @@
map dfg_arity_clause arity_clauses @
helper_clauses_strs @
["end_of_list.\n\nlist_of_clauses(conjectures, cnf).\n"] @
+ conjecture_clss @
tfree_clss @
- conjecture_clss @
["end_of_list.\n\n",
"end_problem.\n"])
- in pool end
+ in (pool, conjecture_offset) end
end;