diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-12-12 14:30:09 -0800 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-12-12 14:30:09 -0800 |
commit | 62e9f6d0a34d4f6623381429b51b65ddfae1e86d (patch) | |
tree | 20bfe0a785d7bebba60b2bb0572e890d95243d87 /src/theory | |
parent | 0e3dc441641c64e6137d85f8d7eaeb78ee562e51 (diff) | |
parent | 751950b3ca631ed92e1af35a290642fe7b7cc0bb (diff) |
Merge pull request #1 from lianah/1.0.x
* fixed bug 481 by adding check for division by 0 in bit-vector division...
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/bv/bitblast_strategies.cpp | 22 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h | 4 |
2 files changed, 24 insertions, 2 deletions
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<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 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<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); } |