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 }