modular bv2int: Stubs and some implementations (#6760)

This PR adds the file int_blaster.cpp. Most of the functions are not yet implemented. Two main functions are implemented.
Additionally, code that will no longer be needed is removed from the BV rewriter.

3 files changed, 252 insertions, 16 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index b3f27b703..74db7c941 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -596,6 +596,7 @@ libcvc5_add_sources(
   theory/bv/bv_subtheory_core.h
   theory/bv/bv_subtheory_inequality.cpp
   theory/bv/bv_subtheory_inequality.h
+  theory/bv/int_blaster.cpp
   theory/bv/int_blaster.h
   theory/bv/proof_checker.cpp
   theory/bv/proof_checker.h
diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp
new file mode 100644
index 000000000..9da9d1c2b
--- /dev/null
+++ b/src/theory/bv/int_blaster.cpp
@@ -0,0 +1,240 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Yoni Zohar
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Int-blasting utility
+ */
+
+#include "theory/bv/int_blaster.h"
+
+#include <cmath>
+#include <string>
+#include <unordered_map>
+#include <vector>
+
+#include "expr/node.h"
+#include "expr/node_traversal.h"
+#include "expr/skolem_manager.h"
+#include "options/option_exception.h"
+#include "options/uf_options.h"
+#include "theory/rewriter.h"
+#include "util/iand.h"
+#include "util/rational.h"
+
+namespace cvc5 {
+using namespace cvc5::theory;
+
+IntBlaster::IntBlaster(context::Context* c,
+                       options::SolveBVAsIntMode mode,
+                       uint64_t granularity,
+                       bool introduceFreshIntVars)
+    : d_binarizeCache(c),
+      d_intblastCache(c),
+      d_rangeAssertions(c),
+      d_bitwiseAssertions(c),
+      d_mode(mode),
+      d_granularity(granularity),
+      d_context(c),
+      d_introduceFreshIntVars(introduceFreshIntVars)
+{
+  d_nm = NodeManager::currentNM();
+  d_zero = d_nm->mkConst<Rational>(0);
+  d_one = d_nm->mkConst<Rational>(1);
+};
+
+void IntBlaster::addRangeConstraint(Node node,
+                                    uint64_t size,
+                                    std::vector<Node>& lemmas)
+{
+}
+
+void IntBlaster::addBitwiseConstraint(Node bitwiseConstraint,
+                                      std::vector<Node>& lemmas)
+{
+}
+
+Node IntBlaster::mkRangeConstraint(Node newVar, uint64_t k) { return Node(); }
+
+Node IntBlaster::maxInt(uint64_t k) { return Node(); }
+
+Node IntBlaster::pow2(uint64_t k) { return Node(); }
+
+Node IntBlaster::modpow2(Node n, uint64_t exponent) { return Node(); }
+
+Node IntBlaster::makeBinary(Node n)
+{
+  if (d_binarizeCache.find(n) != d_binarizeCache.end())
+  {
+    return d_binarizeCache[n];
+  }
+  uint64_t numChildren = n.getNumChildren();
+  kind::Kind_t k = n.getKind();
+  Node result = n;
+  if ((numChildren > 2)
+      && (k == kind::BITVECTOR_ADD || k == kind::BITVECTOR_MULT
+          || k == kind::BITVECTOR_AND || k == kind::BITVECTOR_OR
+          || k == kind::BITVECTOR_XOR || k == kind::BITVECTOR_CONCAT))
+  {
+    result = n[0];
+    for (uint64_t i = 1; i < numChildren; i++)
+    {
+      result = d_nm->mkNode(n.getKind(), result, n[i]);
+    }
+  }
+  d_binarizeCache[n] = result;
+  Trace("int-blaster-debug") << "binarization result: " << result << std::endl;
+  return result;
+}
+
+/**
+ * Translate n to Integers via post-order traversal.
+ */
+Node IntBlaster::intBlast(Node n,
+                          std::vector<Node>& lemmas,
+                          std::map<Node, Node>& skolems)
+{
+  // make sure the node is re-written
+  n = Rewriter::rewrite(n);
+
+  // helper vector for traversal.
+  std::vector<Node> toVisit;
+  toVisit.push_back(makeBinary(n));
+
+  while (!toVisit.empty())
+  {
+    Node current = toVisit.back();
+    uint64_t currentNumChildren = current.getNumChildren();
+    if (d_intblastCache.find(current) == d_intblastCache.end())
+    {
+      // This is the first time we visit this node and it is not in the cache.
+      // We mark this node as visited but not translated by assiging
+      // a null node to it.
+      d_intblastCache[current] = Node();
+      // all the node's children are added to the stack to be visited
+      // before visiting this node again.
+      for (const Node& child : current)
+      {
+        toVisit.push_back(makeBinary(child));
+      }
+      // If this is a UF applicatinon, we also add the function to
+      // toVisit.
+      if (current.getKind() == kind::APPLY_UF)
+      {
+        toVisit.push_back(current.getOperator());
+      }
+    }
+    else
+    {
+      // We already visited and translated this node
+      if (!d_intblastCache[current].get().isNull())
+      {
+        // We are done computing the translation for current
+        toVisit.pop_back();
+      }
+      else
+      {
+        // We are now visiting current on the way back up.
+        // This is when we do the actual translation.
+        Node translation;
+        if (currentNumChildren == 0)
+        {
+          translation = translateNoChildren(current, lemmas, skolems);
+        }
+        else
+        {
+          /**
+           * The current node has children.
+           * Since we are on the way back up,
+           * these children were already translated.
+           * We save their translation for easy access.
+           * If the node's kind is APPLY_UF,
+           * we also need to include the translated uninterpreted function in
+           * this list.
+           */
+          std::vector<Node> translated_children;
+          if (current.getKind() == kind::APPLY_UF)
+          {
+            translated_children.push_back(
+                d_intblastCache[current.getOperator()]);
+          }
+          for (uint64_t i = 0; i < currentNumChildren; i++)
+          {
+            translated_children.push_back(d_intblastCache[current[i]]);
+          }
+          translation =
+              translateWithChildren(current, translated_children, lemmas);
+        }
+
+        Assert(!translation.isNull());
+        // Map the current node to its translation in the cache.
+        d_intblastCache[current] = translation;
+        // Also map the translation to itself.
+        d_intblastCache[translation] = translation;
+        toVisit.pop_back();
+      }
+    }
+  }
+  return d_intblastCache[n].get();
+}
+
+Node IntBlaster::unsignedToSigned(Node n, uint64_t bw) { return Node(); }
+
+Node IntBlaster::translateWithChildren(
+    Node original,
+    const std::vector<Node>& translated_children,
+    std::vector<Node>& lemmas)
+{
+  Node binarized = makeBinary(original);
+  // continue to process the binarized version
+  return Node();
+}
+
+Node IntBlaster::translateNoChildren(Node original,
+                                     std::vector<Node>& lemmas,
+                                     std::map<Node, Node>& skolems)
+{
+  return Node();
+}
+
+Node IntBlaster::defineBVUFAsIntUF(Node bvUF, Node intUF) { return Node(); }
+
+Node IntBlaster::translateFunctionSymbol(Node bvUF,
+                                         std::map<Node, Node>& skolems)
+{
+  return Node();
+}
+
+bool IntBlaster::childrenTypesChanged(Node n) { return true; }
+
+Node IntBlaster::castToType(Node n, TypeNode tn) { return Node(); }
+
+Node IntBlaster::reconstructNode(Node originalNode,
+                                 TypeNode resultType,
+                                 const std::vector<Node>& translated_children)
+{
+  return Node();
+}
+
+Node IntBlaster::createShiftNode(std::vector<Node> children,
+                                 uint64_t bvsize,
+                                 bool isLeftShift)
+{
+  return Node();
+}
+
+Node IntBlaster::translateQuantifiedFormula(Node quantifiedNode)
+{
+  return Node();
+}
+
+Node IntBlaster::createBVNotNode(Node n, uint64_t bvsize) { return Node(); }
+
+}  // namespace cvc5
diff --git a/src/theory/bv/int_blaster.h b/src/theory/bv/int_blaster.h
index f8717e045..444eb88a7 100644
--- a/src/theory/bv/int_blaster.h
+++ b/src/theory/bv/int_blaster.h
@@ -75,9 +75,10 @@ namespace cvc5 {
 ** Tr((bvult a b)) = Tr(a) < Tr(b)
 ** Similar transformations are done for bvule, bvugt, and bvuge.
 **
-** Bit-vector operators that are not listed above are either eliminated using
-** the function eliminationPass, or go through the following default
-*translation, that also works for non-bit-vector operators
+** Bit-vector operators that are not listed above are either
+** eliminated using the BV rewriter,
+** or go through the following default
+** translation, that also works for non-bit-vector operators
 ** with result type BV:
 ** Tr((op t1 ... tn)) = (bv2nat (op (cast t1) ... (cast tn)))
 ** where (cast x) is ((_ nat2bv k) x) or just x,
@@ -118,8 +119,7 @@ class IntBlaster
    * ff((bv2nat x))), where k is the bit-width of the domain of f, i is the
    * bit-width of its range, and ff is a Int->Int function that corresponds to
    * f. For functions with other signatures this is similar
-   * @return integer node that corresponds to n, or a null node if d_supportNoBV
-   * is set to false and n is note purely BV.
+   * @return integer node that corresponds to n
    */
   Node intBlast(Node n,
                 std::vector<Node>& lemmas,
@@ -165,18 +165,15 @@ class IntBlaster
   Node mkRangeConstraint(Node newVar, uint64_t k);
 
   /**
-   * In the translation to integers, it is convenient to assume that certain
-   * bit-vector operators do not occur in the original formula (e.g., repeat).
-   * This function eliminates all these operators.
-   */
-  Node eliminationPass(Node n);
-
-  /**
    * Some bit-vector operators (e.g., bvadd, bvand) are binary, but allow more
    * than two arguments as a syntactic sugar.
    * For example, we can have a node for (bvand x y z),
    * that represents (bvand (x (bvand y z))).
-   * This function makes all such operators strictly binary.
+   * This function locally binarizes these operators.
+   * In the above example, this means that x,y,z
+   * are not handled recursively, but will require a separate
+   * call to the function.
+   *
    */
   Node makeBinary(Node n);
 
@@ -287,7 +284,7 @@ class IntBlaster
    * binary representation of n is the same as the
    * signed binary representation of m.
    */
-  Node unsignedTosigned(Node n, uint64_t bvsize);
+  Node unsignedToSigned(Node n, uint64_t bvsize);
 
   /**
    * Performs the actual translation to integers for nodes
@@ -308,8 +305,6 @@ class IntBlaster
 
   /** Caches for the different functions */
   CDNodeMap d_binarizeCache;
-  CDNodeMap d_eliminationCache;
-  CDNodeMap d_rebuildCache;
   CDNodeMap d_intblastCache;
 
   /** Node manager that is used throughout the pass */