bv2int: bvand translation code move (#5227)

This PR is essentially a code move.
It moves the code that translates bvand from the bv_to_int preprocessing pass to a new class IAndHelper, in the new files nl_iand_utils.{h,cpp}. The goal is to have this code in a place which can be shared between the bv2int preprocessing pass and the iand solver.

Future PRs will:

Optimize this utility
Make use of it in the iand solver
The code in nl_iand_utils.{h,cpp} is almost completely a move from bv_to_int.{h,cpp}. The changes are all minor, and include, e.g., the following changes:

the node manager is no longer a member, and so is the constant 0.
using the oneBitAnd function directly, without a function pointer.

2 files changed, 9 insertions, 194 deletions

diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index 9ee4e2b7d..06a5714d3 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -45,7 +45,6 @@ Rational intpow2(uint64_t b)
 /**
  * Helper functions for createBitwiseNode
  */
-bool oneBitAnd(bool a, bool b) { return (a && b); }
 
 } //end empty namespace
 
@@ -446,12 +445,11 @@ Node BVToInt::translateWithChildren(Node original,
         Assert(options::solveBVAsInt() == options::SolveBVAsIntMode::SUM);
         // Construct a sum of ites, based on granularity.
         Assert(translated_children.size() == 2);
-        Node newNode = createBitwiseNode(translated_children[0],
-                                       translated_children[1],
-                                       bvsize,
-                                       options::BVAndIntegerGranularity(),
-                                       &oneBitAnd);
-        returnNode = newNode;
+        returnNode =
+            d_iandTable.createBitwiseNode(translated_children[0],
+                                          translated_children[1],
+                                          bvsize,
+                                          options::BVAndIntegerGranularity());
       }
       break;
     }
@@ -1077,120 +1075,6 @@ Node BVToInt::translateQuantifiedFormula(Node quantifiedNode)
   return result;
 }
 
-Node BVToInt::createITEFromTable(
-    Node x,
-    Node y,
-    uint64_t granularity,
-    std::map<std::pair<uint64_t, uint64_t>, uint64_t> table)
-{
-  Assert(granularity <= 8);
-  uint64_t max_value = ((uint64_t)pow(2, granularity));
-  // The table represents a function from pairs of integers to integers, where
-  // all integers are between 0 (inclusive) and max_value (exclusive).
-  Assert(table.size() == max_value * max_value);
-  Node ite = d_nm->mkConst<Rational>(table[std::make_pair(0, 0)]);
-  for (uint64_t i = 0; i < max_value; i++)
-  {
-    for (uint64_t j = 0; j < max_value; j++)
-    {
-      if ((i == 0) && (j == 0))
-      {
-        continue;
-      }
-      ite = d_nm->mkNode(
-          kind::ITE,
-          d_nm->mkNode(
-              kind::AND,
-              d_nm->mkNode(kind::EQUAL, x, d_nm->mkConst<Rational>(i)),
-              d_nm->mkNode(kind::EQUAL, y, d_nm->mkConst<Rational>(j))),
-          d_nm->mkConst<Rational>(table[std::make_pair(i, j)]),
-          ite);
-    }
-  }
-  return ite;
-}
-
-Node BVToInt::createBitwiseNode(Node x,
-                                Node y,
-                                uint64_t bvsize,
-                                uint64_t granularity,
-                                bool (*f)(bool, bool))
-{
-  /**
-   * Standardize granularity.
-   * If it is greater than bvsize, it is set to bvsize.
-   * Otherwise, it is set to the closest (going down)  divider of bvsize.
-   */
-  Assert(0 < granularity && granularity <= 8);
-  if (granularity > bvsize)
-  {
-    granularity = bvsize;
-  }
-  else
-  {
-    while (bvsize % granularity != 0)
-    {
-      granularity = granularity - 1;
-    }
-  }
-  // transform f into a table
-  // f is defined over 1 bit, while the table is defined over `granularity` bits
-  std::map<std::pair<uint64_t, uint64_t>, uint64_t> table;
-  uint64_t max_value = ((uint64_t)pow(2, granularity));
-  for (uint64_t i = 0; i < max_value; i++)
-  {
-    for (uint64_t j = 0; j < max_value; j++)
-    {
-      uint64_t sum = 0;
-      for (uint64_t n = 0; n < granularity; n++)
-      {
-        // b is the result of f on the current bit
-        bool b = f((((i >> n) & 1) == 1), (((j >> n) & 1) == 1));
-        // add the corresponding power of 2 only if the result is 1
-        if (b)
-        {
-          sum += 1 << n;
-        }
-      }
-      table[std::make_pair(i, j)] = sum;
-    }
-  }
-   Assert(table.size() == max_value * max_value);
-
-  /*
-   * Create the sum.
-   * For granularity 1, the sum has bvsize elements.
-   * In contrast, if bvsize = granularity, sum has one element.
-   * Each element in the sum is an ite that corresponds to the generated table,
-   * multiplied by the appropriate power of two.
-   * More details are in bv_to_int.h .
-   */
-  uint64_t sumSize = bvsize / granularity;
-  Node sumNode = d_zero;
-  /**
-   * extract definition in integers is:
-   * (define-fun intextract ((k Int) (i Int) (j Int) (a Int)) Int
-   * (mod (div a (two_to_the j)) (two_to_the (+ (- i j) 1))))
-   */
-  for (uint64_t i = 0; i < sumSize; i++)
-  {
-    Node xExtract = d_nm->mkNode(
-        kind::INTS_MODULUS_TOTAL,
-        d_nm->mkNode(kind::INTS_DIVISION_TOTAL, x, pow2(i * granularity)),
-        pow2(granularity));
-    Node yExtract = d_nm->mkNode(
-        kind::INTS_MODULUS_TOTAL,
-        d_nm->mkNode(kind::INTS_DIVISION_TOTAL, y, pow2(i * granularity)),
-        pow2(granularity));
-    Node ite = createITEFromTable(xExtract, yExtract, granularity, table);
-    sumNode =
-        d_nm->mkNode(kind::PLUS,
-                     sumNode,
-                     d_nm->mkNode(kind::MULT, pow2(i * granularity), ite));
-  }
-  return sumNode;
-}
-
 Node BVToInt::createBVNotNode(Node n, uint64_t bvsize)
 {
   return d_nm->mkNode(kind::MINUS, maxInt(bvsize), n);
diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h
index d1562ad65..0f6a6a4bb 100644
--- a/src/preprocessing/passes/bv_to_int.h
+++ b/src/preprocessing/passes/bv_to_int.h
@@ -75,6 +75,7 @@
 #include "context/context.h"
 #include "preprocessing/preprocessing_pass.h"
 #include "preprocessing/preprocessing_pass_context.h"
+#include "theory/arith/nl/iand_table.h"
 
 namespace CVC4 {
 namespace preprocessing {
@@ -90,79 +91,6 @@ class BVToInt : public PreprocessingPass
  protected:
   PreprocessingPassResult applyInternal(
       AssertionPipeline* assertionsToPreprocess) override;
-
-  /**
-   * A generic function that creates a node that represents a bitwise
-   * operation.
-   *
-   * For example: Suppose bvsize is 4, granularity is 1, and f(x,y) = x && y.
-   * Denote by ITE(a,b) the term: ite(a==0, 0, ite(b==1, 1, 0)).
-   * The result of this function would be:
-   * ITE(x[0], y[0])*2^0 + ... + ITE(x[3], y[3])*2^3
-   *
-   * For another example: Suppose bvsize is 4, granularity is 2,
-   * and f(x,y) = x && y.
-   * Denote by ITE(a,b) the term that corresponds to the following table:
-   * a | b |  ITE(a,b)
-   * ----------------
-   * 0 | 0 | 0
-   * 0 | 1 | 0
-   * 0 | 2 | 0
-   * 0 | 3 | 0
-   * 1 | 0 | 0
-   * 1 | 1 | 1
-   * 1 | 2 | 0
-   * 1 | 3 | 1
-   * 2 | 0 | 0
-   * 2 | 1 | 0
-   * 2 | 2 | 2
-   * 2 | 3 | 2
-   * 3 | 0 | 0
-   * 3 | 1 | 1
-   * 3 | 2 | 2
-   * 3 | 3 | 3
-   *
-   * For example, 2 in binary is 10 and 1 in binary is 01, and so doing
-   * "bitwise f" on them gives 00.
-   * The result of this function would be:
-   * ITE(x[1:0], y[1:0])*2^0 + ITE(x[3:2], y[3:2])*2^2
-   *
-   *
-   * @param x is an integer operand that correspond to the first original
-   *        bit-vector operand.
-   * @param y is an integer operand that correspond to the second original
-   *        bit-vector operand.
-   * @param bvsize is the bit width of the original bit-vector variables.
-   * @param granularity is specified in the options for this preprocessing
-   *        pass.
-   * @param f is a pointer to a boolean function that corresponds
-   *        to the original bitwise operation.
-   * @return A node that represents the operation, as described above.
-   */
-  Node createBitwiseNode(Node x,
-                         Node y,
-                         uint64_t bvsize,
-                         uint64_t granularity,
-                         bool (*f)(bool, bool));
-
-  /**
-   * A helper function for createBitwiseNode
-   * @param x integer node corresponding to the original first bit-vector
-   *        argument
-   * @param y integer node corresponding to the original second bit-vector
-   *        argument nodes.
-   * @param granularity the bitwidth of the original bit-vector nodes.
-   * @param table a function from pairs of integers to integers.
-   *        The domain of this function consists of pairs of
-   *        integers between 0 (inclusive) and 2^{bitwidth} (exclusive).
-   * @return An ite term that represents this table.
-   */
-  Node createITEFromTable(
-      Node x,
-      Node y,
-      uint64_t granularity,
-      std::map<std::pair<uint64_t, uint64_t>, uint64_t> table);
-
   /**
    * A generic function that creates a logical shift node (either left or
    * right). a << b gets translated to a * 2^b mod 2^k, where k is the bit
@@ -354,6 +282,9 @@ class BVToInt : public PreprocessingPass
    */
   Node d_zero;
   Node d_one;
+  
+  /** helper class for handeling bvand translation */
+  theory::arith::nl::IAndTable d_iandTable;
 };
 
 }  // namespace passes