From 751950b3ca631ed92e1af35a290642fe7b7cc0bb Mon Sep 17 00:00:00 2001 From: lianah Date: Wed, 12 Dec 2012 17:26:18 -0500 Subject: [PATCH] * 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 --- src/printer/cvc/cvc_printer.cpp | 6 +++++ src/printer/smt2/smt2_printer.cpp | 2 ++ src/theory/bv/bitblast_strategies.cpp | 22 +++++++++++++++++++ ...ory_bv_rewrite_rules_constant_evaluation.h | 4 ++-- src/util/bitvector.h | 18 ++++++++------- 5 files changed, 42 insertions(+), 10 deletions(-) diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index f0a936c97..ecc224026 100644 --- 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 5985f38ef..5821fbc77 100644 --- 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 fbf9a45ee..c25c40c22 100644 --- 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 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 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 8b080d104..498378638 100644 --- 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::apply(TNode node) { BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; BitVector a = node[0].getConst(); BitVector b = node[1].getConst(); - BitVector res = a.unsignedDiv(b); + BitVector res = a.unsignedDivTotal(b); return utils::mkConst(res); } @@ -222,7 +222,7 @@ Node RewriteRule::apply(TNode node) { BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; BitVector a = node[0].getConst(); BitVector b = node[1].getConst(); - 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 2c178ec2e..4cbcba50e 100644 --- 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); -- 2.30.2