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    }