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

diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 55614f4e6ad0b3167fb9bb29ceee7a540b88894f..d8f3604927e1419bd0c13f6abc1a1a8d16c3236b 100644 (file)
--- 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 1213c0f05d12ff0e98778a81e388cdc58f70bfce..a59f6524a856b2873e5d9852a65ae0c24c9a87f3 100644 (file)
--- 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];
 }
@@ -93,6 +93,38 @@ inline Node RewriteRule<BvIteConstChildren>::apply(TNode node)
   return NodeManager::currentNM()->mkNode(kind::BITVECTOR_NOT, node[0]);
 }
 
+/**
+ * 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
  *

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index f0218bbc5cdecf852de6040cfd72c3382617a0af..d63fe4009b25c0f21885c363caa232469d8e4b22 100644 (file)
--- 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);
 }