# HG changeset patch
# User mengj
# Date 1141699766 -3600
# Node ID 45c8db82893d7b9f1ac35daaee20c1e9ae115f82
# Parent  ee5fde055c9a17228e4e11b428eb646269d2a247
When ATP methods call ATPs, all input clauses from one subgoal are written to one file.

diff -r ee5fde055c9a -r 45c8db82893d src/HOL/ResAtpMethods.thy
--- a/src/HOL/ResAtpMethods.thy	Tue Mar 07 03:48:02 2006 +0100
+++ b/src/HOL/ResAtpMethods.thy	Tue Mar 07 03:49:26 2006 +0100
@@ -7,14 +7,13 @@
 theory ResAtpMethods
 imports Reconstruction
 uses
-  "Tools/res_atp_setup.ML"
   "Tools/res_atp_provers.ML"
   ("Tools/res_atp_methods.ML")
 
 begin
 
-oracle vampire_oracle ("(string list * string list) * int") = {* ResAtpProvers.vampire_o *}
-oracle eprover_oracle ("(string list * string list) * int") = {* ResAtpProvers.eprover_o *}
+oracle vampire_oracle ("string * int") = {* ResAtpProvers.vampire_o *}
+oracle eprover_oracle ("string * int") = {* ResAtpProvers.eprover_o *}
 
 use "Tools/res_atp_methods.ML"
 setup ResAtpMethods.ResAtps_setup
diff -r ee5fde055c9a -r 45c8db82893d src/HOL/Tools/res_atp_methods.ML
--- a/src/HOL/Tools/res_atp_methods.ML	Tue Mar 07 03:48:02 2006 +0100
+++ b/src/HOL/Tools/res_atp_methods.ML	Tue Mar 07 03:49:26 2006 +0100
@@ -7,52 +7,34 @@
 
 struct
   
-
-val vampire_time = ref 60;
-val eprover_time = ref 60;
-
-fun run_vampire time =  
-    if (time >0) then vampire_time:= time
-    else vampire_time:=60;
-
-fun run_eprover time = 
-    if (time > 0) then eprover_time:= time
-    else eprover_time:=60;
-
-fun vampireLimit () = !vampire_time;
-fun eproverLimit () = !eprover_time;
-
-
-
-(* convert the negated 1st subgoal into CNF, write to files and call an ATP oracle *)
+(* convert the negated 1st subgoal into CNF, write to file and call an ATP oracle *)
 fun res_atp_tac res_atp_oracle mode timeLimit ctxt user_thms n thm =
-    (SELECT_GOAL
-	(EVERY1 [rtac ccontr,ObjectLogic.atomize_tac, skolemize_tac, 
+    (EVERY' [rtac ccontr,ObjectLogic.atomize_tac, skolemize_tac, 
 		  METAHYPS(fn negs =>
 			      HEADGOAL(Tactic.rtac 
 					   (res_atp_oracle (ProofContext.theory_of ctxt) 
-							   (ResAtpSetup.prep_atp_input mode ctxt negs user_thms n, timeLimit))))]) n thm) handle (Fail _) => Seq.empty;
+							   (ResAtp.write_subgoal_file mode ctxt negs user_thms n, timeLimit))))] n thm) handle (Fail _) => Seq.empty;
 
 (* vampire and eprover tactics *)
 
-fun vampire_tac st = res_atp_tac vampire_oracle ResAtpSetup.Auto (!vampire_time) st;
-fun eprover_tac st = res_atp_tac eprover_oracle ResAtpSetup.Auto (!eprover_time) st;
+fun vampire_tac st = res_atp_tac vampire_oracle ResAtp.Auto (!ResAtp.vampire_time) st;
+fun eprover_tac st = res_atp_tac eprover_oracle ResAtp.Auto (!ResAtp.eprover_time) st;
 
-fun vampireF_tac st = res_atp_tac vampire_oracle ResAtpSetup.Fol (!vampire_time) st;
+fun vampireF_tac st = res_atp_tac vampire_oracle ResAtp.Fol (!ResAtp.vampire_time) st;
 
-fun vampireH_tac st = res_atp_tac vampire_oracle ResAtpSetup.Hol (!vampire_time) st;
+fun vampireH_tac st = res_atp_tac vampire_oracle ResAtp.Hol (!ResAtp.vampire_time) st;
 
-fun eproverF_tac st = res_atp_tac eprover_oracle ResAtpSetup.Fol (!eprover_time) st;
+fun eproverF_tac st = res_atp_tac eprover_oracle ResAtp.Fol (!ResAtp.eprover_time) st;
 
-fun eproverH_tac st = res_atp_tac eprover_oracle ResAtpSetup.Hol (!eprover_time) st;
+fun eproverH_tac st = res_atp_tac eprover_oracle ResAtp.Hol (!ResAtp.eprover_time) st;
 
 val ResAtps_setup =
   Method.add_methods 
-    [("vampireF", ResAtpSetup.atp_method vampireF_tac, "Vampire for FOL problems"),
-     ("eproverF", ResAtpSetup.atp_method eproverF_tac, "E prover for FOL problems"),
-     ("vampireH", ResAtpSetup.atp_method vampireH_tac, "Vampire for HOL problems"),
-     ("eproverH", ResAtpSetup.atp_method eproverH_tac, "E prover for HOL problems"),
-     ("eprover", ResAtpSetup.atp_method eprover_tac, "E prover for FOL and HOL problems"),
-     ("vampire", ResAtpSetup.atp_method vampire_tac, "Vampire for FOL and HOL problems")];
+    [("vampireF", ResAtp.atp_method vampireF_tac, "Vampire for FOL problems"),
+     ("eproverF", ResAtp.atp_method eproverF_tac, "E prover for FOL problems"),
+     ("vampireH", ResAtp.atp_method vampireH_tac, "Vampire for HOL problems"),
+     ("eproverH", ResAtp.atp_method eproverH_tac, "E prover for HOL problems"),
+     ("eprover", ResAtp.atp_method eprover_tac, "E prover for FOL and HOL problems"),
+     ("vampire", ResAtp.atp_method vampire_tac, "Vampire for FOL and HOL problems")];
 
 end