From 22a646e2322c1c571492bb2a835466c69047ce14 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 14 Jun 2017 15:53:51 -0700 Subject: [PATCH] Remove UdivSelf rewrite, add UdivZero rewrite This fixes bug 820. The issue was that (a udiv a) got rewriten to 1, which is not correct when a is 0 (the result is all ones in that case). Even with the --bv-div-zero-const flag disabled, the UdivSelf rewrite was incorrect because it was applied to BITVECTOR_UDIV_TOTAL, which is "defined to be the all-ones bit pattern, if divisor is 0" according to src/theory/bv/kinds . The commit adds instead an optimization that returns all ones if the divisor of a BITVECTOR_UDIV_TOTAL is zero. --- src/theory/bv/theory_bv_rewrite_rules.h | 27 +++++++------- .../theory_bv_rewrite_rules_simplification.h | 36 +++++++++---------- src/theory/bv/theory_bv_rewriter.cpp | 8 ++--- 3 files changed, 35 insertions(+), 36 deletions(-) diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index 5957c641d..39e8e38cd 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -56,7 +56,7 @@ enum RewriteRuleId { SubEliminate, SltEliminate, SleEliminate, - UleEliminate, + UleEliminate, CompEliminate, RepeatEliminate, RotateLeftEliminate, @@ -75,7 +75,7 @@ enum RewriteRuleId { /// ground term evaluation EvalEquals, - EvalConcat, + EvalConcat, EvalAnd, EvalOr, EvalXor, @@ -90,7 +90,7 @@ enum RewriteRuleId { EvalUlt, EvalUltBv, EvalUle, - EvalExtract, + EvalExtract, EvalSignExtend, EvalRotateLeft, EvalRotateRight, @@ -133,18 +133,18 @@ enum RewriteRuleId { ExtractMultLeadingBit, NegIdemp, UdivPow2, + UdivZero, UdivOne, - UdivSelf, UremPow2, UremOne, UremSelf, ShiftZero, UltOne, - SltZero, + SltZero, ZeroUlt, MergeSignExtend, - + /// normalization rules ExtractBitwise, ExtractNot, @@ -156,9 +156,9 @@ enum RewriteRuleId { NegSub, NegPlus, NotConcat, - NotAnd, // not sure why this would help (not done) - NotOr, // not sure why this would help (not done) - NotXor, // not sure why this would help (not done) + NotAnd, // not sure why this would help (not done) + NotOr, // not sure why this would help (not done) + NotXor, // not sure why this would help (not done) FlattenAssocCommut, FlattenAssocCommutNoDuplicates, PlusCombineLikeTerms, @@ -178,7 +178,6 @@ enum RewriteRuleId { IsPowerOfTwo }; - inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { switch (ruleId) { case EmptyRule: out << "EmptyRule"; return out; @@ -272,8 +271,10 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case ExtractMultLeadingBit : out << "ExtractMultLeadingBit"; return out; case NegIdemp : out << "NegIdemp"; return out; case UdivPow2 : out << "UdivPow2"; return out; + case UdivZero: + out << "UdivZero"; + return out; case UdivOne : out << "UdivOne"; return out; - case UdivSelf : out << "UdivSelf"; return out; case UremPow2 : out << "UremPow2"; return out; case UremOne : out << "UremOne"; return out; case UremSelf : out << "UremSelf"; return out; @@ -501,8 +502,8 @@ struct AllRewriteRules { RewriteRule rule88; RewriteRule rule91; RewriteRule rule92; - RewriteRule rule93; - RewriteRule rule94; + RewriteRule rule93; + RewriteRule rule94; RewriteRule rule95; RewriteRule rule96; RewriteRule rule97; diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index 871380467..c49319387 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -908,39 +908,39 @@ Node RewriteRule::apply(TNode node) { } /** - * UdivOne + * UdivZero * - * (a udiv 1) ==> a + * (a udiv 0) ==> 111...1 */ -template<> inline -bool RewriteRule::applies(TNode node) { +template <> +inline bool RewriteRule::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL && - node[1] == utils::mkConst(utils::getSize(node), 1)); + node[1] == utils::mkConst(utils::getSize(node), 0)); } -template<> inline -Node RewriteRule::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; - return node[0]; +template <> +inline Node RewriteRule::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + return utils::mkOnes(utils::getSize(node)); } /** - * UdivSelf + * UdivOne * - * (a udiv a) ==> 1 + * (a udiv 1) ==> a */ -template<> inline -bool RewriteRule::applies(TNode node) { +template <> +inline bool RewriteRule::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL && - node[0] == node[1]); + node[1] == utils::mkConst(utils::getSize(node), 1)); } -template<> inline -Node RewriteRule::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; - return utils::mkConst(utils::getSize(node), 1); +template <> +inline Node RewriteRule::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + return node[0]; } /** diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index e40612ba6..df21093c1 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -439,11 +439,9 @@ RewriteResponse TheoryBVRewriter::RewriteUdivTotal(TNode node, bool prerewrite){ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } - resultNode = LinearRewriteStrategy - < RewriteRule, - RewriteRule, - RewriteRule - >::apply(node); + resultNode = + LinearRewriteStrategy, RewriteRule, + RewriteRule >::apply(node); return RewriteResponse(REWRITE_DONE, resultNode); } -- 2.30.2