Merged updated version of the bitvector theory:

  * added simplification rewrites

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).");
   }