Add rewrite for nested BITVECTOR_ITE with cond_outer == cond_inner. (#2272)

3 files changed, 45 insertions, 9 deletions

diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 55614f4e6..d8f360492 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -105,8 +105,9 @@ enum RewriteRuleId
   /// simplification rules
   /// all of these rules decrease formula size
   BvIteConstCond,
-  BvIteChildren,
+  BvIteEqualChildren,
   BvIteConstChildren,
+  BvIteEqualCond,
   BvComp,
   ShlByConst,
   LshrByConst,
@@ -245,8 +246,9 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case EvalRotateRight :    out << "EvalRotateRight";     return out;
   case EvalNeg :            out << "EvalNeg";             return out;
   case BvIteConstCond :     out << "BvIteConstCond";      return out;
-  case BvIteChildren :      out << "BvIteChildren";       return out;
+  case BvIteEqualChildren : out << "BvIteEqualChildren";  return out;
   case BvIteConstChildren : out << "BvIteConstChildren";  return out;
+  case BvIteEqualCond :     out << "BvIteEqualCond";      return out;
   case BvComp :             out << "BvComp";              return out;
   case ShlByConst :         out << "ShlByConst";          return out;
   case LshrByConst :        out << "LshrByConst";         return out;
@@ -562,8 +564,9 @@ struct AllRewriteRules {
   RewriteRule<NormalizeEqPlusNeg>             rule129;
   RewriteRule<BvComp>                         rule130;
   RewriteRule<BvIteConstCond>                 rule131;
-  RewriteRule<BvIteChildren>                  rule132;
+  RewriteRule<BvIteEqualChildren>             rule132;
   RewriteRule<BvIteConstChildren>             rule133;
+  RewriteRule<BvIteEqualCond>                 rule134;
 };
 
 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 1213c0f05..a59f6524a 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -49,20 +49,20 @@ inline Node RewriteRule<BvIteConstCond>::apply(TNode node)
 }
 
 /**
- * BvIteChildren
+ * BvIteEqualChildren
  *
  * BITVECTOR_ITE with term_then = term_else
  */
 template <>
-inline bool RewriteRule<BvIteChildren>::applies(TNode node)
+inline bool RewriteRule<BvIteEqualChildren>::applies(TNode node)
 {
   return (node.getKind() == kind::BITVECTOR_ITE && node[1] == node[2]);
 }
 
 template <>
-inline Node RewriteRule<BvIteChildren>::apply(TNode node)
+inline Node RewriteRule<BvIteEqualChildren>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<BvIteChildren>(" << node << ")"
+  Debug("bv-rewrite") << "RewriteRule<BvIteEqualChildren>(" << node << ")"
                       << std::endl;
   return node[1];
 }
@@ -94,6 +94,38 @@ inline Node RewriteRule<BvIteConstChildren>::apply(TNode node)
 }
 
 /**
+ * BvIteEqualCond
+ *
+ * Nested BITVECTOR_ITE with cond_outer == cond_inner
+ *
+ * c0 ? (c0 ? t0 : e0) : e1              ->  c0 ? t0 : e1
+ * c0 ? t0             : (c0 ? t1 : e1)  ->  c0 ? t0 : e1
+ * c0 ? (c0 ? t0 : e0) : (c0 ? t1 : e1)  ->  c0 ? t0 : e1
+ */
+template <>
+inline bool RewriteRule<BvIteEqualCond>::applies(TNode node)
+{
+  return (
+      node.getKind() == kind::BITVECTOR_ITE
+      && ((node[1].getKind() == kind::BITVECTOR_ITE && node[0] == node[1][0])
+          || (node[2].getKind() == kind::BITVECTOR_ITE
+              && node[0] == node[2][0])));
+}
+
+template <>
+inline Node RewriteRule<BvIteEqualCond>::apply(TNode node)
+{
+  Debug("bv-rewrite") << "RewriteRule<BvIteEqualCond>(" << node << ")"
+                      << std::endl;
+  Node t0 = node[1].getKind() == kind::BITVECTOR_ITE && node[0] == node[1][0]
+                ? node[1][1]
+                : node[1];
+  Node e1 = node[2].getKind() == kind::BITVECTOR_ITE && node[0] == node[2][0]
+                ? node[2][2]
+                : node[2];
+  return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ITE, node[0], t0, e1);
+}
+/**
  * BvComp
  *
  * BITVECTOR_COMP of children of size 1 with one constant child
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index f0218bbc5..d63fe4009 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -171,8 +171,9 @@ RewriteResponse TheoryBVRewriter::RewriteITEBv(TNode node, bool prerewrite)
   Node resultNode =
       LinearRewriteStrategy<RewriteRule<EvalITEBv>,
                             RewriteRule<BvIteConstCond>,
-                            RewriteRule<BvIteChildren>,
-                            RewriteRule<BvIteConstChildren> >::apply(node);
+                            RewriteRule<BvIteEqualChildren>,
+                            RewriteRule<BvIteConstChildren>,
+                            RewriteRule<BvIteEqualCond>>::apply(node);
   return RewriteResponse(REWRITE_DONE, resultNode);
 }