some fixes and organizational adjustments to assert code, parsers/lexers, and build process

16 files changed, 359 insertions, 241 deletions

diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index 8b728f5f4..e54d4aa2d 100644
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -31,7 +31,7 @@ libcvc4parser_la_LIBADD = \
 libcvc4parser_la_SOURCES = \
 	parser.h \
 	parser.cpp \
+	parser_exception.h \
 	symbol_table.h \
 	antlr_parser.h \
 	antlr_parser.cpp
-
diff --git a/src/parser/Makefile.in b/src/parser/Makefile.in
index 231643474..24cd1ed84 100644
--- a/src/parser/Makefile.in
+++ b/src/parser/Makefile.in
@@ -309,6 +309,7 @@ libcvc4parser_la_LIBADD = \
 libcvc4parser_la_SOURCES = \
 	parser.h \
 	parser.cpp \
+	parser_exception.h \
 	symbol_table.h \
 	antlr_parser.h \
 	antlr_parser.cpp
diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am
index eb0adc39c..6fb9689de 100644
--- a/src/parser/cvc/Makefile.am
+++ b/src/parser/cvc/Makefile.am
@@ -1,4 +1,4 @@
-INCLUDES = -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
+INCLUDES = -I@srcdir@/../../include -I@srcdir@/../..
 AM_CXXFLAGS = -Wall -fvisibility=hidden
 AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB
 
@@ -21,8 +21,10 @@ ANTLR_STUFF = \
 	$(ANTLR_PARSER_STUFF)
 
 libparsercvc_la_SOURCES = \
-	CvcLexer.g \
-	CvcParser.g \
+	cvc_lexer.g \
+	cvc_parser.g \
+	cvc_parser.h \
+	cvc_parser.cpp \
 	$(ANTLR_STUFF)
 
 BUILT_SOURCES = $(ANTLR_STUFF)
@@ -36,13 +38,15 @@ maintainer-clean-local:
 	mkdir -p @srcdir@/generated
 	touch @srcdir@/stamp-generated
 # antlr doesn't overwrite output files, it just leaves them.  So we have to delete them first.
-$(ANTLR_LEXER_STUFF): CvcLexer.g @srcdir@/stamp-generated
+@srcdir@/generated/AntlrCvcLexer.hpp: cvc_lexer.g @srcdir@/stamp-generated
 	-rm -f $(ANTLR_LEXER_STUFF)
-	$(ANTLR) -o "@srcdir@/generated" "@srcdir@/CvcLexer.g"
+	$(ANTLR) -o "@srcdir@/generated" "@srcdir@/cvc_lexer.g"
+@srcdir@/generated/AntlrCvcLexer.cpp $(ANTLR_TOKEN_STUFF): @srcdir@/generated/AntlrCvcLexer.hpp
 # doesn't actually depend on the lexer, but if we're doing parallel
 # make and the lexer needs to be rebuilt, we have to keep the rules
 # from running in parallel (since the token files will be deleted &
 # recreated)
-$(ANTLR_PARSER_STUFF): CvcParser.g CvcLexer.g $(ANTLR_TOKEN_STUFF) @srcdir@/stamp-generated
+@srcdir@/generated/AntlrCvcParser.hpp: cvc_parser.g cvc_lexer.g $(ANTLR_TOKEN_STUFF) @srcdir@/stamp-generated
 	-rm -f $(ANTLR_PARSER_STUFF)
-	$(ANTLR) -o "@srcdir@/generated" "@srcdir@/CvcParser.g"
+	$(ANTLR) -o "@srcdir@/generated" "@srcdir@/cvc_parser.g"
+@srcdir@/generated/AntlrCvcParser.cpp: @srcdir@/generated/AntlrCvcParser.hpp
diff --git a/src/parser/cvc/Makefile.in b/src/parser/cvc/Makefile.in
index f7358bfcc..b953d3c54 100644
--- a/src/parser/cvc/Makefile.in
+++ b/src/parser/cvc/Makefile.in
@@ -56,7 +56,7 @@ am__objects_1 =
 am__objects_2 = AntlrCvcLexer.lo $(am__objects_1)
 am__objects_3 = AntlrCvcParser.lo
 am__objects_4 = $(am__objects_2) $(am__objects_3)
-am_libparsercvc_la_OBJECTS = $(am__objects_4)
+am_libparsercvc_la_OBJECTS = cvc_parser.lo $(am__objects_4)
 libparsercvc_la_OBJECTS = $(am_libparsercvc_la_OBJECTS)
 DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir)
 depcomp = $(SHELL) $(top_srcdir)/config/depcomp
@@ -219,7 +219,7 @@ target_vendor = @target_vendor@
 top_build_prefix = @top_build_prefix@
 top_builddir = @top_builddir@
 top_srcdir = @top_srcdir@
-INCLUDES = -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
+INCLUDES = -I@srcdir@/../../include -I@srcdir@/../..
 AM_CXXFLAGS = -Wall -fvisibility=hidden
 AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB
 noinst_LTLIBRARIES = libparsercvc.la
@@ -243,8 +243,10 @@ ANTLR_STUFF = \
 	$(ANTLR_PARSER_STUFF)
 
 libparsercvc_la_SOURCES = \
-	CvcLexer.g \
-	CvcParser.g \
+	cvc_lexer.g \
+	cvc_parser.g \
+	cvc_parser.h \
+	cvc_parser.cpp \
 	$(ANTLR_STUFF)
 
 BUILT_SOURCES = $(ANTLR_STUFF)
@@ -304,6 +306,7 @@ distclean-compile:
 
 @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrCvcLexer.Plo@am__quote@
 @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrCvcParser.Plo@am__quote@
+@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/cvc_parser.Plo@am__quote@
 
 .cpp.o:
 @am__fastdepCXX_TRUE@	$(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $<
@@ -561,16 +564,18 @@ maintainer-clean-local:
 	mkdir -p @srcdir@/generated
 	touch @srcdir@/stamp-generated
 # antlr doesn't overwrite output files, it just leaves them.  So we have to delete them first.
-$(ANTLR_LEXER_STUFF): CvcLexer.g @srcdir@/stamp-generated
+@srcdir@/generated/AntlrCvcLexer.hpp: cvc_lexer.g @srcdir@/stamp-generated
 	-rm -f $(ANTLR_LEXER_STUFF)
-	$(ANTLR) -o "@srcdir@/generated" "@srcdir@/CvcLexer.g"
+	$(ANTLR) -o "@srcdir@/generated" "@srcdir@/cvc_lexer.g"
+@srcdir@/generated/AntlrCvcLexer.cpp $(ANTLR_TOKEN_STUFF): @srcdir@/generated/AntlrCvcLexer.hpp
 # doesn't actually depend on the lexer, but if we're doing parallel
 # make and the lexer needs to be rebuilt, we have to keep the rules
 # from running in parallel (since the token files will be deleted &
 # recreated)
-$(ANTLR_PARSER_STUFF): CvcParser.g CvcLexer.g $(ANTLR_TOKEN_STUFF) @srcdir@/stamp-generated
+@srcdir@/generated/AntlrCvcParser.hpp: cvc_parser.g cvc_lexer.g $(ANTLR_TOKEN_STUFF) @srcdir@/stamp-generated
 	-rm -f $(ANTLR_PARSER_STUFF)
-	$(ANTLR) -o "@srcdir@/generated" "@srcdir@/CvcParser.g"
+	$(ANTLR) -o "@srcdir@/generated" "@srcdir@/cvc_parser.g"
+@srcdir@/generated/AntlrCvcParser.cpp: @srcdir@/generated/AntlrCvcParser.hpp
 
 # Tell versions [3.59,3.63) of GNU make to not export all variables.
 # Otherwise a system limit (for SysV at least) may be exceeded.
diff --git a/src/parser/cvc/CvcLexer.g b/src/parser/cvc/cvc_lexer.g
index 8d706963f..8d706963f 100644
--- a/src/parser/cvc/CvcLexer.g
+++ b/src/parser/cvc/cvc_lexer.g
diff --git a/src/parser/cvc/cvc_parser.cpp b/src/parser/cvc/cvc_parser.cpp
new file mode 100644
index 000000000..adeb5761d
--- /dev/null
+++ b/src/parser/cvc/cvc_parser.cpp
@@ -0,0 +1,79 @@
+/*********************                                           -*- C++ -*-  */
+/** cvc_parser.cpp
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** CVC presentation language parser implementation.
+ **/
+
+#include <iostream>
+#include <fstream>
+
+#include "parser/parser.h"
+#include "util/command.h"
+#include "util/Assert.h"
+#include "parser/parser_exception.h"
+#include "parser/antlr_parser.h"
+#include "parser/cvc/cvc_parser.h"
+#include "parser/cvc/generated/AntlrCvcParser.hpp"
+#include "parser/cvc/generated/AntlrCvcLexer.hpp"
+
+using namespace std;
+
+namespace CVC4 {
+namespace parser {
+
+Command* CvcParser::parseNextCommand() throw(ParserException) {
+  Command* cmd = 0;
+  if(!done()) {
+    try {
+      cmd = d_antlr_parser->command();
+      if(cmd == 0) {
+        setDone();
+        cmd = new EmptyCommand("EOF");
+      }
+    } catch(antlr::ANTLRException& e) {
+      setDone();
+      throw ParserException(e.toString());
+    }
+  }
+  return cmd;
+}
+
+Expr CvcParser::parseNextExpression() throw(ParserException) {
+  Expr result;
+  if(!done()) {
+    try {
+      result = d_antlr_parser->formula();
+    } catch(antlr::ANTLRException& e) {
+      setDone();
+      throw ParserException(e.toString());
+    }
+  }
+  return result;
+}
+
+CvcParser::~CvcParser() {
+  delete d_antlr_parser;
+  delete d_antlr_lexer;
+}
+
+CvcParser::CvcParser(ExprManager*em, istream& input, const char* file_name) :
+  Parser(em), d_input(input) {
+  if(!d_input) {
+    throw ParserException(string("Read error") +
+                          ((file_name != NULL) ? (string(" on ") + file_name) : ""));
+  }
+  d_antlr_lexer = new AntlrCvcLexer(d_input);
+  d_antlr_lexer->setFilename(file_name);
+  d_antlr_parser = new AntlrCvcParser(*d_antlr_lexer);
+  d_antlr_parser->setExpressionManager(d_expr_manager);
+  d_antlr_parser->setFilename(file_name);
+}
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
diff --git a/src/parser/cvc/CvcParser.g b/src/parser/cvc/cvc_parser.g
index 625f2c381..625f2c381 100644
--- a/src/parser/cvc/CvcParser.g
+++ b/src/parser/cvc/cvc_parser.g
diff --git a/src/parser/cvc/cvc_parser.h b/src/parser/cvc/cvc_parser.h
new file mode 100644
index 000000000..9cb6b7594
--- /dev/null
+++ b/src/parser/cvc/cvc_parser.h
@@ -0,0 +1,77 @@
+/*********************                                           -*- C++ -*-  */
+/** cvc_parser.h
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** CVC presentation language parser abstraction.
+ **/
+
+#ifndef __CVC4__PARSER__CVC_PARSER_H
+#define __CVC4__PARSER__CVC_PARSER_H
+
+#include <string>
+#include <iostream>
+#include <fstream>
+#include "cvc4_config.h"
+#include "parser/parser_exception.h"
+#include "parser/parser.h"
+
+namespace CVC4 {
+namespace parser {
+
+/**
+ * The CVC parser.
+ */
+class CVC4_PUBLIC CvcParser : public Parser {
+
+public:
+
+  /**
+   * 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
+   * @param file_name the name of the file (for diagnostic output)
+   */
+  CvcParser(ExprManager* em, std::istream& input, const char* file_name = "");
+
+  /**
+   * Destructor.
+   */
+  ~CvcParser();
+
+  /**
+   * Parses the next command. By default, the CVC 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);
+
+  /**
+   * Parses the next complete expression of the stream.
+   * @return the expression parsed
+   */
+  Expr parseNextExpression() throw(ParserException);
+
+protected:
+
+  /** The ANTLR smt lexer */
+  AntlrCvcLexer* d_antlr_lexer;
+
+  /** The ANTLR smt parser */
+  AntlrCvcParser* d_antlr_parser;
+
+  /** The file stream we might be using */
+  std::istream& d_input;
+};
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PARSER__CVC_PARSER_H */
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 4309ec355..8d4af5ba1 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -40,112 +40,5 @@ bool Parser::done() const {
   return d_done;
 }
 
-Command* SmtParser::parseNextCommand() throw (ParserException) {
-  Command* cmd = 0;
-  if(!done()) {
-    try {
-      cmd = d_antlr_parser->benchmark();
-      setDone();
-    } catch(antlr::ANTLRException& e) {
-      setDone();
-      throw ParserException(e.toString());
-    }
-  }
-  return cmd;
-}
-
-Expr SmtParser::parseNextExpression() throw (ParserException) {
-  Expr result;
-  if (!done()) {
-    try {
-      result = d_antlr_parser->an_formula();
-    } catch(antlr::ANTLRException& e) {
-      setDone();
-      throw ParserException(e.toString());
-    }
-  }
-  return result;
-}
-
-SmtParser::~SmtParser() {
-  delete d_antlr_parser;
-  delete d_antlr_lexer;
-}
-
-SmtParser::SmtParser(ExprManager* em, istream& input) :
-  Parser(em) {
-  d_antlr_lexer = new AntlrSmtLexer(input);
-  d_antlr_parser = new AntlrSmtParser(*d_antlr_lexer);
-  d_antlr_parser->setExpressionManager(d_expr_manager);
-}
-
-SmtParser::SmtParser(ExprManager*em, const char* file_name) :
-  Parser(em), d_input(file_name) {
-  if(!d_input) {
-    throw ParserException(string("File not found or inaccessible: ") + 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);
-}
-
-Command* CvcParser::parseNextCommand() throw (ParserException) {
-  Command* cmd = 0;
-  if(!done()) {
-    try {
-      cmd = d_antlr_parser->command();
-      if (cmd == 0) {
-        setDone();
-        cmd = new EmptyCommand("EOF");
-      }
-    } catch(antlr::ANTLRException& e) {
-      setDone();
-      throw ParserException(e.toString());
-    }
-  }
-  return cmd;
-}
-
-Expr CvcParser::parseNextExpression() throw (ParserException) {
-  Expr result;
-  if (!done()) {
-    try {
-      result = d_antlr_parser->formula();
-    } catch(antlr::ANTLRException& e) {
-      setDone();
-      throw ParserException(e.toString());
-    }
-  }
-  return result;
-}
-
-CvcParser::~CvcParser() {
-  delete d_antlr_parser;
-  delete d_antlr_lexer;
-}
-
-CvcParser::CvcParser(ExprManager* em, istream& input) :
-  Parser(em) {
-  d_antlr_lexer = new AntlrCvcLexer(input);
-  d_antlr_parser = new AntlrCvcParser(*d_antlr_lexer);
-  d_antlr_parser->setExpressionManager(d_expr_manager);
-}
-
-CvcParser::CvcParser(ExprManager*em, const char* file_name) :
-  Parser(em), d_input(file_name) {
-  if(!d_input) {
-    throw ParserException(string("File not found or inaccessible: ") + file_name);
-  }
-  d_antlr_lexer = new AntlrCvcLexer(d_input);
-  d_antlr_lexer->setFilename(file_name);
-  d_antlr_parser = new AntlrCvcParser(*d_antlr_lexer);
-  d_antlr_parser->setExpressionManager(d_expr_manager);
-  d_antlr_parser->setFilename(file_name);
-}
-
-
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
-
diff --git a/src/parser/parser.h b/src/parser/parser.h
index dbdca4af8..7755d65f0 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -80,109 +80,6 @@ protected:
 
 }; // end of class Parser
 
-class CVC4_PUBLIC SmtParser : public Parser {
-
-public:
-
-  /**
-   * 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 file_name the file to parse
-   */
-  SmtParser(ExprManager* em, const char* file_name);
-
-  /**
-   * Destructor.
-   */
-  ~SmtParser();
-
-  /**
-   * 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);
-
-  /**
-   * Parses the next complete expression of the stream.
-   * @return the expression parsed
-   */
-  Expr parseNextExpression() throw (ParserException);
-
-protected:
-
-  /** The ANTLR smt lexer */
-  AntlrSmtLexer* d_antlr_lexer;
-
-  /** The ANTLR smt parser */
-  AntlrSmtParser* d_antlr_parser;
-
-  /** The file stream we might be using */
-  std::ifstream d_input;
-};
-
-class CVC4_PUBLIC CvcParser : public Parser {
-
-public:
-
-  /**
-   * 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
-   */
-  CvcParser(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 file_name the file to parse
-   */
-  CvcParser(ExprManager* em, const char* file_name);
-
-  /**
-   * Destructor.
-   */
-  ~CvcParser();
-
-  /**
-   * 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);
-
-  /**
-   * Parses the next complete expression of the stream.
-   * @return the expression parsed
-   */
-  Expr parseNextExpression() throw (ParserException);
-
-protected:
-
-  /** The ANTLR smt lexer */
-  AntlrCvcLexer* d_antlr_lexer;
-
-  /** The ANTLR smt parser */
-  AntlrCvcParser* d_antlr_parser;
-
-  /** The file stream we might be using */
-  std::ifstream d_input;
-};
-
-
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
 
diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am
index a6d234bd0..c3273f501 100644
--- a/src/parser/smt/Makefile.am
+++ b/src/parser/smt/Makefile.am
@@ -1,4 +1,4 @@
-INCLUDES = -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
+INCLUDES = -I@srcdir@/../../include -I@srcdir@/../..
 AM_CXXFLAGS = -Wall -fvisibility=hidden
 AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB
 
@@ -21,8 +21,10 @@ ANTLR_STUFF = \
 	$(ANTLR_PARSER_STUFF)
 
 libparsersmt_la_SOURCES = \
-	SmtLexer.g \
-	SmtParser.g \
+	smt_lexer.g \
+	smt_parser.g \
+	smt_parser.h \
+	smt_parser.cpp \
 	$(ANTLR_STUFF)
 
 BUILT_SOURCES = $(ANTLR_STUFF)
@@ -36,13 +38,15 @@ maintainer-clean-local:
 	mkdir -p @srcdir@/generated
 	touch @srcdir@/stamp-generated
 # antlr doesn't overwrite output files, it just leaves them.  So we have to delete them first.
-$(ANTLR_LEXER_STUFF): SmtLexer.g @srcdir@/stamp-generated
+@srcdir@/generated/AntlrSmtLexer.hpp: smt_lexer.g @srcdir@/stamp-generated
 	-rm -f $(ANTLR_LEXER_STUFF)
-	$(ANTLR) -o "@srcdir@/generated" "@srcdir@/SmtLexer.g"
+	$(ANTLR) -o "@srcdir@/generated" "@srcdir@/smt_lexer.g"
+@srcdir@/generated/AntlrSmtLexer.cpp $(ANTLR_TOKEN_STUFF): @srcdir@/generated/AntlrSmtLexer.hpp
 # doesn't actually depend on the lexer, but if we're doing parallel
 # make and the lexer needs to be rebuilt, we have to keep the rules
 # from running in parallel (since the token files will be deleted &
 # recreated)
-$(ANTLR_PARSER_STUFF): SmtParser.g SmtLexer.g $(ANTLR_TOKEN_STUFF) @srcdir@/stamp-generated
+@srcdir@/generated/AntlrSmtParser.hpp: smt_parser.g smt_lexer.g $(ANTLR_TOKEN_STUFF) @srcdir@/stamp-generated
 	-rm -f $(ANTLR_PARSER_STUFF)
-	$(ANTLR) -o "@srcdir@/generated" "@srcdir@/SmtParser.g"
+	$(ANTLR) -o "@srcdir@/generated" "@srcdir@/smt_parser.g"
+@srcdir@/generated/AntlrSmtParser.cpp: @srcdir@/generated/AntlrSmtParser.hpp
diff --git a/src/parser/smt/Makefile.in b/src/parser/smt/Makefile.in
index 20c91c28a..e153135c5 100644
--- a/src/parser/smt/Makefile.in
+++ b/src/parser/smt/Makefile.in
@@ -56,7 +56,7 @@ am__objects_1 =
 am__objects_2 = AntlrSmtLexer.lo $(am__objects_1)
 am__objects_3 = AntlrSmtParser.lo
 am__objects_4 = $(am__objects_2) $(am__objects_3)
-am_libparsersmt_la_OBJECTS = $(am__objects_4)
+am_libparsersmt_la_OBJECTS = smt_parser.lo $(am__objects_4)
 libparsersmt_la_OBJECTS = $(am_libparsersmt_la_OBJECTS)
 DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir)
 depcomp = $(SHELL) $(top_srcdir)/config/depcomp
@@ -219,7 +219,7 @@ target_vendor = @target_vendor@
 top_build_prefix = @top_build_prefix@
 top_builddir = @top_builddir@
 top_srcdir = @top_srcdir@
-INCLUDES = -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
+INCLUDES = -I@srcdir@/../../include -I@srcdir@/../..
 AM_CXXFLAGS = -Wall -fvisibility=hidden
 AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB
 noinst_LTLIBRARIES = libparsersmt.la
@@ -243,8 +243,10 @@ ANTLR_STUFF = \
 	$(ANTLR_PARSER_STUFF)
 
 libparsersmt_la_SOURCES = \
-	SmtLexer.g \
-	SmtParser.g \
+	smt_lexer.g \
+	smt_parser.g \
+	smt_parser.h \
+	smt_parser.cpp \
 	$(ANTLR_STUFF)
 
 BUILT_SOURCES = $(ANTLR_STUFF)
@@ -304,6 +306,7 @@ distclean-compile:
 
 @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrSmtLexer.Plo@am__quote@
 @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrSmtParser.Plo@am__quote@
+@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/smt_parser.Plo@am__quote@
 
 .cpp.o:
 @am__fastdepCXX_TRUE@	$(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $<
@@ -561,16 +564,18 @@ maintainer-clean-local:
 	mkdir -p @srcdir@/generated
 	touch @srcdir@/stamp-generated
 # antlr doesn't overwrite output files, it just leaves them.  So we have to delete them first.
-$(ANTLR_LEXER_STUFF): SmtLexer.g @srcdir@/stamp-generated
+@srcdir@/generated/AntlrSmtLexer.hpp: smt_lexer.g @srcdir@/stamp-generated
 	-rm -f $(ANTLR_LEXER_STUFF)
-	$(ANTLR) -o "@srcdir@/generated" "@srcdir@/SmtLexer.g"
+	$(ANTLR) -o "@srcdir@/generated" "@srcdir@/smt_lexer.g"
+@srcdir@/generated/AntlrSmtLexer.cpp $(ANTLR_TOKEN_STUFF): @srcdir@/generated/AntlrSmtLexer.hpp
 # doesn't actually depend on the lexer, but if we're doing parallel
 # make and the lexer needs to be rebuilt, we have to keep the rules
 # from running in parallel (since the token files will be deleted &
 # recreated)
-$(ANTLR_PARSER_STUFF): SmtParser.g SmtLexer.g $(ANTLR_TOKEN_STUFF) @srcdir@/stamp-generated
+@srcdir@/generated/AntlrSmtParser.hpp: smt_parser.g smt_lexer.g $(ANTLR_TOKEN_STUFF) @srcdir@/stamp-generated
 	-rm -f $(ANTLR_PARSER_STUFF)
-	$(ANTLR) -o "@srcdir@/generated" "@srcdir@/SmtParser.g"
+	$(ANTLR) -o "@srcdir@/generated" "@srcdir@/smt_parser.g"
+@srcdir@/generated/AntlrSmtParser.cpp: @srcdir@/generated/AntlrSmtParser.hpp
 
 # Tell versions [3.59,3.63) of GNU make to not export all variables.
 # Otherwise a system limit (for SysV at least) may be exceeded.
diff --git a/src/parser/smt/SmtLexer.g b/src/parser/smt/smt_lexer.g
index 3d9a84f06..3d9a84f06 100644
--- a/src/parser/smt/SmtLexer.g
+++ b/src/parser/smt/smt_lexer.g
diff --git a/src/parser/smt/smt_parser.cpp b/src/parser/smt/smt_parser.cpp
new file mode 100644
index 000000000..65d36690c
--- /dev/null
+++ b/src/parser/smt/smt_parser.cpp
@@ -0,0 +1,76 @@
+/*********************                                           -*- C++ -*-  */
+/** smt_parser.cpp
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** SMT-LIB language parser implementation.
+ **/
+
+#include <iostream>
+#include <fstream>
+
+#include "parser/parser.h"
+#include "util/command.h"
+#include "util/Assert.h"
+#include "parser/parser_exception.h"
+#include "parser/antlr_parser.h"
+#include "parser/smt/smt_parser.h"
+#include "parser/smt/generated/AntlrSmtParser.hpp"
+#include "parser/smt/generated/AntlrSmtLexer.hpp"
+
+using namespace std;
+
+namespace CVC4 {
+namespace parser {
+
+Command* SmtParser::parseNextCommand() throw(ParserException) {
+  Command* cmd = 0;
+  if(!done()) {
+    try {
+      cmd = d_antlr_parser->benchmark();
+      setDone();
+    } catch(antlr::ANTLRException& e) {
+      setDone();
+      throw ParserException(e.toString());
+    }
+  }
+  return cmd;
+}
+
+Expr SmtParser::parseNextExpression() throw(ParserException) {
+  Expr result;
+  if(!done()) {
+    try {
+      result = d_antlr_parser->an_formula();
+    } catch(antlr::ANTLRException& e) {
+      setDone();
+      throw ParserException(e.toString());
+    }
+  }
+  return result;
+}
+
+SmtParser::~SmtParser() {
+  delete d_antlr_parser;
+  delete d_antlr_lexer;
+}
+
+SmtParser::SmtParser(ExprManager* em, istream& input, const char* file_name) :
+  Parser(em), d_input(input) {
+  if(!d_input) {
+    throw ParserException(string("Read error") +
+                          ((file_name != NULL) ? (string(" on ") + file_name) : ""));
+  }
+  d_antlr_lexer = new AntlrSmtLexer(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 */
+}/* CVC4 namespace */
diff --git a/src/parser/smt/SmtParser.g b/src/parser/smt/smt_parser.g
index f68d783bc..f68d783bc 100644
--- a/src/parser/smt/SmtParser.g
+++ b/src/parser/smt/smt_parser.g
diff --git a/src/parser/smt/smt_parser.h b/src/parser/smt/smt_parser.h
new file mode 100644
index 000000000..a68f0e783
--- /dev/null
+++ b/src/parser/smt/smt_parser.h
@@ -0,0 +1,77 @@
+/*********************                                           -*- C++ -*-  */
+/** smt_parser.h
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** SMT-LIB language parser abstraction.
+ **/
+
+#ifndef __CVC4__PARSER__SMT_PARSER_H
+#define __CVC4__PARSER__SMT_PARSER_H
+
+#include <string>
+#include <iostream>
+#include <fstream>
+#include "cvc4_config.h"
+#include "parser/parser_exception.h"
+#include "parser/parser.h"
+
+namespace CVC4 {
+namespace parser {
+
+/**
+ * The SMT parser.
+ */
+class CVC4_PUBLIC SmtParser : public Parser {
+
+public:
+
+  /**
+   * 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
+   * @param file_name the name of the file (for diagnostic output)
+   */
+  SmtParser(ExprManager* em, std::istream& input, const char* file_name = "");
+
+  /**
+   * Destructor.
+   */
+  ~SmtParser();
+
+  /**
+   * Parses the next command. By default, the SMT-LIB 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);
+
+  /**
+   * Parses the next complete expression of the stream.
+   * @return the expression parsed
+   */
+  Expr parseNextExpression() throw(ParserException);
+
+protected:
+
+  /** The ANTLR smt lexer */
+  AntlrSmtLexer* d_antlr_lexer;
+
+  /** The ANTLR smt parser */
+  AntlrSmtParser* d_antlr_parser;
+
+  /** The file stream we might be using */
+  std::istream& d_input;
+};
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PARSER__SMT_PARSER_H */