From db53123fe114732b647f87e6dd6ee756ca43c291 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 2 Aug 2018 11:52:32 -0700
Subject: [PATCH] Add rewrites for BITVECTOR_ITE and BITVECTOR_COMP with const
 condition/child. (#2259)

---
 src/theory/bv/theory_bv_rewrite_rules.h       |  6 +++
 .../theory_bv_rewrite_rules_simplification.h  | 44 +++++++++++++++++++
 src/theory/bv/theory_bv_rewriter.cpp          | 22 +++++-----
 src/theory/bv/theory_bv_utils.cpp             |  4 +-
 4 files changed, 65 insertions(+), 11 deletions(-)

diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 25f9eccbb..1eb815ef9 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -104,6 +104,8 @@ enum RewriteRuleId
 
   /// simplification rules
   /// all of these rules decrease formula size
+  BvIte,
+  BvComp,
   ShlByConst,
   LshrByConst,
   AshrByConst,
@@ -240,6 +242,8 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case EvalRotateLeft :     out << "EvalRotateLeft";      return out;
   case EvalRotateRight :    out << "EvalRotateRight";     return out;
   case EvalNeg :            out << "EvalNeg";             return out;
+  case BvIte :              out << "BvIte";               return out;
+  case BvComp :             out << "BvComp";              return out;
   case ShlByConst :         out << "ShlByConst";          return out;
   case LshrByConst :        out << "LshrByConst";         return out;
   case AshrByConst :        out << "AshrByConst";         return out;
@@ -474,6 +478,7 @@ struct AllRewriteRules {
   RewriteRule<EvalRotateRight>      rule46;
   RewriteRule<EvalEquals>           rule47;
   RewriteRule<EvalNeg>              rule48;
+  RewriteRule<BvIte>                rule49;
   RewriteRule<ShlByConst>             rule50;
   RewriteRule<LshrByConst>             rule51;
   RewriteRule<AshrByConst>             rule52;
@@ -552,6 +557,7 @@ struct AllRewriteRules {
   RewriteRule<ZeroExtendUltConst> rule127;
   RewriteRule<MultSltMult> rule128;
   RewriteRule<NormalizeEqPlusNeg> rule129;
+  RewriteRule<BvComp> rule130;
 };
 
 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 397385996..9649fec77 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -29,6 +29,50 @@ namespace bv {
 
 // FIXME: this rules subsume the constant evaluation ones
 
+/**
+ * BvIte
+ *
+ * BITVECTOR_ITE with constant condition
+ */
+template <>
+inline bool RewriteRule<BvIte>::applies(TNode node)
+{
+  return (node.getKind() == kind::BITVECTOR_ITE && node[0].isConst());
+}
+
+template <>
+inline Node RewriteRule<BvIte>::apply(TNode node)
+{
+  Debug("bv-rewrite") << "RewriteRule<BvIte>(" << node << ")" << std::endl;
+  return utils::isZero(node[0]) ? node[2] : node[1];
+}
+
+/**
+ * BvComp
+ *
+ * BITVECTOR_COMP of children of size 1 with one constant child
+ */
+template <>
+inline bool RewriteRule<BvComp>::applies(TNode node)
+{
+  return (node.getKind() == kind::BITVECTOR_COMP
+          && utils::getSize(node[0]) == 1
+          && (node[0].isConst() || node[1].isConst()));
+}
+
+template <>
+inline Node RewriteRule<BvComp>::apply(TNode node)
+{
+  Debug("bv-rewrite") << "RewriteRule<BvComp>(" << node << ")" << std::endl;
+  NodeManager* nm = NodeManager::currentNM();
+  if (node[0].isConst())
+  {
+    return utils::isZero(node[0]) ? nm->mkNode(kind::BITVECTOR_NOT, node[1])
+                                  : Node(node[1]);
+  }
+  return utils::isZero(node[1]) ? nm->mkNode(kind::BITVECTOR_NOT, node[0])
+                                : Node(node[0]);
+}
 
 /**
  * ShlByConst
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index aca44aa37..6355da07d 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -166,12 +166,13 @@ RewriteResponse TheoryBVRewriter::RewriteSge(TNode node, bool prerewrite){
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteITEBv(TNode node, bool prerewrite){
-  Node resultNode = LinearRewriteStrategy
-    < RewriteRule < EvalITEBv >
-       >::apply(node);
+RewriteResponse TheoryBVRewriter::RewriteITEBv(TNode node, bool prerewrite)
+{
+  Node resultNode =
+      LinearRewriteStrategy<RewriteRule<EvalITEBv>, RewriteRule<BvIte> >::apply(
+          node);
 
-  return RewriteResponse(REWRITE_DONE, resultNode); 
+  return RewriteResponse(REWRITE_DONE, resultNode);
 }
 
 RewriteResponse TheoryBVRewriter::RewriteNot(TNode node, bool prerewrite){
@@ -329,12 +330,13 @@ RewriteResponse TheoryBVRewriter::RewriteNor(TNode node, bool prerewrite) {
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteComp(TNode node, bool prerewrite) {
-  Node resultNode = LinearRewriteStrategy
-    < RewriteRule < EvalComp >
-       >::apply(node);
+RewriteResponse TheoryBVRewriter::RewriteComp(TNode node, bool prerewrite)
+{
+  Node resultNode =
+      LinearRewriteStrategy<RewriteRule<EvalComp>, RewriteRule<BvComp> >::apply(
+          node);
 
-  return RewriteResponse(REWRITE_DONE, resultNode); 
+  return RewriteResponse(REWRITE_DONE, resultNode);
 }
 
 RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool prerewrite) {
diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index 7c5a68259..e42882a12 100644
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -89,7 +89,9 @@ unsigned isPow2Const(TNode node, bool& isNeg)
 
 bool isBvConstTerm(TNode node)
 {
-  if (node.getNumChildren() == 0) { return node.isConst();
+  if (node.getNumChildren() == 0)
+  {
+    return node.isConst();
   }
 
   for (const TNode& n : node)
-- 
2.30.2