diff options
Diffstat (limited to 'src/util/integer_gmp_imp.cpp')
-rw-r--r-- | src/util/integer_gmp_imp.cpp | 86 |
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()); } |