diff options
author | Tim King <taking@google.com> | 2015-12-24 05:38:43 -0500 |
---|---|---|
committer | Tim King <taking@google.com> | 2015-12-24 05:38:43 -0500 |
commit | a39ad6584c1d61e22e72b53c3838f4f675ed2e19 (patch) | |
tree | ed40cb371c41ac285ca2bf41a82254a36134e132 /src/util/integer_gmp_imp.cpp | |
parent | 87b0fe9ce10d1e5e9ed5a3e7db77f46bf3f68922 (diff) |
Miscellaneous fixes
- Splitting the two instances of CheckArgument. The template version is now always defined in base/exception.h and is available in a cvc4_public header. This version has lost its variadic version (due to swig not supporting va_list's). The CPP macro version has been renamed PrettyCheckArgument. (Taking suggestions for a better name.) This is now only defined in base/cvc4_assert.h. Only use this in cvc4_private headers and in .cpp files that can use cvc4_private headers. To use a variadic version of CheckArguments, outside of this scope, you need to duplicate this macro locally. See cvc3_compat.cpp for an example.
- Making fitsSignedInt() and fitsUnsignedInt() work more robustly for CLN on 32 bit systems.
- Refactoring ArrayStoreAll to avoid potential problems with circular header inclusions.
- Changing some headers to use iosfwd when possible.
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 */ |