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