From aeeb951b0fcc33e03feb6a6300808834a96daff5 Mon Sep 17 00:00:00 2001 From: lianah Date: Sat, 14 Jun 2014 20:44:00 -0400 Subject: [PATCH] bv static learning and rewrites for power of 2 terms --- src/theory/bv/bv_subtheory_bitblast.cpp | 1 + src/theory/bv/theory_bv.cpp | 36 +++++- src/theory/bv/theory_bv_rewrite_rules.h | 5 +- .../theory_bv_rewrite_rules_simplification.h | 105 ++++++++---------- src/theory/bv/theory_bv_utils.h | 5 +- 5 files changed, 86 insertions(+), 66 deletions(-) diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index d606ccee8..ebe017ee1 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -96,6 +96,7 @@ void BitblastSolver::bitblastQueue() { while (!d_bitblastQueue.empty()) { TNode atom = d_bitblastQueue.front(); d_bitblastQueue.pop(); + Debug("bv-bitblast-queue") << "BitblastSolver::bitblastQueue (" << atom << ")\n"; if (options::bvAbstraction() && d_abstractionModule->isLemmaAtom(atom)) { // don't bit-blast lemma atoms diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 04b8e9d6e..5be02322d 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -560,9 +560,7 @@ Node TheoryBV::ppRewrite(TNode t) } else if (RewriteRule::applies(t)) { Node result = RewriteRule::run(t); res = Rewriter::rewrite(result); - } - - if( res.getKind() == kind::EQUAL && + } else if( res.getKind() == kind::EQUAL && ((res[0].getKind() == kind::BITVECTOR_PLUS && RewriteRule::applies(res[1])) || res[1].getKind() == kind::BITVECTOR_PLUS && @@ -579,6 +577,8 @@ Node TheoryBV::ppRewrite(TNode t) } else { res = t; } + } else if (RewriteRule::applies(t)) { + res = RewriteRule::run(t); } @@ -729,7 +729,35 @@ void TheoryBV::enableCoreTheorySlicer() { } -void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) {} +void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) { + if (in.getKind() == kind::EQUAL) { + if(in[0].getKind() == kind::BITVECTOR_PLUS && in[1].getKind() == kind::BITVECTOR_SHL || + in[1].getKind() == kind::BITVECTOR_PLUS && in[0].getKind() == kind::BITVECTOR_SHL){ + TNode p = in[0].getKind() == kind::BITVECTOR_PLUS ? in[0] : in[1]; + TNode s = in[0].getKind() == kind::BITVECTOR_PLUS ? in[1] : in[0]; + + if(p.getNumChildren() == 2 + && p[0].getKind() == kind::BITVECTOR_SHL + && p[1].getKind() == kind::BITVECTOR_SHL ){ + unsigned size = utils::getSize(s); + Node one = utils::mkConst(size, 1u); + if(s[0] == one && p[0][0] == one && p[1][0] == one){ + Node zero = utils::mkConst(size, 0u); + TNode b = p[0]; + TNode c = p[1]; + // (s : 1 << S) = (b : 1 << B) + (c : 1 << C) + Node b_eq_0 = b.eqNode(zero); + Node c_eq_0 = c.eqNode(zero); + Node b_eq_c = b.eqNode(c); + + Node dis = utils::mkNode(kind::OR, b_eq_0, c_eq_0, b_eq_c); + Node imp = in.impNode(dis); + learned << imp; + } + } + } + } +} bool TheoryBV::applyAbstraction(const std::vector& assertions, std::vector& new_assertions) { bool changed = d_abstractionModule->applyAbstraction(assertions, new_assertions); diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index eadb63671..5e85cb145 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -165,7 +165,8 @@ enum RewriteRuleId { // rules to simplify bitblasting BBPlusNeg, UltPlusOne, - ConcatToMult + ConcatToMult, + IsPowerOfTwo }; @@ -293,6 +294,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case MultDistrib: out << "MultDistrib"; return out; case UltPlusOne: out << "UltPlusOne"; return out; case ConcatToMult: out << "ConcatToMult"; return out; + case IsPowerOfTwo: out << "IsPowerOfTwo"; return out; default: Unreachable(); } @@ -516,6 +518,7 @@ struct AllRewriteRules { RewriteRule rule118; RewriteRule rule119; RewriteRule rule120; + RewriteRule rule121; }; template<> inline diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index 71df1edca..33994782a 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -1193,67 +1193,52 @@ Node RewriteRule::apply(TNode node) { return utils::mkNode(kind::AND, not_y_eq_1, not_y_lt_x); } +/** + * x ^(x-1) = 0 => 1 << sk + * Note: only to be called in ppRewrite and not rewrite! + * (it calls the rewriter) + * + * @param node + * + * @return + */ +template<> inline +bool RewriteRule::applies(TNode node) { + if (node.getKind()!= kind::EQUAL) return false; + if (node[0].getKind() != kind::BITVECTOR_AND && + node[1].getKind() != kind::BITVECTOR_AND) + return false; + if (!utils::isZero(node[0]) && + !utils::isZero(node[1])) + return false; + + TNode t = !utils::isZero(node[0])? node[0]: node[1]; + if (t.getNumChildren() != 2) return false; + TNode a = t[0]; + TNode b = t[1]; + unsigned size = utils::getSize(t); + if(size < 2) return false; + Node diff = Rewriter::rewrite(utils::mkNode(kind::BITVECTOR_SUB, a, b)); + return (diff.isConst() && (diff == utils::mkConst(size, 1u) || diff == utils::mkOnes(size))); +} + +template<> inline +Node RewriteRule::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + TNode term = utils::isZero(node[0])? node[1] : node[0]; + TNode a = term[0]; + TNode b = term[1]; + unsigned size = utils::getSize(term); + Node diff = Rewriter::rewrite(utils::mkNode(kind::BITVECTOR_SUB, a, b)); + Assert (diff.isConst()); + TNode x = diff == utils::mkConst(size, 1u) ? a : b; + Node one = utils::mkConst(size, 1u); + Node sk = utils::mkVar(size); + Node sh = utils::mkNode(kind::BITVECTOR_SHL, one, sk); + Node x_eq_sh = utils::mkNode(kind::EQUAL, x, sh); + return x_eq_sh; +} -// /** -// * -// * -// * -// */ - -// template<> inline -// bool RewriteRule::applies(TNode node) { -// if (node.getKind() != kind::BITVECTOR_PLUS) { -// return false; -// } - -// for (unsigned i = 0; i < node.getNumChildren(); ++i) { -// if (node[i].getKind() != kind::BITVECTOR_MULT) { -// return false; -// } -// } -// } - -// template<> inline -// Node RewriteRule::apply(TNode node) { -// Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; -// std::hash_set factors; - -// for (unsigned i = 0; i < node.getNumChildren(); ++i) { -// Assert (node[i].getKind() == kind::BITVECTOR_MULT); -// for (unsigned j = 0; j < node[i].getNumChildren(); ++j) { -// factors.insert(node[i][j]); -// } -// } - -// std::vector gcd; -// std::hash_set::const_iterator it; -// for (it = factors.begin(); it != factors.end(); ++it) { -// // for each factor check if it occurs in all children -// TNode f = *it; -// for (unsigned i = 0; i < node.getNumChildren - -// } -// } -// return ; -// } - - -// /** -// * -// * -// * -// */ - -// template<> inline -// bool RewriteRule<>::applies(TNode node) { -// return (node.getKind() == ); -// } - -// template<> inline -// Node RewriteRule<>::apply(TNode node) { -// Debug("bv-rewrite") << "RewriteRule<>(" << node << ")" << std::endl; -// return ; -// } diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 3650d3091..9679c0260 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -332,7 +332,10 @@ inline Node mkAnd(const std::vector& conjunctions) { return conjunction; }/* mkAnd() */ - +inline bool isZero(TNode node) { + if (!node.isConst()) return false; + return node == utils::mkConst(utils::getSize(node), 0u); +} inline Node flattenAnd(std::vector& queue) { TNodeSet nodes; -- 2.30.2