A new "spass" method.

--- a/src/HOL/Tools/res_atp_methods.ML	Thu May 25 11:51:37 2006 +0200
+++ b/src/HOL/Tools/res_atp_methods.ML	Thu May 25 11:52:33 2006 +0200
@@ -8,25 +8,31 @@
 struct
   
 (* 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 =
+fun res_atp_tac dfg res_atp_oracle mode timeLimit ctxt user_thms n thm =
     (EVERY' [rtac ccontr,ObjectLogic.atomize_tac, skolemize_tac, 
 		  METAHYPS(fn negs =>
 			      HEADGOAL(Tactic.rtac 
 					   (res_atp_oracle (ProofContext.theory_of ctxt) 
-							   (ResAtp.write_subgoal_file mode ctxt negs user_thms n, timeLimit))))] n thm) handle (Fail _) => Seq.empty;
+							   (ResAtp.write_subgoal_file dfg mode ctxt negs user_thms n, timeLimit))))] n thm) handle (Fail _) => Seq.empty;
+
+(* vampire, eprover and spass tactics *)
 
-(* vampire and eprover tactics *)
+fun vampire_tac st = res_atp_tac false vampire_oracle ResAtp.Auto (!ResAtp.vampire_time) st;
+fun eprover_tac st = res_atp_tac false eprover_oracle ResAtp.Auto (!ResAtp.eprover_time) st;
+fun spass_tac st = res_atp_tac true spass_oracle ResAtp.Auto (!ResAtp.spass_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 ResAtp.Fol (!ResAtp.vampire_time) st;
+fun vampireF_tac st = res_atp_tac false vampire_oracle ResAtp.Fol (!ResAtp.vampire_time) st;
 
-fun vampireH_tac st = res_atp_tac vampire_oracle ResAtp.Hol (!ResAtp.vampire_time) st;
+fun vampireH_tac st = res_atp_tac false vampire_oracle ResAtp.Hol (!ResAtp.vampire_time) st;
+
+fun eproverF_tac st = res_atp_tac false eprover_oracle ResAtp.Fol (!ResAtp.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 false eprover_oracle ResAtp.Hol (!ResAtp.eprover_time) st;
 
-fun eproverH_tac st = res_atp_tac eprover_oracle ResAtp.Hol (!ResAtp.eprover_time) st;
+fun spassF_tac st = res_atp_tac true spass_oracle ResAtp.Fol (!ResAtp.spass_time) st;
+
+fun spassH_tac st = res_atp_tac true spass_oracle ResAtp.Hol (!ResAtp.spass_time) st;
 
 val ResAtps_setup =
   Method.add_methods 
@@ -35,6 +41,9 @@
      ("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")];
+     ("vampire", ResAtp.atp_method vampire_tac, "Vampire for FOL and HOL problems"),
+     ("spassF", ResAtp.atp_method spassF_tac, "SPASS for FOL problems"),
+     ("spassH", ResAtp.atp_method spassH_tac, "SPASS for HOL problems"),
+     ("spass", ResAtp.atp_method spass_tac, "SPASS for FOL and HOL problems")];
 
 end

--- a/src/HOL/Tools/res_atp_provers.ML	Thu May 25 11:51:37 2006 +0200
+++ b/src/HOL/Tools/res_atp_provers.ML	Thu May 25 11:52:33 2006 +0200
@@ -17,6 +17,11 @@
      (thisLine = "# Proof found!\n" orelse if_proof_E instr) 
   end;
 
+fun if_proof_spass instr = 
+    let val thisLine = TextIO.inputLine instr
+    in thisLine <> "" andalso 
+       (thisLine = "SPASS beiseite: Proof found.\n" orelse if_proof_spass instr) 
+    end;
 
 local 
 
@@ -44,6 +49,17 @@
   in if_proof_E instr
   end; 
 
+fun call_spass (file:string, time:int) =
+    let val _ = location file
+	val runtime = "-TimeLimit=" ^ (string_of_int time)
+	val spass = ResAtp.helper_path "SPASS_HOME" "SPASS"
+	val ch:(TextIO.instream,TextIO.outstream) Unix.proc =
+	    Unix.execute(spass, [runtime,"-Splits=0", "-FullRed=0", "-SOS=1",file])
+	val (instr,outstr) = Unix.streamsOf ch
+    in if_proof_spass instr
+    end;
+
+
 end
 
 fun vampire_o _ (file,time) = 
@@ -56,5 +72,11 @@
   then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
   else (ResAtp.cond_rm_tmp file; raise Fail ("eprover oracle failed"));
 
+fun spass_o _ (file,time) =
+    if call_spass (file,time)
+    then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
+    else (ResAtp.cond_rm_tmp file; raise Fail ("SPASS oracle failed"));
+
+
 end;