Integer: GMP: Move implementation of member functions to .cpp file. (#5190)

This moves the GMP implementation of member functions of class Integer from
the header to the .cpp file. This only moves code, and adds documentation for
previously undocumented or poorly documented functions.

I ran a performance check on the cluster on non-incremental QF_BV, QF_BVFP,
QF_FP, QF_LIA, QF_LIRA and QF_LRA (BV and FP logics heavily rely on class
Integer since class BitVector is implemented on top of Integer). This change has
no impact on performance.

1 files changed, 122 insertions, 330 deletions

diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index e7c0ee3a4..acd14d8d1 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -65,101 +65,54 @@ class CVC4_PUBLIC Integer
   Integer(uint64_t z) : d_value(static_cast<unsigned long>(z)) {}
 #endif /* CVC4_NEED_INT64_T_OVERLOADS */
 
+  /** Destructor. */
   ~Integer() {}
 
-  /**
-   * Returns a copy of d_value to enable public access of GMP data.
-   */
+  /** Returns a copy of d_value to enable public access of GMP data. */
   const mpz_class& getValue() const { return d_value; }
 
-  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);
-  }
+  /** Overload copy assignment operator. */
+  Integer& operator=(const Integer& x);
+
+  /** Overload equality comparison operator. */
+  bool operator==(const Integer& y) const;
+  /** Overload disequality comparison operator. */
+  bool operator!=(const Integer& y) const;
+  /** Overload less than comparison operator. */
+  bool operator<(const Integer& y) const;
+  /** Overload less than or equal comparison operator. */
+  bool operator<=(const Integer& y) const;
+  /** Overload greater than comparison operator. */
+  bool operator>(const Integer& y) const;
+  /** Overload greater than or equal comparison operator. */
+  bool operator>=(const Integer& y) const;
+
+  /** Overload negation operator. */
+  Integer operator-() const;
+  /** Overload addition operator. */
+  Integer operator+(const Integer& y) const;
+  /** Overload addition assignment operator. */
+  Integer& operator+=(const Integer& y);
+  /** Overload subtraction operator. */
+  Integer operator-(const Integer& y) const;
+  /** Overload subtraction assignment operator. */
+  Integer& operator-=(const Integer& y);
+  /** Overload multiplication operator. */
+  Integer operator*(const Integer& y) const;
+  /** Overload multiplication assignment operator. */
+  Integer& operator*=(const Integer& y);
+
+  /** Return the bit-wise or of this and the given Integer. */
+  Integer bitwiseOr(const Integer& y) const;
+  /** Return the bit-wise and of this and the given Integer. */
+  Integer bitwiseAnd(const Integer& y) const;
+  /** Return the bit-wise exclusive or of this and the given Integer. */
+  Integer bitwiseXor(const Integer& y) const;
+  /** Return the bit-wise not of this Integer. */
+  Integer bitwiseNot() const;
+
+  /** Return this*(2^pow). */
+  Integer multiplyByPow2(uint32_t pow) const;
 
   /**
    * Returns the Integer obtained by setting the ith bit of the
@@ -167,7 +120,8 @@ class CVC4_PUBLIC Integer
    */
   Integer setBit(uint32_t i, bool value) const;
 
-  bool isBitSet(uint32_t i) const { return !extractBitRange(1, i).isZero(); }
+  /** Return true if bit at index 'i' is 1, and false otherwise. */
+  bool isBitSet(uint32_t i) const;
 
   /**
    * Returns the integer with the binary representation of size bits
@@ -175,74 +129,31 @@ class CVC4_PUBLIC Integer
    */
   Integer oneExtend(uint32_t size, uint32_t amount) const;
 
-  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);
-  }
+  uint32_t toUnsignedInt() const;
 
   /**
-   * Returns the floor(this / y)
+   * Extract a range of bits from index 'low' to (excluding) 'low + bitCount'.
+   * Note: corresponds to the extract operator of theory BV.
    */
-  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);
-  }
+  Integer extractBitRange(uint32_t bitCount, uint32_t low) const;
 
-  /**
-   * 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);
-  }
+  /** Returns the floor(this / y) */
+  Integer floorDivideQuotient(const Integer& y) const;
 
-  /**
-   * Computes a floor quotient and remainder for x divided by y.
-   */
+  /** Returns r == this - floor(this/y)*y */
+  Integer floorDivideRemainder(const Integer& y) const;
+
+  /** 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());
-  }
+                      const Integer& y);
 
-  /**
-   * 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 ceilingDivideQuotient(const Integer& y) const;
 
-  /**
-   * 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);
-  }
+  /** Returns the ceil(this / y) */
+  Integer ceilingDivideRemainder(const Integer& y) const;
 
   /**
    * Computes a quotient and remainder according to Boute's Euclidean
@@ -256,139 +167,60 @@ class CVC4_PUBLIC Integer
   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;
-      }
-    }
-  }
+                          const Integer& y);
 
   /**
    * Returns the quotient 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;
-  }
+  Integer euclidianDivideQuotient(const Integer& y) const;
 
   /**
    * Returns the remainder 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;
-  }
+  Integer euclidianDivideRemainder(const Integer& y) const;
 
-  /**
-   * If y divides *this, then exactQuotient returns (this/y)
-   */
+  /** If y divides *this, then exactQuotient returns (this/y). */
   Integer exactQuotient(const Integer& y) const;
 
-  /**
-   * 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 mod 2^exp. */
+  Integer modByPow2(uint32_t exp) const;
 
-  /**
-   * 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);
-  }
+  /** Returns y / 2^exp. */
+  Integer divByPow2(uint32_t exp) const;
 
-  int sgn() const { return mpz_sgn(d_value.get_mpz_t()); }
+  /** Return 1 if this is > 0, 0 if it is 0, and -1 if it is < 0. */
+  int sgn() const;
 
-  inline bool strictlyPositive() const { return sgn() > 0; }
+  /** Return true if this is > 0. */
+  bool strictlyPositive() const;
 
-  inline bool strictlyNegative() const { return sgn() < 0; }
+  /** Return true if this is < 0. */
+  bool strictlyNegative() const;
 
-  inline bool isZero() const { return sgn() == 0; }
+  /** Return true if this is 0. */
+  bool isZero() const;
 
-  bool isOne() const { return mpz_cmp_si(d_value.get_mpz_t(), 1) == 0; }
+  /** Return true if this is 1. */
+  bool isOne() const;
 
-  bool isNegativeOne() const
-  {
-    return mpz_cmp_si(d_value.get_mpz_t(), -1) == 0;
-  }
+  /** Return true if this is -1. */
+  bool isNegativeOne() const;
 
-  /**
-   * 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);
-  }
+  /** Raise this Integer to the power 'exp'. */
+  Integer pow(unsigned long int exp) const;
 
-  /**
-   * 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 greatest common divisor of this integer with another. */
+  Integer gcd(const Integer& y) const;
 
-  /**
-   * 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);
-  }
+  /** Return the least common multiple of this integer with another. */
+  Integer lcm(const Integer& y) const;
 
-  /**
-   * Compute addition of this Integer x + y modulo m.
-   */
+  /** Compute addition of this Integer x + y modulo m. */
   Integer modAdd(const Integer& y, const Integer& m) const;
 
-  /**
-   * Compute multiplication of this Integer x * y modulo m.
-   */
+  /** Compute multiplication of this Integer x * y modulo m. */
   Integer modMultiply(const Integer& y, const Integer& m) const;
 
   /**
@@ -406,59 +238,46 @@ class CVC4_PUBLIC Integer
   Integer modInverse(const Integer& m) const;
 
   /**
-   * All non-zero integers z, z.divide(0)
-   * ! zero.divides(zero)
+   * Return true if 'y' divides this integer.
+   * Note: All non-zero integers devide zero, and zero does not divide 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;
-  }
+  bool divides(const Integer& y) const;
 
-  /**
-   * Return the absolute value of this integer.
-   */
-  Integer abs() const { return d_value >= 0 ? *this : -*this; }
+  /** Return the absolute value of this integer.  */
+  Integer abs() const;
 
-  std::string toString(int base = 10) const { return d_value.get_str(base); }
+  /** Return a string representation of this Integer. */
+  std::string toString(int base = 10) const;
 
+  /** Return true if this Integer fits into a signed int. */
   bool fitsSignedInt() const;
 
+  /** Return true if this Integer fits into an unsigned int. */
   bool fitsUnsignedInt() const;
 
+  /** Return the signed int representation of this Integer. */
   signed int getSignedInt() const;
 
+  /** Return the unsigned int representation of this Integer. */
   unsigned int getUnsignedInt() const;
 
+  /** Return true if this Integer fits into a signed long. */
   bool fitsSignedLong() const;
 
+  /** Return true if this Integer fits into an unsigned long. */
   bool fitsUnsignedLong() 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;
-  }
+  /** Return the signed long representation of this Integer. */
+  long getLong() const;
+
+  /** Return the unsigned long representation of this Integer. */
+  unsigned long getUnsignedLong() const;
 
   /**
    * 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()); }
+  size_t hash() const;
 
   /**
    * Returns true iff bit n is set.
@@ -466,63 +285,36 @@ class CVC4_PUBLIC Integer
    * @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); }
+  bool testBit(unsigned n) const;
 
   /**
    * 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;
-  }
+  unsigned isPow2() const;
 
   /**
    * 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);
-    }
-  }
+  size_t length() const;
 
+  /**
+   * Return the greatest common divisor of a and b, and in addition set s and t
+   * to coefficients satisfying a*s + b*t = g.
+   *
+   * Note: The returned Integer is always positive, even if one or both of a
+   *       and b are negative (or zero if both inputs are zero). For more
+   *       details, see https://gmplib.org/manual/Number-Theoretic-Functions.
+   */
   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());
-  }
+      Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b);
 
   /** Returns a reference to the minimum of two integers. */
-  static const Integer& min(const Integer& a, const Integer& b)
-  {
-    return (a <= b) ? a : b;
-  }
+  static const Integer& min(const Integer& a, const Integer& 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;
-  }
+  static const Integer& max(const Integer& a, const Integer& b);
 
  private:
   /**