* fixed bug 481 by adding check for division by 0 in bit-vector division circuit

* added printing for total bit-vector division kinds for debugging purposes

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index f0a936c97e7fcf26d7a85220d13b710000c80562..ecc224026599bf432b10e30deeb870515d7b4eb5 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -493,9 +493,15 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
     case kind::BITVECTOR_UDIV:
       op << "BVUDIV";
       break;
+    case kind::BITVECTOR_UDIV_TOTAL:
+      op << "BVUDIV_TOTAL";
+      break;
     case kind::BITVECTOR_UREM:
       op << "BVUREM";
       break;
+    case kind::BITVECTOR_UREM_TOTAL:
+      op << "BVUREM_TOTAL";
+      break;
     case kind::BITVECTOR_SDIV:
       op << "BVSDIV";
       break;

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 5985f38ef9d0462aa4835392dbbcb1d99e49257e..5821fbc77e6e9eabd5c15b4cbb430c37b2fb672e 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -254,7 +254,9 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::BITVECTOR_SUB: out << "bvsub "; break;
   case kind::BITVECTOR_NEG: out << "bvneg "; break;
   case kind::BITVECTOR_UDIV: out << "bvudiv "; break;
+  case kind::BITVECTOR_UDIV_TOTAL: out << "bvudiv_total "; break;
   case kind::BITVECTOR_UREM: out << "bvurem "; break;
+  case kind::BITVECTOR_UREM_TOTAL: out << "bvurem_total "; break;
   case kind::BITVECTOR_SDIV: out << "bvsdiv "; break;
   case kind::BITVECTOR_SREM: out << "bvsrem "; break;
   case kind::BITVECTOR_SMOD: out << "bvsmod "; break;

diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index fbf9a45ee8de6d027f2d2c002aff6c2929f8daf1..c25c40c220202d3a0f3ad5745c95cb6295d92c0b 100644 (file)
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -648,6 +648,17 @@ void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) {
 
   Bits r;
   uDivModRec(a, b, q, r, getSize(node)); 
+  // adding a special case for division by 0
+  std::vector<Node> iszero; 
+  for (unsigned i = 0; i < b.size(); ++i) {
+    iszero.push_back(utils::mkNode(kind::IFF, b[i], utils::mkFalse())); 
+  }
+  Node b_is_0 = utils::mkAnd(iszero); 
+  
+  for (unsigned i = 0; i < q.size(); ++i) {
+    q[i] = utils::mkNode(kind::ITE, b_is_0, utils::mkFalse(), q[i]);
+    r[i] = utils::mkNode(kind::ITE, b_is_0, utils::mkFalse(), r[i]);
+  }
 
   // cache the remainder in case we need it later
   Node remainder = mkNode(kind::BITVECTOR_UREM_TOTAL, node[0], node[1]);
@@ -664,6 +675,17 @@ void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) {
 
   Bits q;
   uDivModRec(a, b, q, rem, getSize(node)); 
+  // adding a special case for division by 0
+  std::vector<Node> iszero; 
+  for (unsigned i = 0; i < b.size(); ++i) {
+    iszero.push_back(utils::mkNode(kind::IFF, b[i], utils::mkFalse())); 
+  }
+  Node b_is_0 = utils::mkAnd(iszero); 
+  
+  for (unsigned i = 0; i < q.size(); ++i) {
+    q[i] = utils::mkNode(kind::ITE, b_is_0, utils::mkFalse(), q[i]);
+    rem[i] = utils::mkNode(kind::ITE, b_is_0, utils::mkFalse(), rem[i]);
+  }
 
   // cache the quotient in case we need it later
   Node quotient = mkNode(kind::BITVECTOR_UDIV_TOTAL, node[0], node[1]);

diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
index 8b080d104bfcd6d0079fa3a9000f0b3b7627be86..498378638cd39439f9a558878adeccdeb908a8cb 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
@@ -207,7 +207,7 @@ Node RewriteRule<EvalUdiv>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalUdiv>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
-  BitVector res = a.unsignedDiv(b);
+  BitVector res = a.unsignedDivTotal(b);
   
   return utils::mkConst(res);
 }
@@ -222,7 +222,7 @@ Node RewriteRule<EvalUrem>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalUrem>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
-  BitVector res = a.unsignedRem(b);
+  BitVector res = a.unsignedRemTotal(b);
   return utils::mkConst(res);
 }
 

diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 2c178ec2e2dab71cd4bdf752138f7d8fee1edcbc..4cbcba50eb73d71265f28240e84ad1124fd67281 100644 (file)
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -178,23 +178,25 @@ public:
     Integer prod = d_value * y.d_value;
     return BitVector(d_size, prod);
   }
-  
-  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);