7 files changed, 154 insertions, 19 deletions
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 6597c8b48..7820acb0a 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -25,4 +25,7 @@ libutil_la_SOURCES = \
 	rational.h \
 	rational.cpp \
 	integer.h \
-	integer.cpp
+	integer.cpp \
+	bitvector.h \
+	bitvector.cpp \
+	gmp_util.h
diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp
new file mode 100644
index 000000000..bea06f71a
--- /dev/null
+++ b/src/util/bitvector.cpp
@@ -0,0 +1,16 @@
+/*
+ * bitvector.cpp
+ *
+ *  Created on: Apr 5, 2010
+ *      Author: dejan
+ */
+
+#include "bitvector.h"
+
+namespace CVC4 {
+
+std::ostream& operator <<(std::ostream& os, const BitVector& bv) {
+  return os << bv.toString();
+}
+
+}
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
new file mode 100644
index 000000000..3859fa407
--- /dev/null
+++ b/src/util/bitvector.h
@@ -0,0 +1,99 @@
+/*
+ * bitvector.h
+ *
+ *  Created on: Mar 31, 2010
+ *      Author: dejan
+ */
+
+#ifndef __CVC4__BITVECTOR_H_
+#define __CVC4__BITVECTOR_H_
+
+#include <string>
+#include <iostream>
+#include "util/gmp_util.h"
+
+namespace CVC4 {
+
+class BitVector {
+
+private:
+
+  unsigned d_size;
+  mpz_class d_value;
+
+  BitVector(unsigned size, const mpz_class& val) : d_size(size), d_value(val) {}
+
+public:
+
+  BitVector(unsigned size = 0)
+  : d_size(size), d_value(0) {}
+
+  BitVector(unsigned size, unsigned int z)
+  : d_size(size), d_value(z) {}
+
+  BitVector(unsigned size, unsigned long int z)
+  : d_size(size), d_value(z) {}
+
+  BitVector(unsigned size, const BitVector& q)
+  : d_size(size), d_value(q.d_value) {}
+
+  ~BitVector() {}
+
+  BitVector& operator =(const BitVector& x) {
+    if(this == &x)
+      return *this;
+    d_value = x.d_value;
+    return *this;
+  }
+
+  bool operator ==(const BitVector& y) const {
+    if (d_size != y.d_size) return false;
+    return d_value == y.d_value;
+  }
+
+  bool operator !=(const BitVector& y) const {
+    if (d_size == y.d_size) return false;
+    return d_value != y.d_value;
+  }
+
+  BitVector operator +(const BitVector& y) const {
+    return BitVector(std::max(d_size, y.d_size), d_value + y.d_value);
+  }
+
+  BitVector operator -(const BitVector& y) const {
+    return *this + ~y + 1;
+  }
+
+  BitVector operator -() const {
+    return ~(*this) + 1;
+  }
+
+  BitVector operator *(const BitVector& y) const {
+    return BitVector(d_size, d_value * y.d_value);
+  }
+
+  BitVector operator ~() const {
+    return BitVector(d_size, d_value);
+  }
+
+  size_t hash() const {
+    return gmpz_hash(d_value.get_mpz_t());
+  }
+
+  std::string toString(unsigned int base = 2) const {
+    return d_value.get_str(base);
+  }
+};
+
+struct BitVectorHashStrategy {
+  static inline size_t hash(const BitVector& bv) {
+    return bv.hash();
+  }
+};
+
+std::ostream& operator <<(std::ostream& os, const BitVector& bv);
+
+}
+
+
+#endif /* __CVC4__BITVECTOR_H_ */
diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h
new file mode 100644
index 000000000..1849974cd
--- /dev/null
+++ b/src/util/gmp_util.h
@@ -0,0 +1,28 @@
+/*
+ * gmp.h
+ *
+ *  Created on: Apr 5, 2010
+ *      Author: dejan
+ */
+
+#ifndef __CVC4__GMP_H_
+#define __CVC4__GMP_H_
+
+#include <gmpxx.h>
+
+namespace CVC4 {
+
+  /** Hashes the gmp integer primitive in a word by word fashion. */
+  inline size_t gmpz_hash(const mpz_t toHash) {
+    size_t hash = 0;
+    for (int i=0, n=mpz_size(toHash); i<n; ++i){
+      mp_limb_t limb = mpz_getlimbn(toHash, i);
+      hash = hash * 2;
+      hash = hash xor limb;
+    }
+    return hash;
+  }
+
+}
+
+#endif /* __CVC4__GMP_H_ */
diff --git a/src/util/integer.cpp b/src/util/integer.cpp
index 3a7851eec..a26f2108f 100644
--- a/src/util/integer.cpp
+++ b/src/util/integer.cpp
@@ -23,6 +23,6 @@
 
 using namespace CVC4;
 
-std::ostream& CVC4::operator<<(std::ostream& os, const Integer& n){
+std::ostream& CVC4::operator<<(std::ostream& os, const Integer& n) {
   return os << n.toString();
 }
diff --git a/src/util/integer.h b/src/util/integer.h
index c1e5d90ea..2aa8b711a 100644
--- a/src/util/integer.h
+++ b/src/util/integer.h
@@ -18,22 +18,12 @@
 #ifndef __CVC4__INTEGER_H
 #define __CVC4__INTEGER_H
 
-#include <gmpxx.h>
 #include <string>
+#include <iostream>
+#include "util/gmp_util.h"
 
 namespace CVC4 {
 
-/** Hashes the gmp integer primitive in a word by word fashion. */
-inline size_t gmpz_hash(const mpz_t toHash){
-  size_t hash = 0;
-  for (int i=0, n=mpz_size(toHash); i<n; ++i){
-    mp_limb_t limb = mpz_getlimbn(toHash, i);
-    hash = hash * 2;
-    hash = hash xor limb;
-  }
-  return hash;
-}
-
 class Rational;
 
 class Integer {
diff --git a/src/util/rational.h b/src/util/rational.h
index 48b00899a..e4f0e2bb7 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -24,9 +24,8 @@
 #ifndef __CVC4__RATIONAL_H
 #define __CVC4__RATIONAL_H
 
-#include <gmpxx.h>
 #include <string>
-#include "integer.h"
+#include "util/integer.h"
 
 namespace CVC4 {
 
@@ -76,20 +75,20 @@ public:
   /**
    * Constructs a canonical Rational from a numerator and denominator.
    */
-  Rational(  signed int n,   signed int d) : d_value(n,d) {
+  Rational(signed int n, signed int d) : d_value(n,d) {
     d_value.canonicalize();
   }
   Rational(unsigned int n, unsigned int d) : d_value(n,d) {
     d_value.canonicalize();
   }
-  Rational(  signed long int n,   signed long int d) : d_value(n,d) {
+  Rational(signed long int n, signed long int d) : d_value(n,d) {
     d_value.canonicalize();
   }
   Rational(unsigned long int n, unsigned long int d) : d_value(n,d) {
     d_value.canonicalize();
   }
 
-  Rational(const Integer& n, const Integer& d):
+  Rational(const Integer& n, const Integer& d) :
     d_value(n.get_mpz(), d.get_mpz())
   {
     d_value.canonicalize();