src/util/integer_gmp_imp.h

   1 /*********************                                                        */
   2 /*! \file integer_gmp_imp.h
   3  ** \verbatim
   4  ** Original author: taking
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief A multiprecision integer constant; wraps a GMP multiprecision
  15  ** integer.
  16  **
  17  ** A multiprecision integer constant; wraps a GMP multiprecision integer.
  18  **/
  19
  20 #include "cvc4_public.h"
  21
  22 #ifndef __CVC4__INTEGER_H
  23 #define __CVC4__INTEGER_H
  24
  25 #include <string>
  26 #include <iostream>
  27 #include "util/gmp_util.h"
  28
  29 namespace CVC4 {
  30
  31 class Rational;
  32
  33 class Integer {
  34 private:
  35   /**
  36    * Stores the value of the rational is stored in a C++ GMP integer class.
  37    * Using this instead of mpz_t allows for easier destruction.
  38    */
  39   mpz_class d_value;
  40
  41   /**
  42    * Gets a reference to the gmp data that backs up the integer.
  43    * Only accessible to friend classes.
  44    */
  45   const mpz_class& get_mpz() const { return d_value; }
  46
  47   /**
  48    * Constructs an Integer by copying a GMP C++ primitive.
  49    */
  50   Integer(const mpz_class& val) : d_value(val) {}
  51
  52 public:
  53
  54   /** Constructs a rational with the value 0. */
  55   Integer() : d_value(0){}
  56
  57   /**
  58    * Constructs a Integer from a C string.
  59    * Throws std::invalid_argument if the string is not a valid rational.
  60    * For more information about what is a valid rational string,
  61    * see GMP's documentation for mpq_set_str().
  62    */
  63   explicit Integer(const char * s, int base = 10): d_value(s,base) {}
  64   Integer(const std::string& s, unsigned base = 10) : d_value(s, base) {}
  65
  66   Integer(const Integer& q) : d_value(q.d_value) {}
  67
  68   Integer(  signed int z) : d_value(z) {}
  69   Integer(unsigned int z) : d_value(z) {}
  70   Integer(  signed long int z) : d_value(z) {}
  71   Integer(unsigned long int z) : d_value(z) {}
  72
  73   ~Integer() {}
  74
  75
  76   Integer& operator=(const Integer& x){
  77     if(this == &x) return *this;
  78     d_value = x.d_value;
  79     return *this;
  80   }
  81
  82   bool operator==(const Integer& y) const {
  83     return d_value == y.d_value;
  84   }
  85
  86   Integer operator-() const{
  87     return Integer(-(d_value));
  88   }
  89
  90
  91   bool operator!=(const Integer& y) const {
  92     return d_value != y.d_value;
  93   }
  94
  95   bool operator< (const Integer& y) const {
  96     return d_value < y.d_value;
  97   }
  98
  99   bool operator<=(const Integer& y) const {
 100     return d_value <= y.d_value;
 101   }
 102
 103   bool operator> (const Integer& y) const {
 104     return d_value > y.d_value;
 105   }
 106
 107   bool operator>=(const Integer& y) const {
 108     return d_value >= y.d_value;
 109   }
 110
 111
 112   Integer operator+(const Integer& y) const{
 113     return Integer( d_value + y.d_value );
 114   }
 115
 116   Integer operator-(const Integer& y) const {
 117     return Integer( d_value - y.d_value );
 118   }
 119
 120   Integer operator*(const Integer& y) const {
 121     return Integer( d_value * y.d_value );
 122   }
 123   Integer operator/(const Integer& y) const {
 124     return Integer( d_value / y.d_value );
 125   }
 126   Integer operator%(const Integer& y) const {
 127     return Integer( d_value % y.d_value );
 128   }
 129
 130   /** Raise this Integer to the power <code>exp</code>.
 131    *
 132    * @param exp the exponent
 133    */
 134   Integer pow(unsigned long int exp) const {
 135     mpz_class result;
 136     mpz_pow_ui(result.get_mpz_t(),d_value.get_mpz_t(),exp);
 137     return Integer( result );
 138   }
 139
 140   std::string toString(int base = 10) const{
 141     return d_value.get_str(base);
 142   }
 143
 144   //friend std::ostream& operator<<(std::ostream& os, const Integer& n);
 145
 146   long getLong() const { return d_value.get_si(); }
 147   unsigned long getUnsignedLong() const {return d_value.get_ui(); }
 148
 149   /**
 150    * Computes the hash of the node from the first word of the
 151    * numerator, the denominator.
 152    */
 153   size_t hash() const {
 154     return gmpz_hash(d_value.get_mpz_t());
 155   }
 156
 157   friend class CVC4::Rational;
 158 };/* class Integer */
 159
 160 struct IntegerHashStrategy {
 161   static inline size_t hash(const CVC4::Integer& i) {
 162     return i.hash();
 163   }
 164 };/* struct IntegerHashStrategy */
 165
 166 std::ostream& operator<<(std::ostream& os, const Integer& n);
 167
 168 }/* CVC4 namespace */
 169
 170 #endif /* __CVC4__INTEGER_H */
 171