bv static learning and rewrites for power of 2 terms

5 files changed, 86 insertions, 66 deletions

diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index d606ccee8..ebe017ee1 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -96,6 +96,7 @@ void BitblastSolver::bitblastQueue() {
   while (!d_bitblastQueue.empty()) {
     TNode atom = d_bitblastQueue.front();
     d_bitblastQueue.pop();
+    Debug("bv-bitblast-queue") << "BitblastSolver::bitblastQueue (" << atom << ")\n";
     if (options::bvAbstraction() &&
         d_abstractionModule->isLemmaAtom(atom)) {
       // don't bit-blast lemma atoms
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 04b8e9d6e..5be02322d 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -560,9 +560,7 @@ Node TheoryBV::ppRewrite(TNode t)
   } else if (RewriteRule<UltPlusOne>::applies(t)) {
     Node result = RewriteRule<UltPlusOne>::run<false>(t);
     res = Rewriter::rewrite(result);
-  }
-
-  if( res.getKind() == kind::EQUAL &&
+  } else if( res.getKind() == kind::EQUAL &&
       ((res[0].getKind() == kind::BITVECTOR_PLUS &&
         RewriteRule<ConcatToMult>::applies(res[1])) ||
        res[1].getKind() == kind::BITVECTOR_PLUS &&
@@ -579,6 +577,8 @@ Node TheoryBV::ppRewrite(TNode t)
     } else {
       res = t;
     }
+  } else if (RewriteRule<IsPowerOfTwo>::applies(t)) {
+    res = RewriteRule<IsPowerOfTwo>::run<false>(t);
   }
   
 
@@ -729,7 +729,35 @@ void TheoryBV::enableCoreTheorySlicer() {
 }
 
 
-void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) {}
+void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
+  if (in.getKind() == kind::EQUAL) {
+    if(in[0].getKind() == kind::BITVECTOR_PLUS && in[1].getKind() == kind::BITVECTOR_SHL ||
+       in[1].getKind() == kind::BITVECTOR_PLUS && in[0].getKind() == kind::BITVECTOR_SHL){
+      TNode p = in[0].getKind() == kind::BITVECTOR_PLUS ? in[0] : in[1];
+      TNode s = in[0].getKind() == kind::BITVECTOR_PLUS ? in[1] : in[0];
+
+      if(p.getNumChildren() == 2
+         && p[0].getKind()  == kind::BITVECTOR_SHL 
+         && p[1].getKind()  == kind::BITVECTOR_SHL ){
+        unsigned size = utils::getSize(s);
+        Node one = utils::mkConst(size, 1u);
+        if(s[0] == one && p[0][0] == one && p[1][0] == one){
+          Node zero = utils::mkConst(size, 0u);
+          TNode b = p[0];
+          TNode c = p[1];
+          // (s : 1 << S) = (b : 1 << B) + (c : 1 << C)
+          Node b_eq_0 = b.eqNode(zero);
+          Node c_eq_0 = c.eqNode(zero);
+          Node b_eq_c = b.eqNode(c);
+
+          Node dis = utils::mkNode(kind::OR, b_eq_0, c_eq_0, b_eq_c);
+          Node imp = in.impNode(dis);
+          learned << imp;
+        }
+      }
+    }
+  }       
+}
 
 bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
   bool changed = d_abstractionModule->applyAbstraction(assertions, new_assertions);
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index eadb63671..5e85cb145 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -165,7 +165,8 @@ enum RewriteRuleId {
   // rules to simplify bitblasting
   BBPlusNeg,
   UltPlusOne,
-  ConcatToMult
+  ConcatToMult,
+  IsPowerOfTwo
 };
 
 
@@ -293,6 +294,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case MultDistrib: out << "MultDistrib"; return out;
   case UltPlusOne: out << "UltPlusOne"; return out;
   case ConcatToMult: out << "ConcatToMult"; return out;
+  case IsPowerOfTwo: out << "IsPowerOfTwo"; return out;
   default:
     Unreachable();
   }
@@ -516,6 +518,7 @@ struct AllRewriteRules {
   RewriteRule<MultDistrib> rule118;
   RewriteRule<UltPlusOne> rule119;
   RewriteRule<ConcatToMult> rule120;
+  RewriteRule<IsPowerOfTwo> rule121;
 };
 
 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 71df1edca..33994782a 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -1193,67 +1193,52 @@ Node RewriteRule<UltPlusOne>::apply(TNode node) {
   return utils::mkNode(kind::AND, not_y_eq_1, not_y_lt_x);
 }
 
+/** 
+ * x ^(x-1) = 0 => 1 << sk
+ * Note: only to be called in ppRewrite and not rewrite!
+ * (it calls the rewriter)
+ * 
+ * @param node 
+ * 
+ * @return 
+ */
+template<> inline
+bool RewriteRule<IsPowerOfTwo>::applies(TNode node) {
+  if (node.getKind()!= kind::EQUAL) return false;
+  if (node[0].getKind() != kind::BITVECTOR_AND &&
+      node[1].getKind() != kind::BITVECTOR_AND)
+    return false;
+  if (!utils::isZero(node[0]) &&
+      !utils::isZero(node[1]))
+    return false;
+
+  TNode t = !utils::isZero(node[0])? node[0]: node[1];
+  if (t.getNumChildren() != 2) return false; 
+  TNode a = t[0];
+  TNode b = t[1];
+  unsigned size = utils::getSize(t);
+  if(size < 2) return false;
+  Node diff = Rewriter::rewrite(utils::mkNode(kind::BITVECTOR_SUB, a, b));
+  return (diff.isConst() && (diff == utils::mkConst(size, 1u) || diff == utils::mkOnes(size)));
+}
+
+template<> inline
+Node RewriteRule<IsPowerOfTwo>::apply(TNode node) {
+  Debug("bv-rewrite") << "RewriteRule<IsPowerOfTwo>(" << node << ")" << std::endl;
+  TNode term = utils::isZero(node[0])? node[1] : node[0];
+  TNode a = term[0];
+  TNode b = term[1];
+  unsigned size = utils::getSize(term); 
+  Node diff = Rewriter::rewrite(utils::mkNode(kind::BITVECTOR_SUB, a, b));
+  Assert (diff.isConst());
+  TNode x = diff == utils::mkConst(size, 1u) ? a : b;
+  Node one = utils::mkConst(size, 1u);
+  Node sk = utils::mkVar(size);
+  Node sh = utils::mkNode(kind::BITVECTOR_SHL, one, sk);
+  Node x_eq_sh = utils::mkNode(kind::EQUAL, x, sh);
+  return x_eq_sh;
+}
 
-// /**
-//  * 
-//  *
-//  * 
-//  */
-
-// template<> inline
-// bool RewriteRule<BBFactorOut>::applies(TNode node) {
-//   if (node.getKind() != kind::BITVECTOR_PLUS) {
-//     return false; 
-//   }
-
-//   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
-//     if (node[i].getKind() != kind::BITVECTOR_MULT) {
-//       return false; 
-//     }
-//   }
-// }
-
-// template<> inline
-// Node RewriteRule<BBFactorOut>::apply(TNode node) {
-//   Debug("bv-rewrite") << "RewriteRule<BBFactorOut>(" << node << ")" << std::endl;
-//   std::hash_set<TNode, TNodeHashFunction> factors;
-
-//   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
-//     Assert (node[i].getKind() == kind::BITVECTOR_MULT);
-//     for (unsigned j = 0; j < node[i].getNumChildren(); ++j) {
-//       factors.insert(node[i][j]); 
-//     }
-//   }
-
-//   std::vector<TNode> gcd; 
-//   std::hash_set<TNode, TNodeHashFunction>::const_iterator it;
-//   for (it = factors.begin(); it != factors.end(); ++it) {
-//     // for each factor check if it occurs in all children
-//     TNode f = *it; 
-//     for (unsigned i = 0; i < node.getNumChildren
-    
-//     }
-//   }
-//   return ; 
-// }
-
-
-// /**
-//  * 
-//  *
-//  * 
-//  */
-
-// template<> inline
-// bool RewriteRule<>::applies(TNode node) {
-//   return (node.getKind() == );
-// }
-
-// template<> inline
-// Node RewriteRule<>::apply(TNode node) {
-//   Debug("bv-rewrite") << "RewriteRule<>(" << node << ")" << std::endl;
-//   return ; 
-// }
 
 
 
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 3650d3091..9679c0260 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -332,7 +332,10 @@ inline Node mkAnd(const std::vector<Node>& conjunctions) {
   return conjunction;
 }/* mkAnd() */
 
-
+inline bool isZero(TNode node) {
+  if (!node.isConst()) return false; 
+  return node == utils::mkConst(utils::getSize(node), 0u); 
+}
 
 inline Node flattenAnd(std::vector<TNode>& queue) {
   TNodeSet nodes;