1 package cvc3; 2 3 public class Type extends Embedded { 4 // jni methods 5 private static native boolean jniIsAny(Object Type)6 jniIsAny(Object Type) throws Cvc3Exception; 7 private static native boolean jniIsArray(Object Type)8 jniIsArray(Object Type) throws Cvc3Exception; 9 private static native boolean jniIsBitvector(Object Type)10 jniIsBitvector(Object Type) throws Cvc3Exception; 11 private static native boolean jniIsBool(Object Type)12 jniIsBool(Object Type) throws Cvc3Exception; 13 private static native boolean jniIsDatatype(Object Type)14 jniIsDatatype(Object Type) throws Cvc3Exception; 15 private static native boolean jniIsFunction(Object Type)16 jniIsFunction(Object Type) throws Cvc3Exception; 17 private static native boolean jniIsNull(Object Type)18 jniIsNull(Object Type) throws Cvc3Exception; 19 private static native boolean jniIsSubtype(Object Type)20 jniIsSubtype(Object Type) throws Cvc3Exception; 21 22 private static native Object jniGetExpr(Object Type)23 jniGetExpr(Object Type) throws Cvc3Exception; 24 private static native int jniArity(Object Type)25 jniArity(Object Type) throws Cvc3Exception; 26 private static native Type jniGetChild(Object Type, int i)27 jniGetChild(Object Type, int i) throws Cvc3Exception; 28 29 private static native boolean jniEquals(Object Type1, Object Type2)30 jniEquals(Object Type1, Object Type2) throws Cvc3Exception; 31 private static native String jniToString(Object Type)32 jniToString(Object Type) throws Cvc3Exception; 33 jniConstr(Object expr)34 private static native Object jniConstr(Object expr) throws Cvc3Exception; 35 valueOf(Expr expr)36 public static Type valueOf(Expr expr) throws Cvc3Exception { 37 return new Type(jniConstr(expr.embedded()), expr.embeddedManager()); 38 } 39 40 /// Constructor 41 Type(Object Type, EmbeddedManager embeddedManager)42 public Type(Object Type, EmbeddedManager embeddedManager) { 43 super(Type, embeddedManager); 44 } 45 46 47 /// API (immutable) 48 isAny()49 public boolean isAny() throws Cvc3Exception { 50 return jniIsAny(embedded()); 51 } 52 isArray()53 public boolean isArray() throws Cvc3Exception { 54 return jniIsArray(embedded()); 55 } 56 isBitvector()57 public boolean isBitvector() throws Cvc3Exception { 58 return jniIsBitvector(embedded()); 59 } 60 isBoolean()61 public boolean isBoolean() throws Cvc3Exception { 62 return jniIsBool(embedded()); 63 } 64 isDatatype()65 public boolean isDatatype() throws Cvc3Exception { 66 return jniIsDatatype(embedded()); 67 } 68 isFunction()69 public boolean isFunction() throws Cvc3Exception { 70 return jniIsFunction(embedded()); 71 } 72 isNull()73 public boolean isNull() throws Cvc3Exception { 74 return jniIsNull(embedded()); 75 } 76 isSubtype()77 public boolean isSubtype() throws Cvc3Exception { 78 return jniIsSubtype(embedded()); 79 } 80 81 82 83 84 getExpr()85 public Expr getExpr() throws Cvc3Exception { 86 return new Expr(jniGetExpr(embedded()), embeddedManager()); 87 } 88 arity()89 public int arity() throws Cvc3Exception { 90 return jniArity(embedded()); 91 } 92 getChild(int i)93 public Type getChild(int i) throws Cvc3Exception { 94 assert(i >= 0 && i < arity()); 95 return new Type(jniGetChild(embedded(), i), embeddedManager()); 96 } 97 98 99 // Printing toString()100 public String toString() { 101 String result = ""; 102 try { 103 result = jniToString(embedded()); 104 } catch (Cvc3Exception e) { 105 System.out.println(e); 106 assert(false); 107 } 108 return result; 109 } 110 equals(Object o)111 public boolean equals(Object o) { 112 if (this == o) return true; 113 114 if (!(o instanceof Type)) return false; 115 boolean result = false; 116 try { 117 result = jniEquals(embedded(), ((Embedded)o).embedded()); 118 } catch (Cvc3Exception e) { 119 assert(false); 120 } 121 return result; 122 } 123 124 // must return the same hash code for two exprs if equals returns true 125 hashCode()126 public int hashCode() { 127 try { 128 return getExpr().hashCode(); 129 } catch (Cvc3Exception e) { 130 assert(false); 131 } 132 assert(false); 133 return 0; 134 } 135 } 136