From dafa75521c0b38d0095792f232fbb53f16318676 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Fri, 3 Aug 2018 18:09:07 -0700
Subject: [PATCH] Add rewrite for BITVECTOR_ITE with const children. (#2271)

---
 src/theory/bv/theory_bv_rewrite_rules.h       |  3 +++
 .../theory_bv_rewrite_rules_simplification.h  | 26 +++++++++++++++++++
 src/theory/bv/theory_bv_rewriter.cpp          |  4 +--
 src/theory/bv/theory_bv_utils.cpp             |  6 +++++
 src/theory/bv/theory_bv_utils.h               |  3 +++
 5 files changed, 40 insertions(+), 2 deletions(-)

diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 0ce9e6d5a..55614f4e6 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -106,6 +106,7 @@ enum RewriteRuleId
   /// all of these rules decrease formula size
   BvIteConstCond,
   BvIteChildren,
+  BvIteConstChildren,
   BvComp,
   ShlByConst,
   LshrByConst,
@@ -245,6 +246,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case EvalNeg :            out << "EvalNeg";             return out;
   case BvIteConstCond :     out << "BvIteConstCond";      return out;
   case BvIteChildren :      out << "BvIteChildren";       return out;
+  case BvIteConstChildren : out << "BvIteConstChildren";  return out;
   case BvComp :             out << "BvComp";              return out;
   case ShlByConst :         out << "ShlByConst";          return out;
   case LshrByConst :        out << "LshrByConst";         return out;
@@ -561,6 +563,7 @@ struct AllRewriteRules {
   RewriteRule<BvComp>                         rule130;
   RewriteRule<BvIteConstCond>                 rule131;
   RewriteRule<BvIteChildren>                  rule132;
+  RewriteRule<BvIteConstChildren>             rule133;
 };
 
 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 6f9480489..1213c0f05 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -67,6 +67,32 @@ inline Node RewriteRule<BvIteChildren>::apply(TNode node)
   return node[1];
 }
 
+/**
+ * BvIteConstChildren
+ *
+ * BITVECTOR_ITE with constant children of size one
+ */
+template <>
+inline bool RewriteRule<BvIteConstChildren>::applies(TNode node)
+{
+  return (node.getKind() == kind::BITVECTOR_ITE
+          && utils::getSize(node[1]) == 1
+          && node[1].isConst() && node[2].isConst());
+}
+
+template <>
+inline Node RewriteRule<BvIteConstChildren>::apply(TNode node)
+{
+  Debug("bv-rewrite") << "RewriteRule<BvIteConstChildren>(" << node << ")"
+                      << std::endl;
+  if (utils::isOne(node[1]) && utils::isZero(node[2]))
+  {
+    return node[0];
+  }
+  Assert(utils::isZero(node[1]) && utils::isOne(node[2]));
+  return NodeManager::currentNM()->mkNode(kind::BITVECTOR_NOT, node[0]);
+}
+
 /**
  * BvComp
  *
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 06ff8e77f..f0218bbc5 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -171,8 +171,8 @@ RewriteResponse TheoryBVRewriter::RewriteITEBv(TNode node, bool prerewrite)
   Node resultNode =
       LinearRewriteStrategy<RewriteRule<EvalITEBv>,
                             RewriteRule<BvIteConstCond>,
-                            RewriteRule<BvIteChildren> >::apply(node);
-
+                            RewriteRule<BvIteChildren>,
+                            RewriteRule<BvIteConstChildren> >::apply(node);
   return RewriteResponse(REWRITE_DONE, resultNode);
 }
 
diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index e42882a12..470f9ac7f 100644
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -63,6 +63,12 @@ bool isZero(TNode node)
   return node == mkZero(getSize(node));
 }
 
+bool isOne(TNode node)
+{
+  if (!node.isConst()) return false;
+  return node == mkOne(getSize(node));
+}
+
 unsigned isPow2Const(TNode node, bool& isNeg)
 {
   if (node.getKind() != kind::CONST_BITVECTOR)
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index e4bf90462..9fccf92a7 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -55,6 +55,9 @@ unsigned getSignExtendAmount(TNode node);
 /* Returns true if given node represents a zero bit-vector.  */
 bool isZero(TNode node);
 
+/* Returns true if given node represents a one bit-vector.  */
+bool isOne(TNode node);
+
 /* If node is a constant of the form 2^c or -2^c, then this function returns
  * c+1. Otherwise, this function returns 0. The flag isNeg is updated to
  * indicate whether node is negative.  */
-- 
2.30.2