author  paulson 
Thu, 18 Aug 2005 13:09:21 +0200  
changeset 17121  4c225f640b89 
parent 16805  fadf80952202 
child 17150  ce2a1aeb42aa 
permissions  rwrr 
15789
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15787
diff
changeset

1 
(* Title: Watcher.ML 
16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16100
diff
changeset

2 

15789
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15787
diff
changeset

3 
ID: $Id$ 
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15787
diff
changeset

4 
Author: Claire Quigley 
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15787
diff
changeset

5 
Copyright 2004 University of Cambridge 
15642  6 
*) 
7 

8 
(***************************************************************************) 

9 
(* The watcher process starts a resolution process when it receives a *) 

10 
(* message from Isabelle *) 

11 
(* Signals Isabelle, puts output of child into pipe to Isabelle, *) 

12 
(* and removes dead processes. Also possible to kill all the resolution *) 

13 
(* processes currently running. *) 

14 
(* Hardwired version of where to pick up the tptp files for the moment *) 

15 
(***************************************************************************) 

16 

17 
(*use "Proof_Transfer"; 

18 
use "VampireCommunication"; 

16089
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

19 
use "SpassCommunication";*) 
15642  20 
(*use "/homes/clq20/Jia_Code/TransStartIsar";*) 
21 

22 

23 
structure Watcher: WATCHER = 

24 
struct 

25 

16805  26 
open ReconPrelim Recon_Transfer 
27 

15642  28 
val goals_being_watched = ref 0; 
29 

16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

30 
(*****************************************) 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

31 
(* The result of calling createWatcher *) 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

32 
(*****************************************) 
15642  33 

16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

34 
datatype proc = PROC of { 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

35 
pid : Posix.Process.pid, 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

36 
instr : TextIO.instream, 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

37 
outstr : TextIO.outstream 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

38 
}; 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

39 

dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

40 
(*****************************************) 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

41 
(* The result of calling executeToList *) 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

42 
(*****************************************) 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

43 

dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

44 
datatype cmdproc = CMDPROC of { 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

45 
prover: string, (* Name of the resolution prover used, e.g. Vampire, SPASS *) 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

46 
cmd: string, (* The file containing the goal for res prover to prove *) 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

47 
thmstring: string, (* string representation of subgoal after negation, skolemization*) 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

48 
goalstring: string, (* string representation of subgoal*) 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

49 
proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc, 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

50 
instr : TextIO.instream, (* Input stream to child process *) 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

51 
outstr : TextIO.outstream (* Output stream from child process *) 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

52 
}; 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

53 

dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

54 
type signal = Posix.Signal.signal 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

55 
datatype exit_status = datatype Posix.Process.exit_status 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

56 

dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

57 
val fromStatus = Posix.Process.fromStatus 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

58 

dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

59 

dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

60 
fun reap(pid, instr, outstr) = 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

61 
let 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

62 
val u = TextIO.closeIn instr; 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

63 
val u = TextIO.closeOut outstr; 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

64 

dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

65 
val (_, status) = 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

66 
Posix.Process.waitpid(Posix.Process.W_CHILD pid, []) 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

67 
in 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

68 
status 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

69 
end 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

70 

dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

71 
fun fdReader (name : string, fd : Posix.IO.file_desc) = 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

72 
Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd }; 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

73 

dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

74 
fun fdWriter (name, fd) = 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

75 
Posix.IO.mkTextWriter { 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

76 
appendMode = false, 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

77 
initBlkMode = true, 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

78 
name = name, 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

79 
chunkSize=4096, 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

80 
fd = fd 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

81 
}; 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

82 

dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

83 
fun openOutFD (name, fd) = 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

84 
TextIO.mkOutstream ( 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

85 
TextIO.StreamIO.mkOutstream ( 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

86 
fdWriter (name, fd), IO.BLOCK_BUF)); 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

87 

dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

88 
fun openInFD (name, fd) = 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

89 
TextIO.mkInstream ( 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

90 
TextIO.StreamIO.mkInstream ( 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

91 
fdReader (name, fd), "")); 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

92 

dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

93 

dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

94 

dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

95 

dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

96 

dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

97 
fun killChild child_handle = Unix.reap child_handle 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

98 

dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

99 
fun childInfo (PROC{pid,instr,outstr }) = (pid,(instr,outstr)); 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

100 

dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

101 
fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr); 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

102 

dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

103 
fun cmdInStream (CMDPROC{instr,outstr,...}) = (instr); 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

104 

dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

105 
fun cmdchildInfo (CMDPROC{prover,cmd,thmstring,proc_handle,goalstring,instr,outstr}) = (prover,(cmd, (instr,outstr))); 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

106 

dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

107 
fun cmdchildHandle (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr}) = proc_handle; 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

108 

dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

109 
fun cmdProver (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr}) = (prover); 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

110 

dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

111 
fun cmdThm (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr}) = (thmstring); 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

112 

dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

113 
fun cmdGoal (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr}) = (goalstring); 
15642  114 

115 
fun sendOutput (outstr,str) = (TextIO.outputSubstr (outstr, (Substring.all str));TextIO.flushOut outstr); 

116 

117 
(********************************************************************************************) 

118 
(* takes a list of arguments and sends them individually to the watcher process by pipe *) 

119 
(********************************************************************************************) 

120 

121 
fun outputArgs (toWatcherStr, []) = () 

122 
 outputArgs (toWatcherStr, (x::xs)) = (TextIO.output (toWatcherStr, x); 

123 
TextIO.flushOut toWatcherStr; 

124 
outputArgs (toWatcherStr, xs)) 

125 

126 
(********************************************************************************) 

127 
(* gets individual args from instream and concatenates them into a list *) 

128 
(********************************************************************************) 

129 

130 
fun getArgs (fromParentStr, toParentStr,ys) = let 

131 
val thisLine = TextIO.input fromParentStr 

132 
in 

133 
((ys@[thisLine])) 

134 
end 

135 

136 
(********************************************************************************) 

137 
(* Remove the \n character from the end of each filename *) 

138 
(********************************************************************************) 

139 

16478  140 
(*fun getCmd cmdStr = let val backList = ((rev(explode cmdStr))) 
15642  141 
in 
142 
if (String.isPrefix "\n" (implode backList )) 

16089
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

143 
then (implode (rev ((tl backList)))) 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

144 
else cmdStr 
16478  145 
end*) 
15642  146 

147 
(********************************************************************************) 

148 
(* Send request to Watcher for a vampire to be called for filename in arg *) 

149 
(********************************************************************************) 

150 

151 
fun callResProver (toWatcherStr, arg) = (sendOutput (toWatcherStr, arg^"\n"); 

16089
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

152 
TextIO.flushOut toWatcherStr) 
15642  153 

154 
(*****************************************************************************************) 

16357  155 
(* Send request to Watcher for multiple provers to be called for filenames in arg *) 
156 
(* need to do the dfg stuff in the watcher, not here! send over the clasimp and stuff files too*) 

15642  157 
(*****************************************************************************************) 
158 

16357  159 

15642  160 
(* need to modify to send over hyps file too *) 
16475  161 
fun callResProvers (toWatcherStr, []) = 
162 
(sendOutput (toWatcherStr, "End of calls\n"); TextIO.flushOut toWatcherStr) 

163 
 callResProvers (toWatcherStr, 

164 
(prover,thmstring,goalstring, proverCmd,settings,clasimpfile, 

165 
axfile, hypsfile,probfile) :: args) = 

166 
let val _ = File.write (File.tmp_path (Path.basic "tog_comms")) 

167 
(prover^thmstring^goalstring^proverCmd^settings^ 

168 
clasimpfile^hypsfile^probfile) 

169 
in sendOutput (toWatcherStr, 

16675  170 
(prover^"$"^thmstring^"$"^goalstring^"$"^proverCmd^"$"^ 
171 
settings^"$"^clasimpfile^"$"^hypsfile^"$"^probfile^"\n")); 

16475  172 
goals_being_watched := (!goals_being_watched) + 1; 
173 
TextIO.flushOut toWatcherStr; 

174 
callResProvers (toWatcherStr,args) 

175 
end 

16357  176 

16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16100
diff
changeset

177 

15782  178 
(* 
15642  179 
fun callResProversStr (toWatcherStr, []) = "End of calls\n" 
180 

15782  181 
 callResProversStr (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,clasimpfile, axfile, hypsfile, probfile)::args) = 
182 
((prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^clasimpfile^"*"^axfile^"*"^hypsfile^"*"^probfile^"\n") 

15642  183 

15782  184 
*) 
15642  185 

186 
(**************************************************************) 

187 
(* Send message to watcher to kill currently running vampires *) 

188 
(**************************************************************) 

189 

190 
fun callSlayer (toWatcherStr) = (sendOutput (toWatcherStr, "Kill vampires\n"); 

191 
TextIO.flushOut toWatcherStr) 

192 

193 

194 

195 
(**************************************************************) 

196 
(* Remove \n token from a vampire goal filename and extract *) 

197 
(* prover, proverCmd, settings and file from input string *) 

198 
(**************************************************************) 

199 

200 

201 
fun takeUntil ch [] res = (res, []) 

202 
 takeUntil ch (x::xs) res = if x = ch 

203 
then 

204 
(res, xs) 

205 
else 

206 
takeUntil ch xs (res@[x]) 

207 

208 
fun getSettings [] settings = settings 

209 
 getSettings (xs) settings = let val (set, rest ) = takeUntil "%" xs [] 

210 
in 

211 
getSettings rest (settings@[(implode set)]) 

212 
end 

213 

16475  214 
fun separateFields str = 
215 
let val outfile = TextIO.openAppend(*("sep_field")*)(File.platform_path(File.tmp_path (Path.basic "sep_field"))) 

216 
val _ = TextIO.output (outfile,("In separateFields, str is: "^(implode str)^"\n\n") ) 

217 
val _ = TextIO.closeOut outfile 

16675  218 
val (prover, rest) = takeUntil "$" str [] 
16475  219 
val prover = implode prover 
16357  220 

16675  221 
val (thmstring, rest) = takeUntil "$" rest [] 
16475  222 
val thmstring = implode thmstring 
16357  223 

16675  224 
val (goalstring, rest) = takeUntil "$" rest [] 
16475  225 
val goalstring = implode goalstring 
16357  226 

16675  227 
val (proverCmd, rest ) = takeUntil "$" rest [] 
16475  228 
val proverCmd = implode proverCmd 
229 

16675  230 
val (settings, rest) = takeUntil "$" rest [] 
16475  231 
val settings = getSettings settings [] 
16357  232 

16675  233 
val (clasimpfile, rest ) = takeUntil "$" rest [] 
16475  234 
val clasimpfile = implode clasimpfile 
235 

16675  236 
val (hypsfile, rest ) = takeUntil "$" rest [] 
16475  237 
val hypsfile = implode hypsfile 
15642  238 

16675  239 
val (file, rest) = takeUntil "$" rest [] 
16475  240 
val file = implode file 
241 

242 
val _ = File.append (File.tmp_path (Path.basic "sep_comms")) 

243 
("Sep comms are: "^(implode str)^"**"^ 

16675  244 
prover^" thmstring: "^thmstring^"\n goalstr: "^goalstring^" \n provercmd: "^proverCmd^" \n clasimp "^clasimpfile^" \n hyps "^hypsfile^"\n prob "^file^"\n\n") 
16475  245 
in 
246 
(prover,thmstring,goalstring, proverCmd, settings, clasimpfile, hypsfile, file) 

247 
end 

248 

16357  249 

250 
(***********************************************************************************) 

251 
(* do tptp2x and cat to turn clasimpfile, hypsfile and probfile into one .dfg file *) 

252 
(***********************************************************************************) 

253 

254 
fun formatCmd (prover,thmstring,goalstring, proverCmd, settings, clasimpfile, hypsfile ,probfile) = 

16475  255 
let 
256 
(*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***) 

257 
val probID = List.last(explode probfile) 

258 
val wholefile = File.tmp_path (Path.basic ("ax_prob_" ^ probID)) 

259 

260 
(*** only include problem and clasimp for the moment, not sure 

261 
how to refer to hyps/local axioms just now ***) 

262 
val whole_prob_file = Unix.execute("/bin/cat", 

263 
[clasimpfile,(*axfile, hypsfile,*)probfile, ">", 

264 
File.platform_path wholefile]) 

265 

266 
val dfg_dir = File.tmp_path (Path.basic "dfg"); 

267 
val dfg_path = File.platform_path dfg_dir; 

268 

16561  269 
(*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***) 
270 
val probID = List.last(explode probfile) 

271 
val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID)) 

16478  272 

16561  273 
(*** only include problem and clasimp for the moment, not sure how to refer to ***) 
274 
(*** hyps/local axioms just now ***) 

275 
val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*axfile, hypsfile,*)probfile, ">", (File.platform_path wholefile)]) 

276 
(*** check if the directory exists and, if not, create it***) 

277 
val _ = 

278 
if !SpassComm.spass 

279 
then 

280 
if File.exists dfg_dir then warning("dfg dir exists") 

281 
else File.mkdir dfg_dir 

282 
else 

283 
warning("not converting to dfg") 

284 

285 
val _ = if !SpassComm.spass then 

17121  286 
system (ResLib.helper_path "TPTP2X_HOME" "tptp2X" ^ 
287 
" fdfg d " ^ dfg_path ^ " " ^ 

16561  288 
File.platform_path wholefile) 
289 
else 7 

290 
val newfile = if !SpassComm.spass 

291 
then 

292 
dfg_path^"/ax_prob"^"_"^(probID)^".dfg" 

16675  293 

16478  294 
else 
16561  295 
(File.platform_path wholefile) 
296 
val _ = File.append (File.tmp_path (Path.basic"thmstring_in_watcher")) 

297 
(thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^newfile^"\n") 

298 
in 

299 
(prover,thmstring,goalstring, proverCmd, settings,newfile) 

300 
end; 

16478  301 

16357  302 

303 

304 
(* remove \n from end of command and put back into tuple format *) 

305 

306 

16478  307 
(* val cmdStr = "spass*((ALL xa. (~ P x  P xa) & (~ P xa  P x)) & (P xa  (ALL x. P x)) & ((ALL x. ~ P x)  ~ P xb) [.])*(EX x. ALL y. P x = P y) > (EX x. P x) = (ALL y. P y)*/homes/clq20/bin/SPASS*DocProof*/local/scratch/clq20/27023/clasimp*/local/scratch/clq20/27023/hyps*/local/scratch/clq20/27023/prob_1\n" 
308 

309 
val cmdStr = "vampire*(length (rev xs) = length xs [.]) & (length (rev (a # xs)) ~= length (a # xs) [.])*length (rev []) = length []*/homes/jm318/Vampire8/vkernel*t 300%m 100000*/local/scratch/clq20/23523/clasimp*/local/scratch/clq20/23523/hyps*/local/scratch/clq20/23523/prob_1\n" 

310 
*) 

16357  311 

312 
(*FIX: are the two getCmd procs getting confused? Why do I have two anyway? *) 

15642  313 

16475  314 
fun getCmd cmdStr = 
315 
let val backList = rev(explode cmdStr) 

316 
val _ = File.append (File.tmp_path (Path.basic"cmdStr")) cmdStr 

317 
in 

318 
if (String.isPrefix "\n" (implode backList )) 

319 
then 

320 
let val newCmdStr = (rev(tl backList)) 

321 
in File.write (File.tmp_path (Path.basic"backlist")) 

322 
("about to call sepfields with "^(implode newCmdStr)); 

323 
formatCmd (separateFields newCmdStr) 

324 
end 

325 
else formatCmd (separateFields (explode cmdStr)) 

326 
end 

15642  327 

328 

329 
fun getProofCmd (a,b,c,d,e,f) = d 

330 

16357  331 

15642  332 
(**************************************************************) 
333 
(* Get commands from Isabelle *) 

334 
(**************************************************************) 

16357  335 
(* FIX: or perhaps do the tptp2x stuff here  so it's get commands and then format them, before passing them to spass *) 
15642  336 

337 
fun getCmds (toParentStr,fromParentStr, cmdList) = 

16475  338 
let val thisLine = TextIO.inputLine fromParentStr 
339 
val _ = File.append (File.tmp_path (Path.basic "parent_comms")) thisLine 

340 
in 

341 
if (thisLine = "End of calls\n") 

342 
then cmdList 

343 
else if (thisLine = "Kill children\n") 

344 
then 

345 
( TextIO.output (toParentStr,thisLine ); 

346 
TextIO.flushOut toParentStr; 

347 
(("","","","Kill children",[],"")::cmdList) 

348 
) 

349 
else let val thisCmd = getCmd (thisLine) 

350 
(*********************************************************) 

351 
(* thisCmd = (prover,thmstring,proverCmd, settings, file)*) 

352 
(* i.e. put back into tuple format *) 

353 
(*********************************************************) 

354 
in 

355 
(*TextIO.output (toParentStr, thisCmd); 

356 
TextIO.flushOut toParentStr;*) 

357 
getCmds (toParentStr,fromParentStr, (thisCmd::cmdList)) 

358 
end 

359 
end 

360 

16357  361 

15642  362 
(**************************************************************) 
363 
(* Get Iodescriptor for polling of an input stream *) 

364 
(**************************************************************) 

365 

366 

367 
fun getInIoDesc someInstr = 

368 
let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr) 

15702
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
15684
diff
changeset

369 
val _ = TextIO.output (TextIO.stdOut, buf) 
15642  370 
val ioDesc = 
371 
case rd 

372 
of TextPrimIO.RD{ioDesc = SOME iod, ...} =>SOME iod 

373 
 _ => NONE 

374 
in (* since getting the reader will have terminated the stream, we need 

375 
* to build a new stream. *) 

376 
TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf)); 

377 
ioDesc 

378 
end 

379 

380 

381 
(*************************************) 

382 
(* Set up a Watcher Process *) 

383 
(*************************************) 

384 

385 

386 

16061  387 
fun setupWatcher (thm,clause_arr, num_of_clauses) = 
388 
let 

389 
(** pipes for communication between parent and watcher **) 

390 
val p1 = Posix.IO.pipe () 

391 
val p2 = Posix.IO.pipe () 

392 
fun closep () = ( 

393 
Posix.IO.close (#outfd p1); 

394 
Posix.IO.close (#infd p1); 

395 
Posix.IO.close (#outfd p2); 

396 
Posix.IO.close (#infd p2) 

397 
) 

398 
(***********************************************************) 

399 
(****** fork a watcher process and get it set up and going *) 

400 
(***********************************************************) 

401 
fun startWatcher (procList) = 

402 
(case Posix.Process.fork() (***************************************) 

403 
of SOME pid => pid (* parent  i.e. main Isabelle process *) 

404 
(***************************************) 

405 

406 
(*************************) 

407 
 NONE => let (* child  i.e. watcher *) 

408 
val oldchildin = #infd p1 (*************************) 

409 
val fromParent = Posix.FileSys.wordToFD 0w0 

410 
val oldchildout = #outfd p2 

411 
val toParent = Posix.FileSys.wordToFD 0w1 

412 
val fromParentIOD = Posix.FileSys.fdToIOD fromParent 

413 
val fromParentStr = openInFD ("_exec_in_parent", fromParent) 

414 
val toParentStr = openOutFD ("_exec_out_parent", toParent) 

415 
val sign = sign_of_thm thm 

416 
val prems = prems_of thm 

417 
val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) 

418 
val _ = (warning ("subgoals forked to startWatcher: "^prems_string)); 

419 
(* tracing *) 

420 
(*val tenth_ax = fst( Array.sub(clause_arr, 1)) 

421 
val tenth_ax_thms = memo_find_clause (tenth_ax, clause_tab) 

422 
val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms) 

423 
val _ = (warning ("tenth axiom in array in watcher is: "^tenth_ax)) 

424 
val _ = (warning ("tenth axiom in table in watcher is: "^clause_str)) 

425 
val _ = (warning ("num_of_clauses in watcher is: "^(string_of_int (num_of_clauses))) ) 

426 
*) 

427 
(*val goalstr = string_of_thm (the_goal) 

16260  428 
val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "goal_in_watcher"))); 
16061  429 
val _ = TextIO.output (outfile,goalstr ) 
430 
val _ = TextIO.closeOut outfile*) 

431 
fun killChildren [] = () 

432 
 killChildren (child_handle::children) = (killChild child_handle; killChildren children) 

15642  433 

16061  434 

435 

436 
(*************************************************************) 

437 
(* take an instream and poll its underlying reader for input *) 

438 
(*************************************************************) 

15642  439 

16061  440 
fun pollParentInput () = 
16475  441 
let val pd = OS.IO.pollDesc (fromParentIOD) 
442 
in 

443 
if (isSome pd ) then 

444 
let val pd' = OS.IO.pollIn (valOf pd) 

445 
val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 

446 
val _ = File.append (File.tmp_path (Path.basic "parent_poll")) 

447 
("In parent_poll\n") 

448 
in 

449 
if null pdl 

450 
then 

451 
NONE 

452 
else if (OS.IO.isIn (hd pdl)) 

453 
then 

454 
(SOME ( getCmds (toParentStr, fromParentStr, []))) 

455 
else 

16061  456 
NONE 
16475  457 
end 
458 
else 

459 
NONE 

460 
end 

16061  461 

462 
fun pollChildInput (fromStr) = 

16478  463 

464 
let val _ = File.append (File.tmp_path (Path.basic "child_poll")) 

465 
("In child_poll\n") 

466 
val iod = getInIoDesc fromStr 

467 
in 

468 

469 

470 

16061  471 
if isSome iod 
472 
then 

473 
let val pd = OS.IO.pollDesc (valOf iod) 

474 
in 

475 
if (isSome pd ) then 

476 
let val pd' = OS.IO.pollIn (valOf pd) 

16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16100
diff
changeset

477 
val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
16478  478 

16061  479 
in 
480 
if null pdl 

481 
then 

16478  482 
( File.append (File.tmp_path (Path.basic "child_poll_res")) 
483 
("Null pdl \n");NONE) 

16061  484 
else if (OS.IO.isIn (hd pdl)) 
485 
then 

16478  486 
(let val inval = (TextIO.inputLine fromStr) 
487 
val _ = File.append (File.tmp_path (Path.basic "child_poll_res")) (inval^"\n") 

488 
in 

489 
SOME inval 

490 
end) 

16061  491 
else 
16478  492 
( File.append (File.tmp_path (Path.basic "child_poll_res")) 
493 
("Null pdl \n");NONE) 

16061  494 
end 
495 
else 

496 
NONE 

497 
end 

498 
else 

499 
NONE 

16475  500 
end 
15642  501 

502 

16061  503 
(****************************************************************************) 
504 
(* Check all vampire processes currently running for output *) 

505 
(****************************************************************************) 

506 
(*********************************) 

507 
fun checkChildren ([], toParentStr) = [] (*** no children to check ********) 

508 
(*********************************) 

509 
 checkChildren ((childProc::otherChildren), toParentStr) = 

16357  510 
let val _ = File.append (File.tmp_path (Path.basic "child_check")) 
511 
("In check child, length of queue:"^(string_of_int (length (childProc::otherChildren)))^"\n") 

512 
val (childInput,childOutput) = cmdstreamsOf childProc 

16061  513 
val child_handle= cmdchildHandle childProc 
514 
(* childCmd is the .dfg file that the problem is in *) 

515 
val childCmd = fst(snd (cmdchildInfo childProc)) 

16357  516 
val _ = File.append (File.tmp_path (Path.basic "child_command")) 
517 
(childCmd^"\n") 

16061  518 
(* now get the number of the subgoal from the filename *) 
16520  519 
val sg_num = if (!SpassComm.spass ) 
520 
then 

521 
int_of_string(ReconOrderClauses.get_nth 5 (rev(explode childCmd))) 

522 
else 

523 
int_of_string(hd (rev(explode childCmd))) 

524 

16061  525 
val childIncoming = pollChildInput childInput 
16357  526 
val _ = File.append (File.tmp_path (Path.basic "child_check_polled")) 
527 
("finished polling child \n") 

16061  528 
val parentID = Posix.ProcEnv.getppid() 
529 
val prover = cmdProver childProc 

530 
val thmstring = cmdThm childProc 

531 
val sign = sign_of_thm thm 

532 
val prems = prems_of thm 

533 
val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) 

16100  534 
val _ = warning("subgoals forked to checkChildren: "^prems_string) 
535 
val goalstring = cmdGoal childProc 

16357  536 
val _ = File.append (File.tmp_path (Path.basic "child_comms")) 
537 
(prover^thmstring^goalstring^childCmd^"\n") 

16061  538 
in 
539 
if (isSome childIncoming) 

540 
then 

541 
(* check here for prover label on child*) 

16100  542 
let val _ = File.write (File.tmp_path (Path.basic "child_incoming")) ("subgoals forked to checkChildren: "^prems_string^prover^thmstring^goalstring^childCmd) 
16478  543 
val childDone = (case prover of 
544 
"vampire" => (VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) ) 

545 
"spass" => (SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) ) ) 

16061  546 
in 
547 
if childDone (**********************************************) 

548 
then (* child has found a proof and transferred it *) 

549 
(**********************************************) 

15642  550 

16061  551 
(**********************************************) 
552 
(* Remove this child and go on to check others*) 

553 
(**********************************************) 

554 
( Unix.reap child_handle; 

555 
checkChildren(otherChildren, toParentStr)) 

556 
else 

557 
(**********************************************) 

558 
(* Keep this child and go on to check others *) 

559 
(**********************************************) 

15642  560 

16061  561 
(childProc::(checkChildren (otherChildren, toParentStr))) 
562 
end 

563 
else 

16100  564 
(File.append (File.tmp_path (Path.basic "child_incoming")) "No child output "; 
565 
childProc::(checkChildren (otherChildren, toParentStr))) 

16061  566 
end 
15642  567 

16061  568 

569 
(********************************************************************) 

570 
(* call resolution processes *) 

571 
(* settings should be a list of strings *) 

16520  572 
(* e.g. ["t 300", "m 100000"] (TextIO.input instr)^ *) 
16061  573 
(* takes list of (string, string, string list, string)list proclist *) 
574 
(********************************************************************) 

15642  575 

16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

576 

16061  577 
(*** add subgoal id num to this *) 
578 
fun execCmds [] procList = procList 

16561  579 
 execCmds ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList = let val _ = File.append (File.tmp_path (Path.basic "pre_exec_child")) ("\nAbout to execute command for goal:\n"^goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now())))) 
16357  580 
in 
581 
if (prover = "spass") 

16561  582 
then 
583 
let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = 

584 
(Unix.execute(proverCmd, (["FullRed=0"]@settings@[file]))) 

585 
val (instr, outstr) = Unix.streamsOf childhandle 

586 
val newProcList = (((CMDPROC{ 

587 
prover = prover, 

588 
cmd = file, 

589 
thmstring = thmstring, 

590 
goalstring = goalstring, 

591 
proc_handle = childhandle, 

592 
instr = instr, 

593 
outstr = outstr })::procList)) 

594 
val _ = File.append (File.tmp_path (Path.basic "exec_child")) 

595 
("\nexecuting command for goal:\n"^ 

596 
goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now())))) 

597 
in 

598 
Posix.Process.sleep (Time.fromSeconds 1);execCmds cmds newProcList 

599 
end 

600 
else 

601 
let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = 

602 
(Unix.execute(proverCmd, (settings@[file]))) 

603 
val (instr, outstr) = Unix.streamsOf childhandle 

604 

605 
val newProcList = (((CMDPROC{ 

606 
prover = prover, 

607 
cmd = file, 

608 
thmstring = thmstring, 

609 
goalstring = goalstring, 

610 
proc_handle = childhandle, 

611 
instr = instr, 

612 
outstr = outstr })::procList)) 

613 

614 
val _ = File.append (File.tmp_path (Path.basic "exec_child")) ("executing command for goal:\n"^goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now())))) 

615 
in 

616 
Posix.Process.sleep (Time.fromSeconds 1); execCmds cmds newProcList 

617 
end 

16357  618 
end 
15642  619 

16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

620 

16061  621 
(****************************************) 
622 
(* call resolution processes remotely *) 

623 
(* settings should be a list of strings *) 

624 
(* e.g. ["t 300", "m 100000"] *) 

625 
(****************************************) 

626 

627 
(* fun execRemoteCmds [] procList = procList 

628 
 execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList = 

629 
let val newProcList = mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"t", "shep"]@[proverCmd]@settings@[file]), procList) 

630 
in 

631 
execRemoteCmds cmds newProcList 

632 
end 

16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

633 
*) 
15642  634 

16061  635 
fun printList (outStr, []) = () 
636 
 printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs)) 

15642  637 

638 

16061  639 
(**********************************************) 
640 
(* Watcher Loop *) 

641 
(**********************************************) 

642 

15642  643 

644 

645 

16061  646 
fun keepWatching (toParentStr, fromParentStr,procList) = 
647 
let fun loop (procList) = 

648 
( 

649 
let val cmdsFromIsa = pollParentInput () 

650 
fun killchildHandler (n:int) = (TextIO.output(toParentStr, "Killing child proof processes!\n"); 

651 
TextIO.flushOut toParentStr; 

652 
killChildren (map (cmdchildHandle) procList); 

653 
()) 

654 

655 
in 

656 
(*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*) 

657 
(**********************************) 

658 
if (isSome cmdsFromIsa) then (* deal with input from Isabelle *) 

659 
( (**********************************) 

660 
if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" ) 

661 
then 

662 
( 

663 
let val child_handles = map cmdchildHandle procList 

664 
in 

665 
killChildren child_handles; 

666 
(*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*) loop ([]) 

667 
end 

668 

669 
) 

670 
else 

671 
( 

672 
if ((length procList)<10) (********************) 

673 
then (* Execute locally *) 

674 
( (********************) 

675 
let 

676 
val newProcList = execCmds (valOf cmdsFromIsa) procList 

677 
val parentID = Posix.ProcEnv.getppid() 

16357  678 
val _ = (File.append (File.tmp_path (Path.basic "prekeep_watch")) "Just execed a child\n ") 
16061  679 
val newProcList' =checkChildren (newProcList, toParentStr) 
16357  680 

681 
val _ = warning("off to keep watching...") 

682 
val _ = (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching...\n ") 

16061  683 
in 
684 
(*Posix.Process.sleep (Time.fromSeconds 1);*) 

685 
loop (newProcList') 

686 
end 

687 
) 

688 
else (*********************************) 

689 
(* Execute remotely *) 

690 
(* (actually not remote for now )*) 

691 
( (*********************************) 

692 
let 

693 
val newProcList = execCmds (valOf cmdsFromIsa) procList 

694 
val parentID = Posix.ProcEnv.getppid() 

695 
val newProcList' =checkChildren (newProcList, toParentStr) 

696 
in 

697 
(*Posix.Process.sleep (Time.fromSeconds 1);*) 

698 
loop (newProcList') 

699 
end 

700 
) 

15642  701 

702 

703 

16061  704 
) 
705 
) (******************************) 

706 
else (* No new input from Isabelle *) 

707 
(******************************) 

708 
( let val newProcList = checkChildren ((procList), toParentStr) 

709 
in 

16357  710 
(*Posix.Process.sleep (Time.fromSeconds 1);*) 
711 
(File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching.2..\n "); 

16061  712 
loop (newProcList) 
713 
end 

714 

715 
) 

716 
end) 

717 
in 

718 
loop (procList) 

719 
end 

720 

721 

722 
in 

723 
(***************************) 

724 
(*** Sort out pipes ********) 

725 
(***************************) 

15642  726 

16061  727 
Posix.IO.close (#outfd p1); 
728 
Posix.IO.close (#infd p2); 

729 
Posix.IO.dup2{old = oldchildin, new = fromParent}; 

730 
Posix.IO.close oldchildin; 

731 
Posix.IO.dup2{old = oldchildout, new = toParent}; 

732 
Posix.IO.close oldchildout; 

15642  733 

16061  734 
(***************************) 
735 
(* start the watcher loop *) 

736 
(***************************) 

737 
keepWatching (toParentStr, fromParentStr, procList); 

15642  738 

739 

16061  740 
(****************************************************************************) 
741 
(* fake return value  actually want the watcher to loop until killed *) 

742 
(****************************************************************************) 

743 
Posix.Process.wordToPid 0w0 

744 

745 
end); 

746 
(* end case *) 

15642  747 

748 

16061  749 
val _ = TextIO.flushOut TextIO.stdOut 
15642  750 

16061  751 
(*******************************) 
752 
(*** set watcher going ********) 

753 
(*******************************) 

15642  754 

16061  755 
val procList = [] 
756 
val pid = startWatcher (procList) 

757 
(**************************************************) 

758 
(* communication streams to watcher *) 

759 
(**************************************************) 

15642  760 

16061  761 
val instr = openInFD ("_exec_in", #infd p2) 
762 
val outstr = openOutFD ("_exec_out", #outfd p1) 

763 

764 
in 

765 
(*******************************) 

766 
(* close the childside fds *) 

767 
(*******************************) 

768 
Posix.IO.close (#outfd p2); 

769 
Posix.IO.close (#infd p1); 

770 
(* set the fds close on exec *) 

771 
Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); 

772 
Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); 

773 

774 
(*******************************) 

775 
(* return value *) 

776 
(*******************************) 

777 
PROC{pid = pid, 

778 
instr = instr, 

779 
outstr = outstr 

780 
} 

781 
end; 

15642  782 

783 

784 

785 
(**********************************************************) 

786 
(* Start a watcher and set up signal handlers *) 

787 
(**********************************************************) 

16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

788 

dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

789 
fun killWatcher pid= Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill); 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

790 

dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

791 
fun reapWatcher(pid, instr, outstr) = 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

792 
let 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

793 
val u = TextIO.closeIn instr; 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

794 
val u = TextIO.closeOut outstr; 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

795 

dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

796 
val (_, status) = 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

797 
Posix.Process.waitpid(Posix.Process.W_CHILD pid, []) 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

798 
in 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

799 
status 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

800 
end 
15642  801 

16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16100
diff
changeset

802 

16520  803 

804 
fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) = let val mychild = childInfo (setupWatcher(thm,clause_arr, num_of_clauses)) 

805 
val streams =snd mychild 

806 
val childin = fst streams 

807 
val childout = snd streams 

808 
val childpid = fst mychild 

809 
val sign = sign_of_thm thm 

810 
val prems = prems_of thm 

811 
val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) 

812 
val _ = (warning ("subgoals forked to createWatcher: "^prems_string)); 

813 
fun vampire_proofHandler (n) = 

814 
(Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); 

815 
VampComm.getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361"));() ) 

816 

817 

818 
fun spass_proofHandler (n) = ( 

16548
aa36ae6b955e
Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
quigley
parents:
16520
diff
changeset

819 
let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal1"))); 
16520  820 
val _ = TextIO.output (outfile, ("In signal handler now\n")) 
821 
val _ = TextIO.closeOut outfile 

822 
val (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin 

823 
val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal"))); 

824 

825 
val _ = TextIO.output (outfile, ("In signal handler "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched)))) 

826 
val _ = TextIO.closeOut outfile 

827 
in (* if a proof has been found and sent back as a reconstruction proof *) 

828 
if ( (substring (reconstr, 0,1))= "[") 

829 
then 

15642  830 

16520  831 
( 
832 
Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); 

833 
Recon_Transfer.apply_res_thm reconstr goalstring; 

834 
Pretty.writeln(Pretty.str (oct_char "361")); 

835 

836 
goals_being_watched := ((!goals_being_watched)  1); 

837 

838 
if ((!goals_being_watched) = 0) 

839 
then 

840 
(let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_found"))); 

841 
val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")) 

842 
val _ = TextIO.closeOut outfile 

843 
in 

844 
killWatcher (childpid); reapWatcher (childpid,childin, childout); () 

845 
end) 

846 
else 

847 
() 

848 
) 

16767  849 
(* if there's no proof, but a message from Spass *) 
850 
else if ((substring (reconstr, 0,5))= "SPASS") 

851 
then 

16520  852 
( 
853 
goals_being_watched := (!goals_being_watched) 1; 

854 
Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); 

855 
Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring)^reconstr)); 

856 
Pretty.writeln(Pretty.str (oct_char "361")); 

857 
if (!goals_being_watched = 0) 

858 
then 

859 
(let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp"))); 

860 
val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")) 

861 
val _ = TextIO.closeOut outfile 

862 
in 

863 
killWatcher (childpid); reapWatcher (childpid,childin, childout); () 

864 
end ) 

865 
else 

866 
() 

16767  867 
) 
868 
(* print out a list of rules used from clasimpset*) 

869 
else if ((substring (reconstr, 0,5))= "Rules") 

870 
then 

871 
( 

872 
goals_being_watched := (!goals_being_watched) 1; 

873 
Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); 

874 
Pretty.writeln(Pretty.str (goalstring^reconstr)); 

875 
Pretty.writeln(Pretty.str (oct_char "361")); 

876 
if (!goals_being_watched = 0) 

877 
then 

878 
(let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp"))); 

879 
val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")) 

880 
val _ = TextIO.closeOut outfile 

881 
in 

882 
killWatcher (childpid); reapWatcher (childpid,childin, childout);() 

883 
end ) 

884 
else 

885 
() 

886 
) 

887 

888 
(* if proof translation failed *) 

889 
else if ((substring (reconstr, 0,5)) = "Proof") 

890 
then 

891 
( 

892 
goals_being_watched := (!goals_being_watched) 1; 

893 
Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); 

894 
Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr))); 

895 
Pretty.writeln(Pretty.str (oct_char "361")); 

896 
if (!goals_being_watched = 0) 

897 
then 

898 
(let val outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp"))); 

899 
val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")) 

900 
val _ = TextIO.closeOut outfile 

901 
in 

902 
killWatcher (childpid); reapWatcher (childpid,childin, childout); () 

903 
end ) 

904 
else 

905 
( ) 

906 
) 

907 

908 
else if ((substring (reconstr, 0,1)) = "%") 

909 
then 

910 
( 

911 
goals_being_watched := (!goals_being_watched) 1; 

912 
Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); 

913 
Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr))); 

914 
Pretty.writeln(Pretty.str (oct_char "361")); 

915 
if (!goals_being_watched = 0) 

916 
then 

917 
(let val outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp"))); 

918 
val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")) 

919 
val _ = TextIO.closeOut outfile 

920 
in 

921 
killWatcher (childpid); reapWatcher (childpid,childin, childout); () 

922 
end ) 

923 
else 

924 
( ) 

925 
) 

926 

927 

928 
else (* add something here ?*) 

929 
( 

930 
goals_being_watched := (!goals_being_watched) 1; 

931 
Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); 

932 
Pretty.writeln(Pretty.str ("Ran out of options in handler")); 

933 
Pretty.writeln(Pretty.str (oct_char "361")); 

934 
if (!goals_being_watched = 0) 

935 
then 

936 
(let val outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp"))); 

937 
val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")) 

938 
val _ = TextIO.closeOut outfile 

939 
in 

940 
killWatcher (childpid); reapWatcher (childpid,childin, childout); () 

941 
end ) 

942 
else 

943 
( ) 

944 
) 

945 

946 

16520  947 

948 
end) 

949 

950 

951 

952 
in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler); 

953 
IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler); 

954 
(childin, childout, childpid) 

955 

16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16100
diff
changeset

956 

15642  957 

16100  958 
end 
15642  959 

960 

961 

962 

963 

964 
end (* structure Watcher *) 