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() */