author | paulson |
Thu, 22 Sep 2005 14:09:48 +0200 | |
changeset 17583 | c272b91b619f |
parent 17569 | c1143a96f6d7 |
child 17690 | 8ba7c3cd24a8 |
permissions | -rw-r--r-- |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
1 |
(* Title: VampCommunication.ml |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
3 |
Author: Claire Quigley |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
4 |
Copyright 2004 University of Cambridge |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
5 |
*) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
6 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
7 |
(***************************************************************************) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
8 |
(* Code to deal with the transfer of proofs from a Vampire process *) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
9 |
(***************************************************************************) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
10 |
signature ATP_COMMUNICATION = |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
11 |
sig |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
12 |
val reconstruct : bool ref |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
13 |
val checkEProofFound: |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
14 |
TextIO.instream * TextIO.outstream * Posix.Process.pid * |
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
15 |
string * string * (ResClause.clause * thm) Array.array -> bool |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
16 |
val checkVampProofFound: |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
17 |
TextIO.instream * TextIO.outstream * Posix.Process.pid * |
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
18 |
string * string * (ResClause.clause * thm) Array.array -> bool |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
19 |
val checkSpassProofFound: |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
20 |
TextIO.instream * TextIO.outstream * Posix.Process.pid * |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
21 |
string * string * thm * int * (ResClause.clause * thm) Array.array -> bool |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
22 |
end; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
23 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
24 |
structure AtpCommunication : ATP_COMMUNICATION = |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
25 |
struct |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
26 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
27 |
(* switch for whether to reconstruct a proof found, or just list the lemmas used *) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
28 |
val reconstruct = ref false; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
29 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
30 |
exception EOF; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
31 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
32 |
val start_E = "# Proof object starts here." |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
33 |
val end_E = "# Proof object ends here." |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
34 |
val start_V6 = "%================== Proof: ======================" |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
35 |
val end_V6 = "%============== End of proof. ==================" |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
36 |
val start_V8 = "=========== Refutation ==========" |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
37 |
val end_V8 = "======= End of refutation =======" |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
38 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
39 |
(*Identifies the start/end lines of an ATP's output*) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
40 |
local open Recon_Parse in |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
41 |
fun extract_proof s = |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
42 |
if cut_exists "Here is a proof with" s then |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
43 |
(kill_lines 0 |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
44 |
o snd o cut_after ":" |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
45 |
o snd o cut_after "Here is a proof with" |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
46 |
o fst o cut_after " || -> .") s |
17569 | 47 |
else if cut_exists end_V8 s then |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
48 |
(kill_lines 0 (*Vampire 8.0*) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
49 |
o fst o cut_before end_V8) s |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
50 |
else if cut_exists end_E s then |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
51 |
(kill_lines 0 (*eproof*) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
52 |
o fst o cut_before end_E) s |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
53 |
else "??extract_proof failed" (*Couldn't find a proof*) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
54 |
end; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
55 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
56 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
57 |
(*********************************************************************************) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
58 |
(* Inspect the output of an ATP process to see if it has found a proof, *) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
59 |
(* and if so, transfer output to the input pipe of the main Isabelle process *) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
60 |
(*********************************************************************************) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
61 |
|
17569 | 62 |
fun startTransfer (endS, fromChild, toParent, ppid, goalstring, childCmd, clause_arr) = |
63 |
let fun transferInput currentString = |
|
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
64 |
let val thisLine = TextIO.inputLine fromChild |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
65 |
in |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
66 |
if thisLine = "" (*end of file?*) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
67 |
then (File.write (File.tmp_path (Path.basic"extraction_failed")) |
17569 | 68 |
("end bracket: " ^ endS ^ |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
69 |
"\naccumulated text: " ^ currentString); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
70 |
raise EOF) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
71 |
else if String.isPrefix endS thisLine |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
72 |
then let val proofextract = extract_proof (currentString^thisLine) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
73 |
in |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
74 |
File.write (File.tmp_path (Path.basic"extracted_prf")) proofextract; |
17569 | 75 |
(if endS = end_V8 (*vampire?*) |
76 |
then Recon_Transfer.vamp_lemma_list |
|
77 |
else Recon_Transfer.e_lemma_list) |
|
78 |
proofextract goalstring toParent ppid clause_arr |
|
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
79 |
end |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
80 |
else transferInput (currentString^thisLine) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
81 |
end |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
82 |
in |
17569 | 83 |
transferInput ""; true |
84 |
end handle EOF => false |
|
85 |
||
86 |
fun signal_parent (toParent, ppid, msg, goalstring) = |
|
87 |
(TextIO.output (toParent, msg); |
|
88 |
TextIO.output (toParent, goalstring^"\n"); |
|
89 |
TextIO.flushOut toParent; |
|
17583
c272b91b619f
removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents:
17569
diff
changeset
|
90 |
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)); |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
91 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
92 |
(*Called from watcher. Returns true if the Vampire process has returned a verdict.*) |
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
93 |
fun checkVampProofFound (fromChild, toParent, ppid, goalstring, childCmd, clause_arr) = |
17569 | 94 |
let val thisLine = TextIO.inputLine fromChild |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
95 |
in |
17569 | 96 |
File.append (File.tmp_path (Path.basic "proof")) thisLine; |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
97 |
if thisLine = "" |
17569 | 98 |
then (File.append (File.tmp_path (Path.basic "proof")) |
99 |
"No proof output seen \n"; |
|
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
100 |
false) |
17569 | 101 |
else if String.isPrefix start_V8 thisLine |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
102 |
then |
17569 | 103 |
startTransfer (end_V8, fromChild, toParent, ppid, goalstring, childCmd, clause_arr) |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
104 |
else if (String.isPrefix "Satisfiability detected" thisLine) orelse |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
105 |
(String.isPrefix "Refutation not found" thisLine) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
106 |
then |
17569 | 107 |
(signal_parent (toParent, ppid, "Failure\n", goalstring); |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
108 |
true) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
109 |
else |
17569 | 110 |
checkVampProofFound (fromChild, toParent, ppid, goalstring, childCmd, clause_arr) |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
111 |
end |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
112 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
113 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
114 |
(*Called from watcher. Returns true if the E process has returned a verdict.*) |
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
115 |
fun checkEProofFound (fromChild, toParent, ppid,goalstring, childCmd, clause_arr) = |
17569 | 116 |
let val thisLine = TextIO.inputLine fromChild |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
117 |
in |
17569 | 118 |
File.append (File.tmp_path (Path.basic "proof")) thisLine; |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
119 |
if thisLine = "" |
17569 | 120 |
then (File.append (File.tmp_path (Path.basic "proof")) |
121 |
"No proof output seen \n"; |
|
122 |
false) |
|
123 |
else if String.isPrefix start_E thisLine |
|
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
124 |
then |
17569 | 125 |
startTransfer (end_E, fromChild, toParent, ppid, goalstring, childCmd, clause_arr) |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
126 |
else if String.isPrefix "# Problem is satisfiable" thisLine |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
127 |
then |
17569 | 128 |
(signal_parent (toParent, ppid, "Invalid\n", goalstring); |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
129 |
true) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
130 |
else if String.isPrefix "# Failure: Resource limit exceeded" thisLine |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
131 |
then (*In fact, E distingishes "out of time" and "out of memory"*) |
17569 | 132 |
(signal_parent (toParent, ppid, "Failure\n", goalstring); |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
133 |
true) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
134 |
else |
17569 | 135 |
checkEProofFound (fromChild, toParent, ppid, goalstring, childCmd, clause_arr) |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
136 |
end |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
137 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
138 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
139 |
(**********************************************************************) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
140 |
(* Reconstruct the Spass proof w.r.t. thmstring (string version of *) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
141 |
(* Isabelle goal to be proved), then transfer the reconstruction *) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
142 |
(* steps as a string to the input pipe of the main Isabelle process *) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
143 |
(**********************************************************************) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
144 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
145 |
fun spass_reconstruct_tac proofextract goalstring toParent ppid sg_num |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
146 |
clause_arr = |
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
147 |
SELECT_GOAL |
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17488
diff
changeset
|
148 |
(EVERY1 [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac, |
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
149 |
METAHYPS(fn negs => |
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
150 |
Recon_Transfer.spass_reconstruct proofextract goalstring toParent ppid negs clause_arr)]) sg_num; |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
151 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
152 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
153 |
fun transferSpassInput (fromChild, toParent, ppid, goalstring, |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
154 |
currentString, thm, sg_num, clause_arr) = |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
155 |
let val thisLine = TextIO.inputLine fromChild |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
156 |
in |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
157 |
if thisLine = "" (*end of file?*) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
158 |
then (File.write (File.tmp_path (Path.basic"spass_extraction_failed")) currentString; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
159 |
raise EOF) |
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
160 |
else if String.isPrefix "--------------------------SPASS-STOP" thisLine |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
161 |
then |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
162 |
let val proofextract = extract_proof (currentString^thisLine) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
163 |
in |
17569 | 164 |
File.write (File.tmp_path (Path.basic"extracted_prf")) proofextract; |
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
165 |
if !reconstruct |
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
166 |
then (spass_reconstruct_tac proofextract goalstring toParent ppid sg_num |
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
167 |
clause_arr thm; ()) |
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
168 |
else Recon_Transfer.spass_lemma_list proofextract goalstring |
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
169 |
toParent ppid clause_arr |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
170 |
end |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
171 |
else transferSpassInput (fromChild, toParent, ppid, goalstring, |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
172 |
(currentString^thisLine), thm, sg_num, clause_arr) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
173 |
end; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
174 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
175 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
176 |
(*********************************************************************************) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
177 |
(* Inspect the output of a Spass process to see if it has found a proof, *) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
178 |
(* and if so, transfer output to the input pipe of the main Isabelle process *) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
179 |
(*********************************************************************************) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
180 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
181 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
182 |
fun startSpassTransfer (fromChild, toParent, ppid, goalstring,childCmd, |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
183 |
thm, sg_num,clause_arr) = |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
184 |
let val thisLine = TextIO.inputLine fromChild |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
185 |
in |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
186 |
if thisLine = "" then false |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
187 |
else if String.isPrefix "Here is a proof" thisLine then |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
188 |
(File.append (File.tmp_path (Path.basic "spass_transfer")) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
189 |
("about to transfer proof, thm is: " ^ string_of_thm thm ^ "\n"); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
190 |
transferSpassInput (fromChild, toParent, ppid, goalstring,thisLine, |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
191 |
thm, sg_num,clause_arr); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
192 |
true) handle EOF => false |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
193 |
else startSpassTransfer (fromChild, toParent, ppid, goalstring, |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
194 |
childCmd, thm, sg_num,clause_arr) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
195 |
end |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
196 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
197 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
198 |
(*Called from watcher. Returns true if the E process has returned a verdict.*) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
199 |
fun checkSpassProofFound (fromChild, toParent, ppid, goalstring, childCmd, |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
200 |
thm, sg_num, clause_arr) = |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
201 |
let val spass_proof_file = TextIO.openAppend |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
202 |
(File.platform_path(File.tmp_path (Path.basic "spass_proof"))) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
203 |
val thisLine = TextIO.inputLine fromChild |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
204 |
in |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
205 |
File.write (File.tmp_path (Path.basic "spass_response")) thisLine; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
206 |
if thisLine = "" |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
207 |
then (TextIO.output (spass_proof_file, ("No proof output seen \n")); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
208 |
TextIO.closeOut spass_proof_file; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
209 |
false) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
210 |
else if thisLine = "SPASS beiseite: Proof found.\n" |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
211 |
then |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
212 |
startSpassTransfer (fromChild, toParent, ppid, goalstring, |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
213 |
childCmd, thm, sg_num, clause_arr) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
214 |
else if thisLine = "SPASS beiseite: Completion found.\n" |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
215 |
then |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
216 |
(TextIO.output (spass_proof_file, thisLine); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
217 |
TextIO.closeOut spass_proof_file; |
17569 | 218 |
signal_parent (toParent, ppid, "Invalid\n", goalstring); |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
219 |
true) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
220 |
else if thisLine = "SPASS beiseite: Ran out of time.\n" orelse |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
221 |
thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n" |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
222 |
then |
17569 | 223 |
(signal_parent (toParent, ppid, "Failure\n", goalstring); |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
224 |
TextIO.output (spass_proof_file, "signalled parent\n"); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
225 |
TextIO.closeOut spass_proof_file; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
226 |
true) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
227 |
else |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
228 |
(TextIO.output (spass_proof_file, thisLine); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
229 |
TextIO.flushOut spass_proof_file; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
230 |
checkSpassProofFound (fromChild, toParent, ppid, goalstring, |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
231 |
childCmd, thm, sg_num, clause_arr)) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
232 |
end |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
233 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
234 |
end; |