diff options
| -rw-r--r-- | config/readline.m4 | 25 | ||||
| -rw-r--r-- | configure.ac | 3 | ||||
| -rw-r--r-- | src/expr/command.cpp | 17 | ||||
| -rw-r--r-- | src/expr/command.h | 8 | ||||
| -rw-r--r-- | src/main/Makefile.am | 21 | ||||
| -rw-r--r-- | src/main/interactive_shell.cpp | 249 | ||||
| -rw-r--r-- | src/main/interactive_shell.h | 2 | ||||
| -rw-r--r-- | src/parser/smt2/Smt2.g | 2 | ||||
| -rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 2 | ||||
| -rw-r--r-- | test/unit/Makefile.am | 2 |
10 files changed, 288 insertions, 43 deletions
diff --git a/config/readline.m4 b/config/readline.m4 new file mode 100644 index 000000000..4ebe6bce3 --- /dev/null +++ b/config/readline.m4 @@ -0,0 +1,25 @@ +# CVC4_CHECK_FOR_READLINE +# ----------------------- +# Look for readline and link it in, but allow user to disable. +AC_DEFUN([CVC4_CHECK_FOR_READLINE], [ +AC_MSG_CHECKING([whether user requested readline support]) +AC_ARG_WITH([readline], [AS_HELP_STRING([--with-readline], [support the readline library])], [], [with_readline=check]) +LIBREADLINE= +if test "$with_readline" = no; then + AC_MSG_RESULT([no, readline disabled by user]) +else + if test "$with_readline" = check; then + AC_MSG_RESULT([no preference by user, will auto-detect]) + else + AC_MSG_RESULT([yes, readline enabled by user]) + fi + AC_CHECK_LIB([readline], [readline], + [AC_CHECK_HEADER([readline/readline.h], + AC_SUBST([READLINE_LDFLAGS], ["-lreadline -lncurses"]) + AC_DEFINE([HAVE_LIBREADLINE], [1], [Define to 1 to use libreadline]))], + [if test "$with_readline" != check; then + AC_MSG_FAILURE([cannot find libreadline!]) + fi], -lncurses) +fi +])# CVC4_CHECK_FOR_READLINE + diff --git a/configure.ac b/configure.ac index 8ab087a22..9082fb6ff 100644 --- a/configure.ac +++ b/configure.ac @@ -669,6 +669,9 @@ fi AC_CHECK_LIB(z, gzread, , [AC_MSG_ERROR([zlib required, install your distro's zlib-dev package or see www.zlib.net])]) AC_CHECK_HEADER(zlib.h, , [AC_MSG_ERROR([zlib required, install your distro's zlib-dev package or see www.zlib.net])]) +# Check for libreadline (defined in config/readline.m4) +CVC4_CHECK_FOR_READLINE + AC_SEARCH_LIBS([clock_gettime], [rt], [AC_DEFINE([HAVE_CLOCK_GETTIME], [1], [Defined to 1 if clock_gettime() is supported by the platform.])], diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 48cf4ea93..d300b27de 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -158,6 +158,15 @@ void QueryCommand::toStream(std::ostream& out) const { out << "Query(" << d_expr << ')'; } +/* class QuitCommand */ + +QuitCommand::QuitCommand() { +} + +void QuitCommand::toStream(std::ostream& out) const { + out << "Quit()" << endl; +} + /* class CommandSequence */ CommandSequence::CommandSequence() : @@ -208,6 +217,14 @@ DeclarationCommand::DeclarationCommand(const std::vector<std::string>& ids, Type d_type(t) { } +const std::vector<std::string>& DeclarationCommand::getDeclaredSymbols() const { + return d_declaredSymbols; +} + +Type DeclarationCommand::getDeclaredType() const { + return d_type; +} + void DeclarationCommand::toStream(std::ostream& out) const { out << "Declare(["; copy( d_declaredSymbols.begin(), d_declaredSymbols.end() - 1, diff --git a/src/expr/command.h b/src/expr/command.h index 585e60eb4..17736ed77 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -108,6 +108,8 @@ protected: public: DeclarationCommand(const std::string& id, Type t); DeclarationCommand(const std::vector<std::string>& ids, Type t); + const std::vector<std::string>& getDeclaredSymbols() const; + Type getDeclaredType() const; void toStream(std::ostream& out) const; };/* class DeclarationCommand */ @@ -276,6 +278,12 @@ public: void toStream(std::ostream& out) const; };/* class DatatypeDeclarationCommand */ +class CVC4_PUBLIC QuitCommand : public EmptyCommand { +public: + QuitCommand(); + void toStream(std::ostream& out) const; +};/* class QuitCommand */ + class CVC4_PUBLIC CommandSequence : public Command { private: /** All the commands to be executed (in sequence) */ diff --git a/src/main/Makefile.am b/src/main/Makefile.am index 764d5e062..669ab6fa2 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -19,7 +19,26 @@ cvc4_LDADD = \ libmain.a \ ../parser/libcvc4parser.la \ ../libcvc4.la \ - ../lib/libreplacements.la + ../lib/libreplacements.la \ + $(READLINE_LDFLAGS) + +BUILT_SOURCES = \ + $(TOKENS_FILES) + +TOKENS_FILES = \ + cvc_tokens.h \ + smt_tokens.h \ + smt2_tokens.h + +cvc_tokens.h: @srcdir@/../parser/cvc/Cvc.g + $(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9][a-zA-Z0-9]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9]\+\)'\''.*/"\1",/' | sort -u >$@ +smt_tokens.h: @srcdir@/../parser/smt/Smt.g + $(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9][a-zA-Z0-9]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9]\+\)'\''.*/"\1",/' | sort -u >$@ +smt2_tokens.h: @srcdir@/../parser/smt2/Smt2.g + $(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9][a-zA-Z0-9]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9]\+\)'\''.*/"\1",/' | sort -u >$@ + +clean-local: + rm -f $(BUILT_SOURCES) if STATIC_BINARY cvc4_LINK = $(CXXLINK) -all-static diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index cd7947e2e..cf04dacdf 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -12,9 +12,19 @@ ** information.\endverbatim ** ** \brief Interactive shell for CVC4 + ** + ** This file is the implementation for the CVC4 interactive shell. + ** The shell supports the readline library. **/ #include <iostream> +#include <vector> +#include <string> +#include <set> +#include <algorithm> +#include <utility> + +#include "cvc4autoconfig.h" #include "interactive_shell.h" @@ -23,29 +33,95 @@ #include "parser/parser.h" #include "parser/parser_builder.h" #include "util/options.h" +#include "util/language.h" + +#include <string.h> + +#if HAVE_LIBREADLINE +# include <readline/readline.h> +# include <readline/history.h> +# include <ext/stdio_filebuf.h> +#endif /* HAVE_LIBREADLINE */ using namespace std; namespace CVC4 { using namespace parser; +using namespace language; const string InteractiveShell::INPUT_FILENAME = "<shell>"; +#if HAVE_LIBREADLINE + +using __gnu_cxx::stdio_filebuf; + +//char** commandCompletion(const char* text, int start, int end); +char* commandGenerator(const char* text, int state); + +static const char* const cvc_commands[] = { +#include "cvc_tokens.h" +};/* cvc_commands */ + +static const char* const smt_commands[] = { +#include "smt_tokens.h" +};/* smt_commands */ + +static const char* const smt2_commands[] = { +#include "smt2_tokens.h" +};/* smt2_commands */ + +static const char* const* commandsBegin; +static const char* const* commandsEnd; + +static set<string> s_declarations; + +#endif /* HAVE_LIBREADLINE */ + InteractiveShell::InteractiveShell(ExprManager& exprManager, - const Options& options) : - d_in(*options.in), - d_out(*options.out), - d_language(options.inputLanguage) { - ParserBuilder parserBuilder(&exprManager,INPUT_FILENAME,options); - /* Create parser with bogus input. */ - d_parser = parserBuilder.withStringInput("").build(); + const Options& options) : + d_in(*options.in), + d_out(*options.out), + d_language(options.inputLanguage), + d_quit(false) { + ParserBuilder parserBuilder(&exprManager,INPUT_FILENAME,options); + /* Create parser with bogus input. */ + d_parser = parserBuilder.withStringInput("").build(); + +#if HAVE_LIBREADLINE + if(d_in == cin) { + ::rl_readline_name = "CVC4"; + ::rl_completion_entry_function = commandGenerator; + + switch(OutputLanguage lang = toOutputLanguage(d_language)) { + case output::LANG_CVC4: + commandsBegin = cvc_commands; + commandsEnd = cvc_commands + sizeof(cvc_commands) / sizeof(*cvc_commands); + break; + case output::LANG_SMTLIB: + commandsBegin = smt_commands; + commandsEnd = smt_commands + sizeof(smt_commands) / sizeof(*smt_commands); + break; + case output::LANG_SMTLIB_V2: + commandsBegin = smt2_commands; + commandsEnd = smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands); + break; + default: Unhandled(lang); + } + d_usingReadline = true; + } else { + d_usingReadline = false; + } +#else /* HAVE_LIBREADLINE */ + d_usingReadline = false; +#endif /* HAVE_LIBREADLINE */ }/* InteractiveShell::InteractiveShell() */ Command* InteractiveShell::readCommand() { - /* Don't do anything if the input is closed. */ - if( d_in.eof() ) { + /* Don't do anything if the input is closed or if we've seen a + * QuitCommand. */ + if( d_in.eof() || d_quit ) { return NULL; } @@ -54,23 +130,35 @@ Command* InteractiveShell::readCommand() { throw ParserException("Interactive input broken."); } + char* lineBuf; string input; + stringbuf sb; + string line; /* Prompt the user for input. */ - d_out << "CVC4> " << flush; - while(true) { - stringbuf sb; - string line; + if(d_usingReadline) { +#if HAVE_LIBREADLINE + lineBuf = ::readline("CVC4> "); + if(lineBuf != NULL && lineBuf[0] != '\0') { + ::add_history(lineBuf); + } + line = lineBuf == NULL ? "" : lineBuf; + free(lineBuf); +#endif /* HAVE_LIBREADLINE */ + } else { + d_out << "CVC4> " << flush; /* Read a line */ d_in.get(sb,'\n'); line = sb.str(); - // cout << "Input was '" << input << "'" << endl << flush; + } + while(true) { + Debug("interactive") << "Input now '" << input << line << "'" << endl << flush; Assert( !(d_in.fail() && !d_in.eof()) || line.empty() ); /* Check for failure. */ - if( d_in.fail() && !d_in.eof() ) { + if(d_in.fail() && !d_in.eof()) { /* This should only happen if the input line was empty. */ Assert( line.empty() ); d_in.clear(); @@ -78,13 +166,14 @@ Command* InteractiveShell::readCommand() { /* Strip trailing whitespace. */ int n = line.length() - 1; - while( !line.empty() && isspace(line[n]) ) { - line.erase(n,1); + while( !line.empty() && isspace(line[n]) ) { + line.erase(n,1); n--; } /* If we hit EOF, we're done. */ - if( d_in.eof() ) { + if( (!d_usingReadline && d_in.eof()) || + (d_usingReadline && lineBuf == NULL) ) { input += line; if( input.empty() ) { @@ -92,54 +181,136 @@ Command* InteractiveShell::readCommand() { return NULL; } - /* Some input left to parse, but nothing left to read. + /* Some input left to parse, but nothing left to read. Jump out of input loop. */ break; } - /* Extract the newline delimiter from the stream too */ - int c CVC4_UNUSED = d_in.get(); - Assert( c == '\n' ); - - // cout << "Next char is '" << (char)c << "'" << endl << flush; + if(!d_usingReadline) { + /* Extract the newline delimiter from the stream too */ + int c CVC4_UNUSED = d_in.get(); + Assert( c == '\n' ); + Debug("interactive") << "Next char is '" << (char)c << "'" << endl << flush; + } input += line; - + /* If the last char was a backslash, continue on the next line. */ n = input.length() - 1; if( !line.empty() && input[n] == '\\' ) { input[n] = '\n'; - d_out << "... > " << flush; + if(d_usingReadline) { +#if HAVE_LIBREADLINE + lineBuf = ::readline("... > "); + if(lineBuf != NULL && lineBuf[0] != '\0') { + ::add_history(lineBuf); + } + line = lineBuf == NULL ? "" : lineBuf; + free(lineBuf); +#endif /* HAVE_LIBREADLINE */ + } else { + d_out << "... > " << flush; + + /* Read a line */ + d_in.get(sb,'\n'); + line = sb.str(); + } } else { /* No continuation, we're done. */ - //cout << "Leaving input loop." << endl << flush; + Debug("interactive") << "Leaving input loop." << endl << flush; break; } } d_parser->setInput(Input::newStringInput(d_language,input,INPUT_FILENAME)); - // Parser *parser = - // d_parserBuilder - // .withStringInput(input) - // .withStateFrom(d_lastParser) - // .build(); /* There may be more than one command in the input. Build up a sequence. */ CommandSequence *cmd_seq = new CommandSequence(); Command *cmd; - while( (cmd = d_parser->nextCommand()) ) { - cmd_seq->addCommand(cmd); + try { + while( (cmd = d_parser->nextCommand()) ) { + cmd_seq->addCommand(cmd); + if(dynamic_cast<QuitCommand*>(cmd) != NULL) { + d_quit = true; + break; + } else { +#if HAVE_LIBREADLINE + DeclarationCommand* dcmd = + dynamic_cast<DeclarationCommand*>(cmd); + if(dcmd != NULL) { + const vector<string>& ids = dcmd->getDeclaredSymbols(); + s_declarations.insert(ids.begin(), ids.end()); + } +#endif /* HAVE_LIBREADLINE */ + } + } + } catch(ParserException& pe) { + d_out << pe << endl; + // We can't really clear out the sequence and abort the current line, + // because the parse error might be for the second command on the + // line. The first ones haven't yet been executed by the SmtEngine, + // but the parser state has already made the variables and the mappings + // in the symbol table. So unfortunately, either we exit CVC4 entirely, + // or we commit to the current line up to the command with the parse + // error. + // + // FIXME: does that mean e.g. that a pushed LET scope might not yet have + // been popped?! + // + //delete cmd_seq; + //cmd_seq = new CommandSequence(); } - // if( d_lastParser ) { - // delete d_lastParser; - // } - // d_lastParser = parser; - return cmd_seq; }/* InteractiveShell::readCommand() */ +#if HAVE_LIBREADLINE + +/*char** commandCompletion(const char* text, int start, int end) { + Debug("rl") << "text: " << text << endl; + Debug("rl") << "start: " << start << " end: " << end << endl; + return rl_completion_matches(text, commandGenerator); +}*/ + +// For some reason less<string> crashes on us; oh well, +// we don't need to copy into string anyway. +// Can't use less<const char*> because it compares pointers(?). +struct stringLess { + bool operator()(const char* s1, const char* s2) { + size_t l1 = strlen(s1), l2 = strlen(s2); + return strncmp(s1, s2, l1 <= l2 ? l1 : l2) == -1; + } +};/* struct string_less */ + +char* commandGenerator(const char* text, int state) { + static CVC4_THREADLOCAL(const char* const*) rlPointer; + static CVC4_THREADLOCAL(set<string>::const_iterator*) rlDeclaration; + + const char* const* i = lower_bound(commandsBegin, commandsEnd, text, stringLess()); + const char* const* j = upper_bound(commandsBegin, commandsEnd, text, stringLess()); + + set<string>::const_iterator ii = lower_bound(s_declarations.begin(), s_declarations.end(), text, less<string>()); + set<string>::const_iterator jj = upper_bound(s_declarations.end(), s_declarations.end(), text, less<string>()); + + if(rlDeclaration == NULL) { + rlDeclaration = new set<string>::const_iterator(); + } + + if(state == 0) { + rlPointer = i; + *rlDeclaration = ii; + } + + if(rlPointer != j) { + return strdup(*rlPointer++); + } + + return *rlDeclaration == jj ? NULL : strdup((*(*rlDeclaration)++).c_str()); +} + +#endif /* HAVE_LIBREADLINE */ + }/* CVC4 namespace */ diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h index a08e2cbb4..4fa2d6e96 100644 --- a/src/main/interactive_shell.h +++ b/src/main/interactive_shell.h @@ -37,6 +37,8 @@ class CVC4_PUBLIC InteractiveShell { std::ostream& d_out; parser::Parser* d_parser; const InputLanguage d_language; + bool d_quit; + bool d_usingReadline; static const std::string INPUT_FILENAME; diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 9466f8753..17ea1611d 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -300,7 +300,7 @@ command returns [CVC4::Command* cmd] } } | EXIT_TOK - { cmd = NULL; } + { cmd = new QuitCommand; } ; symbolicExpr[CVC4::SExpr& sexpr] diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 77696465c..b2b801ded 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -280,7 +280,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, case kind::BITVECTOR_CONCAT: out << '('; for(unsigned i = 0; i < n.getNumChildren() - 1; ++i) { - cout << n[i] << ' ' << n.getOperator(); + out << n[i] << ' ' << n.getOperator(); } out << n[n.getNumChildren() - 1] << ')'; diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 691f33406..42f6592ea 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -74,7 +74,7 @@ AM_CPPFLAGS = \ $(ANTLR_INCLUDES) \ $(TEST_CPPFLAGS) AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(TEST_CXXFLAGS) -AM_LDFLAGS = $(TEST_LDFLAGS) +AM_LDFLAGS = $(TEST_LDFLAGS) $(READLINE_LDFLAGS) AM_CXXFLAGS_WHITE = -fno-access-control -D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST AM_CXXFLAGS_BLACK = -D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST |