CVC3
|
00001 /*****************************************************************************/ 00002 /*! 00003 * \file rational.h 00004 * 00005 * Author: Sergey Berezin 00006 * 00007 * Created: Dec 12 22:00:18 GMT 2002 00008 * 00009 * <hr> 00010 * 00011 * License to use, copy, modify, sell and/or distribute this software 00012 * and its documentation for any purpose is hereby granted without 00013 * royalty, subject to the terms and conditions defined in the \ref 00014 * LICENSE file provided with this distribution. 00015 * 00016 * <hr> 00017 * 00018 */ 00019 /*****************************************************************************/ 00020 // Class: Rational 00021 // Author: Sergey Berezin, 12/12/2002 (adapted from Bignum) 00022 // 00023 // Description: This is an abstration of a rational with arbitrary 00024 // precision. It provides a constructor from a pair of ints and 00025 // strings, overloaded operator{+,-,*,/}, assignment, etc. The 00026 // current implementation uses GMP mpq_class. 00027 /////////////////////////////////////////////////////////////////////////////// 00028 00029 #ifndef _cvc3__rational_h_ 00030 #define _cvc3__rational_h_ 00031 00032 // Do not include <gmpxx.h> here; it contains some depricated C++ 00033 // headers. We only include it in the .cpp file. 00034 00035 #include <vector> 00036 #include "debug.h" 00037 00038 // To be defined only in bignum.cpp 00039 namespace CVC3 { 00040 00041 class Unsigned; 00042 00043 class CVC_DLL Rational { 00044 friend class Unsigned; 00045 private: 00046 class Impl; 00047 Impl *d_n; 00048 // Debugging 00049 #ifdef _DEBUG_RATIONAL_ 00050 // Encapsulate static values in a function to guarantee 00051 // initialization when we need it 00052 int& getCreated() { 00053 static int num_created = 0; 00054 return(num_created); 00055 } 00056 00057 int& getDeleted() { 00058 static int num_deleted = 0; 00059 return(num_deleted); 00060 } 00061 00062 void printStats(); 00063 #endif 00064 // Private constructor (for internal consumption only) 00065 Rational(const Impl& t); 00066 00067 public: 00068 // Constructors 00069 Rational(); 00070 // Copy constructor 00071 Rational(const Rational &n); 00072 Rational(const Unsigned& n); 00073 Rational(int n, int d = 1); 00074 Rational(const char* n, int base = 10); 00075 Rational(const std::string& n, int base = 10); 00076 Rational(const char* n, const char* d, int base = 10); 00077 Rational(const std::string& n, const std::string& d, int base = 10); 00078 // Destructor 00079 ~Rational(); 00080 00081 // Assignment 00082 Rational& operator=(const Rational& n); 00083 00084 std::string toString(int base = 10) const; 00085 00086 // Compute hash value (for DAG expression representation) 00087 size_t hash() const; 00088 00089 friend CVC_DLL bool operator==(const Rational &n1, const Rational &n2); 00090 friend CVC_DLL bool operator<(const Rational &n1, const Rational &n2); 00091 friend CVC_DLL bool operator<=(const Rational &n1, const Rational &n2); 00092 friend CVC_DLL bool operator>(const Rational &n1, const Rational &n2); 00093 friend CVC_DLL bool operator>=(const Rational &n1, const Rational &n2); 00094 friend CVC_DLL bool operator!=(const Rational &n1, const Rational &n2); 00095 friend CVC_DLL Rational operator+(const Rational &n1, const Rational &n2); 00096 friend CVC_DLL Rational operator-(const Rational &n1, const Rational &n2); 00097 friend CVC_DLL Rational operator*(const Rational &n1, const Rational &n2); 00098 friend CVC_DLL Rational operator/(const Rational &n1, const Rational &n2); 00099 // 'mod' operator, defined only for integer values of n1 and n2 00100 friend CVC_DLL Rational operator%(const Rational &n1, const Rational &n2); 00101 00102 // Unary minus 00103 Rational operator-() const; 00104 Rational &operator+=(const Rational &n2); 00105 Rational &operator-=(const Rational &n2); 00106 Rational &operator*=(const Rational &n2); 00107 Rational &operator/=(const Rational &n2); 00108 //! Prefix increment 00109 const Rational& operator++() { *this = (*this)+1; return *this; } 00110 //! Postfix increment 00111 Rational operator++(int) { Rational x(*this); *this = x+1; return x; } 00112 //! Prefix decrement 00113 const Rational& operator--() { *this = (*this)-1; return *this; } 00114 //! Postfix decrement 00115 Rational operator--(int) { Rational x(*this); *this = x-1; return x; } 00116 00117 // Result is integer 00118 Rational getNumerator() const; 00119 Rational getDenominator() const; 00120 00121 // Equivalent to (getDenominator() == 1), but possibly more efficient 00122 bool isInteger() const; 00123 // Convert to int; defined only on integer values 00124 int getInt() const; 00125 // Equivalent to (*this >= 0 && isInteger()) 00126 bool isUnsigned() const { return (isInteger() && (*this) >= 0); } 00127 // Convert to unsigned int; defined only on non-negative integer values 00128 unsigned int getUnsigned() const; 00129 Unsigned getUnsignedMP() const; 00130 00131 friend std::ostream &operator<<(std::ostream &os, const Rational &n); 00132 friend std::ostream &operator<<(std::ostream &os, const Impl &n); 00133 00134 /* Computes gcd and lcm on *integer* values. Result is always a 00135 positive integer. */ 00136 00137 friend CVC_DLL Rational gcd(const Rational &x, const Rational &y); 00138 friend CVC_DLL Rational gcd(const std::vector<Rational> &v); 00139 friend CVC_DLL Rational lcm(const Rational &x, const Rational &y); 00140 friend CVC_DLL Rational lcm(const std::vector<Rational> &v); 00141 00142 friend CVC_DLL Rational abs(const Rational &x); 00143 00144 //! Compute the floor of x (result is an integer) 00145 friend CVC_DLL Rational floor(const Rational &x); 00146 //! Compute the ceiling of x (result is an integer) 00147 friend CVC_DLL Rational ceil(const Rational &x); 00148 //! Compute non-negative remainder for *integer* x,y. 00149 friend CVC_DLL Rational mod(const Rational &x, const Rational &y); 00150 //! nth root: return 0 if no exact answer (base should be nonzero) 00151 friend CVC_DLL Rational intRoot(const Rational& base, unsigned long int n); 00152 00153 // For debugging, to be able to print in gdb 00154 void print() const; 00155 00156 }; // Rational class 00157 00158 //! Raise 'base' into the power of 'pow' (pow must be an integer) 00159 inline Rational pow(Rational pow, const Rational& base) { 00160 DebugAssert(pow.isInteger(), "pow("+pow.toString() 00161 +", "+base.toString()+")"); 00162 FatalAssert(base != 0 || pow >= 0, "Attempt to divide by zero"); 00163 bool neg(pow < 0); 00164 if(neg) pow = -pow; 00165 Rational res(1); 00166 for(; pow > 0; --pow) res *= base; 00167 if(neg) res = 1/res; 00168 return res; 00169 } 00170 //! take nth root of base, return result if it is exact, 0 otherwise 00171 // base should not be 0 00172 inline Rational ratRoot(const Rational& base, unsigned long int n) 00173 { 00174 DebugAssert(base != 0, "Expected nonzero base"); 00175 Rational num = base.getNumerator(); 00176 num = intRoot(num, n); 00177 if (num != 0) { 00178 Rational den = base.getDenominator(); 00179 den = intRoot(den, n); 00180 if (den != 0) { 00181 return num / den; 00182 } 00183 } 00184 return 0; 00185 } 00186 00187 // Methods creating new Rational values, similar to the 00188 // constructors, but can be nested 00189 inline Rational newRational(int n, int d = 1) { return Rational(n, d); } 00190 inline Rational newRational(const char* n, int base = 10) 00191 { return Rational(n, base); } 00192 inline Rational newRational(const std::string& n, int base = 10) 00193 { return Rational(n, base); } 00194 inline Rational newRational(const char* n, const char* d, int base = 10) 00195 { return Rational(n, d, base); } 00196 inline Rational newRational(const std::string& n, const std::string& d, 00197 int base = 10) 00198 { return Rational(n, d, base); } 00199 00200 // Debugging print 00201 void printRational(const Rational &x); 00202 00203 class CVC_DLL Unsigned { 00204 private: 00205 friend class Rational::Impl; 00206 class Impl; 00207 Impl *d_n; 00208 00209 // Private constructor (for internal consumption only) 00210 Unsigned(const Impl& t); 00211 00212 public: 00213 // Constructors 00214 Unsigned(); 00215 // Copy constructor 00216 Unsigned(const Unsigned &n); 00217 Unsigned(int n); 00218 Unsigned(unsigned n); 00219 Unsigned(const char* n, int base = 10); 00220 Unsigned(const std::string& n, int base = 10); 00221 // Destructor 00222 ~Unsigned(); 00223 00224 // Assignment 00225 Unsigned& operator=(const Unsigned& n); 00226 00227 std::string toString(int base = 10) const; 00228 00229 // Compute hash value (for DAG expression representation) 00230 size_t hash() const; 00231 00232 friend CVC_DLL bool operator==(const Unsigned &n1, const Unsigned &n2); 00233 friend CVC_DLL bool operator<(const Unsigned &n1, const Unsigned &n2); 00234 friend CVC_DLL bool operator<=(const Unsigned &n1, const Unsigned &n2); 00235 friend CVC_DLL bool operator>(const Unsigned &n1, const Unsigned &n2); 00236 friend CVC_DLL bool operator>=(const Unsigned &n1, const Unsigned &n2); 00237 friend CVC_DLL bool operator!=(const Unsigned &n1, const Unsigned &n2); 00238 friend CVC_DLL Unsigned operator+(const Unsigned &n1, const Unsigned &n2); 00239 friend CVC_DLL Unsigned operator-(const Unsigned &n1, const Unsigned &n2); 00240 friend CVC_DLL Unsigned operator*(const Unsigned &n1, const Unsigned &n2); 00241 friend CVC_DLL Unsigned operator/(const Unsigned &n1, const Unsigned &n2); 00242 // 'mod' operator, defined only for integer values of n1 and n2 00243 friend CVC_DLL Unsigned operator%(const Unsigned &n1, const Unsigned &n2); 00244 00245 friend CVC_DLL Unsigned operator<<(const Unsigned& n1, unsigned n2); 00246 friend CVC_DLL Unsigned operator&(const Unsigned& n1, const Unsigned& n2); 00247 00248 Unsigned &operator+=(const Unsigned &n2); 00249 Unsigned &operator-=(const Unsigned &n2); 00250 Unsigned &operator*=(const Unsigned &n2); 00251 Unsigned &operator/=(const Unsigned &n2); 00252 //! Prefix increment 00253 const Unsigned& operator++() { *this = (*this)+1; return *this; } 00254 //! Postfix increment 00255 Unsigned operator++(int) { Unsigned x(*this); *this = x+1; return x; } 00256 //! Prefix decrement 00257 const Unsigned& operator--() { *this = (*this)-1; return *this; } 00258 //! Postfix decrement 00259 Unsigned operator--(int) { Unsigned x(*this); *this = x-1; return x; } 00260 00261 // Convert to unsigned int if possible 00262 unsigned long getUnsigned() const; 00263 00264 friend std::ostream &operator<<(std::ostream &os, const Unsigned &n); 00265 00266 /* Computes gcd and lcm on *integer* values. Result is always a 00267 positive integer. */ 00268 00269 friend CVC_DLL Unsigned gcd(const Unsigned &x, const Unsigned &y); 00270 friend CVC_DLL Unsigned gcd(const std::vector<Unsigned> &v); 00271 friend CVC_DLL Unsigned lcm(const Unsigned &x, const Unsigned &y); 00272 friend CVC_DLL Unsigned lcm(const std::vector<Unsigned> &v); 00273 00274 //! Compute non-negative remainder for *integer* x,y. 00275 friend CVC_DLL Unsigned mod(const Unsigned &x, const Unsigned &y); 00276 //! nth root: return 0 if no exact answer (base should be nonzero) 00277 friend CVC_DLL Unsigned intRoot(const Unsigned& base, unsigned long int n); 00278 00279 // For debugging, to be able to print in gdb 00280 void print() const; 00281 00282 }; // Unsigned class 00283 00284 //! Raise 'base' into the power of 'pow' (pow must be an integer) 00285 inline Unsigned pow(Unsigned pow, const Unsigned& base) { 00286 Unsigned res(1); 00287 for(; pow > (unsigned)0; --pow) res *= base; 00288 return res; 00289 } 00290 00291 // Methods creating new Unsigned values, similar to the 00292 // constructors, but can be nested 00293 inline Unsigned newUnsigned(int n) { return Unsigned(n); } 00294 inline Unsigned newUnsigned(const char* n, int base = 10) 00295 { return Unsigned(n, base); } 00296 inline Unsigned newUnsigned(const std::string& n, int base = 10) 00297 { return Unsigned(n, base); } 00298 00299 // Debugging print 00300 void printUnsigned(const Unsigned &x); 00301 00302 } // end of namespace CVC3 00303 00304 #endif