Merged updated version of the bitvector theory:

  * added simplification rewrites

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.
    */