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

27 files changed, 692 insertions, 338 deletions

diff --git a/src/include/cvc4_config.h b/src/include/cvc4_config.h
index 95fac9aaa..a42ae28fb 100644
--- a/src/include/cvc4_config.h
+++ b/src/include/cvc4_config.h
@@ -34,3 +34,4 @@
 
 #define EXPECT_TRUE(x) __builtin_expect( (x), true)
 #define EXPECT_FALSE(x) __builtin_expect( (x), false)
+#define NORETURN __attribute__ ((noreturn))
diff --git a/src/main/main.cpp b/src/main/main.cpp
index d4ee8fd0d..8b59e6013 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -20,6 +20,8 @@
 #include "main.h"
 #include "usage.h"
 #include "parser/parser.h"
+#include "parser/smt/smt_parser.h"
+#include "parser/cvc/cvc_parser.h"
 #include "expr/expr_manager.h"
 #include "smt/smt_engine.h"
 #include "util/command.h"
@@ -82,20 +84,16 @@ int main(int argc, char *argv[]) {
         Warning.setStream(CVC4::null_os);
     }
 
+    const char* fname = inputFromStdin ? argv[firstArgIndex] : "stdin";
+
     // Create the parser
     Parser* parser;
     switch(options.lang) {
     case Options::LANG_SMTLIB:
-      if(inputFromStdin)
-        parser = new SmtParser(&exprMgr, cin);
-      else
-        parser = new SmtParser(&exprMgr, argv[firstArgIndex]);
+      parser = new SmtParser(&exprMgr, cin, fname);
       break;
     case Options::LANG_CVC4:
-      if(inputFromStdin)
-        parser = new CvcParser(&exprMgr, cin);
-      else
-        parser = new CvcParser(&exprMgr, argv[firstArgIndex]);
+      parser = new CvcParser(&exprMgr, cin, fname);
       break;
     case Options::LANG_AUTO:
       cerr << "Auto language detection not supported yet." << endl;
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 */
diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am
index 4071197ad..715e79d16 100644
--- a/src/prop/Makefile.am
+++ b/src/prop/Makefile.am
@@ -5,6 +5,8 @@ AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 noinst_LTLIBRARIES = libprop.la
 
 libprop_la_SOURCES = \
-	prop_engine.cpp
+	prop_engine.cpp \
+	prop_engine.h \
+	sat.h
 
 SUBDIRS = minisat
diff --git a/src/prop/Makefile.in b/src/prop/Makefile.in
index 1bfd4d706..5fb636c23 100644
--- a/src/prop/Makefile.in
+++ b/src/prop/Makefile.in
@@ -67,6 +67,15 @@ CXXLD = $(CXX)
 CXXLINK = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
 	--mode=link $(CXXLD) $(AM_CXXFLAGS) $(CXXFLAGS) $(AM_LDFLAGS) \
 	$(LDFLAGS) -o $@
+COMPILE = $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) \
+	$(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+LTCOMPILE = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+	--mode=compile $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \
+	$(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+CCLD = $(CC)
+LINK = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+	--mode=link $(CCLD) $(AM_CFLAGS) $(CFLAGS) $(AM_LDFLAGS) \
+	$(LDFLAGS) -o $@
 SOURCES = $(libprop_la_SOURCES)
 DIST_SOURCES = $(libprop_la_SOURCES)
 RECURSIVE_TARGETS = all-recursive check-recursive dvi-recursive \
@@ -249,7 +258,9 @@ AM_CXXFLAGS = -Wall -fvisibility=hidden
 AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 noinst_LTLIBRARIES = libprop.la
 libprop_la_SOURCES = \
-	prop_engine.cpp
+	prop_engine.cpp \
+	prop_engine.h \
+	sat.h
 
 SUBDIRS = minisat
 all: all-recursive
diff --git a/src/prop/minisat/Makefile.am b/src/prop/minisat/Makefile.am
index f2716ff56..cef9a4c1e 100644
--- a/src/prop/minisat/Makefile.am
+++ b/src/prop/minisat/Makefile.am
@@ -5,4 +5,23 @@ AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 noinst_LTLIBRARIES = libminisat.la
 libminisat_la_SOURCES = \
 	core/Solver.C \
-	simp/SimpSolver.C
+	core/Solver.h \
+	core/SolverTypes.h \
+	simp/SimpSolver.C \
+	simp/SimpSolver.h
+
+EXTRA_DIST = \
+	core/Main.C \
+	core/Makefile \
+	simp/Main.C \
+	simp/Makefile \
+	README \
+	LICENSE \
+	mtl/Heap.h \
+	mtl/Map.h \
+	mtl/Queue.h \
+	mtl/Alg.h \
+	mtl/Sort.h \
+	mtl/BasicHeap.h \
+	mtl/BoxedVec.h \
+	mtl/template.mk
diff --git a/src/prop/minisat/Makefile.in b/src/prop/minisat/Makefile.in
index fe890e46a..646389c80 100644
--- a/src/prop/minisat/Makefile.in
+++ b/src/prop/minisat/Makefile.in
@@ -67,6 +67,15 @@ CXXLD = $(CXX)
 CXXLINK = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
 	--mode=link $(CXXLD) $(AM_CXXFLAGS) $(CXXFLAGS) $(AM_LDFLAGS) \
 	$(LDFLAGS) -o $@
+COMPILE = $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) \
+	$(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+LTCOMPILE = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+	--mode=compile $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \
+	$(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+CCLD = $(CC)
+LINK = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+	--mode=link $(CCLD) $(AM_CFLAGS) $(CFLAGS) $(AM_LDFLAGS) \
+	$(LDFLAGS) -o $@
 SOURCES = $(libminisat_la_SOURCES)
 DIST_SOURCES = $(libminisat_la_SOURCES)
 ETAGS = etags
@@ -212,7 +221,26 @@ AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 noinst_LTLIBRARIES = libminisat.la
 libminisat_la_SOURCES = \
 	core/Solver.C \
-	simp/SimpSolver.C
+	core/Solver.h \
+	core/SolverTypes.h \
+	simp/SimpSolver.C \
+	simp/SimpSolver.h
+
+EXTRA_DIST = \
+	core/Main.C \
+	core/Makefile \
+	simp/Main.C \
+	simp/Makefile \
+	README \
+	LICENSE \
+	mtl/Heap.h \
+	mtl/Map.h \
+	mtl/Queue.h \
+	mtl/Alg.h \
+	mtl/Sort.h \
+	mtl/BasicHeap.h \
+	mtl/BoxedVec.h \
+	mtl/template.mk
 
 all: all-am
 
diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp
new file mode 100644
index 000000000..799af12ab
--- /dev/null
+++ b/src/util/Assert.cpp
@@ -0,0 +1,101 @@
+/*********************                                           -*- C++ -*-  */
+/** Assert.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.
+ **
+ ** Assertion utility classes, functions, and exceptions.  Implementation.
+ **/
+
+#include <new>
+#include <cstdarg>
+#include <cstdio>
+#include "util/Assert.h"
+#include "util/exception.h"
+#include "cvc4_config.h"
+#include "config.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+void AssertionException::construct(const char* header, const char* extra,
+                                   const char* function, const char* file,
+                                   unsigned line, const char* fmt,
+                                   va_list args) {
+  // try building the exception msg with a smallish buffer first,
+  // then with a larger one if sprintf tells us to.
+  int n = 256;
+  char* buf;
+
+  for(;;) {
+    buf = new char[n];
+
+    int size;
+    if(extra == NULL) {
+      size = snprintf(buf, n, "%s\n%s\n%s:%d\n",
+                      header, function, file, line);
+    } else {
+      size = snprintf(buf, n, "%s\n%s\n%s:%d:\n\n  %s\n",
+                      header, function, file, line, extra);
+    }
+
+    if(size < n) {
+      va_list args_copy;
+      va_copy(args_copy, args);
+      size += vsnprintf(buf + size, n - size, fmt, args);
+      va_end(args_copy);
+
+      if(size < n) {
+        break;
+      }
+    }
+
+    if(size >= n) {
+      // try again with a buffer that's large enough
+      n = size + 1;
+      delete [] buf;
+    }
+  }
+
+  setMessage(string(buf));
+  delete [] buf;
+}
+
+void AssertionException::construct(const char* header, const char* extra,
+                                   const char* function, const char* file,
+                                   unsigned line) {
+  // try building the exception msg with a smallish buffer first,
+  // then with a larger one if sprintf tells us to.
+  int n = 256;
+  char* buf;
+
+  for(;;) {
+    buf = new char[n];
+
+    int size;
+    if(extra == NULL) {
+      size = snprintf(buf, n, "%s.\n%s\n%s:%d\n",
+                      header, function, file, line);
+    } else {
+      size = snprintf(buf, n, "%s.\n%s\n%s:%d:\n\n  %s\n",
+                      header, function, file, line, extra);
+    }
+
+    if(size < n) {
+      break;
+    } else {
+      // try again with a buffer that's large enough
+      n = size + 1;
+      delete [] buf;
+    }
+  }
+
+  setMessage(string(buf));
+  delete [] buf;
+}
+
+}/* CVC4 namespace */
diff --git a/src/util/Assert.h b/src/util/Assert.h
index 8fd970c6c..3da76c5db 100644
--- a/src/util/Assert.h
+++ b/src/util/Assert.h
@@ -1,5 +1,5 @@
 /*********************                                           -*- C++ -*-  */
-/** assert.h
+/** Assert.h
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,13 +7,15 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** Assertion utility classes, functions, and exceptions.
+ ** Assertion utility classes, functions, exceptions, and macros.
  **/
 
 #ifndef __CVC4__ASSERT_H
 #define __CVC4__ASSERT_H
 
 #include <string>
+#include <cstdio>
+#include <cstdarg>
 #include "util/exception.h"
 #include "cvc4_config.h"
 #include "config.h"
@@ -21,91 +23,136 @@
 namespace CVC4 {
 
 class CVC4_PUBLIC AssertionException : public Exception {
-public:
+protected:
+  void construct(const char* header, const char* extra,
+                 const char* function, const char* file,
+                 unsigned line, const char* fmt, ...) {
+    va_list args;
+    va_start(args, fmt);
+    construct(header, extra, function, file, line, fmt, args);
+    va_end(args);
+  }
+  void construct(const char* header, const char* extra,
+                 const char* function, const char* file,
+                 unsigned line, const char* fmt, va_list args);
+  void construct(const char* header, const char* extra,
+                 const char* function, const char* file,
+                 unsigned line);
+
   AssertionException() : Exception() {}
-  AssertionException(std::string msg) : Exception(msg) {}
-  AssertionException(const char* msg) : Exception(msg) {}
+
+public:
+  AssertionException(const char* extra, const char* function,
+                     const char* file, unsigned line,
+                     const char* fmt, ...) :
+    Exception() {
+    va_list args;
+    va_start(args, fmt);
+    construct("Assertion failure", extra, function, file, line, fmt, args);
+    va_end(args);
+  }
+
+  AssertionException(const char* extra, const char* function,
+                     const char* file, unsigned line) :
+    Exception() {
+    construct("Assertion failure", extra, function, file, line);
+  }
 };/* class AssertionException */
 
 class CVC4_PUBLIC UnreachableCodeException : public AssertionException {
-public:
+protected:
   UnreachableCodeException() : AssertionException() {}
-  UnreachableCodeException(std::string msg) : AssertionException(msg) {}
-  UnreachableCodeException(const char* msg) : AssertionException(msg) {}
+
+public:
+  UnreachableCodeException(const char* function, const char* file,
+                           unsigned line, const char* fmt, ...) :
+    AssertionException() {
+    va_list args;
+    va_start(args, fmt);
+    construct("Unreachable code reached",
+              NULL, function, file, line, fmt, args);
+    va_end(args);
+  }
+
+  UnreachableCodeException(const char* function, const char* file,
+                           unsigned line) :
+    AssertionException() {
+    construct("Unreachable code reached", NULL, function, file, line);
+  }
 };/* class UnreachableCodeException */
 
 class CVC4_PUBLIC UnhandledCaseException : public UnreachableCodeException {
-public:
+protected:
   UnhandledCaseException() : UnreachableCodeException() {}
-  UnhandledCaseException(std::string msg) : UnreachableCodeException(msg) {}
-  UnhandledCaseException(const char* msg) : UnreachableCodeException(msg) {}
+
+public:
+  UnhandledCaseException(const char* function, const char* file,
+                         unsigned line, const char* fmt, ...) :
+    UnreachableCodeException() {
+    va_list args;
+    va_start(args, fmt);
+    construct("Unhandled case encountered",
+              NULL, function, file, line, fmt, args);
+    va_end(args);
+  }
+
+  UnhandledCaseException(const char* function, const char* file,
+                         unsigned line, int theCase) :
+    UnreachableCodeException() {
+    construct("Unhandled case encountered",
+              NULL, function, file, line, "The case was: %d", theCase);
+  }
+
+  UnhandledCaseException(const char* function, const char* file,
+                         unsigned line) :
+    UnreachableCodeException() {
+    construct("Unhandled case encountered", NULL, function, file, line);
+  }
 };/* class UnhandledCaseException */
 
+class CVC4_PUBLIC IllegalArgumentException : public AssertionException {
+protected:
+  IllegalArgumentException() : AssertionException() {}
+
+public:
+  IllegalArgumentException(const char* argDesc, const char* function,
+                           const char* file, unsigned line,
+                           const char* fmt, ...) :
+    AssertionException() {
+    va_list args;
+    va_start(args, fmt);
+    construct("Illegal argument detected",
+              argDesc, function, file, line, fmt, args);
+    va_end(args);
+  }
+
+  IllegalArgumentException(const char* argDesc, const char* function,
+                           const char* file, unsigned line) :
+    AssertionException() {
+    construct("Illegal argument detected",
+              argDesc, function, file, line);
+  }
+};/* class IllegalArgumentException */
+
+#define AlwaysAssert(cond, msg...) \
+  do { \
+    if(EXPECT_FALSE( ! (cond) )) { \
+      throw AssertionException(#cond, __FUNCTION__, __FILE__, __LINE__, ## msg); \
+    } \
+  } while(0)
+#define Unreachable(msg...) \
+  throw UnreachableCodeException(__FUNCTION__, __FILE__, __LINE__, ## msg)
+#define Unhandled(msg...) \
+  throw UnhandledCaseException(__FUNCTION__, __FILE__, __LINE__, ## msg)
+#define IllegalArgument(arg, msg...) \
+  throw IllegalArgumentException(#arg, __FUNCTION__, __FILE__, __LINE__, ## msg)
+
 #ifdef CVC4_ASSERTIONS
-#  define Assert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ":  " #cond, __builtin_expect((cond), 1), ## msg)
+#  define Assert(cond, msg...) AlwaysAssert(cond, ## msg)
 #else /* ! CVC4_ASSERTIONS */
 #  define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/
 #endif /* CVC4_ASSERTIONS */
 
-#define AlwaysAssert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ":  " #cond, __builtin_expect((cond), 1), ## msg)
-#define Unreachable(msg...) __CVC4_UNREACHABLEGLUE("Hit a section of unreachable code at " __FILE__ ":", __LINE__, ## msg)
-#define Unhandled(msg...) __CVC4_UNHANDLEDGLUE("Hit an unhandled case at " __FILE__ ":", __LINE__, ## msg)
-
-#define __CVC4_ASSERTGLUE(str1, line, str2, cond, msg...) AssertImpl(str1 #line str2, cond, ## msg)
-#define __CVC4_UNREACHABLEGLUE(str, line, msg...) UnreachableImpl(str #line, ## msg)
-#define __CVC4_UNHANDLEDGLUE(str, line, msg...) UnhandledImpl(str #line, ## msg)
-
-inline void AssertImpl(const char* info, bool cond, std::string msg) {
-  if(EXPECT_FALSE( ! cond ))
-    throw AssertionException(std::string(info) + "\n" + msg);
-}
-
-inline void AssertImpl(const char* info, bool cond, const char* msg) {
-  if(EXPECT_FALSE( ! cond ))
-    throw AssertionException(std::string(info) + "\n" + msg);
-}
-
-inline void AssertImpl(const char* info, bool cond) {
-  if(EXPECT_FALSE( ! cond ))
-    throw AssertionException(info);
-}
-
-#ifdef __GNUC__
-inline void UnreachableImpl(const char* info, std::string msg) __attribute__ ((noreturn));
-inline void UnreachableImpl(const char* info, const char* msg) __attribute__ ((noreturn));
-inline void UnreachableImpl(const char* info) __attribute__ ((noreturn));
-#endif /* __GNUC__ */
-
-inline void UnreachableImpl(const char* info, std::string msg) {
-  throw UnreachableCodeException(std::string(info) + "\n" + msg);
-}
-
-inline void UnreachableImpl(const char* info, const char* msg) {
-  throw UnreachableCodeException(std::string(info) + "\n" + msg);
-}
-
-inline void UnreachableImpl(const char* info) {
-  throw UnreachableCodeException(info);
-}
-
-#ifdef __GNUC__
-inline void UnhandledImpl(const char* info, std::string msg) __attribute__ ((noreturn));
-inline void UnhandledImpl(const char* info, const char* msg) __attribute__ ((noreturn));
-inline void UnhandledImpl(const char* info) __attribute__ ((noreturn));
-#endif /* __GNUC__ */
-
-inline void UnhandledImpl(const char* info, std::string msg) {
-  throw UnhandledCaseException(std::string(info) + "\n" + msg);
-}
-
-inline void UnhandledImpl(const char* info, const char* msg) {
-  throw UnhandledCaseException(std::string(info) + "\n" + msg);
-}
-
-inline void UnhandledImpl(const char* info) {
-  throw UnhandledCaseException(info);
-}
-
 }/* CVC4 namespace */
 
 #endif /* __CVC4__ASSERT_H */
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 8baf872d2..b6c116a6d 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -5,6 +5,20 @@ AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 noinst_LTLIBRARIES = libutil.la
 
 libutil_la_SOURCES = \
+	Assert.h \
+	Assert.cpp \
+	Makefile.am \
+	Makefile.in \
 	command.cpp \
+	command.h \
+	debug.h \
 	decision_engine.cpp \
-	output.cpp
+	decision_engine.h \
+	exception.h \
+	literal.h \
+	model.h \
+	options.h \
+	output.cpp \
+	output.h \
+	result.h \
+	unique_id.h
diff --git a/src/util/Makefile.in b/src/util/Makefile.in
index ac8d4b522..9f17df4c7 100644
--- a/src/util/Makefile.in
+++ b/src/util/Makefile.in
@@ -52,7 +52,8 @@ CONFIG_CLEAN_FILES =
 CONFIG_CLEAN_VPATH_FILES =
 LTLIBRARIES = $(noinst_LTLIBRARIES)
 libutil_la_LIBADD =
-am_libutil_la_OBJECTS = command.lo decision_engine.lo output.lo
+am_libutil_la_OBJECTS = Assert.lo command.lo decision_engine.lo \
+	output.lo
 libutil_la_OBJECTS = $(am_libutil_la_OBJECTS)
 DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir)
 depcomp = $(SHELL) $(top_srcdir)/config/depcomp
@@ -67,6 +68,15 @@ CXXLD = $(CXX)
 CXXLINK = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
 	--mode=link $(CXXLD) $(AM_CXXFLAGS) $(CXXFLAGS) $(AM_LDFLAGS) \
 	$(LDFLAGS) -o $@
+COMPILE = $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) \
+	$(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+LTCOMPILE = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+	--mode=compile $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \
+	$(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+CCLD = $(CC)
+LINK = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+	--mode=link $(CCLD) $(AM_CFLAGS) $(CFLAGS) $(AM_LDFLAGS) \
+	$(LDFLAGS) -o $@
 SOURCES = $(libutil_la_SOURCES)
 DIST_SOURCES = $(libutil_la_SOURCES)
 ETAGS = etags
@@ -211,9 +221,23 @@ AM_CXXFLAGS = -Wall -fvisibility=hidden
 AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 noinst_LTLIBRARIES = libutil.la
 libutil_la_SOURCES = \
+	Assert.h \
+	Assert.cpp \
+	Makefile.am \
+	Makefile.in \
 	command.cpp \
+	command.h \
+	debug.h \
 	decision_engine.cpp \
-	output.cpp
+	decision_engine.h \
+	exception.h \
+	literal.h \
+	model.h \
+	options.h \
+	output.cpp \
+	output.h \
+	result.h \
+	unique_id.h
 
 all: all-am
 
@@ -267,6 +291,7 @@ mostlyclean-compile:
 distclean-compile:
 	-rm -f *.tab.c
 
+@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/Assert.Plo@am__quote@
 @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/command.Plo@am__quote@
 @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/decision_engine.Plo@am__quote@
 @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/output.Plo@am__quote@
diff --git a/src/util/exception.h b/src/util/exception.h
index 164cda8b5..d239f48de 100644
--- a/src/util/exception.h
+++ b/src/util/exception.h
@@ -31,7 +31,7 @@ public:
   Exception(const char* msg) : d_msg(msg) {}
   // Destructor
   virtual ~Exception() {}
-  // NON-VIRTUAL METHODs for setting and printing the error message
+  // NON-VIRTUAL METHOD for setting and printing the error message
   void setMessage(const std::string& msg) { d_msg = msg; }
   // Printing: feel free to redefine toString().  When inherited,
   // it's recommended that this method print the type of exception
@@ -41,20 +41,10 @@ public:
   friend std::ostream& operator<<(std::ostream& os, const Exception& e);
 };/* class Exception */
 
-
-class CVC4_PUBLIC IllegalArgumentException : public Exception {
-public:
-  IllegalArgumentException() : Exception("Illegal argument to method or function") {}
-  IllegalArgumentException(const std::string& msg) : Exception(msg) {}
-  IllegalArgumentException(const char* msg) : Exception(msg) {}
-};/* class IllegalArgumentException */
-
-
 inline std::ostream& operator<<(std::ostream& os, const Exception& e) {
   return os << e.toString();
 }
 
-
 }/* CVC4 namespace */
 
 #endif /* __CVC4__EXCEPTION_H */