1.1 --- a/src/HOL/Tools/res_atp.ML Mon Jul 11 14:52:55 2005 +0200
1.2 +++ b/src/HOL/Tools/res_atp.ML Mon Jul 11 16:42:42 2005 +0200
1.3 @@ -113,7 +113,7 @@
1.4 (* convert clauses from "assume" to conjecture. write to file "hyps" *)
1.5 (* hypotheses of the goal currently being proved *)
1.6 (*********************************************************************)
1.7 -
1.8 +(*perhaps have 2 different versions of this, depending on whether or not SpassComm.spass is set *)
1.9 fun isar_atp_h thms =
1.10
1.11 let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms
1.12 @@ -123,6 +123,7 @@
1.13 val clss = map ResClause.make_conjecture_clause prems'''
1.14 val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
1.15 val tfree_lits = ResLib.flat_noDup tfree_litss
1.16 + (* tfree clause is different in tptp and dfg versions *)
1.17 val tfree_clss = map ResClause.tfree_clause tfree_lits
1.18 val hypsfile = File.platform_path hyps_file
1.19 val out = TextIO.openOut(hypsfile)
1.20 @@ -151,6 +152,24 @@
1.21 end;
1.22
1.23
1.24 +(*********************************************************************)
1.25 +(* write out a subgoal as DFG clauses to the file "probN" *)
1.26 +(* where N is the number of this subgoal *)
1.27 +(*********************************************************************)
1.28 +(*
1.29 +fun dfg_inputs_tfrees thms n tfrees =
1.30 + let val _ = (warning ("in dfg_inputs_tfrees 0"))
1.31 + val clss = map (ResClause.make_conjecture_clause_thm) thms
1.32 + val _ = (warning ("in dfg_inputs_tfrees 1"))
1.33 + val (dfg_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2dfg clss)
1.34 + val _ = (warning ("in dfg_inputs_tfrees 2"))
1.35 + val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees)
1.36 + val _ = (warning ("in dfg_inputs_tfrees 3"))
1.37 + val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
1.38 + val out = TextIO.openOut(probfile)
1.39 + in
1.40 + (ResLib.writeln_strs out (tfree_clss @ dfg_clss); TextIO.closeOut out; (if !trace_res then (warning probfile) else ()))
1.41 + end;*)
1.42
1.43 (*********************************************************************)
1.44 (* call SPASS with settings and problem file for the current subgoal *)