This PR addresses a few issues on our 32bit builds. Most importantly, it adds int64_t Integer::getSigned64() and uint64_t Integer::getUnsigned64().
CVC5_API_ARG_CHECK_EXPECTED(detail::isInt64(*d_node), *d_node)
<< "Term to be a 64-bit integer value when calling getInt64Value()";
//////// all checks before this line
- return detail::getInteger(*d_node).getLong();
+ return detail::getInteger(*d_node).getSigned64();
////////
CVC5_API_TRY_CATCH_END;
}
<< "Term to be a unsigned 64-bit integer value when calling "
"getUInt64Value()";
//////// all checks before this line
- return detail::getInteger(*d_node).getUnsignedLong();
+ return detail::getInteger(*d_node).getUnsigned64();
////////
CVC5_API_TRY_CATCH_END;
}
<< "Term to be a 64-bit rational value when calling getReal64Value()";
//////// all checks before this line
const Rational& r = detail::getRational(*d_node);
- return std::make_pair(r.getNumerator().getLong(),
- r.getDenominator().getUnsignedLong());
+ return std::make_pair(r.getNumerator().getSigned64(),
+ r.getDenominator().getUnsigned64());
////////
CVC5_API_TRY_CATCH_END;
}
return cln::cl_I_to_uint(d_value);
}
-bool Integer::fitsSignedLong() const
-{
- return d_value <= s_signedLongMax && d_value >= s_signedLongMin;
-}
-
-bool Integer::fitsUnsignedLong() const
-{
- return sgn() >= 0 && d_value <= s_unsignedLongMax;
-}
-
long Integer::getLong() const
{
// ensure there isn't overflow
return cln::cl_I_to_ulong(d_value);
}
+int64_t Integer::getSigned64() const
+{
+ if constexpr (sizeof(int64_t) == sizeof(signed long int))
+ {
+ return getLong();
+ }
+ else
+ {
+ if (std::numeric_limits<long>::min() <= d_value
+ && d_value <= std::numeric_limits<long>::max())
+ {
+ return getLong();
+ }
+ // ensure there isn't overflow
+ CheckArgument(d_value <= std::numeric_limits<int64_t>::max(),
+ this,
+ "Overflow detected in Integer::getSigned64()");
+ CheckArgument(d_value >= std::numeric_limits<int64_t>::min(),
+ 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 (std::numeric_limits<unsigned long>::min() <= d_value
+ && d_value <= std::numeric_limits<unsigned long>::max())
+ {
+ return getUnsignedLong();
+ }
+ // ensure there isn't overflow
+ CheckArgument(d_value <= std::numeric_limits<uint64_t>::max(),
+ this,
+ "Overflow detected in Integer::getSigned64()");
+ CheckArgument(d_value >= std::numeric_limits<uint64_t>::min(),
+ this,
+ "Overflow detected in Integer::getSigned64()");
+ return std::stoull(toString());
+ }
+}
+
size_t Integer::hash() const { return equal_hashcode(d_value); }
bool Integer::testBit(unsigned n) const { return cln::logbitp(n, d_value); }
/** 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;
-
/** Return the signed long representation of this Integer. */
long getLong() const;
/** Return the unsigned long representation of this Integer. */
unsigned long getUnsignedLong() const;
+ /** Return the int64_t representation of this Integer. */
+ int64_t getSigned64() const;
+
+ /** Return the uint64_t representation of this Integer. */
+ uint64_t getUnsigned64() const;
+
/**
* Computes the hash of the node from the first word of the
* numerator, the denominator.
*/
#include <cmath>
+#include <limits>
#include <sstream>
#include <string>
: 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;
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()); }
Integer(unsigned long int z) : d_value(z) {}
#ifdef CVC5_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)) {}
+ Integer(int64_t z);
+ Integer(uint64_t z);
#endif /* CVC5_NEED_INT64_T_OVERLOADS */
/** Destructor. */
/** 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;
-
/** Return the signed long representation of this Integer. */
long getLong() const;
/** Return the unsigned long representation of this Integer. */
unsigned long getUnsignedLong() const;
+ /** Return the int64_t representation of this Integer. */
+ int64_t getSigned64() const;
+
+ /** Return the uint64_t representation of this Integer. */
+ uint64_t getUnsigned64() const;
+
/**
* Computes the hash of the node from the first word of the
* numerator, the denominator.
ASSERT_EQ(Integer(-1000), Integer(-10).pow(3));
}
-TEST_F(TestUtilBlackInteger, overly_long)
+TEST_F(TestUtilBlackInteger, overly_long_signed)
+{
+ int64_t sl = std::numeric_limits<int64_t>::max();
+ Integer i(sl);
+ if constexpr (sizeof(unsigned long) == sizeof(uint64_t))
+ {
+ ASSERT_EQ(i.getLong(), sl);
+ }
+ ASSERT_NO_THROW(i.getSigned64());
+ ASSERT_EQ(i.getSigned64(), sl);
+ i = i + 1;
+ ASSERT_THROW(i.getSigned64(), IllegalArgumentException);
+}
+
+TEST_F(TestUtilBlackInteger, overly_long_unsigned)
{
uint64_t ul = std::numeric_limits<uint64_t>::max();
Integer i(ul);
- ASSERT_EQ(i.getUnsignedLong(), ul);
+ if constexpr (sizeof(unsigned long) == sizeof(uint64_t))
+ {
+ ASSERT_EQ(i.getUnsignedLong(), ul);
+ }
ASSERT_THROW(i.getLong(), IllegalArgumentException);
+ ASSERT_NO_THROW(i.getUnsigned64());
+ ASSERT_EQ(i.getUnsigned64(), ul);
uint64_t ulplus1 = ul + 1;
ASSERT_EQ(ulplus1, 0);
i = i + 1;
ASSERT_THROW(i.getUnsignedLong(), IllegalArgumentException);
}
+TEST_F(TestUtilBlackInteger, getSigned64)
+{
+ {
+ int64_t i = std::numeric_limits<int64_t>::max();
+ Integer a(i);
+ EXPECT_EQ(a.getSigned64(), i);
+ EXPECT_THROW((a + 1).getSigned64(), IllegalArgumentException);
+ }
+ {
+ int64_t i = std::numeric_limits<int64_t>::min();
+ Integer a(i);
+ EXPECT_EQ(a.getSigned64(), i);
+ EXPECT_THROW((a - 1).getSigned64(), IllegalArgumentException);
+ }
+}
+
+TEST_F(TestUtilBlackInteger, getUnsigned64)
+{
+ {
+ uint64_t i = std::numeric_limits<uint64_t>::max();
+ Integer a(i);
+ EXPECT_EQ(a.getUnsigned64(), i);
+ EXPECT_THROW((a + 1).getUnsigned64(), IllegalArgumentException);
+ }
+ {
+ uint64_t i = std::numeric_limits<uint64_t>::min();
+ Integer a(i);
+ EXPECT_EQ(a.getUnsigned64(), i);
+ EXPECT_THROW((a - 1).getUnsigned64(), IllegalArgumentException);
+ }
+}
+
TEST_F(TestUtilBlackInteger, testBit)
{
ASSERT_FALSE(Integer(0).testBit(6));
projects / cvc5.git / commitdiff