Evil bitvector preprocessing pass for simplifying powers of two.

5 files changed, 114 insertions, 1 deletions

diff --git a/src/theory/bv/bvintropow2.cpp b/src/theory/bv/bvintropow2.cpp
new file mode 100644
index 000000000..bd092ed12
--- /dev/null
+++ b/src/theory/bv/bvintropow2.cpp
@@ -0,0 +1,64 @@
+#include "theory/bv/bvintropow2.h"
+#include "theory/rewriter.h"
+#include "theory/bv/theory_bv_rewrite_rules_simplification.h"
+
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+void BVIntroducePow2::pow2Rewrite(std::vector<Node>& assertionsToPreprocess){
+  NodeMap cache;
+  for(size_t i = 0, N= assertionsToPreprocess.size(); i < N; ++i){
+    Node curr = assertionsToPreprocess[i];
+    Node next = pow2Rewrite(curr, cache);
+    assertionsToPreprocess[i] = next;
+  }
+}
+
+Node  BVIntroducePow2::pow2Rewrite(Node node, NodeMap& cache){
+  NodeMap::const_iterator ci = cache.find(node);
+  if(ci != cache.end()){
+    Node incache = (*ci).second;
+    
+    return incache.isNull() ? node : incache;
+  }
+
+  Node res = Node::null();
+  switch(node.getKind()){
+  case kind::AND:
+    {
+      bool changed = false;
+      std::vector<Node> children;
+      for(unsigned i = 0, N = node.getNumChildren(); i < N; ++i){
+        Node child = node[i];
+        Node found = pow2Rewrite(child, cache);
+        changed = changed || (child != found);
+        children.push_back(found);
+      }
+      if(changed){
+        res = NodeManager::currentNM()->mkNode(kind::AND, children);
+      }
+    }
+    break;
+
+  case kind::EQUAL:
+    if(node[0].getType().isBitVector()){
+      if (RewriteRule<IsPowerOfTwo>::applies(node)) {
+        res = RewriteRule<IsPowerOfTwo>::run<false>(node);
+      }
+    }
+    break;
+  default:
+    break;
+  }
+
+  cache.insert(std::make_pair(node, res));
+  return res.isNull() ? node : res;
+}
+
+
+}/* CVC4::theory::bv namespace */
+}/* CVC4::theory namespace */
+
+}/* CVC4 namespace */
diff --git a/src/theory/bv/bvintropow2.h b/src/theory/bv/bvintropow2.h
new file mode 100644
index 000000000..3844d03e1
--- /dev/null
+++ b/src/theory/bv/bvintropow2.h
@@ -0,0 +1,34 @@
+
+
+#include "cvc4_private.h"
+#include "expr/node.h"
+
+#include <vector>
+#include <ext/hash_map>
+
+#ifndef __CVC4__THEORY__BV__BV_INTRO_POW_H
+#define __CVC4__THEORY__BV__BV_INTRO_POW_H
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+
+class BVIntroducePow2 {
+public:
+  static void pow2Rewrite(std::vector<Node>& assertionsToPreprocess);
+
+private:
+  typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeMap;
+  static Node pow2Rewrite(Node assertionsToPreprocess, NodeMap& cache);
+}; 
+
+
+
+}/* CVC4::theory::bv namespace */
+}/* CVC4::theory namespace */
+
+}/* CVC4 namespace */
+
+
+#endif /* __CVC4__THEORY__BV__BV_INTRO_POW_H */
diff --git a/src/theory/bv/options b/src/theory/bv/options
index fc704a71a..b5a4fea93 100644
--- a/src/theory/bv/options
+++ b/src/theory/bv/options
@@ -61,5 +61,7 @@ expert-option bvEagerExplanations --bv-eager-explanations bool :default false :r
 expert-option bitvectorQuickXplain --bv-quick-xplain bool :default false
  minimize bv conflicts using the QuickXplain algorithm
  
+expert-option bvIntroducePow2 --bv-intro-pow2 bool :default false
+ introduce bitvector powers of two as a preprocessing pass
  
 endmodule
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 5be02322d..5ae07466a 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -48,6 +48,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel&
     d_subtheories(),
     d_subtheoryMap(),
     d_statistics(),
+    d_staticLearnCache(),
     d_lemmasAdded(c, false),
     d_conflict(c, false),
     d_literalsToPropagate(c),
@@ -730,6 +731,11 @@ void TheoryBV::enableCoreTheorySlicer() {
 
 
 void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
+  if(d_staticLearnCache.find(in) != d_staticLearnCache.end()){
+    return;
+  }
+  d_staticLearnCache.insert(in);
+    
   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){
@@ -756,7 +762,11 @@ void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
         }
       }
     }
-  }       
+  }else if(in.getKind() == kind::AND){
+    for(size_t i = 0, N = in.getNumChildren(); i < N; ++i){
+      ppStaticLearn(in[i], learned);
+    }
+  }
 }
 
 bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 27b6b37c4..26ed8c296 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -117,6 +117,9 @@ private:
   typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; 
   void collectNumerators(TNode term, TNodeSet& seen);
   
+  typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+  NodeSet d_staticLearnCache;
+  
   /**
    * Maps from bit-vector width to divison-by-zero uninterpreted
    * function symbols.