Add missing side conditions for SHL, LSHR, ASHR for CBQI BV. (#1441)

This adds side conditions for operators BITVECTOR_SHL, BITVECTOR_LSHR and
BITVECTOR_ASHR for index = 1, i.e., s << x = t and s >> x = t. Previously, we treated
 these cases as non-invertible.

1 files changed, 10 insertions, 10 deletions

diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.h b/test/unit/theory/theory_quantifiers_bv_inverter_white.h
index 04c97a831..ce01c17e4 100644
--- a/test/unit/theory/theory_quantifiers_bv_inverter_white.h
+++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.h
@@ -84,10 +84,6 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
            || k == kind::BITVECTOR_ASHR
            || k == kind::BITVECTOR_SHL);
     Assert(k != kind::BITVECTOR_UREM_TOTAL || idx == 1);
-    Assert((k != kind::BITVECTOR_LSHR
-            && k != kind::BITVECTOR_ASHR
-            && k != kind::BITVECTOR_SHL)
-           || idx == 0);
 
     Node sc = getsc(k, idx, d_sk, d_s, d_t);
     Kind ksc = sc.getKind();
@@ -98,6 +94,12 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
     Node scr = d_nm->mkNode(kind::EXISTS, d_bvarlist, body);
     Expr a = d_nm->mkNode(kind::DISTINCT, sc[0], scr).toExpr();
     Result res = d_smt->checkSat(a);
+    if (res.d_sat == Result::SAT)
+    {
+      std::cout << std::endl << "s " << d_smt->getValue(d_s.toExpr()) << std::endl;
+      std::cout << "t " << d_smt->getValue(d_t.toExpr()) << std::endl;
+      std::cout << "x " << d_smt->getValue(d_x.toExpr()) << std::endl;
+    }
     TS_ASSERT(res.d_sat == Result::UNSAT);
   }
 
@@ -110,6 +112,7 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
     d_nm = NodeManager::fromExprManager(d_em);
     d_smt = new SmtEngine(d_em);
     d_smt->setOption("cbqi-bv", CVC4::SExpr(false));
+    d_smt->setOption("produce-models", CVC4::SExpr(true));
     d_scope = new SmtScope(d_smt);
 
     d_s = d_nm->mkVar("s", d_nm->mkBitVectorType(4));
@@ -243,8 +246,7 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
 
   void testGetScBvLshr1()
   {
-    TS_ASSERT_THROWS(runTest(BITVECTOR_LSHR, 1, getScBvLshr),
-                     AssertionException);
+    runTest(BITVECTOR_LSHR, 1, getScBvLshr);
   }
 
   void testGetScBvAshr0()
@@ -254,8 +256,7 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
 
   void testGetScBvAshr1()
   {
-    TS_ASSERT_THROWS(runTest(BITVECTOR_ASHR, 1, getScBvAshr),
-                     AssertionException);
+    runTest(BITVECTOR_ASHR, 1, getScBvAshr);
   }
 
   void testGetScBvShl0()
@@ -265,8 +266,7 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
 
   void testGetScBvShl1()
   {
-    TS_ASSERT_THROWS(runTest(BITVECTOR_SHL, 1, getScBvShl),
-                     AssertionException);
+    runTest(BITVECTOR_SHL, 1, getScBvShl);
   }
 
 };