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