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).

1 files changed, 17 insertions, 0 deletions

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)