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    }