Interactive mode support for multiline input

6 files changed, 38 insertions, 9 deletions

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 */