Add support for CaDiCaL as eager BV SAT solver. (#1675)

3 files changed, 28 insertions, 8 deletions

diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
index 7e7da1500..7ceb64885 100644
--- a/src/base/configuration.cpp
+++ b/src/base/configuration.cpp
@@ -134,7 +134,10 @@ std::string Configuration::copyright() {
      << "\n\n";
 
   if (Configuration::isBuiltWithAbc()
-      || Configuration::isBuiltWithLfsc()) {
+      || Configuration::isBuiltWithLfsc()
+      || Configuration::isBuiltWithCadical()
+      || Configuration::isBuiltWithCryptominisat())
+  {
     ss << "This version of CVC4 is linked against the following non-(L)GPL'ed\n"
        << "third party libraries.\n\n";
     if (Configuration::isBuiltWithAbc()) {
@@ -147,10 +150,22 @@ std::string Configuration::copyright() {
          << "  See http://github.com/CVC4/LFSC 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"
+         << "  See https://github.com/msoos/cryptominisat for copyright "
+         << "information.\n\n";
+    }
   }
 
-  if (Configuration::isBuiltWithGmp()
-      || Configuration::isBuiltWithCryptominisat()) {
+  if (Configuration::isBuiltWithGmp())
+  {
     ss << "This version of CVC4 is linked against the following third party\n"
        << "libraries covered by the LGPLv3 license.\n"
        << "See licenses/lgpl-3.0.txt for more information.\n\n";
@@ -158,11 +173,6 @@ std::string Configuration::copyright() {
       ss << "  GMP - Gnu Multi Precision Arithmetic Library\n"
          << "  See http://gmplib.org for copyright information.\n\n";
     }
-    if (Configuration::isBuiltWithCryptominisat()) {
-      ss << "  CryptoMiniSat - An Advanced SAT Solver\n"
-         << "  See http://github.com/msoos/cryptominisat for copyright "
-         << "information.\n\n";
-    }
   }
 
   if (Configuration::isBuiltWithCln()
@@ -228,6 +238,8 @@ 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 29f23ab18..897f234d7 100644
--- a/src/base/configuration.h
+++ b/src/base/configuration.h
@@ -95,6 +95,8 @@ public:
 
   static bool isBuiltWithAbc();
 
+  static bool isBuiltWithCadical();
+
   static bool isBuiltWithCryptominisat();
 
   static bool isBuiltWithReadline();
diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h
index eba45cc61..cf9117100 100644
--- a/src/base/configuration_private.h
+++ b/src/base/configuration_private.h
@@ -114,6 +114,12 @@ namespace CVC4 {
 #  define IS_ABC_BUILD false
 #endif /* CVC4_USE_ABC */
 
+#if CVC4_USE_CADICAL
+#define IS_CADICAL_BUILD true
+#else /* CVC4_USE_CADICAL */
+#define IS_CADICAL_BUILD false
+#endif /* CVC4_USE_CADICAL */
+
 #if CVC4_USE_CRYPTOMINISAT
 #  define IS_CRYPTOMINISAT_BUILD true
 #else /* CVC4_USE_CRYPTOMINISAT */