author | paulson |
Tue, 20 Sep 2005 18:43:39 +0200 | |
changeset 17525 | ae5bb6001afb |
parent 17488 | 67376a311a2b |
child 17569 | c1143a96f6d7 |
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 |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
47 |
else if cut_exists start_V8 s then |
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 snd o cut_after start_V8 |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
50 |
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
|
51 |
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
|
52 |
(kill_lines 0 (*eproof*) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
53 |
o snd o cut_after start_E |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
54 |
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
|
55 |
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
|
56 |
end; |
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 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
59 |
(*********************************************************************************) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
60 |
(* 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
|
61 |
(* 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
|
62 |
(*********************************************************************************) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
63 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
64 |
fun startTransfer (startS,endS) |
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
65 |
(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
|
66 |
let val thisLine = TextIO.inputLine fromChild |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
67 |
fun transferInput currentString = |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
68 |
let val thisLine = TextIO.inputLine fromChild |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
69 |
in |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
70 |
if thisLine = "" (*end of file?*) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
71 |
then (File.write (File.tmp_path (Path.basic"extraction_failed")) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
72 |
("start bracket: " ^ startS ^ |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
73 |
"\nend bracket: " ^ endS ^ |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
74 |
"\naccumulated text: " ^ currentString); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
75 |
raise EOF) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
76 |
else if String.isPrefix endS thisLine |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
77 |
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
|
78 |
in |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
79 |
File.write (File.tmp_path (Path.basic"extracted_prf")) proofextract; |
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
80 |
Recon_Transfer.prover_lemma_list proofextract goalstring toParent ppid clause_arr |
17484
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 |
else transferInput (currentString^thisLine) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
83 |
end |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
84 |
in |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
85 |
if thisLine = "" then false |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
86 |
else if String.isPrefix startS thisLine |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
87 |
then |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
88 |
(File.append (File.tmp_path (Path.basic "transfer_start")) |
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
89 |
("about to transfer proof, first line is: " ^ thisLine); |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
90 |
transferInput thisLine; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
91 |
true) handle EOF => false |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
92 |
else |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
93 |
startTransfer (startS,endS) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
94 |
(fromChild, toParent, ppid, goalstring, |
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
95 |
childCmd, clause_arr) |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
96 |
end |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
97 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
98 |
(*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
|
99 |
fun 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
|
100 |
let val proof_file = TextIO.openAppend |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
101 |
(File.platform_path(File.tmp_path (Path.basic "vampire_proof"))) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
102 |
val _ = File.write (File.tmp_path (Path.basic "vampire_checking_prf")) |
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
103 |
("checking if proof found. childCmd is " ^ childCmd ^ |
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
104 |
"\ngoalstring is: " ^ goalstring) |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
105 |
val thisLine = TextIO.inputLine fromChild |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
106 |
in |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
107 |
File.write (File.tmp_path (Path.basic "vampire_response")) thisLine; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
108 |
if thisLine = "" |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
109 |
then (TextIO.output (proof_file, "No proof output seen \n"); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
110 |
TextIO.closeOut proof_file; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
111 |
false) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
112 |
else if String.isPrefix "Refutation found. Thanks to Tanya" thisLine |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
113 |
then |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
114 |
startTransfer (start_V8, end_V8) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
115 |
(fromChild, toParent, ppid, goalstring, |
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
116 |
childCmd, clause_arr) |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
117 |
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
|
118 |
(String.isPrefix "Refutation not found" thisLine) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
119 |
then |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
120 |
(TextIO.output (toParent, "Failure\n"); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
121 |
TextIO.output (toParent, goalstring^"\n"); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
122 |
TextIO.flushOut toParent; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
123 |
TextIO.output (proof_file, thisLine); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
124 |
TextIO.closeOut proof_file; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
125 |
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
126 |
(* Attempt to prevent several signals from turning up simultaneously *) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
127 |
Posix.Process.sleep(Time.fromSeconds 1); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
128 |
true) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
129 |
else |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
130 |
(TextIO.output (proof_file, thisLine); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
131 |
TextIO.flushOut proof_file; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
132 |
checkVampProofFound (fromChild, toParent, ppid, |
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
133 |
goalstring,childCmd, clause_arr)) |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
134 |
end |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
135 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
136 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
137 |
(*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
|
138 |
fun 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
|
139 |
let val E_proof_file = TextIO.openAppend |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
140 |
(File.platform_path(File.tmp_path (Path.basic "e_proof"))) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
141 |
val _ = File.write (File.tmp_path (Path.basic "e_checking_prf")) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
142 |
("checking if proof found. childCmd is " ^ childCmd ^ |
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
143 |
"\ngoalstring is: " ^ goalstring) |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
144 |
val thisLine = TextIO.inputLine fromChild |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
145 |
in |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
146 |
File.write (File.tmp_path (Path.basic "e_response")) thisLine; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
147 |
if thisLine = "" |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
148 |
then (TextIO.output (E_proof_file, "No proof output seen \n"); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
149 |
TextIO.closeOut E_proof_file; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
150 |
false) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
151 |
else if thisLine = "# TSTP exit status: Unsatisfiable\n" |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
152 |
then |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
153 |
startTransfer (start_E, end_E) |
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
154 |
(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
|
155 |
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
|
156 |
then |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
157 |
(TextIO.output (toParent, "Invalid\n"); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
158 |
TextIO.output (toParent, goalstring^"\n"); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
159 |
TextIO.flushOut toParent; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
160 |
TextIO.output (E_proof_file, thisLine); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
161 |
TextIO.closeOut E_proof_file; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
162 |
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
163 |
(* Attempt to prevent several signals from turning up simultaneously *) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
164 |
Posix.Process.sleep(Time.fromSeconds 1); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
165 |
true) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
166 |
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
|
167 |
then (*In fact, E distingishes "out of time" and "out of memory"*) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
168 |
(File.write (File.tmp_path (Path.basic "e_response")) thisLine; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
169 |
TextIO.output (toParent, "Failure\n"); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
170 |
TextIO.output (toParent, goalstring^"\n"); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
171 |
TextIO.flushOut toParent; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
172 |
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
173 |
TextIO.output (E_proof_file, "signalled parent\n"); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
174 |
TextIO.closeOut E_proof_file; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
175 |
(* Attempt to prevent several signals from turning up simultaneously *) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
176 |
Posix.Process.sleep(Time.fromSeconds 1); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
177 |
true) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
178 |
else |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
179 |
(TextIO.output (E_proof_file, thisLine); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
180 |
TextIO.flushOut E_proof_file; |
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
181 |
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
|
182 |
end |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
183 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
184 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
185 |
(**********************************************************************) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
186 |
(* 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
|
187 |
(* 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
|
188 |
(* 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
|
189 |
(**********************************************************************) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
190 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
191 |
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
|
192 |
clause_arr = |
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
193 |
SELECT_GOAL |
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17488
diff
changeset
|
194 |
(EVERY1 [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac, |
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
195 |
METAHYPS(fn negs => |
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
196 |
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
|
197 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
198 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
199 |
fun transferSpassInput (fromChild, toParent, ppid, goalstring, |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
200 |
currentString, 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 thisLine = TextIO.inputLine fromChild |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
202 |
in |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
203 |
if thisLine = "" (*end of file?*) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
204 |
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
|
205 |
raise EOF) |
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
206 |
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
|
207 |
then |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
208 |
let val proofextract = extract_proof (currentString^thisLine) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
209 |
in |
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
210 |
File.write (File.tmp_path (Path.basic"spass_extracted_prf")) proofextract; |
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
211 |
if !reconstruct |
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
212 |
then (spass_reconstruct_tac proofextract goalstring toParent ppid sg_num |
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
213 |
clause_arr thm; ()) |
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
214 |
else Recon_Transfer.spass_lemma_list proofextract goalstring |
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
215 |
toParent ppid clause_arr |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
216 |
end |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
217 |
else transferSpassInput (fromChild, toParent, ppid, goalstring, |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
218 |
(currentString^thisLine), thm, sg_num, clause_arr) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
219 |
end; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
220 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
221 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
222 |
(*********************************************************************************) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
223 |
(* 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
|
224 |
(* 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
|
225 |
(*********************************************************************************) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
226 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
227 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
228 |
fun startSpassTransfer (fromChild, toParent, ppid, goalstring,childCmd, |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
229 |
thm, sg_num,clause_arr) = |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
230 |
let val thisLine = TextIO.inputLine fromChild |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
231 |
in |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
232 |
if thisLine = "" then false |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
233 |
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
|
234 |
(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
|
235 |
("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
|
236 |
transferSpassInput (fromChild, toParent, ppid, goalstring,thisLine, |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
237 |
thm, sg_num,clause_arr); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
238 |
true) handle EOF => false |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
239 |
else startSpassTransfer (fromChild, toParent, ppid, goalstring, |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
240 |
childCmd, thm, sg_num,clause_arr) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
241 |
end |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
242 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
243 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
244 |
(*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
|
245 |
fun checkSpassProofFound (fromChild, toParent, ppid, goalstring, childCmd, |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
246 |
thm, sg_num, clause_arr) = |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
247 |
let val spass_proof_file = TextIO.openAppend |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
248 |
(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
|
249 |
val _ = File.write(File.tmp_path (Path.basic "spass_checking_prf")) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
250 |
("checking if proof found, thm is: "^(string_of_thm thm)) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
251 |
val thisLine = TextIO.inputLine fromChild |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
252 |
in |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
253 |
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
|
254 |
if thisLine = "" |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
255 |
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
|
256 |
TextIO.closeOut spass_proof_file; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
257 |
false) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
258 |
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
|
259 |
then |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
260 |
startSpassTransfer (fromChild, toParent, ppid, goalstring, |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
261 |
childCmd, thm, sg_num, clause_arr) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
262 |
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
|
263 |
then |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
264 |
(TextIO.output (spass_proof_file, thisLine); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
265 |
TextIO.closeOut spass_proof_file; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
266 |
TextIO.output (toParent, "Invalid\n"); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
267 |
TextIO.output (toParent, goalstring^"\n"); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
268 |
TextIO.flushOut toParent; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
269 |
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
270 |
(* Attempt to prevent several signals from turning up simultaneously *) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
271 |
Posix.Process.sleep(Time.fromSeconds 1); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
272 |
true) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
273 |
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
|
274 |
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
|
275 |
then |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
276 |
(TextIO.output (toParent, "Failure\n"); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
277 |
TextIO.output (toParent, goalstring^"\n"); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
278 |
TextIO.flushOut toParent; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
279 |
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
280 |
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
|
281 |
TextIO.closeOut spass_proof_file; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
282 |
(* Attempt to prevent several signals from turning up simultaneously *) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
283 |
Posix.Process.sleep(Time.fromSeconds 1); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
284 |
true) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
285 |
else |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
286 |
(TextIO.output (spass_proof_file, thisLine); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
287 |
TextIO.flushOut spass_proof_file; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
288 |
checkSpassProofFound (fromChild, toParent, ppid, goalstring, |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
289 |
childCmd, thm, sg_num, clause_arr)) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
290 |
end |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
291 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
diff
changeset
|
292 |
end; |