diff options
Diffstat (limited to 'src/util/bitvector.h')
-rw-r--r-- | src/util/bitvector.h | 64 |
1 files changed, 34 insertions, 30 deletions
diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 185bb55d9..a3d4f1b60 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -23,7 +23,7 @@ #define __CVC4__BITVECTOR_H #include <iostream> -#include "util/Assert.h" +#include "util/exception.h" #include "util/integer.h" namespace CVC4 { @@ -99,8 +99,8 @@ public: return d_value != y.d_value; } - BitVector equals(const BitVector& y) const { - Assert(d_size == y.d_size); + BitVector equals(const BitVector& y) const { + CheckArgument(d_size == y.d_size, y); return d_value == y.d_value; } @@ -118,19 +118,19 @@ public: // xor BitVector operator ^(const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); return BitVector(d_size, d_value.bitwiseXor(y.d_value)); } // or BitVector operator |(const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); return BitVector(d_size, d_value.bitwiseOr(y.d_value)); } // and BitVector operator &(const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); return BitVector(d_size, d_value.bitwiseAnd(y.d_value)); } @@ -162,13 +162,13 @@ public: BitVector operator +(const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); Integer sum = d_value + y.d_value; return BitVector(d_size, sum); } BitVector operator -(const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); // to maintain the invariant that we are only adding BitVectors of the // same size BitVector one(d_size, Integer(1)); @@ -181,35 +181,38 @@ public: } BitVector operator *(const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); Integer prod = d_value * y.d_value; return BitVector(d_size, prod); } BitVector unsignedDiv (const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); // TODO: decide whether we really want these semantics if (y.d_value == 0) { return BitVector(d_size, Integer(0)); } - Assert (d_value >= 0 && y.d_value > 0); + CheckArgument(d_value >= 0, this); + CheckArgument(y.d_value > 0, y); return BitVector(d_size, d_value.floorDivideQuotient(y.d_value)); } BitVector unsignedRem(const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); // TODO: decide whether we really want these semantics if (y.d_value == 0) { return BitVector(d_size, Integer(0)); } - Assert (d_value >= 0 && y.d_value > 0); + CheckArgument(d_value >= 0, this); + CheckArgument(y.d_value > 0, y); 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); + CheckArgument(d_size == y.d_size, y); + CheckArgument(d_value >= 0, this); + CheckArgument(y.d_value >= 0, y); Integer a = (*this).toSignedInt(); Integer b = y.toSignedInt(); @@ -217,14 +220,16 @@ public: } bool unsignedLessThan(const BitVector& y) const { - Assert(d_size == y.d_size); - Assert(d_value >= 0 && y.d_value >= 0); + CheckArgument(d_size == y.d_size, y); + CheckArgument(d_value >= 0, this); + CheckArgument(y.d_value >= 0, y); return d_value < y.d_value; } bool signedLessThanEq(const BitVector& y) const { - Assert(d_size == y.d_size); - Assert(d_value >= 0 && y.d_value >= 0); + CheckArgument(d_size == y.d_size, y); + CheckArgument(d_value >= 0, this); + CheckArgument(y.d_value >= 0, y); Integer a = (*this).toSignedInt(); Integer b = y.toSignedInt(); @@ -232,8 +237,9 @@ public: } bool unsignedLessThanEq(const BitVector& y) const { - Assert(d_size == y.d_size); - Assert(d_value >= 0 && y.d_value >= 0); + CheckArgument(d_size == y.d_size, this); + CheckArgument(d_value >= 0, this); + CheckArgument(y.d_value >= 0, y); return d_value <= y.d_value; } @@ -269,7 +275,7 @@ public: } // making sure we don't lose information casting - Assert(y.d_value < Integer(1).multiplyByPow2(32)); + CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y); uint32_t amount = y.d_value.toUnsignedInt(); Integer res = d_value.multiplyByPow2(amount); return BitVector(d_size, res); @@ -281,7 +287,7 @@ public: } // making sure we don't lose information casting - Assert(y.d_value < Integer(1).multiplyByPow2(32)); + CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y); uint32_t amount = y.d_value.toUnsignedInt(); Integer res = d_value.divByPow2(amount); return BitVector(d_size, res); @@ -302,7 +308,7 @@ public: } // making sure we don't lose information casting - Assert(y.d_value < Integer(1).multiplyByPow2(32)); + CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y); uint32_t amount = y.d_value.toUnsignedInt(); Integer rest = d_value.divByPow2(amount); @@ -310,7 +316,7 @@ public: if(sign_bit == Integer(0)) { return BitVector(d_size, rest); } - Integer res = rest.oneExtend(d_size - amount, amount); + Integer res = rest.oneExtend(d_size - amount, amount); return BitVector(d_size, res); } @@ -358,17 +364,15 @@ public: inline BitVector::BitVector(const std::string& num, unsigned base) { - AlwaysAssert( base == 2 || base == 16 ); + CheckArgument(base == 2 || base == 16, base); if( base == 2 ) { d_size = num.size(); - } else if( base == 16 ) { - d_size = num.size() * 4; } else { - Unreachable("Unsupported base in BitVector(std::string&, unsigned int)."); + d_size = num.size() * 4; } - d_value = Integer(num,base); + d_value = Integer(num, base); }/* BitVector::BitVector() */ |