1 package cvc3; 2 3 import java.util.*; 4 5 public class Rational extends Embedded { 6 // jni methods 7 private static native Object jniRational1(int n, int d)8 jniRational1(int n, int d) throws Cvc3Exception; 9 private static native Object jniRational2(String n, int base)10 jniRational2(String n, int base) throws Cvc3Exception; 11 private static native Object jniRational3(String n, String d, int base)12 jniRational3(String n, String d, int base) throws Cvc3Exception; 13 14 private static native boolean jniEquals(Object Rational1, Object Rational2)15 jniEquals(Object Rational1, Object Rational2) throws Cvc3Exception; 16 private static native String jniToString(Object Rational)17 jniToString(Object Rational) throws Cvc3Exception; 18 private static native int jniHash(Object Rational)19 jniHash(Object Rational) throws Cvc3Exception; 20 21 private static native boolean jniIsLe(Object Rational1, Object Rational2)22 jniIsLe(Object Rational1, Object Rational2) throws Cvc3Exception; 23 private static native boolean jniIsLt(Object Rational1, Object Rational2)24 jniIsLt(Object Rational1, Object Rational2) throws Cvc3Exception; 25 private static native boolean jniIsGe(Object Rational1, Object Rational2)26 jniIsGe(Object Rational1, Object Rational2) throws Cvc3Exception; 27 private static native boolean jniIsGt(Object Rational1, Object Rational2)28 jniIsGt(Object Rational1, Object Rational2) throws Cvc3Exception; 29 30 private static native Object jniPlus(Object Rational1, Object Rational2)31 jniPlus(Object Rational1, Object Rational2) throws Cvc3Exception; 32 private static native Object jniMinus(Object Rational1, Object Rational2)33 jniMinus(Object Rational1, Object Rational2) throws Cvc3Exception; 34 private static native Object jniMult(Object Rational1, Object Rational2)35 jniMult(Object Rational1, Object Rational2) throws Cvc3Exception; 36 private static native Object jniDivide(Object Rational1, Object Rational2)37 jniDivide(Object Rational1, Object Rational2) throws Cvc3Exception; 38 private static native Object jniMod(Object Rational1, Object Rational2)39 jniMod(Object Rational1, Object Rational2) throws Cvc3Exception; 40 41 42 private static native Object jniGetNumerator(Object Rational)43 jniGetNumerator(Object Rational) throws Cvc3Exception; 44 private static native Object jniGetDenominator(Object Rational)45 jniGetDenominator(Object Rational) throws Cvc3Exception; 46 private static native boolean jniIsInteger(Object Rational)47 jniIsInteger(Object Rational) throws Cvc3Exception; 48 private static native int jniGetInteger(Object Rational)49 jniGetInteger(Object Rational) throws Cvc3Exception; 50 51 52 private static native Object jniGcd(Object Rational1, Object Rational2)53 jniGcd(Object Rational1, Object Rational2) throws Cvc3Exception; 54 private static native Object jniLcm(Object Rational1, Object Rational2)55 jniLcm(Object Rational1, Object Rational2) throws Cvc3Exception; 56 private static native Object jniAbs(Object Rational)57 jniAbs(Object Rational) throws Cvc3Exception; 58 private static native Object jniFloor(Object Rational)59 jniFloor(Object Rational) throws Cvc3Exception; 60 private static native Object jniCeil(Object Rational)61 jniCeil(Object Rational) throws Cvc3Exception; 62 63 /// Constructor 64 Rational(Object Rational, EmbeddedManager embeddedManager)65 public Rational(Object Rational, EmbeddedManager embeddedManager) { 66 super(Rational, embeddedManager); 67 } 68 69 Rational(int n, EmbeddedManager embeddedManager)70 public Rational(int n, EmbeddedManager embeddedManager) throws Cvc3Exception { 71 this(jniRational1(n, 10), embeddedManager); 72 } 73 Rational(int n, int d, EmbeddedManager embeddedManager)74 public Rational(int n, int d, EmbeddedManager embeddedManager) throws Cvc3Exception { 75 this(jniRational1(n, d), embeddedManager); 76 } 77 Rational(String n, EmbeddedManager embeddedManager)78 public Rational(String n, EmbeddedManager embeddedManager) throws Cvc3Exception { 79 this(jniRational2(n, 10), embeddedManager); 80 } 81 Rational(String n, int base, EmbeddedManager embeddedManager)82 public Rational(String n, int base, EmbeddedManager embeddedManager) throws Cvc3Exception { 83 this(jniRational2(n, base), embeddedManager); 84 } 85 Rational(String n, String d, EmbeddedManager embeddedManager)86 public Rational(String n, String d, EmbeddedManager embeddedManager) throws Cvc3Exception { 87 this(jniRational3(n, d, 10), embeddedManager); 88 } 89 Rational(String n, String d, int base, EmbeddedManager embeddedManager)90 public Rational(String n, String d, int base, EmbeddedManager embeddedManager) throws Cvc3Exception { 91 this(jniRational3(n, d, base), embeddedManager); 92 } 93 94 95 96 /// API (immutable) 97 98 // 'Problem' with equals/hashCode: 99 // this is based on the wrapped c++ expressions. 100 // as a consequence two Expr objects are equal iff 101 // the wrapped expression is equal, 102 // and are indistinguishable for example in a HashMap. 103 equals(Object o)104 public boolean equals(Object o) { 105 if (this == o) return true; 106 107 if (!(o instanceof Rational)) return false; 108 boolean result = false; 109 try { 110 result = jniEquals(embedded(), ((Embedded)o).embedded()); 111 } catch (Cvc3Exception e) { 112 assert(false); 113 } 114 return result; 115 } 116 117 // must return the same hash code for two objects if equals returns true hashCode()118 public int hashCode() { 119 try { 120 return jniHash(embedded()); 121 } catch (Cvc3Exception e) { 122 assert(false); 123 } 124 assert(false); 125 return 0; 126 } 127 128 toString()129 public String toString() { 130 String result = ""; 131 try { 132 result = jniToString(embedded()); 133 } catch (Cvc3Exception e) { 134 assert(false); 135 } 136 return result; 137 } 138 139 isLt(Rational r)140 public boolean isLt(Rational r) throws Cvc3Exception { 141 return jniIsLt(embedded(), r.embedded()); 142 } 143 isLe(Rational r)144 public boolean isLe(Rational r) throws Cvc3Exception { 145 return jniIsLe(embedded(), r.embedded()); 146 } 147 isGt(Rational r)148 public boolean isGt(Rational r) throws Cvc3Exception { 149 return jniIsGt(embedded(), r.embedded()); 150 } 151 isGe(Rational r)152 public boolean isGe(Rational r) throws Cvc3Exception { 153 return jniIsGe(embedded(), r.embedded()); 154 } 155 156 157 plus(Rational r)158 public Rational plus(Rational r) throws Cvc3Exception { 159 return new Rational(jniPlus(embedded(), r.embedded()), embeddedManager()); 160 } 161 minus(Rational r)162 public Rational minus(Rational r) throws Cvc3Exception { 163 return new Rational(jniPlus(embedded(), r.embedded()), embeddedManager()); 164 } 165 mult(Rational r)166 public Rational mult(Rational r) throws Cvc3Exception { 167 return new Rational(jniPlus(embedded(), r.embedded()), embeddedManager()); 168 } 169 divide(Rational r)170 public Rational divide(Rational r) throws Cvc3Exception { 171 return new Rational(jniPlus(embedded(), r.embedded()), embeddedManager()); 172 } 173 mod(Rational r)174 public Rational mod(Rational r) throws Cvc3Exception { 175 return new Rational(jniPlus(embedded(), r.embedded()), embeddedManager()); 176 } 177 178 179 getNumerator()180 public Rational getNumerator() throws Cvc3Exception { 181 return new Rational(jniGetNumerator(embedded()), embeddedManager()); 182 } 183 getDenominator()184 public Rational getDenominator() throws Cvc3Exception { 185 return new Rational(jniGetDenominator(embedded()), embeddedManager()); 186 } 187 isInteger()188 public boolean isInteger() throws Cvc3Exception { 189 return jniIsInteger(embedded()); 190 } 191 getInteger()192 public int getInteger() throws Cvc3Exception { 193 assert(isInteger()); 194 return jniGetInteger(embedded()); 195 } 196 197 198 gcd(Rational r)199 public Rational gcd(Rational r) throws Cvc3Exception { 200 return new Rational(jniGcd(embedded(), r.embedded()), embeddedManager()); 201 } 202 lcm(Rational r)203 public Rational lcm(Rational r) throws Cvc3Exception { 204 return new Rational(jniLcm(embedded(), r.embedded()), embeddedManager()); 205 } 206 abs()207 public Rational abs() throws Cvc3Exception { 208 return new Rational(jniAbs(embedded()), embeddedManager()); 209 } 210 floor()211 public Rational floor() throws Cvc3Exception { 212 return new Rational(jniFloor(embedded()), embeddedManager()); 213 } 214 ceil()215 public Rational ceil() throws Cvc3Exception { 216 return new Rational(jniCeil(embedded()), embeddedManager()); 217 } 218 } 219