141 ( |
141 ( |
142 let val thisLine = TextIO.inputLine fromChild |
142 let val thisLine = TextIO.inputLine fromChild |
143 in if ( thisLine = "SPASS beiseite: Proof found.\n" ) |
143 in if ( thisLine = "SPASS beiseite: Proof found.\n" ) |
144 then |
144 then |
145 ( |
145 ( |
146 let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (*val _ = Posix.Process.sleep(Time.fromSeconds 3 );*) |
146 let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (*val _ = Posix.Process.sleep(Time.fromSeconds 3 );*) |
147 val _ = TextIO.output (outfile, (thisLine)) |
147 val _ = TextIO.output (outfile, (thisLine)) |
148 |
148 |
149 val _ = TextIO.closeOut outfile |
149 val _ = TextIO.closeOut outfile |
150 in |
150 in |
151 startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses) |
151 startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses) |
153 ) |
153 ) |
154 else if (thisLine= "SPASS beiseite: Completion found.\n" ) |
154 else if (thisLine= "SPASS beiseite: Completion found.\n" ) |
155 then |
155 then |
156 |
156 |
157 ( |
157 ( |
158 let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (* val _ = Posix.Process.sleep(Time.fromSeconds 3 );*) |
158 let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (* val _ = Posix.Process.sleep(Time.fromSeconds 3 );*) |
159 val _ = TextIO.output (outfile, (thisLine)) |
159 val _ = TextIO.output (outfile, (thisLine)) |
160 |
160 |
161 val _ = TextIO.closeOut outfile |
161 val _ = TextIO.closeOut outfile |
162 in |
162 in |
163 |
163 |
182 Posix.Process.sleep(Time.fromSeconds 1); |
182 Posix.Process.sleep(Time.fromSeconds 1); |
183 true |
183 true |
184 end) |
184 end) |
185 else if ( thisLine = "SPASS beiseite: Ran out of time.\n" ) |
185 else if ( thisLine = "SPASS beiseite: Ran out of time.\n" ) |
186 then |
186 then |
187 ( |
187 ( let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (*val _ = Posix.Process.sleep(Time.fromSeconds 3 );*) |
188 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); |
188 val _ = TextIO.output (outfile, (thisLine)) |
189 TextIO.output (toParent,childCmd^"\n" ); |
189 |
190 TextIO.flushOut toParent; |
190 |
191 TextIO.output (toParent, thisLine); |
191 in TextIO.output (toParent, thisLine^"\n"); |
192 TextIO.flushOut toParent; |
192 TextIO.flushOut toParent; |
193 |
193 TextIO.output (toParent, thmstring^"\n"); |
194 true) |
194 TextIO.flushOut toParent; |
195 else if ( thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n" ) then |
195 TextIO.output (toParent, goalstring^"\n"); |
|
196 TextIO.flushOut toParent; |
|
197 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); |
|
198 TextIO.output (outfile, ("signalled parent\n"));TextIO.closeOut outfile; |
|
199 |
|
200 (* Attempt to prevent several signals from turning up simultaneously *) |
|
201 Posix.Process.sleep(Time.fromSeconds 1); |
|
202 true |
|
203 end) |
|
204 |
|
205 |
|
206 |
|
207 else if ( thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n" ) then |
196 ( |
208 ( |
197 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); |
209 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); |
198 TextIO.output (toParent,childCmd^"\n" ); |
210 TextIO.output (toParent,childCmd^"\n" ); |
199 TextIO.flushOut toParent; |
211 TextIO.flushOut toParent; |
200 TextIO.output (toParent, thisLine); |
212 TextIO.output (toParent, thisLine); |
234 val thmstring = TextIO.inputLine instr |
246 val thmstring = TextIO.inputLine instr |
235 val goalstring = TextIO.inputLine instr |
247 val goalstring = TextIO.inputLine instr |
236 in |
248 in |
237 (reconstr, thmstring, goalstring) |
249 (reconstr, thmstring, goalstring) |
238 end |
250 end |
239 else if (thisLine = "SPASS beiseite: Completion found.\n" ) |
251 else if (String.isPrefix "SPASS beiseite:" thisLine ) |
240 then |
252 then |
241 ( |
253 ( |
242 let val reconstr = thisLine |
254 let val reconstr = thisLine |
243 val thmstring = TextIO.inputLine instr |
255 val thmstring = TextIO.inputLine instr |
244 val goalstring = TextIO.inputLine instr |
256 val goalstring = TextIO.inputLine instr |