diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2017-12-13 19:10:16 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-12-13 19:10:16 -0800 |
commit | 26214b7b02e90fca270e6bac7d6b64ea1a6d723a (patch) | |
tree | e27be86f2fd70c677ed7edaa7527d6ab43e6e21d /test/unit/theory | |
parent | 83d2279aaa79ce04aa35b394b5063c6d59ff3ac1 (diff) |
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.
Diffstat (limited to 'test/unit/theory')
-rw-r--r-- | test/unit/theory/theory_quantifiers_bv_inverter_white.h | 20 |
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); } }; |