--- 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
--- 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
--- 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"