From: yoni206 <yoni206@users.noreply.github.com>
Date: Wed, 20 Apr 2022 15:39:16 +0000 (+0300)
Subject: int-blaster: direct support for bvcomp (#8640)
X-Git-Tag: cvc5-1.0.1~241
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=854b81c30cbd189e89ef143f4a6aae6ac0deb915;p=cvc5.git

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 246b70d8a..85159a424 100644
--- 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 dd4039cf0..59891768a 100644
--- 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
index 000000000..a48502315
--- /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)