From cf97bbba5725abcb7a4085271719de8b1a832628 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Mon, 30 Jul 2018 15:24:55 -0700 Subject: 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. --- src/prop/cryptominisat.h | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/prop/cryptominisat.h') diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h index c265b2f35..c5345cb86 100644 --- a/src/prop/cryptominisat.h +++ b/src/prop/cryptominisat.h @@ -64,6 +64,8 @@ public: SatValue solve() override; SatValue solve(long unsigned int&) override; + SatValue solve(const std::vector& assumptions) override; + bool ok() const override; SatValue value(SatLiteral l) override; SatValue modelValue(SatLiteral l) override; -- cgit v1.2.3