Make CaDiCaL a required dependency. (#6761)

Since the new BV solver is enabled by default and uses CaDiCaL
(and optionally CryptoMiniSat) we make CaDiCaL a required dependency.

9 files changed, 11 insertions, 62 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index d7da67cbe..b3f27b703 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -1185,9 +1185,9 @@ if(USE_ABC)
   target_link_libraries(cvc5 PRIVATE ${ABC_LIBRARIES})
   target_include_directories(cvc5 PRIVATE ${ABC_INCLUDE_DIR})
 endif()
-if(USE_CADICAL)
-  target_link_libraries(cvc5 PRIVATE CaDiCaL)
-endif()
+
+target_link_libraries(cvc5 PRIVATE CaDiCaL)
+
 if(USE_CLN)
   target_link_libraries(cvc5 PRIVATE CLN)
 endif()
diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
index 1befb34ea..c6b004574 100644
--- a/src/base/configuration.cpp
+++ b/src/base/configuration.cpp
@@ -120,24 +120,23 @@ std::string Configuration::copyright() {
      << "See licenses/antlr3-LICENSE for copyright and licensing information."
      << "\n\n";
 
-  if (Configuration::isBuiltWithAbc() || Configuration::isBuiltWithCadical()
+  ss << "This version of cvc5 is linked against the following non-(L)GPL'ed\n"
+     << "third party libraries.\n\n";
+
+  ss << "  CaDiCaL - Simplified Satisfiability Solver\n"
+     << "  See https://github.com/arminbiere/cadical for copyright "
+     << "information.\n\n";
+
+  if (Configuration::isBuiltWithAbc()
       || Configuration::isBuiltWithCryptominisat()
       || Configuration::isBuiltWithKissat()
       || Configuration::isBuiltWithEditline())
   {
-    ss << "This version of cvc5 is linked against the following non-(L)GPL'ed\n"
-       << "third party libraries.\n\n";
     if (Configuration::isBuiltWithAbc()) {
       ss << "  ABC - A System for Sequential Synthesis and Verification\n"
          << "  See http://bitbucket.org/alanmi/abc for copyright and\n"
          << "  licensing information.\n\n";
     }
-    if (Configuration::isBuiltWithCadical())
-    {
-      ss << "  CaDiCaL - Simplified Satisfiability Solver\n"
-         << "  See https://github.com/arminbiere/cadical for copyright "
-         << "information.\n\n";
-    }
     if (Configuration::isBuiltWithCryptominisat())
     {
       ss << "  CryptoMiniSat - An Advanced SAT Solver\n"
@@ -241,8 +240,6 @@ bool Configuration::isBuiltWithAbc() {
   return IS_ABC_BUILD;
 }
 
-bool Configuration::isBuiltWithCadical() { return IS_CADICAL_BUILD; }
-
 bool Configuration::isBuiltWithCryptominisat() {
   return IS_CRYPTOMINISAT_BUILD;
 }
diff --git a/src/base/configuration.h b/src/base/configuration.h
index 2a7df1b4a..71c79c22e 100644
--- a/src/base/configuration.h
+++ b/src/base/configuration.h
@@ -103,8 +103,6 @@ public:
 
   static bool isBuiltWithAbc();
 
-  static bool isBuiltWithCadical();
-
   static bool isBuiltWithCryptominisat();
 
   static bool isBuiltWithKissat();
diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h
index 39c5e89e9..b348da380 100644
--- a/src/base/configuration_private.h
+++ b/src/base/configuration_private.h
@@ -96,12 +96,6 @@ namespace cvc5 {
 #  define IS_ABC_BUILD false
 #endif /* CVC5_USE_ABC */
 
-#if CVC5_USE_CADICAL
-#define IS_CADICAL_BUILD true
-#else /* CVC5_USE_CADICAL */
-#define IS_CADICAL_BUILD false
-#endif /* CVC5_USE_CADICAL */
-
 #if CVC5_USE_CRYPTOMINISAT
 #  define IS_CRYPTOMINISAT_BUILD true
 #else /* CVC5_USE_CRYPTOMINISAT */
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index d31d2e58f..07138dce3 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -146,15 +146,6 @@ void OptionsHandler::checkBvSatSolver(const std::string& option,
     throw OptionException(ss.str());
   }
 
-  if (m == SatSolverMode::CADICAL && !Configuration::isBuiltWithCadical())
-  {
-    std::stringstream ss;
-    ss << "option `" << option
-       << "' requires a CaDiCaL build of cvc5; this binary was not built with "
-          "CaDiCaL support";
-    throw OptionException(ss.str());
-  }
-
   if (m == SatSolverMode::KISSAT && !Configuration::isBuiltWithKissat())
   {
     std::stringstream ss;
@@ -397,7 +388,6 @@ void OptionsHandler::showConfiguration(const std::string& option,
   print_config_cond("abc", Configuration::isBuiltWithAbc());
   print_config_cond("cln", Configuration::isBuiltWithCln());
   print_config_cond("glpk", Configuration::isBuiltWithGlpk());
-  print_config_cond("cadical", Configuration::isBuiltWithCadical());
   print_config_cond("cryptominisat", Configuration::isBuiltWithCryptominisat());
   print_config_cond("gmp", Configuration::isBuiltWithGmp());
   print_config_cond("kissat", Configuration::isBuiltWithKissat());
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 9aee1df22..3b3f80e6c 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -84,11 +84,6 @@ public:
                        const std::string& flag,
                        const std::string& value);
 
-  template <class T>
-  void checkSatSolverEnabled(const std::string& option,
-                             const std::string& flag,
-                             T m);
-
   void checkBvSatSolver(const std::string& option,
                         const std::string& flag,
                         SatSolverMode m);
@@ -171,20 +166,6 @@ public:
 
 }; /* class OptionHandler */
 
-template <class T>
-void OptionsHandler::checkSatSolverEnabled(const std::string& option,
-                                           const std::string& flag,
-                                           T m)
-{
-#if !defined(CVC5_USE_CRYPTOMINISAT) && !defined(CVC5_USE_CADICAL) \
-    && !defined(CVC5_USE_KISSAT)
-  std::stringstream ss;
-  ss << "option `" << option
-     << "' requires cvc5 to be built with CryptoMiniSat or CaDiCaL or Kissat";
-  throw OptionException(ss.str());
-#endif
-}
-
 }  // namespace options
 }  // namespace cvc5
 
diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp
index ec8919b0b..ddf20f5a1 100644
--- a/src/prop/cadical.cpp
+++ b/src/prop/cadical.cpp
@@ -17,8 +17,6 @@
 
 #include "prop/cadical.h"
 
-#ifdef CVC5_USE_CADICAL
-
 #include "base/check.h"
 #include "util/statistics_registry.h"
 
@@ -191,5 +189,3 @@ CadicalSolver::Statistics::Statistics(StatisticsRegistry& registry,
 
 }  // namespace prop
 }  // namespace cvc5
-
-#endif  // CVC5_USE_CADICAL
diff --git a/src/prop/cadical.h b/src/prop/cadical.h
index b5e26df9f..46c7c7e42 100644
--- a/src/prop/cadical.h
+++ b/src/prop/cadical.h
@@ -20,8 +20,6 @@
 #ifndef CVC5__PROP__CADICAL_H
 #define CVC5__PROP__CADICAL_H
 
-#ifdef CVC5_USE_CADICAL
-
 #include "prop/sat_solver.h"
 
 #include <cadical.hpp>
@@ -103,5 +101,4 @@ class CadicalSolver : public SatSolver
 }  // namespace prop
 }  // namespace cvc5
 
-#endif  // CVC5_USE_CADICAL
 #endif  // CVC5__PROP__CADICAL_H
diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index 446f72451..0855cbda5 100644
--- a/src/prop/sat_solver_factory.cpp
+++ b/src/prop/sat_solver_factory.cpp
@@ -53,13 +53,9 @@ SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry& registry,
 SatSolver* SatSolverFactory::createCadical(StatisticsRegistry& registry,
                                            const std::string& name)
 {
-#ifdef CVC5_USE_CADICAL
   CadicalSolver* res = new CadicalSolver(registry, name);
   res->init();
   return res;
-#else
-  Unreachable() << "cvc5 was not compiled with CaDiCaL support.";
-#endif
 }
 
 SatSolver* SatSolverFactory::createKissat(StatisticsRegistry& registry,