include:
- name: production
- config: production --all-bindings --lfsc
+ config: production --all-bindings --lfsc --editline
cache-key: production
python-bindings: true
check-examples: true
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
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: |
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.
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")
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
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()
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)
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
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
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
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)
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
=================
--- /dev/null
+# 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()
+++ /dev/null
-# 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()
--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
python3=default
python_bindings=default
java_bindings=default
-readline=default
+editline=default
shared=default
static_binary=default
statistics=default
--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##*=} ;;
&& 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 ] \
/* 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
/* 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
|| 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";
<< " 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())
}
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";
<< " 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"
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;
static bool isBuiltWithDrat2Er();
- static bool isBuiltWithReadline();
+ static bool isBuiltWithEditline();
static bool isBuiltWithLfsc();
#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
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()
#-----------------------------------------------------------------------------#
** \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"
#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"
const string InteractiveShell::INPUT_FILENAME = "<shell>";
-#if HAVE_LIBREADLINE
+#if HAVE_LIBEDITLINE
#if HAVE_EXT_STDIO_FILEBUF_H
using __gnu_cxx::stdio_filebuf;
static set<string> s_declarations;
-#endif /* HAVE_LIBREADLINE */
+#endif /* HAVE_LIBEDITLINE */
InteractiveShell::InteractiveShell(api::Solver* solver)
: d_options(solver->getOptions()),
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());
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()) {
}
}
} 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 "
Notice() << "Could not write history to " << d_historyFilename
<< ": " << strerror(err) << std::endl;
}
-#endif /* HAVE_LIBREADLINE */
+#endif /* HAVE_LIBEDITLINE */
delete d_parser;
}
}
/* 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') {
}
line += lineBuf == NULL ? "" : lineBuf;
free(lineBuf);
-#endif /* HAVE_LIBREADLINE */
- } else {
+#endif /* HAVE_LIBEDITLINE */
+ }
+ else
+ {
if(d_options.getInteractivePrompt()) {
if(line == "") {
d_out << "CVC4> " << flush;
}
/* 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()) {
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');
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;
}
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) {
} else if(dynamic_cast<DefineTypeCommand*>(cmd) != NULL) {
s_declarations.insert(dynamic_cast<DefineTypeCommand*>(cmd)->getSymbol());
}
-#endif /* HAVE_LIBREADLINE */
+#endif /* HAVE_LIBEDITLINE */
}
}
} catch(ParserEndOfFileException& pe) {
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;
return *rlDeclaration == jj ? NULL : strdup((*(*rlDeclaration)++).c_str());
}
-#endif /* HAVE_LIBREADLINE */
+#endif /* HAVE_LIBEDITLINE */
}/* CVC4 namespace */
std::ostream& d_out;
parser::Parser* d_parser;
bool d_quit;
- bool d_usingReadline;
+ bool d_usingEditline;
std::string d_historyFilename;
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);
# 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)
--- /dev/null
+#!/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
projects / cvc5.git / commitdiff