diff options
-rw-r--r-- | NEWS | 1 | ||||
-rw-r--r-- | README.interactive | 2 | ||||
-rw-r--r-- | src/main/interactive_shell.cpp | 46 | ||||
-rw-r--r-- | src/parser/antlr_input.cpp | 14 | ||||
-rw-r--r-- | src/parser/antlr_input.h | 2 | ||||
-rw-r--r-- | src/parser/antlr_input_imports.cpp | 2 | ||||
-rw-r--r-- | src/parser/cvc/Cvc.g | 3 | ||||
-rw-r--r-- | src/parser/input.h | 2 | ||||
-rw-r--r-- | src/parser/parser_exception.h | 24 | ||||
-rw-r--r-- | test/unit/main/interactive_shell_black.h | 4 |
10 files changed, 74 insertions, 26 deletions
@@ -10,6 +10,7 @@ Changes since 1.0 * for printing commands as they're invoked from the driver, you now need verbosity of 3 or higher (e.g. -vvv) instead of verbosity 1 or higher (-v). This allows tracing the solver's activities without having too much output. +* multiline support in interactive mode * To make CVC4 quieter in abnormal (e.g., "warning" conditions), you can use -q. Previously, this would silence all output (including "sat" or "unsat") as well. Now, single -q silences messages and warnings, and diff --git a/README.interactive b/README.interactive new file mode 100644 index 000000000..2fcc6c2fb --- /dev/null +++ b/README.interactive @@ -0,0 +1,2 @@ +The interactive branch is intended to merge the user-interactive +and tool-interactive modes. diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index c1d2c2bb1..cba896e4e 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -162,9 +162,15 @@ InteractiveShell::~InteractiveShell() { } Command* InteractiveShell::readCommand() { + char* lineBuf = NULL; + string line = ""; + +restart: + /* Don't do anything if the input is closed or if we've seen a * QuitCommand. */ - if( d_in.eof() || d_quit ) { + if(d_in.eof() || d_quit) { + d_out << endl; return NULL; } @@ -173,30 +179,32 @@ Command* InteractiveShell::readCommand() { throw ParserException("Interactive input broken."); } - char* lineBuf = NULL; - string input; - stringbuf sb; - string line; - /* Prompt the user for input. */ if(d_usingReadline) { #if HAVE_LIBREADLINE - lineBuf = ::readline(d_options[options::verbosity] >= 0 ? "CVC4> " : ""); + lineBuf = ::readline(d_options[options::verbosity] >= 0 ? (line == "" ? "CVC4> " : "... > ") : ""); if(lineBuf != NULL && lineBuf[0] != '\0') { ::add_history(lineBuf); } - line = lineBuf == NULL ? "" : lineBuf; + line += lineBuf == NULL ? "" : lineBuf; free(lineBuf); #endif /* HAVE_LIBREADLINE */ } else { if(d_options[options::verbosity] >= 0) { - d_out << "CVC4> " << flush; + if(line == "") { + d_out << "CVC4> " << flush; + } else { + d_out << "... > " << flush; + } } /* Read a line */ - d_in.get(sb,'\n'); - line = sb.str(); + stringbuf sb; + d_in.get(sb); + line += sb.str(); } + + string input = ""; while(true) { Debug("interactive") << "Input now '" << input << line << "'" << endl << flush; @@ -221,20 +229,24 @@ Command* InteractiveShell::readCommand() { (d_usingReadline && lineBuf == NULL) ) { input += line; - if( input.empty() ) { + if(input.empty()) { /* Nothing left to parse. */ + d_out << endl; return NULL; } /* Some input left to parse, but nothing left to read. Jump out of input loop. */ - break; + d_out << endl; + input = line = ""; + d_in.clear(); + goto restart; } if(!d_usingReadline) { /* Extract the newline delimiter from the stream too */ int c CVC4_UNUSED = d_in.get(); - assert( c == '\n' ); + assert(c == '\n'); Debug("interactive") << "Next char is '" << (char)c << "'" << endl << flush; } @@ -259,7 +271,8 @@ Command* InteractiveShell::readCommand() { } /* Read a line */ - d_in.get(sb,'\n'); + stringbuf sb; + d_in.get(sb); line = sb.str(); } } else { @@ -296,6 +309,9 @@ Command* InteractiveShell::readCommand() { #endif /* HAVE_LIBREADLINE */ } } + } catch(ParserEndOfFileException& pe) { + line += "\n"; + goto restart; } catch(ParserException& pe) { d_out << pe << endl; // We can't really clear out the sequence and abort the current line, diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index fbf2b8650..2279865ae 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -283,16 +283,22 @@ void AntlrInput::warning(const std::string& message) { Warning() << getInputStream()->getName() << ':' << d_lexer->getLine(d_lexer) << '.' << d_lexer->getCharPositionInLine(d_lexer) << ": " << message << endl; } -void AntlrInput::parseError(const std::string& message) +void AntlrInput::parseError(const std::string& message, bool eofException) throw (ParserException) { Debug("parser") << "Throwing exception: " << getInputStream()->getName() << ":" << d_lexer->getLine(d_lexer) << "." << d_lexer->getCharPositionInLine(d_lexer) << ": " << message << endl; - throw ParserException(message, getInputStream()->getName(), - d_lexer->getLine(d_lexer), - d_lexer->getCharPositionInLine(d_lexer)); + if(eofException) { + throw ParserEndOfFileException(message, getInputStream()->getName(), + d_lexer->getLine(d_lexer), + d_lexer->getCharPositionInLine(d_lexer)); + } else { + throw ParserException(message, getInputStream()->getName(), + d_lexer->getLine(d_lexer), + d_lexer->getCharPositionInLine(d_lexer)); + } } diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index a2fe99f52..020db0d50 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -209,7 +209,7 @@ protected: /** * Throws a <code>ParserException</code> with the given message. */ - void parseError(const std::string& msg) + void parseError(const std::string& msg, bool eofException = false) throw (ParserException); /** Set the ANTLR3 lexer for this input. */ diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp index 9c92846bb..07283f1af 100644 --- a/src/parser/antlr_input_imports.cpp +++ b/src/parser/antlr_input_imports.cpp @@ -261,7 +261,7 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { } // Call the error display routine - input->parseError(ss.str()); + input->parseError(ss.str(), ((pANTLR3_COMMON_TOKEN)ex->token)->type == ANTLR3_TOKEN_EOF); } /// diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index b8ec160e8..e5e26c9a2 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -625,8 +625,7 @@ mainCommand[CVC4::Command*& cmd] : ASSERT_TOK formula[f] { cmd = new AssertCommand(f); } | QUERY_TOK formula[f] { cmd = new QueryCommand(f); } - | CHECKSAT_TOK formula[f] { cmd = new CheckSatCommand(f); } - | CHECKSAT_TOK { cmd = new CheckSatCommand(); } + | CHECKSAT_TOK formula[f]? { cmd = f.isNull() ? new CheckSatCommand() : new CheckSatCommand(f); } /* options */ | OPTION_TOK diff --git a/src/parser/input.h b/src/parser/input.h index f4b36469b..5fd3611be 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -178,7 +178,7 @@ protected: /** * Throws a <code>ParserException</code> with the given message. */ - virtual void parseError(const std::string& msg) + virtual void parseError(const std::string& msg, bool eofException = false) throw (ParserException) = 0; /** Parse an expression from the input by invoking the diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h index 8abc04c15..6eae3047d 100644 --- a/src/parser/parser_exception.h +++ b/src/parser/parser_exception.h @@ -89,6 +89,30 @@ protected: unsigned long d_column; };/* class ParserException */ +class CVC4_PUBLIC ParserEndOfFileException : public ParserException { +public: + + // Constructors same as ParserException's + + ParserEndOfFileException() throw() : + ParserException() { + } + + ParserEndOfFileException(const std::string& msg) throw() : + ParserException(msg) { + } + + ParserEndOfFileException(const char* msg) throw() : + ParserException(msg) { + } + + ParserEndOfFileException(const std::string& msg, const std::string& filename, + unsigned long line, unsigned long column) throw() : + ParserException(msg, filename, line, column) { + } + +};/* class ParserEndOfFileException */ + }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h index 664027c49..66fcabed0 100644 --- a/test/unit/main/interactive_shell_black.h +++ b/test/unit/main/interactive_shell_black.h @@ -69,13 +69,13 @@ private: } void testAssertTrue() { - *d_sin << "ASSERT TRUE;" << flush; + *d_sin << "ASSERT TRUE;\n" << flush; InteractiveShell shell(*d_exprManager, d_options); countCommands( shell, 1, 1 ); } void testQueryFalse() { - *d_sin << "QUERY FALSE;" << flush; + *d_sin << "QUERY FALSE;\n" << flush; InteractiveShell shell(*d_exprManager, d_options); countCommands( shell, 1, 1 ); } |