Integer: CLN: Move implementation of member functions to .cpp file. (#5304)

This moves the CLN 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.

Analogous to #5190.

1 files changed, 434 insertions, 70 deletions

diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp
index 6293544ff..05293529c 100644
--- a/src/util/integer_cln_imp.cpp
+++ b/src/util/integer_cln_imp.cpp
@@ -14,16 +14,14 @@
  ** [[ Add lengthier description here ]]
  ** \todo document this file
  **/
-#include "util/integer.h"
-
 #include <sstream>
 #include <string>
 
 #include "cvc4autoconfig.h"
-
+#include "util/integer.h"
 
 #ifndef CVC4_CLN_IMP
-#  error "This source should only ever be built if CVC4_CLN_IMP is on !"
+#error "This source should only ever be built if CVC4_CLN_IMP is on !"
 #endif /* CVC4_CLN_IMP */
 
 #include "base/check.h"
@@ -32,17 +30,117 @@ using namespace std;
 
 namespace CVC4 {
 
-signed int Integer::s_fastSignedIntMin = -(1<<29);
-signed int Integer::s_fastSignedIntMax = (1<<29)-1;
-signed long Integer::s_slowSignedIntMin = (signed long) std::numeric_limits<signed int>::min();
-signed long Integer::s_slowSignedIntMax =  (signed long) std::numeric_limits<signed int>::max();
+signed int Integer::s_fastSignedIntMin = -(1 << 29);
+signed int Integer::s_fastSignedIntMax = (1 << 29) - 1;
+signed long Integer::s_slowSignedIntMin =
+    (signed long)std::numeric_limits<signed int>::min();
+signed long Integer::s_slowSignedIntMax =
+    (signed long)std::numeric_limits<signed int>::max();
 
-unsigned int Integer::s_fastUnsignedIntMax = (1<<29)-1;
-unsigned long Integer::s_slowUnsignedIntMax =  (unsigned long) std::numeric_limits<unsigned int>::max();
+unsigned int Integer::s_fastUnsignedIntMax = (1 << 29) - 1;
+unsigned long Integer::s_slowUnsignedIntMax =
+    (unsigned long)std::numeric_limits<unsigned int>::max();
+
+unsigned long Integer::s_signedLongMin =
+    std::numeric_limits<signed long>::min();
+unsigned long Integer::s_signedLongMax =
+    std::numeric_limits<signed long>::max();
+unsigned long Integer::s_unsignedLongMax =
+    std::numeric_limits<unsigned long>::max();
+
+Integer& Integer::operator=(const Integer& x)
+{
+  if (this == &x) return *this;
+  d_value = x.d_value;
+  return *this;
+}
+
+bool Integer::operator==(const Integer& y) const
+{
+  return d_value == y.d_value;
+}
+
+Integer Integer::operator-() const { return Integer(-(d_value)); }
+
+bool Integer::operator!=(const Integer& y) const
+{
+  return d_value != y.d_value;
+}
 
-unsigned long Integer::s_signedLongMin = std::numeric_limits<signed long>::min();
-unsigned long Integer::s_signedLongMax = std::numeric_limits<signed long>::max();
-unsigned long Integer::s_unsignedLongMax = std::numeric_limits<unsigned long>::max();
+bool Integer::operator<(const Integer& y) const { return d_value < y.d_value; }
+
+bool Integer::operator<=(const Integer& y) const
+{
+  return d_value <= y.d_value;
+}
+
+bool Integer::operator>(const Integer& y) const { return d_value > y.d_value; }
+
+bool Integer::operator>=(const Integer& y) const
+{
+  return d_value >= y.d_value;
+}
+
+Integer Integer::operator+(const Integer& y) const
+{
+  return Integer(d_value + y.d_value);
+}
+
+Integer& Integer::operator+=(const Integer& y)
+{
+  d_value += y.d_value;
+  return *this;
+}
+
+Integer Integer::operator-(const Integer& y) const
+{
+  return Integer(d_value - y.d_value);
+}
+
+Integer& Integer::operator-=(const Integer& y)
+{
+  d_value -= y.d_value;
+  return *this;
+}
+
+Integer Integer::operator*(const Integer& y) const
+{
+  return Integer(d_value * y.d_value);
+}
+
+Integer& Integer::operator*=(const Integer& y)
+{
+  d_value *= y.d_value;
+  return *this;
+}
+
+Integer Integer::bitwiseOr(const Integer& y) const
+{
+  return Integer(cln::logior(d_value, y.d_value));
+}
+
+Integer Integer::bitwiseAnd(const Integer& y) const
+{
+  return Integer(cln::logand(d_value, y.d_value));
+}
+
+Integer Integer::bitwiseXor(const Integer& y) const
+{
+  return Integer(cln::logxor(d_value, y.d_value));
+}
+
+Integer Integer::bitwiseNot() const { return Integer(cln::lognot(d_value)); }
+
+Integer Integer::multiplyByPow2(uint32_t pow) const
+{
+  cln::cl_I ipow(pow);
+  return Integer(d_value << ipow);
+}
+
+bool Integer::isBitSet(uint32_t i) const
+{
+  return !extractBitRange(1, i).isZero();
+}
 
 Integer Integer::setBit(uint32_t i, bool value) const
 {
@@ -53,41 +151,252 @@ Integer Integer::setBit(uint32_t i, bool value) const
   return Integer(cln::logand(d_value, mask));
 }
 
-Integer Integer::oneExtend(uint32_t size, uint32_t amount) const {
+Integer Integer::oneExtend(uint32_t size, uint32_t amount) const
+{
   DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size);
   cln::cl_byte range(amount, size);
-  cln::cl_I allones = (cln::cl_I(1) << (size + amount))- 1; // 2^size - 1
+  cln::cl_I allones = (cln::cl_I(1) << (size + amount)) - 1;  // 2^size - 1
   Integer temp(allones);
 
   return Integer(cln::deposit_field(allones, d_value, range));
 }
 
-Integer Integer::exactQuotient(const Integer& y) const {
+uint32_t Integer::toUnsignedInt() const { return cln::cl_I_to_uint(d_value); }
+
+Integer Integer::extractBitRange(uint32_t bitCount, uint32_t low) const
+{
+  cln::cl_byte range(bitCount, low);
+  return Integer(cln::ldb(d_value, range));
+}
+
+Integer Integer::floorDivideQuotient(const Integer& y) const
+{
+  return Integer(cln::floor1(d_value, y.d_value));
+}
+
+Integer Integer::floorDivideRemainder(const Integer& y) const
+{
+  return Integer(cln::floor2(d_value, y.d_value).remainder);
+}
+
+void Integer::floorQR(Integer& q,
+                      Integer& r,
+                      const Integer& x,
+                      const Integer& y)
+{
+  cln::cl_I_div_t res = cln::floor2(x.d_value, y.d_value);
+  q.d_value = res.quotient;
+  r.d_value = res.remainder;
+}
+
+Integer Integer::ceilingDivideQuotient(const Integer& y) const
+{
+  return Integer(cln::ceiling1(d_value, y.d_value));
+}
+
+Integer Integer::ceilingDivideRemainder(const Integer& y) const
+{
+  return Integer(cln::ceiling2(d_value, y.d_value).remainder);
+}
+
+void Integer::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;
+    }
+  }
+}
+
+Integer Integer::euclidianDivideQuotient(const Integer& y) const
+{
+  Integer q, r;
+  euclidianQR(q, r, *this, y);
+  return q;
+}
+
+Integer Integer::euclidianDivideRemainder(const Integer& y) const
+{
+  Integer q, r;
+  euclidianQR(q, r, *this, y);
+  return r;
+}
+
+Integer Integer::exactQuotient(const Integer& y) const
+{
   DebugCheckArgument(y.divides(*this), y);
-  return Integer( cln::exquo(d_value, y.d_value) );
+  return Integer(cln::exquo(d_value, y.d_value));
+}
+
+Integer Integer::modByPow2(uint32_t exp) const
+{
+  cln::cl_byte range(exp, 0);
+  return Integer(cln::ldb(d_value, range));
+}
+
+Integer Integer::divByPow2(uint32_t exp) const { return d_value >> exp; }
+
+Integer Integer::pow(unsigned long int exp) const
+{
+  if (exp == 0)
+  {
+    return Integer(1);
+  }
+  else
+  {
+    Assert(exp > 0);
+    cln::cl_I result = cln::expt_pos(d_value, exp);
+    return Integer(result);
+  }
+}
+
+Integer Integer::gcd(const Integer& y) const
+{
+  cln::cl_I result = cln::gcd(d_value, y.d_value);
+  return Integer(result);
+}
+
+Integer Integer::lcm(const Integer& y) const
+{
+  cln::cl_I result = cln::lcm(d_value, y.d_value);
+  return Integer(result);
+}
+
+Integer Integer::modAdd(const Integer& y, const Integer& m) const
+{
+  cln::cl_modint_ring ry = cln::find_modint_ring(m.d_value);
+  cln::cl_MI xm = ry->canonhom(d_value);
+  cln::cl_MI ym = ry->canonhom(y.d_value);
+  cln::cl_MI res = xm + ym;
+  return Integer(ry->retract(res));
 }
 
+Integer Integer::modMultiply(const Integer& y, const Integer& m) const
+{
+  cln::cl_modint_ring ry = cln::find_modint_ring(m.d_value);
+  cln::cl_MI xm = ry->canonhom(d_value);
+  cln::cl_MI ym = ry->canonhom(y.d_value);
+  cln::cl_MI res = xm * ym;
+  return Integer(ry->retract(res));
+}
+
+Integer Integer::modInverse(const Integer& m) const
+{
+  PrettyCheckArgument(m > 0, m, "m must be greater than zero");
+  cln::cl_modint_ring ry = cln::find_modint_ring(m.d_value);
+  cln::cl_MI xm = ry->canonhom(d_value);
+  /* normalize to modulo m for coprime check */
+  cln::cl_I x = ry->retract(xm);
+  if (x == 0 || cln::gcd(x, m.d_value) != 1)
+  {
+    return Integer(-1);
+  }
+  cln::cl_MI res = cln::recip(xm);
+  return Integer(ry->retract(res));
+}
+
+bool Integer::divides(const Integer& y) const
+{
+  cln::cl_I result = cln::rem(y.d_value, d_value);
+  return cln::zerop(result);
+}
+
+Integer Integer::abs() const { return d_value >= 0 ? *this : -*this; }
+
+std::string Integer::toString(int base) const
+{
+  std::stringstream ss;
+  switch (base)
+  {
+    case 2: fprintbinary(ss, d_value); break;
+    case 8: fprintoctal(ss, d_value); break;
+    case 10: fprintdecimal(ss, d_value); break;
+    case 16: fprinthexadecimal(ss, d_value); break;
+    default: throw Exception("Unhandled base in Integer::toString()");
+  }
+  std::string output = ss.str();
+  for (unsigned i = 0; i <= output.length(); ++i)
+  {
+    if (isalpha(output[i]))
+    {
+      output.replace(i, 1, 1, tolower(output[i]));
+    }
+  }
+
+  return output;
+}
+
+int Integer::sgn() const
+{
+  cln::cl_I sgn = cln::signum(d_value);
+  return cln::cl_I_to_int(sgn);
+}
+
+bool Integer::strictlyPositive() const { return sgn() > 0; }
+
+bool Integer::strictlyNegative() const { return sgn() < 0; }
+
+bool Integer::isZero() const { return sgn() == 0; }
+
+bool Integer::isOne() const { return d_value == 1; }
+
+bool Integer::isNegativeOne() const { return d_value == -1; }
+
 void Integer::parseInt(const std::string& s, unsigned base)
 {
   cln::cl_read_flags flags;
   flags.syntax = cln::syntax_integer;
   flags.lsyntax = cln::lsyntax_standard;
   flags.rational_base = base;
-  if(base == 0) {
+  if (base == 0)
+  {
     // infer base in a manner consistent with GMP
-    if(s[0] == '0') {
+    if (s[0] == '0')
+    {
       flags.lsyntax = cln::lsyntax_commonlisp;
       std::string st = s;
-      if(s[1] == 'X' || s[1] == 'x') {
+      if (s[1] == 'X' || s[1] == 'x')
+      {
         st.replace(0, 2, "#x");
-      } else if(s[1] == 'B' || s[1] == 'b') {
+      }
+      else if (s[1] == 'B' || s[1] == 'b')
+      {
         st.replace(0, 2, "#b");
-      } else {
+      }
+      else
+      {
         st.replace(0, 1, "#o");
       }
       readInt(flags, st, base);
       return;
-    } else {
+    }
+    else
+    {
       flags.rational_base = 10;
     }
   }
@@ -98,104 +407,159 @@ void Integer::readInt(const cln::cl_read_flags& flags,
                       const std::string& s,
                       unsigned base)
 {
-  try {
+  try
+  {
     // Removing leading zeroes, CLN has a bug for these inputs up to and
     // including CLN v1.3.2.
-    // See http://www.ginac.de/CLN/cln.git/?a=commit;h=4a477b0cc3dd7fbfb23b25090ff8c8869c8fa21a for details.
+    // See
+    // http://www.ginac.de/CLN/cln.git/?a=commit;h=4a477b0cc3dd7fbfb23b25090ff8c8869c8fa21a
+    // for details.
     size_t pos = s.find_first_not_of('0');
-    if(pos == std::string::npos) {
+    if (pos == std::string::npos)
+    {
       d_value = read_integer(flags, "0", NULL, NULL);
-    } else {
+    }
+    else
+    {
       const char* cstr = s.c_str();
       const char* start = cstr + pos;
       const char* end = cstr + s.length();
       d_value = read_integer(flags, start, end, NULL);
     }
-  } catch(...) {
+  }
+  catch (...)
+  {
     std::stringstream ss;
     ss << "Integer() failed to parse value \"" << s << "\" in base " << base;
     throw std::invalid_argument(ss.str());
   }
 }
 
-bool Integer::fitsSignedInt() const {
+bool Integer::fitsSignedInt() const
+{
   // http://www.ginac.de/CLN/cln.html#Conversions
   // TODO improve performance
   Assert(s_slowSignedIntMin <= s_fastSignedIntMin);
   Assert(s_fastSignedIntMin <= s_fastSignedIntMax);
   Assert(s_fastSignedIntMax <= s_slowSignedIntMax);
 
-  return (d_value <= s_fastSignedIntMax || d_value <= s_slowSignedIntMax) &&
-    (d_value >= s_fastSignedIntMin || d_value >= s_slowSignedIntMax);
+  return (d_value <= s_fastSignedIntMax || d_value <= s_slowSignedIntMax)
+         && (d_value >= s_fastSignedIntMin || d_value >= s_slowSignedIntMax);
 }
 
-bool Integer::fitsUnsignedInt() const {
+bool Integer::fitsUnsignedInt() const
+{
   // TODO improve performance
   Assert(s_fastUnsignedIntMax <= s_slowUnsignedIntMax);
-  return sgn() >= 0 &&
-    (d_value <= s_fastUnsignedIntMax || d_value <= s_slowUnsignedIntMax);
+  return sgn() >= 0
+         && (d_value <= s_fastUnsignedIntMax
+             || d_value <= s_slowUnsignedIntMax);
 }
 
-signed int Integer::getSignedInt() const {
+signed int Integer::getSignedInt() const
+{
   // ensure there isn't overflow
-  CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getSignedInt()");
+  CheckArgument(
+      fitsSignedInt(), this, "Overflow detected in Integer::getSignedInt()");
   return cln::cl_I_to_int(d_value);
 }
 
-unsigned int Integer::getUnsignedInt() const {
+unsigned int Integer::getUnsignedInt() const
+{
   // ensure there isn't overflow
-  CheckArgument(fitsUnsignedInt(), this, "Overflow detected in Integer::getUnsignedInt()");
+  CheckArgument(fitsUnsignedInt(),
+                this,
+                "Overflow detected in Integer::getUnsignedInt()");
   return cln::cl_I_to_uint(d_value);
 }
 
-bool Integer::fitsSignedLong() const {
+bool Integer::fitsSignedLong() const
+{
   return d_value <= s_signedLongMax && d_value >= s_signedLongMin;
 }
 
-bool Integer::fitsUnsignedLong() const {
+bool Integer::fitsUnsignedLong() const
+{
   return sgn() >= 0 && d_value <= s_unsignedLongMax;
 }
 
-Integer Integer::pow(unsigned long int exp) const {
-  if (exp == 0) {
-    return Integer(1);
-  } else {
-    Assert(exp > 0);
-    cln::cl_I result = cln::expt_pos(d_value, exp);
-    return Integer(result);
-  }
+long Integer::getLong() const
+{
+  // ensure there isn't overflow
+  CheckArgument(d_value <= std::numeric_limits<long>::max(),
+                this,
+                "Overflow detected in Integer::getLong()");
+  CheckArgument(d_value >= std::numeric_limits<long>::min(),
+                this,
+                "Overflow detected in Integer::getLong()");
+  return cln::cl_I_to_long(d_value);
 }
 
-Integer Integer::modAdd(const Integer& y, const Integer& m) const
+unsigned long Integer::getUnsignedLong() const
 {
-  cln::cl_modint_ring ry = cln::find_modint_ring(m.d_value);
-  cln::cl_MI xm = ry->canonhom(d_value);
-  cln::cl_MI ym = ry->canonhom(y.d_value);
-  cln::cl_MI res = xm + ym;
-  return Integer(ry->retract(res));
+  // ensure there isn't overflow
+  CheckArgument(d_value <= std::numeric_limits<unsigned long>::max(),
+                this,
+                "Overflow detected in Integer::getUnsignedLong()");
+  CheckArgument(d_value >= std::numeric_limits<unsigned long>::min(),
+                this,
+                "Overflow detected in Integer::getUnsignedLong()");
+  return cln::cl_I_to_ulong(d_value);
 }
 
-Integer Integer::modMultiply(const Integer& y, const Integer& m) const
+size_t Integer::hash() const { return equal_hashcode(d_value); }
+
+bool Integer::testBit(unsigned n) const { return cln::logbitp(n, d_value); }
+
+unsigned Integer::isPow2() const
 {
-  cln::cl_modint_ring ry = cln::find_modint_ring(m.d_value);
-  cln::cl_MI xm = ry->canonhom(d_value);
-  cln::cl_MI ym = ry->canonhom(y.d_value);
-  cln::cl_MI res = xm * ym;
-  return Integer(ry->retract(res));
+  if (d_value <= 0) return 0;
+  // power2p returns n such that d_value = 2^(n-1)
+  return cln::power2p(d_value);
 }
 
-Integer Integer::modInverse(const Integer& m) const
+size_t Integer::length() const
 {
-  PrettyCheckArgument(m > 0, m, "m must be greater than zero");
-  cln::cl_modint_ring ry = cln::find_modint_ring(m.d_value);
-  cln::cl_MI xm = ry->canonhom(d_value);
-  /* normalize to modulo m for coprime check */
-  cln::cl_I x = ry->retract(xm);
-  if (x == 0 || cln::gcd(x, m.d_value) != 1)
+  int s = sgn();
+  if (s == 0)
   {
-    return Integer(-1);
+    return 1;
   }
-  cln::cl_MI res = cln::recip(xm);
-  return Integer(ry->retract(res));
+  else if (s < 0)
+  {
+    size_t len = cln::integer_length(d_value);
+    /*If this is -2^n, return len+1 not len to stay consistent with the
+     * definition above! From CLN's documentation of integer_length: This is
+     * the smallest n >= 0 such that -2^n <= x < 2^n. If x > 0, this is the
+     * unique n > 0 such that 2^(n-1) <= x < 2^n.
+     */
+    size_t ord2 = cln::ord2(d_value);
+    return (len == ord2) ? (len + 1) : len;
+  }
+  else
+  {
+    return cln::integer_length(d_value);
+  }
+}
+
+void Integer::extendedGcd(
+    Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b)
+{
+  g.d_value = cln::xgcd(a.d_value, b.d_value, &s.d_value, &t.d_value);
+}
+
+const Integer& Integer::min(const Integer& a, const Integer& b)
+{
+  return (a <= b) ? a : b;
+}
+
+const Integer& Integer::max(const Integer& a, const Integer& b)
+{
+  return (a >= b) ? a : b;
+}
+
+std::ostream& operator<<(std::ostream& os, const Integer& n)
+{
+  return os << n.toString();
 }
 } /* namespace CVC4 */