Adding support for interactive mode

5 files changed, 33 insertions, 50 deletions

diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index e55e07efd..d86a18004 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -180,6 +180,8 @@ public:
   /** Get a bitvector constant from the text of the number and the size token */
   static BitVector tokenToBitvector(pANTLR3_COMMON_TOKEN number, pANTLR3_COMMON_TOKEN size);
 
+  std::string getUnparsedText();
+
 protected:
   /** Create an input. This input takes ownership of the given input stream,
    * and will delete it at destruction time.
@@ -210,6 +212,14 @@ protected:
   virtual void setParser(Parser& parser);
 };
 
+inline std::string AntlrInput::getUnparsedText() {
+  const char *base = (const char *)d_antlr3InputStream->data;
+  const char *cur = (const char *)d_antlr3InputStream->nextChar;
+
+  return std::string(cur, d_antlr3InputStream->sizeBuf - (cur - base));
+}
+
+
 inline std::string AntlrInput::tokenText(pANTLR3_COMMON_TOKEN token) {
   ANTLR3_MARKER start = token->getStartIndex(token);
   ANTLR3_MARKER end = token->getStopIndex(token);
diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp
index a1ebee523..2805d518a 100644
--- a/src/parser/antlr_input_imports.cpp
+++ b/src/parser/antlr_input_imports.cpp
@@ -56,6 +56,7 @@
 
 #include "antlr_input.h"
 #include "parser.h"
+#include "parser_exception.h"
 #include "util/Assert.h"
 
 using namespace std;
@@ -89,6 +90,14 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) {
   pANTLR3_UINT8 * tokenNames = recognizer->state->tokenNames;
   stringstream ss;
 
+  // Dig the CVC4 objects out of the ANTLR3 mess
+  pANTLR3_PARSER antlr3Parser = (pANTLR3_PARSER)(recognizer->super);
+  AlwaysAssert(antlr3Parser!=NULL);
+  Parser *parser = (Parser*)(antlr3Parser->super);
+  AlwaysAssert(parser!=NULL);
+  AntlrInput *input = (AntlrInput*) parser->getInput() ;
+  AlwaysAssert(input!=NULL);
+
   // Signal we are in error recovery now
   recognizer->state->errorRecovery = ANTLR3_TRUE;
 
@@ -252,14 +261,6 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) {
     break;
   }
 
-  // Now get ready to throw an exception
-  pANTLR3_PARSER antlr3Parser = (pANTLR3_PARSER)(recognizer->super);
-  AlwaysAssert(antlr3Parser!=NULL);
-  Parser *parser = (Parser*)(antlr3Parser->super);
-  AlwaysAssert(parser!=NULL);
-  AntlrInput *input = (AntlrInput*) parser->getInput() ;
-  AlwaysAssert(input!=NULL);
-
   // Call the error display routine
   input->parseError(ss.str());
 }
diff --git a/src/parser/input.h b/src/parser/input.h
index 1a90a4191..7cfafe429 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -47,7 +47,7 @@ public:
   virtual ~InputStreamException() throw() { }
 };
 
-/** Wrapper around an ANTLR3 input stream. */
+/** Wrapper around an input stream. */
 class InputStream {
 
   /** The name of this input stream. */
@@ -93,7 +93,7 @@ class CVC4_PUBLIC Input {
   /** The input stream. */
   InputStream *d_inputStream;
 
-  /* Since we own d_tokenStream and it needs to be freed, we need to prevent
+  /* Since we own d_inputStream and it needs to be freed, we need to prevent
    * copy construction and assignment.
    */
   Input(const Input& input) { Unimplemented("Copy constructor for Input."); }
@@ -134,9 +134,12 @@ class CVC4_PUBLIC Input {
 
 public:
 
-  /** Destructor. Frees the token stream and closes the input. */
+  /** Destructor. Frees the input stream and closes the input. */
   virtual ~Input();
 
+  /** Retrieve the remaining text in this input. */
+  virtual std::string getUnparsedText() = 0;
+
 protected:
 
   /** Create an input.
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 4d1e64176..280bd3c97 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -160,12 +160,6 @@ public:
     return d_input;
   }
 
-  /** Set the declaration scope manager for this input. NOTE: This should <em>only</me> be
-   * called before parsing begins. Otherwise, previous declarations will be lost. */
-/*  inline void setDeclarationScope(DeclarationScope declScope) {
-    d_declScope = declScope;
-  }*/
-
   /**
    * Check if we are done -- either the end of input has been reached, or some
    * error has been encountered.
@@ -189,7 +183,8 @@ public:
   /** Enable strict parsing, according to the language standards. */
   void enableStrictMode() { d_strictMode = true; }
 
-  /** Disable strict parsing. Allows certain syntactic infelicities to pass without comment. */
+  /** Disable strict parsing. Allows certain syntactic infelicities to
+      pass without comment. */
   void disableStrictMode() { d_strictMode = false; }
 
   bool strictModeEnabled() { return d_strictMode; }
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index f53d7cc9c..dcc052c3a 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -84,46 +84,20 @@ Parser *ParserBuilder::build() throw (InputStreamException,AssertionException) {
   default:
     Unreachable();
   }
+
+  Parser *parser = NULL;
   switch(d_lang) {
   case language::input::LANG_SMTLIB:
-    return new Smt(&d_exprManager, input, d_strictMode);
+    parser = new Smt(&d_exprManager, input, d_strictMode);
   case language::input::LANG_SMTLIB_V2:
-    return new Smt2(&d_exprManager, input, d_strictMode);
+    parser = new Smt2(&d_exprManager, input, d_strictMode);
   default:
-    return new Parser(&d_exprManager, input, d_strictMode);
+    parser = new Parser(&d_exprManager, input, d_strictMode);
   }
-}
-
-/*ParserBuilder& ParserBuilder::disableChecks() {
-  d_checksEnabled = false;
-  return *this;
-}
 
-ParserBuilder& ParserBuilder::disableMmap() {
-  d_mmap = false;
-  return *this;
-}
-
-ParserBuilder& ParserBuilder::disableStrictMode() {
-  d_strictMode = false;
-  return *this;
+  return parser;
 }
 
-ParserBuilder& ParserBuilder::enableChecks() {
-  d_checksEnabled = true;
-  return *this;
-}
-
-ParserBuilder& ParserBuilder::enableMmap() {
-  d_mmap = true;
-  return *this;
-}
-
-ParserBuilder& ParserBuilder::enableStrictMode() {
-  d_strictMode = true;
-  return *this;
-}*/
-
 ParserBuilder& ParserBuilder::withChecks(bool flag) {
   d_checksEnabled = flag;
   return *this;