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 #ifdef RATIONAL_GMPXX
00028
00029 #include <gmpxx.h>
00030 #include "compat_hash_set.h"
00031 #include "rational.h"
00032
00033 namespace CVC3 {
00034
00035 using namespace std;
00036
00037
00038 class Rational::Impl : public mpq_class {
00039 public:
00040
00041
00042 Impl() : mpq_class() { }
00043
00044
00045
00046 Impl(const mpq_class &x) : mpq_class(x) { }
00047
00048 Impl(const Impl &x) : mpq_class(x) { }
00049
00050 Impl(int n, int d) : mpq_class(n,d) { canonicalize(); }
00051 Impl(const mpz_class& n, const mpz_class& d)
00052 : mpq_class(n,d) { canonicalize(); }
00053
00054 Impl(const string &n, int base): mpq_class(n, base) { canonicalize(); }
00055 Impl(const string &n, const string& d, int base)
00056 : mpq_class(n + "/" + d, base) { canonicalize(); }
00057
00058 virtual ~Impl() { }
00059
00060 mpz_class getNum() { return get_num(); }
00061 mpz_class getDen() { return get_den(); }
00062 };
00063
00064
00065 Rational::Rational() : d_n(new Impl) {
00066 #ifdef _DEBUG_RATIONAL_
00067 int &num_created = getCreated();
00068 num_created++;
00069 printStats();
00070 #endif
00071 }
00072
00073 Rational::Rational(const Rational &n) : d_n(new Impl(*n.d_n)) {
00074 #ifdef _DEBUG_RATIONAL_
00075 int &num_created = getCreated();
00076 num_created++;
00077 printStats();
00078 #endif
00079 }
00080
00081
00082 Rational::Rational(const Impl& t): d_n(new Impl(t)) {
00083 #ifdef _DEBUG_RATIONAL_
00084 int &num_created = getCreated();
00085 num_created++;
00086 printStats();
00087 #endif
00088 }
00089 Rational::Rational(int n, int d): d_n(new Impl(n, d)) {
00090 #ifdef _DEBUG_RATIONAL_
00091 int &num_created = getCreated();
00092 num_created++;
00093 printStats();
00094 #endif
00095 }
00096
00097 Rational::Rational(const char* n, int base)
00098 : d_n(new Impl(string(n), base)) {
00099 #ifdef _DEBUG_RATIONAL_
00100 int &num_created = getCreated();
00101 num_created++;
00102 printStats();
00103 #endif
00104 }
00105 Rational::Rational(const string& n, int base)
00106 : d_n(new Impl(n, base)) {
00107 #ifdef _DEBUG_RATIONAL_
00108 int &num_created = getCreated();
00109 num_created++;
00110 printStats();
00111 #endif
00112 }
00113 Rational::Rational(const char* n, const char* d, int base)
00114 : d_n(new Impl(string(n), string(d), base)) {
00115 #ifdef _DEBUG_RATIONAL_
00116 int &num_created = getCreated();
00117 num_created++;
00118 printStats();
00119 #endif
00120 }
00121 Rational::Rational(const string& n, const string& d, int base)
00122 : d_n(new Impl(n, d, base)) {
00123 #ifdef _DEBUG_RATIONAL_
00124 int &num_created = getCreated();
00125 num_created++;
00126 printStats();
00127 #endif
00128 }
00129
00130 Rational::~Rational() {
00131 delete d_n;
00132 #ifdef _DEBUG_RATIONAL_
00133 int &num_deleted = getDeleted();
00134 num_deleted++;
00135 printStats();
00136 #endif
00137 }
00138
00139
00140 Rational Rational::getNumerator() const
00141 { return Rational(Impl(d_n->getNum(), 1)); }
00142 Rational Rational::getDenominator() const
00143 { return Rational(Impl(d_n->getDen(), 1)); }
00144
00145 bool Rational::isInteger() const { return 1 == d_n->getDen(); }
00146
00147
00148 Rational& Rational::operator=(const Rational& n) {
00149 if(this == &n) return *this;
00150 delete d_n;
00151 d_n = new Impl(*n.d_n);
00152 return *this;
00153 }
00154
00155 ostream &operator<<(ostream &os, const Rational &n) {
00156 return(os << n.toString());
00157 }
00158
00159
00160
00161
00162 static void checkInt(const Rational& n, const string& funName) {
00163 DebugAssert(n.isInteger(),
00164 ("CVC3::Rational::" + funName
00165 + ": argument is not an integer: " + n.toString()).c_str());
00166 }
00167
00168
00169
00170
00171
00172 Rational gcd(const Rational &x, const Rational &y) {
00173 mpz_class g;
00174 checkInt(x, "gcd(*x*,y)");
00175 checkInt(y, "gcd(x,*y*)");
00176 mpz_gcd(g.get_mpz_t(), x.d_n->get_num_mpz_t(), y.d_n->get_num_mpz_t());
00177 return Rational(Rational::Impl(g,1));
00178 }
00179
00180 Rational gcd(const vector<Rational> &v) {
00181 mpz_class g(1);
00182 if(v.size() > 0) {
00183 checkInt(v[0], "gcd(vector<Rational>[0])");
00184 g = v[0].d_n->getNum();
00185 }
00186 for(unsigned i=1; i<v.size(); i++) {
00187 checkInt(v[i], "gcd(vector<Rational>)");
00188 if(*v[i].d_n != 0)
00189 mpz_gcd(g.get_mpz_t(), g.get_mpz_t(), v[i].d_n->get_num_mpz_t());
00190 }
00191 return Rational(Rational::Impl(g,1));
00192 }
00193
00194 Rational lcm(const Rational &x, const Rational &y) {
00195 mpz_class g;
00196 checkInt(x, "lcm(*x*,y)");
00197 checkInt(y, "lcm(x,*y*)");
00198 mpz_lcm(g.get_mpz_t(), x.d_n->get_num_mpz_t(), y.d_n->get_num_mpz_t());
00199 return Rational(Rational::Impl(g, 1));
00200 }
00201
00202 Rational lcm(const vector<Rational> &v) {
00203 mpz_class g(1);
00204 for(unsigned i=0; i<v.size(); i++) {
00205 checkInt(v[i], "lcm(vector<Rational>)");
00206 if(*v[i].d_n != 0)
00207 mpz_lcm(g.get_mpz_t(), g.get_mpz_t(), v[i].d_n->get_num_mpz_t());
00208 }
00209 return Rational(Rational::Impl(g,1));
00210 }
00211
00212 Rational abs(const Rational &x) {
00213 return Rational(Rational::Impl(abs(*x.d_n)));
00214 }
00215
00216 Rational floor(const Rational &x) {
00217 mpz_class q;
00218 mpz_fdiv_q(q.get_mpz_t(), x.d_n->get_num_mpz_t(), x.d_n->get_den_mpz_t());
00219 return Rational(Rational::Impl(q,1));
00220 }
00221
00222 Rational ceil(const Rational &x) {
00223 mpz_class q;
00224 mpz_cdiv_q(q.get_mpz_t(), x.d_n->get_num_mpz_t(), x.d_n->get_den_mpz_t());
00225 return Rational(Rational::Impl(q,1));
00226 }
00227
00228 Rational mod(const Rational &x, const Rational &y) {
00229 checkInt(x, "mod(*x*,y)");
00230 checkInt(y, "mod(x,*y*)");
00231 mpz_class r;
00232 mpz_mod(r.get_mpz_t(), x.d_n->get_num_mpz_t(), y.d_n->get_num_mpz_t());
00233 return(Rational(Rational::Impl(r,1)));
00234 }
00235
00236 Rational intRoot(const Rational& base, unsigned long int n)
00237 {
00238 return Rational(Rational::Impl(0,1));
00239 }
00240
00241 string Rational::toString(int base) const {
00242 char *tmp = mpq_get_str(NULL, base, d_n->get_mpq_t());
00243 string res(tmp);
00244
00245 free(tmp);
00246 return(res);
00247 }
00248
00249 size_t Rational::hash() const {
00250 std::hash<const char *> h;
00251 return h(toString().c_str());
00252 }
00253
00254 void Rational::print() const {
00255 cout << (*d_n) << endl;
00256 }
00257
00258
00259
00260
00261 Rational Rational::operator-() const {
00262 return Rational(Rational::Impl(- (*d_n)));
00263 }
00264
00265 Rational &Rational::operator+=(const Rational &n2) {
00266 *d_n += (*n2.d_n);
00267 return *this;
00268 }
00269
00270 Rational &Rational::operator-=(const Rational &n2) {
00271 *d_n -= (*n2.d_n);
00272 return *this;
00273 }
00274
00275 Rational &Rational::operator*=(const Rational &n2) {
00276 *d_n *= (*n2.d_n);
00277 return *this;
00278 }
00279
00280 Rational &Rational::operator/=(const Rational &n2) {
00281 *d_n /= (*n2.d_n);
00282 return *this;
00283 }
00284
00285 int Rational::getInt() const {
00286 checkInt(*this, "getInt()");
00287 return mpz_get_si(d_n->get_num_mpz_t());
00288 }
00289
00290 unsigned int Rational::getUnsigned() const {
00291 checkInt(*this, "getUnsigned()");
00292 return mpz_get_ui(d_n->get_num_mpz_t());
00293 }
00294
00295 #ifdef _DEBUG_RATIONAL_
00296 void Rational::printStats() {
00297 int &num_created = getCreated();
00298 int &num_deleted = getDeleted();
00299 if(num_created % 1000 == 0 || num_deleted % 1000 == 0) {
00300 std::cerr << "Rational(" << *d_n << "): created " << num_created
00301 << ", deleted " << num_deleted
00302 << ", currently alive " << num_created-num_deleted
00303 << std::endl;
00304 }
00305 }
00306 #endif
00307
00308 bool operator==(const Rational &n1, const Rational &n2) {
00309 return(*n1.d_n == *n2.d_n);
00310 }
00311
00312 bool operator<(const Rational &n1, const Rational &n2) {
00313 return(*n1.d_n < *n2.d_n);
00314 }
00315
00316 bool operator<=(const Rational &n1, const Rational &n2) {
00317 return(*n1.d_n <= *n2.d_n);
00318 }
00319
00320 bool operator>(const Rational &n1, const Rational &n2) {
00321 return(*n1.d_n > *n2.d_n);
00322 }
00323
00324 bool operator>=(const Rational &n1, const Rational &n2) {
00325 return(*n1.d_n >= *n2.d_n);
00326 }
00327
00328 bool operator!=(const Rational &n1, const Rational &n2) {
00329 return(*n1.d_n != *n2.d_n);
00330 }
00331
00332 Rational operator+(const Rational &n1, const Rational &n2) {
00333 return Rational(Rational::Impl(*n1.d_n + *n2.d_n));
00334 }
00335
00336 Rational operator-(const Rational &n1, const Rational &n2) {
00337 return Rational(Rational::Impl((*n1.d_n) - (*n2.d_n)));
00338 }
00339
00340 Rational operator*(const Rational &n1, const Rational &n2) {
00341 return Rational(Rational::Impl((*n1.d_n) * (*n2.d_n)));
00342 }
00343
00344 Rational operator/(const Rational &n1, const Rational &n2) {
00345 return Rational(Rational::Impl(*n1.d_n / *n2.d_n));
00346 }
00347
00348 Rational operator%(const Rational &n1, const Rational &n2) {
00349 return Rational(Rational::Impl(*n1.d_n + *n2.d_n));
00350 }
00351
00352 };
00353
00354 #endif