Add rewrite for BITVECTOR_ITE with const children. (#2271)

diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 0ce9e6d5aa158a41fbfe86ecf4814448adc02180..55614f4e6ad0b3167fb9bb29ceee7a540b88894f 100644 (file)
--- 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 6f94804892c9f1a78be2387dfad9e299acd01abf..1213c0f05d12ff0e98778a81e388cdc58f70bfce 100644 (file)
--- 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 06ff8e77f273092a646337ba81cca265f9478bb2..f0218bbc5cdecf852de6040cfd72c3382617a0af 100644 (file)
--- 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 e42882a122419d3ed60130d61449e38ab841800d..470f9ac7f6fcbdc47eef0d629c853b772cd5580d 100644 (file)
--- 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 e4bf904628eb363fe39318abfcb1ac2f5f8c05f7..9fccf92a70cd0bd653ba16154911e91899639e24 100644 (file)
--- 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.  */