00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00029
00030
00031
00032 #ifdef RATIONAL_NATIVE
00033
00034 #include "compat_hash_set.h"
00035 #include "rational.h"
00036
00037 #include <stdlib.h>
00038 #include <errno.h>
00039 #include <sstream>
00040
00041 #define OVERFLOW_MSG "\nThis is NOT a bug, but an explicit feature to preserve soundness\nwhen CVC Lite uses native computer arithmetic (finite precision). To\navoid this type of errors, please recompile CVC Lite with GMP library."
00042
00043 namespace CVCL {
00044
00045 using namespace std;
00046
00047
00048 static long int plus(long int x, long int y) {
00049 long int res = x+y;
00050 FatalAssert(((x > 0) != (y > 0)) || ((x > 0) == (res > 0)),
00051 "plus(x,y): arithmetic overflow" OVERFLOW_MSG);
00052 return res;
00053 }
00054
00055
00056 static long int uminus(long int x) {
00057 FatalAssert(x == 0 || x != -x, "uminus(x): arithmetic overflow"
00058 OVERFLOW_MSG);
00059 return -x;
00060 }
00061
00062
00063 static long int mult(long int x, long int y) {
00064 long int res = x*y;
00065 FatalAssert(x==0 || res/x == y, "mult(x,y): arithmetic overflow"
00066 OVERFLOW_MSG);
00067 return res;
00068 }
00069
00070
00071 static long int gcd(long int n1, long int n2) {
00072 DebugAssert(n1!=0 && n2!=0,
00073 "gcd("+int2string(n1)+", "+int2string(n2)+"): bad args");
00074
00075 if(n1 < 0) n1 = uminus(n1);
00076 if(n2 < 0) n2 = uminus(n2);
00077
00078 if (n1 < n2) {
00079 long int tmp = n1;
00080 n1 = n2;
00081 n2 = tmp;
00082 }
00083
00084
00085 long int r = n1 % n2;
00086 if (!r)
00087 return n2;
00088
00089 return gcd(n2, r);
00090 }
00091
00092
00093 static long int lcm(long int n1, long int n2) {
00094 long int g = gcd(n1,n2);
00095 return mult(n1/g, n2);
00096 }
00097
00098
00099 class Rational::Impl {
00100 long int d_num;
00101 long int d_denom;
00102
00103 void canonicalize();
00104 public:
00105
00106 Impl(): d_num(0), d_denom(1) { }
00107
00108 Impl(const Impl &x) : d_num(x.d_num), d_denom(x.d_denom) { }
00109
00110 Impl(long int n, long int d): d_num(n), d_denom(d) { canonicalize(); }
00111
00112 Impl(const string &n, int base);
00113
00114 Impl(const string &n, const string& d, int base);
00115
00116 virtual ~Impl() { }
00117
00118 long int getNum() const { return d_num; }
00119
00120 long int getDen() const { return d_denom; }
00121
00122
00123 Impl operator-() const;
00124
00125
00126 friend bool operator==(const Impl& x, const Impl& y) {
00127 return (x.d_num == y.d_num && x.d_denom == y.d_denom);
00128 }
00129
00130 friend bool operator!=(const Impl& x, const Impl& y) {
00131 return (x.d_num != y.d_num || x.d_denom != y.d_denom);
00132 }
00133
00134
00135
00136
00137 friend bool operator<(const Impl& x, const Impl& y) {
00138 Impl diff(x-y);
00139 return diff.d_num < 0;
00140 }
00141
00142 friend bool operator<=(const Impl& x, const Impl& y) {
00143 return (x == y || x < y);
00144 }
00145
00146 friend bool operator>(const Impl& x, const Impl& y) {
00147 Impl diff(x-y);
00148 return diff.d_num > 0;
00149 }
00150
00151 friend bool operator>=(const Impl& x, const Impl& y) {
00152 return (x == y || x > y);
00153 }
00154
00155
00156
00157
00158 friend Impl operator+(const Impl& x, const Impl& y) {
00159 long int d1(x.getDen()), d2(y.getDen());
00160 long int f(lcm(d1,d2)), f1(f/d1), f2(f/d2);
00161 long int n = plus(mult(x.getNum(), f1), mult(y.getNum(), f2));
00162 return Impl(n, f);
00163 }
00164
00165 friend Impl operator-(const Impl& x, const Impl& y) {
00166 TRACE("rational", "operator-(", x, ", "+y.toString()+")");
00167 long int d1(x.getDen()), d2(y.getDen());
00168 long int f(lcm(d1,d2)), f1(f/d1), f2(f/d2);
00169 long int n = plus(mult(x.getNum(), f1), uminus(mult(y.getNum(), f2)));
00170 Impl res(n, f);
00171 TRACE("rational", " => ", res, "");
00172 return res;
00173 }
00174
00175
00176
00177
00178
00179
00180 friend Impl operator*(const Impl& x, const Impl& y) {
00181 long int n1(x.getNum()), d1(x.getDen()), n2(y.getNum()), d2(y.getDen());
00182 long int g1(n1? gcd(n1,d2) : 1), g2(n2? gcd(n2,d1) : 1);
00183 long int n(mult(n1/g1, n2/g2)), d(mult(d1/g2, d2/g1));
00184 return Impl(n,d);
00185 }
00186
00187
00188
00189
00190
00191
00192 friend Impl operator/(const Impl& x, const Impl& y) {
00193 long int n1(x.getNum()), d1(x.getDen()), n2(y.getNum()), d2(y.getDen());
00194 DebugAssert(n2 != 0, "Impl::operator/: divisor is 0");
00195 long int g1(n1? gcd(n1,n2) : 1), g2(gcd(d1,d2));
00196 long int n(n1? mult(n1/g1, d2/g2) : 0), d(n1? mult(d1/g2, n2/g1) : 1);
00197 return Impl(n,d);
00198 }
00199
00200 friend Impl operator%(const Impl& x, const Impl& y) {
00201 DebugAssert(x.getDen() == 1 && y.getDen() == 1,
00202 "Impl % Impl: x and y must be integers");
00203 return Impl(x.getNum() % y.getNum(), 1);
00204 }
00205
00206
00207 string toString(int base = 10) const {
00208 ostringstream ss;
00209 DebugAssert(base == 10, "Rational::Impl::toString(): Sorry, base "
00210 +int2string(base)+
00211 " is not implemented for native machine arithmetic");
00212 ss << d_num;
00213 if(d_denom != 1)
00214 ss << "/" << d_denom;
00215 return(ss.str());
00216 }
00217
00218
00219 friend ostream& operator<<(ostream& os, const Rational::Impl& n) {
00220 return os << n.toString();
00221 }
00222
00223 };
00224
00225
00226 void Rational::Impl::canonicalize() {
00227 DebugAssert(d_denom != 0,
00228 "Rational::Impl::canonicalize: bad denominator: "
00229 +int2string(d_denom));
00230 if(d_num == 0) {
00231 d_denom = 1;
00232 } else {
00233 if(d_denom < 0) {
00234 d_num = uminus(d_num);
00235 d_denom = uminus(d_denom);
00236 }
00237 long int d = gcd(d_num, d_denom);
00238 if(d != 1) {
00239 d_num /= d;
00240 d_denom /= d;
00241 }
00242 }
00243 }
00244
00245
00246 Rational::Impl::Impl(const string &n, int base) {
00247 size_t i, iend;
00248 for(i=0,iend=n.size(); i<iend && n[i] != '/'; ++i);
00249 if(i<iend)
00250
00251 *this = Impl(n.substr(0,i-1), n.substr(i+1,iend-1), base);
00252 else
00253 *this = Impl(n, "1", base);
00254 canonicalize();
00255 }
00256
00257 Rational::Impl::Impl(const string &n, const string& d, int base) {
00258 d_num = strtol(n.c_str(), NULL, base);
00259 FatalAssert(d_num != LONG_MIN && d_num != LONG_MAX,
00260 "Rational::Impl(string, string): arithmetic overflow:"
00261 "n = "+n+", d="+d+", base="+int2string(base)
00262 +OVERFLOW_MSG);
00263 d_denom = strtol(d.c_str(), NULL, base);
00264 FatalAssert(d_denom != LONG_MIN && d_denom != LONG_MAX,
00265 "Rational::Impl(string, string): arithmetic overflow:"
00266 "n = "+n+", d="+d+", base="+int2string(base)
00267 +OVERFLOW_MSG);
00268 canonicalize();
00269 }
00270
00271 Rational::Impl Rational::Impl::operator-() const {
00272 return Impl(uminus(d_num), d_denom);
00273 }
00274
00275
00276
00277 Rational::Rational() : d_n(new Impl) {
00278 #ifdef _DEBUG_RATIONAL_
00279 int &num_created = getCreated();
00280 num_created++;
00281 printStats();
00282 #endif
00283 }
00284
00285 Rational::Rational(const Rational &n) : d_n(new Impl(*n.d_n)) {
00286 #ifdef _DEBUG_RATIONAL_
00287 int &num_created = getCreated();
00288 num_created++;
00289 printStats();
00290 #endif
00291 }
00292
00293
00294 Rational::Rational(const Impl& t): d_n(new Impl(t)) {
00295 #ifdef _DEBUG_RATIONAL_
00296 int &num_created = getCreated();
00297 num_created++;
00298 printStats();
00299 #endif
00300 }
00301 Rational::Rational(int n, int d): d_n(new Impl(n, d)) {
00302 #ifdef _DEBUG_RATIONAL_
00303 int &num_created = getCreated();
00304 num_created++;
00305 printStats();
00306 #endif
00307 }
00308
00309 Rational::Rational(const char* n, int base)
00310 : d_n(new Impl(string(n), base)) {
00311 #ifdef _DEBUG_RATIONAL_
00312 int &num_created = getCreated();
00313 num_created++;
00314 printStats();
00315 #endif
00316 }
00317 Rational::Rational(const string& n, int base)
00318 : d_n(new Impl(n, base)) {
00319 #ifdef _DEBUG_RATIONAL_
00320 int &num_created = getCreated();
00321 num_created++;
00322 printStats();
00323 #endif
00324 }
00325 Rational::Rational(const char* n, const char* d, int base)
00326 : d_n(new Impl(string(n), string(d), base)) {
00327 #ifdef _DEBUG_RATIONAL_
00328 int &num_created = getCreated();
00329 num_created++;
00330 printStats();
00331 #endif
00332 }
00333 Rational::Rational(const string& n, const string& d, int base)
00334 : d_n(new Impl(n, d, base)) {
00335 #ifdef _DEBUG_RATIONAL_
00336 int &num_created = getCreated();
00337 num_created++;
00338 printStats();
00339 #endif
00340 }
00341
00342 Rational::~Rational() {
00343 delete d_n;
00344 #ifdef _DEBUG_RATIONAL_
00345 int &num_deleted = getDeleted();
00346 num_deleted++;
00347 printStats();
00348 #endif
00349 }
00350
00351
00352 Rational Rational::getNumerator() const
00353 { return Rational(Impl(d_n->getNum(), 1)); }
00354 Rational Rational::getDenominator() const
00355 { return Rational(Impl(d_n->getDen(), 1)); }
00356
00357 bool Rational::isInteger() const { return 1 == d_n->getDen(); }
00358
00359
00360 Rational& Rational::operator=(const Rational& n) {
00361 if(this == &n) return *this;
00362 delete d_n;
00363 d_n = new Impl(*n.d_n);
00364 return *this;
00365 }
00366
00367 ostream &operator<<(ostream &os, const Rational &n) {
00368 return(os << n.toString());
00369 }
00370
00371
00372
00373
00374 static void checkInt(const Rational& n, const string& funName) {
00375 DebugAssert(n.isInteger(),
00376 ("CVCL::Rational::" + funName
00377 + ": argument is not an integer: " + n.toString()).c_str());
00378 }
00379
00380
00381
00382
00383
00384 Rational gcd(const Rational &x, const Rational &y) {
00385 checkInt(x, "gcd(*x*,y)");
00386 checkInt(y, "gcd(x,*y*)");
00387 return Rational(Rational::Impl(gcd(x.d_n->getNum(), y.d_n->getNum()), 1));
00388 }
00389
00390 Rational gcd(const vector<Rational> &v) {
00391 long int g(1);
00392 if(v.size() > 0) {
00393 checkInt(v[0], "gcd(vector<Rational>[0])");
00394 g = v[0].d_n->getNum();
00395 }
00396 for(size_t i=1; i<v.size(); i++) {
00397 checkInt(v[i], "gcd(vector<Rational>)");
00398 if(g == 0) g = v[i].d_n->getNum();
00399 else if(v[i].d_n->getNum() != 0)
00400 g = gcd(g, v[i].d_n->getNum());
00401 }
00402 return Rational(Rational::Impl(g,1));
00403 }
00404
00405 Rational lcm(const Rational &x, const Rational &y) {
00406 long int g;
00407 checkInt(x, "lcm(*x*,y)");
00408 checkInt(y, "lcm(x,*y*)");
00409 g = lcm(x.d_n->getNum(), y.d_n->getNum());
00410 return Rational(Rational::Impl(g, 1));
00411 }
00412
00413 Rational lcm(const vector<Rational> &v) {
00414 long int g(1);
00415 for(size_t i=0; i<v.size(); i++) {
00416 checkInt(v[i], "lcm(vector<Rational>)");
00417 if(v[i].d_n->getNum() != 0)
00418 g = lcm(g, v[i].d_n->getNum());
00419 }
00420 return Rational(Rational::Impl(g,1));
00421 }
00422
00423 Rational abs(const Rational &x) {
00424 long int n(x.d_n->getNum());
00425 if(n>=0) return x;
00426 return Rational(Rational::Impl(-n, x.d_n->getDen()));
00427 }
00428
00429 Rational floor(const Rational &x) {
00430 if(x.d_n->getDen() == 1) return x;
00431 long int n = x.d_n->getNum();
00432 long int nAbs = (n<0)? uminus(n) : n;
00433 long int q = nAbs / x.d_n->getDen();
00434 if(n < 0) q = plus(uminus(q), -1);
00435 return Rational(Rational::Impl(q,1));
00436 }
00437
00438 Rational ceil(const Rational &x) {
00439 if(x.d_n->getDen() == 1) return x;
00440 long int n = x.d_n->getNum();
00441 long int nAbs = (n<0)? -n : n;
00442 long int q = nAbs / x.d_n->getDen();
00443 if(n > 0) q = plus(q, 1);
00444 else q = uminus(q);
00445 return Rational(Rational::Impl(q,1));
00446 }
00447
00448 Rational mod(const Rational &x, const Rational &y) {
00449 checkInt(x, "mod(*x*,y)");
00450 checkInt(y, "mod(x,*y*)");
00451 long int r = x.d_n->getNum() % x.d_n->getDen();
00452 return(Rational(Rational::Impl(r,1)));
00453 }
00454
00455 string Rational::toString(int base) const {
00456 return(d_n->toString(base));
00457 }
00458
00459 size_t Rational::hash() const {
00460 std::hash<const char *> h;
00461 return h(toString().c_str());
00462 }
00463
00464 void Rational::print() const {
00465 cout << (*this) << endl;
00466 }
00467
00468
00469 Rational Rational::operator-() const {
00470 return Rational(Rational::Impl(-(d_n->getNum()), d_n->getDen()));
00471 }
00472
00473 Rational &Rational::operator+=(const Rational &n2) {
00474 *this = (*this) + n2;
00475 return *this;
00476 }
00477
00478 Rational &Rational::operator-=(const Rational &n2) {
00479 *this = (*this) - n2;
00480 return *this;
00481 }
00482
00483 Rational &Rational::operator*=(const Rational &n2) {
00484 *this = (*this) * n2;
00485 return *this;
00486 }
00487
00488 Rational &Rational::operator/=(const Rational &n2) {
00489 *this = (*this) / n2;
00490 return *this;
00491 }
00492
00493 int Rational::getInt() const {
00494 checkInt(*this, "getInt()");
00495 long int res = d_n->getNum();
00496 FatalAssert(res >= INT_MIN && res <= INT_MAX,
00497 "Rational::getInt(): overflow on "+toString());
00498 return (int)res;
00499 }
00500
00501 unsigned int Rational::getUnsigned() const {
00502 checkInt(*this, "getUnsigned()");
00503 long int res = d_n->getNum();
00504 FatalAssert(res >= 0 && res <= (long int)UINT_MAX,
00505 "Rational::getUnsigned(): overflow on "+toString());
00506 return (unsigned int)res;
00507 }
00508
00509 #ifdef _DEBUG_RATIONAL_
00510 void Rational::printStats() {
00511 int &num_created = getCreated();
00512 int &num_deleted = getDeleted();
00513 if(num_created % 1000 == 0 || num_deleted % 1000 == 0) {
00514 std::cerr << "Rational(" << *d_n << "): created " << num_created
00515 << ", deleted " << num_deleted
00516 << ", currently alive " << num_created-num_deleted
00517 << std::endl;
00518 }
00519 }
00520 #endif
00521
00522 bool operator==(const Rational &n1, const Rational &n2) {
00523 return(*n1.d_n == *n2.d_n);
00524 }
00525
00526 bool operator<(const Rational &n1, const Rational &n2) {
00527 return(*n1.d_n < *n2.d_n);
00528 }
00529
00530 bool operator<=(const Rational &n1, const Rational &n2) {
00531 return(*n1.d_n <= *n2.d_n);
00532 }
00533
00534 bool operator>(const Rational &n1, const Rational &n2) {
00535 return(*n1.d_n > *n2.d_n);
00536 }
00537
00538 bool operator>=(const Rational &n1, const Rational &n2) {
00539 return(*n1.d_n >= *n2.d_n);
00540 }
00541
00542 bool operator!=(const Rational &n1, const Rational &n2) {
00543 return(*n1.d_n != *n2.d_n);
00544 }
00545
00546 Rational operator+(const Rational &n1, const Rational &n2) {
00547 return Rational(Rational::Impl(*n1.d_n + *n2.d_n));
00548 }
00549
00550 Rational operator-(const Rational &n1, const Rational &n2) {
00551 return Rational(Rational::Impl((*n1.d_n) - (*n2.d_n)));
00552 }
00553
00554 Rational operator*(const Rational &n1, const Rational &n2) {
00555 return Rational(Rational::Impl((*n1.d_n) * (*n2.d_n)));
00556 }
00557
00558 Rational operator/(const Rational &n1, const Rational &n2) {
00559 return Rational(Rational::Impl(*n1.d_n / *n2.d_n));
00560 }
00561
00562 Rational operator%(const Rational &n1, const Rational &n2) {
00563 return Rational(Rational::Impl(*n1.d_n + *n2.d_n));
00564 }
00565
00566 };
00567
00568 #endif