Add bitwise option to IntBlaster (#7721)

This is part of a series of PRs by @yoni206  to add full int-blasting support to the master branch of `cvc5`. This adds support for the bitwise encoding to `IntBlaster`. Future PRs would unify the `bv2int` and `IntBlaster` helper functions.

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 2e2742e733ee44e68dacc4872d028c7d517f19c2..026c8f494ff296f65c8d7e0897a535a94c5b1a89 100644 (file)
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -395,6 +395,9 @@ name   = "SMT Layer"
 [[option.mode.BV]]
   name = "bv"
   help = "Translate bvand back to bit-vectors"
+[[option.mode.BITWISE]]
+  name = "bitwise"
+  help = "Introduce a UF operator for bvand, and eagerly add bitwise lemmas"
 
 [[option]]
   name       = "BVAndIntegerGranularity"

diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index 33f3dd445f97cf15a6889e91c22ca9114f1c34c0..f106f1ccf461de69284466506397e47e9ed6b5d1 100644 (file)
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -27,6 +27,7 @@
 #include "expr/node.h"
 #include "expr/node_traversal.h"
 #include "expr/skolem_manager.h"
+#include "options/option_exception.h"
 #include "options/smt_options.h"
 #include "options/uf_options.h"
 #include "preprocessing/assertion_pipeline.h"
@@ -938,6 +939,11 @@ BVToInt::BVToInt(PreprocessingPassContext* preprocContext)
   d_nm = NodeManager::currentNM();
   d_zero = d_nm->mkConst(CONST_RATIONAL, Rational(0));
   d_one = d_nm->mkConst(CONST_RATIONAL, Rational(1));
+
+  if (options().smt.solveBVAsInt == options::SolveBVAsIntMode::BITWISE)
+  {
+    throw OptionException("bitwise option is not supported currently");
+  }
 };
 
 PreprocessingPassResult BVToInt::applyInternal(

diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp
index 649be5aabb9f7bdd8f6d3ae70014d677691c69c0..0109649f00885d18f2471ea2ce4fecfbefcf636e 100644 (file)
--- a/src/theory/bv/int_blaster.cpp
+++ b/src/theory/bv/int_blaster.cpp
@@ -547,6 +547,11 @@ Node IntBlaster::translateWithChildren(
     case kind::BOUND_VAR_LIST:
     {
       returnNode = d_nm->mkNode(oldKind, translated_children);
+      if (d_mode == options::SolveBVAsIntMode::BITWISE)
+      {
+        throw OptionException(
+            "--solve-bv-as-int=bitwise does not support quantifiers");
+      }
       break;
     }
     case kind::FORALL:
@@ -1008,6 +1013,38 @@ Node IntBlaster::createBVAndNode(Node x,
     // Construct a sum of ites, based on granularity.
     returnNode = d_iandUtils.createSumNode(x, y, bvsize, d_granularity);
   }
+  else
+  {
+    Assert(d_mode == options::SolveBVAsIntMode::BITWISE);
+    // Enforce semantics over individual bits with iextract and ites
+    uint64_t granularity = options::BVAndIntegerGranularity();
+
+    Node iAndOp = d_nm->mkConst(IntAnd(bvsize));
+    Node iAnd = d_nm->mkNode(kind::IAND, iAndOp, x, y);
+    // get a skolem so the IAND solver knows not to do work
+    returnNode = d_nm->getSkolemManager()->mkPurifySkolem(
+        iAnd,
+        "__intblast__iand",
+        "skolem for an IAND node in bitwise mode " + iAnd.toString());
+    addRangeConstraint(returnNode, bvsize, lemmas);
+
+    // eagerly add bitwise lemmas according to the provided granularity
+    uint64_t high_bit;
+    for (uint64_t j = 0; j < bvsize; j += granularity)
+    {
+      high_bit = j + granularity - 1;
+      // don't let high_bit pass bvsize
+      if (high_bit >= bvsize)
+      {
+        high_bit = bvsize - 1;
+      }
+      Node extractedReturnNode = d_iandUtils.iextract(high_bit, j, returnNode);
+      addBitwiseConstraint(
+          extractedReturnNode.eqNode(
+              d_iandUtils.createBitwiseIAndNode(x, y, high_bit, j)),
+          lemmas);
+    }
+  }
   return returnNode;
 }
 

diff --git a/test/unit/theory/theory_bv_int_blaster_white.cpp b/test/unit/theory/theory_bv_int_blaster_white.cpp
index 2ad8695de76547677b8a6157700059f4345ff820..0412fdabb98c540c074de4175f72d02ce2de0ddb 100644 (file)
--- a/test/unit/theory/theory_bv_int_blaster_white.cpp
+++ b/test/unit/theory/theory_bv_int_blaster_white.cpp
@@ -130,7 +130,7 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_uf)
 }
 
 /** Check all cases of the translation.
- * This is a sanity check, that noly verifies
+ * This is a sanity check, that only verifies
  * the expected type, and that there were no
  * failures.
  */
@@ -280,5 +280,45 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_with_children)
   ASSERT_TRUE(result.getType().isInteger());
 }
 
+/** Check AND translation for bitwise option.
+ * This is a sanity check, that only verifies
+ * the expected kind, and that there were no
+ * failures.
+ */
+TEST_F(TestTheoryWhiteBvIntblaster, intblaster_bitwise)
+{
+  // place holders for lemmas and skolem
+  std::vector<Node> lemmas;
+  std::map<Node, Node> skolems;
+  Options opts;
+  Env env(d_nodeManager, &opts);
+  env.d_logic.setLogicString("QF_UFBV");
+  env.d_logic.lock();
+  IntBlaster intBlaster(env, options::SolveBVAsIntMode::BITWISE, 1, true);
+
+  // bit-vector variables
+  TypeNode bvType = d_nodeManager->mkBitVectorType(4);
+  Node v1 = d_nodeManager->mkVar("v1", bvType);
+  Node v2 = d_nodeManager->mkVar("v2", bvType);
+
+  // translated integer variables
+  Node i1 = intBlaster.translateNoChildren(v1, lemmas, skolems);
+  Node i2 = intBlaster.translateNoChildren(v2, lemmas, skolems);
+
+  // if original is BV, result should be Int.
+  // Otherwise, they should have the same type.
+  Node original;
+  Node result;
+
+  // bvand
+  original = d_nodeManager->mkNode(BITVECTOR_AND, v1, v2);
+  size_t orig_num_lemmas = lemmas.size();
+  result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas);
+  // should have kind skolem, would use bitwise comparisons to refine
+  ASSERT_TRUE(result.getKind() == kind::SKOLEM);
+  // check that a lemma was added
+  ASSERT_TRUE(lemmas.size() > orig_num_lemmas);
+}
+
 }  // namespace test
 }  // namespace cvc5