Add support for incremental eager bit-blasting. (#1838)
authorMathias Preiner <mathias.preiner@gmail.com>
Mon, 30 Jul 2018 22:24:55 +0000 (15:24 -0700)
committerGitHub <noreply@github.com>
Mon, 30 Jul 2018 22:24:55 +0000 (15:24 -0700)
commitcf97bbba5725abcb7a4085271719de8b1a832628
treeb6a62fa6abef6aacc07e1d0ff25d71789d92f3f5
parent46520451e7f6408c6caf3e52a15672732abc5911
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.
13 files changed:
src/options/options_handler.cpp
src/prop/cryptominisat.cpp
src/prop/cryptominisat.h
src/prop/sat_solver.h
src/smt/smt_engine.cpp
src/theory/bv/bitblast/eager_bitblaster.cpp
src/theory/bv/bitblast/eager_bitblaster.h
src/theory/bv/bv_eager_solver.cpp
src/theory/bv/bv_eager_solver.h
src/theory/bv/theory_bv.cpp
test/regress/Makefile.tests
test/regress/regress0/bv/eager-inc-cryptominisat.smt2 [new file with mode: 0644]
test/unit/theory/theory_bv_white.h