1 files changed, 54 insertions, 28 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index cd03f21f2..b9091668e 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -11,49 +11,75 @@
  **/
 
 #include <iostream>
+#include <fstream>
 
-#include "cvc4_config.h"
-#include "parser/parser.h"
+#include "parser.h"
 #include "util/command.h"
 #include "util/assert.h"
-#include "parser/parser_state.h"
-#include "parser/parser_exception.h"
-
-int CVC4_PUBLIC smtlibparse();
-int CVC4_PUBLIC PLparse();
-extern "C" int smtlibdebug, PLdebug;
+#include "parser_exception.h"
+#include "parser/antlr_parser.h"
+#include "parser/smt/AntlrSmtParser.hpp"
+#include "parser/smt/AntlrSmtLexer.hpp"
 
 using namespace std;
-using namespace CVC4;
 
 namespace CVC4 {
 namespace parser {
 
-ParserState CVC4_PUBLIC *_global_parser_state = 0;
+Parser::Parser(ExprManager* em) :
+  d_expr_manager(em) {
+}
 
-bool Parser::done() const {
-  return _global_parser_state->done();
+bool SmtParser::done() const {
+  return d_done;
+}
+
+Command* SmtParser::parseNextCommand() throw (ParserException) {
+  Command* cmd = 0;
+  if(!d_done) {
+    try {
+      cmd = d_antlr_parser->benchmark();
+      d_done = true;
+    } catch(antlr::ANTLRException& e) {
+      d_done = true;
+      throw ParserException(e.toString());
+    }
+  }
+  return cmd;
 }
 
-Command* Parser::parseNextCommand(bool verbose) {
-  switch(d_lang) {
-  case PL:
-    PLdebug = verbose;
-    PLparse();
-    cout << "getting command" << endl;
-    return _global_parser_state->getCommand();
-  case SMTLIB:
-    smtlibdebug = verbose;
-    smtlibparse();
-    return _global_parser_state->getCommand();
-  default:
-    Unhandled();
+Expr SmtParser::parseNextExpression() throw (ParserException) {
+  Expr result;
+  if (!d_done) {
+    try {
+      result = d_antlr_parser->an_formula();
+    } catch(antlr::ANTLRException& e) {
+      d_done = true;
+      throw ParserException(e.toString());
+    }
   }
-  return new EmptyCommand;
+  return result;
+}
+
+SmtParser::~SmtParser() {
+  delete d_antlr_parser;
+  delete d_antlr_lexer;
+}
+
+SmtParser::SmtParser(ExprManager* em, istream& input) :
+  Parser(em), d_done(false) {
+  d_antlr_lexer = new AntlrSmtLexer(input);
+  d_antlr_parser = new AntlrSmtParser(*d_antlr_lexer);
+  d_antlr_parser->setExpressionManager(d_expr_manager);
 }
 
-Parser::~Parser() {
-  //delete d_data;
+SmtParser::SmtParser(ExprManager*em, const char* file_name) :
+  Parser(em), d_done(false), d_input(file_name) {
+  d_antlr_lexer = new AntlrSmtLexer(d_input);
+  d_antlr_lexer->setFilename(file_name);
+  d_antlr_parser = new AntlrSmtParser(*d_antlr_lexer);
+  d_antlr_parser->setExpressionManager(d_expr_manager);
+  d_antlr_parser->setFilename(file_name);
 }
 
 }/* CVC4::parser namespace */