diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2017-10-04 20:40:11 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-04 20:40:11 -0700 |
commit | a63efde07c65a3a0499f85c13757643ff52f154c (patch) | |
tree | d125c7f47dd4e25ba6a51cd59fb2c1d24e5f5970 /test/unit | |
parent | 01c540202392fad77ee32c65e065257890c8d07e (diff) |
Add mkZero, mkOne and mkUmulo to bv utils. (#1200)
This adds several utility functions for the theory BV. Function mkUmulo encodes an unsigned multiplication overflow detection operation, which we need for CBQI BV. In the future, we will introduce a Umulo node kind (and a corresponding bit-blasting strategy based on the encoding implemented in mkUmulo).
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/theory/theory_bv_white.h | 37 |
1 files changed, 29 insertions, 8 deletions
diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h index 19b715f76..5721957ec 100644 --- a/test/unit/theory/theory_bv_white.h +++ b/test/unit/theory/theory_bv_white.h @@ -47,7 +47,6 @@ class TheoryBVWhite : public CxxTest::TestSuite { NodeManager* d_nm; SmtEngine* d_smt; SmtScope* d_scope; - EagerBitblaster* d_bb; public: @@ -58,18 +57,18 @@ public: d_nm = NodeManager::fromExprManager(d_em); d_smt = new SmtEngine(d_em); d_scope = new SmtScope(d_smt); - d_smt->setOption("bitblast", SExpr("eager")); - d_bb = new EagerBitblaster(dynamic_cast<TheoryBV*>(d_smt->d_theoryEngine->d_theoryTable[THEORY_BV])); } void tearDown() { - delete d_bb; delete d_scope; delete d_smt; delete d_em; } void testBitblasterCore() { + d_smt->setOption("bitblast", SExpr("eager")); + EagerBitblaster* bb = new EagerBitblaster(dynamic_cast<TheoryBV*>( + d_smt->d_theoryEngine->d_theoryTable[THEORY_BV])); Node x = d_nm->mkVar("x", d_nm->mkBitVectorType(16)); Node y = d_nm->mkVar("y", d_nm->mkBitVectorType(16)); Node x_plus_y = d_nm->mkNode(kind::BITVECTOR_PLUS, x, y); @@ -77,11 +76,33 @@ public: Node x_shl_one = d_nm->mkNode(kind::BITVECTOR_SHL, x, one); Node eq = d_nm->mkNode(kind::EQUAL, x_plus_y, x_shl_one); Node not_x_eq_y = d_nm->mkNode(kind::NOT, d_nm->mkNode(kind::EQUAL, x, y)); - - d_bb->bbFormula(eq); - d_bb->bbFormula(not_x_eq_y); - bool res = d_bb->solve(); + bb->bbFormula(eq); + bb->bbFormula(not_x_eq_y); + + bool res = bb->solve(); TS_ASSERT (res == false); + delete bb; + } + + void testMkUmulo() { + d_smt->setOption("incremental", SExpr("true")); + for (size_t w = 1; w < 16; ++w) { + d_smt->push(); + Node x = d_nm->mkVar("x", d_nm->mkBitVectorType(w)); + Node y = d_nm->mkVar("y", d_nm->mkBitVectorType(w)); + + Node zx = mkConcat(mkZero(w), x); + Node zy = mkConcat(mkZero(w), y); + Node mul = d_nm->mkNode(kind::BITVECTOR_MULT, zx, zy); + Node lhs = + d_nm->mkNode(kind::DISTINCT, mkExtract(mul, 2 * w - 1, w), mkZero(w)); + Node rhs = mkUmulo(x, y); + Node eq = d_nm->mkNode(kind::DISTINCT, lhs, rhs); + d_smt->assertFormula(eq.toExpr()); + Result res = d_smt->checkSat(); + TS_ASSERT(res.isSat() == Result::UNSAT); + d_smt->pop(); + } } };/* class TheoryBVWhite */ |