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