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