Add explicit 64bit getters for Integer class (#7728)

This PR addresses a few issues on our 32bit builds. Most importantly, it adds int64_t Integer::getSigned64() and uint64_t Integer::getUnsigned64().

1 files changed, 74 insertions, 12 deletions

diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp
index f33a90408..f1d927d09 100644
--- a/src/util/integer_gmp_imp.cpp
+++ b/src/util/integer_gmp_imp.cpp
@@ -14,6 +14,7 @@
  */
 
 #include <cmath>
+#include <limits>
 #include <sstream>
 #include <string>
 
@@ -38,6 +39,33 @@ Integer::Integer(const std::string& s, unsigned base)
   : d_value(s, base)
 {}
 
+#ifdef CVC5_NEED_INT64_T_OVERLOADS
+Integer::Integer(int64_t z)
+{
+  if (std::numeric_limits<signed long int>::min() <= z
+      && z <= std::numeric_limits<signed long int>::max())
+  {
+    d_value = static_cast<signed long int>(z);
+  }
+  else
+  {
+    d_value = std::to_string(z);
+  }
+}
+Integer::Integer(uint64_t z)
+{
+  if (std::numeric_limits<unsigned long int>::min() <= z
+      && z <= std::numeric_limits<unsigned long int>::max())
+  {
+    d_value = static_cast<unsigned long int>(z);
+  }
+  else
+  {
+    d_value = std::to_string(z);
+  }
+}
+#endif /* CVC5_NEED_INT64_T_OVERLOADS */
+
 Integer& Integer::operator=(const Integer& x)
 {
   if (this == &x) return *this;
@@ -402,28 +430,62 @@ unsigned int Integer::getUnsignedInt() const
   return (unsigned int)d_value.get_ui();
 }
 
-bool Integer::fitsSignedLong() const { return d_value.fits_slong_p(); }
-
-bool Integer::fitsUnsignedLong() const { return d_value.fits_ulong_p(); }
-
 long Integer::getLong() const
 {
-  long si = d_value.get_si();
-  // ensure there wasn't overflow
-  CheckArgument(mpz_cmp_si(d_value.get_mpz_t(), si) == 0,
+  // ensure there it fits
+  CheckArgument(mpz_fits_slong_p(d_value.get_mpz_t()) != 0,
                 this,
                 "Overflow detected in Integer::getLong().");
-  return si;
+  return d_value.get_si();
 }
 
 unsigned long Integer::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,
+  // ensure that it fits
+  CheckArgument(mpz_fits_ulong_p(d_value.get_mpz_t()) != 0,
                 this,
                 "Overflow detected in Integer::getUnsignedLong().");
-  return ui;
+  return d_value.get_ui();
+}
+
+int64_t Integer::getSigned64() const
+{
+  if constexpr (sizeof(int64_t) == sizeof(signed long int))
+  {
+    return getLong();
+  }
+  else
+  {
+    if (mpz_fits_slong_p(d_value.get_mpz_t()) != 0)
+    {
+      return getLong();
+    }
+    // ensure there is no overflow.
+    // mpz_sizeinbase ignores the sign bit, thus at most 63 bits.
+    CheckArgument(mpz_sizeinbase(d_value.get_mpz_t(), 2) < 64,
+                  this,
+                  "Overflow detected in Integer::getSigned64().");
+    return std::stoll(toString());
+  }
+}
+uint64_t Integer::getUnsigned64() const
+{
+  if constexpr (sizeof(uint64_t) == sizeof(unsigned long int))
+  {
+    return getUnsignedLong();
+  }
+  else
+  {
+    if (mpz_fits_ulong_p(d_value.get_mpz_t()) != 0)
+    {
+      return getUnsignedLong();
+    }
+    // ensure there isn't overflow
+    CheckArgument(mpz_sizeinbase(d_value.get_mpz_t(), 2) <= 64,
+                  this,
+                  "Overflow detected in Integer::getUnsigned64().");
+    return std::stoull(toString());
+  }
 }
 
 size_t Integer::hash() const { return gmpz_hash(d_value.get_mpz_t()); }