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.

diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index 9b84c8ecfd368dfd2f36727a5aedbdd84dc110fe..0795c3068cb1ee3cd37b3c05971fbfd52b94f065 100644 (file)
--- 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 e045ad44c922b068dae02123dff83d5946664721..3a8634d1e27cbc02e52a3121022b458220f1c978 100644 (file)
--- 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 040bc33c185cbc5a5c483e3bbb5f639853cdf606..d611fcd6869fd390c1adb95d33fb19d390087790 100644 (file)
--- 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 2fb5d9becbdb2486fa2dfe7288f96494b23baa7f..d40e88248efb748a2f559973de83db7364ef0725 100644 (file)
--- 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 c83b0ca7343415c552dd76012ffb486ec9b3f75d..287da08c72919508d998890b63c2f3e729151766 100644 (file)
--- 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 (file)
index f54abcc..0000000
--- 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 a10f2fbeac681fcdd617664eb1e8fc9fec813966..13c1bf10a3b92772694c82e0053936340802a733 100644 (file)
--- 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 6a1987c49b97109adec815e5b39c980ea7e89e5e..f7fe54e3e2486c9dad1e71b9e8f60fe985d58c98 100644 (file)
--- 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))