diff options
author | Clark Barrett <barrett@cs.stanford.edu> | 2017-06-14 19:56:56 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-06-14 19:56:56 -0700 |
commit | 8bb55a22b7c0f20305274f8609b9e8404e4bb41c (patch) | |
tree | 807f703fcc626d1af5c7b774ae5ed9d1488841be | |
parent | e8c8f864bdde2fbfc6ec7ec63928683cbd57ac0c (diff) | |
parent | 22a646e2322c1c571492bb2a835466c69047ce14 (diff) |
Merge pull request #167 from CVC4/fix_div
Remove UdivSelf rewrite, add UdivZero rewrite
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules.h | 27 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 36 | ||||
-rw-r--r-- | 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<ExtractMultLeadingBit> rule88; RewriteRule<NegIdemp> rule91; RewriteRule<UdivPow2> rule92; - RewriteRule<UdivOne> rule93; - RewriteRule<UdivSelf> rule94; + RewriteRule<UdivZero> rule93; + RewriteRule<UdivOne> rule94; RewriteRule<UremPow2> rule95; RewriteRule<UremOne> rule96; RewriteRule<UremSelf> 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<UdivPow2>::apply(TNode node) { } /** - * UdivOne + * UdivZero * - * (a udiv 1) ==> a + * (a udiv 0) ==> 111...1 */ -template<> inline -bool RewriteRule<UdivOne>::applies(TNode node) { +template <> +inline bool RewriteRule<UdivZero>::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<UdivOne>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<UdivOne>(" << node << ")" << std::endl; - return node[0]; +template <> +inline Node RewriteRule<UdivZero>::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule<UdivZero>(" << node << ")" << std::endl; + return utils::mkOnes(utils::getSize(node)); } /** - * UdivSelf + * UdivOne * - * (a udiv a) ==> 1 + * (a udiv 1) ==> a */ -template<> inline -bool RewriteRule<UdivSelf>::applies(TNode node) { +template <> +inline bool RewriteRule<UdivOne>::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<UdivSelf>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<UdivSelf>(" << node << ")" << std::endl; - return utils::mkConst(utils::getSize(node), 1); +template <> +inline Node RewriteRule<UdivOne>::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule<UdivOne>(" << 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<EvalUdiv>, - RewriteRule<UdivOne>, - RewriteRule<UdivSelf> - >::apply(node); + resultNode = + LinearRewriteStrategy<RewriteRule<EvalUdiv>, RewriteRule<UdivZero>, + RewriteRule<UdivOne> >::apply(node); return RewriteResponse(REWRITE_DONE, resultNode); } |