Merge branch 'feature'

CMakeLists.txt

@@ -39,22 +39,37 @@ endfunction(su_add_pthread)
 find_package(Boost 1.64.0 COMPONENTS program_options REQUIRED)
 
 # Glucose related part
-if(DEFINED ENV{GLUCOSE_HOME})
-   set (GLUCOSE_HOME $ENV{GLUCOSE_HOME})
-   message(STATUS "Using GLUCOSE_HOME=${GLUCOSE_HOME}")
+option(USE_GLUCOSE "If the project should compile with glucose support" ON)
+if(USE_GLUCOSE)
+   if(DEFINED ENV{GLUCOSE_HOME})
+      set (GLUCOSE_HOME $ENV{GLUCOSE_HOME})
+      message(STATUS "Using GLUCOSE_HOME=${GLUCOSE_HOME}")
+   else()
+      set (GLUCOSE_HOME ${SUBool_SOURCE_DIR}/solvers/glucose)
+      message(STATUS "GLUCOSE_HOME not defined, using default GLUCOSE_HOME=${GLUCOSE_HOME}")
+   endif()
+   # find_library(GLUCOSE_LIB glucose_debug /usr/local/glucose/simp)
+   # find_library(GLUCOSE_LIB glucose_release /usr/local/glucose/simp)
+   find_library(GLUCOSE_LIB _release PATHS ${GLUCOSE_HOME}/simp NO_SYSTEM_ENVIRONMENT_PATH NO_DEFAULT_PATH)
+   if(GLUCOSE_LIB)
+      message(STATUS "Using GLUCOSE_LIB=${GLUCOSE_LIB}")
+      include_directories (SYSTEM ${GLUCOSE_HOME})
+      add_compile_definitions(HAS_GLUCOSE=1)
+   else()
+      message(WARNING "Glucose lib not found, glucose support is switched off")
+      set(GLUCOSE_LIB "")
+      set(USE_GLUCOSE OFF)
+   endif()
 else()
-   set (GLUCOSE_HOME ${SUBool_SOURCE_DIR}/solvers/glucose)
-   message(STATUS "GLUCOSE_HOME not defined, using default GLUCOSE_HOME=${GLUCOSE_HOME}")
+   message(STATUS "Glucose support will not be available")
 endif()
-# find_library(GLUCOSE_LIB glucose_debug /usr/local/glucose/simp)
-# find_library(GLUCOSE_LIB glucose_release /usr/local/glucose/simp)
-find_library(GLUCOSE_LIB _release ${GLUCOSE_HOME}/simp)
-message(STATUS "Using GLUCOSE_LIB: ${GLUCOSE_LIB}")
-# END of Glusoce related part
 
 function(su_add_glucose_lib libs)
-   set(${libs} ${${libs}} ${GLUCOSE_LIB} PARENT_SCOPE)
+   if(USE_GLUCOSE)
+      set(${libs} ${${libs}} ${GLUCOSE_LIB} PARENT_SCOPE)
+   endif()
 endfunction(su_add_glucose_lib)
+# END of Glusoce related part
 
 # KISSAT related part
 option(USE_KISSAT "If the project should compile with kissat support" ON)
@@ -66,9 +81,9 @@ if(USE_KISSAT)
       set (KISSAT_HOME ${SUBool_SOURCE_DIR}/solvers/kissat)
       message(STATUS "KISSAT_HOME not defined, using default KISSAT_HOME=${KISSAT_HOME}")
    endif()
-   find_library(KISSAT_LIB kissat ${KISSAT_HOME}/build)
+   find_library(KISSAT_LIB kissat PATHS ${KISSAT_HOME}/build NO_SYSTEM_ENVIRONMENT_PATH NO_DEFAULT_PATH)
    if(KISSAT_LIB)
-      message(STATUS "Using KISSAT_LIB: ${KISSAT_LIB}")
+      message(STATUS "Using KISSAT_LIB=${KISSAT_LIB}")
       add_compile_definitions(KISSAT_INTERNAL_H="${KISSAT_HOME}/src/internal.h")
       add_compile_definitions(KISSAT_KISSAT_H="${KISSAT_HOME}/src/kissat.h")
       add_compile_definitions(HAS_KISSAT=1)
@@ -88,9 +103,44 @@ function(su_add_kissat_lib libs)
 endfunction(su_add_kissat_lib)
 # END of KISSAT related part
 
+# CaDiCaL related part
+option(USE_CADICAL "If the project should compile with CaDiCaL support" ON)
+if(USE_CADICAL)
+   if(DEFINED ENV{CADICAL_HOME})
+      set (CADICAL_HOME $ENV{CADICAL_HOME})
+      message(STATUS "Using CADICAL_HOME=${CADICAL_HOME}")
+   else()
+      set (CADICAL_HOME ${SUBool_SOURCE_DIR}/solvers/cadical)
+      message(STATUS "CADICAL_HOME not defined, using default CADICAL_HOME=${CADICAL_HOME}")
+   endif()
+   find_library(CADICAL_LIB cadical PATHS ${CADICAL_HOME}/build NO_SYSTEM_ENVIRONMENT_PATH NO_DEFAULT_PATH)
+   if(CADICAL_LIB)
+      message(STATUS "Using CADICAL_LIB=${CADICAL_LIB}")
+      include_directories(SYSTEM "${CADICAL_HOME}/src")
+      add_compile_definitions(CADICAL_H="cadical.hpp")
+      add_compile_definitions(HAS_CADICAL=1)
+   else()
+      message(WARNING "CaDiCaL lib not found, CaDiCaL support is switched off")
+      set(CADICAL_LIB "")
+      set(USE_CADICAL OFF)
+   endif()
+else()
+   message(STATUS "CaDiCaL support will not be available")
+endif()
+
+function(su_add_cadical_lib libs)
+   if(USE_CADICAL)
+      set(${libs} ${${libs}} ${CADICAL_LIB} PARENT_SCOPE)
+   endif()
+endfunction(su_add_cadical_lib)
+# END of CADICAL related part
+
+if(NOT USE_GLUCOSE AND NOT USE_CADICAL)
+   message(FATAL_ERROR "At least one incremental solver (Glucose or CaDiCaL) must be available")
+endif()
+
 include_directories (BEFORE SYSTEM ${Boost_INCLUDE_DIRS})
 include_directories (${SUBool_SOURCE_DIR}/lib)
-include_directories (SYSTEM ${GLUCOSE_HOME})
 include_directories (/usr/local/include/)
 
 add_subdirectory (lib)

Makefile

+USE_GLUCOSE=ON
+USE_CADICAL=ON
 USE_KISSAT=ON
 
 all:
@@ -13,13 +15,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_GLUCOSE=$(USE_GLUCOSE) -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_GLUCOSE=$(USE_GLUCOSE) -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_GLUCOSE=$(USE_GLUCOSE) -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_GLUCOSE=$(USE_GLUCOSE) -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)
@@ -31,6 +32,7 @@ su_add_exec(cnfcanon true true)
 su_add_exec(cnfprime true true)
 su_add_exec(cnfcomp true true)
 su_add_exec(cnfdiff false false)
+su_add_exec(cnfsize false false)
 
 su_add_exec_x(cnfgraph false false cnfgraphx.cpp)
 

bin/cnfcanon.cpp

@@ -21,6 +21,7 @@
 #include "normalform.h"
 #include "prgutil.h"
 #include "sbexception.h"
+#include "solver_opt.h"
 
 const std::string SUBool::kPrgName = "cnfcanon";
 const std::string SUBool::kPrgDesc =
@@ -59,6 +60,7 @@ parse_arguments(int argc, char *argv[])
    std::string process;
    SUBool::PrgOptions opts;
    opts.InputOutput(&conf.input_file, &conf.output_file);
+   auto solver_opts = opts.MakeOptionsGroup<SUBool::SolverOptions>();
    po::options_description desc("Configuration options");
    desc.add(opt_process);
    opts.Add(desc);
@@ -72,6 +74,7 @@ parse_arguments(int argc, char *argv[])
 void
 config_t::InnerDump(unsigned level) const
 {
+   SUBool::SolverPool::DumpSolverTypes("\t", level);
    SUBool::logs.DumpValue("\t", level, "input_file", input_file);
    SUBool::logs.DumpValue("\t", level, "output_file", output_file);
    kProcessAnnotation.DumpValue("\t", level, "process", process);

bin/cnfprime.cpp

@@ -20,6 +20,7 @@
 #include "normalform.h"
 #include "prgutil.h"
 #include "sbexception.h"
+#include "solver_opt.h"
 
 const std::string SUBool::kPrgName = "cnfprime";
 const std::string SUBool::kPrgDesc = "Making a CNF prime";
@@ -31,6 +32,7 @@ struct config_t : public SUBool::PrgConfigBase
    std::string input_file{};
    std::string output_file{};
    bool unitprop{false};
+   unsigned progress_step{0};
 
    virtual void InnerDump(unsigned level) const override;
 };
@@ -42,12 +44,16 @@ parse_arguments(int argc, char *argv[])
    SUBool::PrgOptions opts;
    opts.SetHelpDesc(prg_help);
    opts.InputOutput(&conf.input_file, &conf.output_file);
+   auto solver_opts = opts.MakeOptionsGroup<SUBool::SolverOptions>();
    po::options_description desc("Configuration options");
    desc.add_options()("unitprop,u", po::bool_switch(&conf.unitprop),
        "Use only unit propagation instead of SAT. It means "
        "that the result is not necessarily prime, but it is prime with "
        "respect to 1-provability (although not fully as only one round of "
-       "prime subimplicate finding is performed");
+       "prime subimplicate finding is performed")("progress-step",
+       po::value(&conf.progress_step)->default_value(0),
+       "If positive, then report progress after this many clauses. Has no "
+       "effect with option -u.");
    opts.Add(desc);
    if (!opts.Parse(argc, argv, conf))
    {
@@ -59,9 +65,11 @@ parse_arguments(int argc, char *argv[])
 void
 config_t::InnerDump(unsigned level) const
 {
+   SUBool::SolverPool::DumpSolverTypes("\t", level);
    SUBool::logs.DumpValue("\t", level, "input_file", input_file);
    SUBool::logs.DumpValue("\t", level, "output_file", output_file);
    SUBool::logs.DumpValue("\t", level, "unitprop", unitprop);
+   SUBool::logs.DumpValue("\t", level, "progress_step", progress_step);
 }
 
 SUBool::CNF
@@ -73,7 +81,7 @@ process(const config_t &conf, SUBool::CNF input)
    }
    else
    {
-      return SUBool::prime_cnf(input);
+      return SUBool::prime_cnf(input, conf.progress_step);
    }
 }
 

bin/cnfsize.cpp

+/*
+ * Project SUBool
+ * Petr Kucera, 2022
+ */
+/**@file cnfsize.cpp
+ * Program for printing size statistics of CNF formulas.
+ */
+
+#include <string>
+#include <vector>
+
+#include "dimacs.h"
+#include "normalform.h"
+#include "prgutil.h"
+
+const std::string SUBool::kPrgName = "cnfsize";
+const std::string SUBool::kPrgDesc = "Determining the sizes of CNF formulas";
+
+struct config_t : public SUBool::PrgConfigBase
+{
+   std::vector<std::string> input_files{};
+   bool print_vars{false};
+   bool print_size{false};
+   bool print_length{false};
+   bool print_head{false};
+
+   virtual void InnerDump(unsigned level) const override;
+};
+
+void
+config_t::InnerDump(unsigned level) const
+{
+   SUBool::logs.TLog(level) << "input files:";
+   for (const auto &fname : input_files)
+   {
+      SUBool::logs.Log(level) << ' ' << fname;
+   }
+   SUBool::logs.Log(level) << '\n';
+   SUBool::logs.DumpValue("\t", level, "print_vars", print_vars);
+   SUBool::logs.DumpValue("\t", level, "print_size", print_size);
+   SUBool::logs.DumpValue("\t", level, "print_length", print_length);
+   SUBool::logs.DumpValue("\t", level, "print_head", print_head);
+}
+
+std::optional<config_t>
+parse_arguments(int argc, char *argv[])
+{
+   config_t conf;
+   SUBool::PrgOptions opts;
+   opts.SetMultipleInputs(&conf.input_files);
+   po::options_description desc("Configuration options");
+   desc.add_options() //
+       ("print-head,H", po::bool_switch(&conf.print_head),
+           "Print the header line") //
+       ("print-vars,n", po::bool_switch(&conf.print_vars),
+           "Print column with the number of variables (var)") //
+       ("print-size,m", po::bool_switch(&conf.print_size),
+           "Print column with the number of clauses (cls)") //
+       ("print-length,l", po::bool_switch(&conf.print_length),
+           "Print column with the length of the formula (len)");
+   opts.Add(desc);
+   if (!opts.Parse(argc, argv, conf))
+   {
+      return {};
+   }
+   if (!conf.print_vars && !conf.print_size && !conf.print_length)
+   {
+      conf.print_vars = conf.print_size = conf.print_length = true;
+   }
+   return conf;
+}
+
+int
+process_cnf(const config_t &conf [[maybe_unused]], const SUBool::CNF &cnf,
+    const std::string &fname)
+{
+   if (conf.print_vars)
+   {
+      std::cout << std::setw(8) << cnf.MaxVariable();
+   }
+   if (conf.print_size)
+   {
+      std::cout << std::setw(8) << cnf.Size();
+   }
+   if (conf.print_length)
+   {
+      std::cout << std::setw(8) << cnf.Length();
+   }
+   std::cout << ' ' << fname << '\n';
+   return 0;
+}
+
+int
+process_file(const config_t &conf, const std::string &fname)
+{
+   auto cnf = SUBool::input_or_die<SUBool::CNF>(fname);
+   return process_cnf(conf, cnf, fname);
+}
+
+void
+print_head(const config_t &conf)
+{
+   if (!conf.print_head)
+   {
+      return;
+   }
+   if (conf.print_vars)
+   {
+      std::cout << std::setw(8) << "var";
+   }
+   if (conf.print_size)
+   {
+      std::cout << std::setw(8) << "cls";
+   }
+   if (conf.print_length)
+   {
+      std::cout << std::setw(8) << "len";
+   }
+   std::cout << '\n';
+}
+
+int
+process(const config_t &conf)
+{
+   print_head(conf);
+   if (conf.input_files.empty())
+   {
+      return process_file(conf, "");
+   }
+   int retcode = 0;
+   for (const auto &fname : conf.input_files)
+   {
+      retcode = process_file(conf, fname);
+      if (retcode != 0)
+      {
+         break;
+      }
+   }
+   return retcode;
+}
+
+int
+main(int argc, char *argv[])
+{
+   auto conf = parse_arguments(argc, argv);
+   if (!conf)
+   {
+      return 1;
+   }
+   conf->Dump(SUBool::LogStream::kDumpShortConfigLevel);
+   return process(*conf);
+}

bin/dpelim.cpp

@@ -15,6 +15,7 @@
 #include "enum_opt.h"
 #include "logstream.h"
 #include "prgutil.h"
+#include "solver_opt.h"
 
 const std::string SUBool::kPrgName = "dpelim";
 const std::string SUBool::kPrgDesc = "DP elimination of variables";
@@ -55,6 +56,7 @@ struct config_t : public SUBool::PrgConfigBase
 void
 config_t::InnerDump(unsigned level) const
 {
+   SUBool::SolverPool::DumpSolverTypes("\t", level);
    SUBool::logs.DumpValue("\t", level, "input_file", input_file);
    SUBool::logs.DumpValue("\t", level, "output_file", output_file);
    SUBool::logs.DumpValue("\t", level, "max_input_var", max_input_var);
@@ -87,6 +89,7 @@ parse_arguments(int argc, char *argv[])
    opts.InputOutput(&conf.input_file, &conf.output_file);
    opts.SetHelpDesc(prg_help);
 
+   auto solver_opts = opts.MakeOptionsGroup<SUBool::SolverOptions>();
    auto elim_opts = opts.MakeOptionsGroup<SUBool::DPElimEliminationOptions>();
    auto clause_manip_opts =
        opts.MakeOptionsGroup<SUBool::DPElimClauseManipOptions>();

bin/nnfencode.cpp

@@ -17,6 +17,7 @@
 #include "enum_opt.h"
 #include "logstream.h"
 #include "prgutil.h"
+#include "solver_opt.h"
 
 const std::string SUBool::kPrgName = "nnfencode";
 const std::string SUBool::kPrgDesc =
@@ -70,6 +71,7 @@ struct config_t : public SUBool::PrgConfigBase
 void
 config_t::InnerDump(unsigned level) const
 {
+   SUBool::SolverPool::DumpSolverTypes("\t", level);
    SUBool::logs.DumpValue("\t", level, "input_file", input_file);
    SUBool::logs.DumpValue("\t", level, "output_file", output_file);
    kEncodingTypeAnnotation.DumpValue(
@@ -105,6 +107,7 @@ parse_arguments(int argc, char *argv[])
    SUBool::PrgOptions opts(true);
    opts.SetHelpDesc(kPrgHelp);
    opts.InputOutput(&conf.input_file, &conf.output_file);
+   auto solver_opts = opts.MakeOptionsGroup<SUBool::SolverOptions>();
    po::options_description desc("Encoding construction");
    desc.add(opt_encoding_type);
    desc.add(opt_level_func);

bin/pccheck.cpp

@@ -28,6 +28,7 @@
 #include "prgutil.h"
 #include "random_utils.h"
 #include "resolve.h"
+#include "solver_opt.h"
 #include "uccomp.h"
 #include "ucenc.h"
 #include "unitprop.h"
@@ -52,7 +53,6 @@ struct config_t : public SUBool::PrgConfigBase
        SUBool::PCCheckGeneralOptions::kDefaultGoal};
    SUBool::AmoEncoder::KIND amo_encoding{SUBool::AmoEncoder::KIND::REPR};
    SUBool::ExOneEncoder::KIND exone_encoding{SUBool::ExOneEncoder::KIND::REPR};
-   SUBool::SOLVER_TYPE solver_type{SUBool::SOLVER_TYPE::GLUCOSE};
 
    virtual void InnerDump(unsigned level) const override;
 };
@@ -60,6 +60,7 @@ struct config_t : public SUBool::PrgConfigBase
 void
 config_t::InnerDump(unsigned level) const
 {
+   SUBool::SolverPool::DumpSolverTypes("\t", level);
    SUBool::logs.DumpValue("\t", level, "input_file", input_file);
    SUBool::PCCheckGeneralOptions::kGoalAnnotation.DumpValue(
        "\t", level, "goal", goal);
@@ -82,8 +83,6 @@ config_t::InnerDump(unsigned level) const
        "\t", level, "amo_encoding", amo_encoding);
    SUBool::ExOneEncoder::kKindAnnotation.DumpValue(
        "\t", level, "exone_encoding", exone_encoding);
-   SUBool::kSolverTypeAnnotation.DumpValue(
-       "\t", level, "solver_type", solver_type);
 }
 
 std::optional<config_t>
@@ -94,7 +93,7 @@ parse_arguments(int argc, char *argv[])
    opts.SetHelpDesc(prg_help);
    opts.SinglePositional({&conf.input_file, "input"});
    auto general_opts = opts.MakeOptionsGroup<SUBool::PCCheckGeneralOptions>();
-   auto solver_opts = opts.MakeOptionsGroup<SUBool::PCSolverOptions>();
+   auto solver_opts = opts.MakeOptionsGroup<SUBool::SolverOptions>();
    auto oneprove_opts = opts.MakeOptionsGroup<SUBool::PCOneProveOptions>(false);
    auto timeout_opts = opts.MakeOptionsGroup<SUBool::PCTimeoutsOptions>(false);
    auto cardinal_opt_group =
@@ -112,7 +111,6 @@ parse_arguments(int argc, char *argv[])
    conf.enc_conf.use_backmap = general_opts->Dump();
    conf.no_up_backbones = general_opts->NoUPBackbones();
    conf.initial_up_level = general_opts->InitialUPLevel();
-   conf.solver_type = solver_opts->SolverType();
    conf.enc_conf.up_one_prove = oneprove_opts->OneProve();
    conf.enc_conf.up_level_bound = oneprove_opts->UPLevelBound();
    conf.enc_conf.log_conf = oneprove_opts->EncLogarithmicConf();
@@ -204,7 +202,6 @@ pc_checker_sat(const config_t &conf)
    auto checker = std::make_unique<SUBool::PCCheckerSAT>();
    SUBool::PCEncoder::Config check_conf(conf.enc_conf);
    checker->Init(check_conf, false, conf.timeouts, conf.initial_up_level);
-   checker->SetSolverType(conf.solver_type);
    return checker;
 }
 
@@ -213,7 +210,6 @@ urc_checker_sat(const config_t &conf)
 {
    auto checker = std::make_unique<SUBool::UCCheckerSAT>();
    checker->Init(conf.enc_conf, false, conf.timeouts);
-   checker->SetSolverType(conf.solver_type);
    return checker;
 }
 

bin/pccompile.cpp

@@ -27,6 +27,7 @@
 #include "prgutil.h"
 #include "random_utils.h"
 #include "resolve.h"
+#include "solver_opt.h"
 #include "uccomp.h"
 #include "ucenc.h"
 #include "unitprop.h"
@@ -72,6 +73,7 @@ config_t the_conf;
 void
 config_t::InnerDump(unsigned level) const
 {
+   SUBool::SolverPool::DumpSolverTypes("\t", level);
    SUBool::logs.DumpValue("\t", level, "input_file", input_file);
    SUBool::logs.DumpValue("\t", level, "output_file", output_file);
    SUBool::logs.DumpValue("\t", level, "minimize", minimize);
@@ -116,8 +118,6 @@ config_t::InnerDump(unsigned level) const
        comp_base_config.timeouts.level_base);
    SUBool::logs.DumpValue("\t", level, "comp_base_config.timeouts.level_factor",
        comp_base_config.timeouts.level_factor);
-   SUBool::kSolverTypeAnnotation.DumpValue("\t", level,
-       "comp_base_config.solver_type", comp_base_config.solver_type);
    SUBool::logs.TLog(level) << "\tenc_conf:" << std::endl;
    comp_base_config.enc_conf.Dump("\t\t", level);
    SUBool::AmoEncoder::kKindAnnotation.DumpValue(
@@ -137,7 +137,7 @@ parse_arguments(int argc, char *argv[], config_t &conf)
    auto pclearncomp_opts = opts.MakeOptionsGroup<SUBool::PCLearnCompOptions>();
    auto preprocess_opts =
        opts.MakeOptionsGroup<SUBool::PCCompPreprocessOptions>();
-   auto solver_opts = opts.MakeOptionsGroup<SUBool::PCSolverOptions>();
+   auto solver_opts = opts.MakeOptionsGroup<SUBool::SolverOptions>();
    auto oneprove_opts = opts.MakeOptionsGroup<SUBool::PCOneProveOptions>(true);
    auto pccheck_random_opts =
        opts.MakeOptionsGroup<SUBool::PCRandomPCChecksOptions>();
@@ -158,7 +158,6 @@ parse_arguments(int argc, char *argv[], config_t &conf)
    conf.comp_base_config.preprocess = preprocess_opts->PreprocessMethod();
    conf.comp_base_config.propagate_backbones =
        !preprocess_opts->NoBackbonePropagation();
-   conf.comp_base_config.solver_type = solver_opts->SolverType();
    conf.comp_base_config.enc_conf.up_one_prove = oneprove_opts->OneProve();
    conf.comp_base_config.enc_conf.up_level_bound =
        oneprove_opts->UPLevelBound();

lib/CMakeLists.txt

 cmake_minimum_required (VERSION 3.0.2)
 
 file(GLOB SUBOOL_SOURCES *.cpp)
+if(NOT USE_GLUCOSE)
+   list(FILTER SUBOOL_SOURCES EXCLUDE REGEX ".*/glucose_bind\\.cpp$")
+endif()
+if(NOT USE_CADICAL)
+   list(FILTER SUBOOL_SOURCES EXCLUDE REGEX ".*/cadical_bind\\.cpp$")
+endif()
 if(NOT USE_KISSAT)
    list(FILTER SUBOOL_SOURCES EXCLUDE REGEX ".*/kissat_bind\\.cpp$")
 endif()

lib/abscomp.h

@@ -78,7 +78,6 @@ namespace SUBool
          AbsCheckerSAT::Timeouts timeouts{};
          bool level_minimize{false};
          LIT_IMPL_SYSTEM impl_system{LIT_IMPL_SYSTEM::Default};
-         SOLVER_TYPE solver_type{SOLVER_TYPE::GLUCOSE};
          IMPL_SYSTEM_REBUILD impl_system_rebuild{
              IMPL_SYSTEM_REBUILD::CLAUSE_ADDED};
       };

lib/absenc.h

@@ -18,10 +18,10 @@
 #include "cl2lit.h"
 #include "enc_is_provider.h"
 #include "enum.h"
-#include "glucose_bind.h"
 #include "impl_system.h"
 #include "impl_system_graph.h"
 #include "normalform.h"
+#include "solver_bind.h"
 #include "up_min_lq.h"
 #include "upenc.h"
 #include "varstore.h"

lib/cadical_bind.cpp

+/*
+ * Project SUBool
+ * Petr Kucera, 2022
+ */
+/**@file cadical_bind.cpp
+ * Binding class to CaDiCaL solver library. */
+
+#include "cadical_bind.h"
+
+void
+SUBool::CadicalBind::SolverInit()
+{
+   logs.TLog(3) << "Initializing CaDiCaL solver" << std::endl;
+   mSolver = std::make_unique<CaDiCaL::Solver>();
+   mResult = PartialValue::UNDEF;
+   mSolver->set("seed", sub_rand() % 2147483647);
+   mSolver->set("verbose", -1);
+   mSolver->set("quiet", 1);
+   Adapt();
+   if (mCollectLearnts)
+   {
+      if (!mLearner)
+      {
+         mLearner = std::make_unique<CBLearner>();
+      }
+      else
+      {
+         mLearner->Clear();
+      }
+      mSolver->connect_learner(mLearner.get());
+   }
+}
+
+bool
+SUBool::CadicalBind::Reset(const CNF &cnf)
+{
+   SolverInit();
+   return AddCnf(cnf);
+}
+
+bool
+SUBool::CadicalBind::AddCnf(const CNF &cnf)
+{
+   for (const auto &clause : cnf)
+   {
+      if (!AddClause(clause))
+      {
+         return false;
+      }
+   }
+   return true;
+}
+