CVC3
rational.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file rational.h
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: This is an abstration of a rational with arbitrary
24 // precision. It provides a constructor from a pair of ints and
25 // strings, overloaded operator{+,-,*,/}, assignment, etc. The
26 // current implementation uses GMP mpq_class.
27 ///////////////////////////////////////////////////////////////////////////////
28 
29 #ifndef _cvc3__rational_h_
30 #define _cvc3__rational_h_
31 
32 // Do not include <gmpxx.h> here; it contains some depricated C++
33 // headers. We only include it in the .cpp file.
34 
35 #include <vector>
36 #include "debug.h"
37 
38 // To be defined only in bignum.cpp
39 namespace CVC3 {
40 
41  class Unsigned;
42 
43  class CVC_DLL Rational {
44  friend class Unsigned;
45  private:
46  class Impl;
47  Impl *d_n;
48  // Debugging
49 #ifdef _DEBUG_RATIONAL_
50  // Encapsulate static values in a function to guarantee
51  // initialization when we need it
52  int& getCreated() {
53  static int num_created = 0;
54  return(num_created);
55  }
56 
57  int& getDeleted() {
58  static int num_deleted = 0;
59  return(num_deleted);
60  }
61 
62  void printStats();
63 #endif
64  // Private constructor (for internal consumption only)
65  Rational(const Impl& t);
66 
67  public:
68  // Constructors
69  Rational();
70  // Copy constructor
71  Rational(const Rational &n);
72  Rational(const Unsigned& n);
73  Rational(int n, int d = 1);
74  Rational(const char* n, int base = 10);
75  Rational(const std::string& n, int base = 10);
76  Rational(const char* n, const char* d, int base = 10);
77  Rational(const std::string& n, const std::string& d, int base = 10);
78  // Destructor
79  ~Rational();
80 
81  // Assignment
82  Rational& operator=(const Rational& n);
83 
84  std::string toString(int base = 10) const;
85 
86  // Compute hash value (for DAG expression representation)
87  size_t hash() const;
88 
89  friend CVC_DLL bool operator==(const Rational &n1, const Rational &n2);
90  friend CVC_DLL bool operator<(const Rational &n1, const Rational &n2);
91  friend CVC_DLL bool operator<=(const Rational &n1, const Rational &n2);
92  friend CVC_DLL bool operator>(const Rational &n1, const Rational &n2);
93  friend CVC_DLL bool operator>=(const Rational &n1, const Rational &n2);
94  friend CVC_DLL bool operator!=(const Rational &n1, const Rational &n2);
95  friend CVC_DLL Rational operator+(const Rational &n1, const Rational &n2);
96  friend CVC_DLL Rational operator-(const Rational &n1, const Rational &n2);
97  friend CVC_DLL Rational operator*(const Rational &n1, const Rational &n2);
98  friend CVC_DLL Rational operator/(const Rational &n1, const Rational &n2);
99  // 'mod' operator, defined only for integer values of n1 and n2
100  friend CVC_DLL Rational operator%(const Rational &n1, const Rational &n2);
101 
102  // Unary minus
103  Rational operator-() const;
104  Rational &operator+=(const Rational &n2);
105  Rational &operator-=(const Rational &n2);
106  Rational &operator*=(const Rational &n2);
107  Rational &operator/=(const Rational &n2);
108  //! Prefix increment
109  const Rational& operator++() { *this = (*this)+1; return *this; }
110  //! Postfix increment
111  Rational operator++(int) { Rational x(*this); *this = x+1; return x; }
112  //! Prefix decrement
113  const Rational& operator--() { *this = (*this)-1; return *this; }
114  //! Postfix decrement
115  Rational operator--(int) { Rational x(*this); *this = x-1; return x; }
116 
117  // Result is integer
118  Rational getNumerator() const;
119  Rational getDenominator() const;
120 
121  // Equivalent to (getDenominator() == 1), but possibly more efficient
122  bool isInteger() const;
123  // Convert to int; defined only on integer values
124  int getInt() const;
125  // Equivalent to (*this >= 0 && isInteger())
126  bool isUnsigned() const { return (isInteger() && (*this) >= 0); }
127  // Convert to unsigned int; defined only on non-negative integer values
128  unsigned int getUnsigned() const;
129  Unsigned getUnsignedMP() const;
130 
131  friend std::ostream &operator<<(std::ostream &os, const Rational &n);
132  friend std::ostream &operator<<(std::ostream &os, const Impl &n);
133 
134  /* Computes gcd and lcm on *integer* values. Result is always a
135  positive integer. */
136 
137  friend CVC_DLL Rational gcd(const Rational &x, const Rational &y);
138  friend CVC_DLL Rational gcd(const std::vector<Rational> &v);
139  friend CVC_DLL Rational lcm(const Rational &x, const Rational &y);
140  friend CVC_DLL Rational lcm(const std::vector<Rational> &v);
141 
142  friend CVC_DLL Rational abs(const Rational &x);
143 
144  //! Compute the floor of x (result is an integer)
145  friend CVC_DLL Rational floor(const Rational &x);
146  //! Compute the ceiling of x (result is an integer)
147  friend CVC_DLL Rational ceil(const Rational &x);
148  //! Compute non-negative remainder for *integer* x,y.
149  friend CVC_DLL Rational mod(const Rational &x, const Rational &y);
150  //! nth root: return 0 if no exact answer (base should be nonzero)
151  friend CVC_DLL Rational intRoot(const Rational& base, unsigned long int n);
152 
153  // For debugging, to be able to print in gdb
154  void print() const;
155 
156  }; // Rational class
157 
158  //! Raise 'base' into the power of 'pow' (pow must be an integer)
159  inline Rational pow(Rational pow, const Rational& base) {
160  DebugAssert(pow.isInteger(), "pow("+pow.toString()
161  +", "+base.toString()+")");
162  FatalAssert(base != 0 || pow >= 0, "Attempt to divide by zero");
163  bool neg(pow < 0);
164  if(neg) pow = -pow;
165  Rational res(1);
166  for(; pow > 0; --pow) res *= base;
167  if(neg) res = 1/res;
168  return res;
169  }
170  //! take nth root of base, return result if it is exact, 0 otherwise
171  // base should not be 0
172  inline Rational ratRoot(const Rational& base, unsigned long int n)
173  {
174  DebugAssert(base != 0, "Expected nonzero base");
175  Rational num = base.getNumerator();
176  num = intRoot(num, n);
177  if (num != 0) {
178  Rational den = base.getDenominator();
179  den = intRoot(den, n);
180  if (den != 0) {
181  return num / den;
182  }
183  }
184  return 0;
185  }
186 
187  // Methods creating new Rational values, similar to the
188  // constructors, but can be nested
189  inline Rational newRational(int n, int d = 1) { return Rational(n, d); }
190  inline Rational newRational(const char* n, int base = 10)
191  { return Rational(n, base); }
192  inline Rational newRational(const std::string& n, int base = 10)
193  { return Rational(n, base); }
194  inline Rational newRational(const char* n, const char* d, int base = 10)
195  { return Rational(n, d, base); }
196  inline Rational newRational(const std::string& n, const std::string& d,
197  int base = 10)
198  { return Rational(n, d, base); }
199 
200  // Debugging print
201  void printRational(const Rational &x);
202 
204  private:
205  friend class Rational::Impl;
206  class Impl;
207  Impl *d_n;
208 
209  // Private constructor (for internal consumption only)
210  Unsigned(const Impl& t);
211 
212  public:
213  // Constructors
214  Unsigned();
215  // Copy constructor
216  Unsigned(const Unsigned &n);
217  Unsigned(int n);
218  Unsigned(unsigned n);
219  Unsigned(const char* n, int base = 10);
220  Unsigned(const std::string& n, int base = 10);
221  // Destructor
222  ~Unsigned();
223 
224  // Assignment
225  Unsigned& operator=(const Unsigned& n);
226 
227  std::string toString(int base = 10) const;
228 
229  // Compute hash value (for DAG expression representation)
230  size_t hash() const;
231 
232  friend CVC_DLL bool operator==(const Unsigned &n1, const Unsigned &n2);
233  friend CVC_DLL bool operator<(const Unsigned &n1, const Unsigned &n2);
234  friend CVC_DLL bool operator<=(const Unsigned &n1, const Unsigned &n2);
235  friend CVC_DLL bool operator>(const Unsigned &n1, const Unsigned &n2);
236  friend CVC_DLL bool operator>=(const Unsigned &n1, const Unsigned &n2);
237  friend CVC_DLL bool operator!=(const Unsigned &n1, const Unsigned &n2);
238  friend CVC_DLL Unsigned operator+(const Unsigned &n1, const Unsigned &n2);
239  friend CVC_DLL Unsigned operator-(const Unsigned &n1, const Unsigned &n2);
240  friend CVC_DLL Unsigned operator*(const Unsigned &n1, const Unsigned &n2);
241  friend CVC_DLL Unsigned operator/(const Unsigned &n1, const Unsigned &n2);
242  // 'mod' operator, defined only for integer values of n1 and n2
243  friend CVC_DLL Unsigned operator%(const Unsigned &n1, const Unsigned &n2);
244 
245  friend CVC_DLL Unsigned operator<<(const Unsigned& n1, unsigned n2);
246  friend CVC_DLL Unsigned operator&(const Unsigned& n1, const Unsigned& n2);
247 
248  Unsigned &operator+=(const Unsigned &n2);
249  Unsigned &operator-=(const Unsigned &n2);
250  Unsigned &operator*=(const Unsigned &n2);
251  Unsigned &operator/=(const Unsigned &n2);
252  //! Prefix increment
253  const Unsigned& operator++() { *this = (*this)+1; return *this; }
254  //! Postfix increment
255  Unsigned operator++(int) { Unsigned x(*this); *this = x+1; return x; }
256  //! Prefix decrement
257  const Unsigned& operator--() { *this = (*this)-1; return *this; }
258  //! Postfix decrement
259  Unsigned operator--(int) { Unsigned x(*this); *this = x-1; return x; }
260 
261  // Convert to unsigned int if possible
262  unsigned long getUnsigned() const;
263 
264  friend std::ostream &operator<<(std::ostream &os, const Unsigned &n);
265 
266  /* Computes gcd and lcm on *integer* values. Result is always a
267  positive integer. */
268 
269  friend CVC_DLL Unsigned gcd(const Unsigned &x, const Unsigned &y);
270  friend CVC_DLL Unsigned gcd(const std::vector<Unsigned> &v);
271  friend CVC_DLL Unsigned lcm(const Unsigned &x, const Unsigned &y);
272  friend CVC_DLL Unsigned lcm(const std::vector<Unsigned> &v);
273 
274  //! Compute non-negative remainder for *integer* x,y.
275  friend CVC_DLL Unsigned mod(const Unsigned &x, const Unsigned &y);
276  //! nth root: return 0 if no exact answer (base should be nonzero)
277  friend CVC_DLL Unsigned intRoot(const Unsigned& base, unsigned long int n);
278 
279  // For debugging, to be able to print in gdb
280  void print() const;
281 
282  }; // Unsigned class
283 
284  //! Raise 'base' into the power of 'pow' (pow must be an integer)
285  inline Unsigned pow(Unsigned pow, const Unsigned& base) {
286  Unsigned res(1);
287  for(; pow > (unsigned)0; --pow) res *= base;
288  return res;
289  }
290 
291  // Methods creating new Unsigned values, similar to the
292  // constructors, but can be nested
293  inline Unsigned newUnsigned(int n) { return Unsigned(n); }
294  inline Unsigned newUnsigned(const char* n, int base = 10)
295  { return Unsigned(n, base); }
296  inline Unsigned newUnsigned(const std::string& n, int base = 10)
297  { return Unsigned(n, base); }
298 
299  // Debugging print
300  void printUnsigned(const Unsigned &x);
301 
302 } // end of namespace CVC3
303 
304 #endif