diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-02-29 20:33:43 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-02-29 20:33:43 +0000 |
commit | 2821b7a47e779c7d4f189ffdffaebe4bdb5b9036 (patch) | |
tree | 16101f79b9c8927645fa896306c1e5cb83721332 /src/theory/bv/bitblast_strategies.cpp | |
parent | 9062483193f4ec9b38aaa57b228cae1fb551566a (diff) |
This should fix the debian build fails:
* removed bvpicosat directory as it is currently not used
Cleared some of the flurry of warnings my previous merge caused in src/prop/
Diffstat (limited to 'src/theory/bv/bitblast_strategies.cpp')
-rw-r--r-- | src/theory/bv/bitblast_strategies.cpp | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp index b0a02c0a5..6967bff98 100644 --- a/src/theory/bv/bitblast_strategies.cpp +++ b/src/theory/bv/bitblast_strategies.cpp @@ -55,13 +55,13 @@ void inline extractBits(const Bits& b, Bits& dest, unsigned lo, unsigned hi) { } void inline negateBits(const Bits& bits, Bits& negated_bits) { - for(int i = 0; i < bits.size(); ++i) { + for(unsigned i = 0; i < bits.size(); ++i) { negated_bits.push_back(utils::mkNot(bits[i])); } } bool inline isZero(const Bits& bits) { - for(int i = 0; i < bits.size(); ++i) { + for(unsigned i = 0; i < bits.size(); ++i) { if(bits[i] != mkFalse()) { return false; } @@ -323,7 +323,6 @@ void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) { Assert(node.getKind() == kind::CONST_BITVECTOR); Assert(bits.size() == 0); - NodeManager* nm = NodeManager::currentNM(); for (unsigned i = 0; i < utils::getSize(node); ++i) { Integer bit = node.getConst<BitVector>().extract(i, i).getValue(); if(bit == Integer(0)){ @@ -690,12 +689,12 @@ void DefaultLshrBB (TNode node, Bits& res, Bitblaster* bb) { res = a; Bits prev_res; - for(int s = 0; s < b.size(); ++s) { + for(unsigned s = 0; s < b.size(); ++s) { // barrel shift stage: at each stage you can either shift by 2^s bits // or leave the previous stage untouched prev_res = res; int threshold = pow(2, s); - for(int i = 0; i < a.size(); ++i) { + for(unsigned i = 0; i < a.size(); ++i) { if (i + threshold >= a.size()) { // if b[s] is true then we must have shifted by at least 2^b bits so // all bits above 2^s will be 0, otherwise just use previous shift value @@ -723,12 +722,12 @@ void DefaultAshrBB (TNode node, Bits& res, Bitblaster* bb) { TNode sign_bit = a.back(); Bits prev_res; - for(int s = 0; s < b.size(); ++s) { + for(unsigned s = 0; s < b.size(); ++s) { // barrel shift stage: at each stage you can either shift by 2^s bits // or leave the previous stage untouched prev_res = res; int threshold = pow(2, s); - for(int i = 0; i < a.size(); ++i) { + for(unsigned i = 0; i < a.size(); ++i) { if (i + threshold >= a.size()) { // if b[s] is true then we must have shifted by at least 2^b bits so // all bits above 2^s will be the sign bit, otherwise just use previous shift value |