Interactive mode support for multiline input

10 files changed, 74 insertions, 26 deletions

diff --git a/NEWS b/NEWS
index ba396ad0c..3c38aab56 100644
--- a/NEWS
+++ b/NEWS
@@ -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 );
   }