From 26214b7b02e90fca270e6bac7d6b64ea1a6d723a Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 13 Dec 2017 19:10:16 -0800 Subject: 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. --- .../theory/theory_quantifiers_bv_inverter_white.h | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'test/unit/theory') 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); } }; -- cgit v1.2.3