CVC3

rational.h

Go to the documentation of this file.
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