Support for using 'libedit' over 'readline' #4571 (#4579)

Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>

3 files changed, 16 insertions, 17 deletions

diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
index c50311840..ef20b47cb 100644
--- a/src/base/configuration.cpp
+++ b/src/base/configuration.cpp
@@ -139,7 +139,8 @@ std::string Configuration::copyright() {
       || Configuration::isBuiltWithCadical()
       || Configuration::isBuiltWithCryptominisat()
       || Configuration::isBuiltWithKissat()
-      || Configuration::isBuiltWithSymFPU())
+      || Configuration::isBuiltWithSymFPU()
+      || Configuration::isBuiltWithEditline())
   {
     ss << "This version of CVC4 is linked against the following non-(L)GPL'ed\n"
        << "third party libraries.\n\n";
@@ -177,6 +178,12 @@ std::string Configuration::copyright() {
          << "  See https://github.com/martin-cs/symfpu/tree/CVC4 for copyright "
          << "information.\n\n";
     }
+    if (Configuration::isBuiltWithEditline())
+    {
+      ss << "  Editline Library\n"
+         << "  See https://thrysoee.dk/editline\n"
+         << "  for copyright information.\n\n";
+    }
   }
 
   if (Configuration::isBuiltWithGmp() || Configuration::isBuiltWithPoly())
@@ -197,8 +204,7 @@ std::string Configuration::copyright() {
   }
 
   if (Configuration::isBuiltWithCln()
-      || Configuration::isBuiltWithGlpk ()
-      || Configuration::isBuiltWithReadline()) {
+      || Configuration::isBuiltWithGlpk ()) {
     ss << "This version of CVC4 is linked against the following third party\n"
        << "libraries covered by the GPLv3 license.\n"
        << "See licenses/gpl-3.0.txt for more information.\n\n";
@@ -212,11 +218,6 @@ std::string Configuration::copyright() {
          << "  See http://github.com/timothy-king/glpk-cut-log for copyright"
          << "information\n\n";
     }
-    if (Configuration::isBuiltWithReadline()) {
-      ss << "  GNU Readline\n"
-         << "  See http://cnswww.cns.cwru.edu/php/chet/readline/rltop.html\n"
-         << "  for copyright information.\n\n";
-    }
   }
 
   ss << "See the file COPYING (distributed with the source code, and with\n"
@@ -267,9 +268,7 @@ bool Configuration::isBuiltWithKissat() { return IS_KISSAT_BUILD; }
 
 bool Configuration::isBuiltWithDrat2Er() { return IS_DRAT2ER_BUILD; }
 
-bool Configuration::isBuiltWithReadline() {
-  return IS_READLINE_BUILD;
-}
+bool Configuration::isBuiltWithEditline() { return IS_EDITLINE_BUILD; }
 
 bool Configuration::isBuiltWithLfsc() {
   return IS_LFSC_BUILD;
diff --git a/src/base/configuration.h b/src/base/configuration.h
index 40914e531..d148adcbb 100644
--- a/src/base/configuration.h
+++ b/src/base/configuration.h
@@ -103,7 +103,7 @@ public:
 
   static bool isBuiltWithDrat2Er();
 
-  static bool isBuiltWithReadline();
+  static bool isBuiltWithEditline();
 
   static bool isBuiltWithLfsc();
 
diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h
index 906cf831d..fcfc6d500 100644
--- a/src/base/configuration_private.h
+++ b/src/base/configuration_private.h
@@ -144,11 +144,11 @@ namespace CVC4 {
 #define IS_POLY_BUILD false
 #endif /* CVC4_USE_POLY */
 
-#if HAVE_LIBREADLINE
-#  define IS_READLINE_BUILD true
-#else /* HAVE_LIBREADLINE */
-#  define IS_READLINE_BUILD false
-#endif /* HAVE_LIBREADLINE */
+#if HAVE_LIBEDITLINE
+#define IS_EDITLINE_BUILD true
+#else /* HAVE_LIBEDITLINE */
+#define IS_EDITLINE_BUILD false
+#endif /* HAVE_LIBEDITLINE */
 
 #ifdef CVC4_USE_SYMFPU
 #define IS_SYMFPU_BUILD true