From 3d21e4397f5f5db2266b623729542755b34b1996 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Tue, 29 Mar 2022 23:00:32 +0300 Subject: [PATCH] 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 . --- src/theory/bv/int_blaster.cpp | 5 +++-- test/regress/cli/CMakeLists.txt | 2 ++ .../cli/regress0/bv/bv_to_int_issue_8413_1.smt2 | 12 ++++++++++++ .../cli/regress0/bv/bv_to_int_issue_8413_2.smt2 | 7 +++++++ 4 files changed, 24 insertions(+), 2 deletions(-) create mode 100644 test/regress/cli/regress0/bv/bv_to_int_issue_8413_1.smt2 create mode 100644 test/regress/cli/regress0/bv/bv_to_int_issue_8413_2.smt2 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) -- 2.30.2