summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/api/cpp/cvc5.cpp8
-rw-r--r--src/util/integer_cln_imp.cpp57
-rw-r--r--src/util/integer_cln_imp.h12
-rw-r--r--src/util/integer_gmp_imp.cpp86
-rw-r--r--src/util/integer_gmp_imp.h16
-rw-r--r--test/unit/util/integer_black.cpp55
6 files changed, 192 insertions, 42 deletions
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<std::int64_t, std::uint64_t> 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<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); }
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 <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()); }
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<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. */
@@ -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<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));
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback