diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-03-05 19:28:19 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-05 21:28:19 -0600 |
commit | 59d9aad4839e64e0f6d6b57ff112c418ffbbe9fb (patch) | |
tree | d0df100653994157bc631e9ca7fe422dd78e29ff /src/theory/bv | |
parent | c6fffe4fd328401f7f7e0757303e8dea5f6c14a4 (diff) |
Remove partial UDIV/UREM operators. (#6069)
This commit removes the partial UDIV/UREM operator handling. BITVECTOR_UDIV and BITVECTOR_UREM are now total.
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/bitblast/bitblast_strategies_template.h | 12 | ||||
-rw-r--r-- | src/theory/bv/bitblast/bitblaster.h | 6 | ||||
-rw-r--r-- | src/theory/bv/bv_solver_lazy.cpp | 4 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_algebraic.cpp | 7 | ||||
-rw-r--r-- | src/theory/bv/kinds | 9 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 55 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 15 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h | 8 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h | 8 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 21 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 19 |
11 files changed, 35 insertions, 129 deletions
diff --git a/src/theory/bv/bitblast/bitblast_strategies_template.h b/src/theory/bv/bitblast/bitblast_strategies_template.h index 8bab969c5..2cc1b7e68 100644 --- a/src/theory/bv/bitblast/bitblast_strategies_template.h +++ b/src/theory/bv/bitblast/bitblast_strategies_template.h @@ -517,7 +517,7 @@ void DefaultUdivBB(TNode node, std::vector<T>& q, TBitblaster<T>* bb) { Debug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node << "\n"; - Assert(node.getKind() == kind::BITVECTOR_UDIV_TOTAL && q.size() == 0); + Assert(node.getKind() == kind::BITVECTOR_UDIV && q.size() == 0); std::vector<T> a, b; bb->bbTerm(node[0], a); @@ -540,8 +540,8 @@ void DefaultUdivBB(TNode node, std::vector<T>& q, TBitblaster<T>* bb) } // cache the remainder in case we need it later - Node remainder = Rewriter::rewrite(NodeManager::currentNM()->mkNode( - kind::BITVECTOR_UREM_TOTAL, node[0], node[1])); + Node remainder = Rewriter::rewrite( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_UREM, node[0], node[1])); bb->storeBBTerm(remainder, r); } @@ -550,7 +550,7 @@ 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_TOTAL && rem.size() == 0); + Assert(node.getKind() == kind::BITVECTOR_UREM && rem.size() == 0); std::vector<T> a, b; bb->bbTerm(node[0], a); @@ -573,8 +573,8 @@ void DefaultUremBB(TNode node, std::vector<T>& rem, TBitblaster<T>* bb) } // cache the quotient in case we need it later - Node quotient = Rewriter::rewrite(NodeManager::currentNM()->mkNode( - kind::BITVECTOR_UDIV_TOTAL, node[0], node[1])); + Node quotient = Rewriter::rewrite( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_UDIV, node[0], node[1])); bb->storeBBTerm(quotient, q); } diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h index a1763d081..1e9db1597 100644 --- a/src/theory/bv/bitblast/bitblaster.h +++ b/src/theory/bv/bitblast/bitblaster.h @@ -160,10 +160,8 @@ void TBitblaster<T>::initTermBBStrategies() d_termBBStrategies[kind::BITVECTOR_PLUS] = DefaultPlusBB<T>; d_termBBStrategies[kind::BITVECTOR_SUB] = DefaultSubBB<T>; d_termBBStrategies[kind::BITVECTOR_NEG] = DefaultNegBB<T>; - d_termBBStrategies[kind::BITVECTOR_UDIV] = UndefinedTermBBStrategy<T>; - d_termBBStrategies[kind::BITVECTOR_UREM] = UndefinedTermBBStrategy<T>; - d_termBBStrategies[kind::BITVECTOR_UDIV_TOTAL] = DefaultUdivBB<T>; - d_termBBStrategies[kind::BITVECTOR_UREM_TOTAL] = DefaultUremBB<T>; + d_termBBStrategies[kind::BITVECTOR_UDIV] = DefaultUdivBB<T>; + d_termBBStrategies[kind::BITVECTOR_UREM] = DefaultUremBB<T>; d_termBBStrategies[kind::BITVECTOR_SDIV] = UndefinedTermBBStrategy<T>; d_termBBStrategies[kind::BITVECTOR_SREM] = UndefinedTermBBStrategy<T>; d_termBBStrategies[kind::BITVECTOR_SMOD] = UndefinedTermBBStrategy<T>; diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp index 3cadac621..fbf295a85 100644 --- a/src/theory/bv/bv_solver_lazy.cpp +++ b/src/theory/bv/bv_solver_lazy.cpp @@ -208,7 +208,7 @@ void BVSolverLazy::checkForLemma(TNode fact) if (fact.getKind() == kind::EQUAL) { NodeManager* nm = NodeManager::currentNM(); - if (fact[0].getKind() == kind::BITVECTOR_UREM_TOTAL) + if (fact[0].getKind() == kind::BITVECTOR_UREM) { TNode urem = fact[0]; TNode result = fact[1]; @@ -220,7 +220,7 @@ void BVSolverLazy::checkForLemma(TNode fact) kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div); lemma(split); } - if (fact[1].getKind() == kind::BITVECTOR_UREM_TOTAL) + if (fact[1].getKind() == kind::BITVECTOR_UREM) { TNode urem = fact[1]; TNode result = fact[0]; diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index e1230a56c..003e9dd1a 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -781,9 +781,10 @@ AlgebraicSolver::Statistics::~Statistics() { } bool hasExpensiveBVOperatorsRec(TNode fact, TNodeSet& seen) { - if (fact.getKind() == kind::BITVECTOR_MULT || - fact.getKind() == kind::BITVECTOR_UDIV_TOTAL || - fact.getKind() == kind::BITVECTOR_UREM_TOTAL) { + if (fact.getKind() == kind::BITVECTOR_MULT + || fact.getKind() == kind::BITVECTOR_UDIV + || fact.getKind() == kind::BITVECTOR_UREM) + { return true; } diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index f9caf119a..32e0e9e85 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -56,14 +56,12 @@ operator BITVECTOR_MULT 2: "multiplication of two or more bit-vectors" operator BITVECTOR_NEG 1 "unary negation of a bit-vector" operator BITVECTOR_PLUS 2: "addition of two or more bit-vectors" operator BITVECTOR_SUB 2 "subtraction of two bit-vectors" -operator BITVECTOR_UDIV 2 "unsigned division of two bit-vectors, truncating towards 0 (undefined if divisor is 0)" -operator BITVECTOR_UREM 2 "unsigned remainder from truncating division of two bit-vectors (undefined if divisor is 0)" +operator BITVECTOR_UDIV 2 "unsigned division of two bit-vectors, truncating towards 0 (defined to be the all-ones bit pattern, if divisor is 0)" +operator BITVECTOR_UREM 2 "unsigned remainder from truncating division of two bit-vectors (defined to be equal to the dividend, if divisor is 0)" operator BITVECTOR_SDIV 2 "2's complement signed division" operator BITVECTOR_SMOD 2 "2's complement signed remainder (sign follows divisor)" operator BITVECTOR_SREM 2 "2's complement signed remainder (sign follows dividend)" # total division kinds -operator BITVECTOR_UDIV_TOTAL 2 "unsigned division of two bit-vectors, truncating towards 0 (defined to be the all-ones bit pattern, if divisor is 0)" -operator BITVECTOR_UREM_TOTAL 2 "unsigned remainder from truncating division of two bit-vectors (defined to be equal to the dividend, if divisor is 0)" ## shift kinds operator BITVECTOR_ASHR 2 "bit-vector arithmetic shift right (the two bit-vector parameters must have same width)" @@ -183,9 +181,6 @@ typerule BITVECTOR_UREM ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_SDIV ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_SMOD ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_SREM ::CVC4::theory::bv::BitVectorFixedWidthTypeRule -# total division kinds -typerule BITVECTOR_UDIV_TOTAL ::CVC4::theory::bv::BitVectorFixedWidthTypeRule -typerule BITVECTOR_UREM_TOTAL ::CVC4::theory::bv::BitVectorFixedWidthTypeRule ## shift kinds typerule BITVECTOR_ASHR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 47974fc03..52bb55757 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -36,8 +36,6 @@ TheoryBV::TheoryBV(context::Context* c, std::string name) : Theory(THEORY_BV, c, u, out, valuation, logicInfo, pnm, name), d_internal(nullptr), - d_ufDivByZero(), - d_ufRemByZero(), d_rewriter(), d_state(c, u, valuation), d_im(*this, d_state, nullptr, "theory::bv"), @@ -126,46 +124,6 @@ void TheoryBV::finishInit() } } -Node TheoryBV::getUFDivByZero(Kind k, unsigned width) -{ - NodeManager* nm = NodeManager::currentNM(); - if (k == kind::BITVECTOR_UDIV) - { - if (d_ufDivByZero.find(width) == d_ufDivByZero.end()) - { - // lazily create the function symbols - std::ostringstream os; - os << "BVUDivByZero_" << width; - Node divByZero = - nm->mkSkolem(os.str(), - nm->mkFunctionType(nm->mkBitVectorType(width), - nm->mkBitVectorType(width)), - "partial bvudiv", - NodeManager::SKOLEM_EXACT_NAME); - d_ufDivByZero[width] = divByZero; - } - return d_ufDivByZero[width]; - } - else if (k == kind::BITVECTOR_UREM) - { - if (d_ufRemByZero.find(width) == d_ufRemByZero.end()) - { - std::ostringstream os; - os << "BVURemByZero_" << width; - Node divByZero = - nm->mkSkolem(os.str(), - nm->mkFunctionType(nm->mkBitVectorType(width), - nm->mkBitVectorType(width)), - "partial bvurem", - NodeManager::SKOLEM_EXACT_NAME); - d_ufRemByZero[width] = divByZero; - } - return d_ufRemByZero[width]; - } - - Unreachable(); -} - TrustNode TheoryBV::expandDefinition(Node node) { Debug("bitvector-expandDefinition") @@ -180,19 +138,6 @@ TrustNode TheoryBV::expandDefinition(Node node) ret = TheoryBVRewriter::eliminateBVSDiv(node); break; - case kind::BITVECTOR_UDIV: - case kind::BITVECTOR_UREM: - { - NodeManager* nm = NodeManager::currentNM(); - - Kind kind = node.getKind() == kind::BITVECTOR_UDIV - ? kind::BITVECTOR_UDIV_TOTAL - : kind::BITVECTOR_UREM_TOTAL; - ret = nm->mkNode(kind, node[0], node[1]); - break; - } - break; - default: break; } if (!ret.isNull() && node != ret) diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index fafde0601..685f25a92 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -107,24 +107,9 @@ class TheoryBV : public Theory private: void notifySharedTerm(TNode t) override; - /** - * Return the UF symbol corresponding to division-by-zero for this particular - * bit-width. - * @param k should be UREM or UDIV - * @param width bit-width - */ - Node getUFDivByZero(Kind k, unsigned width); - /** Internal BV solver. */ std::unique_ptr<BVSolver> d_internal; - /** - * Maps from bit-vector width to division-by-zero uninterpreted - * function symbols. - */ - std::unordered_map<unsigned, Node> d_ufDivByZero; - std::unordered_map<unsigned, Node> d_ufRemByZero; - /** The theory rewriter for this theory. */ TheoryBVRewriter d_rewriter; 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 dfcc4f052..2334d96f2 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h +++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h @@ -198,9 +198,7 @@ Node RewriteRule<EvalNeg>::apply(TNode node) { } template<> inline bool RewriteRule<EvalUdiv>::applies(TNode node) { - return (utils::isBvConstTerm(node) && - (node.getKind() == kind::BITVECTOR_UDIV_TOTAL || - (node.getKind() == kind::BITVECTOR_UDIV && node[1].isConst()))); + return utils::isBvConstTerm(node) && node.getKind() == kind::BITVECTOR_UDIV; } template<> inline @@ -214,9 +212,7 @@ Node RewriteRule<EvalUdiv>::apply(TNode node) { } template<> inline bool RewriteRule<EvalUrem>::applies(TNode node) { - return (utils::isBvConstTerm(node) && - (node.getKind() == kind::BITVECTOR_UREM_TOTAL || - (node.getKind() == kind::BITVECTOR_UREM && node[1].isConst()))); + return utils::isBvConstTerm(node) && node.getKind() == kind::BITVECTOR_UREM; } template<> inline diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index 2fff03c10..dda5c0420 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -464,7 +464,7 @@ inline Node RewriteRule<SdivEliminate>::apply(TNode node) Node abs_b = nm->mkNode(kind::ITE, b_lt_0, nm->mkNode(kind::BITVECTOR_NEG, b), b); - Node a_udiv_b = nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, abs_a, abs_b); + Node a_udiv_b = nm->mkNode(kind::BITVECTOR_UDIV, abs_a, abs_b); Node neg_result = nm->mkNode(kind::BITVECTOR_NEG, a_udiv_b); Node condition = nm->mkNode(kind::XOR, a_lt_0, b_lt_0); @@ -502,7 +502,7 @@ inline Node RewriteRule<SdivEliminateFewerBitwiseOps>::apply(TNode node) Node abs_b = nm->mkNode(kind::ITE, b_lt_0, nm->mkNode(kind::BITVECTOR_NEG, b), b); - Node a_udiv_b = nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, abs_a, abs_b); + Node a_udiv_b = nm->mkNode(kind::BITVECTOR_UDIV, abs_a, abs_b); Node neg_result = nm->mkNode(kind::BITVECTOR_NEG, a_udiv_b); Node result = nm->mkNode(kind::ITE, a_lt_0.xorNode(b_lt_0), neg_result, a_udiv_b); @@ -536,7 +536,7 @@ inline Node RewriteRule<SremEliminate>::apply(TNode node) Node abs_b = nm->mkNode(kind::ITE, b_lt_0, nm->mkNode(kind::BITVECTOR_NEG, b), b); - Node a_urem_b = nm->mkNode(kind::BITVECTOR_UREM_TOTAL, abs_a, abs_b); + Node a_urem_b = nm->mkNode(kind::BITVECTOR_UREM, abs_a, abs_b); Node neg_result = nm->mkNode(kind::BITVECTOR_NEG, a_urem_b); Node result = nm->mkNode(kind::ITE, a_lt_0, neg_result, a_urem_b); @@ -571,7 +571,7 @@ inline Node RewriteRule<SremEliminateFewerBitwiseOps>::apply(TNode node) nm->mkNode(kind::ITE, a_lt_0, nm->mkNode(kind::BITVECTOR_NEG, a), a); Node abs_b = nm->mkNode(kind::ITE, b_lt_0, nm->mkNode(kind::BITVECTOR_NEG, b), b); - Node a_urem_b = nm->mkNode(kind::BITVECTOR_UREM_TOTAL, abs_a, abs_b); + Node a_urem_b = nm->mkNode(kind::BITVECTOR_UREM, abs_a, abs_b); Node neg_result = nm->mkNode(kind::BITVECTOR_NEG, a_urem_b); Node result = nm->mkNode(kind::ITE, a_lt_0, neg_result, a_urem_b); diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index ca26577bf..d5a230098 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -1393,7 +1393,7 @@ template <> inline bool RewriteRule<UdivPow2>::applies(TNode node) { bool isNeg = false; - if (node.getKind() == kind::BITVECTOR_UDIV_TOTAL + if (node.getKind() == kind::BITVECTOR_UDIV && utils::isPow2Const(node[1], isNeg)) { return !isNeg; @@ -1439,8 +1439,8 @@ inline Node RewriteRule<UdivPow2>::apply(TNode node) template <> inline bool RewriteRule<UdivZero>::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL && - node[1] == utils::mkConst(utils::getSize(node), 0)); + return (node.getKind() == kind::BITVECTOR_UDIV + && node[1] == utils::mkConst(utils::getSize(node), 0)); } template <> @@ -1459,8 +1459,8 @@ inline Node RewriteRule<UdivZero>::apply(TNode node) { template <> inline bool RewriteRule<UdivOne>::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL && - node[1] == utils::mkConst(utils::getSize(node), 1)); + return (node.getKind() == kind::BITVECTOR_UDIV + && node[1] == utils::mkConst(utils::getSize(node), 1)); } template <> @@ -1481,7 +1481,7 @@ template <> inline bool RewriteRule<UremPow2>::applies(TNode node) { bool isNeg; - if (node.getKind() == kind::BITVECTOR_UREM_TOTAL + if (node.getKind() == kind::BITVECTOR_UREM && utils::isPow2Const(node[1], isNeg)) { return !isNeg; @@ -1521,8 +1521,8 @@ inline Node RewriteRule<UremPow2>::apply(TNode node) template<> inline bool RewriteRule<UremOne>::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_UREM_TOTAL && - node[1] == utils::mkConst(utils::getSize(node), 1)); + return (node.getKind() == kind::BITVECTOR_UREM + && node[1] == utils::mkConst(utils::getSize(node), 1)); } template<> inline @@ -1541,8 +1541,7 @@ Node RewriteRule<UremOne>::apply(TNode node) { template<> inline bool RewriteRule<UremSelf>::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_UREM_TOTAL && - node[0] == node[1]); + return (node.getKind() == kind::BITVECTOR_UREM && node[0] == node[1]); } template<> inline @@ -1590,7 +1589,7 @@ template <> inline bool RewriteRule<UgtUrem>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_UGT - && node[0].getKind() == kind::BITVECTOR_UREM_TOTAL + && node[0].getKind() == kind::BITVECTOR_UREM && node[0][1] == node[1]); } diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index b883ab537..4651b9256 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -440,18 +440,6 @@ RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool prerewrite) { RewriteResponse TheoryBVRewriter::RewriteUdiv(TNode node, bool prerewrite){ Node resultNode = node; - return RewriteUdivTotal(node, prerewrite); -} - -RewriteResponse TheoryBVRewriter::RewriteUrem(TNode node, bool prerewrite){ - Node resultNode = node; - - return RewriteUremTotal(node, prerewrite); -} - -RewriteResponse TheoryBVRewriter::RewriteUdivTotal(TNode node, bool prerewrite){ - Node resultNode = node; - if(RewriteRule<UdivPow2>::applies(node)) { resultNode = RewriteRule<UdivPow2>::run <false> (node); return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); @@ -464,7 +452,8 @@ RewriteResponse TheoryBVRewriter::RewriteUdivTotal(TNode node, bool prerewrite){ return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteUremTotal(TNode node, bool prerewrite) { +RewriteResponse TheoryBVRewriter::RewriteUrem(TNode node, bool prerewrite) +{ Node resultNode = node; if(RewriteRule<UremPow2>::applies(node)) { @@ -477,7 +466,7 @@ RewriteResponse TheoryBVRewriter::RewriteUremTotal(TNode node, bool prerewrite) RewriteRule<UremOne>, RewriteRule<UremSelf> >::apply(node); - return RewriteResponse(REWRITE_DONE, resultNode); + return RewriteResponse(REWRITE_DONE, resultNode); } RewriteResponse TheoryBVRewriter::RewriteSmod(TNode node, bool prerewrite) { @@ -705,8 +694,6 @@ void TheoryBVRewriter::initializeRewrites() { d_rewriteTable [ kind::BITVECTOR_NEG ] = RewriteNeg; d_rewriteTable [ kind::BITVECTOR_UDIV ] = RewriteUdiv; d_rewriteTable [ kind::BITVECTOR_UREM ] = RewriteUrem; - d_rewriteTable [ kind::BITVECTOR_UDIV_TOTAL ] = RewriteUdivTotal; - d_rewriteTable [ kind::BITVECTOR_UREM_TOTAL ] = RewriteUremTotal; d_rewriteTable [ kind::BITVECTOR_SMOD ] = RewriteSmod; d_rewriteTable [ kind::BITVECTOR_SDIV ] = RewriteSdiv; d_rewriteTable [ kind::BITVECTOR_SREM ] = RewriteSrem; |