CVC3  2.4.1
rational.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file rational.cpp
4  *
5  * Author: Sergey Berezin
6  *
7  * Created: Dec 12 22:00:18 GMT 2002
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 // Class: Rational
21 // Author: Sergey Berezin, 12/12/2002 (adapted from Bignum)
22 //
23 // Description: Implementation of class Rational. See comments in
24 // rational.h file.
25 ///////////////////////////////////////////////////////////////////////////////
26 
27 #ifdef RATIONAL_GMPXX
28 
29 #include <gmpxx.h>
30 #include "compat_hash_set.h"
31 #include "rational.h"
32 
33 namespace CVC3 {
34 
35  using namespace std;
36 
37  // Implementation of the forward-declared internal class
38  class Rational::Impl : public mpq_class {
39  public:
40  // mpz_class _n;
41  // Constructors
42  Impl() : mpq_class() { }
43  // Constructor from integer
44  // Impl(const mpz_class &x) : mpq_class(x) { }
45  // Constructor from rational
46  Impl(const mpq_class &x) : mpq_class(x) { }
47  // Copy constructor
48  Impl(const Impl &x) : mpq_class(x) { }
49  // From pair of integers / strings
50  Impl(int n, int d) : mpq_class(n,d) { canonicalize(); }
51  Impl(const mpz_class& n, const mpz_class& d)
52  : mpq_class(n,d) { canonicalize(); }
53  // From string(s)
54  Impl(const string &n, int base): mpq_class(n, base) { canonicalize(); }
55  Impl(const string &n, const string& d, int base)
56  : mpq_class(n + "/" + d, base) { canonicalize(); }
57  // Destructor
58  virtual ~Impl() { }
59  // Getting numerator and denominator. DON NOT ASSIGN to the result
60  mpz_class getNum() { return get_num(); }
61  mpz_class getDen() { return get_den(); }
62  };
63 
64  // Constructors
65  Rational::Rational() : d_n(new Impl) {
66 #ifdef _DEBUG_RATIONAL_
67  int &num_created = getCreated();
68  num_created++;
69  printStats();
70 #endif
71  }
72  // Copy constructor
73  Rational::Rational(const Rational &n) : d_n(new Impl(*n.d_n)) {
74 #ifdef _DEBUG_RATIONAL_
75  int &num_created = getCreated();
76  num_created++;
77  printStats();
78 #endif
79  }
80 
81  // Private constructor
82  Rational::Rational(const Impl& t): d_n(new Impl(t)) {
83 #ifdef _DEBUG_RATIONAL_
84  int &num_created = getCreated();
85  num_created++;
86  printStats();
87 #endif
88  }
89  Rational::Rational(int n, int d): d_n(new Impl(n, d)) {
90 #ifdef _DEBUG_RATIONAL_
91  int &num_created = getCreated();
92  num_created++;
93  printStats();
94 #endif
95  }
96  // Constructors from strings
97  Rational::Rational(const char* n, int base)
98  : d_n(new Impl(string(n), base)) {
99 #ifdef _DEBUG_RATIONAL_
100  int &num_created = getCreated();
101  num_created++;
102  printStats();
103 #endif
104  }
105  Rational::Rational(const string& n, int base)
106  : d_n(new Impl(n, base)) {
107 #ifdef _DEBUG_RATIONAL_
108  int &num_created = getCreated();
109  num_created++;
110  printStats();
111 #endif
112  }
113  Rational::Rational(const char* n, const char* d, int base)
114  : d_n(new Impl(string(n), string(d), base)) {
115 #ifdef _DEBUG_RATIONAL_
116  int &num_created = getCreated();
117  num_created++;
118  printStats();
119 #endif
120  }
121  Rational::Rational(const string& n, const string& d, int base)
122  : d_n(new Impl(n, d, base)) {
123 #ifdef _DEBUG_RATIONAL_
124  int &num_created = getCreated();
125  num_created++;
126  printStats();
127 #endif
128  }
129  // Destructor
130  Rational::~Rational() {
131  delete d_n;
132 #ifdef _DEBUG_RATIONAL_
133  int &num_deleted = getDeleted();
134  num_deleted++;
135  printStats();
136 #endif
137  }
138 
139  // Get components
140  Rational Rational::getNumerator() const
141  { return Rational(Impl(d_n->getNum(), 1)); }
142  Rational Rational::getDenominator() const
143  { return Rational(Impl(d_n->getDen(), 1)); }
144 
145  bool Rational::isInteger() const { return 1 == d_n->getDen(); }
146 
147  // Assignment
148  Rational& Rational::operator=(const Rational& n) {
149  if(this == &n) return *this;
150  delete d_n;
151  d_n = new Impl(*n.d_n);
152  return *this;
153  }
154 
155  ostream &operator<<(ostream &os, const Rational &n) {
156  return(os << n.toString());
157  }
158 
159 
160  // Check that argument is an int and print an error message otherwise
161 
162  static void checkInt(const Rational& n, const string& funName) {
163  DebugAssert(n.isInteger(),
164  ("CVC3::Rational::" + funName
165  + ": argument is not an integer: " + n.toString()).c_str());
166  }
167 
168  /* Computes gcd and lcm on *integer* values. Result is always a
169  positive integer. In this implementation, it is guaranteed by
170  GMP. */
171 
172  Rational gcd(const Rational &x, const Rational &y) {
173  mpz_class g;
174  checkInt(x, "gcd(*x*,y)");
175  checkInt(y, "gcd(x,*y*)");
176  mpz_gcd(g.get_mpz_t(), x.d_n->get_num_mpz_t(), y.d_n->get_num_mpz_t());
177  return Rational(Rational::Impl(g,1));
178  }
179 
180  Rational gcd(const vector<Rational> &v) {
181  mpz_class g(1);
182  if(v.size() > 0) {
183  checkInt(v[0], "gcd(vector<Rational>[0])");
184  g = v[0].d_n->getNum();
185  }
186  for(unsigned i=1; i<v.size(); i++) {
187  checkInt(v[i], "gcd(vector<Rational>)");
188  if(*v[i].d_n != 0)
189  mpz_gcd(g.get_mpz_t(), g.get_mpz_t(), v[i].d_n->get_num_mpz_t());
190  }
191  return Rational(Rational::Impl(g,1));
192  }
193 
194  Rational lcm(const Rational &x, const Rational &y) {
195  mpz_class g;
196  checkInt(x, "lcm(*x*,y)");
197  checkInt(y, "lcm(x,*y*)");
198  mpz_lcm(g.get_mpz_t(), x.d_n->get_num_mpz_t(), y.d_n->get_num_mpz_t());
199  return Rational(Rational::Impl(g, 1));
200  }
201 
202  Rational lcm(const vector<Rational> &v) {
203  mpz_class g(1);
204  for(unsigned i=0; i<v.size(); i++) {
205  checkInt(v[i], "lcm(vector<Rational>)");
206  if(*v[i].d_n != 0)
207  mpz_lcm(g.get_mpz_t(), g.get_mpz_t(), v[i].d_n->get_num_mpz_t());
208  }
209  return Rational(Rational::Impl(g,1));
210  }
211 
212  Rational abs(const Rational &x) {
213  return Rational(Rational::Impl(abs(*x.d_n)));
214  }
215 
216  Rational floor(const Rational &x) {
217  mpz_class q;
218  mpz_fdiv_q(q.get_mpz_t(), x.d_n->get_num_mpz_t(), x.d_n->get_den_mpz_t());
219  return Rational(Rational::Impl(q,1));
220  }
221 
222  Rational ceil(const Rational &x) {
223  mpz_class q;
224  mpz_cdiv_q(q.get_mpz_t(), x.d_n->get_num_mpz_t(), x.d_n->get_den_mpz_t());
225  return Rational(Rational::Impl(q,1));
226  }
227 
228  Rational mod(const Rational &x, const Rational &y) {
229  checkInt(x, "mod(*x*,y)");
230  checkInt(y, "mod(x,*y*)");
231  mpz_class r;
232  mpz_mod(r.get_mpz_t(), x.d_n->get_num_mpz_t(), y.d_n->get_num_mpz_t());
233  return(Rational(Rational::Impl(r,1)));
234  }
235 
236  Rational intRoot(const Rational& base, unsigned long int n)
237  {
238  return Rational(Rational::Impl(0,1));
239  }
240 
241  string Rational::toString(int base) const {
242  char *tmp = mpq_get_str(NULL, base, d_n->get_mpq_t());
243  string res(tmp);
244 // delete tmp;
245  free(tmp);
246  return(res);
247  }
248 
249  size_t Rational::hash() const {
251  return h(toString().c_str());
252  }
253 
254  void Rational::print() const {
255  cout << (*d_n) << endl;
256  }
257 
258 
259 
260  // Unary minus
261  Rational Rational::operator-() const {
262  return Rational(Rational::Impl(- (*d_n)));
263  }
264 
265  Rational &Rational::operator+=(const Rational &n2) {
266  *d_n += (*n2.d_n);
267  return *this;
268  }
269 
270  Rational &Rational::operator-=(const Rational &n2) {
271  *d_n -= (*n2.d_n);
272  return *this;
273  }
274 
275  Rational &Rational::operator*=(const Rational &n2) {
276  *d_n *= (*n2.d_n);
277  return *this;
278  }
279 
280  Rational &Rational::operator/=(const Rational &n2) {
281  *d_n /= (*n2.d_n);
282  return *this;
283  }
284 
285  int Rational::getInt() const {
286  checkInt(*this, "getInt()");
287  return mpz_get_si(d_n->get_num_mpz_t());
288  }
289 
290  unsigned int Rational::getUnsigned() const {
291  checkInt(*this, "getUnsigned()");
292  return mpz_get_ui(d_n->get_num_mpz_t());
293  }
294 
295 #ifdef _DEBUG_RATIONAL_
296  void Rational::printStats() {
297  int &num_created = getCreated();
298  int &num_deleted = getDeleted();
299  if(num_created % 1000 == 0 || num_deleted % 1000 == 0) {
300  std::cerr << "Rational(" << *d_n << "): created " << num_created
301  << ", deleted " << num_deleted
302  << ", currently alive " << num_created-num_deleted
303  << std::endl;
304  }
305  }
306 #endif
307 
308  bool operator==(const Rational &n1, const Rational &n2) {
309  return(*n1.d_n == *n2.d_n);
310  }
311 
312  bool operator<(const Rational &n1, const Rational &n2) {
313  return(*n1.d_n < *n2.d_n);
314  }
315 
316  bool operator<=(const Rational &n1, const Rational &n2) {
317  return(*n1.d_n <= *n2.d_n);
318  }
319 
320  bool operator>(const Rational &n1, const Rational &n2) {
321  return(*n1.d_n > *n2.d_n);
322  }
323 
324  bool operator>=(const Rational &n1, const Rational &n2) {
325  return(*n1.d_n >= *n2.d_n);
326  }
327 
328  bool operator!=(const Rational &n1, const Rational &n2) {
329  return(*n1.d_n != *n2.d_n);
330  }
331 
332  Rational operator+(const Rational &n1, const Rational &n2) {
333  return Rational(Rational::Impl(*n1.d_n + *n2.d_n));
334  }
335 
336  Rational operator-(const Rational &n1, const Rational &n2) {
337  return Rational(Rational::Impl((*n1.d_n) - (*n2.d_n)));
338  }
339 
340  Rational operator*(const Rational &n1, const Rational &n2) {
341  return Rational(Rational::Impl((*n1.d_n) * (*n2.d_n)));
342  }
343 
344  Rational operator/(const Rational &n1, const Rational &n2) {
345  return Rational(Rational::Impl(*n1.d_n / *n2.d_n));
346  }
347 
348  Rational operator%(const Rational &n1, const Rational &n2) {
349  return Rational(Rational::Impl(*n1.d_n + *n2.d_n));
350  }
351 
352 
353  // Implementation of the forward-declared internal class
354  class Unsigned::Impl : public mpz_class {
355  public:
356  // mpz_class _n;
357  // Constructors
358  Impl() : mpz_class() { }
359  // Constructor from integer
360  // Impl(const mpz_class &x) : mpq_class(x) { }
361  // Constructor from rational
362  Impl(const mpz_class &x) : mpz_class(x) { }
363  // Copy constructor
364  Impl(const Impl &x) : mpz_class(x) { }
365  // From pair of integers / strings
366  Impl(int n) : mpz_class(n) { }
367  Impl(const mpz_class& n, const mpz_class& d)
368  : mpq_class(n,d) { canonicalize(); }
369  // From string(s)
370  Impl(const string &n, int base): mpz_class(n, base) { }
371  // Destructor
372  virtual ~Impl() { }
373  };
374 
375  // Constructors
376  Unsigned::Unsigned() : d_n(new Impl) { }
377  // Copy constructor
378  Unsigned::Unsigned(const Unsigned &n) : d_n(new Impl(*n.d_n)) { }
379 
380  // Private constructor
381  Unsigned::Unsigned(const Impl& t): d_n(new Impl(t)) { }
382  // Constructors from strings
383  Unsigned::Unsigned(const char* n, int base)
384  : d_n(new Impl(string(n), base)) { }
385  Unsigned::Unsigned(const string& n, int base)
386  : d_n(new Impl(n, base)) { }
387  // Destructor
388  Unsigned::~Unsigned() {
389  delete d_n;
390  }
391 
392  // Assignment
393  Unsigned& Unsigned::operator=(const Unsigned& n) {
394  if(this == &n) return *this;
395  delete d_n;
396  d_n = new Impl(*n.d_n);
397  return *this;
398  }
399 
400  ostream &operator<<(ostream &os, const Unsigned &n) {
401  return(os << n.toString());
402  }
403 
404 
405  /* Computes gcd and lcm on *integer* values. Result is always a
406  positive integer. In this implementation, it is guaranteed by
407  GMP. */
408 
409  Unsigned gcd(const Unsigned &x, const Unsigned &y) {
410  mpz_class g;
411  mpz_gcd(g, *(x.d_n), *(y.d_n));
412  return Unsigned(Unsigned::Impl(g));
413  }
414 
415  Unsigned gcd(const vector<Unsigned> &v) {
416  mpz_class g(1);
417  if(v.size() > 0) {
418  g = *(v[0].d_n);
419  }
420  for(unsigned i=1; i<v.size(); i++) {
421  if(*v[i].d_n != 0)
422  mpz_gcd(g, g, *(v[i].d_n));
423  }
424  return Unsigned(Unsigned::Impl(g));
425  }
426 
427  Unsigned lcm(const Unsigned &x, const Unsigned &y) {
428  mpz_class g;
429  mpz_lcm(g, *x.d_n, *y.d_n);
430  return Unsigned(Unsigned::Impl(g));
431  }
432 
433  Unsigned lcm(const vector<Unsigned> &v) {
434  mpz_class g(1);
435  for(unsigned i=0; i<v.size(); i++) {
436  if(*v[i].d_n != 0)
437  mpz_lcm(g, g, *v[i].d_n);
438  }
439  return Unsigned(Unsigned::Impl(g));
440  }
441 
442  Unsigned abs(const Unsigned &x) {
443  return Unsigned(Unsigned::Impl(abs(*x.d_n)));
444  }
445 
446  Unsigned mod(const Unsigned &x, const Unsigned &y) {
447  mpz_class r;
448  mpz_mod(r, *x.d_n, *y.d_n);
449  return(Unsigned(Unsigned::Impl(r)));
450  }
451 
452  Unsigned intRoot(const Unsigned& base, unsigned long int n)
453  {
454  return Unsigned(Unsigned::Impl(0,1));
455  }
456 
457  string Unsigned::toString(int base) const {
458  char *tmp = mpz_get_str(NULL, base, *d_n);
459  string res(tmp);
460 // delete tmp;
461  free(tmp);
462  return(res);
463  }
464 
465  size_t Unsigned::hash() const {
467  return h(toString().c_str());
468  }
469 
470  void Unsigned::print() const {
471  cout << (*d_n) << endl;
472  }
473 
474 
475 
476  // Unary minus
477  Unsigned Unsigned::operator-() const {
478  return Unsigned(Unsigned::Impl(- (*d_n)));
479  }
480 
481  Unsigned &Unsigned::operator+=(const Unsigned &n2) {
482  *d_n += (*n2.d_n);
483  return *this;
484  }
485 
486  Unsigned &Unsigned::operator-=(const Unsigned &n2) {
487  *d_n -= (*n2.d_n);
488  return *this;
489  }
490 
491  Unsigned &Unsigned::operator*=(const Unsigned &n2) {
492  *d_n *= (*n2.d_n);
493  return *this;
494  }
495 
496  Unsigned &Unsigned::operator/=(const Unsigned &n2) {
497  *d_n /= (*n2.d_n);
498  return *this;
499  }
500 
501  int Unsigned::getInt() const {
502  return mpz_get_si(*d_n);
503  }
504 
505  unsigned int Unsigned::getUnsigned() const {
506  return mpz_get_ui(*d_n);
507  }
508 
509  bool operator==(const Unsigned &n1, const Unsigned &n2) {
510  return(*n1.d_n == *n2.d_n);
511  }
512 
513  bool operator<(const Unsigned &n1, const Unsigned &n2) {
514  return(*n1.d_n < *n2.d_n);
515  }
516 
517  bool operator<=(const Unsigned &n1, const Unsigned &n2) {
518  return(*n1.d_n <= *n2.d_n);
519  }
520 
521  bool operator>(const Unsigned &n1, const Unsigned &n2) {
522  return(*n1.d_n > *n2.d_n);
523  }
524 
525  bool operator>=(const Unsigned &n1, const Unsigned &n2) {
526  return(*n1.d_n >= *n2.d_n);
527  }
528 
529  bool operator!=(const Unsigned &n1, const Unsigned &n2) {
530  return(*n1.d_n != *n2.d_n);
531  }
532 
533  Unsigned operator+(const Unsigned &n1, const Unsigned &n2) {
534  return Unsigned(Unsigned::Impl(*n1.d_n + *n2.d_n));
535  }
536 
537  Unsigned operator-(const Unsigned &n1, const Unsigned &n2) {
538  return Unsigned(Unsigned::Impl((*n1.d_n) - (*n2.d_n)));
539  }
540 
541  Unsigned operator*(const Unsigned &n1, const Unsigned &n2) {
542  return Unsigned(Unsigned::Impl((*n1.d_n) * (*n2.d_n)));
543  }
544 
545  Unsigned operator/(const Unsigned &n1, const Unsigned &n2) {
546  return Unsigned(Unsigned::Impl(*n1.d_n / *n2.d_n));
547  }
548 
549  Unsigned operator%(const Unsigned &n1, const Unsigned &n2) {
550  return Unsigned(Unsigned::Impl(*n1.d_n + *n2.d_n));
551  }
552 
553 }; /* close namespace */
554 
555 
556 #endif
bool operator<=(const Expr &e1, const Expr &e2)
Definition: expr.h:1612
ostream & operator<<(ostream &os, const Expr &e)
Definition: expr.cpp:621
Expr operator+(const Expr &left, const Expr &right)
Definition: theory_arith.h:232
STL namespace.
Expr operator/(const Expr &left, const Expr &right)
Definition: theory_arith.h:238
#define DebugAssert(cond, str)
Definition: debug.h:408
bool operator==(const Expr &e1, const Expr &e2)
Definition: expr.h:1600
bool operator>(const Expr &e1, const Expr &e2)
Definition: expr.h:1614
Expr operator-(const Expr &child)
Definition: theory_arith.h:230
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
Expr operator*(const Expr &left, const Expr &right)
Definition: theory_arith.h:236
T abs(T t)
Definition: cvc_util.h:53
bool operator<(const Expr &e1, const Expr &e2)
Definition: expr.h:1610
bool operator>=(const Expr &e1, const Expr &e2)
Definition: expr.h:1616
bool operator!=(const Expr &e1, const Expr &e2)
Definition: expr.h:1605
Definition: expr.cpp:35