From 5dd102d4cb7fc8413d6e8f68b0c32c9ef06b1b17 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 11 Oct 2017 22:20:17 -0700 Subject: [PATCH] Enable regressions for CBQI BV and fix inverse for LSHR. (#1234) This fixes and enables previously added regression tests for CBQI BV. It further removes one of the tests that was obsolete (since it goes through even without --cbqi-bv). This further fixes the inverse computation for BITVECTOR_LSHR, which was broken due to a mismatching bit-width when creating a shift node. --- src/theory/quantifiers/bv_inverter.cpp | 7 ++++--- test/regress/regress0/quantifiers/Makefile.am | 4 ++++ .../regress0/quantifiers/qbv-test-invert-bvand.smt2 | 1 + .../regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 | 1 + .../regress0/quantifiers/qbv-test-invert-bvor.smt2 | 1 + .../regress0/quantifiers/qbv-test-invert-bvult-0.smt2 | 8 -------- .../regress0/quantifiers/qbv-test-invert-bvult-1.smt2 | 1 + .../regress0/quantifiers/qbv-test-invert-bvurem-1.smt2 | 3 ++- 8 files changed, 14 insertions(+), 12 deletions(-) delete mode 100644 test/regress/regress0/quantifiers/qbv-test-invert-bvult-0.smt2 diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index 9b84c8ecf..0795c3068 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -384,9 +384,10 @@ Node BvInverter::solve_bv_constraint(Node sv, Node sv_t, Node t, Kind rk, * with w = getSize(t) = getSize(s) and z = 0 with getSize(z) = w */ unsigned w = bv::utils::getSize(s); Node z = bv::utils::mkZero(w); - Node z_o_t = nm->mkNode(BITVECTOR_CONCAT, z, t); - Node zot_shl_s = nm->mkNode(BITVECTOR_SHL, z_o_t, s); - Node ext = bv::utils::mkExtract(zot_shl_s, 2*w-1, w); + Node z_o_t = nm->mkNode(BITVECTOR_CONCAT, z, t); + Node z_o_s = nm->mkNode(BITVECTOR_CONCAT, z, s); + Node zot_shl_zos = nm->mkNode(BITVECTOR_SHL, z_o_t, z_o_s); + Node ext = bv::utils::mkExtract(zot_shl_zos, 2*w-1, w); scl = nm->mkNode(OR, nm->mkNode(EQUAL, s, z), nm->mkNode(EQUAL, ext, z)); diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index e045ad44c..3a8634d1e 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -91,6 +91,10 @@ TESTS = \ psyco-001-bv.smt2 \ bug822.smt2 \ qbv-test-invert-mul.smt2 \ + qbv-test-invert-bvand.smt2 \ + qbv-test-invert-bvor.smt2 \ + qbv-test-invert-bvlshr-0.smt2 \ + qbv-test-invert-bvurem-1.smt2 \ qbv-simple-2vars-vo.smt2 \ qbv-test-invert-concat-0.smt2 \ qbv-test-invert-concat-1.smt2 \ diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 index 040bc33c1..d611fcd68 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --cbqi-bv +; EXPECT: sat (set-logic BV) (set-info :status sat) (declare-fun a () (_ BitVec 32)) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 index 2fb5d9bec..d40e88248 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --cbqi-bv +; EXPECT: sat (set-logic BV) (set-info :status sat) (declare-fun a () (_ BitVec 32)) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 index c83b0ca73..287da08c7 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --cbqi-bv +; EXPECT: sat (set-logic BV) (set-info :status sat) (declare-fun a () (_ BitVec 32)) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvult-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvult-0.smt2 deleted file mode 100644 index f54abccfd..000000000 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvult-0.smt2 +++ /dev/null @@ -1,8 +0,0 @@ -; COMMAND-LINE: --cbqi-bv -(set-logic BV) -(set-info :status sat) -(declare-fun a () (_ BitVec 32)) - -(assert (forall ((x (_ BitVec 32))) (not (bvult x a) ))) - -(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 index a10f2fbea..13c1bf10a 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --cbqi-bv +; EXPECT: sat (set-logic BV) (set-info :status sat) (declare-fun a () (_ BitVec 32)) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2 index 6a1987c49..f7fe54e3e 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2 @@ -1,4 +1,5 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --bv-div-zero-const +; EXPECT: sat (set-logic BV) (set-info :status sat) (declare-fun a () (_ BitVec 32)) -- 2.30.2