1 files changed, 54 insertions, 53 deletions
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 765fb0553..411e7760c 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -16,83 +16,84 @@
 #include <string>
 #include <iostream>
 
-namespace CVC4
-{
-namespace parser
-{
+#include "parser/language.h"
+#include "parser/parser_state.h"
+
+namespace CVC4 {
 
 // Forward declarations
 class Expr;
 class Command;
 class ExprManager;
-class ParserState;
+class SmtEngine;
+class Options;
+
+namespace parser {
 
 /**
- * The 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.
  */
-class Parser
-{
-  private:
+extern ParserState CVC4_PUBLIC *_global_parser_state;
 
-    /** Internal parser state we are keeping */
-    ParserState* d_data;
+/**
+ * The parser.
+ */
+class CVC4_PUBLIC Parser {
+ private:
 
-    /** Initialize the parser */
-    void initParser();
+  /** Internal parser state we are keeping */
+  //ParserState* d_data;
 
-    /** Remove the parser components */
-    void deleteParser();
+  /** Initialize the parser */
+  void initParser();
 
-  public:
+  /** Remove the parser components */
+  void deleteParser();
 
-    /** The supported input languages */
-    enum InputLanguage {
-      /** SMT-LIB language */
-      INPUT_SMTLIB,
-      /** CVC language */
-      INPUT_CVC
-    };
+  Language d_lang;
+  std::istream &d_in;
+  Options *d_opts;
 
-    /**
-     * Constructor for parsing out of a file.
-     * @param em the expression manager to use
-     * @param lang the language syntax to use
-     * @param file_name the file to parse
-     */
-    Parser(ExprManager* em, InputLanguage lang, const std::string& file_name);
+ public:
 
-    /**
-     * Destructor.
-     */
-    ~Parser();
+  /**
+   * Constructor for parsing out of a 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);
+  }
 
-    /** Parse a command */
-    Command parseNextCommand();
+  /**
+   * Destructor.
+   */
+  ~Parser();
 
-    /** Parse an expression of the stream */
-    Expr parseNextExpression();
+  /** Parse a command */
+  Command* parseNextCommand(bool verbose = false);
 
-    // Check if we are done (end of input has been reached)
-    bool done() const;
+  /** Parse an expression of the stream */
+  Expr parseNextExpression();
 
-    // The same check can be done by using the class Parser's value as a Boolean
-    operator bool() const { return done(); }
+  // Check if we are done (end of input has been reached)
+  bool done() const;
 
-    /** Prints the location to the output stream */
-    void printLocation(std::ostream& out) const;
+  // The same check can be done by using the class Parser's value as a Boolean
+  operator bool() const { return done(); }
 
-    /** Reset any local data */
-    void reset();
+  /** Prints the location to the output stream */
+  void printLocation(std::ostream& out) const;
 
+  /** Reset any local data */
+  void reset();
 }; // end of class 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* _global_parser_state;
-
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */