# HG changeset patch
# User quigley
# Date 1117720451 -7200
# Node ID bb71c91e781edf26d79ed8a412e1ae8c9c1fe648
# Parent  80617b8d33c53f7d467a7af6dfed1fd6a0ef61f0
Added time lime (60 secs) to Spass calls.

diff -r 80617b8d33c5 -r bb71c91e781e src/HOL/Tools/ATP/watcher.ML
--- a/src/HOL/Tools/ATP/watcher.ML	Thu Jun 02 13:47:08 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML	Thu Jun 02 15:54:11 2005 +0200
@@ -175,9 +175,13 @@
 			   else File.mkdir dfg_dir; 
 	  
 	  val dfg_path = File.sysify_path dfg_dir;
-	  val exec_tptp2x = 
+	 (* val exec_tptp2x = 
 	        Unix.execute(getenv "TPTP2X_HOME" ^ "/tptp2X",  
-	                     ["-fdfg", "-d " ^ dfg_path, File.sysify_path wholefile])
+	                     ["-fdfg", "-d " ^ dfg_path, File.sysify_path wholefile]) *)
+        val tptp_home = getenv "TPTP2X_HOME" ^ "/tptp2X"
+       
+        val systemcall = system (tptp_home^" -fdfg -d " ^ dfg_path^" "^( File.sysify_path wholefile))
+        val _ =  warning("systemcall is "^ (string_of_int systemcall))
 	(*val _ = Posix.Process.wait ()*)
 	(*val _ =Unix.reap exec_tptp2x*)
 	  val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg"
@@ -193,7 +197,7 @@
 	       "*" ^ settings ^ "*" ^ newfile ^ "\n");
  (*sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^"/homes/clq20/IsabelleCVS/isabelle/HOL/Tools/ATP/dfg/mini_p1.dfg"^"\n"));*)
 	  TextIO.flushOut toWatcherStr;
-	  Unix.reap exec_tptp2x;
+	  (*Unix.reap exec_tptp2x;*)
 	  if File.exists
 	        (Path.append dfg_dir (Path.basic ("ax_prob"^"_" ^ probID ^ ".dfg")))
 	  then callResProvers (toWatcherStr, args)
diff -r 80617b8d33c5 -r bb71c91e781e src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Thu Jun 02 13:47:08 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML	Thu Jun 02 15:54:11 2005 +0200
@@ -189,13 +189,13 @@
    (Watcher.callResProvers(childout,
 	    [("spass", thmstr, goalstring (*,spass_home*), 
 	     getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",  
-	     "-DocProof", 
+	     "-DocProof%-TimeLimit=60", 
 	     clasimpfile, axfile, hypsfile, probfile)]))
   else	
    (Watcher.callResProvers(childout,
 	    [("spass", thmstr, goalstring (*,spass_home*), 
 	     getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",  
-	     "-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof", 
+	     "-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof%-TimeLimit=60", 
 	     clasimpfile, axfile, hypsfile, probfile)]));
      
 	(* with paramodulation *)