From 7c4a214cf3ce2facf4c98cd3bd347562c66f10a6 Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Mon, 21 Jun 2021 10:11:16 -0700
Subject: [PATCH] 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.
---
 CMakeLists.txt                                |  7 +------
 NEWS                                          |  1 +
 configure.sh                                  |  8 --------
 src/CMakeLists.txt                            |  6 +++---
 src/base/configuration.cpp                    | 19 ++++++++-----------
 src/base/configuration.h                      |  2 --
 src/base/configuration_private.h              |  6 ------
 src/options/options_handler.cpp               | 10 ----------
 src/options/options_handler.h                 | 19 -------------------
 src/prop/cadical.cpp                          |  4 ----
 src/prop/cadical.h                            |  3 ---
 src/prop/sat_solver_factory.cpp               |  4 ----
 .../regress0/bv/eager-inc-cadical.smt2        |  1 -
 13 files changed, 13 insertions(+), 77 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index b29585f3b..3780b0b5b 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -118,7 +118,6 @@ option(ENABLE_PROFILING        "Enable support for gprof profiling")
 #    > allows to detect if set by user (default: IGNORE)
 #    > only necessary for options set for ENABLE_BEST
 cvc5_option(USE_ABC           "Use ABC for AIG bit-blasting")
-cvc5_option(USE_CADICAL       "Use CaDiCaL SAT solver")
 cvc5_option(USE_CLN           "Use CLN instead of GMP")
 cvc5_option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver")
 cvc5_option(USE_GLPK          "Use GLPK simplex solver")
@@ -417,10 +416,7 @@ if(USE_ABC)
   add_definitions(-DCVC5_USE_ABC ${ABC_ARCH_FLAGS})
 endif()
 
-if(USE_CADICAL)
-  find_package(CaDiCaL REQUIRED)
-  add_definitions(-DCVC5_USE_CADICAL)
-endif()
+find_package(CaDiCaL REQUIRED)
 
 if(USE_CLN)
   set(GPL_LIBS "${GPL_LIBS} cln")
@@ -651,7 +647,6 @@ print_config("Java bindings             " ${BUILD_BINDINGS_JAVA})
 print_config("Python2                   " ${USE_PYTHON2})
 message("")
 print_config("ABC                       " ${USE_ABC})
-print_config("CaDiCaL                   " ${USE_CADICAL})
 print_config("CryptoMiniSat             " ${USE_CRYPTOMINISAT})
 print_config("GLPK                      " ${USE_GLPK})
 print_config("Kissat                    " ${USE_KISSAT})
diff --git a/NEWS b/NEWS
index 1943d7f00..8e0ace2cf 100644
--- a/NEWS
+++ b/NEWS
@@ -4,6 +4,7 @@ Changes since CVC4 1.8
 ======================
 
 New Features:
+* CaDiCaL is now a required dependency.
 * SymFPU is now a required dependency.
 * New unsat-core production modes based on the new proof infrastructure
   (`--unsat-cores-mode=sat-proof`) and on the solving-under-assumption feature
diff --git a/configure.sh b/configure.sh
index 25203f8a6..4ba153a75 100755
--- a/configure.sh
+++ b/configure.sh
@@ -59,7 +59,6 @@ The following flags enable optional packages (disable with --no-<option name>).
   --cln                    use CLN instead of GMP
   --glpk                   use GLPK simplex solver
   --abc                    use the ABC AIG library
-  --cadical                use the CaDiCaL SAT solver [default=yes]
   --cryptominisat          use the CryptoMiniSat SAT solver
   --kissat                 use the Kissat SAT solver
   --poly                   use the LibPoly library [default=yes]
@@ -108,7 +107,6 @@ abc=default
 asan=default
 assertions=default
 auto_download=default
-cadical=ON
 cln=default
 comp_inc=default
 coverage=default
@@ -174,7 +172,6 @@ do
     # Best configuration
     --best)
       abc=ON
-      cadical=ON
       cln=ON
       cryptominisat=ON
       glpk=ON
@@ -198,9 +195,6 @@ do
     --name) die "missing argument to $1 (try -h)" ;;
     --name=*) build_dir=${1##*=} ;;
 
-    --cadical) cadical=ON;;
-    --no-cadical) cadical=OFF;;
-
     --cln) cln=ON;;
     --no-cln) cln=OFF;;
 
@@ -379,8 +373,6 @@ cmake_opts=""
   && cmake_opts="$cmake_opts -DUSE_EDITLINE=$editline"
 [ $abc != default ] \
   && cmake_opts="$cmake_opts -DUSE_ABC=$abc"
-[ $cadical != default ] \
-  && cmake_opts="$cmake_opts -DUSE_CADICAL=$cadical"
 [ $cln != default ] \
   && cmake_opts="$cmake_opts -DUSE_CLN=$cln"
 [ $cryptominisat != default ] \
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,
diff --git a/test/regress/regress0/bv/eager-inc-cadical.smt2 b/test/regress/regress0/bv/eager-inc-cadical.smt2
index 01840dffa..34007f6aa 100644
--- a/test/regress/regress0/bv/eager-inc-cadical.smt2
+++ b/test/regress/regress0/bv/eager-inc-cadical.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: cadical
 ; COMMAND-LINE: --incremental --bv-sat-solver=cadical --bitblast=eager
 (set-logic QF_BV)
 (set-option :incremental true)
-- 
2.30.2