From: lianah <lianahady@gmail.com>
Date: Sat, 2 Feb 2013 00:43:37 +0000 (-0500)
Subject: merged master into branch
X-Git-Tag: cvc5-1.0.0~7361^2~48
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=764bda53ed154495286d7ff117aa7182a8ce5f7b;p=cvc5.git

merged master into branch
---

764bda53ed154495286d7ff117aa7182a8ce5f7b
diff --cc src/util/bitvector.h
index 5df632ff4,4cbcba50e..c9661c0c7
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@@ -178,34 -178,25 +178,39 @@@ public
      Integer prod = d_value * y.d_value;
      return BitVector(d_size, prod);
    }
 +
 +  BitVector setBit(uint32_t i) const {
 +    CheckArgument(i < d_size, i);
 +    Integer res = d_value.setBit(i);
 +    return BitVector(d_size, res); 
 +  }
 +
 +  bool isBitSet(uint32_t i) const {
 +    CheckArgument(i < d_size, i); 
 +    return d_value.isBitSet(i); 
 +  }
 +  
-   BitVector unsignedDiv (const BitVector& y) const {
+   /** 
+    * Total division function that returns 0 when the denominator is 0.  
+    */
+   BitVector unsignedDivTotal (const BitVector& y) const {
++
      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));
+       return BitVector(d_size, 0u);
      }
      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 {
++  
+   /** 
+    * Total division function that returns 0 when the denominator is 0.  
+    */
+   BitVector unsignedRemTotal(const BitVector& y) const {
      CheckArgument(d_size == y.d_size, y);
-     // TODO: decide whether we really want these semantics
      if (y.d_value == 0) {
-       return BitVector(d_size, d_value);
+       return BitVector(d_size, 0u);
      }
      CheckArgument(d_value >= 0, this);
      CheckArgument(y.d_value > 0, y);