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 | |
parent | 8c4495b18e40a406be35baceaf473878bcc375f1 (diff) |
Merged updated version of the bitvector theory:
* added simplification rewrites
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/bitvector.h | 283 | ||||
-rw-r--r-- | src/util/integer_cln_imp.h | 51 | ||||
-rw-r--r-- | src/util/integer_gmp_imp.h | 84 |
3 files changed, 374 insertions, 44 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)."); } diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index 06459e3e1..9d67e8fba 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -185,6 +185,24 @@ public: } */ + + Integer bitwiseOr(const Integer& y) const { + return Integer(cln::logior(d_value, y.d_value)); + } + + Integer bitwiseAnd(const Integer& y) const { + return Integer(cln::logand(d_value, y.d_value)); + } + + Integer bitwiseXor(const Integer& y) const { + return Integer(cln::logxor(d_value, y.d_value)); + } + + Integer bitwiseNot() const { + return Integer(cln::lognot(d_value)); + } + + /** * Return this*(2^pow). */ @@ -193,6 +211,20 @@ public: return Integer( d_value << ipow); } + Integer oneExtend(uint32_t size, uint32_t amount) const { + Assert((*this) < Integer(1).multiplyByPow2(size)); + cln::cl_byte range(amount, size); + cln::cl_I allones = (cln::cl_I(1) << (size + amount))- 1; // 2^size - 1 + Integer temp(allones); + + return Integer(cln::deposit_field(allones, d_value, range)); + } + + uint32_t toUnsignedInt() const { + return cln::cl_I_to_uint(d_value); + } + + /** See CLN Documentation. */ Integer extractBitRange(uint32_t bitCount, uint32_t low) const { cln::cl_byte range(bitCount, low); @@ -243,6 +275,15 @@ public: return Integer( cln::exquo(d_value, y.d_value) ); } + Integer modByPow2(uint32_t exp) const { + cln::cl_byte range(exp, 0); + return Integer(cln::ldb(d_value, range)); + } + + Integer divByPow2(uint32_t exp) const { + return d_value >> exp; + } + /** * Raise this Integer to the power <code>exp</code>. * @@ -364,6 +405,16 @@ public: } /** + * Returns k if the integer is equal to 2^(k-1) + * @return k if the integer is equal to 2^(k-1) and 0 otherwise + */ + unsigned isPow2() const { + if (d_value <= 0) return 0; + // power2p returns n such that d_value = 2^(n-1) + return cln::power2p(d_value); + } + + /** * If x != 0, returns the unique n s.t. 2^{n-1} <= abs(x) < 2^{n}. * If x == 0, returns 1. */ diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index a02f5d2c1..ceb585852 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -135,6 +135,30 @@ public: return *this; } + Integer bitwiseOr(const Integer& y) const { + mpz_class result; + mpz_ior(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t()); + return Integer(result); + } + + Integer bitwiseAnd(const Integer& y) const { + mpz_class result; + mpz_and(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t()); + return Integer(result); + } + + Integer bitwiseXor(const Integer& y) const { + mpz_class result; + mpz_xor(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t()); + return Integer(result); + } + + Integer bitwiseNot() const { + mpz_class result; + mpz_com(result.get_mpz_t(), d_value.get_mpz_t()); + return Integer(result); + } + /** * Return this*(2^pow). */ @@ -144,6 +168,26 @@ public: return Integer( result ); } + /** + * Returns the integer with the binary representation of size bits + * extended with amount 1's + */ + Integer oneExtend(uint32_t size, uint32_t amount) const { + // check that the size is accurate + Assert ((*this) < Integer(1).multiplyByPow2(size)); + mpz_class res = d_value; + + for (unsigned i = size; i < size + amount; ++i) { + mpz_setbit(res.get_mpz_t(), i); + } + + return Integer(res); + } + + uint32_t toUnsignedInt() const { + return mpz_get_ui(d_value.get_mpz_t()); + } + /** See GMP Documentation. */ Integer extractBitRange(uint32_t bitCount, uint32_t low) const { // bitCount = high-low+1 @@ -175,7 +219,7 @@ public: } /** - * Computes a floor quoient and remainder for x divided by y. + * Computes a floor quotient and remainder for x divided by y. */ static void floorQR(Integer& q, Integer& r, const Integer& x, const Integer& y) { mpz_fdiv_qr(q.d_value.get_mpz_t(), r.d_value.get_mpz_t(), x.d_value.get_mpz_t(), y.d_value.get_mpz_t()); @@ -209,6 +253,25 @@ public: return Integer( q ); } + /** + * Returns y mod 2^exp + */ + Integer modByPow2(uint32_t exp) const { + mpz_class res; + mpz_fdiv_r_2exp(res.get_mpz_t(), d_value.get_mpz_t(), exp); + return Integer(res); + } + + /** + * Returns y / 2^exp + */ + Integer divByPow2(uint32_t exp) const { + mpz_class res; + mpz_fdiv_q_2exp(res.get_mpz_t(), d_value.get_mpz_t(), exp); + return Integer(res); + } + + int sgn() const { return mpz_sgn(d_value.get_mpz_t()); } @@ -268,14 +331,14 @@ public: long si = d_value.get_si(); // ensure there wasn't overflow AlwaysAssert(mpz_cmp_si(d_value.get_mpz_t(), si) == 0, - "Overflow when extracting long from multiprecision integer"); + "Overflow detected in Integer::getLong()"); return si; } unsigned long getUnsignedLong() const { unsigned long ui = d_value.get_ui(); // ensure there wasn't overflow AlwaysAssert(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0, - "Overflow when extracting unsigned long from multiprecision integer"); + "Overflow detected in Integer::getUnsignedLong()"); return ui; } @@ -298,6 +361,21 @@ public: } /** + * Returns k if the integer is equal to 2^(k-1) + * @return k if the integer is equal to 2^(k-1) and 0 otherwise + */ + unsigned isPow2() const { + if (d_value <= 0) return 0; + // check that the number of ones in the binary represenation is 1 + if (mpz_popcount(d_value.get_mpz_t()) == 1) { + // return the index of the first one plus 1 + return mpz_scan1(d_value.get_mpz_t(), 0) + 1; + } + return 0; + } + + + /** * If x != 0, returns the smallest n s.t. 2^{n-1} <= abs(x) < 2^{n}. * If x == 0, returns 1. */ |