text: /*********************                                                        */
  /*! \file integer_gmp_imp.h
   ** \verbatim
   ** Original author: Tim King
   ** Major contributors: Morgan Deters, Liana Hadarean
   ** Minor contributors (to current version): Dejan Jovanovic
   ** This file is part of the CVC4 project.
   ** Copyright (c) 2009-2014  New York University and The University of Iowa
   ** See the file COPYING in the top-level source directory for licensing
   ** information.\endverbatim
   **
   ** \brief A multiprecision integer constant; wraps a GMP multiprecision
   ** integer.
   **
   ** A multiprecision integer constant; wraps a GMP multiprecision integer.
   **/
  
  #include "cvc4_public.h"
  
  #ifndef __CVC4__INTEGER_H
  #define __CVC4__INTEGER_H
  
  #include <string>
  #include <iostream>
  #include <limits>
  
  #include "util/gmp_util.h"
  #include "util/exception.h"
  
  namespace CVC4 {
  
  class Rational;
  
  class CVC4_PUBLIC Integer {
  private:
    /**
     * Stores the value of the rational is stored in a C++ GMP integer class.
     * Using this instead of mpz_t allows for easier destruction.
     */
    mpz_class d_value;
  
    /**
     * Gets a reference to the gmp data that backs up the integer.
     * Only accessible to friend classes.
     */
    const mpz_class& get_mpz() const { return d_value; }
  
    /**
     * Constructs an Integer by copying a GMP C++ primitive.
     */
    Integer(const mpz_class& val) : d_value(val) {}
  
  public:
  
    /** Constructs a rational with the value 0. */
    Integer() : d_value(0){}
  
    /**
     * Constructs a Integer from a C string.
     * Throws std::invalid_argument if the string is not a valid rational.
     * For more information about what is a valid rational string,
     * see GMP's documentation for mpq_set_str().
     */
    explicit Integer(const char* s, unsigned base = 10);
    explicit Integer(const std::string& s, unsigned base = 10);
  
    Integer(const Integer& q) : d_value(q.d_value) {}
  
    Integer(  signed int z) : d_value(z) {}
    Integer(unsigned int z) : d_value(z) {}
    Integer(  signed long int z) : d_value(z) {}
    Integer(unsigned long int z) : d_value(z) {}
  
  #ifdef CVC4_NEED_INT64_T_OVERLOADS
    Integer( int64_t z) : d_value(static_cast<long>(z)) {}
    Integer(uint64_t z) : d_value(static_cast<unsigned long>(z)) {}
  #endif /* CVC4_NEED_INT64_T_OVERLOADS */
  
    ~Integer() {}
  
    Integer& operator=(const Integer& x){
      if(this == &x) return *this;
      d_value = x.d_value;
      return *this;
    }
  
    bool operator==(const Integer& y) const {
      return d_value == y.d_value;
    }
  
    Integer operator-() const {
      return Integer(-(d_value));
    }
  
  
    bool operator!=(const Integer& y) const {
      return d_value != y.d_value;
    }
  
    bool operator< (const Integer& y) const {
      return d_value < y.d_value;
    }
  
    bool operator<=(const Integer& y) const {
      return d_value <= y.d_value;
    }
  
    bool operator> (const Integer& y) const {
      return d_value > y.d_value;
    }
  
    bool operator>=(const Integer& y) const {
      return d_value >= y.d_value;
    }
  
  
    Integer operator+(const Integer& y) const {
      return Integer( d_value + y.d_value );
    }
    Integer& operator+=(const Integer& y) {
      d_value += y.d_value;
      return *this;
    }
  
    Integer operator-(const Integer& y) const {
      return Integer( d_value - y.d_value );
    }
    Integer& operator-=(const Integer& y) {
      d_value -= y.d_value;
      return *this;
    }
  
    Integer operator*(const Integer& y) const {
      return Integer( d_value * y.d_value );
    }
    Integer& operator*=(const Integer& y) {
      d_value *= y.d_value;
      return *this;
    }
  
  
    Integer bitwiseOr(const Integer& y) const {
      mpz_class result;
      mpz_ior(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
      return Integer(result);
    }
  
    Integer bitwiseAnd(const Integer& y) const {
      mpz_class result;
      mpz_and(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
      return Integer(result);
    }
  
    Integer bitwiseXor(const Integer& y) const {
      mpz_class result;
      mpz_xor(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
      return Integer(result);
    }
  
    Integer bitwiseNot() const {
      mpz_class result;
      mpz_com(result.get_mpz_t(), d_value.get_mpz_t());
      return Integer(result);
    }
  
    /**
     * Return this*(2^pow).
     */
    Integer multiplyByPow2(uint32_t pow) const{
      mpz_class result;
      mpz_mul_2exp(result.get_mpz_t(), d_value.get_mpz_t(), pow);
      return Integer( result );
    }
  
    /**
     * Returns the Integer obtained by setting the ith bit of the
     * current Integer to 1.
     */
    Integer setBit(uint32_t i) const {
      mpz_class res = d_value;
      mpz_setbit(res.get_mpz_t(), i);
      return Integer(res);
    }
  
    bool isBitSet(uint32_t i) const {
      return !extractBitRange(1, i).isZero();
    }
  
    /**
     * Returns the integer with the binary representation of size bits
     * extended with amount 1's
     */
    Integer oneExtend(uint32_t size, uint32_t amount) const {
      // check that the size is accurate
      DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size);
      mpz_class res = d_value;
  
      for (unsigned i = size; i < size + amount; ++i) {
        mpz_setbit(res.get_mpz_t(), i);
      }
  
      return Integer(res);
    }
  
    uint32_t toUnsignedInt() const {
      return  mpz_get_ui(d_value.get_mpz_t());
    }
  
    /** See GMP Documentation. */
    Integer extractBitRange(uint32_t bitCount, uint32_t low) const {
      // bitCount = high-low+1
      uint32_t high = low + bitCount-1;
      //— Function: void mpz_fdiv_r_2exp (mpz_t r, mpz_t n, mp_bitcnt_t b)
      mpz_class rem, div;
      mpz_fdiv_r_2exp(rem.get_mpz_t(), d_value.get_mpz_t(), high+1);
      mpz_fdiv_q_2exp(div.get_mpz_t(), rem.get_mpz_t(), low);
  
      return Integer(div);
    }
  
    /**
     * Returns the floor(this / y)
     */
    Integer floorDivideQuotient(const Integer& y) const {
      mpz_class q;
      mpz_fdiv_q(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
      return Integer( q );
    }
  
    /**
     * Returns r == this - floor(this/y)*y
     */
    Integer floorDivideRemainder(const Integer& y) const {
      mpz_class r;
      mpz_fdiv_r(r.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
      return Integer( r );
    }
  
    /**
     * Computes a floor quotient and remainder for x divided by y.
     */
    static void floorQR(Integer& q, Integer& r, const Integer& x, const Integer& y) {
      mpz_fdiv_qr(q.d_value.get_mpz_t(), r.d_value.get_mpz_t(), x.d_value.get_mpz_t(), y.d_value.get_mpz_t());
    }
  
    /**
     * Returns the ceil(this / y)
     */
    Integer ceilingDivideQuotient(const Integer& y) const {
      mpz_class q;
      mpz_cdiv_q(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
      return Integer( q );
    }
  
    /**
     * Returns the ceil(this / y)
     */
    Integer ceilingDivideRemainder(const Integer& y) const {
      mpz_class r;
      mpz_cdiv_r(r.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
      return Integer( r );
    }
  
    /**
     * Computes a quoitent and remainder according to Boute's Euclidean definition.
     * euclidianDivideQuotient, euclidianDivideRemainder.
     *
     * Boute, Raymond T. (April 1992).
     * The Euclidean definition of the functions div and mod.
     * ACM Transactions on Programming Languages and Systems (TOPLAS)
     * ACM Press. 14 (2): 127 - 144. doi:10.1145/128861.128862.
     */
    static void euclidianQR(Integer& q, Integer& r, const Integer& x, const Integer& y) {
      // compute the floor and then fix the value up if needed.
      floorQR(q,r,x,y);
  
      if(r.strictlyNegative()){
        // if r < 0
        // abs(r) < abs(y)
        // - abs(y) < r < 0, then 0 < r + abs(y) < abs(y)
        // n = y * q + r
        // n = y * q - abs(y) + r + abs(y)
        if(r.sgn() >= 0){
          // y = abs(y)
          // n = y * q - y + r + y
          // n = y * (q-1) + (r+y)
          q -= 1;
          r += y;
        }else{
          // y = -abs(y)
          // n = y * q + y + r - y
          // n = y * (q+1) + (r-y)
          q += 1;
          r -= y;
        }
      }
    }
    /**
     * Returns the quoitent according to Boute's Euclidean definition.
     * See the documentation for euclidianQR.
     */
    Integer euclidianDivideQuotient(const Integer& y) const {
      Integer q,r;
      euclidianQR(q,r, *this, y);
      return q;
    }
  
    /**
     * Returns the remainfing according to Boute's Euclidean definition.
     * See the documentation for euclidianQR.
     */
    Integer euclidianDivideRemainder(const Integer& y) const {
      Integer q,r;
      euclidianQR(q,r, *this, y);
      return r;
    }
  
  
    /**
     * If y divides *this, then exactQuotient returns (this/y)
     */
    Integer exactQuotient(const Integer& y) const {
      DebugCheckArgument(y.divides(*this), y);
      mpz_class q;
      mpz_divexact(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
      return Integer( q );
    }
  
    /**
     * Returns y mod 2^exp
     */
    Integer modByPow2(uint32_t exp) const {
      mpz_class res;
      mpz_fdiv_r_2exp(res.get_mpz_t(), d_value.get_mpz_t(), exp);
      return Integer(res);
    }
  
    /**
     * Returns y / 2^exp
     */
    Integer divByPow2(uint32_t exp) const {
      mpz_class res;
      mpz_fdiv_q_2exp(res.get_mpz_t(), d_value.get_mpz_t(), exp);
      return Integer(res);
    }
  
  
    int sgn() const {
      return mpz_sgn(d_value.get_mpz_t());
    }
  
    inline bool strictlyPositive() const {
      return sgn() > 0;
    }
  
    inline bool strictlyNegative() const {
      return sgn() < 0;
    }
  
    inline bool isZero() const {
      return sgn() == 0;
    }
  
    bool isOne() const {
      return mpz_cmp_si(d_value.get_mpz_t(), 1) == 0;
    }
  
    bool isNegativeOne() const {
      return mpz_cmp_si(d_value.get_mpz_t(), -1) == 0;
    }
  
    /**
     * Raise this Integer to the power <code>exp</code>.
     *
     * @param exp the exponent
     */
    Integer pow(unsigned long int exp) const {
      mpz_class result;
      mpz_pow_ui(result.get_mpz_t(),d_value.get_mpz_t(),exp);
      return Integer( result );
    }
  
    /**
     * Return the greatest common divisor of this integer with another.
     */
    Integer gcd(const Integer& y) const {
      mpz_class result;
      mpz_gcd(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
      return Integer(result);
    }
  
    /**
     * Return the least common multiple of this integer with another.
     */
    Integer lcm(const Integer& y) const {
      mpz_class result;
      mpz_lcm(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
      return Integer(result);
    }
  
    /**
     * All non-zero integers z, z.divide(0)
     * ! zero.divides(zero)
     */
    bool divides(const Integer& y) const {
      int res = mpz_divisible_p(y.d_value.get_mpz_t(), d_value.get_mpz_t());
      return res != 0;
    }
  
    /**
     * Return the absolute value of this integer.
     */
    Integer abs() const {
      return d_value >= 0 ? *this : -*this;
    }
  
    std::string toString(int base = 10) const{
      return d_value.get_str(base);
    }
  
    bool fitsSignedInt() const;
  
    bool fitsUnsignedInt() const;
  
    signed int getSignedInt() const;
  
    unsigned int getUnsignedInt() const;
  
    long getLong() const {
      long si = d_value.get_si();
      // ensure there wasn't overflow
      CheckArgument(mpz_cmp_si(d_value.get_mpz_t(), si) == 0, this,
                   "Overflow detected in Integer::getLong()");
      return si;
    }
    unsigned long getUnsignedLong() const {
      unsigned long ui = d_value.get_ui();
      // ensure there wasn't overflow
      CheckArgument(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0, this,
                    "Overflow detected in Integer::getUnsignedLong()");
      return ui;
    }
  
    /**
     * Computes the hash of the node from the first word of the
     * numerator, the denominator.
     */
    size_t hash() const {
      return gmpz_hash(d_value.get_mpz_t());
    }
  
    /**
     * Returns true iff bit n is set.
     *
     * @param n the bit to test (0 == least significant bit)
     * @return true if bit n is set in this integer; false otherwise
     */
    bool testBit(unsigned n) const {
      return mpz_tstbit(d_value.get_mpz_t(), n);
    }
  
    /**
     * Returns k if the integer is equal to 2^(k-1)
     * @return k if the integer is equal to 2^(k-1) and 0 otherwise
     */
    unsigned isPow2() const {
      if (d_value <= 0) return 0;
      // check that the number of ones in the binary representation is 1
      if (mpz_popcount(d_value.get_mpz_t()) == 1) {
        // return the index of the first one plus 1
        return mpz_scan1(d_value.get_mpz_t(), 0) + 1;
      }
      return 0; 
    }
  
    
    /**
     * If x != 0, returns the smallest n s.t. 2^{n-1} <= abs(x) < 2^{n}.
     * If x == 0, returns 1.
     */
    size_t length() const {
      if(sgn() == 0){
        return 1;
      }else{
        return mpz_sizeinbase(d_value.get_mpz_t(),2);
      }
    }
  
    static void extendedGcd(Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b){
      //see the documentation for:
      //mpz_gcdext (mpz_t g, mpz_t s, mpz_t t, mpz_t a, mpz_t b);
      mpz_gcdext (g.d_value.get_mpz_t(), s.d_value.get_mpz_t(), t.d_value.get_mpz_t(), a.d_value.get_mpz_t(), b.d_value.get_mpz_t());
    }
  
    /** Returns a reference to the minimum of two integers. */
    static const Integer& min(const Integer& a, const Integer& b){
      return (a <=b ) ? a : b;
    }
  
    /** Returns a reference to the maximum of two integers. */
    static const Integer& max(const Integer& a, const Integer& b){
      return (a >= b ) ? a : b;
    }
  
    friend class CVC4::Rational;
  };/* class Integer */
  
  struct IntegerHashFunction {
    inline size_t operator()(const CVC4::Integer& i) const {
      return i.hash();
    }
  };/* struct IntegerHashFunction */
  
  inline std::ostream& operator<<(std::ostream& os, const Integer& n) {
    return os << n.toString();
  }
  
  }/* CVC4 namespace */
  
  #endif /* __CVC4__INTEGER_H */
  