bv2int: new options for bvand translation (#5096)

Currently, (bvand x y) is translated into a sum of ITEs.
This PR introduces two more options for the translation of (bvand x y):

bv: cast the integer translations of x and y back to bit-vectors, do a bvand, and cast the result to integers.
iand: use the builtin iand operator.
These options are added to many of the tests, and some new tests are added.
In addition, some tests are cleaned up (e.g., removing --no-check-unsat-cores for satisfiable benchmarks).
Finally, some tests are moved from regress0 to regress2 because they take several seconds to complete (2 -- 10 seconds).

1 files changed, 36 insertions, 6 deletions

diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index aa1b5ac5b..9ee4e2b7d 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -169,7 +169,8 @@ Node BVToInt::eliminationPass(Node n)
   {
     current = toVisit.back();
     // assert that the node is binarized
-    kind::Kind_t k = current.getKind();
+    // The following variable is only used in assertions
+    CVC4_UNUSED kind::Kind_t k = current.getKind();
     uint64_t numChildren = current.getNumChildren();
     Assert((numChildren == 2)
            || !(k == kind::BITVECTOR_PLUS || k == kind::BITVECTOR_MULT
@@ -350,7 +351,8 @@ Node BVToInt::translateWithChildren(Node original,
   // ultbv and sltbv were supposed to be eliminated before this point.
   Assert(oldKind != kind::BITVECTOR_ULTBV);
   Assert(oldKind != kind::BITVECTOR_SLTBV);
-  uint64_t originalNumChildren = original.getNumChildren();
+  // The following variable will only be used in assertions.
+  CVC4_UNUSED uint64_t originalNumChildren = original.getNumChildren();
   Node returnNode;
   switch (oldKind)
   {
@@ -414,15 +416,43 @@ Node BVToInt::translateWithChildren(Node original,
     }
     case kind::BITVECTOR_AND:
     {
-      // Construct an ite, based on granularity.
+      // We support three configurations:
+      // 1. translating to IAND
+      // 2. translating back to BV (using BITVECTOR_TO_NAT and INT_TO_BV
+      // operators)
+      // 3. translating into a sum
       uint64_t bvsize = original[0].getType().getBitVectorSize();
-      Assert(translated_children.size() == 2);
-      Node newNode = createBitwiseNode(translated_children[0],
+      if (options::solveBVAsInt() == options::SolveBVAsIntMode::IAND)
+      {
+        Node iAndOp = d_nm->mkConst(IntAnd(bvsize));
+        returnNode = d_nm->mkNode(
+            kind::IAND, iAndOp, translated_children[0], translated_children[1]);
+      }
+      else if (options::solveBVAsInt() == options::SolveBVAsIntMode::BV)
+      {
+        // translate the children back to BV
+        Node intToBVOp = d_nm->mkConst<IntToBitVector>(IntToBitVector(bvsize));
+        Node x = translated_children[0];
+        Node y = translated_children[1];
+        Node bvx = d_nm->mkNode(intToBVOp, x);
+        Node bvy = d_nm->mkNode(intToBVOp, y);
+        // perform bvand on the bit-vectors
+        Node bvand = d_nm->mkNode(kind::BITVECTOR_AND, bvx, bvy);
+        // translate the result to integers
+        returnNode = d_nm->mkNode(kind::BITVECTOR_TO_NAT, bvand);
+      }
+      else
+      {
+        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 = newNode;
+      }
       break;
     }
     case kind::BITVECTOR_SHL: