src/HOL/Tools/res_atp.ML
changeset 16767 2d4433759b8d
parent 16741 7a6c17b826c0
child 16802 6eeee59dac4c
--- a/src/HOL/Tools/res_atp.ML	Mon Jul 11 14:52:55 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML	Mon Jul 11 16:42:42 2005 +0200
@@ -113,7 +113,7 @@
 (* convert clauses from "assume" to conjecture. write to file "hyps" *)
 (* hypotheses of the goal currently being proved                     *)
 (*********************************************************************)
-
+(*perhaps have 2 different versions of this, depending on whether or not SpassComm.spass is set *)
 fun isar_atp_h thms =
         
     let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms
@@ -123,6 +123,7 @@
         val clss = map ResClause.make_conjecture_clause prems'''
 	val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss) 
 	val tfree_lits = ResLib.flat_noDup tfree_litss
+        (* tfree clause is different in tptp and dfg versions *)
 	val tfree_clss = map ResClause.tfree_clause tfree_lits 
         val hypsfile = File.platform_path hyps_file
 	val out = TextIO.openOut(hypsfile)
@@ -151,6 +152,24 @@
     end;
 
 
+(*********************************************************************)
+(* write out a subgoal as DFG clauses to the file "probN"           *)
+(* where N is the number of this subgoal                             *)
+(*********************************************************************)
+(*
+fun dfg_inputs_tfrees thms n tfrees = 
+    let val _ = (warning ("in dfg_inputs_tfrees 0"))
+        val clss = map (ResClause.make_conjecture_clause_thm) thms
+         val _ = (warning ("in dfg_inputs_tfrees 1"))
+	val (dfg_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2dfg clss)
+        val _ = (warning ("in dfg_inputs_tfrees 2"))
+	val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) 
+         val _ = (warning ("in dfg_inputs_tfrees 3"))
+        val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
+	val out = TextIO.openOut(probfile)
+    in
+	(ResLib.writeln_strs out (tfree_clss @ dfg_clss); TextIO.closeOut out; (if !trace_res then (warning probfile) else ()))
+    end;*)
 
 (*********************************************************************)
 (* call SPASS with settings and problem file for the current subgoal *)