CVC3  2.4.1
rational-gmp.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file rational-gmp.cpp
4  *
5  * \brief Implementation of class Rational using GMP library (C interface)
6  *
7  * Author: Sergey Berezin
8  *
9  * Created: Mon Aug 4 10:06:04 2003
10  *
11  * <hr>
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  *
19  */
20 /*****************************************************************************/
21 
22 #ifdef RATIONAL_GMP
23 
24 #include "compat_hash_set.h"
25 #include "rational.h"
26 
27 #include <climits>
28 #include <sstream>
29 #include <gmp.h>
30 #include <limits.h>
31 
32 namespace CVC3 {
33 
34  using namespace std;
35 
36  //! Implementation of the forward-declared internal class
37  class Rational::Impl {
38  mpq_t d_n;
39  //! Make the rational number canonical
40  void canonicalize() { mpq_canonicalize(d_n); }
41  public:
42  //! Default Constructor
43  Impl() { mpq_init(d_n); }
44  //! Copy constructor (assumes x is canonicalized)
45  Impl(const Impl &x) { mpq_init(d_n); mpq_set(d_n, x.d_n); }
46  //! Constructor from mpq_t
47  Impl(mpq_t n) {
48  mpq_init(d_n);
49  mpq_set(d_n, n);
50  canonicalize();
51  }
52  //! Constructor from a pair of mpz_t (integers)
53  Impl(mpz_t n, mpz_t d) {
54  mpq_init(d_n);
55  mpq_set_num(d_n, n); mpq_set_den(d_n, d);
56  canonicalize();
57  }
58  //! Constructor from a single mpz_t (integer)
59  Impl(mpz_t n) {
60  mpq_init(d_n);
61  mpq_set_num(d_n, n);
62  canonicalize();
63  }
64  //! Constructor from a pair of integers
65  Impl(long int n, long int d);
66  //! Constructor from a pair of unsigned integers
67  Impl(unsigned int n, unsigned int d, unsigned int /* dummy arg */);
68  //! Constructor from a string
69  Impl(const string &n, int base);
70  //! Constructor from a pair of strings
71  Impl(const string &n, const string& d, int base);
72  // Destructor
73  virtual ~Impl() { mpq_clear(d_n); }
74 
75  //! Assignment
76  Impl& operator=(const Impl& x) {
77  if(this == &x) return *this;
78  mpq_set(d_n, x.d_n);
79  return *this;
80  }
81 
82  //! Get numerator
83  Impl getNum() const {
84  return Impl(mpq_numref(const_cast<Impl*>(this)->d_n));
85  }
86  //! Get denominator
87  Impl getDen() const {
88  return Impl(mpq_denref(const_cast<Impl*>(this)->d_n));
89  }
90 
91  int getInt() const {
92  // Check for overflow
93  static Impl min((int)INT_MIN, 1), max((int)INT_MAX, 1);
94  FatalAssert(isInteger() && min <= *this && *this <= max,
95  "Rational::getInt(): Arithmetic overflow for "
96  +toString());
97  return mpz_get_si(mpq_numref(d_n));
98  }
99 
100  unsigned int getUnsigned() const {
101  // Check for overflow
102  static Impl min(0, 1, 0), max(UINT_MAX, 1, 0);
103  FatalAssert(min <= *this && *this <= max,
104  "Rational::getUnsigned(): Arithmetic overflow for "
105  +toString());
106  return mpz_get_ui(mpq_numref(d_n));
107  }
108 
109  Unsigned getUnsignedMP() const;
110 
111  //! Unary minus
112  Impl operator-() const;
113  //! Get the floor
114  Impl floor() const;
115  //! Get the ceiling
116  Impl ceil() const;
117 
118  //! Testing whether the denominator is 1
119  bool isInteger() const;
120 
121  //! Equality
122  friend bool operator==(const Impl& x, const Impl& y) {
123  return mpq_equal(x.d_n, y.d_n);
124  }
125 
126  //! Dis-equality
127  friend bool operator!=(const Impl& x, const Impl& y) {
128  return !mpq_equal(x.d_n, y.d_n);
129  }
130  //! Less than
131  friend bool operator<(const Impl& x, const Impl& y) {
132  return mpq_cmp(x.d_n, y.d_n) < 0;
133  }
134 
135  friend bool operator<=(const Impl& x, const Impl& y) {
136  return mpq_cmp(x.d_n, y.d_n) <= 0;
137  }
138 
139  friend bool operator>(const Impl& x, const Impl& y) {
140  return mpq_cmp(x.d_n, y.d_n) > 0;
141  }
142 
143  friend bool operator>=(const Impl& x, const Impl& y) {
144  return mpq_cmp(x.d_n, y.d_n) >= 0;
145  }
146 
147  //! Addition
148  friend Impl operator+(const Impl& x, const Impl& y) {
149  Impl res;
150  mpq_add(res.d_n, x.d_n, y.d_n);
151  return res;
152  }
153 
154  //! Subtraction
155  friend Impl operator-(const Impl& x, const Impl& y) {
156  Impl res;
157  mpq_sub(res.d_n, x.d_n, y.d_n);
158  return res;
159  }
160 
161  //! Multiplication
162  friend Impl operator*(const Impl& x, const Impl& y) {
163  Impl res;
164  mpq_mul(res.d_n, x.d_n, y.d_n);
165  return res;
166  }
167 
168  //! Division
169  friend Impl operator/(const Impl& x, const Impl& y) {
170  Impl res;
171  mpq_div(res.d_n, x.d_n, y.d_n);
172  return res;
173  }
174 
175  friend Impl operator%(const Impl& x, const Impl& y) {
176  DebugAssert(x.isInteger() && y.isInteger(),
177  "Impl % Impl: x and y must be integers");
178  mpz_t res;
179  mpz_init(res);
180  // Put the remainder directly into 'res'
181  mpz_fdiv_r(res, mpq_numref(x.d_n), mpq_numref(y.d_n));
182  Impl r(res);
183  mpz_clear(res);
184  return r;
185  }
186 
187  //! Compute the remainder of x/y
188  friend Impl mod(const Impl& x, const Impl& y) {
189  DebugAssert(x.isInteger() && y.isInteger(),
190  "Rational::Impl::mod(): x="+x.toString()
191  +", y="+y.toString());
192  mpz_t res;
193  mpz_init(res);
194  mpz_mod(res, mpq_numref(x.d_n), mpq_numref(y.d_n));
195  Impl r(res);
196  mpz_clear(res);
197  return r;
198  }
199 
200  friend Impl intRoot(const Impl& x, unsigned long int y) {
201  DebugAssert(x.isInteger(),
202  "Rational::Impl::intRoot(): x="+x.toString());
203  mpz_t res;
204  mpz_init(res);
205  int exact = mpz_root(res, mpq_numref(x.d_n), y);
206  if (!exact) {
207  mpz_set_ui(res, 0);
208  }
209  Impl r(res);
210  mpz_clear(res);
211  return r;
212  }
213 
214  friend Impl gcd(const Impl& x, const Impl& y) {
215  DebugAssert(x.isInteger() && y.isInteger(),
216  "Rational::Impl::gcd(): x="+x.toString()
217  +", y="+y.toString());
218  TRACE("rational", "Impl::gcd(", x, ", "+y.toString()+") {");
219  mpz_t res;
220  mpz_init(res);
221  mpz_gcd(res, mpq_numref(x.d_n), mpq_numref(y.d_n));
222  Impl r(res);
223  mpz_clear(res);
224  TRACE("rational", "Impl::gcd => ", r, "}");
225  return r;
226  }
227 
228  friend Impl lcm(const Impl& x, const Impl& y) {
229  DebugAssert(x.isInteger() && y.isInteger(),
230  "Rational::Impl::lcm(): x="+x.toString()
231  +", y="+y.toString());
232  mpz_t res;
233  mpz_init(res);
234  mpz_lcm(res, mpq_numref(x.d_n), mpq_numref(y.d_n));
235  Impl r(res);
236  mpz_clear(res);
237  return r;
238  }
239 
240  //! Print to string
241  string toString(int base = 10) const {
242  char* str = (char*)malloc(mpz_sizeinbase(mpq_numref(d_n), base)
243  +mpz_sizeinbase(mpq_denref(d_n), base)+3);
244  mpq_get_str(str, base, d_n);
245  string res(str);
246  free(str);
247  return res;
248  }
249  };
250 
251  // Constructor from a pair of integers
252  Rational::Impl::Impl(long int n, long int d) {
253  mpq_init(d_n);
254  DebugAssert(d > 0, "Rational::Impl(long n, long d): d = "+int2string(d));
255  mpq_set_si(d_n, n, (unsigned long int)d);
256  canonicalize();
257  }
258 
259  // Constructor from a pair of unsigned integers
260  Rational::Impl::Impl(unsigned int n, unsigned int d,
261  unsigned int /* dummy arg, to disambiguate */) {
262  mpq_init(d_n);
263  mpq_set_ui(d_n, n, (unsigned long int)d);
264  canonicalize();
265  }
266 
267  // Constructor from a string
268  Rational::Impl::Impl(const string &n, int base) {
269  mpq_init(d_n);
270  mpq_set_str(d_n, n.c_str(), base);
271  canonicalize();
272  }
273 
274  // Constructor from a pair of strings
275  Rational::Impl::Impl(const string &n, const string& d, int base) {
276  mpq_init(d_n);
277  mpq_set_str(d_n, (n+"/"+d).c_str(), base);
278  canonicalize();
279  }
280 
281  Rational::Impl Rational::Impl::operator-() const {
282  Impl res;
283  mpq_neg(res.d_n, d_n);
284  return res;
285  }
286 
287  Rational::Impl Rational::Impl::floor() const {
288  mpz_t res;
289  mpz_init(res);
290  mpz_fdiv_q(res, mpq_numref(d_n), mpq_denref(d_n));
291  Impl r(res);
292  mpz_clear(res);
293  return r;
294  }
295 
296  Rational::Impl Rational::Impl::ceil() const {
297  mpz_t res;
298  mpz_init(res);
299  mpz_cdiv_q(res, mpq_numref(d_n), mpq_denref(d_n));
300  Impl r(res);
301  mpz_clear(res);
302  return r;
303  }
304 
305  bool Rational::Impl::isInteger() const {
306  bool res(mpz_cmp_ui(mpq_denref(d_n), 1) == 0);
307  TRACE("rational", "Impl::isInteger(", *this,
308  ") => "+string(res? "true" : "false"));
309  return res;
310  }
311 
312  //! Default constructor
313  Rational::Rational() : d_n(new Impl) {
314 #ifdef _DEBUG_RATIONAL_
315  int &num_created = getCreated();
316  num_created++;
317  printStats();
318 #endif
319  }
320  //! Copy constructor
321  Rational::Rational(const Rational &n) : d_n(new Impl(*n.d_n)) {
322 #ifdef _DEBUG_RATIONAL_
323  int &num_created = getCreated();
324  num_created++;
325  printStats();
326 #endif
327  }
328 
329  Rational::Rational(const Unsigned& n): d_n(new Impl(n.toString(), 10)) {
330 #ifdef _DEBUG_RATIONAL_
331  int &num_created = getCreated();
332  num_created++;
333  printStats();
334 #endif
335  }
336  //! Private constructor
337  Rational::Rational(const Impl& t): d_n(new Impl(t)) {
338 #ifdef _DEBUG_RATIONAL_
339  int &num_created = getCreated();
340  num_created++;
341  printStats();
342 #endif
343  }
344  Rational::Rational(int n, int d): d_n(new Impl(n, d)) {
345 #ifdef _DEBUG_RATIONAL_
346  int &num_created = getCreated();
347  num_created++;
348  printStats();
349 #endif
350  }
351  // Constructors from strings
352  Rational::Rational(const char* n, int base)
353  : d_n(new Impl(string(n), base)) {
354 #ifdef _DEBUG_RATIONAL_
355  int &num_created = getCreated();
356  num_created++;
357  printStats();
358 #endif
359  }
360  Rational::Rational(const string& n, int base)
361  : d_n(new Impl(n, base)) {
362 #ifdef _DEBUG_RATIONAL_
363  int &num_created = getCreated();
364  num_created++;
365  printStats();
366 #endif
367  }
368  Rational::Rational(const char* n, const char* d, int base)
369  : d_n(new Impl(string(n), string(d), base)) {
370 #ifdef _DEBUG_RATIONAL_
371  int &num_created = getCreated();
372  num_created++;
373  printStats();
374 #endif
375  }
376  Rational::Rational(const string& n, const string& d, int base)
377  : d_n(new Impl(n, d, base)) {
378 #ifdef _DEBUG_RATIONAL_
379  int &num_created = getCreated();
380  num_created++;
381  printStats();
382 #endif
383  }
384  // Destructor
385  Rational::~Rational() {
386 #ifdef _DEBUG_RATIONAL_
387  int &num_deleted = getDeleted();
388  num_deleted++;
389  printStats();
390 #endif
391  delete d_n;
392  }
393 
394  // Get components
395  Rational Rational::getNumerator() const
396  { return Rational(d_n->getNum()); }
397  Rational Rational::getDenominator() const
398  { return Rational(d_n->getDen()); }
399 
400  bool Rational::isInteger() const { return d_n->isInteger(); }
401 
402  // Assignment
403  Rational& Rational::operator=(const Rational& n) {
404  if(this == &n) return *this;
405  delete d_n;
406  d_n = new Impl(*n.d_n);
407  return *this;
408  }
409 
410  ostream &operator<<(ostream &os, const Rational &n) {
411  return(os << n.toString());
412  }
413 
414  //! Printing to ostream
415  std::ostream& operator<<(std::ostream& os, const Rational::Impl& n) {
416  return os << n.toString();
417  }
418 
419 
420  // Check that argument is an int and print an error message otherwise
421 
422  static void checkInt(const Rational& n, const string& funName) {
423  TRACE("rational", "checkInt(", n, ")");
424  DebugAssert(n.isInteger(),
425  "CVC3::Rational::" + funName
426  + ": argument is not an integer: " + n.toString());
427  }
428 
429  /* Computes gcd and lcm on *integer* values. Result is always a
430  positive integer. In this implementation, it is guaranteed by
431  GMP. */
432 
433  Rational gcd(const Rational &x, const Rational &y) {
434  checkInt(x, "gcd(*x*,y)");
435  checkInt(y, "gcd(x,*y*)");
436  return Rational(gcd(*x.d_n, *y.d_n));
437  }
438 
439  Rational gcd(const vector<Rational> &v) {
440  Rational::Impl g(1,1), zero;
441  if(v.size() > 0) {
442  checkInt(v[0], "gcd(vector<Rational>[0])");
443  g = *v[0].d_n;
444  }
445  for(size_t i=1; i<v.size(); i++) {
446  checkInt(v[i], "gcd(vector<Rational>)");
447  if(g == zero)
448  g = *(v[i].d_n);
449  else if(*(v[i].d_n) != zero)
450  g = gcd(g, *(v[i].d_n));
451  }
452  return Rational(g);
453  }
454 
455  Rational lcm(const Rational &x, const Rational &y) {
456  checkInt(x, "lcm(*x*,y)");
457  checkInt(y, "lcm(x,*y*)");
458  return Rational(lcm(*x.d_n, *y.d_n));
459  }
460 
461  Rational lcm(const vector<Rational> &v) {
462  Rational::Impl g(1,1), zero;
463  for(size_t i=0; i<v.size(); i++) {
464  checkInt(v[i], "lcm(vector<Rational>)");
465  if(*v[i].d_n != zero)
466  g = lcm(g, *v[i].d_n);
467  }
468  return Rational(g);
469  }
470 
471  Rational abs(const Rational &x) {
472  if(x<0) return -x;
473  return x;
474  }
475 
476  Rational floor(const Rational &x) {
477  return Rational(x.d_n->floor());
478  }
479 
480  Rational ceil(const Rational &x) {
481  return Rational(x.d_n->ceil());
482  }
483 
484  Rational mod(const Rational &x, const Rational &y) {
485  checkInt(x, "mod(*x*,y)");
486  checkInt(y, "mod(x,*y*)");
487  return(Rational(mod(*x.d_n, *y.d_n)));
488  }
489 
490  Rational intRoot(const Rational& base, unsigned long int n) {
491  checkInt(base, "intRoot(*x*,y)");
492  return Rational(intRoot(*base.d_n, n));
493  }
494 
495  string Rational::toString(int base) const {
496  return(d_n->toString(base));
497  }
498 
499  size_t Rational::hash() const {
501  return h(toString().c_str());
502  }
503 
504  void Rational::print() const {
505  cout << (*this) << endl;
506  }
507 
508  // Unary minus
509  Rational Rational::operator-() const {
510  return Rational(-(*d_n));
511  }
512 
513  Rational &Rational::operator+=(const Rational &n2) {
514  *this = (*this) + n2;
515  return *this;
516  }
517 
518  Rational &Rational::operator-=(const Rational &n2) {
519  *this = (*this) - n2;
520  return *this;
521  }
522 
523  Rational &Rational::operator*=(const Rational &n2) {
524  *this = (*this) * n2;
525  return *this;
526  }
527 
528  Rational &Rational::operator/=(const Rational &n2) {
529  *this = (*this) / n2;
530  return *this;
531  }
532 
533  int Rational::getInt() const {
534  checkInt(*this, "getInt()");
535  return d_n->getInt();
536  }
537 
538  unsigned int Rational::getUnsigned() const {
539  checkInt(*this, "getUnsigned()");
540  return d_n->getUnsigned();
541  }
542 
543  Unsigned Rational::getUnsignedMP() const {
544  checkInt(*this, "getUnsignedMP()");
545  return d_n->getUnsignedMP();
546  }
547 
548 #ifdef _DEBUG_RATIONAL_
549  void Rational::printStats() {
550  int &num_created = getCreated();
551  int &num_deleted = getDeleted();
552  if(num_created % 1000 == 0 || num_deleted % 1000 == 0) {
553  std::cerr << "Rational(" << *d_n << "): created " << num_created
554  << ", deleted " << num_deleted
555  << ", currently alive " << num_created-num_deleted
556  << std::endl;
557  }
558  }
559 #endif
560 
561  bool operator==(const Rational &n1, const Rational &n2) {
562  return(*n1.d_n == *n2.d_n);
563  }
564 
565  bool operator<(const Rational &n1, const Rational &n2) {
566  return(*n1.d_n < *n2.d_n);
567  }
568 
569  bool operator<=(const Rational &n1, const Rational &n2) {
570  return(*n1.d_n <= *n2.d_n);
571  }
572 
573  bool operator>(const Rational &n1, const Rational &n2) {
574  return(*n1.d_n > *n2.d_n);
575  }
576 
577  bool operator>=(const Rational &n1, const Rational &n2) {
578  return(*n1.d_n >= *n2.d_n);
579  }
580 
581  bool operator!=(const Rational &n1, const Rational &n2) {
582  return(*n1.d_n != *n2.d_n);
583  }
584 
585  Rational operator+(const Rational &n1, const Rational &n2) {
586  return Rational((*n1.d_n) + (*n2.d_n));
587  }
588 
589  Rational operator-(const Rational &n1, const Rational &n2) {
590  return Rational((*n1.d_n) - (*n2.d_n));
591  }
592 
593  Rational operator*(const Rational &n1, const Rational &n2) {
594  return Rational((*n1.d_n) * (*n2.d_n));
595  }
596 
597  Rational operator/(const Rational &n1, const Rational &n2) {
598  return Rational((*n1.d_n) / (*n2.d_n));
599  }
600 
601  Rational operator%(const Rational &n1, const Rational &n2) {
602  return Rational((*n1.d_n) % (*n2.d_n));
603  }
604 
605  //! Implementation of the forward-declared internal class
606  class Unsigned::Impl {
607  mpz_t d_n;
608  public:
609  //! Default Constructor
610  Impl() { mpz_init(d_n); }
611  //! Copy constructor (assumes x is canonicalized)
612  Impl(const Impl &x) { mpz_init(d_n); mpz_set(d_n, x.d_n); }
613  //! Constructor from mpz_t
614  Impl(const mpz_t n) {
615  mpz_init(d_n);
616  mpz_set(d_n, n);
617  }
618  //! Constructor from an unsigned integer
619  Impl(unsigned int n);
620  //! Constructor from a string
621  Impl(const string &n, int base);
622  // Destructor
623  virtual ~Impl() { mpz_clear(d_n); }
624 
625  //! Assignment
626  Impl& operator=(const Impl& x) {
627  if(this == &x) return *this;
628  mpz_set(d_n, x.d_n);
629  return *this;
630  }
631 
632  int getInt() const {
633  // Check for overflow
634  static Impl max((int)INT_MAX);
635  FatalAssert(*this <= max,
636  "Unsigned::getInt(): Arithmetic overflow for "
637  +toString());
638  return mpz_get_si(d_n);
639  }
640 
641  unsigned long getUnsigned() const {
642  // Check for overflow
643  static Impl max(UINT_MAX);
644  FatalAssert(*this <= max,
645  "Unsigned::getUnsigned(): Arithmetic overflow for "
646  +toString());
647  return mpz_get_ui(d_n);
648  }
649 
650  //! Unary minus
651  Impl operator-() const;
652 
653  //! Equality
654  friend bool operator==(const Impl& x, const Impl& y) {
655  return mpz_cmp(x.d_n, y.d_n) == 0;
656  }
657 
658  //! Dis-equality
659  friend bool operator!=(const Impl& x, const Impl& y) {
660  return mpz_cmp(x.d_n, y.d_n) != 0;
661  }
662  //! Less than
663  friend bool operator<(const Impl& x, const Impl& y) {
664  return mpz_cmp(x.d_n, y.d_n) < 0;
665  }
666 
667  friend bool operator<=(const Impl& x, const Impl& y) {
668  return mpz_cmp(x.d_n, y.d_n) <= 0;
669  }
670 
671  friend bool operator>(const Impl& x, const Impl& y) {
672  return mpz_cmp(x.d_n, y.d_n) > 0;
673  }
674 
675  friend bool operator>=(const Impl& x, const Impl& y) {
676  return mpz_cmp(x.d_n, y.d_n) >= 0;
677  }
678 
679  //! Addition
680  friend Impl operator+(const Impl& x, const Impl& y) {
681  Impl res;
682  mpz_add(res.d_n, x.d_n, y.d_n);
683  return res;
684  }
685 
686  //! Subtraction
687  friend Impl operator-(const Impl& x, const Impl& y) {
688  Impl res;
689  mpz_sub(res.d_n, x.d_n, y.d_n);
690  return res;
691  }
692 
693  //! Multiplication
694  friend Impl operator*(const Impl& x, const Impl& y) {
695  Impl res;
696  mpz_mul(res.d_n, x.d_n, y.d_n);
697  return res;
698  }
699 
700  //! Division
701  friend Impl operator/(const Impl& x, const Impl& y) {
702  Impl res;
703  mpz_div(res.d_n, x.d_n, y.d_n);
704  return res;
705  }
706 
707  friend Impl operator%(const Impl& x, const Impl& y) {
708  mpz_t res;
709  mpz_init(res);
710  // Put the remainder directly into 'res'
711  mpz_fdiv_r(res, x.d_n, y.d_n);
712  Impl r(res);
713  mpz_clear(res);
714  return r;
715  }
716 
717  friend Impl operator<<(const Impl& x, unsigned y) {
718  mpz_t res;
719  mpz_init(res);
720  mpz_mul_2exp (res, x.d_n, y);
721  Impl r(res);
722  mpz_clear(res);
723  return r;
724  }
725 
726  friend Impl operator&(const Impl& x, const Impl& y) {
727  mpz_t res;
728  mpz_init(res);
729  mpz_and (res, x.d_n, y.d_n);
730  Impl r(res);
731  mpz_clear(res);
732  return r;
733  }
734 
735  //! Compute the remainder of x/y
736  friend Impl mod(const Impl& x, const Impl& y) {
737  mpz_t res;
738  mpz_init(res);
739  mpz_mod(res, x.d_n, y.d_n);
740  Impl r(res);
741  mpz_clear(res);
742  return r;
743  }
744 
745  friend Impl intRoot(const Impl& x, unsigned long int y) {
746  mpz_t res;
747  mpz_init(res);
748  int exact = mpz_root(res, x.d_n, y);
749  if (!exact) {
750  mpz_set_ui(res, 0);
751  }
752  Impl r(res);
753  mpz_clear(res);
754  return r;
755  }
756 
757  friend Impl gcd(const Impl& x, const Impl& y) {
758  mpz_t res;
759  mpz_init(res);
760  mpz_gcd(res, x.d_n, y.d_n);
761  Impl r(res);
762  mpz_clear(res);
763  return r;
764  }
765 
766  friend Impl lcm(const Impl& x, const Impl& y) {
767  mpz_t res;
768  mpz_init(res);
769  mpz_lcm(res, x.d_n, y.d_n);
770  Impl r(res);
771  mpz_clear(res);
772  return r;
773  }
774 
775  //! Print to string
776  string toString(int base = 10) const {
777  char* str = (char*)malloc(mpz_sizeinbase(d_n, base)+2);
778  mpz_get_str(str, base, d_n);
779  string res(str);
780  free(str);
781  return res;
782  }
783 
784  //! Printing to ostream
785  friend ostream& operator<<(ostream& os, const Unsigned::Impl& n) {
786  return os << n.toString();
787  }
788 
789  };
790 
791  // Constructor from a pair of unsigned integers
792  Unsigned::Impl::Impl(unsigned int n) {
793  mpz_init(d_n);
794  mpz_set_ui(d_n, n);
795  }
796 
797  // Constructor from a string
798  Unsigned::Impl::Impl(const string &n, int base) {
799  mpz_init(d_n);
800  mpz_set_str(d_n, n.c_str(), base);
801  }
802 
803  Unsigned::Impl Unsigned::Impl::operator-() const {
804  Impl res;
805  mpz_neg(res.d_n, d_n);
806  return res;
807  }
808 
809  //! Default constructor
810  Unsigned::Unsigned() : d_n(new Impl) { }
811  //! Copy constructor
812  Unsigned::Unsigned(const Unsigned &n) : d_n(new Impl(*n.d_n)) { }
813 
814  Unsigned::Unsigned(int n) : d_n(new Impl((unsigned)n)) { }
815 
816  Unsigned::Unsigned(unsigned n) : d_n(new Impl(n)) { }
817  //! Private constructor
818  Unsigned::Unsigned(const Impl& t): d_n(new Impl(t)) { }
819  // Constructors from strings
820  Unsigned::Unsigned(const char* n, int base)
821  : d_n(new Impl(string(n), base)) { }
822  Unsigned::Unsigned(const string& n, int base)
823  : d_n(new Impl(n, base)) { }
824  // Destructor
825  Unsigned::~Unsigned() {
826  delete d_n;
827  }
828 
829  // Assignment
830  Unsigned& Unsigned::operator=(const Unsigned& n) {
831  if(this == &n) return *this;
832  delete d_n;
833  d_n = new Impl(*n.d_n);
834  return *this;
835  }
836 
837  ostream &operator<<(ostream &os, const Unsigned &n) {
838  return(os << n.toString());
839  }
840 
841 
842  // Check that argument is an int and print an error message otherwise
843 
844  /* Computes gcd and lcm on *integer* values. Result is always a
845  positive integer. In this implementation, it is guaranteed by
846  GMP. */
847 
848  Unsigned gcd(const Unsigned &x, const Unsigned &y) {
849  return Unsigned(gcd(*x.d_n, *y.d_n));
850  }
851 
852  Unsigned gcd(const vector<Unsigned> &v) {
853  Unsigned::Impl g(1), zero;
854  if(v.size() > 0) {
855  g = *v[0].d_n;
856  }
857  for(size_t i=1; i<v.size(); i++) {
858  if(g == zero)
859  g = *(v[i].d_n);
860  else if(*(v[i].d_n) != zero)
861  g = gcd(g, *(v[i].d_n));
862  }
863  return Unsigned(g);
864  }
865 
866  Unsigned lcm(const Unsigned &x, const Unsigned &y) {
867  return Unsigned(lcm(*x.d_n, *y.d_n));
868  }
869 
870  Unsigned lcm(const vector<Unsigned> &v) {
871  Unsigned::Impl g(1), zero;
872  for(size_t i=0; i<v.size(); i++) {
873  if(*v[i].d_n != zero)
874  g = lcm(g, *v[i].d_n);
875  }
876  return Unsigned(g);
877  }
878 
879  Unsigned mod(const Unsigned &x, const Unsigned &y) {
880  return(Unsigned(mod(*x.d_n, *y.d_n)));
881  }
882 
883  Unsigned intRoot(const Unsigned& base, unsigned long int n) {
884  return Unsigned(intRoot(*base.d_n, n));
885  }
886 
887  string Unsigned::toString(int base) const {
888  return(d_n->toString(base));
889  }
890 
891  size_t Unsigned::hash() const {
893  return h(toString().c_str());
894  }
895 
896  void Unsigned::print() const {
897  cout << (*this) << endl;
898  }
899 
900  Unsigned &Unsigned::operator+=(const Unsigned &n2) {
901  *this = (*this) + n2;
902  return *this;
903  }
904 
905  Unsigned &Unsigned::operator-=(const Unsigned &n2) {
906  *this = (*this) - n2;
907  return *this;
908  }
909 
910  Unsigned &Unsigned::operator*=(const Unsigned &n2) {
911  *this = (*this) * n2;
912  return *this;
913  }
914 
915  Unsigned &Unsigned::operator/=(const Unsigned &n2) {
916  *this = (*this) / n2;
917  return *this;
918  }
919 
920  unsigned long Unsigned::getUnsigned() const {
921  return d_n->getUnsigned();
922  }
923 
924  bool operator==(const Unsigned &n1, const Unsigned &n2) {
925  return(*n1.d_n == *n2.d_n);
926  }
927 
928  bool operator<(const Unsigned &n1, const Unsigned &n2) {
929  return(*n1.d_n < *n2.d_n);
930  }
931 
932  bool operator<=(const Unsigned &n1, const Unsigned &n2) {
933  return(*n1.d_n <= *n2.d_n);
934  }
935 
936  bool operator>(const Unsigned &n1, const Unsigned &n2) {
937  return(*n1.d_n > *n2.d_n);
938  }
939 
940  bool operator>=(const Unsigned &n1, const Unsigned &n2) {
941  return(*n1.d_n >= *n2.d_n);
942  }
943 
944  bool operator!=(const Unsigned &n1, const Unsigned &n2) {
945  return(*n1.d_n != *n2.d_n);
946  }
947 
948  Unsigned operator+(const Unsigned &n1, const Unsigned &n2) {
949  return Unsigned((*n1.d_n) + (*n2.d_n));
950  }
951 
952  Unsigned operator-(const Unsigned &n1, const Unsigned &n2) {
953  return Unsigned((*n1.d_n) - (*n2.d_n));
954  }
955 
956  Unsigned operator*(const Unsigned &n1, const Unsigned &n2) {
957  return Unsigned((*n1.d_n) * (*n2.d_n));
958  }
959 
960  Unsigned operator/(const Unsigned &n1, const Unsigned &n2) {
961  return Unsigned((*n1.d_n) / (*n2.d_n));
962  }
963 
964  Unsigned operator%(const Unsigned &n1, const Unsigned &n2) {
965  return Unsigned((*n1.d_n) % (*n2.d_n));
966  }
967 
968  Unsigned operator<<(const Unsigned &n1, unsigned n2) {
969  return Unsigned((*n1.d_n) << n2);
970  }
971 
972  Unsigned operator&(const Unsigned &n1, const Unsigned &n2) {
973  return Unsigned((*n1.d_n) & (*n2.d_n));
974  }
975 
976  Unsigned Rational::Impl::getUnsignedMP() const {
977  return Unsigned(Unsigned::Impl(mpq_numref(d_n)));
978  }
979 
980 
981 } /* close namespace */
982 
983 #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
T max(T a, T b)
Definition: cvc_util.h:56
STL namespace.
static T min(T x, T y)
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
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
Definition: debug.h:37
T abs(T t)
Definition: cvc_util.h:53
std::string int2string(int n)
Definition: cvc_util.h:46
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
Definition: kinds.h:99