Support for incremental bit-blasting with CaDiCaL (#3006)

This commit adds support for eager bit-blasting with CaDiCaL on
incremental benchmarks. Since not all CaDiCaL versions support
incremental solving, the commit adds a CMake check that checks whether
`CaDiCaL::Solver::assume()` exists.

Note: The check uses `check_cxx_source_compiles`, which is not very
elegant but I could not find a better solution (e.g.
`check_cxx_symbol_exists()` does not seem to support methods in classes
and `check_struct_has_member()` only seems to support data members).

3 files changed, 24 insertions, 5 deletions

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 2a59ace11..5e98f8f5a 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -1175,14 +1175,16 @@ theory::bv::SatSolverMode OptionsHandler::stringToSatSolver(std::string option,
   }
   else if (optarg == "cadical")
   {
+#ifndef CVC4_INCREMENTAL_CADICAL
     if (options::incrementalSolving()
         && options::incrementalSolving.wasSetByUser())
     {
-      throw OptionException(
-          std::string("CaDiCaL does not support incremental mode. \n\
-                         Try --bv-sat-solver=cryptominisat or "
-                      "--bv-sat-solver=minisat"));
+      throw OptionException(std::string(
+          "CaDiCaL version used does not support incremental mode. \n\
+                       Update CaDiCal or Try --bv-sat-solver=cryptominisat or "
+          "--bv-sat-solver=minisat"));
     }
+#endif
 
     if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY
         && options::bitblastMode.wasSetByUser())
diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp
index 5a0968ec8..b4851f945 100644
--- a/src/prop/cadical.cpp
+++ b/src/prop/cadical.cpp
@@ -117,6 +117,23 @@ SatValue CadicalSolver::solve(long unsigned int&)
   Unimplemented("Setting limits for CaDiCaL not supported yet");
 };
 
+SatValue CadicalSolver::solve(const std::vector<SatLiteral>& assumptions)
+{
+#ifdef CVC4_INCREMENTAL_CADICAL
+  TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime);
+  for (const SatLiteral& lit : assumptions)
+  {
+    d_solver->assume(toCadicalLit(lit));
+  }
+  SatValue res = toSatValue(d_solver->solve());
+  d_okay = (res == SAT_VALUE_TRUE);
+  ++d_statistics.d_numSatCalls;
+  return res;
+#else
+  Unimplemented("CaDiCaL version used does not support incremental solving");
+#endif
+}
+
 void CadicalSolver::interrupt() { d_solver->terminate(); }
 
 SatValue CadicalSolver::value(SatLiteral l)
diff --git a/src/prop/cadical.h b/src/prop/cadical.h
index e43a2d278..6ab0c2850 100644
--- a/src/prop/cadical.h
+++ b/src/prop/cadical.h
@@ -48,8 +48,8 @@ class CadicalSolver : public SatSolver
   SatVariable falseVar() override;
 
   SatValue solve() override;
-
   SatValue solve(long unsigned int&) override;
+  SatValue solve(const std::vector<SatLiteral>& assumptions) override;
 
   void interrupt() override;