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.

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); 
 }