CVC3 2.2
|
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 CVC_DLL Rational { 00042 private: 00043 class Impl; 00044 Impl *d_n; 00045 // Debugging 00046 #ifdef _DEBUG_RATIONAL_ 00047 // Encapsulate static values in a function to guarantee 00048 // initialization when we need it 00049 int& getCreated() { 00050 static int num_created = 0; 00051 return(num_created); 00052 } 00053 00054 int& getDeleted() { 00055 static int num_deleted = 0; 00056 return(num_deleted); 00057 } 00058 00059 void printStats(); 00060 #endif 00061 // Private constructor (for internal consumption only) 00062 Rational(const Impl& t); 00063 00064 public: 00065 // Constructors 00066 Rational(); 00067 // Copy constructor 00068 Rational(const Rational &n); 00069 Rational(int n, int d = 1); 00070 Rational(const char* n, int base = 10); 00071 Rational(const std::string& n, int base = 10); 00072 Rational(const char* n, const char* d, int base = 10); 00073 Rational(const std::string& n, const std::string& d, int base = 10); 00074 // Destructor 00075 ~Rational(); 00076 00077 // Assignment 00078 Rational& operator=(const Rational& n); 00079 00080 std::string toString(int base = 10) const; 00081 00082 // Compute hash value (for DAG expression representation) 00083 size_t hash() const; 00084 00085 friend CVC_DLL bool operator==(const Rational &n1, const Rational &n2); 00086 friend CVC_DLL bool operator<(const Rational &n1, const Rational &n2); 00087 friend CVC_DLL bool operator<=(const Rational &n1, const Rational &n2); 00088 friend CVC_DLL bool operator>(const Rational &n1, const Rational &n2); 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 Rational operator+(const Rational &n1, const Rational &n2); 00092 friend CVC_DLL Rational operator-(const Rational &n1, const Rational &n2); 00093 friend CVC_DLL Rational operator*(const Rational &n1, const Rational &n2); 00094 friend CVC_DLL Rational operator/(const Rational &n1, const Rational &n2); 00095 // 'mod' operator, defined only for integer values of n1 and n2 00096 friend CVC_DLL Rational operator%(const Rational &n1, const Rational &n2); 00097 00098 // Unary minus 00099 Rational operator-() const; 00100 Rational &operator+=(const Rational &n2); 00101 Rational &operator-=(const Rational &n2); 00102 Rational &operator*=(const Rational &n2); 00103 Rational &operator/=(const Rational &n2); 00104 //! Prefix increment 00105 const Rational& operator++() { *this = (*this)+1; return *this; } 00106 //! Postfix increment 00107 Rational operator++(int) { Rational x(*this); *this = x+1; return x; } 00108 //! Prefix decrement 00109 const Rational& operator--() { *this = (*this)-1; return *this; } 00110 //! Postfix decrement 00111 Rational operator--(int) { Rational x(*this); *this = x-1; return x; } 00112 00113 // Result is integer 00114 Rational getNumerator() const; 00115 Rational getDenominator() const; 00116 00117 // Equivalent to (getDenominator() == 1), but possibly more efficient 00118 bool isInteger() const; 00119 // Convert to int; defined only on integer values 00120 int getInt() const; 00121 // Equivalent to (*this >= 0 && isInteger()) 00122 bool isUnsigned() const { return (isInteger() && (*this) >= 0); } 00123 // Convert to unsigned int; defined only on non-negative integer values 00124 unsigned int getUnsigned() const; 00125 00126 friend std::ostream &operator<<(std::ostream &os, const Rational &n); 00127 00128 /* Computes gcd and lcm on *integer* values. Result is always a 00129 positive integer. */ 00130 00131 friend CVC_DLL Rational gcd(const Rational &x, const Rational &y); 00132 friend CVC_DLL Rational gcd(const std::vector<Rational> &v); 00133 friend CVC_DLL Rational lcm(const Rational &x, const Rational &y); 00134 friend CVC_DLL Rational lcm(const std::vector<Rational> &v); 00135 00136 friend CVC_DLL Rational abs(const Rational &x); 00137 00138 //! Compute the floor of x (result is an integer) 00139 friend CVC_DLL Rational floor(const Rational &x); 00140 //! Compute the ceiling of x (result is an integer) 00141 friend CVC_DLL Rational ceil(const Rational &x); 00142 //! Compute non-negative remainder for *integer* x,y. 00143 friend CVC_DLL Rational mod(const Rational &x, const Rational &y); 00144 //! nth root: return 0 if no exact answer (base should be nonzero) 00145 friend CVC_DLL Rational intRoot(const Rational& base, unsigned long int n); 00146 00147 // For debugging, to be able to print in gdb 00148 void print() const; 00149 00150 }; // Rational class 00151 00152 //! Raise 'base' into the power of 'pow' (pow must be an integer) 00153 inline Rational pow(Rational pow, const Rational& base) { 00154 DebugAssert(pow.isInteger(), "pow("+pow.toString() 00155 +", "+base.toString()+")"); 00156 FatalAssert(base != 0 || pow >= 0, "Attempt to divide by zero"); 00157 bool neg(pow < 0); 00158 if(neg) pow = -pow; 00159 Rational res(1); 00160 for(; pow > 0; --pow) res *= base; 00161 if(neg) res = 1/res; 00162 return res; 00163 } 00164 //! take nth root of base, return result if it is exact, 0 otherwise 00165 // base should not be 0 00166 inline Rational ratRoot(const Rational& base, unsigned long int n) 00167 { 00168 DebugAssert(base != 0, "Expected nonzero base"); 00169 Rational num = base.getNumerator(); 00170 num = intRoot(num, n); 00171 if (num != 0) { 00172 Rational den = base.getDenominator(); 00173 den = intRoot(den, n); 00174 if (den != 0) { 00175 return num / den; 00176 } 00177 } 00178 return 0; 00179 } 00180 00181 // Methods creating new Rational values, similar to the 00182 // constructors, but can be nested 00183 inline Rational newRational(int n, int d = 1) { return Rational(n, d); } 00184 inline Rational newRational(const char* n, int base = 10) 00185 { return Rational(n, base); } 00186 inline Rational newRational(const std::string& n, int base = 10) 00187 { return Rational(n, base); } 00188 inline Rational newRational(const char* n, const char* d, int base = 10) 00189 { return Rational(n, d, base); } 00190 inline Rational newRational(const std::string& n, const std::string& d, 00191 int base = 10) 00192 { return Rational(n, d, base); } 00193 00194 // Debugging print 00195 void printRational(const Rational &x); 00196 00197 // TODO: implement this properly 00198 typedef unsigned long Unsigned; 00199 00200 } // end of namespace CVC3 00201 00202 #endif