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

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

7 files changed, 63 insertions, 57 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
diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt
index 4fbb14183..c168daeaa 100644
--- a/src/main/CMakeLists.txt
+++ b/src/main/CMakeLists.txt
@@ -68,10 +68,10 @@ if(ENABLE_STATIC_BINARY)
   set_target_properties(cvc4-bin PROPERTIES LINK_SEARCH_END_STATIC ON)
 endif()
 
-if(USE_READLINE)
-  target_link_libraries(cvc4-bin ${Readline_LIBRARIES})
-  target_link_libraries(main-test ${Readline_LIBRARIES})
-  target_include_directories(main PRIVATE ${Readline_INCLUDE_DIR})
+if(USE_EDITLINE)
+  target_link_libraries(cvc4-bin ${Editline_LIBRARIES})
+  target_link_libraries(main-test ${Editline_LIBRARIES})
+  target_include_directories(main PRIVATE ${Editline_INCLUDE_DIR})
 endif()
 
 #-----------------------------------------------------------------------------#
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 17b792ab4..87ebf99cf 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -12,7 +12,7 @@
  ** \brief Interactive shell for CVC4
  **
  ** This file is the implementation for the CVC4 interactive shell.
- ** The shell supports the readline library.
+ ** The shell supports the editline library.
  **/
 #include "main/interactive_shell.h"
 
@@ -26,16 +26,15 @@
 #include <utility>
 #include <vector>
 
-//This must go before HAVE_LIBREADLINE.
+// This must go before HAVE_LIBEDITLINE.
 #include "cvc4autoconfig.h"
 
-#if HAVE_LIBREADLINE
-#  include <readline/readline.h>
-#  include <readline/history.h>
+#if HAVE_LIBEDITLINE
+#include <editline/readline.h>
 #  if HAVE_EXT_STDIO_FILEBUF_H
 #    include <ext/stdio_filebuf.h>
 #  endif /* HAVE_EXT_STDIO_FILEBUF_H */
-#endif /* HAVE_LIBREADLINE */
+#endif   /* HAVE_LIBEDITLINE */
 
 #include "api/cvc4cpp.h"
 #include "base/output.h"
@@ -56,7 +55,7 @@ using namespace language;
 
 const string InteractiveShell::INPUT_FILENAME = "<shell>";
 
-#if HAVE_LIBREADLINE
+#if HAVE_LIBEDITLINE
 
 #if HAVE_EXT_STDIO_FILEBUF_H
 using __gnu_cxx::stdio_filebuf;
@@ -82,7 +81,7 @@ static const std::string* commandsEnd;
 
 static set<string> s_declarations;
 
-#endif /* HAVE_LIBREADLINE */
+#endif /* HAVE_LIBEDITLINE */
 
 InteractiveShell::InteractiveShell(api::Solver* solver)
     : d_options(solver->getOptions()),
@@ -98,14 +97,14 @@ InteractiveShell::InteractiveShell(api::Solver* solver)
     d_parser->forceLogic(tmp.getLogicString());
   }
 
-#if HAVE_LIBREADLINE
+#if HAVE_LIBEDITLINE
   if(&d_in == &cin) {
     ::rl_readline_name = const_cast<char*>("CVC4");
-#if READLINE_COMPENTRY_FUNC_RETURNS_CHARP
+#if EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP
     ::rl_completion_entry_function = commandGenerator;
-#else /* READLINE_COMPENTRY_FUNC_RETURNS_CHARP */
+#else /* EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP */
     ::rl_completion_entry_function = (int (*)(const char*, int)) commandGenerator;
-#endif /* READLINE_COMPENTRY_FUNC_RETURNS_CHARP */
+#endif /* EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP */
     ::using_history();
 
     OutputLanguage lang = toOutputLanguage(d_options.getInputLanguage());
@@ -135,7 +134,7 @@ InteractiveShell::InteractiveShell(api::Solver* solver)
         throw Exception(ss.str());
       }
     }
-    d_usingReadline = true;
+    d_usingEditline = true;
     int err = ::read_history(d_historyFilename.c_str());
     ::stifle_history(s_historyLimit);
     if(Notice.isOn()) {
@@ -148,15 +147,15 @@ InteractiveShell::InteractiveShell(api::Solver* solver)
       }
     }
   } else {
-    d_usingReadline = false;
+    d_usingEditline = false;
   }
-#else /* HAVE_LIBREADLINE */
-  d_usingReadline = false;
-#endif /* HAVE_LIBREADLINE */
+#else  /* HAVE_LIBEDITLINE */
+  d_usingEditline = false;
+#endif /* HAVE_LIBEDITLINE */
 }/* InteractiveShell::InteractiveShell() */
 
 InteractiveShell::~InteractiveShell() {
-#if HAVE_LIBREADLINE
+#if HAVE_LIBEDITLINE
   int err = ::write_history(d_historyFilename.c_str());
   if(err == 0) {
     Notice() << "Wrote " << ::history_length << " lines of history to "
@@ -165,7 +164,7 @@ InteractiveShell::~InteractiveShell() {
     Notice() << "Could not write history to " << d_historyFilename
              << ": " << strerror(err) << std::endl;
   }
-#endif /* HAVE_LIBREADLINE */
+#endif /* HAVE_LIBEDITLINE */
   delete d_parser;
 }
 
@@ -189,8 +188,9 @@ restart:
   }
 
   /* Prompt the user for input. */
-  if(d_usingReadline) {
-#if HAVE_LIBREADLINE
+  if (d_usingEditline)
+  {
+#if HAVE_LIBEDITLINE
     lineBuf = ::readline(d_options.getInteractivePrompt()
                          ? (line == "" ? "CVC4> " : "... > ") : "");
     if(lineBuf != NULL && lineBuf[0] != '\0') {
@@ -198,8 +198,10 @@ restart:
     }
     line += lineBuf == NULL ? "" : lineBuf;
     free(lineBuf);
-#endif /* HAVE_LIBREADLINE */
-  } else {
+#endif /* HAVE_LIBEDITLINE */
+  }
+  else
+  {
     if(d_options.getInteractivePrompt()) {
       if(line == "") {
         d_out << "CVC4> " << flush;
@@ -236,8 +238,9 @@ restart:
     }
 
     /* If we hit EOF, we're done. */
-    if( (!d_usingReadline && d_in.eof()) ||
-        (d_usingReadline && lineBuf == NULL) ) {
+    if ((!d_usingEditline && d_in.eof())
+        || (d_usingEditline && lineBuf == NULL))
+    {
       input += line;
 
       if(input.empty()) {
@@ -254,7 +257,8 @@ restart:
       goto restart;
     }
 
-    if(!d_usingReadline) {
+    if (!d_usingEditline)
+    {
       /* Extract the newline delimiter from the stream too */
       int c CVC4_UNUSED = d_in.get();
       assert(c == '\n');
@@ -268,16 +272,19 @@ restart:
     n = input.length() - 1;
     if( !line.empty() && input[n] == '\\' ) {
       input[n] = '\n';
-      if(d_usingReadline) {
-#if HAVE_LIBREADLINE
+      if (d_usingEditline)
+      {
+#if HAVE_LIBEDITLINE
         lineBuf = ::readline(d_options.getInteractivePrompt() ? "... > " : "");
         if(lineBuf != NULL && lineBuf[0] != '\0') {
           ::add_history(lineBuf);
         }
         line = lineBuf == NULL ? "" : lineBuf;
         free(lineBuf);
-#endif /* HAVE_LIBREADLINE */
-      } else {
+#endif /* HAVE_LIBEDITLINE */
+      }
+      else
+      {
         if(d_options.getInteractivePrompt()) {
           d_out << "... > " << flush;
         }
@@ -309,7 +316,7 @@ restart:
         d_quit = true;
         break;
       } else {
-#if HAVE_LIBREADLINE
+#if HAVE_LIBEDITLINE
         if(dynamic_cast<DeclareFunctionCommand*>(cmd) != NULL) {
           s_declarations.insert(dynamic_cast<DeclareFunctionCommand*>(cmd)->getSymbol());
         } else if(dynamic_cast<DefineFunctionCommand*>(cmd) != NULL) {
@@ -319,7 +326,7 @@ restart:
         } else if(dynamic_cast<DefineTypeCommand*>(cmd) != NULL) {
           s_declarations.insert(dynamic_cast<DefineTypeCommand*>(cmd)->getSymbol());
         }
-#endif /* HAVE_LIBREADLINE */
+#endif /* HAVE_LIBEDITLINE */
       }
     }
   } catch(ParserEndOfFileException& pe) {
@@ -350,7 +357,7 @@ restart:
   return cmd_seq;
 }/* InteractiveShell::readCommand() */
 
-#if HAVE_LIBREADLINE
+#if HAVE_LIBEDITLINE
 
 char** commandCompletion(const char* text, int start, int end) {
   Debug("rl") << "text: " << text << endl;
@@ -400,6 +407,6 @@ char* commandGenerator(const char* text, int state) {
   return *rlDeclaration == jj ? NULL : strdup((*(*rlDeclaration)++).c_str());
 }
 
-#endif /* HAVE_LIBREADLINE */
+#endif /* HAVE_LIBEDITLINE */
 
 }/* CVC4 namespace */
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index 87845b0ed..f4edb1015 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -42,7 +42,7 @@ class CVC4_PUBLIC InteractiveShell
   std::ostream& d_out;
   parser::Parser* d_parser;
   bool d_quit;
-  bool d_usingReadline;
+  bool d_usingEditline;
 
   std::string d_historyFilename;
 
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 380325a1b..40f9b898e 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -443,7 +443,7 @@ void OptionsHandler::showConfiguration(std::string option) {
   print_config_cond("kissat", Configuration::isBuiltWithKissat());
   print_config_cond("lfsc", Configuration::isBuiltWithLfsc());
   print_config_cond("poly", Configuration::isBuiltWithPoly());
-  print_config_cond("readline", Configuration::isBuiltWithReadline());
+  print_config_cond("editline", Configuration::isBuiltWithEditline());
   print_config_cond("symfpu", Configuration::isBuiltWithSymFPU());
   
   exit(0);