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