diff options
Diffstat (limited to 'src/util/bitvector.h')
-rw-r--r-- | src/util/bitvector.h | 34 |
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 */ |