Integrated vampire lemma code.
authorquigley
Tue Jun 21 23:44:18 2005 +0200 (2005-06-21)
changeset 165207a9cda53bfa2
parent 16519 b3235bd87da7
child 16521 ad77345f1db8
Integrated vampire lemma code.
src/HOL/Tools/ATP/SpassCommunication.ML
src/HOL/Tools/ATP/recon_parse.ML
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/ATP/SpassCommunication.ML	Tue Jun 21 21:41:08 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/SpassCommunication.ML	Tue Jun 21 23:44:18 2005 +0200
     1.3 @@ -42,8 +42,7 @@
     1.4  (**********************************************************************)
     1.5  
     1.6  
     1.7 -val atomize_tac =
     1.8 -    SUBGOAL
     1.9 +val atomize_tac =    SUBGOAL
    1.10       (fn (prop,_) =>
    1.11  	 let val ts = Logic.strip_assums_hyp prop
    1.12  	 in EVERY1 
     2.1 --- a/src/HOL/Tools/ATP/recon_parse.ML	Tue Jun 21 21:41:08 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/recon_parse.ML	Tue Jun 21 23:44:18 2005 +0200
     2.3 @@ -209,16 +209,24 @@
     2.4  				  then 
     2.5  				      nums
     2.6  				  else
     2.7 -			          let val num = hd rest
     2.8 -                                      val int_of = num_int num
     2.9 -	
    2.10 +			          let val first = hd rest
    2.11 +				
    2.12  			          in
    2.13 -				     linenums rest (int_of::nums)
    2.14 +				    if (first = (Other "*") ) 
    2.15 +				    then 
    2.16 +					
    2.17 +					 linenums rest ((num_int (hd (tl rest)))::nums)
    2.18 +				     else
    2.19 +					  linenums rest ((num_int first)::nums)
    2.20  			         end
    2.21                                  end
    2.22  
    2.23 -fun get_linenums proofstr = let val s = extract_proof proofstr
    2.24 -                                val tokens = #1(lex s)
    2.25 +
    2.26 +(* This relies on a Vampire proof line starting "% Number" or "% * Number"*)
    2.27 +(* Check this is right *)
    2.28 +
    2.29 +fun get_linenums proofstr = let (*val s = extract_proof proofstr*)
    2.30 +                                val tokens = #1(lex proofstr)
    2.31  	                 
    2.32  	                    in
    2.33  		                rev (linenums tokens [])
     3.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue Jun 21 21:41:08 2005 +0200
     3.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue Jun 21 23:44:18 2005 +0200
     3.3 @@ -475,7 +475,7 @@
     3.4                                                (***********************************)
     3.5           
     3.6                                                 val (axiom_names) = get_axiom_names_vamp proofstr  thms clause_arr  num_of_clauses
     3.7 -                                               val ax_str = "Rules from clasimpset used in proof found by SPASS: "^(rules_to_string axiom_names "")
     3.8 +                                               val ax_str = "Rules from clasimpset used in proof found by Vampire: "^(rules_to_string axiom_names "")
     3.9                                                 val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "reconstrfile")));                                                    val _ = TextIO.output (outfile, ("reconstring is: "^ax_str^"  "^goalstring))
    3.10                                                 val _ =  TextIO.closeOut outfile
    3.11                                                     
    3.12 @@ -496,7 +496,7 @@
    3.13                                                    val _ = TextIO.output (outfile, ("In exception handler"));
    3.14                                                    val _ =  TextIO.closeOut outfile
    3.15                                                in 
    3.16 -                                                  TextIO.output (toParent,"Proof found but translation failed for resolution proof: "^(remove_linebreaks proofstr) );
    3.17 +                                                  TextIO.output (toParent,"Proof found by Vampire but translation failed for resolution proof: "^(remove_linebreaks proofstr) );
    3.18                                                    TextIO.flushOut toParent;
    3.19  						   TextIO.output (toParent, thmstring^"\n");
    3.20                                           	   TextIO.flushOut toParent;
     4.1 --- a/src/HOL/Tools/ATP/watcher.ML	Tue Jun 21 21:41:08 2005 +0200
     4.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Tue Jun 21 23:44:18 2005 +0200
     4.3 @@ -514,7 +514,12 @@
     4.4                          val _ = File.append (File.tmp_path (Path.basic "child_command")) 
     4.5  			           (childCmd^"\n")
     4.6  			(* now get the number of the subgoal from the filename *)
     4.7 -			val sg_num = int_of_string(ReconOrderClauses.get_nth 5 (rev(explode childCmd)))
     4.8 +			val sg_num = if (!SpassComm.spass )
     4.9 +				     then 
    4.10 +					int_of_string(ReconOrderClauses.get_nth 5 (rev(explode childCmd)))
    4.11 +				     else
    4.12 +					int_of_string(hd (rev(explode childCmd)))
    4.13 +
    4.14  			val childIncoming = pollChildInput childInput
    4.15   			val _ = File.append (File.tmp_path (Path.basic "child_check_polled")) 
    4.16  			           ("finished polling child \n")
    4.17 @@ -562,7 +567,7 @@
    4.18  	  (********************************************************************)                  
    4.19  	  (* call resolution processes                                        *)
    4.20  	  (* settings should be a list of strings                             *)
    4.21 -	  (* e.g. ["-t 300", "-m 100000"]                                     *)
    4.22 +	  (* e.g. ["-t 300", "-m 100000"]         (TextIO.input instr)^                            *)
    4.23  	  (* takes list of (string, string, string list, string)list proclist *)
    4.24  	  (********************************************************************)
    4.25  
    4.26 @@ -600,7 +605,7 @@
    4.27  						instr = instr,
    4.28  						outstr = outstr })::procList))
    4.29                
    4.30 -                           val _ = File.append (File.tmp_path (Path.basic "exec_child"))  ("executing command for goal:\n"^goalstring^proverCmd^(concat settings)^file^(TextIO.input instr)^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
    4.31 +                           val _ = File.append (File.tmp_path (Path.basic "exec_child"))  ("executing command for goal:\n"^goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
    4.32  		       in
    4.33  			 Posix.Process.sleep (Time.fromSeconds 1); execCmds cmds newProcList
    4.34  		       end
    4.35 @@ -789,95 +794,125 @@
    4.36  	end
    4.37  
    4.38  
    4.39 -fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) =
    4.40 -  let val mychild = childInfo (setupWatcher(thm,clause_arr,  num_of_clauses))
    4.41 -      val streams =snd mychild
    4.42 -      val childin = fst streams
    4.43 -      val childout = snd streams
    4.44 -      val childpid = fst mychild
    4.45 -      val sign = sign_of_thm thm
    4.46 -      val prems = prems_of thm
    4.47 -      val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
    4.48 -      val _ = (warning ("subgoals forked to createWatcher: "^prems_string));
    4.49 -      fun vampire_proofHandler (n) =
    4.50 -	  (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    4.51 -	  VampComm.getVampInput childin; Pretty.writeln(Pretty.str  (oct_char "361")))               
    4.52 +
    4.53 +fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) = let val mychild = childInfo (setupWatcher(thm,clause_arr,  num_of_clauses))
    4.54 +			   val streams =snd mychild
    4.55 +                           val childin = fst streams
    4.56 +                           val childout = snd streams
    4.57 +                           val childpid = fst mychild
    4.58 +                           val sign = sign_of_thm thm
    4.59 +                           val prems = prems_of thm
    4.60 +                           val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
    4.61 +                           val _ = (warning ("subgoals forked to createWatcher: "^prems_string));
    4.62 +                           fun vampire_proofHandler (n) =
    4.63 +                           (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    4.64 +                           VampComm.getVampInput childin; Pretty.writeln(Pretty.str  (oct_char "361"));() )               
    4.65 +                          
    4.66 +
    4.67 +fun spass_proofHandler (n) = (
    4.68 +                                 let  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_signal1")));
    4.69 +                                      val _ = TextIO.output (outfile, ("In signal handler now\n"))
    4.70 +                                      val _ =  TextIO.closeOut outfile
    4.71 +                                      val (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin
    4.72 +                                      val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal")));
    4.73 +
    4.74 +                                      val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched))))
    4.75 +                                      val _ =  TextIO.closeOut outfile
    4.76 +                                      in          (* if a proof has been found and sent back as a reconstruction proof *)
    4.77 +                                                  if ( (substring (reconstr, 0,1))= "[")
    4.78 +                                                  then 
    4.79  
    4.80 -      fun spass_proofHandler (n) = 
    4.81 -       let val _ = File.write (File.tmp_path (Path.basic "foo_signal1")) "In signal handler now\n"
    4.82 -	   val (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin
    4.83 -	   val _ = File.append (File.tmp_path (Path.basic "foo_signal")) 
    4.84 -		      ("In signal handler  "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched)))
    4.85 -       in  (* if a proof has been found and sent back as a reconstruction proof *)
    4.86 -	 if ( (substring (reconstr, 0,1))= "[")
    4.87 -	 then 
    4.88 -	   (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    4.89 -	    Recon_Transfer.apply_res_thm reconstr goalstring;
    4.90 -	    Pretty.writeln(Pretty.str  (oct_char "361"));
    4.91 -	    
    4.92 -	    goals_being_watched := ((!goals_being_watched) - 1);
    4.93 -     
    4.94 -	    if ((!goals_being_watched) = 0)
    4.95 -	    then 
    4.96 -		let val _ = File.write (File.tmp_path (Path.basic "foo_reap_found"))
    4.97 -			       ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")
    4.98 -		in
    4.99 -		    killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   4.100 -		end
   4.101 -	    else ()
   4.102 -	   )
   4.103 -	 (* if there's no proof, but a message from Spass *)
   4.104 -	 else if ((substring (reconstr, 0,5))= "SPASS")
   4.105 -	 then
   4.106 -	   (goals_being_watched := (!goals_being_watched) -1;
   4.107 -	    Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   4.108 -	    Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring)^reconstr));
   4.109 -	    Pretty.writeln(Pretty.str  (oct_char "361"));
   4.110 -	    if (!goals_being_watched = 0)
   4.111 -	    then 
   4.112 -	      (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   4.113 -				("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n");
   4.114 -	       killWatcher (childpid); reapWatcher (childpid,childin, childout); ())
   4.115 -	    else ()
   4.116 -	  ) 
   4.117 -	  (* print out a list of rules used from clasimpset*)
   4.118 -	   else if ((substring (reconstr, 0,5))= "Rules")
   4.119 -	   then
   4.120 -	     (goals_being_watched := (!goals_being_watched) -1;
   4.121 -	      Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   4.122 -	       Pretty.writeln(Pretty.str (goalstring^reconstr));
   4.123 -	       Pretty.writeln(Pretty.str  (oct_char "361"));
   4.124 -	       if (!goals_being_watched = 0)
   4.125 -	       then 
   4.126 -		  (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   4.127 -			       ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n");
   4.128 -		   killWatcher (childpid);  reapWatcher (childpid,childin, childout);())
   4.129 -	       else ()
   4.130 -	     )
   4.131 -	  
   4.132 -	    (* if proof translation failed *)
   4.133 -	    else if ((substring (reconstr, 0,5)) = "Proof")
   4.134 -	    then 
   4.135 -	      (goals_being_watched := (!goals_being_watched) -1;
   4.136 -	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   4.137 -		Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
   4.138 -		Pretty.writeln(Pretty.str  (oct_char "361"));
   4.139 -		if (!goals_being_watched = 0)
   4.140 -		then 
   4.141 -		  (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   4.142 -			       ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n");
   4.143 -		    killWatcher (childpid); reapWatcher (childpid,childin, childout); ())
   4.144 -		else
   4.145 -		   ()
   4.146 -	     )
   4.147 -	    else  (* add something here ?*)
   4.148 -		()
   4.149 -			    
   4.150 -      end
   4.151 -	    
   4.152 -  in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
   4.153 -     IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
   4.154 -     (childin, childout, childpid)
   4.155 +                                                            (
   4.156 +                                                                 Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   4.157 +                                                                 Recon_Transfer.apply_res_thm reconstr goalstring;
   4.158 +                                                                 Pretty.writeln(Pretty.str  (oct_char "361"));
   4.159 +                                                                 
   4.160 +                                                                 goals_being_watched := ((!goals_being_watched) - 1);
   4.161 +                                                         
   4.162 +                                                                 if ((!goals_being_watched) = 0)
   4.163 +                                                                 then 
   4.164 +                                                                    (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_found")));
   4.165 +                                                                         val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   4.166 +                                                                         val _ =  TextIO.closeOut outfile
   4.167 +                                                                     in
   4.168 +                                                                         killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   4.169 +                                                                     end)
   4.170 +                                                                 else
   4.171 +                                                                    ()
   4.172 +                                                            )
   4.173 +                                                    (* if there's no proof, but a message from Spass *)
   4.174 +                                                    else if ((substring (reconstr, 0,5))= "SPASS")
   4.175 +                                                         then
   4.176 +                                                                 (
   4.177 +                                                                     goals_being_watched := (!goals_being_watched) -1;
   4.178 +                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   4.179 +                                                                      Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring)^reconstr));
   4.180 +                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));
   4.181 +                                                                      if (!goals_being_watched = 0)
   4.182 +                                                                      then 
   4.183 +                                                                          (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp")));
   4.184 +                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   4.185 +                                                                               val _ =  TextIO.closeOut outfile
   4.186 +                                                                           in
   4.187 +                                                                              killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   4.188 +                                                                           end )
   4.189 +                                                                      else
   4.190 +                                                                         ()
   4.191 +                                                                ) 
   4.192 +						   (* print out a list of rules used from clasimpset*)
   4.193 +                                                    else if ((substring (reconstr, 0,5))= "Rules")
   4.194 +                                                         then
   4.195 +                                                                 (
   4.196 +                                                                     goals_being_watched := (!goals_being_watched) -1;
   4.197 +                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   4.198 +                                                                      Pretty.writeln(Pretty.str (goalstring^reconstr));
   4.199 +                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));
   4.200 +                                                                      if (!goals_being_watched = 0)
   4.201 +                                                                      then 
   4.202 +                                                                          (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp")));
   4.203 +                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   4.204 +                                                                               val _ =  TextIO.closeOut outfile
   4.205 +                                                                           in
   4.206 +                                                                              killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
   4.207 +                                                                           end )
   4.208 +                                                                      else
   4.209 +                                                                         ()
   4.210 +                                                                )
   4.211 +							
   4.212 +                                                          (* if proof translation failed *)
   4.213 +                                                          else if ((substring (reconstr, 0,5)) = "Proof")
   4.214 +                                                               then 
   4.215 +                                                                   (
   4.216 +                                                                     goals_being_watched := (!goals_being_watched) -1;
   4.217 +                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   4.218 +                                                                      Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
   4.219 +                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));
   4.220 +                                                                      if (!goals_being_watched = 0)
   4.221 +                                                                      then 
   4.222 +                                                                          (let val  outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp")));
   4.223 +                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   4.224 +                                                                               val _ =  TextIO.closeOut outfile
   4.225 +                                                                           in
   4.226 +                                                                              killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   4.227 +                                                                           end )
   4.228 +                                                                      else
   4.229 +                                                                         ( )
   4.230 +                                                                      )
   4.231 +
   4.232 +
   4.233 +                                                                else  (* add something here ?*)
   4.234 +                                                                   ()
   4.235 +                                                                     
   4.236 +                                                                           
   4.237 +                                                            
   4.238 +                                       end)
   4.239 +
   4.240 +
   4.241 +                        
   4.242 +                       in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
   4.243 +                          IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
   4.244 +                          (childin, childout, childpid)
   4.245 +
   4.246  
   4.247  
   4.248    end
     5.1 --- a/src/HOL/Tools/res_atp.ML	Tue Jun 21 21:41:08 2005 +0200
     5.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Jun 21 23:44:18 2005 +0200
     5.3 @@ -1,5 +1,7 @@
     5.4  (*  Author: Jia Meng, Cambridge University Computer Laboratory
     5.5 +
     5.6      ID: $Id$
     5.7 +
     5.8      Copyright 2004 University of Cambridge
     5.9  
    5.10  ATPs with TPTP format input.
    5.11 @@ -24,6 +26,7 @@
    5.12  val full_spass: bool ref
    5.13  (*val spass: bool ref*)
    5.14  val vampire: bool ref
    5.15 +val custom_spass :string list  ref
    5.16  end;
    5.17  
    5.18  structure ResAtp : RES_ATP =
    5.19 @@ -44,6 +47,8 @@
    5.20  (* use spass as default prover *)
    5.21  (*val spass = ref true;*)
    5.22  
    5.23 +val custom_spass = ref ["Auto=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub","-DocProof","-TimeLimit=60"];
    5.24 +
    5.25  val vampire = ref false;
    5.26  
    5.27  val trace_res = ref false;
    5.28 @@ -156,12 +161,16 @@
    5.29  fun call_resolve_tac  (thms: Thm.thm list list)  sign (sg_terms:  Term.term list) (childin, childout,pid) n  = 
    5.30   let
    5.31     val axfile = (File.platform_path axiom_file)
    5.32 -   val hypsfile = (File.platform_path hyps_file)
    5.33 -   val clasimpfile = (File.platform_path clasimp_file)
    5.34 -     
    5.35 +
    5.36 +    val hypsfile = (File.platform_path hyps_file)
    5.37 +     val clasimpfile = (File.platform_path clasimp_file)
    5.38 +    val spass_home = getenv "SPASS_HOME"
    5.39 +
    5.40 +
    5.41     fun make_atp_list [] sign n = []
    5.42     |   make_atp_list ((sko_thm, sg_term)::xs) sign  n = 
    5.43       let 
    5.44 +
    5.45  	val skothmstr = Meson.concat_with_and (map string_of_thm sko_thm) 
    5.46  	val thmproofstr = proofstring ( skothmstr)
    5.47  	val no_returns =List.filter   not_newline ( thmproofstr)
    5.48 @@ -175,6 +184,7 @@
    5.49  	val _ = warning ("goalstring in make_atp_lists is: "^goalstring)
    5.50  
    5.51  	val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
    5.52 +
    5.53  	val _ = (warning ("prob file in cal_res_tac is: "^probfile))      
    5.54       in
    5.55         if !SpassComm.spass 
    5.56 @@ -183,14 +193,17 @@
    5.57           in  (*We've checked that SPASS is there for ATP/spassshell to run.*)
    5.58             if !full_spass 
    5.59              then (*Allow SPASS to run in Auto mode, using all its inference rules*)
    5.60 +
    5.61     		([("spass", thmstr, goalstring (*,spass_home*), 
    5.62 -	    	 getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",  
    5.63 -	     	"-DocProof%-TimeLimit=60", 
    5.64 +
    5.65 +	    	 getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell"(*( getenv "SPASS_HOME")^"/SPASS"*),  
    5.66 +	     	"-DocProof%-TimeLimit=60%-SOS", 
    5.67 +
    5.68  	     	clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1)))
    5.69    	    else (*Restrict SPASS to a small set of rules that we can parse*)
    5.70     		([("spass", thmstr, goalstring (*,spass_home*), 
    5.71  	     	getenv "ISABELLE_HOME" ^"/src/HOL/Tools/ATP/spassshell"(* (getenv "SPASS_HOME")^"/SPASS"*),  
    5.72 -	     	"-Auto=0%-IORe%-IOFc%-RTaut%-RFSub%-RBSub%-DocProof%-TimeLimit=60", 
    5.73 +	     	("-" ^ space_implode "%-" (!custom_spass)), 
    5.74  	     	clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1)))
    5.75  	 end
    5.76       else
    5.77 @@ -209,21 +222,7 @@
    5.78          warning("Sent commands to watcher!");
    5.79    	dummy_tac
    5.80   end
    5.81 -(*
    5.82 -  val axfile = (File.platform_path axiom_file)
    5.83 -    val hypsfile = (File.platform_path hyps_file)
    5.84 -     val clasimpfile = (File.platform_path  clasimp_file)
    5.85 -    val spass_home = getenv "SPASS_HOME"
    5.86 - val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int 1)
    5.87 -    
    5.88 - val (clause_arr, num_of_clauses) = ResClasimp.write_out_clasimp_small (File.platform_path clasimp_file) ;
    5.89 - val (childin,childout,pid) = Watcher.createWatcher(mp, clause_arr, num_of_clauses);
    5.90 -Watcher.callResProvers(childout, [("spass", "thmstring", "goalstr", spass_home,  "-DocProof", clasimpfile, axfile, hypsfile,probfile)]);
    5.91  
    5.92 -Watcher.callResProvers(childout, [("spass", "thmstring", "goalstr", "/homes/clq20/spassshell",  "", clasimpfile, axfile, hypsfile,probfile)]);
    5.93 -
    5.94 -
    5.95 -*)
    5.96  (**********************************************************)
    5.97  (* write out the current subgoal as a tptp file, probN,   *)
    5.98  (* then call dummy_tac - should be call_res_tac           *)
    5.99 @@ -263,9 +262,7 @@
   5.100  	get_sko_thms tfree_lits sign  prems (childin, childout, pid) thm n []
   5.101      end ;
   5.102  
   5.103 -(*fun isar_atp_goal thm n_subgoals tfree_lits   (childin, childout, pid) = 
   5.104 -              (if (!debug) then warning (string_of_thm thm) 
   5.105 -               else (isar_atp_goal' thm n_subgoals tfree_lits  (childin, childout, pid) ));*)
   5.106 +
   5.107  
   5.108  (**************************************************)
   5.109  (* convert clauses from "assume" to conjecture.   *)
   5.110 @@ -305,18 +302,7 @@
   5.111  	    ResClasimp.write_out_clasimp(*_small*) (File.platform_path clasimp_file) 
   5.112  	                                 (ProofContext.theory_of ctxt)
   5.113          val _ = (warning ("clasimp_file is this: "^(File.platform_path clasimp_file)) )  
   5.114 -
   5.115 -        (* cq: add write out clasimps to file *)
   5.116 -        (* cq:create watcher and pass to isar_atp_aux *)
   5.117 -        (* tracing *) 
   5.118 -        (*val tenth_ax = fst( Array.sub(clause_arr, 1))  
   5.119 -         val tenth_ax_thms = Recon_Transfer.memo_find_clause (tenth_ax, clause_tab)
   5.120 -         val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms)
   5.121 -         val _ = (warning ("tenth axiom in array is: "^tenth_ax))         
   5.122 -         val _ = (warning ("tenth axiom in table is: "^clause_str))         
   5.123 -                 
   5.124 -         val _ = (warning ("num_of_clauses is: "^(string_of_int (num_of_clauses))) )     
   5.125 -         *)             
   5.126 +           
   5.127          
   5.128          val (childin,childout,pid) = Watcher.createWatcher(thm,clause_arr, num_of_clauses)
   5.129          val pidstring = string_of_int(Word.toInt (Word.fromLargeWord ( Posix.Process.pidToWord pid )))