diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-09-14 11:00:13 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-09-14 18:00:13 +0000 |
commit | 06689796a7eddffb7b0d56aa2cc7917ab6bab602 (patch) | |
tree | 312c3107648474b7fd5745823906d447cf862e1c /src/theory/bv | |
parent | 54853f9584f2de2bf4e1ff16517b44a45e6d7cf2 (diff) |
bv: Unify bit-blasting code for udiv and urem. (#7188)
This refactor additionally removes the caching for urem/udiv cases when
bit-blasting udiv/urem and eliminates the only rewrite() calls in the
bit-blaster. Caching is not required since repeated calls to udiv/urem
with the same arguments will produce the same circuit. Further, the rewrite()
calls during bit-blasting would further complicate the recording of
bit-blasting proofs and hence is removed.
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/bitblast/bitblast_strategies_template.h | 64 | ||||
-rw-r--r-- | src/theory/bv/bitblast/bitblaster.h | 1 |
2 files changed, 28 insertions, 37 deletions
diff --git a/src/theory/bv/bitblast/bitblast_strategies_template.h b/src/theory/bv/bitblast/bitblast_strategies_template.h index f71f82ce1..ca2d55dc9 100644 --- a/src/theory/bv/bitblast/bitblast_strategies_template.h +++ b/src/theory/bv/bitblast/bitblast_strategies_template.h @@ -24,7 +24,6 @@ #include "expr/node.h" #include "theory/bv/bitblast/bitblast_utils.h" #include "theory/bv/theory_bv_utils.h" -#include "theory/rewriter.h" #include "util/bitvector.h" namespace cvc5 { @@ -514,36 +513,48 @@ void uDivModRec(const std::vector<T>& a, const std::vector<T>& b, std::vector<T> } template <class T> -void DefaultUdivBB(TNode node, std::vector<T>& q, TBitblaster<T>* bb) +void UdivUremBB(TNode node, + std::vector<T>& quot, + std::vector<T>& rem, + TBitblaster<T>* bb) { Debug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node << "\n"; - Assert(node.getKind() == kind::BITVECTOR_UDIV && q.size() == 0); + Assert(quot.empty()); + Assert(rem.empty()); + Assert(node.getKind() == kind::BITVECTOR_UDIV + || node.getKind() == kind::BITVECTOR_UREM); std::vector<T> a, b; bb->bbTerm(node[0], a); bb->bbTerm(node[1], b); - std::vector<T> r; - uDivModRec(a, b, q, r, utils::getSize(node)); + uDivModRec(a, b, quot, rem, utils::getSize(node)); // adding a special case for division by 0 std::vector<T> iszero; - for (unsigned i = 0; i < b.size(); ++i) + for (size_t i = 0, size = b.size(); i < size; ++i) { iszero.push_back(mkIff(b[i], mkFalse<T>())); } T b_is_0 = mkAnd(iszero); - for (unsigned i = 0; i < q.size(); ++i) + for (size_t i = 0, size = quot.size(); i < size; ++i) { - q[i] = mkIte(b_is_0, mkTrue<T>(), q[i]); // a udiv 0 is 11..11 - r[i] = mkIte(b_is_0, a[i], r[i]); // a urem 0 is a + quot[i] = mkIte(b_is_0, mkTrue<T>(), quot[i]); // a udiv 0 is 11..11 + rem[i] = mkIte(b_is_0, a[i], rem[i]); // a urem 0 is a } +} + +template <class T> +void DefaultUdivBB(TNode node, std::vector<T>& quot, TBitblaster<T>* bb) +{ + Debug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node + << "\n"; + Assert(quot.empty()); + Assert(node.getKind() == kind::BITVECTOR_UDIV); - // cache the remainder in case we need it later - Node remainder = Rewriter::rewrite( - NodeManager::currentNM()->mkNode(kind::BITVECTOR_UREM, node[0], node[1])); - bb->storeBBTerm(remainder, r); + std::vector<T> r; + UdivUremBB(node, quot, r, bb); } template <class T> @@ -551,32 +562,11 @@ void DefaultUremBB(TNode node, std::vector<T>& rem, TBitblaster<T>* bb) { Debug("bitvector-bb") << "theory::bv::DefaultUremBB bitblasting " << node << "\n"; - Assert(node.getKind() == kind::BITVECTOR_UREM && rem.size() == 0); - - std::vector<T> a, b; - bb->bbTerm(node[0], a); - bb->bbTerm(node[1], b); + Assert(rem.empty()); + Assert(node.getKind() == kind::BITVECTOR_UREM); std::vector<T> q; - uDivModRec(a, b, q, rem, utils::getSize(node)); - // adding a special case for division by 0 - std::vector<T> iszero; - for (unsigned i = 0; i < b.size(); ++i) - { - iszero.push_back(mkIff(b[i], mkFalse<T>())); - } - T b_is_0 = mkAnd(iszero); - - for (unsigned i = 0; i < q.size(); ++i) - { - q[i] = mkIte(b_is_0, mkTrue<T>(), q[i]); // a udiv 0 is 11..11 - rem[i] = mkIte(b_is_0, a[i], rem[i]); // a urem 0 is a - } - - // cache the quotient in case we need it later - Node quotient = Rewriter::rewrite( - NodeManager::currentNM()->mkNode(kind::BITVECTOR_UDIV, node[0], node[1])); - bb->storeBBTerm(quotient, q); + UdivUremBB(node, q, rem, bb); } template <class T> diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h index 6e9444ba6..17c233789 100644 --- a/src/theory/bv/bitblast/bitblaster.h +++ b/src/theory/bv/bitblast/bitblaster.h @@ -30,6 +30,7 @@ #include "prop/sat_solver_types.h" #include "smt/smt_engine_scope.h" #include "theory/bv/bitblast/bitblast_strategies_template.h" +#include "theory/rewriter.h" #include "theory/theory.h" #include "theory/valuation.h" #include "util/resource_manager.h" |