# HG changeset patch
# User paulson
# Date 1137489996 -3600
# Node ID f04a8755d6ca7235d7d05bc6309e87a02be12617
# Parent  f3bfe81b6e58fefaa8b4a15c384b330b1424decf
improved SPASS support

diff -r f3bfe81b6e58 -r f04a8755d6ca src/HOL/Tools/ATP/AtpCommunication.ML
--- a/src/HOL/Tools/ATP/AtpCommunication.ML	Mon Jan 16 21:55:17 2006 +0100
+++ b/src/HOL/Tools/ATP/AtpCommunication.ML	Tue Jan 17 10:26:36 2006 +0100
@@ -46,11 +46,9 @@
 (*Identifies the start/end lines of an ATP's output*)
 local open Recon_Parse in
 fun extract_proof s =
-  if cut_exists "Here is a proof with" s then
+  if cut_exists "Formulae used in the proof" s then  (*SPASS*)
     (kill_lines 0
-     o snd o cut_after ":"
-     o snd o cut_after "Here is a proof with"
-     o fst o cut_after " ||  -> .") s
+     o fst o cut_before "Formulae used in the proof") s
   else if cut_exists end_V8 s then
     (kill_lines 0    (*Vampire 8.0*)
      o fst o cut_before end_V8) s
@@ -161,7 +159,7 @@
     if thisLine = "" (*end of file?*)
     then (trace ("\nspass_extraction_failed: " ^ currentString);
 	  raise EOF)                    
-    else if String.isPrefix "--------------------------SPASS-STOP" thisLine
+    else if String.isPrefix "Formulae used in the proof" thisLine
     then 
       let val proofextract = extract_proof (currentString^thisLine)
       in 
@@ -189,7 +187,7 @@
    in                 
       if thisLine = "" then false
       else if String.isPrefix "Here is a proof" thisLine then     
-	 (trace ("\nabout to transfer SPASS proof\n:");
+	 (trace ("\nabout to transfer SPASS proof:\n");
 	  transferSpassInput (fromChild, toParent, ppid, probfile, thisLine, 
  	                     thm, sg_num,clause_arr);
 	  true) handle EOF => false
diff -r f3bfe81b6e58 -r f04a8755d6ca src/HOL/Tools/ATP/recon_transfer_proof.ML
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Mon Jan 16 21:55:17 2006 +0100
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue Jan 17 10:26:36 2006 +0100
@@ -162,15 +162,18 @@
             (map (ResClause.get_axiomName o #1) 
 	     (get_clasimp_cls clause_arr step_nums)));   
 
-fun get_axiom_names_spass proofstr clause_arr =
-  let (* parse spass proof into datatype *)
-      val _ = trace ("\nStarted parsing:\n" ^ proofstr)
-      val proof_steps = parse (#1(lex proofstr))
-      val _ = trace "\nParsing finished!"
-      (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
-  in
-    get_axiom_names (get_step_nums (List.filter is_axiom proof_steps) []) clause_arr
-  end;
+ (*String contains multiple lines. We want those of the form 
+     "253[0:Inp] et cetera..."
+  A list consisting of the first number in each line is returned. *)
+fun get_spass_linenums proofstr = 
+  let val toks = String.tokens (not o Char.isAlphaNum)
+      fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok
+        | inputno _ = NONE
+      val lines = String.tokens (fn c => c = #"\n") proofstr
+  in  List.mapPartial (inputno o toks) lines  end
+
+fun get_axiom_names_spass proofstr clause_arr  =
+   get_axiom_names (get_spass_linenums proofstr) clause_arr;
     
  (*String contains multiple lines.
   A list consisting of the first number in each line is returned. *)
@@ -189,7 +192,7 @@
   A list consisting of the first number in each line is returned. *)
 fun get_vamp_linenums proofstr = 
   let val toks = String.tokens (not o Char.isAlphaNum)
-      fun inputno [n,"input"] = Int.fromString n
+      fun inputno [ntok,"input"] = Int.fromString ntok
         | inputno _ = NONE
       val lines = String.tokens (fn c => c = #"\n") proofstr
   in  List.mapPartial (inputno o toks) lines  end
diff -r f3bfe81b6e58 -r f04a8755d6ca src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Mon Jan 16 21:55:17 2006 +0100
+++ b/src/HOL/Tools/res_atp.ML	Tue Jan 17 10:26:36 2006 +0100
@@ -97,20 +97,15 @@
             (*options are separated by Watcher.setting_sep, currently #"%"*)
             if !prover = "spass"
             then
-              let val optionline = 
+              let val baseopts = "%-PGiven=0%-PProblem=0%-Splits=0%-FullRed=0%-DocProof%-TimeLimit=" ^ time
+              val infopts = 
 		      if !AtpCommunication.reconstruct 
-		          (*Proof reconstruction works for only a limited set of 
-		            inference rules*)
-                      then space_implode "%" (!custom_spass) ^
-                           "%-DocProof%-TimeLimit=" ^ time
-                      else "-DocProof%-SOS%-FullRed=0%-TimeLimit=" ^ time (*Auto mode*)
-                  val _ = Output.debug ("SPASS option string is " ^ optionline)
-                  val _ = helper_path "SPASS_HOME" "SPASS"
-                    (*We've checked that SPASS is there for ATP/spassshell to run.*)
-              in 
-                  ([("spass", 
-                     getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",
-                     optionline, probfile)] @ 
+		          (*Proof reconstruction needs a limited set of inf rules*)
+                      then space_implode "%" (!custom_spass)                           
+                      else "-Auto%-SOS=1"
+                  val spass = helper_path "SPASS_HOME" "SPASS"
+            in 
+                ([("spass", spass, infopts ^ baseopts, probfile)] @ 
                   (make_atp_list xs (n+1)))
               end
             else if !prover = "vampire"