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

diff --git a/cmake/ConfigureCVC4.cmake b/cmake/ConfigureCVC4.cmake
index 67c1f414d0a1478f651de247d1970fdb277c8ac0..cdf8e4d9a7efde1f1683ccaa419671b7c7025d6b 100644 (file)
--- a/cmake/ConfigureCVC4.cmake
+++ b/cmake/ConfigureCVC4.cmake
@@ -67,6 +67,20 @@ check_symbol_exists(sigaltstack "signal.h" HAVE_SIGALTSTACK)
 check_symbol_exists(strerror_r "string.h" HAVE_STRERROR_R)
 check_symbol_exists(strtok_r "string.h" HAVE_STRTOK_R)
 
+# Check whether the verison of CaDiCaL used supports incremental solving
+if(USE_CADICAL)
+  check_cxx_source_compiles(
+    "
+    #include <${CaDiCaL_HOME}/src/cadical.hpp>
+    int main() { return sizeof(&CaDiCaL::Solver::assume); }
+    "
+    CVC4_INCREMENTAL_CADICAL
+  )
+  if(CVC4_INCREMENTAL_CADICAL)
+    add_definitions(-DCVC4_INCREMENTAL_CADICAL)
+  endif()
+endif()
+
 # Determine if we have the POSIX (int) or GNU (char *) variant of strerror_r.
 check_c_source_compiles(
   "

diff --git a/contrib/run-script-smtcomp2019-application b/contrib/run-script-smtcomp2019-application
index 58db84d36cbc96d94767a18db7fc919fa5771d0f..a7d4d985c66c3836d8860a55d3813c90152634ae 100755 (executable)
--- a/contrib/run-script-smtcomp2019-application
+++ b/contrib/run-script-smtcomp2019-application
@@ -44,7 +44,7 @@ QF_AUFLIA)
   runcvc4 --no-arrays-eager-index --arrays-eager-lemmas --incremental
   ;;
 QF_BV)
-  runcvc4 --tear-down-incremental=4 --bv-eq-slicer=auto --bv-div-zero-const --bv-intro-pow2
+  runcvc4 --incremental --bitblast=eager --bv-sat-solver=cadical
   ;;
 QF_LIA)
   runcvc4 --tear-down-incremental=1 --unconstrained-simp

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 2a59ace11cbb2f1ef1258228f3796107107d699d..5e98f8f5ab346eb1f3fc6a59828f701c2401ffb1 100644 (file)
--- 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 5a0968ec8503ecaf8ced53c3e7188a01a39186ae..b4851f945e6a33bd4833fdce298b22fada9c6050 100644 (file)
--- 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 e43a2d278a4c6c3c098887f7faaf196d7b0896fc..6ab0c2850012f00c8b03c08f8d08a3bcd1dc3ab7 100644 (file)
--- 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;