From 1e1efe98961c87e96767ee362378b5573b49c2ff Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 7 Aug 2018 11:22:05 -0700
Subject: [PATCH] Add rewrite for nested BITVECTOR_ITE that can be merged.
 (#2273)

---
 src/theory/bv/theory_bv_rewrite_rules.h       |  12 ++
 .../theory_bv_rewrite_rules_simplification.h  | 107 ++++++++++++++++++
 src/theory/bv/theory_bv_rewriter.cpp          |   6 +-
 3 files changed, 124 insertions(+), 1 deletion(-)

diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index d8f360492..97284a01b 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -108,6 +108,10 @@ enum RewriteRuleId
   BvIteEqualChildren,
   BvIteConstChildren,
   BvIteEqualCond,
+  BvIteMergeThenIf,
+  BvIteMergeElseIf,
+  BvIteMergeThenElse,
+  BvIteMergeElseElse,
   BvComp,
   ShlByConst,
   LshrByConst,
@@ -249,6 +253,10 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case BvIteEqualChildren : out << "BvIteEqualChildren";  return out;
   case BvIteConstChildren : out << "BvIteConstChildren";  return out;
   case BvIteEqualCond :     out << "BvIteEqualCond";      return out;
+  case BvIteMergeThenIf :   out << "BvIteMergeThenIf";    return out;
+  case BvIteMergeElseIf :   out << "BvIteMergeElseIf";    return out;
+  case BvIteMergeThenElse : out << "BvIteMergeThenElse";  return out;
+  case BvIteMergeElseElse : out << "BvIteMergeElseElse";  return out;
   case BvComp :             out << "BvComp";              return out;
   case ShlByConst :         out << "ShlByConst";          return out;
   case LshrByConst :        out << "LshrByConst";         return out;
@@ -567,6 +575,10 @@ struct AllRewriteRules {
   RewriteRule<BvIteEqualChildren>             rule132;
   RewriteRule<BvIteConstChildren>             rule133;
   RewriteRule<BvIteEqualCond>                 rule134;
+  RewriteRule<BvIteMergeThenIf>               rule135;
+  RewriteRule<BvIteMergeElseIf>               rule136;
+  RewriteRule<BvIteMergeThenElse>             rule137;
+  RewriteRule<BvIteMergeElseElse>             rule138;
 };
 
 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 a59f6524a..9df3a0cd5 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -125,6 +125,113 @@ inline Node RewriteRule<BvIteEqualCond>::apply(TNode node)
                 : node[2];
   return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ITE, node[0], t0, e1);
 }
+
+/**
+ * BvIteMergeThenIf
+ *
+ * Nested BITVECTOR_ITE of the form
+ *   c0 ? (c1 ? t1 : e1) : t1  ->  c0 AND NOT(c1) ? e1 : t1
+ */
+template <>
+inline bool RewriteRule<BvIteMergeThenIf>::applies(TNode node)
+{
+  return (node.getKind() == kind::BITVECTOR_ITE
+          && node[1].getKind() == kind::BITVECTOR_ITE
+          && node[1][1] == node[2]);
+}
+
+template <>
+inline Node RewriteRule<BvIteMergeThenIf>::apply(TNode node)
+{
+  Debug("bv-rewrite") << "RewriteRule<BvIteMergeThenIf>(" << node << ")"
+                      << std::endl;
+  NodeManager* nm = NodeManager::currentNM();
+  Assert(node[1].getKind() == kind::BITVECTOR_ITE);
+  Node cond = nm->mkNode(kind::BITVECTOR_AND,
+                         node[0],
+                         nm->mkNode(kind::BITVECTOR_NOT, node[1][0]));
+  return nm->mkNode(kind::BITVECTOR_ITE, cond, node[1][2], node[2]);
+}
+
+/**
+ * BvIteMergeElseIf
+ *
+ * Nested BITVECTOR_ITE of the form
+ *   c0 ? (c1 ? t1 : e1) : e1  ->  c0 AND c1 ? t1 : e1
+ */
+template <>
+inline bool RewriteRule<BvIteMergeElseIf>::applies(TNode node)
+{
+  return (node.getKind() == kind::BITVECTOR_ITE
+          && node[1].getKind() == kind::BITVECTOR_ITE
+          && node[1][2] == node[2]);
+}
+
+template <>
+inline Node RewriteRule<BvIteMergeElseIf>::apply(TNode node)
+{
+  Debug("bv-rewrite") << "RewriteRule<BvIteMergeElseIf>(" << node << ")"
+                      << std::endl;
+  NodeManager* nm = NodeManager::currentNM();
+  Assert(node[1].getKind() == kind::BITVECTOR_ITE);
+  Node cond = nm->mkNode(kind::BITVECTOR_AND, node[0], node[1][0]);
+  return nm->mkNode(kind::BITVECTOR_ITE, cond, node[1][1], node[2]);
+}
+
+/**
+ * BvIteMergeThenElse
+ *
+ * Nested BITVECTOR_ITE of the form
+ *   c0 ? t0 : (c1 ? t0 : e1)  ->  NOT(c0) AND NOT(c1) ? e1 : t0
+ */
+template <>
+inline bool RewriteRule<BvIteMergeThenElse>::applies(TNode node)
+{
+  return (node.getKind() == kind::BITVECTOR_ITE
+          && node[2].getKind() == kind::BITVECTOR_ITE
+          && node[1] == node[2][1]);
+}
+
+template <>
+inline Node RewriteRule<BvIteMergeThenElse>::apply(TNode node)
+{
+  Debug("bv-rewrite") << "RewriteRule<BvIteMergeThenElse>(" << node << ")"
+                      << std::endl;
+  NodeManager* nm = NodeManager::currentNM();
+  Assert(node[2].getKind() == kind::BITVECTOR_ITE);
+  Node cond = nm->mkNode(kind::BITVECTOR_AND,
+                         nm->mkNode(kind::BITVECTOR_NOT, node[0]),
+                         nm->mkNode(kind::BITVECTOR_NOT, node[2][0]));
+  return nm->mkNode(kind::BITVECTOR_ITE, cond, node[2][2], node[1]);
+}
+
+/**
+ * BvIteMergeElseElse
+ *
+ * Nested BITVECTOR_ITE of the form
+ *   c0 ? t0 : (c1 ? t1 : t0)  ->  NOT(c0) AND c1 ? t1 : t0
+ */
+template <>
+inline bool RewriteRule<BvIteMergeElseElse>::applies(TNode node)
+{
+  return (node.getKind() == kind::BITVECTOR_ITE
+          && node[2].getKind() == kind::BITVECTOR_ITE
+          && node[1] == node[2][2]);
+}
+
+template <>
+inline Node RewriteRule<BvIteMergeElseElse>::apply(TNode node)
+{
+  Debug("bv-rewrite") << "RewriteRule<BvIteMergeElseElse>(" << node << ")"
+                      << std::endl;
+  NodeManager* nm = NodeManager::currentNM();
+  Assert(node[2].getKind() == kind::BITVECTOR_ITE);
+  Node cond = nm->mkNode(kind::BITVECTOR_AND,
+                         nm->mkNode(kind::BITVECTOR_NOT, node[0]),
+                         node[2][0]);
+  return nm->mkNode(kind::BITVECTOR_ITE, cond, node[2][1], node[1]);
+}
+
 /**
  * BvComp
  *
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index d63fe4009..8b5d34cf4 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -173,7 +173,11 @@ RewriteResponse TheoryBVRewriter::RewriteITEBv(TNode node, bool prerewrite)
                             RewriteRule<BvIteConstCond>,
                             RewriteRule<BvIteEqualChildren>,
                             RewriteRule<BvIteConstChildren>,
-                            RewriteRule<BvIteEqualCond>>::apply(node);
+                            RewriteRule<BvIteEqualCond>,
+                            RewriteRule<BvIteMergeThenIf>,
+                            RewriteRule<BvIteMergeElseIf>,
+                            RewriteRule<BvIteMergeThenElse>,
+                            RewriteRule<BvIteMergeElseElse>>::apply(node);
   return RewriteResponse(REWRITE_DONE, resultNode);
 }
 
-- 
2.30.2