1 files changed, 81 insertions, 42 deletions
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 411e7760c..d0ef3776a 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -15,9 +15,9 @@
 
 #include <string>
 #include <iostream>
-
-#include "parser/language.h"
-#include "parser/parser_state.h"
+#include <fstream>
+#include "cvc4_config.h"
+#include "parser_exception.h"
 
 namespace CVC4 {
 
@@ -25,74 +25,113 @@ namespace CVC4 {
 class Expr;
 class Command;
 class ExprManager;
-class SmtEngine;
-class Options;
 
 namespace parser {
 
-/**
- * The global pointer to ParserTemp.  Each instance of class Parser sets this pointer
- * before any calls to the lexer.  We do it this way because flex and bison use global
- * vars, and we want each Parser object to appear independent.
- */
-extern ParserState CVC4_PUBLIC *_global_parser_state;
+class AntlrSmtLexer;
+class AntlrSmtParser;
 
 /**
  * The parser.
  */
 class CVC4_PUBLIC Parser {
- private:
 
-  /** Internal parser state we are keeping */
-  //ParserState* d_data;
+public:
+
+  /**
+   * Construct the parser that uses the given expression manager.
+   * @param em the expression manager.
+   */
+  Parser(ExprManager* em);
+
+  /**
+   * Destructor.
+   */
+  virtual ~Parser() {
+  }
+  ;
+
+  /**
+   * Parse the next command of the input
+   */
+  virtual Command* parseNextCommand() throw (ParserException) = 0;
+
+  /**
+   * Parse the next expression of the stream
+   */
+  virtual Expr parseNextExpression() throw (ParserException) = 0;
+
+  /**
+   * Check if we are done -- either the end of input has been reached.
+   */
+  virtual bool done() const = 0;
 
-  /** Initialize the parser */
-  void initParser();
+protected:
 
-  /** Remove the parser components */
-  void deleteParser();
+  /** Expression manager the parser will be using */
+  ExprManager* d_expr_manager;
 
-  Language d_lang;
-  std::istream &d_in;
-  Options *d_opts;
+}; // end of class Parser
 
- public:
+class CVC4_PUBLIC SmtParser : public Parser {
+
+public:
 
   /**
-   * Constructor for parsing out of a file.
+   * Construct the parser that uses the given expression manager and parses
+   * from the given input stream.
+   * @param em the expression manager to use
+   * @param input the input stream to parse
+   */
+  SmtParser(ExprManager* em, std::istream& input);
+
+  /**
+   * Construct the parser that uses the given expression manager and parses
+   * from the file.
    * @param em the expression manager to use
-   * @param lang the language syntax to use
    * @param file_name the file to parse
    */
-  Parser(SmtEngine* smt, ExprManager* em, Language lang, std::istream& in, Options* opts) :
-    d_lang(lang), d_in(in), d_opts(opts) {
-    _global_parser_state = new ParserState(smt, em);
-    _global_parser_state->setInputStream(in);
-  }
+  SmtParser(ExprManager* em, const char* file_name);
 
   /**
    * Destructor.
    */
-  ~Parser();
+  ~SmtParser();
 
-  /** Parse a command */
-  Command* parseNextCommand(bool verbose = false);
+  /**
+   * Parses the next command. By default, the SMTLIB parser produces one
+   * CommandSequence command. If parsing is successful, we should be done
+   * after the first call to this command.
+   * @return the CommandSequence command that includes the whole benchmark
+   */
+  Command* parseNextCommand() throw (ParserException);
 
-  /** Parse an expression of the stream */
-  Expr parseNextExpression();
+  /**
+   * Parses the next complete expression of the stream.
+   * @return the expression parsed
+   */
+  Expr parseNextExpression() throw (ParserException);
 
-  // Check if we are done (end of input has been reached)
+  /**
+   * Check if we are done with the stream, i.e. EOF has been reached, or the
+   * whole SMT benchmark has been parsed.
+   */
   bool done() const;
 
-  // The same check can be done by using the class Parser's value as a Boolean
-  operator bool() const { return done(); }
+protected:
 
-  /** Prints the location to the output stream */
-  void printLocation(std::ostream& out) const;
+  /** The ANTLR smt lexer */
+  AntlrSmtLexer* d_antlr_lexer;
 
-  /** Reset any local data */
-  void reset();
-}; // end of class Parser
+  /** The ANTLR smt parser */
+  AntlrSmtParser* d_antlr_parser;
+
+  /** Are we done */
+  bool d_done;
+
+  /** The file stream we might be using */
+  std::ifstream d_input;
+};
 
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */