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 sr19 and
fix the use of the cnf_solvert interface.

Author: tautschnig

CMakeLists.txt

@@ -33,7 +33,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})

jbmc/lib/java-models-library

@@ -149,13 +149,12 @@ glucose-download:
 	@(cd ../glucose-syrup; patch -p1 < ../scripts/glucose-syrup-patch)
 	@rm glucose-syrup.tgz
 
-cadical_release = rel-06w
+cadical_release = sr19
 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 :

scripts/cadical-patch

@@ -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/sr19.tar.gz
+        PATCH_COMMAND true
+        COMMAND CXX=${CXX_COMPILER} CXXFLAGS=-O3 ./configure --debug
+        URL_MD5 dd9b7c7b88aa769985993e33fbfdfb35
+    )
+
+    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/Makefile

@@ -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());
@@ -79,6 +79,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 +122,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 +135,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/CMakeLists.txt

@@ -20,7 +20,7 @@ namespace CaDiCaL // NOLINT(readability/namespace)
 class satcheck_cadicalt:public cnf_solvert
 {
 public:
-  satcheck_cadicalt();
+  explicit satcheck_cadicalt(message_handlert &message_handler);
   virtual ~satcheck_cadicalt();
 
   const std::string solver_text() override;
@@ -32,11 +32,11 @@ 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;
 
@@ -45,6 +45,8 @@ class satcheck_cadicalt:public cnf_solvert
 
   // NOLINTNEXTLINE(readability/identifiers)
   CaDiCaL::Solver * solver;
+
+  bvt assumptions;
 };
 
 #endif // CPROVER_SOLVERS_SAT_SATCHECK_CADICAL_H

src/solvers/sat/satcheck_cadical.cpp

@@ -45,6 +45,7 @@ SRC += analyses/ai/ai.cpp \
        solvers/floatbv/float_utils.cpp \
        solvers/lowering/byte_operators.cpp \
        solvers/prop/bdd_expr.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 \