001 /* Copyright 2000, 2001, Compaq Computer Corporation */
002
003 package escjava.prover;
004
005 import java.io.*;
006 import java.util.Enumeration;
007
008 import javafe.util.*;
009
010 /**
011 * <p> The interface to the Simplify theorem prover program using
012 * Strings to send and S-expressions to receive. </p>
013 *
014 * <p> Note that a Java application will not exit normally (i.e., when
015 * its <code>main()</code> method returns) until all subprocesses have
016 * finished. In particular, this implies that all
017 * <code>Simplify</code> instances must be closed before this can
018 * occur. Alternatively, a Java application can just call
019 * <code>java.lang.System.exit</code> to force an exit to occur
020 * without waiting for subprocesses. </p>
021 *
022 *
023 * <p> <strong>Warning:</strong> This class uses {@link
024 * SubProcess#readSExp()}, which does not implement the full grammer
025 * for SExps. See that routine for the exact limitations. </p>
026 *
027 * @see SExp
028 * @see SubProcess
029 * @see escjava.prover.CECEnum
030 */
031
032 public class Simplify
033 {
034 /**
035 * Our Simplify subprocess; no actions should be taken on this
036 * subprocess unless {@link #readySubProcess()} is called first.
037 */
038 //@ spec_public
039 private final /*@ non_null @*/ SubProcess P;
040
041 //@ invariant P == null ==> closed;
042
043 /**
044 * This variable holds the {@link CECEnum} that is currently using
045 * Simplify (there can be at most 1 such CECEnum), or
046 * <code>null</code> if there is no such CECEnum.
047 *
048 * <p> Simplify is available for use iff this is
049 * <code>null</code>. Use {@link #readySubProcess()} to make
050 * Simplify available. </p>
051 */
052 //@ spec_public
053 private CECEnum subProcessUser = null;
054
055 //@ public model boolean closed;
056 //@ represents closed <- (P == null);
057
058 // Multiplexing Simplify
059
060 /**
061 * Prepare Simplify for use.
062 *
063 * <p> Precondition: we are not closed. </p>
064 *
065 * <p> Ensures any {@link CECEnum} currently using Simplify
066 * finishes. </p>
067 */
068 //@ requires !closed;
069 //@ ensures subProcessUser != null ==> subProcessUser == null;
070 private void readySubProcess() {
071 if (subProcessUser != null) {
072 subProcessUser.finishUsingSimplify();
073 eatPrompt();
074 subProcessUser = null;
075 }
076 }
077
078
079 // Creation and destruction
080
081 /**
082 * Create a new invocation of Simplify as a sub-process.
083 *
084 * <p> The resulting invocation is initially open, but may be
085 * closed permanently with the {@link #close()} method. </p>
086 *
087 * <p> This constructor may result in a fatal error if any
088 * problems occur. </p>
089 */
090 //@ ensures !closed;
091 public Simplify() {
092 P = new SubProcess("Simplify",
093 new String[] {
094 java.lang.System.getProperty("simplify",
095 "/usr/local/escjava/bin/Simplify"),
096 "-noprune",
097 "-noplunge"}, // FIXME - make controllable
098 null);
099 eatPrompt();
100 }
101
102 /**
103 * Close us.
104 *
105 * <p> This destroys the associated subprocess. Afterwards, none
106 * of our methods should ever be called again. Likewise, no
107 * methods of any {@link Enumeration} we've returned should ever
108 * be called again. </p>
109 *
110 * <p> This method may result in a fatal error if any problems
111 * occur. Our subprocess is guaranteed to be destroyed afterwards,
112 * regardless of which exit is taken. </p>
113 */
114 //@ ensures closed;
115 public void close() {
116 P.close();
117 }
118
119
120 // Client operations
121
122 /**
123 * Send a single <code>String</code> command to Simplify.
124 *
125 * <p> A command is something that produces no output other than
126 * whitespace and a prompt. If any other output is produced, a
127 * fatal error will result. </p>
128 *
129 * <p> Precondition: we are not closed. </p>
130 *
131 * @param s the string containing the command to be sent to
132 * simplify.
133 */
134 //@ requires !closed;
135 public void sendCommand(/*@ non_null @*/ String s) {
136 readySubProcess();
137 P.resetInfo();
138
139 if (Info.on) {
140 Info.out("[calling Simplify with command '" + s + "']");
141 }
142
143 P.send(s);
144
145 eatPrompt();
146
147 Info.out("[Simplify: command done]");
148 }
149
150
151 /**
152 * Send a <code>String</code> containing zero-or-more commands to
153 * our Simplify subprocess.
154 *
155 * <p> A command is something that produces no output other than
156 * whitespace and a prompt. If any other output is produced, a
157 * fatal error will result. </p>
158 *
159 * <p> Precondition: we are not closed. </p>
160 *
161 * @param s the string containing the commands to be sent to
162 * simplify.
163 */
164 //@ requires !closed;
165 public void sendCommands(/*@ non_null @*/ String s) {
166 readySubProcess();
167 P.resetInfo();
168
169 if (Info.on) {
170 Info.out("[calling Simplify with commands '" + s + "']");
171 }
172
173 P.send(s);
174
175 // review kiniry 14 March 2004 - Why is this code block no
176 // longer necessary?
177
178 /*
179 // this is so we can be sure we have resynchronized the stream:
180 P.send(" (LBL |<resync>| (EQ |<A>| |<B>|))");
181
182 // eat resulting prompts from s:
183 while (P.peekChar() == '>')
184 eatPrompt();
185
186 // Eat output from synchronization expression:
187 Enumeration results = prove("");
188 try {
189 while (true) {
190 if (!results.hasMoreElements()) {
191 // get into exception handling code below
192 throw new SExpTypeError();
193 }
194 SimplifyOutput so = (SimplifyOutput)results.nextElement();
195 if (so.getKind() == SimplifyOutput.COUNTEREXAMPLE) {
196 SimplifyResult sr = (SimplifyResult)so;
197 if (sr.labels.at(0).getAtom().toString().equals("<resync>")) {
198 // all is well (any remaining results will be eaten
199 // with the next call to readySubProcess)
200 break;
201 }
202 }
203 }
204 } catch (Exception e) {
205 P.handleUnexpected("to have seen the label <resync>");
206 }
207 */
208
209 Info.out("[Simplify: commands done]");
210 }
211
212 /**
213 * Attempt to verify expression <code>exp</code>.
214 *
215 * <p> We always return an {@link Enumeration} of
216 * non-<code>null</code> {@link SimplifyOutput}s. If verifying
217 * <code>exp</code> succeeds, the resulting {@link Enumeration}
218 * will end with a {@link SimplifyOutput} of kind {@link
219 * SimplifyOutput#VALID}. </p>
220 *
221 * <p> Precondition: we are not closed, and <code>exp</code> is
222 * properly formed according to Simplify's rules. </p>
223 */
224 //@ requires !closed;
225 //@ ensures \result.elementType == \type(SimplifyOutput);
226 //@ ensures !\result.returnsNull;
227 public /*@ non_null @*/ Enumeration prove(/*@ non_null @*/ String exp) {
228 readySubProcess();
229 subProcessUser = new CECEnum(P, exp);
230 return subProcessUser;
231 }
232
233 /**
234 * Readies the simplify subprocess and sets its user to this, but
235 * send no commands.
236 */
237 //@ normal_behavior
238 //@ modifies subProcessUser;
239 //@ ensures subProcessUser != null;
240 public void startProve() {
241 readySubProcess();
242 subProcessUser = new CECEnum(P);
243 }
244
245 //@ ensures \result.elementType == \type(SimplifyOutput);
246 //@ ensures !\result.returnsNull;
247 public /*@ non_null @*/ Enumeration streamProve() {
248 P.ToStream().flush();
249 while (P.peekChar() == '>') {
250 eatPrompt();
251 }
252 return subProcessUser;
253 }
254
255 //@ ensures \result == null <==> closed;
256 public PrintStream subProcessToStream() {
257 return P.ToStream();
258 }
259
260
261 // Utility routines
262
263 /**
264 * Consume the prompt from our Simplify subprocess. If the next
265 * output characters are not exactly the prompt (possibly preceeded
266 * by some whitespace), a fatal error is reported.
267 *
268 * <p> Precondition: we are not closed. </p>
269 */
270 //@ requires !closed;
271 //@ requires P != null;
272 private void eatPrompt() {
273 P.eatWhitespace();
274 P.checkChar('>');
275 P.checkChar('\t');
276 }
277
278
279 // Test methods
280
281 /**
282 * A simple test routine
283 */
284 public static void main(String[] args) throws IOException {
285 Info.on = true; // Turn on verbose mode
286
287 Simplify S = new Simplify();
288
289 exhaust(S.prove("(EQ A B)"));
290
291 exhaust(S.prove("(EQ A A)"));
292
293 S.sendCommand("(BG_PUSH (EQ B A))");
294 exhaust(S.prove("(EQ A B)"));
295 S.sendCommand("(BG_POP)");
296
297 exhaust(S.prove("(EQ A B)"));
298
299 S.sendCommands("(BG_PUSH (EQ B A)) (BG_POP)");
300
301 // The following is not a command and thus should produce
302 // an error:
303 try {
304 S.sendCommand("(EQ A A)");
305 } finally {
306 S.close();
307 }
308 }
309
310 /**
311 * Force an {@link Enumeration} to compute all of its elements
312 */
313 static void exhaust(/*@ non_null @*/ Enumeration n) {
314 while (n.hasMoreElements())
315 n.nextElement();
316 }
317 }