Evil bitvector preprocessing pass for simplifying powers of two.

diff --git a/src/Makefile.am b/src/Makefile.am
index 810e3302a342aa9d69f3511dc2094dc9a1622768..b1a2032c0cca34819ff99fde7a8842c7af4dadbe 100644 (file)
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -217,6 +217,8 @@ libcvc4_la_SOURCES = \
        theory/bv/bitblast_mode.h \
        theory/bv/bitblast_mode.cpp \
        theory/bv/bitblast_utils.h \
+       theory/bv/bvintropow2.h \
+       theory/bv/bvintropow2.cpp \
        theory/idl/idl_model.h \
        theory/idl/idl_model.cpp \
        theory/idl/idl_assertion.h \

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 6b7bf424f819305974d4be7d3c286d1fba9c7458..ab805a6c589de393d4e8769b10fe31de3c88d8aa 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -89,6 +89,7 @@
 #include "printer/options.h"
 
 #include "theory/arith/pseudoboolean_proc.h"
+#include "theory/bv/bvintropow2.h"
 
 using namespace std;
 using namespace CVC4;
@@ -2926,6 +2927,10 @@ void SmtEnginePrivate::processAssertions() {
     dumpAssertions("post-unconstrained-simp", d_assertionsToPreprocess);
   }
 
+  if(options::bvIntroducePow2()){
+    theory::bv::BVIntroducePow2::pow2Rewrite(d_assertionsToPreprocess);
+  }
+
   dumpAssertions("pre-substitution", d_assertionsToPreprocess);
 
   // Apply the substitutions we already have, and normalize

diff --git a/src/theory/bv/bvintropow2.cpp b/src/theory/bv/bvintropow2.cpp
new file mode 100644 (file)
index 0000000..bd092ed
--- /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 (file)
index 0000000..3844d03
--- /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 fc704a71a7f849a8d9cca021239589e8945e360e..b5a4fea93c10e5b316dcad78966521801f6595b4 100644 (file)
--- 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 5be02322db262ec34a302e7f0eb848d0b8c15d8c..5ae07466ab2dd25f6df8ad1e10dc43e1f459e625 100644 (file)
--- 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 27b6b37c4a3060706fb5556d040f0de729e1e420..26ed8c296b82735c5ee12938ba2ee32513894d22 100644 (file)
--- 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.