1 files changed, 34 insertions, 0 deletions
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index d7f0e13a5..8adb466cf 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -203,6 +203,33 @@ public:
   }
 };/* class BitVectorExtractHashStrategy */
 
+
+/**
+ * The structure representing the extraction of one Boolean bit. 
+ */
+struct CVC4_PUBLIC BitVectorBitOf {
+  /** The index of the bit */
+  unsigned bitIndex;
+  BitVectorBitOf(unsigned i)
+    : bitIndex(i) {}
+
+  bool operator == (const BitVectorBitOf& other) const {
+    return bitIndex == other.bitIndex; 
+  }
+};/* struct BitVectorBitOf */
+
+/**
+ * Hash function for the BitVectorBitOf objects.
+ */
+class CVC4_PUBLIC BitVectorBitOfHashStrategy {
+public:
+  static size_t hash(const BitVectorBitOf& b) {
+    return b.bitIndex;
+  }
+};/* class BitVectorBitOfHashStrategy */
+
+
+
 struct CVC4_PUBLIC BitVectorSize {
   unsigned size;
   BitVectorSize(unsigned size)
@@ -262,6 +289,13 @@ inline std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) {
   return os << "[" << bv.high << ":" << bv.low << "]";
 }
 
+inline std::ostream& operator <<(std::ostream& os, const BitVectorBitOf& bv) CVC4_PUBLIC;
+inline std::ostream& operator <<(std::ostream& os, const BitVectorBitOf& bv) {
+  return os << "[" << bv.bitIndex << "]";
+}
+
+
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__BITVECTOR_H */