Glucose can now be missing if cadical is present

CMakeLists.txt

@@ -39,8 +39,8 @@ endfunction(su_add_pthread)
 find_package(Boost 1.64.0 COMPONENTS program_options REQUIRED)
 
 # Glucose related part
-option(USE_KISSAT "If the project should compile with kissat support" ON)
-if(USE_KISSAT)
+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}")
@@ -50,9 +50,16 @@ if(USE_KISSAT)
    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}")
-   include_directories (SYSTEM ${GLUCOSE_HOME})
+   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()
    message(STATUS "Glucose support will not be available")
 endif()
@@ -74,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)
@@ -106,9 +113,9 @@ if(USE_CADICAL)
       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 ${CADICAL_HOME}/build)
+   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}")
+      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)
@@ -128,6 +135,10 @@ function(su_add_cadical_lib libs)
 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 (/usr/local/include/)

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/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/canon.h

@@ -10,8 +10,8 @@
 #include <queue>
 
 #include "cpuutil.h"
-#include "glucose_bind.h"
 #include "normalform.h"
+#include "solver_bind.h"
 
 namespace SUBool
 {

lib/cnfutil.h

@@ -17,10 +17,10 @@
 #include <queue>
 #include <unordered_set>
 
-#include "glucose_bind.h"
 #include "logstream.h"
 #include "normalform.h"
 #include "random_utils.h"
+#include "solver_bind.h"
 #include "unitprop.h"
 
 namespace SUBool

lib/encoding.cpp

@@ -9,10 +9,10 @@
 #include "encoding.h"
 #include "dimacs.h"
 #include "dpelim.h"
-#include "glucose_bind.h"
 #include "pccomp.h"
 #include "propagate.h"
 #include "sbexception.h"
+#include "solver_bind.h"
 
 const size_t SUBool::CNFEncoding::kEliminateAll =
     SUBool::DPEliminator::kEliminateAll;

lib/glucose_bind.h

@@ -8,6 +8,8 @@
 #ifndef __GLUCOSE_BIND_H
 #define __GLUCOSE_BIND_H
 
+#if HAS_GLUCOSE
+
 #include "random_utils.h"
 #include "solver_bind.h"
 #include <simp/SimpSolver.h>
@@ -366,4 +368,5 @@ SUBool::GlucoseBind<Solver>::IsIncremental() const
    return mSolver->isIncremental();
 }
 
-#endif
+#endif // HAS_GLUCOSE
+#endif // __GLUCOSE_BIND_H

lib/pcchecker.cpp

@@ -9,9 +9,8 @@
 #include "pcchecker.h"
 #include "cpuutil.h"
 #include "drenc.h"
-#include "glucose_bind.h"
-#include "kissat_bind.h"
 #include "logstream.h"
+#include "solver_bind.h"
 
 void
 SUBool::AbsCheckerSAT::InitBase(unsigned max_up_level_bound,

lib/pcenc.h

@@ -17,8 +17,8 @@
 #include "absenc.h"
 #include "cl2lit.h"
 #include "enum.h"
-#include "glucose_bind.h"
 #include "normalform.h"
+#include "solver_bind.h"
 #include "upenc.h"
 #include "varstore.h"
 

lib/propagate.cpp

@@ -7,6 +7,7 @@
  */
 
 #include "propagate.h"
+#include "random_utils.h"
 
 namespace SUBool
 {

lib/propagate.h

@@ -11,9 +11,9 @@
 
 #include <unordered_set>
 
-#include "glucose_bind.h"
 #include "logstream.h"
 #include "min_model.h"
+#include "solver_bind.h"
 #include "unitprop.h"
 #include "unitprop2.h"
 #include "util.h"

lib/rh_bdmc.cpp

@@ -12,10 +12,10 @@
 #include "cnfgraph.h"
 #include "cnfutil.h"
 #include "empower.h"
-#include "glucose_bind.h"
 #include "logstream.h"
 #include "rhorn.h"
 #include "sbexception.h"
+#include "solver_bind.h"
 #include "unitprop.h"
 
 #include "pcchecker.h"
@@ -93,8 +93,8 @@ SUBool::RHBackdoorTree::DetermineNextEvent()
       return EventType::DECISION;
       // return EventType::COMPONENT_SPLIT;
    }
-   throw BadParameterException("RHBackdoorTree::DetermineNextEvent",
-                               "Unknown stack type");
+   throw BadParameterException(
+       "RHBackdoorTree::DetermineNextEvent", "Unknown stack type");
 }
 
 void
@@ -303,7 +303,7 @@ SUBool::RHBackdoorTree::BacktrackDecision()
       }
       mCurrentNnf =
           NnfNode::MakeDecision(mDecisionStack.top().literal.Variable(),
-                                mDecisionStack.top().first_branch, mCurrentNnf);
+              mDecisionStack.top().first_branch, mCurrentNnf);
    }
    // std::cout << "here, " << mShouldBacktrack << std::endl;
    mValues[mDecisionStack.top().literal.Variable()] = PartialValue::UNDEF;

lib/solver_bind.cpp

@@ -86,7 +86,12 @@ SUBool::noninc_solver_wrapper(
    switch (solver_type)
    {
    case NONINC_SOLVER_TYPE::GLUCOSE:
+#if HAS_GLUCOSE
       return GlucoseSimpWrapper(adapt);
+#else
+      throw BadParameterException(
+          "noninc_solver_wrapper", "Glucose support not available");
+#endif
    case NONINC_SOLVER_TYPE::CADICAL:
 #if HAS_CADICAL
       return CadicalWrapper(false, adapt);
@@ -114,7 +119,12 @@ SUBool::noninc_solver_wrapper(NONINC_SOLVER_TYPE solver_type, const CNF &cnf,
    switch (solver_type)
    {
    case NONINC_SOLVER_TYPE::GLUCOSE:
+#if HAS_GLUCOSE
       return GlucoseSimpWrapper(cnf, adapt);
+#else
+      throw BadParameterException(
+          "noninc_solver_wrapper", "Glucose support not available");
+#endif
    case NONINC_SOLVER_TYPE::CADICAL:
 #if HAS_CADICAL
       return CadicalWrapper(cnf, false, adapt);
@@ -142,7 +152,12 @@ SUBool::inc_solver_wrapper(INC_SOLVER_TYPE solver_type,
    switch (solver_type)
    {
    case INC_SOLVER_TYPE::GLUCOSE:
+#if HAS_GLUCOSE
       return GlucoseIncWrapper(adapt);
+#else
+      throw BadParameterException(
+          "inc_solver_wrapper", "Glucose support not available");
+#endif
    case INC_SOLVER_TYPE::CADICAL:
 #if HAS_CADICAL
       return CadicalWrapper(collect_learnts, adapt);
@@ -162,7 +177,12 @@ SUBool::inc_solver_wrapper(INC_SOLVER_TYPE solver_type, const CNF &cnf,
    switch (solver_type)
    {
    case INC_SOLVER_TYPE::GLUCOSE:
+#if HAS_GLUCOSE
       return GlucoseIncWrapper(cnf, adapt);
+#else
+      throw BadParameterException(
+          "inc_solver_wrapper", "Glucose support not available");
+#endif
    case INC_SOLVER_TYPE::CADICAL:
 #if HAS_CADICAL
       return CadicalWrapper(cnf, collect_learnts, adapt);

lib/solver_bind.h

@@ -332,10 +332,10 @@ SUBool::SolverPool::NewSolver(Args &&...arg)
 }
 
 #if HAS_GLUCOSE
-constexpr SUBool::SOLVER_TYPE
-SUBool::default_solver_type()
+constexpr SUBool::NONINC_SOLVER_TYPE
+SUBool::default_noninc_solver_type()
 {
-   return SOLVER_TYPE::GLUCOSE;
+   return NONINC_SOLVER_TYPE::GLUCOSE;
 }
 constexpr SUBool::INC_SOLVER_TYPE
 SUBool::default_inc_solver_type()

test/CMakeLists.txt

@@ -26,8 +26,12 @@ su_add_test_exec(resolve false false)
 if(USE_KISSAT)
    su_add_test_exec(kissat true true)
 endif()
-su_add_test_exec(glucose true true)
-su_add_test_exec(cadical true true)
+if(USE_GLUCOSE)
+   su_add_test_exec(glucose true true)
+endif()
+if(USE_CADICAL)
+   su_add_test_exec(cadical true true)
+endif()
 su_add_test_exec(cnfcompress false false)
 su_add_test_exec(cnfutil true true)
 su_add_test_exec(canon true true)

test/test_encoding.cpp

@@ -11,9 +11,9 @@
 
 #include "dimacs.h"
 #include "encoding.h"
-#include "glucose_bind.h"
 #include "logstream.h"
 #include "random_utils.h"
+#include "solver_bind.h"
 #include "test_common.h"
 #include "test_encoding.h"
 

test/test_glucose.cpp

@@ -11,8 +11,8 @@
 
 #include "cnfutil.h"
 #include "dimacs.h"
-#include "glucose_bind.h"
 #include "random_utils.h"
+#include "solver_bind.h"
 #include "test_glucose.h"
 #include "util.h"
 

test/test_propagate.cpp

@@ -9,6 +9,7 @@
 #include "test_propagate.h"
 #include "dimacs.h"
 #include "propagate.h"
+#include "random_utils.h"
 
 const char *dimacs_simple = "p cnf 8 8\n"
                             "1 2 5 0\n"