diff options
Diffstat (limited to 'src/util/bitvector.h')
-rw-r--r-- | src/util/bitvector.h | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 2d5d29339..04e23217b 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -396,7 +396,7 @@ struct CVC4_PUBLIC BitVectorHashFunction { /** * The structure representing the extraction operation for bit-vectors. The - * operation map bit-vectors to bit-vector of size <code>high - low + 1</code> + * operation maps bit-vectors to bit-vector of size <code>high - low + 1</code> * by taking the bits at indices <code>high ... low</code> */ struct CVC4_PUBLIC BitVectorExtract { @@ -492,6 +492,13 @@ struct CVC4_PUBLIC BitVectorRotateRight { operator unsigned () const { return rotateRightAmount; } };/* struct BitVectorRotateRight */ +struct CVC4_PUBLIC IntToBitVector { + unsigned size; + IntToBitVector(unsigned size) + : size(size) {} + operator unsigned () const { return size; } +};/* struct IntToBitVector */ + template <typename T> struct CVC4_PUBLIC UnsignedHashFunction { inline size_t operator()(const T& x) const { @@ -514,6 +521,11 @@ inline std::ostream& operator <<(std::ostream& os, const BitVectorBitOf& bv) { return os << "[" << bv.bitIndex << "]"; } +inline std::ostream& operator <<(std::ostream& os, const IntToBitVector& bv) CVC4_PUBLIC; +inline std::ostream& operator <<(std::ostream& os, const IntToBitVector& bv) { + return os << "[" << bv.size << "]"; +} + }/* CVC4 namespace */ #endif /* __CVC4__BITVECTOR_H */ |