diff options
| -rw-r--r-- | .github/workflows/ci.yml | 8 | ||||
| -rw-r--r-- | CMakeLists.txt | 17 | ||||
| -rw-r--r-- | COPYING | 11 | ||||
| -rw-r--r-- | INSTALL.md | 16 | ||||
| -rw-r--r-- | NEWS | 4 | ||||
| -rw-r--r-- | cmake/FindEditline.cmake | 40 | ||||
| -rw-r--r-- | cmake/FindReadline.cmake | 69 | ||||
| -rwxr-xr-x | configure.sh | 12 | ||||
| -rw-r--r-- | cvc4autoconfig.h.in | 10 | ||||
| -rw-r--r-- | src/base/configuration.cpp | 21 | ||||
| -rw-r--r-- | src/base/configuration.h | 2 | ||||
| -rw-r--r-- | src/base/configuration_private.h | 10 | ||||
| -rw-r--r-- | src/main/CMakeLists.txt | 8 | ||||
| -rw-r--r-- | src/main/interactive_shell.cpp | 75 | ||||
| -rw-r--r-- | src/main/interactive_shell.h | 2 | ||||
| -rw-r--r-- | src/options/options_handler.cpp | 2 | ||||
| -rw-r--r-- | test/system/CMakeLists.txt | 22 | ||||
| -rwxr-xr-x | test/system/interactive_shell.py | 94 |
18 files changed, 257 insertions, 166 deletions
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7dd080f71..e9587e2e6 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -16,7 +16,7 @@ jobs: include: - name: production - config: production --all-bindings --lfsc + config: production --all-bindings --lfsc --editline cache-key: production python-bindings: true check-examples: true @@ -28,7 +28,7 @@ jobs: env: CC=clang CXX=clang++ - name: debug - config: debug --symfpu --lfsc --no-debug-symbols + config: debug --symfpu --lfsc --no-debug-symbols --editline cache-key: debug - name: debug-cln @@ -51,11 +51,14 @@ jobs: cxxtest \ libcln-dev \ libgmp-dev \ + libedit-dev \ swig3.0 python3 -m pip install toml python3 -m pip install setuptools + python3 -m pip install pexpect echo "::add-path::/usr/lib/ccache" + # Note: macOS comes with a libedit; it does not need to brew-installed - name: Install Packages (macOS) if: runner.os == 'macOS' run: | @@ -67,6 +70,7 @@ jobs: swig python3 -m pip install toml python3 -m pip install setuptools + python3 -m pip install pexpect echo "::add-path::/usr/local/opt/ccache/libexec" # Note: We install Cython with sudo since cmake can't find Cython otherwise. diff --git a/CMakeLists.txt b/CMakeLists.txt index f4aa6c611..7fc0af52c 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -139,7 +139,7 @@ cvc4_option(USE_CLN "Use CLN instead of GMP") cvc4_option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver") cvc4_option(USE_GLPK "Use GLPK simplex solver") cvc4_option(USE_KISSAT "Use Kissat SAT solver") -cvc4_option(USE_READLINE "Use readline for better interactive support") +cvc4_option(USE_EDITLINE "Use Editline for better interactive support") # >> 2-valued: ON OFF # > for options where we don't need to detect if set by user (default: OFF) option(USE_DRAT2ER "Include drat2er for making eager BV proofs") @@ -274,7 +274,7 @@ if(ENABLE_BEST) cvc4_set_option(USE_CLN ON) cvc4_set_option(USE_CRYPTOMINISAT ON) cvc4_set_option(USE_GLPK ON) - cvc4_set_option(USE_READLINE ON) + cvc4_set_option(USE_EDITLINE ON) endif() # Only enable unit testing if assertions are enabled. Otherwise, unit tests @@ -514,12 +514,11 @@ else() set(CVC4_USE_POLY_IMP 0) endif() -if(USE_READLINE) - set(GPL_LIBS "${GPL_LIBS} readline") - find_package(Readline REQUIRED) - set(HAVE_LIBREADLINE 1) - if(Readline_COMPENTRY_FUNC_RETURNS_CHARPTR) - set(READLINE_COMPENTRY_FUNC_RETURNS_CHARP 1) +if(USE_EDITLINE) + find_package(Editline REQUIRED) + set(HAVE_LIBEDITLINE 1) + if(Editline_COMPENTRY_FUNC_RETURNS_CHARPTR) + set(EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP 1) endif() endif() @@ -707,7 +706,7 @@ if(CVC4_USE_CLN_IMP) else() message("MP library : gmp") endif() -print_config("Readline :" ${USE_READLINE}) +print_config("Editline :" ${USE_EDITLINE}) print_config("SymFPU :" ${USE_SYMFPU}) message("") if(ABC_DIR) @@ -8,9 +8,9 @@ original or modified versions; distribution is under the terms of the modified BSD license (reproduced below). Please note that CVC4 can be configured (however, by default it is not) to link against some GPLed libraries, and therefore the use of these builds may be restricted in non-GPL-compatible -projects. See below for a discussion of CLN, GLPK, and Readline (the three -GPLed optional library dependences for CVC4), and how to ensure you have a -build that doesn't link against GPLed libraries. +projects. See below for a discussion of CLN and GLPK (the two GPLed optional +library dependences for CVC4), and how to ensure you have a build that doesn't +link against GPLed libraries. Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are @@ -80,6 +80,7 @@ CVC4 optionally links against the following libraries: CryptoMiniSat (https://github.com/msoos/cryptominisat) LFSC checker (https://github.com/CVC4/LFSC) LibPoly (https://github.com/SRI-CSL/libpoly) + libedit (https://thrysoee.dk/editline) Linking CVC4 against these libraries does not affect the license terms of the CVC4 code. See the respective projects for copyright and licensing @@ -108,7 +109,3 @@ version of GLPK, the GNU Linear Programming Kit, available here: https://github.com/timothy-king/glpk-cut-log -CVC4 can be optionally configured to link against GNU Readline for improved -text-editing support in interactive mode. GNU Readline is available here: - - http://cnswww.cns.cwru.edu/php/chet/readline/rltop.html diff --git a/INSTALL.md b/INSTALL.md index 2c73827c1..a5b048131 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -176,18 +176,12 @@ and-inverter-graphs (AIG) and ABC is used to simplify these AIGs. ABC can be installed using the `contrib/get-abc` script. Configure CVC4 with `configure.sh --abc` to build with this dependency. -### GNU Readline library (Improved Interactive Experience) +### Editline library (Improved Interactive Experience) -The [GNU Readline](http://cnswww.cns.cwru.edu/php/chet/readline/rltop.html) -library is optionally used to provide command editing, tab completion, and -history functionality at the CVC4 prompt (when running in interactive mode). -Check your distribution for a package named "libreadline-dev" or -"readline-devel" or similar. - -Note that GNU Readline is covered by the [GNU General Public License, version 3](https://www.gnu.org/licenses/gpl-3.0.en.html). -If you choose to use CVC4 with GNU Readline support, you are licensing CVC4 -under that same license. -(Usually CVC4's license is more permissive; see above discussion.) +The [Editline Library](https://thrysoee.dk/editline/) library is optionally +used to provide command editing, tab completion, and history functionality at +the CVC4 prompt (when running in interactive mode). Check your distribution +for a package named "libedit-dev" or "libedit-devel" or similar. ### Boost C++ base libraries (Examples) @@ -18,6 +18,10 @@ Improvements: Changes: * SyGuS: Removed support for SyGuS-IF 1.0. * Removed Java and Python bindings for the legacy API +* Interactive shell: the GPL-licensed Readline library has been replaced the + BSD-licensed Editline. Compiling with `--best` now enables Editline, instead + of Readline. Without selecting optional GPL components, Editline-enabled CVC4 + builds will be BSD licensed. Changes since 1.7 ================= diff --git a/cmake/FindEditline.cmake b/cmake/FindEditline.cmake new file mode 100644 index 000000000..fe4001173 --- /dev/null +++ b/cmake/FindEditline.cmake @@ -0,0 +1,40 @@ +# Find Editline +# Editline_FOUND - found Editline lib +# Editline_INCLUDE_DIR - the Editline include directory +# Editline_LIBRARIES - Libraries needed to use Editline +# Editline_COMPENTRY_FUNC_RETURNS_CHARPTR - Indicates if compentry function +# returns a (char *) + +find_path(Editline_INCLUDE_DIR NAMES histedit.h) +find_library(Editline_LIBRARIES NAMES edit libedit) + +if(Editline_INCLUDE_DIR) + # Check which standard of editline is installed on the system. + # https://github.com/CVC4/CVC4/issues/702 + include(CheckCXXSourceCompiles) + set(CMAKE_REQUIRED_QUIET TRUE) + set(CMAKE_REQUIRED_LIBRARIES ${Editline_LIBRARIES}) + set(CMAKE_REQUIRED_INCLUDES ${Editline_INCLUDE_DIR}) + check_cxx_source_compiles( + "#include <stdio.h> + #include <editline/readline.h> + char* foo(const char*, int) { return (char*)0; } + int main() { rl_completion_entry_function = foo; return 0; }" + Editline_COMPENTRY_FUNC_RETURNS_CHARPTR + ) + unset(CMAKE_REQUIRED_QUIET) + unset(CMAKE_REQUIRED_LIBRARIES) + unset(CMAKE_REQUIRED_INCLUDES) +endif() + +include(FindPackageHandleStandardArgs) +find_package_handle_standard_args(Editline + DEFAULT_MSG Editline_INCLUDE_DIR Editline_LIBRARIES) +mark_as_advanced( + Editline_INCLUDE_DIR + Editline_LIBRARIES + Editline_COMPENTRY_FUNC_RETURNS_CHARPTR +) +if(Editline_LIBRARIES) + message(STATUS "Editline library: ${Editline_LIBRARIES}") +endif() diff --git a/cmake/FindReadline.cmake b/cmake/FindReadline.cmake deleted file mode 100644 index edac03027..000000000 --- a/cmake/FindReadline.cmake +++ /dev/null @@ -1,69 +0,0 @@ -# Find Readline -# Readline_FOUND - system has Readline lib -# Readline_INCLUDE_DIR - the Readline include directory -# Readline_LIBRARIES - Libraries needed to use Readline -# Readline_COMPENTRY_FUNC_RETURNS_CHARPTR - Indicates if compentry function -# returns a (char *) - -find_path(Readline_INCLUDE_DIR NAMES readline/readline.h) -find_library(Readline_LIBRARIES NAMES readline) - -# Try to compile and link a simple program against readline. 'libs' can be -# used to specify additional required libraries. -function(try_compile_readline libs _result) - set(CMAKE_REQUIRED_QUIET TRUE) - set(CMAKE_REQUIRED_LIBRARIES ${Readline_LIBRARIES} ${libs}) - check_cxx_source_compiles( - " - #include <stdio.h> - #include <readline/readline.h> - int main() { readline(\"\"); return 0; } - " - ${_result} - ) - set(${_result} ${${_result}} PARENT_SCOPE) -endfunction() - -if(Readline_INCLUDE_DIR) - # We only need to figure out readline's additional libraries dependencies if - # we compile static. - # Note: It might be the case that we need to check for more/other libraries - # depending on what the installed version of readline is linked against - # (e.g., termcap, ncurses, ...). - find_library(TINFO_LIBRARY tinfo) - try_compile_readline(${TINFO_LIBRARY} OK) - if(OK) - list(APPEND Readline_LIBRARIES ${TINFO_LIBRARY}) - else() - message(FATAL_ERROR - "Could not link against readline. " - "Check CMakeError.log for more details") - endif() - - # Check which standard of readline is installed on the system. - # https://github.com/CVC4/CVC4/issues/702 - include(CheckCXXSourceCompiles) - set(CMAKE_REQUIRED_QUIET TRUE) - set(CMAKE_REQUIRED_LIBRARIES ${Readline_LIBRARIES}) - check_cxx_source_compiles( - "#include <stdio.h> - #include <readline/readline.h> - char* foo(const char*, int) { return (char*)0; } - int main() { rl_completion_entry_function = foo; return 0; }" - Readline_COMPENTRY_FUNC_RETURNS_CHARPTR - ) - unset(CMAKE_REQUIRED_QUIET) - unset(CMAKE_REQUIRED_LIBRARIES) -endif() - -include(FindPackageHandleStandardArgs) -find_package_handle_standard_args(Readline - DEFAULT_MSG Readline_INCLUDE_DIR Readline_LIBRARIES) -mark_as_advanced( - Readline_INCLUDE_DIR - Readline_LIBRARIES - Readline_COMPENTRY_FUNC_RETURNS_CHARPTR -) -if(Readline_LIBRARIES) - message(STATUS "Found Readline libs: ${Readline_LIBRARIES}") -endif() diff --git a/configure.sh b/configure.sh index f720e67c2..3bce5a548 100755 --- a/configure.sh +++ b/configure.sh @@ -64,7 +64,7 @@ The following flags enable optional packages (disable with --no-<option name>). --lfsc use the LFSC proof checker --poly use the LibPoly library --symfpu use SymFPU for floating point solver - --readline support the readline library + --editline support the editline library Optional Path to Optional Packages: --abc-dir=PATH path to top level of ABC source tree @@ -136,7 +136,7 @@ python2=default python3=default python_bindings=default java_bindings=default -readline=default +editline=default shared=default static_binary=default statistics=default @@ -295,8 +295,8 @@ do --profiling) profiling=ON;; --no-profiling) profiling=OFF;; - --readline) readline=ON;; - --no-readline) readline=OFF;; + --editline) editline=ON;; + --no-editline) editline=OFF;; --abc-dir) die "missing argument to $1 (try -h)" ;; --abc-dir=*) abc_dir=${1##*=} ;; @@ -409,8 +409,8 @@ cmake_opts="" && cmake_opts="$cmake_opts -DENABLE_VALGRIND=$valgrind" [ $profiling != default ] \ && cmake_opts="$cmake_opts -DENABLE_PROFILING=$profiling" -[ $readline != default ] \ - && cmake_opts="$cmake_opts -DUSE_READLINE=$readline" +[ $editline != default ] \ + && cmake_opts="$cmake_opts -DUSE_EDITLINE=$editline" [ $abc != default ] \ && cmake_opts="$cmake_opts -DUSE_ABC=$abc" [ $cadical != default ] \ diff --git a/cvc4autoconfig.h.in b/cvc4autoconfig.h.in index 1c9fdf605..603670a3a 100644 --- a/cvc4autoconfig.h.in +++ b/cvc4autoconfig.h.in @@ -43,8 +43,11 @@ /* Define if `ffs' is supported by the platform. */ #cmakedefine HAVE_FFS -/* Define to 1 to use libreadline. */ -#cmakedefine01 HAVE_LIBREADLINE +/* Define to 1 to use libedit. */ +#cmakedefine01 HAVE_LIBEDITLINE + +/* Define to 1 if `rl_completion_entry_function' returns (char *). */ +#cmakedefine01 EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP /* Define if `sigaltstack' is supported by the platform. */ #cmakedefine HAVE_SIGALTSTACK @@ -58,9 +61,6 @@ /* Define to 1 if the <unistd.h> header file is available. */ #cmakedefine01 HAVE_UNISTD_H -/* Define to 1 if `rl_completion_entry_function' returns (char *). */ -#cmakedefine01 READLINE_COMPENTRY_FUNC_RETURNS_CHARP - /* Define to 1 if `strerror_r' returns (char *). */ #cmakedefine01 STRERROR_R_CHAR_P 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); diff --git a/test/system/CMakeLists.txt b/test/system/CMakeLists.txt index 589ff0db7..a9c1a80db 100644 --- a/test/system/CMakeLists.txt +++ b/test/system/CMakeLists.txt @@ -34,4 +34,26 @@ cvc4_add_system_test(smt2_compliance) # TODO(cvc4-projects#209): Add methods for retrieving statistics to new API # cvc4_add_system_test(statistics) cvc4_add_system_test(two_solvers) + +# if we've built using libedit, then we want the interactive shell tests +if (USE_EDITLINE) + + # Check for pexpect -- zero return code is success + execute_process( + COMMAND ${PYTHON_EXECUTABLE} -c "import pexpect" + RESULT_VARIABLE PEXPECT_RC + ERROR_QUIET + ) + + # Add the test if we have pexpect + if(PEXPECT_RC EQUAL 0) + add_test( + NAME interactive_shell + COMMAND + "${PYTHON_EXECUTABLE}" "${CMAKE_SOURCE_DIR}/test/system/interactive_shell.py" + WORKING_DIRECTORY "${CMAKE_BINARY_DIR}" + ) + endif() +endif() + # TODO: Move CVC4JavaTest.java to test/java and delete run_java_test (after full cmake migration) diff --git a/test/system/interactive_shell.py b/test/system/interactive_shell.py new file mode 100755 index 000000000..3cc9953ee --- /dev/null +++ b/test/system/interactive_shell.py @@ -0,0 +1,94 @@ +#!/usr/bin/env python3 + +##################### +#! \file interactive_shell.py +## \verbatim +## Top contributors (to current version): +## Andrew V. Jones +## This file is part of the CVC4 project. +## Copyright (c) 2020 by the authors listed in the file AUTHORS +## in the top-level source directory) and their institutional affiliations. +## All rights reserved. See the file COPYING in the top-level source +## directory for licensing information.\endverbatim +## +## \brief A simple test file to interact with CVC4 with line editing +##################### + +import sys +import pexpect + +def check_iteractive_shell(): + """ + Interacts with CVC4's interactive shell and checks that things such a tab + completion and "pressing up" works. + """ + + # Open CVC4 + child = pexpect.spawnu("bin/cvc4", timeout=1) + + # We expect to see the CVC4 prompt + child.expect("CVC4>") + + # If we send a line with just 'BOOLE' ... + child.sendline("BOOLE") + + # ... then we get an error + child.expect("Parse Error: <shell>:...: Unexpected token: 'BOOLE'") + + # Start sending 'BOOL' (without an E) + child.send("BOOL") + + # Send tab twice + child.sendcontrol("i") + child.sendcontrol("i") + + # We expect to see the completion + child.expect("BOOL.*BOOLEAN.*BOOLEXTRACT") + + # NOTE: the double tab has completed our 'BOOL' to 'BOOLE'! + + # Now send enter (which submits 'BOOLE') + child.sendcontrol("m") + + # So we expect to see an error for 'BOOLE' + child.expect("Parse Error: <shell>:...: Unexpected token: 'BOOLE'") + + # Send enter + child.sendcontrol("m") + + # We expect to see the CVC4 prompt + child.expect("CVC4>") + + # Now send an up key + child.send("\033[A") + + # Send enter + child.sendcontrol("m") + + # We expect to see an error on 'BOOLE' again + child.expect("Parse Error: <shell>:...: Unexpected token: 'BOOLE'") + + return 0 + + +def main(): + """ + Runs our interactive shell test + + Caveats: + + * If we don't have the "pexpect" model, the test doesn't get run, but + passes + + * We expect pexpect to raise and exit with a non-zero exit code if any + of the steps fail + """ + + # If any of the "steps" fail, the pexpect will raise a Python will exit + # with a non-zero error code + sys.exit(check_iteractive_shell()) + +if __name__ == "__main__": + main() + +# EOF |