    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package escjava.prover;
    004
    005    /**
    006     * Objects of this class represent possible normal outputs from Simplify.
    007     *
    008     * @see Simplify
    009     * @see escjava.prover.CECEnum
    010     * @see SExp
    011     */
    012
    013    public class SimplifyOutput
    014    {
    015        // Constants representing output types.
    016        public static final int VALID = 0;
    017        public static final int INVALID = VALID + 1;
    018        public static final int UNKNOWN = INVALID + 1;
    019
    020        public static final int COMMENT = UNKNOWN + 1;
    021
    022        public static final int COUNTEREXAMPLE = COMMENT + 1;
    023        public static final int EXCEEDED_PROVER_KILL_TIME = COUNTEREXAMPLE + 1;
    024        public static final int EXCEEDED_PROVER_KILL_ITER = EXCEEDED_PROVER_KILL_TIME + 1;
    025        public static final int REACHED_CC_LIMIT = EXCEEDED_PROVER_KILL_ITER + 1;
    026        public static final int EXCEEDED_PROVER_SUBGOAL_KILL_TIME = REACHED_CC_LIMIT + 1;
    027        public static final int EXCEEDED_PROVER_SUBGOAL_KILL_ITER = EXCEEDED_PROVER_SUBGOAL_KILL_TIME + 1;
    028
    029        public static final int WARNING_TRIGGERLESS_QUANT = EXCEEDED_PROVER_SUBGOAL_KILL_ITER + 1;
    030
    031        public static final int END = WARNING_TRIGGERLESS_QUANT + 1;
    032
    033        // What kind of output are we?
    034        int kind;
    035        //@ invariant VALID <= kind && kind < END;
    036
    037        //@ normal_behavior
    038        //@   ensures VALID <= \result && \result < END;
    039        public /*@ pure @*/ int getKind() {
    040            return kind;
    041        }
    042
    043        //@ normal_behavior
    044        //@   requires VALID <= kind && kind < END;
    045        //@   modifies this.kind;
    046        //@   ensures this.kind == kind;
    047        SimplifyOutput(int kind) {
    048            this.kind = kind;
    049        }
    050
    051        public /*@ non_null @*/ String toString() {
    052            return super.toString() + " kind=" + kind;
    053        }
    054    }