From: lianah Date: Tue, 30 Apr 2013 17:42:50 +0000 (-0400) Subject: added several rewrite rules (BitwiseSlicing, Ule/SleEliminate, ExtractSignExtend... X-Git-Tag: cvc5-1.0.0~7296 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2ba4f51d43406c9475116abbab7f3ebea94679af;p=cvc5.git added several rewrite rules (BitwiseSlicing, Ule/SleEliminate, ExtractSignExtend) and bvurem lemma --- diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index ab25fa6cb..fa5f53113 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -101,6 +101,7 @@ void BVMinisatSatSolver::interrupt(){ } SatValue BVMinisatSatSolver::solve(){ + ++d_statistics.d_statCallsToSolve; return toSatLiteralValue(d_minisat->solve()); } @@ -121,30 +122,6 @@ SatValue BVMinisatSatSolver::solve(long unsigned int& resource){ return result; } -// SatValue BVMinisatSatSolver::solve(const context::CDList & assumptions, bool only_bcp){ -// ++d_solveCount; -// ++d_statistics.d_statCallsToSolve; - -// Debug("sat::minisat") << "Solve with assumptions "; -// context::CDList::const_iterator it = assumptions.begin(); -// BVMinisat::vec assump; -// for(; it!= assumptions.end(); ++it) { -// SatLiteral lit = *it; -// Debug("sat::minisat") << lit <<" "; -// assump.push(toMinisatLit(lit)); -// } -// Debug("sat::minisat") <<"\n"; - -// clock_t begin, end; -// begin = clock(); -// d_minisat->setOnlyBCP(only_bcp); -// SatLiteralValue result = toSatLiteralValue(d_minisat->solve(assump)); -// end = clock(); -// d_statistics.d_statSolveTime = d_statistics.d_statSolveTime.getData() + (end - begin)/(double)CLOCKS_PER_SEC; -// return result; -// } - - void BVMinisatSatSolver::getUnsatCore(SatClause& unsatCore) { // TODO add assertion to check the call was after an unsat call for (int i = 0; i < d_minisat->conflict.size(); ++i) { diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 953f9b3e5..b2f91e070 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -132,16 +132,22 @@ void TheoryBV::checkForLemma(TNode fact) { TNode urem = fact[0]; TNode result = fact[1]; TNode divisor = urem[1]; - Node result_ult_div = utils::mkNode(kind::BITVECTOR_ULT, result, divisor); - Node split = utils::mkNode(kind::OR, utils::mkNode(kind::NOT, fact), result_ult_div); + Node result_ult_div = mkNode(kind::BITVECTOR_ULT, result, divisor); + Node divisor_eq_0 = mkNode(kind::EQUAL, + divisor, + mkConst(BitVector(getSize(divisor), 0u))); + Node split = utils::mkNode(kind::OR, divisor_eq_0, mkNode(kind::NOT, fact), result_ult_div); lemma(split); } if (fact[1].getKind() == kind::BITVECTOR_UREM_TOTAL) { TNode urem = fact[1]; TNode result = fact[0]; TNode divisor = urem[1]; - Node result_ult_div = utils::mkNode(kind::BITVECTOR_ULT, result, divisor); - Node split = utils::mkNode(kind::OR, utils::mkNode(kind::NOT, fact), result_ult_div); + Node result_ult_div = mkNode(kind::BITVECTOR_ULT, result, divisor); + Node divisor_eq_0 = mkNode(kind::EQUAL, + divisor, + mkConst(BitVector(getSize(divisor), 0u))); + Node split = utils::mkNode(kind::OR, divisor_eq_0, mkNode(kind::NOT, fact), result_ult_div); lemma(split); } } diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index d362fa603..baaf7e133 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -52,6 +52,7 @@ enum RewriteRuleId { SubEliminate, SltEliminate, SleEliminate, + UleEliminate, CompEliminate, RepeatEliminate, RotateLeftEliminate, @@ -135,6 +136,7 @@ enum RewriteRuleId { ExtractNot, ExtractArith, ExtractArith2, + ExtractSignExtend, DoubleNeg, NegMult, NegSub, @@ -152,7 +154,7 @@ enum RewriteRuleId { AndSimplify, OrSimplify, XorSimplify, - UleEliminate, + BitwiseSlicing, // rules to simplify bitblasting BBPlusNeg }; @@ -270,7 +272,9 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case UltOne : out << "UltOne"; return out; case SltZero : out << "SltZero"; return out; case ZeroUlt : out << "ZeroUlt"; return out; - case UleEliminate : out << "UleEliminate"; return out; + case UleEliminate : out << "UleEliminate"; return out; + case BitwiseSlicing : out << "BitwiseSlicing"; return out; + case ExtractSignExtend : out << "ExtractSignExtend"; return out; default: Unreachable(); } diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 4ba09ef67..035bd4469 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -72,6 +72,58 @@ Node RewriteRule::apply(TNode node) { return utils::mkNode(kind::BITVECTOR_NOT, a); } +/** + * ExtractSignExtend + * + * (sign_extend k x) [i:j] => pushes extract in + * + * @return + */ + +template<> inline +bool RewriteRule::applies(TNode node) { + if (node.getKind() == kind::BITVECTOR_EXTRACT && + node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND) { + return true; + } + return false; +} + +template<> inline +Node RewriteRule::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + TNode extendee = node[0][0]; + unsigned extendee_size = utils::getSize(extendee); + + unsigned high = utils::getExtractHigh(node); + unsigned low = utils::getExtractLow(node); + + Node resultNode; + // extract falls on extendee + if (high < extendee_size) { + resultNode = utils::mkExtract(extendee, high, low); + } else if (low < extendee_size && high >= extendee_size) { + // if extract overlaps sign extend and extendee + Node low_extract = utils::mkExtract(extendee, extendee_size - 1, low); + unsigned new_ammount = high - extendee_size + 1; + resultNode = utils::mkSignExtend(low_extract, new_ammount); + } else { + // extract only over sign extend + Assert (low >= extendee_size); + unsigned top = utils::getSize(extendee) - 1; + Node most_significant_bit = utils::mkExtract(extendee, top, top); + std::vector bits; + for (unsigned i = 0; i < high - low + 1; ++i) { + bits.push_back(most_significant_bit); + } + resultNode = utils::mkNode(kind::BITVECTOR_CONCAT, bits); + } + Debug("bv-rewrite") << " =>" << resultNode << std::endl; + return resultNode; +} + + + /** * ExtractArith * @@ -1032,19 +1084,84 @@ Node RewriteRule::apply(TNode node) { } +/** + * BitwiseSlicing + * + * (a bvand c) ==> (concat (bvand a[i0:j0] c0) ... (bvand a[in:jn] cn)) + * where c0,..., cn are maximally continuous substrings of 0 or 1 in the constant c + * + * Note: this rule assumes AndSimplify has already been called on the node + */ +template<> inline +bool RewriteRule::applies(TNode node) { + if ((node.getKind() != kind::BITVECTOR_AND && + node.getKind() != kind::BITVECTOR_OR && + node.getKind() != kind::BITVECTOR_XOR) || + utils::getSize(node) == 1) + return false; + + for (unsigned i = 0; i < node.getNumChildren(); ++i) { + if (node[i].getKind() == kind::CONST_BITVECTOR) { + BitVector constant = node[i].getConst(); + // we do not apply the rule if the constant is all 0s or all 1s + if (constant == BitVector(utils::getSize(node), 0u)) + return false; + + for (unsigned i = 0; i < constant.getSize(); ++i) { + if (!constant.isBitSet(i)) + return true; + } + } + } + return false; +} +template<> inline +Node RewriteRule::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + // get the constant + bool found_constant = false; + TNode constant; + std::vector other_children; + for (unsigned i = 0; i < node.getNumChildren(); ++i) { + if (node[i].getKind() == kind::CONST_BITVECTOR) { + constant = node[i]; + Assert (!found_constant); + found_constant = true; + } else { + other_children.push_back(node[i]); + } + } + Assert (found_constant && other_children.size() == node.getNumChildren() - 1); -// template<> inline -// bool RewriteRule::applies(TNode node) { -// return (node.getKind() == kind::BITVECTOR_AND); -// } - -// template<> inline -// Node RewriteRule::apply(TNode node) { -// Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; -// return resultNode; -// } + Node other = utils::mkNode(node.getKind(), other_children); + + BitVector bv_constant = constant.getConst(); + std::vector concat_children; + int start = bv_constant.getSize() - 1; + int end = start; + for (int i = end - 1; i >= 0; --i) { + if (bv_constant.isBitSet(i + 1) != bv_constant.isBitSet(i)) { + Node other_extract = utils::mkExtract(other, end, start); + Node const_extract = utils::mkExtract(constant, end, start); + Node bitwise_op = utils::mkNode(node.getKind(), const_extract, other_extract); + concat_children.push_back(bitwise_op); + start = end = i; + } else { + start--; + } + if (i == 0) { + Node other_extract = utils::mkExtract(other, end, 0); + Node const_extract = utils::mkExtract(constant, end, 0); + Node bitwise_op = utils::mkNode(node.getKind(), const_extract, other_extract); + concat_children.push_back(bitwise_op); + } + } + Node result = utils::mkNode(kind::BITVECTOR_CONCAT, concat_children); + Debug("bv-rewrite") << " =>" << result << std::endl; + return result; +} // template<> inline // bool RewriteRule<>::applies(TNode node) { diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index f6d138f5d..44c498947 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -177,6 +177,11 @@ RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node, bool preregister) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } + // if (RewriteRule::applies(node)) { + // resultNode = RewriteRule::run(node); + // return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + // } + if (RewriteRule::applies(node)) { resultNode = RewriteRule::run(node); return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); @@ -223,14 +228,14 @@ RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool preregister){ resultNode = LinearRewriteStrategy < RewriteRule, - RewriteRule - // RewriteRule, - // RewriteRule, - // //RewriteRule, -> might need rw again - // RewriteRule, - // RewriteRule + RewriteRule//, + // RewriteRule >::apply(node); + if (resultNode.getKind() != node.getKind()) { + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } + return RewriteResponse(REWRITE_DONE, resultNode); } @@ -239,8 +244,13 @@ RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool preregister){ resultNode = LinearRewriteStrategy < RewriteRule, - RewriteRule + RewriteRule//, + // RewriteRule >::apply(node); + + if (resultNode.getKind() != node.getKind()) { + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } return RewriteResponse(REWRITE_DONE, resultNode); } @@ -251,7 +261,8 @@ RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool preregister) { resultNode = LinearRewriteStrategy < RewriteRule, // flatten the expression RewriteRule, // simplify duplicates and constants - RewriteRule // checks if the constant part is zero and eliminates it + RewriteRule//, // checks if the constant part is zero and eliminates it + // RewriteRule >::apply(node); // this simplification introduces new terms and might require further @@ -261,6 +272,10 @@ RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool preregister) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } + if (resultNode.getKind() != node.getKind()) { + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } + return RewriteResponse(REWRITE_DONE, resultNode); } @@ -301,7 +316,8 @@ RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool preregister) { resultNode = LinearRewriteStrategy < RewriteRule, // flattens and sorts - RewriteRule // multiplies constant part and checks for 0 + RewriteRule, // multiplies constant part and checks for 0 + RewriteRule // replaces multiplication by a power of 2 by a shift >::apply(node); // only apply if every subterm was already rewritten @@ -317,7 +333,7 @@ RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool preregister) { if(resultNode == node) { return RewriteResponse(REWRITE_DONE, resultNode); } - return RewriteResponse(REWRITE_DONE, resultNode); + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } RewriteResponse TheoryBVRewriter::RewritePlus(TNode node, bool preregister) { diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 174df03ab..5847bac3e 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -84,6 +84,7 @@ inline Node mkSortedNode(Kind kind, std::vector& children) { inline Node mkNode(Kind kind, std::vector& children) { + Assert (children.size() > 0); if (children.size() == 1) { return children[0]; } @@ -133,6 +134,12 @@ inline Node mkXor(TNode node1, TNode node2) { } +inline Node mkSignExtend(TNode node, unsigned ammount) { + NodeManager* nm = NodeManager::currentNM(); + Node signExtendOp = nm->mkConst(BitVectorSignExtend(ammount)); + return nm->mkNode(signExtendOp, node); +} + inline Node mkExtract(TNode node, unsigned high, unsigned low) { Node extractOp = NodeManager::currentNM()->mkConst(BitVectorExtract(high, low)); std::vector children;