diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-07-30 15:24:55 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-07-30 15:24:55 -0700 |
| commit | cf97bbba5725abcb7a4085271719de8b1a832628 (patch) | |
| tree | b6a62fa6abef6aacc07e1d0ff25d71789d92f3f5 /test | |
| parent | 46520451e7f6408c6caf3e52a15672732abc5911 (diff) | |
Add support for incremental eager bit-blasting. (#1838)
Eager incremental solving is achieved via solving under assumptions. As soon as incremental and eager bit-blasting is enabled, assertions are passed to the SAT solver as assumptions rather than assertions. This requires the eager SAT solver to support incremental solving, which is currently only supported by CryptoMiniSat.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/Makefile.tests | 1 | ||||
| -rw-r--r-- | test/regress/regress0/bv/eager-inc-cryptominisat.smt2 | 27 | ||||
| -rw-r--r-- | test/unit/theory/theory_bv_white.h | 7 |
3 files changed, 33 insertions, 2 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index c43e083f3..c15e3d045 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -239,6 +239,7 @@ REG0_TESTS = \ regress0/bv/core/slice-18.smt \ regress0/bv/core/slice-19.smt \ regress0/bv/core/slice-20.smt \ + regress0/bv/eager-inc-cryptominisat.smt2 \ regress0/bv/divtest_2_5.smt2 \ regress0/bv/divtest_2_6.smt2 \ regress0/bv/fuzz01.smt \ diff --git a/test/regress/regress0/bv/eager-inc-cryptominisat.smt2 b/test/regress/regress0/bv/eager-inc-cryptominisat.smt2 new file mode 100644 index 000000000..1c96ca25d --- /dev/null +++ b/test/regress/regress0/bv/eager-inc-cryptominisat.smt2 @@ -0,0 +1,27 @@ +; REQUIRES: cryptominisat +; COMMAND-LINE: --incremental --bv-sat-solver=cryptominisat --bitblast=eager +(set-logic QF_BV) +(set-option :incremental true) +(declare-fun a () (_ BitVec 16)) +(declare-fun b () (_ BitVec 16)) +(declare-fun c () (_ BitVec 16)) + +(assert (bvult a (bvadd b c))) +(check-sat) +; EXPECT: sat + +(push 1) +(assert (bvult c b)) +(check-sat) +; EXPECT: sat + + +(push 1) +(assert (bvugt c b)) +(check-sat) +; EXPECT: unsat +(pop 2) + +(check-sat) +; EXPECT: sat +(exit) diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h index f95785f53..c830e7813 100644 --- a/test/unit/theory/theory_bv_white.h +++ b/test/unit/theory/theory_bv_white.h @@ -67,8 +67,11 @@ public: void testBitblasterCore() { d_smt->setOption("bitblast", SExpr("eager")); - EagerBitblaster* bb = new EagerBitblaster(dynamic_cast<TheoryBV*>( - d_smt->d_theoryEngine->d_theoryTable[THEORY_BV])); + d_smt->setOption("incremental", SExpr("false")); + EagerBitblaster* bb = new EagerBitblaster( + dynamic_cast<TheoryBV*>( + d_smt->d_theoryEngine->d_theoryTable[THEORY_BV]), + d_smt->d_context); 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); |