Merge pull request #4758 from tautschnig/cadical

Add CaDiCaL support to CMake

Author: tautschnig

.github/workflows/pull-request-checks.yaml

@@ -332,7 +332,7 @@ jobs:
         run: |
           mkdir build
           cd build
-          cmake .. -G Ninja -DCMAKE_BUILD_TYPE=Release
+          cmake .. -G Ninja -DCMAKE_BUILD_TYPE=Release -Dsat_impl=cadical
       - name: Build using Ninja
         run: |
           cd build

CMakeLists.txt

@@ -65,7 +65,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

@@ -152,15 +152,14 @@ 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)"
 	@$(DOWNLOADER) https://github.com/arminbiere/cadical/archive/$(cadical_release).tar.gz
 	@$(TAR) xfz $(cadical_release).tar.gz
 	@rm -Rf ../cadical
 	@mv cadical-$(cadical_release) ../cadical
-	@(cd ../cadical; patch -p1 < ../scripts/cadical-patch)
-	@cd ../cadical && CXX=$(CXX) CXXFLAGS=-O3 ./configure --debug && make
+	@cd ../cadical && CXX=$(CXX) ./configure -O3 -s -j && make
 	@$(RM) $(cadical_release).tar.gz
 
 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} ./configure -O3 -s -j
+        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

@@ -123,6 +123,10 @@ void bv_refinementt::check_SAT()
 
   arrays_overapproximated();
 
+  // get values before modifying the formula
+  for(approximationt &approximation : this->approximations)
+    get_values(approximation);
+
   for(approximationt &approximation : this->approximations)
     check_SAT(approximation);
 }

src/solvers/refinement/bv_refinement_loop.cpp

@@ -158,9 +158,6 @@ void bv_refinementt::get_values(approximationt &a)
 /// refine overapproximation
 void bv_refinementt::check_SAT(approximationt &a)
 {
-  // get values
-  get_values(a);
-
   // see if the satisfying assignment is spurious in any way
 
   const typet &type = a.expr.type();

src/solvers/refinement/refine_arithmetic.cpp

@@ -10,6 +10,7 @@ Author: Michael Tautschnig
 
 #include <util/exception_utils.h>
 #include <util/invariant.h>
+#include <util/narrow.h>
 #include <util/threeval.h>
 
 #ifdef HAVE_CADICAL
@@ -23,7 +24,7 @@ tvt satcheck_cadicalt::l_get(literalt a) const
 
   tvt result;
 
-  if(a.var_no() > static_cast<unsigned>(solver->max()))
+  if(a.var_no() > narrow<unsigned>(solver->vars()))
     return tvt(tvt::tv_enumt::TV_UNKNOWN);
 
   const int val = solver->val(a.dimacs());
@@ -62,6 +63,23 @@ void satcheck_cadicalt::lcnf(const bvt &bv)
   }
   solver->add(0); // terminate clause
 
+  with_solver_hardness([this, &bv](solver_hardnesst &hardness) {
+    // To map clauses to lines of program code, track clause indices in the
+    // dimacs cnf output. Dimacs output is generated after processing
+    // clauses to remove duplicates and clauses that are trivially true.
+    // Here, a clause is checked to see if it can be thus eliminated. If
+    // not, add the clause index to list of clauses in
+    // solver_hardnesst::register_clause().
+    static size_t cnf_clause_index = 0;
+    bvt cnf;
+    bool clause_removed = process_clause(bv, cnf);
+
+    if(!clause_removed)
+      cnf_clause_index++;
+
+    hardness.register_clause(bv, cnf, cnf_clause_index, !clause_removed);
+  });
+
   clause_counter++;
 }
 
@@ -72,31 +90,37 @@ propt::resultt satcheck_cadicalt::do_prop_solve()
   log.statistics() << (no_variables() - 1) << " variables, " << clause_counter
                    << " clauses" << messaget::eom;
 
-  if(status == statust::UNSAT)
+  // if assumptions contains false, we need this to be UNSAT
+  for(const auto &a : assumptions)
   {
-    log.status() << "SAT checker inconsistent: instance is UNSATISFIABLE"
-                 << messaget::eom;
-  }
-  else
-  {
-    switch(solver->solve())
+    if(a.is_false())
     {
-      case 10:
-        log.status() << "SAT checker: instance is SATISFIABLE" << messaget::eom;
-        status = statust::SAT;
-        return resultt::P_SATISFIABLE;
-      case 20:
-        log.status() << "SAT checker: instance is UNSATISFIABLE"
-                     << messaget::eom;
-        break;
-      default:
-        log.status() << "SAT checker: solving returned without solution"
-                     << messaget::eom;
-        throw analysis_exceptiont(
-          "solving inside CaDiCaL SAT solver has been interrupted");
+      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:
+    log.status() << "SAT checker: instance is SATISFIABLE" << messaget::eom;
+    status = statust::SAT;
+    return resultt::P_SATISFIABLE;
+  case 20:
+    log.status() << "SAT checker: instance is UNSATISFIABLE" << messaget::eom;
+    break;
+  default:
+    log.status() << "SAT checker: solving returned without solution"
+                 << messaget::eom;
+    throw analysis_exceptiont(
+      "solving inside CaDiCaL SAT solver has been interrupted");
+  }
+
   status = statust::UNSAT;
   return resultt::P_UNSATISFIABLE;
 }
@@ -107,8 +131,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 +144,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

@@ -69,6 +69,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 \
@@ -228,6 +229,9 @@ endif
 ifeq ($(MINISAT2),)
 EXCLUDED_TESTS += satcheck_minisat2.cpp
 endif
+ifeq ($(CADICAL),)
+EXCLUDED_TESTS += satcheck_cadical.cpp
+endif
 
 N_CATCH_TESTS = $(shell \
                   cat $$(find . -name "*.cpp" \