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
00237 string Rational::toString(int base) const {
00238 char *tmp = mpq_get_str(NULL, base, d_n->get_mpq_t());
00239 string res(tmp);
00240
00241 free(tmp);
00242 return(res);
00243 }
00244
00245 size_t Rational::hash() const {
00246 std::hash<const char *> h;
00247 return h(toString().c_str());
00248 }
00249
00250 void Rational::print() const {
00251 cout << (*d_n) << endl;
00252 }
00253
00254
00255 Rational Rational::operator-() const {
00256 return Rational(Rational::Impl(- (*d_n)));
00257 }
00258
00259 Rational &Rational::operator+=(const Rational &n2) {
00260 *d_n += (*n2.d_n);
00261 return *this;
00262 }
00263
00264 Rational &Rational::operator-=(const Rational &n2) {
00265 *d_n -= (*n2.d_n);
00266 return *this;
00267 }
00268
00269 Rational &Rational::operator*=(const Rational &n2) {
00270 *d_n *= (*n2.d_n);
00271 return *this;
00272 }
00273
00274 Rational &Rational::operator/=(const Rational &n2) {
00275 *d_n /= (*n2.d_n);
00276 return *this;
00277 }
00278
00279 int Rational::getInt() const {
00280 checkInt(*this, "getInt()");
00281 return mpz_get_si(d_n->get_num_mpz_t());
00282 }
00283
00284 unsigned int Rational::getUnsigned() const {
00285 checkInt(*this, "getUnsigned()");
00286 return mpz_get_ui(d_n->get_num_mpz_t());
00287 }
00288
00289 #ifdef _DEBUG_RATIONAL_
00290 void Rational::printStats() {
00291 int &num_created = getCreated();
00292 int &num_deleted = getDeleted();
00293 if(num_created % 1000 == 0 || num_deleted % 1000 == 0) {
00294 std::cerr << "Rational(" << *d_n << "): created " << num_created
00295 << ", deleted " << num_deleted
00296 << ", currently alive " << num_created-num_deleted
00297 << std::endl;
00298 }
00299 }
00300 #endif
00301
00302 bool operator==(const Rational &n1, const Rational &n2) {
00303 return(*n1.d_n == *n2.d_n);
00304 }
00305
00306 bool operator<(const Rational &n1, const Rational &n2) {
00307 return(*n1.d_n < *n2.d_n);
00308 }
00309
00310 bool operator<=(const Rational &n1, const Rational &n2) {
00311 return(*n1.d_n <= *n2.d_n);
00312 }
00313
00314 bool operator>(const Rational &n1, const Rational &n2) {
00315 return(*n1.d_n > *n2.d_n);
00316 }
00317
00318 bool operator>=(const Rational &n1, const Rational &n2) {
00319 return(*n1.d_n >= *n2.d_n);
00320 }
00321
00322 bool operator!=(const Rational &n1, const Rational &n2) {
00323 return(*n1.d_n != *n2.d_n);
00324 }
00325
00326 Rational operator+(const Rational &n1, const Rational &n2) {
00327 return Rational(Rational::Impl(*n1.d_n + *n2.d_n));
00328 }
00329
00330 Rational operator-(const Rational &n1, const Rational &n2) {
00331 return Rational(Rational::Impl((*n1.d_n) - (*n2.d_n)));
00332 }
00333
00334 Rational operator*(const Rational &n1, const Rational &n2) {
00335 return Rational(Rational::Impl((*n1.d_n) * (*n2.d_n)));
00336 }
00337
00338 Rational operator/(const Rational &n1, const Rational &n2) {
00339 return Rational(Rational::Impl(*n1.d_n / *n2.d_n));
00340 }
00341
00342 Rational operator%(const Rational &n1, const Rational &n2) {
00343 return Rational(Rational::Impl(*n1.d_n + *n2.d_n));
00344 }
00345
00346 };
00347
00348 #endif