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.

1 files changed, 5 insertions, 121 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);