From 12f48b0a11207ddbd34b2b2b88362250e9692ac2 Mon Sep 17 00:00:00 2001 From: lianah Date: Sun, 21 Apr 2013 19:00:09 -0400 Subject: [PATCH] added some bv rewrite rules --- src/theory/bv/theory_bv.cpp | 2 +- src/theory/bv/theory_bv_rewrite_rules.h | 12 +++- ...ry_bv_rewrite_rules_operator_elimination.h | 32 ++++++++--- .../theory_bv_rewrite_rules_simplification.h | 55 +++++++++++++++++++ src/theory/bv/theory_bv_rewriter.cpp | 10 +++- src/theory/term_registration_visitor.h | 5 -- 6 files changed, 98 insertions(+), 18 deletions(-) diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index fd2946d24..7cb06ca15 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -250,7 +250,7 @@ Node TheoryBV::ppRewrite(TNode t) // return Rewriter::rewrite(result); // } - if (options::bitvectorCoreSolver() && t.getKind() == kind::EQUAL) { + if (/*options::bitvectorCoreSolver() && */t.getKind() == kind::EQUAL) { std::vector equalities; Slicer::splitEqualities(t, equalities); return utils::mkAnd(equalities); diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index e9a3494f0..cff85b92b 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -125,6 +125,10 @@ enum RewriteRuleId { UremOne, UremSelf, ShiftZero, + + UltOne, + SltZero, + ZeroUlt, /// normalization rules ExtractBitwise, @@ -262,7 +266,10 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case OrSimplify : out << "OrSimplify"; return out; case XorSimplify : out << "XorSimplify"; return out; case NegPlus : out << "NegPlus"; return out; - case BBPlusNeg : out << "BBPlusNeg"; return out; + case BBPlusNeg : out << "BBPlusNeg"; return out; + case UltOne : out << "UltOne"; return out; + case SltZero : out << "SltZero"; return out; + case ZeroUlt : out << "ZeroUlt"; return out; default: Unreachable(); } @@ -477,6 +484,9 @@ struct AllRewriteRules { RewriteRule rule111; RewriteRule rule112; RewriteRule rule113; + RewriteRule rule114; + RewriteRule rule115; + }; 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 06ddc215d..b466aceae 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -103,6 +103,24 @@ Node RewriteRule::apply(TNode node) { } +// template <> +// bool RewriteRule::applies(TNode node) { +// return (node.getKind() == kind::BITVECTOR_SLE); +// } + +// template <> +// Node RewriteRule::apply(TNode node) { +// Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + +// unsigned size = utils::getSize(node[0]); +// Node pow_two = utils::mkConst(BitVector(size, Integer(1).multiplyByPow2(size - 1))); +// Node a = utils::mkNode(kind::BITVECTOR_PLUS, node[0], pow_two); +// Node b = utils::mkNode(kind::BITVECTOR_PLUS, node[1], pow_two); + +// return utils::mkNode(kind::BITVECTOR_ULE, a, b); + +// } + template <> bool RewriteRule::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_SLE); @@ -111,16 +129,14 @@ bool RewriteRule::applies(TNode node) { template <> Node RewriteRule::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; - - unsigned size = utils::getSize(node[0]); - Node pow_two = utils::mkConst(BitVector(size, Integer(1).multiplyByPow2(size - 1))); - Node a = utils::mkNode(kind::BITVECTOR_PLUS, node[0], pow_two); - Node b = utils::mkNode(kind::BITVECTOR_PLUS, node[1], pow_two); - - return utils::mkNode(kind::BITVECTOR_ULE, a, b); - + + TNode a = node[0]; + TNode b = node[1]; + Node b_slt_a = utils::mkNode(kind::BITVECTOR_SLT, b, a); + return utils::mkNode(kind::NOT, b_slt_a); } + template <> bool RewriteRule::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_COMP); diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index bcfb189af..d660dde29 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -523,6 +523,25 @@ Node RewriteRule::apply(TNode node) { return utils::mkTrue(); } +/** + * ZeroUlt + * + * 0 < a ==> a != 0 + */ + +template<> inline +bool RewriteRule::applies(TNode node) { + return (node.getKind() == kind::BITVECTOR_ULT && + node[0] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0)))); +} + +template<> inline +Node RewriteRule::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + return utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, node[0], node[1])); +} + + /** * UltZero * @@ -541,6 +560,42 @@ Node RewriteRule::apply(TNode node) { return utils::mkFalse(); } + +/** + * + */ +template<> inline +bool RewriteRule::applies(TNode node) { + return (node.getKind() == kind::BITVECTOR_ULT && + node[1] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(1)))); +} + +template<> inline +Node RewriteRule::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + return utils::mkNode(kind::EQUAL, node[0], utils::mkConst(BitVector(utils::getSize(node[0]), 0u))); +} + +/** + * + */ +template<> inline +bool RewriteRule::applies(TNode node) { + return (node.getKind() == kind::BITVECTOR_SLT && + node[1] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0)))); +} + +template<> inline +Node RewriteRule::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + unsigned size = utils::getSize(node[0]); + Node most_significant_bit = utils::mkExtract(node[0], size - 1, size - 1); + Node one = utils::mkConst(BitVector(1, 1u)); + + return utils::mkNode(kind::EQUAL, most_significant_bit, one); +} + + /** * UltSelf * diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index a712a8391..07499d01a 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -75,8 +75,10 @@ RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool preregister) { Node resultNode = LinearRewriteStrategy < RewriteRule, // if both arguments are constants evaluates - RewriteRule + RewriteRule, // a < 0 rewrites to false + RewriteRule, + RewriteRule >::apply(node); return RewriteResponse(REWRITE_DONE, resultNode); @@ -84,7 +86,8 @@ RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool preregister) { RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node, bool preregister){ Node resultNode = LinearRewriteStrategy - < RewriteRule < EvalSlt > + < RewriteRule < EvalSlt >, + RewriteRule < SltZero > >::apply(node); return RewriteResponse(REWRITE_DONE, resultNode); @@ -110,7 +113,8 @@ RewriteResponse TheoryBVRewriter::RewriteUle(TNode node, bool preregister){ RewriteResponse TheoryBVRewriter::RewriteSle(TNode node, bool preregister){ Node resultNode = LinearRewriteStrategy - < RewriteRule < EvalSle > + < RewriteRule , + RewriteRule >::apply(node); return RewriteResponse(REWRITE_DONE, resultNode); diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h index 5f89af9c6..d573213b7 100644 --- a/src/theory/term_registration_visitor.h +++ b/src/theory/term_registration_visitor.h @@ -95,11 +95,6 @@ public: * Notifies the engine of all the theories used. */ bool done(TNode node); - ~PreRegisterVisitor() { - for (TNodeToTheorySetMap::const_iterator it = d_visited.begin(); it != d_visited.end(); ++it) { - std::cout << it->first <<"\n"; - } - } }; -- 2.30.2