    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    }