diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-18 16:53:18 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-18 16:53:23 -0400 |
commit | aa16fb32ac7a66e327f32ea4c794a3ccf832c587 (patch) | |
tree | cdb11834a67cfa393311028d06addaef265590b2 /src/util/bitvector.h | |
parent | 066191d91d9f42f34a412162203be818e202aeba (diff) |
Support for bv2nat/int2bv in parser and BV rewriter.
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 */ |