Add CaDiCaL support to CMake

Add CMake configuration to build using CaDiCaL, which was already
supported with Makefiles. Also bump the version of CaDiCaL to rel-1.3.0
and fix the use of the cnf_solvert interface.

Author: tautschnig

CMakeLists.txt

@@ -58,7 +58,8 @@ endif()
 set(enable_cbmc_tests on CACHE BOOL "Whether CBMC tests should be enabled")
 
 set(sat_impl "minisat2" CACHE STRING
-    "This setting controls the SAT library which is used. Valid values are 'minisat2' and 'glucose'"
+    "This setting controls the SAT library which is used. Valid values are
+    'minisat2', 'glucose', or 'cadical'"
 )
 
 if(${enable_cbmc_tests})

scripts/cadical-patch

@@ -151,13 +151,12 @@ glucose-download:
 	@(cd ../glucose-syrup; patch -p1 < ../scripts/glucose-syrup-patch)
 	@rm glucose-syrup.tgz
 
-cadical_release = rel-06w
+cadical_release = rel-1.3.0
 cadical-download:
 	@echo "Downloading CaDiCaL $(cadical_release)"
 	@curl -L https://github.com/arminbiere/cadical/archive/$(cadical_release).tar.gz | tar xz
 	@rm -Rf ../cadical
 	@mv cadical-$(cadical_release) ../cadical
-	@(cd ../cadical; patch -p1 < ../scripts/cadical-patch)
 	@cd ../cadical && CXX=$(CXX) CXXFLAGS=-O3 ./configure --debug && make
 
 doc :

src/Makefile

@@ -98,6 +98,36 @@ elseif("${sat_impl}" STREQUAL "glucose")
     target_sources(solvers PRIVATE ${glucose_source})
 
     target_link_libraries(solvers glucose-condensed)
+elseif("${sat_impl}" STREQUAL "cadical")
+    message(STATUS "Building solvers with cadical")
+
+    download_project(PROJ cadical
+        URL https://github.com/arminbiere/cadical/archive/rel-1.3.0.tar.gz
+        PATCH_COMMAND true
+        COMMAND CXX=${CMAKE_CXX_COMPILER} CXXFLAGS=-O3 ./configure --debug
+        URL_MD5 5bd15d1e198d2e904a8af8b7873dd341
+    )
+
+    message(STATUS "Building CaDiCaL")
+    execute_process(COMMAND make WORKING_DIRECTORY ${cadical_SOURCE_DIR})
+
+    target_compile_definitions(solvers PUBLIC
+        SATCHECK_CADICAL HAVE_CADICAL
+    )
+
+    add_library(cadical STATIC IMPORTED)
+
+    set_target_properties(
+        cadical
+        PROPERTIES IMPORTED_LOCATION ${cadical_SOURCE_DIR}/build/libcadical.a
+    )
+
+    target_include_directories(solvers
+      PUBLIC
+      ${cadical_SOURCE_DIR}/src
+    )
+
+    target_link_libraries(solvers cadical)
 endif()
 
 if(CMAKE_USE_CUDD)

src/solvers/CMakeLists.txt

@@ -23,7 +23,7 @@ tvt satcheck_cadicalt::l_get(literalt a) const
 
   tvt result;
 
-  if(a.var_no() > static_cast<unsigned>(solver->max()))
+  if(a.var_no() > static_cast<unsigned>(solver->vars()))
     return tvt(tvt::tv_enumt::TV_UNKNOWN);
 
   const int val = solver->val(a.dimacs());
@@ -62,6 +62,9 @@ void satcheck_cadicalt::lcnf(const bvt &bv)
   }
   solver->add(0); // terminate clause
 
+  with_solver_hardness(
+    [&bv](solver_hardnesst &hardness) { hardness.register_clause(bv); });
+
   clause_counter++;
 }
 
@@ -79,6 +82,21 @@ propt::resultt satcheck_cadicalt::do_prop_solve()
   }
   else
   {
+    // if assumptions contains false, we need this to be UNSAT
+    for(const auto &a : assumptions)
+    {
+      if(a.is_false())
+      {
+        log.status() << "got FALSE as assumption: instance is UNSATISFIABLE"
+                     << messaget::eom;
+        status = statust::UNSAT;
+        return resultt::P_UNSATISFIABLE;
+      }
+    }
+
+    for(const auto &a : assumptions)
+      solver->assume(a.dimacs());
+
     switch(solver->solve())
     {
       case 10:
@@ -107,8 +125,8 @@ void satcheck_cadicalt::set_assignment(literalt a, bool value)
   INVARIANT(false, "method not supported");
 }
 
-satcheck_cadicalt::satcheck_cadicalt() :
-  solver(new CaDiCaL::Solver())
+satcheck_cadicalt::satcheck_cadicalt(message_handlert &message_handler)
+  : cnf_solvert(message_handler), solver(new CaDiCaL::Solver())
 {
   solver->set("quiet", 1);
 }
@@ -120,13 +138,20 @@ satcheck_cadicalt::~satcheck_cadicalt()
 
 void satcheck_cadicalt::set_assumptions(const bvt &bv)
 {
-  INVARIANT(false, "method not supported");
+  // We filter out 'true' assumptions which cause spurious results with CaDiCaL.
+  assumptions.clear();
+  for(const auto &assumption : bv)
+  {
+    if(!assumption.is_true())
+    {
+      assumptions.push_back(assumption);
+    }
+  }
 }
 
 bool satcheck_cadicalt::is_in_conflict(literalt a) const
 {
-  INVARIANT(false, "method not supported");
-  return false;
+  return solver->failed(a.dimacs());
 }
 
 #endif

src/solvers/sat/satcheck_cadical.cpp

@@ -12,15 +12,17 @@ Author: Michael Tautschnig
 
 #include "cnf.h"
 
+#include <solvers/hardness_collector.h>
+
 namespace CaDiCaL // NOLINT(readability/namespace)
 {
   class Solver; // NOLINT(readability/identifiers)
 }
 
-class satcheck_cadicalt:public cnf_solvert
+class satcheck_cadicalt : public cnf_solvert, public hardness_collectort
 {
 public:
-  satcheck_cadicalt();
+  explicit satcheck_cadicalt(message_handlert &message_handler);
   virtual ~satcheck_cadicalt();
 
   const std::string solver_text() override;
@@ -32,19 +34,37 @@ class satcheck_cadicalt:public cnf_solvert
   void set_assumptions(const bvt &_assumptions) override;
   bool has_set_assumptions() const override
   {
-    return false;
+    return true;
   }
   bool has_is_in_conflict() const override
   {
-    return false;
+    return true;
   }
   bool is_in_conflict(literalt a) const override;
 
+  void
+  with_solver_hardness(std::function<void(solver_hardnesst &)> handler) override
+  {
+    if(solver_hardness.has_value())
+    {
+      handler(solver_hardness.value());
+    }
+  }
+
+  void enable_hardness_collection() override
+  {
+    solver_hardness = solver_hardnesst{};
+  }
+
 protected:
   resultt do_prop_solve() override;
 
   // NOLINTNEXTLINE(readability/identifiers)
   CaDiCaL::Solver * solver;
+
+  bvt assumptions;
+
+  optionalt<solver_hardnesst> solver_hardness;
 };
 
 #endif // CPROVER_SOLVERS_SAT_SATCHECK_CADICAL_H

src/solvers/sat/satcheck_cadical.h

@@ -59,6 +59,7 @@ SRC += analyses/ai/ai.cpp \
        solvers/lowering/byte_operators.cpp \
        solvers/prop/bdd_expr.cpp \
        solvers/sat/external_sat.cpp \
+       solvers/sat/satcheck_cadical.cpp \
        solvers/sat/satcheck_minisat2.cpp \
        solvers/strings/array_pool/array_pool.cpp \
        solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp \