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.

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 */