bitvector rewriting for the core theory and testcases

3 files changed, 24 insertions, 3 deletions

diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 0b5952481..5c05bd6a7 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -35,10 +35,11 @@ private:
   unsigned d_size;
   Integer d_value;
 
-  BitVector(unsigned size, const Integer& val) : d_size(size), d_value(val) {}
-
 public:
 
+  BitVector(unsigned size, const Integer& val)
+  : d_size(size), d_value(val) {}
+
   BitVector(unsigned size = 0)
   : d_size(size), d_value(0) {}
 
@@ -58,6 +59,7 @@ public:
   BitVector& operator =(const BitVector& x) {
     if(this == &x)
       return *this;
+    d_size = x.d_size;
     d_value = x.d_value;
     return *this;
   }
@@ -92,8 +94,16 @@ public:
     return BitVector(d_size, d_value);
   }
 
+  BitVector concat (const BitVector& other) const {
+    return BitVector(d_size + other.d_size, (d_value * Integer(2).pow(other.d_size)) + other.d_value);
+  }
+
+  BitVector extract(unsigned high, unsigned low) {
+    return BitVector(high - low + 1, (d_value % (Integer(2).pow(high + 1))) / Integer(2).pow(low));
+  }
+
   size_t hash() const {
-    return d_value.hash();
+    return d_value.hash() + d_size;
   }
 
   std::string toString(unsigned int base = 2) const {
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 8551d0a6a..233b3aa08 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -152,6 +152,14 @@ public:
     return Integer( d_value * y.d_value );
   }
 
+  Integer operator/(const Integer& y) const {
+    return Integer( cln::floor1(d_value, y.d_value) );
+  }
+
+  Integer operator%(const Integer& y) const {
+    return Integer( cln::floor2(d_value, y.d_value).remainder );
+  }
+
   /** Raise this Integer to the power <code>exp</code>.
    *
    * @param exp the exponent
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index b065dca23..4b2ab1a79 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -123,6 +123,9 @@ public:
   Integer operator/(const Integer& y) const {
     return Integer( d_value / y.d_value );
   }
+  Integer operator%(const Integer& y) const {
+    return Integer( d_value % y.d_value );
+  }
 
   /** Raise this Integer to the power <code>exp</code>.
    *