Refactor IntToBV preprocessing pass (#1716)

This commit refactors the IntToBV preprocessing pass into the new style.
This commit is essentially just a code move, it does not attempt to fix
issues (e.g. #1715).

1 files changed, 10 insertions, 244 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2f6832089..abefaf215 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -18,12 +18,13 @@
 
 #include <algorithm>
 #include <cctype>
-#include <unordered_map>
-#include <unordered_set>
 #include <iterator>
+#include <memory>
 #include <sstream>
 #include <stack>
 #include <string>
+#include <unordered_map>
+#include <unordered_set>
 #include <utility>
 #include <vector>
 
@@ -67,6 +68,7 @@
 #include "options/strings_options.h"
 #include "options/theory_options.h"
 #include "options/uf_options.h"
+#include "preprocessing/passes/int_to_bv.h"
 #include "preprocessing/preprocessing_pass.h"
 #include "preprocessing/preprocessing_pass_context.h"
 #include "preprocessing/preprocessing_pass_registry.h"
@@ -116,6 +118,7 @@ using namespace std;
 using namespace CVC4;
 using namespace CVC4::smt;
 using namespace CVC4::preprocessing;
+using namespace CVC4::preprocessing::passes;
 using namespace CVC4::prop;
 using namespace CVC4::context;
 using namespace CVC4::theory;
@@ -2542,7 +2545,10 @@ bool SmtEngine::isDefinedFunction( Expr func ){
 
 void SmtEnginePrivate::finishInit() {
   d_preprocessingPassContext.reset(new PreprocessingPassContext(&d_smt));
-  //TODO: register passes here
+  // TODO: register passes here (this will likely change when we add support for
+  // actually assembling preprocessing pipelines).
+  std::unique_ptr<IntToBV> intToBV(new IntToBV(d_preprocessingPassContext.get()));
+  d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV));
 }
 
 Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
@@ -2703,244 +2709,8 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, Node
   return result.top();
 }
 
-//TODO: clean this up
-struct intToBV_stack_element {
-  TNode node;
-  bool children_added;
-  intToBV_stack_element(TNode node)
-  : node(node), children_added(false) {}
-};/* struct intToBV_stack_element */
-
 typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
 
-Node SmtEnginePrivate::intToBVMakeBinary(TNode n, NodeMap& cache) {
-  // Do a topological sort of the subexpressions and substitute them
-  vector<intToBV_stack_element> toVisit;
-  toVisit.push_back(n);
-
-  while (!toVisit.empty())
-  {
-    // The current node we are processing
-    intToBV_stack_element& stackHead = toVisit.back();
-    TNode current = stackHead.node;
-
-    NodeMap::iterator find = cache.find(current);
-    if (find != cache.end()) {
-      toVisit.pop_back();
-      continue;
-    }
-    if (stackHead.children_added) {
-      // Children have been processed, so rebuild this node
-      Node result;
-      NodeManager* nm = NodeManager::currentNM();
-      if (current.getNumChildren() > 2 && (current.getKind() == kind::PLUS || current.getKind() == kind::MULT)) {
-        Assert(cache.find(current[0]) != cache.end());
-        result = cache[current[0]];
-        for (unsigned i = 1; i < current.getNumChildren(); ++ i) {
-          Assert(cache.find(current[i]) != cache.end());
-          Node child = current[i];
-          Node childRes = cache[current[i]];
-          result = nm->mkNode(current.getKind(), result, childRes);
-        }
-      }
-      else {
-        NodeBuilder<> builder(current.getKind());
-        for (unsigned i = 0; i < current.getNumChildren(); ++ i) {
-          Assert(cache.find(current[i]) != cache.end());
-          builder << cache[current[i]];
-        }
-        result = builder;
-      }
-      cache[current] = result;
-      toVisit.pop_back();
-    } else {
-      // Mark that we have added the children if any
-      if (current.getNumChildren() > 0) {
-        stackHead.children_added = true;
-        // We need to add the children
-        for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
-          TNode childNode = *child_it;
-          NodeMap::iterator childFind = cache.find(childNode);
-          if (childFind == cache.end()) {
-            toVisit.push_back(childNode);
-          }
-        }
-      } else {
-        cache[current] = current;
-        toVisit.pop_back();
-      }
-    }
-  }
-  return cache[n];
-}
-
-Node SmtEnginePrivate::intToBV(TNode n, NodeMap& cache) {
-  int size = options::solveIntAsBV();
-  AlwaysAssert(size > 0);
-  AlwaysAssert(!options::incrementalSolving());
-
-  vector<intToBV_stack_element> toVisit;
-  NodeMap binaryCache;
-  Node n_binary = intToBVMakeBinary(n, binaryCache);
-  toVisit.push_back(TNode(n_binary));
-
-  while (!toVisit.empty())
-  {
-    // The current node we are processing
-    intToBV_stack_element& stackHead = toVisit.back();
-    TNode current = stackHead.node;
-
-    // If node is already in the cache we're done, pop from the stack
-    NodeMap::iterator find = cache.find(current);
-    if (find != cache.end()) {
-      toVisit.pop_back();
-      continue;
-    }
-
-    // Not yet substituted, so process
-    NodeManager* nm = NodeManager::currentNM();
-    if (stackHead.children_added) {
-      // Children have been processed, so rebuild this node
-      vector<Node> children;
-      unsigned max = 0;
-      for (unsigned i = 0; i < current.getNumChildren(); ++ i) {
-        Assert(cache.find(current[i]) != cache.end());
-        TNode childRes = cache[current[i]];
-        TypeNode type = childRes.getType();
-        if (type.isBitVector()) {
-          unsigned bvsize = type.getBitVectorSize();
-          if (bvsize > max) {
-            max = bvsize;
-          }
-        }
-        children.push_back(childRes);
-      }
-
-      kind::Kind_t newKind = current.getKind();
-      if (max > 0) {
-        switch (newKind) {
-          case kind::PLUS:
-            Assert(children.size() == 2);
-            newKind = kind::BITVECTOR_PLUS;
-            max = max + 1;
-            break;
-          case kind::MULT:
-            Assert(children.size() == 2);
-            newKind = kind::BITVECTOR_MULT;
-            max = max * 2;
-            break;
-          case kind::MINUS:
-            Assert(children.size() == 2);
-            newKind = kind::BITVECTOR_SUB;
-            max = max + 1;
-            break;
-          case kind::UMINUS:
-            Assert(children.size() == 1);
-            newKind = kind::BITVECTOR_NEG;
-            max = max + 1;
-            break;
-          case kind::LT:
-            newKind = kind::BITVECTOR_SLT;
-            break;
-          case kind::LEQ:
-            newKind = kind::BITVECTOR_SLE;
-            break;
-          case kind::GT:
-            newKind = kind::BITVECTOR_SGT;
-            break;
-          case kind::GEQ:
-            newKind = kind::BITVECTOR_SGE;
-            break;
-          case kind::EQUAL:
-          case kind::ITE:
-            break;
-          default:
-            if (Theory::theoryOf(current) == THEORY_BOOL) {
-              break;
-            }
-            throw TypeCheckingException(current.toExpr(), string("Cannot translate to BV: ") + current.toString());
-        }
-        for (unsigned i = 0; i < children.size(); ++i) {
-          TypeNode type = children[i].getType();
-          if (!type.isBitVector()) {
-            continue;
-          }
-          unsigned bvsize = type.getBitVectorSize();
-          if (bvsize < max) {
-            // sign extend
-            Node signExtendOp = nm->mkConst<BitVectorSignExtend>(BitVectorSignExtend(max - bvsize));
-            children[i] = nm->mkNode(signExtendOp, children[i]);
-          }
-        }
-      }
-      NodeBuilder<> builder(newKind);
-      for (unsigned i = 0; i < children.size(); ++i) {
-        builder << children[i];
-      }
-      // Mark the substitution and continue
-      Node result = builder;
-
-      result = Rewriter::rewrite(result);
-      cache[current] = result;
-      toVisit.pop_back();
-    } else {
-      // Mark that we have added the children if any
-      if (current.getNumChildren() > 0) {
-        stackHead.children_added = true;
-        // We need to add the children
-        for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
-          TNode childNode = *child_it;
-          NodeMap::iterator childFind = cache.find(childNode);
-          if (childFind == cache.end()) {
-            toVisit.push_back(childNode);
-          }
-        }
-      } else {
-        // It's a leaf: could be a variable or a numeral
-        Node result = current;
-        if (current.isVar()) {
-          if (current.getType() == nm->integerType()) {
-            result = nm->mkSkolem("__intToBV_var", nm->mkBitVectorType(size),
-                                  "Variable introduced in intToBV pass");
-          }
-          else {
-            AlwaysAssert(current.getType() == nm->booleanType());
-          }
-        }
-        else if (current.isConst()) {
-          switch (current.getKind()) {
-            case kind::CONST_RATIONAL: {
-              Rational constant = current.getConst<Rational>();
-              AlwaysAssert(constant.isIntegral());
-              AlwaysAssert(constant >= 0);
-              BitVector bv(size, constant.getNumerator());
-              if (bv.toSignedInteger() != constant.getNumerator())
-              {
-                throw TypeCheckingException(
-                    current.toExpr(),
-                    string("Not enough bits for constant in intToBV: ")
-                        + current.toString());
-              }
-              result = nm->mkConst(bv);
-              break;
-            }
-            case kind::CONST_BOOLEAN:
-              break;
-            default:
-              throw TypeCheckingException(current.toExpr(), string("Cannot translate const to BV: ") + current.toString());
-          }
-        }
-        else {
-          throw TypeCheckingException(current.toExpr(), string("Cannot translate to BV: ") + current.toString());
-        }
-        cache[current] = result;
-        toVisit.pop_back();
-      }
-    }
-  }
-  return cache[n_binary];
-}
-
 Node SmtEnginePrivate::realToInt(TNode n, NodeMap& cache, std::vector< Node >& var_eq) {
   Trace("real-as-int-debug") << "Convert : " << n << std::endl;
   NodeMap::iterator find = cache.find(n);
@@ -4317,11 +4087,7 @@ void SmtEnginePrivate::processAssertions() {
   }
 
   if (options::solveIntAsBV() > 0) {
-    Chat() << "converting ints to bit-vectors..." << endl;
-    unordered_map<Node, Node, NodeHashFunction> cache;
-    for(unsigned i = 0; i < d_assertions.size(); ++ i) {
-      d_assertions.replace(i, intToBV(d_assertions[i], cache));
-    }
+    d_preprocessingPassRegistry.getPass("int-to-bv")->apply(&d_assertions);
   }
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER &&