Refactor bv-intro-pow2 preprocessing pass. (#1851)

6 files changed, 159 insertions, 141 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 168e1e3b8..0eefbc1de 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -64,6 +64,8 @@ libcvc4_la_SOURCES = \
 	decision/justification_heuristic.h \
 	preprocessing/passes/bv_gauss.cpp \
 	preprocessing/passes/bv_gauss.h \
+	preprocessing/passes/bv_intro_pow2.cpp \
+	preprocessing/passes/bv_intro_pow2.h \
 	preprocessing/passes/int_to_bv.cpp \
 	preprocessing/passes/int_to_bv.h \
 	preprocessing/passes/pseudo_boolean_processor.cpp \
@@ -326,8 +328,6 @@ libcvc4_la_SOURCES = \
 	theory/bv/bv_subtheory_core.h \
 	theory/bv/bv_subtheory_inequality.cpp \
 	theory/bv/bv_subtheory_inequality.h \
-	theory/bv/bvintropow2.cpp \
-	theory/bv/bvintropow2.h \
 	theory/bv/slicer.cpp \
 	theory/bv/slicer.h \
 	theory/bv/theory_bv.cpp \
diff --git a/src/preprocessing/passes/bv_intro_pow2.cpp b/src/preprocessing/passes/bv_intro_pow2.cpp
new file mode 100644
index 000000000..17336b86c
--- /dev/null
+++ b/src/preprocessing/passes/bv_intro_pow2.cpp
@@ -0,0 +1,104 @@
+/*********************                                                        */
+/*! \file bv_intro_pow2.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Mathias Preiner, Liana Hadarean, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The BvIntroPow2 preprocessing pass
+ **
+ ** Traverses the formula and applies the IsPowerOfTwo rewrite rule. This
+ ** preprocessing pass is particularly useful on QF_BV/pspace benchmarks and
+ ** can be enabled via option `--bv-intro-pow2`.
+ **/
+
+#include "preprocessing/passes/bv_intro_pow2.h"
+
+#include <unordered_map>
+
+#include "theory/bv/theory_bv_rewrite_rules_simplification.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>;
+using namespace CVC4::theory;
+
+namespace {
+
+Node 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, size = node.getNumChildren(); i < size; ++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()
+          && theory::bv::RewriteRule<theory::bv::IsPowerOfTwo>::applies(node))
+      {
+        res = theory::bv::RewriteRule<theory::bv::IsPowerOfTwo>::run<false>(node);
+      }
+      break;
+    default: break;
+  }
+
+  cache.insert(std::make_pair(node, res));
+  return res.isNull() ? node : res;
+}
+
+}  // namespace
+
+BvIntroPow2::BvIntroPow2(PreprocessingPassContext* preprocContext)
+    : PreprocessingPass(preprocContext, "bv-intro-pow2"){};
+
+PreprocessingPassResult BvIntroPow2::applyInternal(
+    AssertionPipeline* assertionsToPreprocess)
+{
+  std::unordered_map<Node, Node, NodeHashFunction> cache;
+  for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
+  {
+    Node cur = (*assertionsToPreprocess)[i];
+    Node res = pow2Rewrite(cur, cache);
+    if (res != cur)
+    {
+      res = Rewriter::rewrite(res);
+      assertionsToPreprocess->replace(i, res);
+    }
+  }
+  return PreprocessingPassResult::NO_CONFLICT;
+}
+
+}/* CVC4::theory::bv namespace */
+}/* CVC4::theory namespace */
+
+}/* CVC4 namespace */
diff --git a/src/preprocessing/passes/bv_intro_pow2.h b/src/preprocessing/passes/bv_intro_pow2.h
new file mode 100644
index 000000000..a5fe8e7bb
--- /dev/null
+++ b/src/preprocessing/passes/bv_intro_pow2.h
@@ -0,0 +1,45 @@
+/*********************                                                        */
+/*! \file bv_intro_pow2.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Mathias Preiner
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The BvIntroPow2 preprocessing pass
+ **
+ ** Traverses the formula and applies the IsPowerOfTwo rewrite rule. This
+ ** preprocessing pass is particularly useful on QF_BV/pspace benchmarks and
+ ** can be enabled via option `--bv-intro-pow2`.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H
+#define __CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H
+
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+class BvIntroPow2 : public PreprocessingPass
+{
+ public:
+  BvIntroPow2(PreprocessingPassContext* preprocContext);
+
+ protected:
+  PreprocessingPassResult applyInternal(
+      AssertionPipeline* assertionsToPreprocess) override;
+};
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c1e8596cf..10d21a66c 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -70,6 +70,7 @@
 #include "options/uf_options.h"
 #include "preprocessing/passes/bool_to_bv.h"
 #include "preprocessing/passes/bv_gauss.h"
+#include "preprocessing/passes/bv_intro_pow2.h"
 #include "preprocessing/passes/bv_to_bool.h"
 #include "preprocessing/passes/int_to_bv.h"
 #include "preprocessing/passes/pseudo_boolean_processor.h"
@@ -95,7 +96,6 @@
 #include "smt_util/nary_builder.h"
 #include "smt_util/node_visitor.h"
 #include "theory/booleans/circuit_propagator.h"
-#include "theory/bv/bvintropow2.h"
 #include "theory/bv/theory_bv_rewriter.h"
 #include "theory/logic_info.h"
 #include "theory/quantifiers/fun_def_process.h"
@@ -2603,6 +2603,10 @@ void SmtEnginePrivate::finishInit() {
   std::unique_ptr<BoolToBV> boolToBv(
       new BoolToBV(d_preprocessingPassContext.get()));
   d_preprocessingPassRegistry.registerPass("bool-to-bv", std::move(boolToBv));
+  std::unique_ptr<BvIntroPow2> bvIntroPow2(
+      new BvIntroPow2(d_preprocessingPassContext.get()));
+  d_preprocessingPassRegistry.registerPass("bv-intro-pow2",
+                                           std::move(bvIntroPow2));
 }
 
 Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
@@ -4070,8 +4074,9 @@ void SmtEnginePrivate::processAssertions() {
     dumpAssertions("post-unconstrained-simp", d_assertions);
   }
 
-  if(options::bvIntroducePow2()){
-    theory::bv::BVIntroducePow2::pow2Rewrite(d_assertions.ref());
+  if(options::bvIntroducePow2())
+  {
+    d_preprocessingPassRegistry.getPass("bv-intro-pow2")->apply(&d_assertions);
   }
 
   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-substitution" << endl;
diff --git a/src/theory/bv/bvintropow2.cpp b/src/theory/bv/bvintropow2.cpp
deleted file mode 100644
index e7b6caaef..000000000
--- a/src/theory/bv/bvintropow2.cpp
+++ /dev/null
@@ -1,85 +0,0 @@
-/*********************                                                        */
-/*! \file bvintropow2.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Liana Hadarean, Morgan Deters, Paul Meng
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#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);
-    if(next != curr){
-      Node tmp = Rewriter::rewrite(next);
-      next = tmp;
-    }
-    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
deleted file mode 100644
index e335c1339..000000000
--- a/src/theory/bv/bvintropow2.h
+++ /dev/null
@@ -1,51 +0,0 @@
-/*********************                                                        */
-/*! \file bvintropow2.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Liana Hadarean, Morgan Deters, Paul Meng
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-
-
-#include "cvc4_private.h"
-#include "expr/node.h"
-
-#include <vector>
-#include <unordered_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 std::unordered_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 */