From: Gereon Kremer Date: Thu, 2 Dec 2021 22:33:04 +0000 (-0800) Subject: Add explicit 64bit getters for Integer class (#7728) X-Git-Tag: cvc5-1.0.0~732 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cb4274dd5dfc403b410b63de2b396cdd323d2e9f;p=cvc5.git 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(). --- diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index c62dde511..9e398b518 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -2908,7 +2908,7 @@ std::int64_t Term::getInt64Value() const 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; } @@ -2931,7 +2931,7 @@ std::uint64_t Term::getUInt64Value() const << "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; } @@ -3029,8 +3029,8 @@ std::pair Term::getReal64Value() const << "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; } diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp index e09708ae5..149e02edc 100644 --- a/src/util/integer_cln_imp.cpp +++ b/src/util/integer_cln_imp.cpp @@ -483,16 +483,6 @@ unsigned int Integer::getUnsignedInt() const 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 @@ -517,6 +507,53 @@ unsigned long Integer::getUnsignedLong() const 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::min() <= d_value + && d_value <= std::numeric_limits::max()) + { + return getLong(); + } + // ensure there isn't overflow + CheckArgument(d_value <= std::numeric_limits::max(), + this, + "Overflow detected in Integer::getSigned64()"); + CheckArgument(d_value >= std::numeric_limits::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::min() <= d_value + && d_value <= std::numeric_limits::max()) + { + return getUnsignedLong(); + } + // ensure there isn't overflow + CheckArgument(d_value <= std::numeric_limits::max(), + this, + "Overflow detected in Integer::getSigned64()"); + CheckArgument(d_value >= std::numeric_limits::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); } diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index 2120a4d5d..333d8f502 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -274,18 +274,18 @@ class CVC5_EXPORT Integer /** 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. 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 +#include #include #include @@ -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::min() <= z + && z <= std::numeric_limits::max()) + { + d_value = static_cast(z); + } + else + { + d_value = std::to_string(z); + } +} +Integer::Integer(uint64_t z) +{ + if (std::numeric_limits::min() <= z + && z <= std::numeric_limits::max()) + { + d_value = static_cast(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()); } diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index ff2ea9815..397455f87 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -59,8 +59,8 @@ class CVC5_EXPORT Integer Integer(unsigned long int z) : d_value(z) {} #ifdef CVC5_NEED_INT64_T_OVERLOADS - Integer(int64_t z) : d_value(static_cast(z)) {} - Integer(uint64_t z) : d_value(static_cast(z)) {} + Integer(int64_t z); + Integer(uint64_t z); #endif /* CVC5_NEED_INT64_T_OVERLOADS */ /** Destructor. */ @@ -257,18 +257,18 @@ class CVC5_EXPORT Integer /** 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. diff --git a/test/unit/util/integer_black.cpp b/test/unit/util/integer_black.cpp index 368f12222..2be2515eb 100644 --- a/test/unit/util/integer_black.cpp +++ b/test/unit/util/integer_black.cpp @@ -333,18 +333,69 @@ TEST_F(TestUtilBlackInteger, pow) 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::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::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::max(); + Integer a(i); + EXPECT_EQ(a.getSigned64(), i); + EXPECT_THROW((a + 1).getSigned64(), IllegalArgumentException); + } + { + int64_t i = std::numeric_limits::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::max(); + Integer a(i); + EXPECT_EQ(a.getUnsigned64(), i); + EXPECT_THROW((a + 1).getUnsigned64(), IllegalArgumentException); + } + { + uint64_t i = std::numeric_limits::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));