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.

3 files changed, 20 insertions, 0 deletions

diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
index 4f239343e..df5a20791 100644
--- a/src/prop/cryptominisat.cpp
+++ b/src/prop/cryptominisat.cpp
@@ -164,6 +164,18 @@ SatValue CryptoMinisatSolver::solve(long unsigned int& resource) {
   return solve();
 }
 
+SatValue CryptoMinisatSolver::solve(const std::vector<SatLiteral>& assumptions)
+{
+  TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime);
+  std::vector<CMSat::Lit> assumpts;
+  for (const SatLiteral& lit : assumptions)
+  {
+    assumpts.push_back(toInternalLit(lit));
+  }
+  ++d_statistics.d_statCallsToSolve;
+  return toSatLiteralValue(d_solver->solve(&assumpts));
+}
+
 SatValue CryptoMinisatSolver::value(SatLiteral l){
   const std::vector<CMSat::lbool> model = d_solver->get_model();
   CMSatVar var = l.getSatVariable();
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<SatLiteral>& assumptions) override;
+
   bool ok() const override;
   SatValue value(SatLiteral l) override;
   SatValue modelValue(SatLiteral l) override;
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 055efa413..add73eebe 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -76,6 +76,12 @@ public:
   /** Check the satisfiability of the added clauses */
   virtual SatValue solve(long unsigned int&) = 0;
 
+  /** Check satisfiability under assumptions */
+  virtual SatValue solve(const std::vector<SatLiteral>& assumptions)
+  {
+    Unimplemented("Solving under assumptions not implemented");
+  };
+
   /** Interrupt the solver */
   virtual void interrupt() = 0;