int-blaster: direct support for bvcomp (#8640)

This PR adds a translation of bvcomp using an ite.
Fixes cvc5/cvc5-projects#417
and contains the failed formula as a regression.

diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp
index 246b70d8a399bface6855948f9a241f7691b3958..85159a4240b05a714fa18b10b0619bb1a163b1ba 100644 (file)
--- a/src/theory/bv/int_blaster.cpp
+++ b/src/theory/bv/int_blaster.cpp
@@ -261,7 +261,6 @@ Node IntBlaster::translateWithChildren(
   Assert(oldKind != kind::BITVECTOR_REPEAT);
   Assert(oldKind != kind::BITVECTOR_ROTATE_RIGHT);
   Assert(oldKind != kind::BITVECTOR_ROTATE_LEFT);
-  Assert(oldKind != kind::BITVECTOR_COMP);
   Assert(oldKind != kind::BITVECTOR_SGT);
   Assert(oldKind != kind::BITVECTOR_SLE);
   Assert(oldKind != kind::BITVECTOR_SGE);
@@ -517,6 +516,17 @@ Node IntBlaster::translateWithChildren(
                        d_zero);
       break;
     }
+    case kind::BITVECTOR_COMP:
+    {
+      returnNode =
+          d_nm->mkNode(kind::ITE,
+                       d_nm->mkNode(kind::EQUAL,
+                                    translated_children[0],
+                                    translated_children[1]),
+                       d_one,
+                       d_zero);
+      break;
+    }
     case kind::ITE:
     {
       returnNode = d_nm->mkNode(oldKind, translated_children);

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index dd4039cf01b4209799b0f5709deaa58b9b63ba66..59891768a813fc74295ba0079d897b953dde76c6 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -283,6 +283,7 @@ set(regress_0_tests
   regress0/bv/bv_to_int_issue_8413_1.smt2
   regress0/bv/bv_to_int_issue_8413_2.smt2
   regress0/bv/bv_to_int_int1.smt2
+  regress0/bv/bv_to_int_proj_417.smt2
   regress0/bv/bv_to_int_zext.smt2
   regress0/bv/bvcomp.cvc.smt2
   regress0/bv/bvmul-pow2-only.smt2

diff --git a/test/regress/cli/regress0/bv/bv_to_int_proj_417.smt2 b/test/regress/cli/regress0/bv/bv_to_int_proj_417.smt2
new file mode 100644 (file)
index 0000000..a485023
--- /dev/null
+++ b/test/regress/cli/regress0/bv/bv_to_int_proj_417.smt2
@@ -0,0 +1,6 @@
+; EXPECT: unsat
+(set-logic QF_BV)
+(set-option :solve-bv-as-int bitwise)
+(declare-const _x15 (_ BitVec 86))
+(assert (let ((_let0 (bvcomp _x15 _x15)))(bvugt _let0 _let0)))
+(check-sat)