From: yoni206 <yoni206@users.noreply.github.com>
Date: Tue, 29 Mar 2022 20:00:32 +0000 (+0300)
Subject: bv-to-int: fix translation of bvneg  (#8437)
X-Git-Tag: cvc5-1.0.0~136
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3d21e4397f5f5db2266b623729542755b34b1996;p=cvc5.git

bv-to-int: fix translation of bvneg  (#8437)

The translation of bvneg to integers did not match the comment documenting it, causing #8413 .
This PR fixes the issue and includes the test from #8413 as well as a simpler test.
Fixes #8413 .
---

diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp
index 875896cd4..a0596b3b6 100644
--- a/src/theory/bv/int_blaster.cpp
+++ b/src/theory/bv/int_blaster.cpp
@@ -255,6 +255,7 @@ Node IntBlaster::translateWithChildren(
   Assert(oldKind != kind::BITVECTOR_SREM);
   Assert(oldKind != kind::BITVECTOR_SMOD);
   Assert(oldKind != kind::BITVECTOR_XNOR);
+  Assert(oldKind != kind::BITVECTOR_NOR);
   Assert(oldKind != kind::BITVECTOR_NAND);
   Assert(oldKind != kind::BITVECTOR_SUB);
   Assert(oldKind != kind::BITVECTOR_REPEAT);
@@ -1080,8 +1081,8 @@ Node IntBlaster::createBVNegNode(Node n, uint64_t bvsize)
 {
   // Based on Hacker's Delight section 2-2 equation a:
   // -x = ~x+1
-  Node p2 = pow2(bvsize);
-  return d_nm->mkNode(kind::SUB, p2, n);
+  Node bvNotNode = createBVNotNode(n, bvsize);
+  return createBVAddNode(bvNotNode, d_one, bvsize);
 }
 
 Node IntBlaster::createBVNotNode(Node n, uint64_t bvsize)
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 000cbc376..ac0ec5f05 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -278,6 +278,8 @@ set(regress_0_tests
   regress0/bv/bv_to_int_bvuf_to_intuf.smt2
   regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
   regress0/bv/bv_to_int_elim_err.smt2
+  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_zext.smt2
   regress0/bv/bvcomp.cvc.smt2
diff --git a/test/regress/cli/regress0/bv/bv_to_int_issue_8413_1.smt2 b/test/regress/cli/regress0/bv/bv_to_int_issue_8413_1.smt2
new file mode 100644
index 000000000..48073ac67
--- /dev/null
+++ b/test/regress/cli/regress0/bv/bv_to_int_issue_8413_1.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --solve-bv-as-int=sum
+; EXPECT: sat
+
+(set-logic QF_BV)
+
+(declare-fun zero () (_ BitVec 16))
+(declare-fun x () (_ BitVec 16))
+
+(assert (= zero (_ bv0 16)))
+(assert (= zero (bvneg x)))
+
+(check-sat)
diff --git a/test/regress/cli/regress0/bv/bv_to_int_issue_8413_2.smt2 b/test/regress/cli/regress0/bv/bv_to_int_issue_8413_2.smt2
new file mode 100644
index 000000000..0dfa7a77a
--- /dev/null
+++ b/test/regress/cli/regress0/bv/bv_to_int_issue_8413_2.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --solve-bv-as-int=sum
+; EXPECT: sat
+
+(set-logic QF_BV)
+(declare-fun a () (_ BitVec 1))
+(assert (= (_ bv0 16) (bvsdiv ((_ zero_extend 8) ((_ zero_extend 7) a)) (bvnor (_ bv0 16) (_ bv0 16)))))
+(check-sat)