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

2 files changed, 149 insertions, 0 deletions

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 */