Cadical can be used for PC checks

Makefile

@@ -14,13 +14,13 @@ build:
 	mkdir build
 
 cmake: build
-	cd build && cmake -DCMAKE_BUILD_TYPE=Release -DUSE_KISSAT=$(USE_KISSAT) ..
+	cd build && cmake -DCMAKE_BUILD_TYPE=Release -DUSE_KISSAT=$(USE_KISSAT) -DUSE_CADICAL=$(USE_CADICAL) ..
 
 cmake_debug: build
-	cd build && cmake -DCMAKE_BUILD_TYPE=Debug -DUSE_KISSAT=$(USE_KISSAT) ..
+	cd build && cmake -DCMAKE_BUILD_TYPE=Debug -DUSE_KISSAT=$(USE_KISSAT) -DUSE_CADICAL=$(USE_CADICAL) ..
 
 cmake_static: build
-	cd build && cmake -DBUILD_STATIC=ON -DCMAKE_BUILD_TYPE=Release -DUSE_KISSAT=$(USE_KISSAT) ..
+	cd build && cmake -DBUILD_STATIC=ON -DCMAKE_BUILD_TYPE=Release -DUSE_KISSAT=$(USE_KISSAT) -DUSE_CADICAL=$(USE_CADICAL) ..
 
 cmake_subool_glucose: build
-	cd build && cmake -DBUILD_SUBOOL_GLUCOSE=ON -DCMAKE_BUILD_TYPE=Release -DUSE_KISSAT=$(USE_KISSAT) ..
+	cd build && cmake -DBUILD_SUBOOL_GLUCOSE=ON -DCMAKE_BUILD_TYPE=Release -DUSE_KISSAT=$(USE_KISSAT) -DUSE_CADICAL=$(USE_CADICAL) ..

bin/CMakeLists.txt

 cmake_minimum_required (VERSION 3.0.2)
 
-function(su_add_exec_x name use_glucose use_kissat)
+function(su_add_exec_x name use_inc_solver use_kissat)
    set(ATE_LIBS subool)
-   if (${use_glucose})
+   if (${use_inc_solver})
       su_add_glucose_lib(ATE_LIBS)
+      su_add_cadical_lib(ATE_LIBS)
    endif()
    if (${use_kissat})
       su_add_kissat_lib(ATE_LIBS)

lib/pcchecker.cpp

@@ -79,9 +79,9 @@ SUBool::AbsCheckerSAT::FindEmpoweringWithLevel(const CNF &cnf,
    logs.TLog(3) << "[AbsCheckerSAT::FindEmpoweringWithLevel] level="
                 << (level == 0 ? mMaxUPLevel : level) << ", input cnf "
                 << cnf.MaxVariable() << " " << cnf.Size() << std::endl;
-   auto wrap = solver_wrapper(
-       mSolverType, assume_sat ? SolverInterface::ADAPTATION::LIKELY_SAT
-                               : SolverInterface::ADAPTATION::LIKELY_UNSAT);
+   auto wrap = solver_wrapper(mSolverType, false,
+       assume_sat ? SolverInterface::ADAPTATION::LIKELY_SAT
+                  : SolverInterface::ADAPTATION::LIKELY_UNSAT);
    auto &g = wrap.Solver();
    enc->PassToSolver(g);
    logs.TLog(3) << "... Calling SAT with encoding (p cnf " << enc->MaxVariable()

lib/solver_bind.cpp

@@ -6,6 +6,7 @@
  * Binding class to solver library. */
 
 #include "solver_bind.h"
+#include "cadical_bind.h"
 #include "glucose_bind.h"
 #include "kissat_bind.h"
 #include "util.h"
@@ -20,11 +21,24 @@ const SUBool::EnumAnnotation<SUBool::SOLVER_TYPE> SUBool::kSolverTypeAnnotation(
        {
           SOLVER_TYPE::GLUCOSE, "glucose", "use glucose."
        }
+#if HAS_CADICAL
+       , { SOLVER_TYPE::CADICAL, "cadical", "use cadical." }
+#endif
 #if HAS_KISSAT
        , { SOLVER_TYPE::KISSAT, "kissat", "use kissat." }
 #endif
     });
 
+const SUBool::EnumAnnotation<SUBool::INC_SOLVER_TYPE>
+    SUBool::kIncSolverTypeAnnotation("INC_SOLVER_TYPE", { //
+       {
+          INC_SOLVER_TYPE::GLUCOSE, "glucose", "use glucose."
+       }
+#if HAS_CADICAL
+       , { INC_SOLVER_TYPE::CADICAL, "cadical", "use cadical." }
+#endif
+    });
+
 bool
 SUBool::SolverInterface::AddClauses(const std::vector<Clause> &clauses)
 {
@@ -61,13 +75,20 @@ SUBool::SolverPool::InterruptInThread(std::thread::id thread_id)
 }
 
 SUBool::AbsSolverWrapper
-SUBool::solver_wrapper(
-    SOLVER_TYPE solver_type, SolverInterface::ADAPTATION adapt)
+SUBool::solver_wrapper(SOLVER_TYPE solver_type,
+    bool collect_learnts [[maybe_unused]], SolverInterface::ADAPTATION adapt)
 {
    switch (solver_type)
    {
    case SOLVER_TYPE::GLUCOSE:
       return SimpSolverWrapper(adapt);
+   case SOLVER_TYPE::CADICAL:
+#if HAS_CADICAL
+      return CadicalWrapper(collect_learnts, adapt);
+#else
+      throw BadParameterException(
+          "AbsCheckerSAT::NewSolverWrapper", "Cadical support not available");
+#endif
    case SOLVER_TYPE::KISSAT:
 #if HAS_KISSAT
       return KissatSolverWrapper(adapt);

lib/solver_bind.h

@@ -227,13 +227,21 @@ namespace SUBool
    enum class SOLVER_TYPE
    {
       GLUCOSE,
+      CADICAL,
       KISSAT
    };
 
+   enum class INC_SOLVER_TYPE
+   {
+      GLUCOSE,
+      CADICAL
+   };
+
    extern const EnumAnnotation<SOLVER_TYPE> kSolverTypeAnnotation;
+   extern const EnumAnnotation<INC_SOLVER_TYPE> kIncSolverTypeAnnotation;
 
-   AbsSolverWrapper solver_wrapper(
-       SOLVER_TYPE solver_type, SolverInterface::ADAPTATION adapt);
+   AbsSolverWrapper solver_wrapper(SOLVER_TYPE solver_type,
+       bool collect_learnts, SolverInterface::ADAPTATION adapt);
 
    template <class S> class SolverWrapperTemplate : public AbsSolverWrapper
    {