001    package escjava.prover;
002    
003    import java.util.Properties;
004    
005    public class ProverResponse
006    {
007        /**
008         * A singleton response code to indicate everything is fine.
009         */
010        public /*@ non_null @*/ static ProverResponse OK =
011            new ProverResponse();
012    
013        /**
014         * A singleton response code to indicate that something is seriously
015         * wrong with the corresponding call and/or the prover and a failure
016         * has taken place.  A response code of FAIL typically indicates a
017         * non-correctable situation.  The {@link #info} field should be
018         * consulted for additional information, and no further calls, but
019         * for {@link ProverInterface#stop_prover()} should be made.
020         */
021        public /*@ non_null @*/ static ProverResponse FAIL =
022            new ProverResponse();
023    
024        /**
025         * A singleton response code to indicate a positive response to the
026         * last command.
027         */
028        public /*@ non_null @*/ static ProverResponse YES =
029            new ProverResponse();
030    
031        /**
032         * A singleton response code to indicate a negative response to the
033         * last command.
034         */
035        public /*@ non_null @*/ static ProverResponse NO =
036            new ProverResponse();
037    
038        /**
039         * A singleton response code to indicate a counter-example is
040         * available.  The counter-example is contained in the {@link
041         * #formula} field of this response object.
042         */
043        public /*@ non_null @*/ static ProverResponse COUNTER_EXAMPLE =
044            new ProverResponse();
045    
046        /**
047         * A singleton response code to indicate a syntax error in the
048         * corresponding prover call.  The {@link #info} field should be
049         * consulted for additional information.
050         */
051        public /*@ non_null @*/ static ProverResponse SYNTAX_ERROR =
052            new ProverResponse();
053    
054        /**
055         * A singleton response code to indicate that some progress
056         * information is available from the prover.  The {@link #info}
057         * field should be consulted for additional information.
058         */
059        public /*@ non_null @*/ static ProverResponse PROGRESS_INFORMATION =
060            new ProverResponse();
061    
062        /**
063         * A singleton response code to indicate that the prover has timed
064         * out on the corresponding prover call.  The {@link #info} and/or
065         * {@link #formula} fields should be consulted for additional
066         * information.
067         */
068        public /*@ non_null @*/ static ProverResponse TIMEOUT =
069            new ProverResponse();
070    
071        /**
072         * A singleton response code to indicate an inconsistency warning
073         * from the prover for one or more of the previous {@link
074         * ProverInterface#declare_axiom(Formula)} and {@link
075         * ProverInterface#make_assumption(Formula)} calls.  The {@link
076         * #info} and/or {@link #formula} fields should be consulted for
077         * additional information.
078         */
079        public /*@ non_null @*/ static ProverResponse INCONSISTENCY_WARNING =
080            new ProverResponse();
081    
082        /**
083         * A formula.  Typically, this field is used to represent a
084         * counter-example in response to a call to {@link
085         * ProverInterface#is_valid(Formula)}.
086         */
087        public Formula formula;
088    
089        /**
090         * A set of properties.  Typically, this field is used to represent
091         * property/value pairs specific to reporting prover progress,
092         * state, resource utilization, etc.
093         */
094        public Properties info;
095    
096        /**
097         * A private constructor that is only to be used during static
098         * initialization.
099         */
100        protected ProverResponse() {
101            ; // skip
102        }
103    
104        // placeholder for factory for building ProverResponses
105        /*@   ensures \result == ProverResponse.OK ||
106          @   \result == ProverResponse.FAIL ||
107          @   \result == ProverResponse.YES ||
108          @   \result == ProverResponse.NO ||
109          @   \result == ProverResponse.COUNTER_EXAMPLE ||
110          @   \result == ProverResponse.SYNTAX_ERROR ||
111          @   \result == ProverResponse.PROGRESS_INFORMATION ||
112          @   \result == ProverResponse.TIMEOUT ||
113          @   \result == ProverResponse.INCONSISTENCY_WARNING;
114          @*/
115        static public /*@ pure non_null @*/ ProverResponse factory(int return_code) {
116    
117            /*
118             * Naive implementation, should be redefined in subclasses
119             */
120    
121            if( return_code >= 0 )
122                return ProverResponse.OK;
123            else
124                return ProverResponse.FAIL;
125    
126        }
127    }