diff options
Diffstat (limited to 'src/util/integer_gmp_imp.cpp')
-rw-r--r-- | src/util/integer_gmp_imp.cpp | 37 |
1 files changed, 31 insertions, 6 deletions
diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp index bde759219..df1bd297a 100644 --- a/src/util/integer_gmp_imp.cpp +++ b/src/util/integer_gmp_imp.cpp @@ -21,16 +21,18 @@ #include <string> #include "cvc4autoconfig.h" + +#include "base/cvc4_assert.h" #include "util/rational.h" #ifndef CVC4_GMP_IMP # error "This source should only ever be built if CVC4_GMP_IMP is on !" #endif /* CVC4_GMP_IMP */ -using namespace std; -using namespace CVC4; +using namespace std; +namespace CVC4 { Integer::Integer(const char* s, unsigned base) : d_value(s, base) @@ -52,10 +54,11 @@ bool Integer::fitsUnsignedInt() const { signed int Integer::getSignedInt() const { // ensure there isn't overflow CheckArgument(d_value <= std::numeric_limits<int>::max(), this, - "Overflow detected in Integer::getSignedInt()"); + "Overflow detected in Integer::getSignedInt()."); CheckArgument(d_value >= std::numeric_limits<int>::min(), this, - "Overflow detected in Integer::getSignedInt()"); - CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getSignedInt()"); + "Overflow detected in Integer::getSignedInt()."); + CheckArgument(fitsSignedInt(), this, + "Overflow detected in Integer::getSignedInt()."); return (signed int) d_value.get_si(); } @@ -65,6 +68,28 @@ unsigned int Integer::getUnsignedInt() const { "Overflow detected in Integer::getUnsignedInt()"); CheckArgument(d_value >= std::numeric_limits<unsigned int>::min(), this, "Overflow detected in Integer::getUnsignedInt()"); - CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getUnsignedInt()"); + CheckArgument(fitsSignedInt(), this, + "Overflow detected in Integer::getUnsignedInt()"); return (unsigned int) d_value.get_ui(); } + +Integer Integer::oneExtend(uint32_t size, uint32_t amount) const { + // check that the size is accurate + DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size); + mpz_class res = d_value; + + for (unsigned i = size; i < size + amount; ++i) { + mpz_setbit(res.get_mpz_t(), i); + } + + return Integer(res); +} + +Integer Integer::exactQuotient(const Integer& y) const { + DebugCheckArgument(y.divides(*this), y); + mpz_class q; + mpz_divexact(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t()); + return Integer( q ); +} + +} /* namespace CVC4 */ |