diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-03-22 21:45:31 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-03-22 21:45:31 +0000 |
commit | c0324db3ac7e5984c632f46690f58c333b9a42b2 (patch) | |
tree | 7a9a83b7dc1f929d4eb3de06b59ed6ff7b7f43bd /src/util/bitvector.h | |
parent | 8c4495b18e40a406be35baceaf473878bcc375f1 (diff) |
Merged updated version of the bitvector theory:
* added simplification rewrites
Diffstat (limited to 'src/util/bitvector.h')
-rw-r--r-- | src/util/bitvector.h | 283 |
1 files changed, 242 insertions, 41 deletions
diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 8adb466cf..7429ac8c9 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -32,30 +32,55 @@ class CVC4_PUBLIC BitVector { private: + /* + Class invariants: + * no overflows: 2^d_size < d_value + * no negative numbers: d_value >= 0 + */ unsigned d_size; Integer d_value; + Integer toSignedInt() const { + // returns Integer corresponding to two's complement interpretation of bv + unsigned size = d_size; + Integer sign_bit = d_value.extractBitRange(1,size-1); + Integer val = d_value.extractBitRange(size-1, 0); + Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val; + return res; + } + + public: - BitVector(unsigned size, const Integer& val) - : d_size(size), d_value(val) {} - + BitVector(unsigned size, const Integer& val): + d_size(size), + d_value(val.modByPow2(size)) + {} + BitVector(unsigned size = 0) - : d_size(size), d_value(0) {} + : d_size(size), d_value(0) {} BitVector(unsigned size, unsigned int z) - : d_size(size), d_value(z) {} - + : d_size(size), d_value(z) { + d_value = d_value.modByPow2(size); + } + BitVector(unsigned size, unsigned long int z) - : d_size(size), d_value(z) {} + : d_size(size), d_value(z) { + d_value = d_value.modByPow2(size); + } BitVector(unsigned size, const BitVector& q) - : d_size(size), d_value(q.d_value) {} - + : d_size(size), d_value(q.d_value) {} + BitVector(const std::string& num, unsigned base = 2); ~BitVector() {} + Integer toInteger() const { + return d_value; + } + BitVector& operator =(const BitVector& x) { if(this == &x) return *this; @@ -65,46 +90,227 @@ public: } bool operator ==(const BitVector& y) const { - if (d_size != y.d_size) return false; + 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; + if (d_size != y.d_size) return true; return d_value != y.d_value; } + BitVector equals(const BitVector& y) const { + Assert(d_size == y.d_size); + return d_value == y.d_value; + } + + BitVector concat (const BitVector& other) const { + return BitVector(d_size + other.d_size, (d_value.multiplyByPow2(other.d_size)) + other.d_value); + } + + BitVector extract(unsigned high, unsigned low) const { + return BitVector(high - low + 1, d_value.extractBitRange(high - low + 1, low)); + } + + /* + Bitwise operations on BitVectors + */ + + // xor + BitVector operator ^(const BitVector& y) const { + Assert (d_size == y.d_size); + return BitVector(d_size, d_value.bitwiseXor(y.d_value)); + } + + // or + BitVector operator |(const BitVector& y) const { + Assert (d_size == y.d_size); + return BitVector(d_size, d_value.bitwiseOr(y.d_value)); + } + + // and + BitVector operator &(const BitVector& y) const { + Assert (d_size == y.d_size); + return BitVector(d_size, d_value.bitwiseAnd(y.d_value)); + } + + // not + BitVector operator ~() const { + return BitVector(d_size, d_value.bitwiseNot()); + } + + /* + Arithmetic operations on BitVectors + */ + + + bool operator <(const BitVector& y) const { + return d_value < y.d_value; + } + + bool operator >(const BitVector& y) const { + return d_value > y.d_value ; + } + + bool operator <=(const BitVector& y) const { + return d_value <= y.d_value; + } + + bool operator >=(const BitVector& y) const { + 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); + Assert (d_size == y.d_size); + Integer sum = d_value + y.d_value; + return BitVector(d_size, sum); } BitVector operator -(const BitVector& y) const { - return *this + ~y + 1; + Assert (d_size == y.d_size); + // to maintain the invariant that we are only adding BitVectors of the + // same size + BitVector one(d_size, Integer(1)); + return *this + ~y + one; } BitVector operator -() const { - return ~(*this) + 1; + BitVector one(d_size, Integer(1)); + return ~(*this) + one; } BitVector operator *(const BitVector& y) const { - return BitVector(d_size, d_value * y.d_value); + Assert (d_size == y.d_size); + Integer prod = d_value * y.d_value; + return BitVector(d_size, prod); + } + + BitVector unsignedDiv (const BitVector& y) const { + Assert (d_size == y.d_size); + Assert (d_value >= 0 && y.d_value > 0); + return BitVector(d_size, d_value.floorDivideQuotient(y.d_value)); } - BitVector operator ~() const { - //is this right? it looks like a no-op? - return BitVector(d_size, d_value); + BitVector unsignedRem(const BitVector& y) const { + Assert (d_size == y.d_size); + Assert (d_value >= 0 && y.d_value > 0); + return BitVector(d_size, d_value.floorDivideRemainder(y.d_value)); + } + + + bool signedLessThan(const BitVector& y) const { + Assert(d_size == y.d_size); + Assert(d_value >= 0 && y.d_value >= 0); + Integer a = (*this).toSignedInt(); + Integer b = y.toSignedInt(); + + return a < b; } - BitVector concat (const BitVector& other) const { - return BitVector(d_size + other.d_size, (d_value.multiplyByPow2(other.d_size)) + other.d_value); - //return BitVector(d_size + other.d_size, (d_value * Integer(2).pow(other.d_size)) + other.d_value); + bool unsignedLessThan(const BitVector& y) const { + Assert(d_size == y.d_size); + Assert(d_value >= 0 && y.d_value >= 0); + return d_value < y.d_value; } - BitVector extract(unsigned high, unsigned low) const { - return BitVector(high - low + 1, d_value.extractBitRange(high - low + 1, low)); - //return BitVector(high - low + 1, (d_value % (Integer(2).pow(high + 1))) / Integer(2).pow(low)); + bool signedLessThanEq(const BitVector& y) const { + Assert(d_size == y.d_size); + Assert(d_value >= 0 && y.d_value >= 0); + Integer a = (*this).toSignedInt(); + Integer b = y.toSignedInt(); + + return a <= b; + } + + bool unsignedLessThanEq(const BitVector& y) const { + Assert(d_size == y.d_size); + Assert(d_value >= 0 && y.d_value >= 0); + return d_value <= y.d_value; + } + + + /* + Extend operations + */ + + BitVector zeroExtend(unsigned amount) const { + return BitVector(d_size + amount, d_value); + } + + BitVector signExtend(unsigned amount) const { + Integer sign_bit = d_value.extractBitRange(1, d_size -1); + if(sign_bit == Integer(0)) { + return BitVector(d_size + amount, d_value); + } else { + Integer val = d_value.oneExtend(d_size, amount); + return BitVector(d_size+ amount, val); + } + } + + /* + Shifts on BitVectors + */ + + BitVector leftShift(const BitVector& y) const { + if (y.d_value > Integer(d_size)) { + return BitVector(d_size, Integer(0)); + } + if (y.d_value == 0) { + return *this; + } + + // making sure we don't lose information casting + Assert(y.d_value < Integer(1).multiplyByPow2(32)); + uint32_t amount = y.d_value.toUnsignedInt(); + Integer res = d_value.multiplyByPow2(amount); + return BitVector(d_size, res); } + BitVector logicalRightShift(const BitVector& y) const { + if(y.d_value > Integer(d_size)) { + return BitVector(d_size, Integer(0)); + } + + // making sure we don't lose information casting + Assert(y.d_value < Integer(1).multiplyByPow2(32)); + uint32_t amount = y.d_value.toUnsignedInt(); + Integer res = d_value.divByPow2(amount); + return BitVector(d_size, res); + } + + BitVector arithRightShift(const BitVector& y) const { + Integer sign_bit = d_value.extractBitRange(1, d_size - 1); + if(y.d_value > Integer(d_size)) { + if(sign_bit == Integer(0)) { + return BitVector(d_size, Integer(0)); + } else { + return BitVector(d_size, Integer(d_size).multiplyByPow2(d_size) -1 ); + } + } + + if (y.d_value == 0) { + return *this; + } + + // making sure we don't lose information casting + Assert(y.d_value < Integer(1).multiplyByPow2(32)); + + uint32_t amount = y.d_value.toUnsignedInt(); + Integer rest = d_value.divByPow2(amount); + + if(sign_bit == Integer(0)) { + return BitVector(d_size, rest); + } + Integer res = rest.oneExtend(d_size - amount, amount); + return BitVector(d_size, res); + } + + + /* + Convenience functions + */ + size_t hash() const { return d_value.hash() + d_size; } @@ -129,32 +335,27 @@ public: const Integer& getValue() const { return d_value; } + + /** + Returns k is the integer is equal to 2^k and zero + otherwise + @return k if the integer is equal to 2^k and zero otherwise + */ + unsigned isPow2() { + return d_value.isPow2(); + } + };/* class BitVector */ + + inline BitVector::BitVector(const std::string& num, unsigned base) { AlwaysAssert( base == 2 || base == 16 ); if( base == 2 ) { d_size = num.size(); -// d_value = Integer(num,2); -/* - for( string::const_iterator it = num.begin(); it != num.end(); ++it ) { - if( *it != '0' || *it != '1' ) { - IllegalArgument(num, "BitVector argument is not a binary string."); - } - z = (Integer(2) * z) + (*it == '1'); - d_value = mpz_class(z.get_mpz()); - } -*/ } else if( base == 16 ) { d_size = num.size() * 4; -// // Use a stream to decode the hex string -// stringstream ss; -// ss.setf(ios::hex, ios::basefield); -// ss << num; -// ss >> z; -// d_value = mpz_class(z); -// break; } else { Unreachable("Unsupported base in BitVector(std::string&, unsigned int)."); } |