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.

diff --git a/CMakeLists.txt b/CMakeLists.txt
index b29585f3bd08867b3c2b554d2655824cb612a352..3780b0b5bfa72eba672cc82533b6218598fd4497 100644 (file)
--- 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 1943d7f00b71cd838b079d612abb470a588a9628..8e0ace2cf671ec8161051b899409ac02340b478a 100644 (file)
--- 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 25203f8a699a91043d7fe2c81c877b5fa14d4525..4ba153a758c891e641d3dd0c98603169af4ca4b4 100755 (executable)
--- 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 d7da67cbeea358c7ec4d3c5001ff03c75b59c0df..b3f27b70398e5f2521f91c53643733bf26762cd4 100644 (file)
--- 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 1befb34ea528521e1f01d471593df4484ef8e50e..c6b0045743ea26e884d34c9932a9744c6cc82e1a 100644 (file)
--- 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 2a7df1b4ae2478ec2e5c9e40b28f67f948cf2ce3..71c79c22e3692a8667f869e3011591182583375e 100644 (file)
--- 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 39c5e89e964f0aba693325c6f572fc24599d7b1d..b348da3809c0599106fdb81cc72c728480178976 100644 (file)
--- 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 d31d2e58f4ee6b2b046d22fbb6627a3771200ee4..07138dce35c4715a80a41b1d1b0a6c8c1d3ec946 100644 (file)
--- 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 9aee1df2268ac816d912ca8577f6d5945e041cb4..3b3f80e6cd62fa8dad4e532c453d211e40fd6e04 100644 (file)
--- 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 ec8919b0b2253026f6d19a1c4aec049e197d46a9..ddf20f5a1e00a5e33a39388bc49d5097ca52ea1c 100644 (file)
--- 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 b5e26df9ffb2494e8f732c7be2e92185e65a11c6..46c7c7e42cd2b94d5ce5eeb561a588210d0ecb19 100644 (file)
--- 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 446f72451649e0544ba20950f22f08ff6648b86d..0855cbda5ac8a39bfd6cf2522c2397be1410409d 100644 (file)
--- 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 01840dffaa732113478c0656878fb49512912ebb..34007f6aafb3013c41f2338cee7a9bb63725b042 100644 (file)
--- 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)