From 521701398b15bd41a1cb8a9b530fc4af4892c7af Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 17 May 2019 19:16:55 -0700
Subject: [PATCH] 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).
---
 cmake/ConfigureCVC4.cmake                  | 14 ++++++++++++++
 contrib/run-script-smtcomp2019-application |  2 +-
 src/options/options_handler.cpp            | 10 ++++++----
 src/prop/cadical.cpp                       | 17 +++++++++++++++++
 src/prop/cadical.h                         |  2 +-
 5 files changed, 39 insertions(+), 6 deletions(-)

diff --git a/cmake/ConfigureCVC4.cmake b/cmake/ConfigureCVC4.cmake
index 67c1f414d..cdf8e4d9a 100644
--- 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 58db84d36..a7d4d985c 100755
--- 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 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;
 
-- 
2.30.2