additional work on parser hookup, configuration + build

20 files changed, 357 insertions, 133 deletions

diff --git a/Makefile.am b/Makefile.am
index b3e12c811..02d9e1bea 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -5,3 +5,8 @@ ACLOCAL_AMFLAGS = -I config
 
 SUBDIRS = src test doc contrib
 
+.PHONY: production debug default competition
+production: ; @srcdir@/configure --with-build=production && $(MAKE)
+debug:      ; @srcdir@/configure --with-build=debug && $(MAKE)
+default:    ; @srcdir@/configure --with-build=default && $(MAKE)
+competition:; @srcdir@/configure --with-build=competition && $(MAKE)
diff --git a/configure.ac b/configure.ac
index 0aba48aa3..168f80320 100644
--- a/configure.ac
+++ b/configure.ac
@@ -11,9 +11,15 @@ AC_CONFIG_HEADERS([config.h])
 
 # keep track of whether the user set these (check here, because
 # autoconf might set a default later)
+AC_MSG_CHECKING([for user CPPFLAGS])
 if test -z "${CPPFLAGS+set}"; then user_cppflags=no; else user_cppflags=yes; fi
+AC_MSG_RESULT([${CPPFLAGS-none}])
+AC_MSG_CHECKING([for user CXXFLAGS])
 if test -z "${CXXFLAGS+set}"; then user_cxxflags=no; else user_cxxflags=yes; fi
+AC_MSG_RESULT([${CXXFLAGS-none}])
+AC_MSG_CHECKING([for user LDFLAGS])
 if test -z "${LDFLAGS+set}" ; then user_ldflags=no ; else user_ldflags=yes ; fi
+AC_MSG_RESULT([${LDFLAGS-none}])
 
 LT_INIT
 
@@ -209,6 +215,16 @@ AC_TYPE_SIZE_T
 
 # Prepare configure output
 
+if test "$user_cppflags" = no; then
+  CPPFLAGS="$CVC4CPPFLAGS"
+fi
+if test "$user_cxxflags" = no; then
+  CXXFLAGS="$CVC4CXXFLAGS"
+fi
+if test "$user_ldflags" = no; then
+  LDFLAGS="$CVC4LDFLAGS"
+fi
+
 AC_CONFIG_FILES([
   Makefile
   contrib/Makefile
@@ -251,7 +267,7 @@ LDFLAGS      : $LDFLAGS
 
 Now just type make, followed by make check or make install, as you like.
 
-You can also use 'make build_profile' to reconfigure for a different profile.
+You can use 'make <build_profile>' to reconfig/build a different profile.
 Build profiles: production optimized default competition
 
 EOF
@@ -262,8 +278,6 @@ if test "$user_cppflags" = yes; then
   AC_MSG_WARN([To support your options to configure, I would like to set CPPFLAGS to:])
   AC_MSG_WARN([    $CVC4CPPFLAGS])
   AC_MSG_WARN([])
-else
-  CPPFLAGS="$CVC4CPPFLAGS"
 fi
 if test "$user_cxxflags" = yes; then
   AC_MSG_WARN([])
@@ -271,8 +285,6 @@ if test "$user_cxxflags" = yes; then
   AC_MSG_WARN([To support your options to configure, I would like to set CXXFLAGS to:])
   AC_MSG_WARN([    $CVC4CXXFLAGS])
   AC_MSG_WARN([])
-else
-  CXXFLAGS="$CVC4CXXFLAGS"
 fi
 if test "$user_ldflags" = yes; then
   AC_MSG_WARN([])
@@ -280,8 +292,6 @@ if test "$user_ldflags" = yes; then
   AC_MSG_WARN([To support your options to configure, I would like to set LDFLAGS to:])
   AC_MSG_WARN([    $CVC4LDFLAGS])
   AC_MSG_WARN([])
-else
-  LDFLAGS="$CVC4LDFLAGS"
 fi
 
 non_standard=
diff --git a/src/include/cvc4.h b/src/include/cvc4.h
index 5d33fa838..bbaffabb0 100644
--- a/src/include/cvc4.h
+++ b/src/include/cvc4.h
@@ -67,7 +67,7 @@ public:
   /*
    * Construct an SmtEngine with the given expression manager and user options.
    */
-  SmtEngine(ExprManager*, Options*);
+  SmtEngine(ExprManager*, Options*) throw();
 
   /**
    * Execute a command.
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 1fc616fe6..58d86a42d 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -71,9 +71,6 @@ int main(int argc, char *argv[]) {
       cmd->invoke();
       delete cmd;
     }
-
-    if(infile)
-      infile.close();
   } catch(CVC4::main::OptionException* e) {
     if(opts.smtcomp_mode) {
       printf("unknown");
diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index 7965b88f9..8d8730d68 100644
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -5,19 +5,21 @@ AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 noinst_LTLIBRARIES = libparser.la
 
 libparser_la_SOURCES = \
+	parser.cpp \
+	parser_state.cpp \
+	symbol_table.cpp \
 	pl_scanner.lpp \
-	pl.ypp # \
-	# smtlib_scanner.lpp \
-	# smtlib.ypp \
-	# parser.cpp
+	pl.ypp
+#	smtlib_scanner.lpp \
+#	smtlib.ypp
 
 BUILT_SOURCES = \
 	pl_scanner.cpp \
 	pl.cpp \
-	pl.hpp # \
-	# smtlib_scanner.cpp \
-	# smtlib.cpp \
-	# smtlib.hpp
+	pl.hpp \
+	smtlib_scanner.cpp \
+	smtlib.cpp \
+	smtlib.hpp
 
 # produce headers too
 AM_YFLAGS = -d
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 89170beeb..42ff506fa 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -8,19 +8,87 @@
  ** information.
  **
  ** Parser implementation.
- **
- ** The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
  **/
 
-#include "parser.h"
-#include "parser_temp.h"
-#include "parser_exception.h"
+#include "parser/parser.h"
+#include "parser/parser_state.h"
+#include "parser/parser_exception.h"
+#include "parser/pl.hpp"
+//#include "parser/smtlib.hpp"
+
+// The communication entry points of the actual parsers
+
+// for presentation language (PL.y and PL.lex)
+extern int PLparse(); 
+extern void *PL_createBuffer(int);
+extern void PL_deleteBuffer(void *);
+extern void PL_switchToBuffer(void *);
+extern int PL_bufSize();
+extern void *PL_bufState();
+void PL_setInteractive(bool);
+
+// for smtlib language (smtlib.y and smtlib.lex)
+extern int smtlibparse(); 
+extern void *smtlib_createBuffer(int);
+extern void smtlib_deleteBuffer(void *);
+extern void smtlib_switchToBuffer(void *);
+extern int smtlib_bufSize();
+extern void *smtlibBufState();
+void smtlib_setInteractive(bool);
 
 namespace CVC4 {
+namespace parser {
 
-ParserTemp *parserTemp;
+ParserState *parserState;
 
-}/* CVC4 namespace */
+Parser::Parser(CVC4::SmtEngine* smt, Language lang, std::istream& is, CVC4::Options* opts, bool interactive) throw()
+  : d_smt(smt),
+    d_is(is),
+    d_opts(opts),
+    d_lang(lang),
+    d_interactive(interactive),
+    d_buffer(0) {
+
+  parserState->lineNum = 1;
+  switch(d_lang) {
+  case PL:
+    d_buffer = ::PL_createBuffer(::PL_bufSize());
+    break;
+  case SMTLIB:
+    //d_buffer = ::smtlib_createBuffer(::smtlib_bufSize());
+    break;
+  default:
+    Unhandled();
+  }
+}
 
+Parser::~Parser() throw() {
+  switch(d_lang) {
+  case PL:
+    ::PL_deleteBuffer(d_buffer);
+    break;
+  case SMTLIB:
+    //::smtlib_deleteBuffer(d_buffer);
+    break;
+  default:
+    Unhandled();
+  }
+}
+
+CVC4::Command* Parser::next() throw() {
+  return 0;
+}
+
+bool Parser::done() const throw() {
+  return false;
+}
+
+void Parser::printLocation(std::ostream & out) const throw() {
+}
+
+void Parser::reset() throw() {
+}
+
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 73565b8c4..8103238b3 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -13,47 +13,45 @@
 #ifndef __CVC4__PARSER__PARSER_H
 #define __CVC4__PARSER__PARSER_H
 
+#include <iostream>
+
 #include "util/exception.h"
 #include "parser/language.h"
+#include "parser/parser_state.h"
 #include "util/command.h"
+#include "util/options.h"
+#include "expr/expr.h"
+#include "smt/smt_engine.h"
+#include "util/assert.h"
 
 namespace CVC4 {
 namespace parser {
 
-  class Expr;
-  
-  // Internal parser state and other data
-  class ParserData;
-
-  class Parser {
-  private:
-    ParserData* d_data;
-    // Internal methods for constructing and destroying the actual parser
-    void initParser();
-    void deleteParser();
-  public:
-    // Constructors
-    Parser(CVC4::SmtEngine* smt, Language lang, std::istream& is, Options* opts, bool interactive = false);
-    // Destructor
-    ~Parser();
-    // Read the next command.  
-    CVC4::Command* next();
-    // Check if we are done (end of input has been reached)
-    bool done() const;
-    // The same check can be done by using the class Parser's value as
-    // a Boolean
-    operator bool() const { return done(); }
-    void printLocation(std::ostream & out) const;
-    // Reset any local data that depends on validity checker
-    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.
-  class ParserTemp;
-  extern ParserTemp* parserTemp;
+class Parser {
+
+  CVC4::SmtEngine *d_smt;
+  std::istream &d_is;
+  CVC4::Options *d_opts;
+  Language d_lang;
+  bool d_interactive;
+  void *d_buffer;
+
+public:
+  // Constructors
+  Parser(CVC4::SmtEngine* smt, Language lang, std::istream& is, CVC4::Options* opts, bool interactive = false) throw();
+  // Destructor
+  ~Parser() throw();
+  // Read the next command.
+  CVC4::Command* next() throw();
+  // Check if we are done (end of input has been reached)
+  bool done() const throw();
+  // The same check can be done by using the class Parser's value as
+  // a Boolean
+  operator bool() const throw() { return done(); }
+  void printLocation(std::ostream & out) const throw();
+  // Reset any local data that depends on SmtEngine
+  void reset() throw();
+}; // end of class Parser
 
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h
index 89490fad8..b2cf8bc55 100644
--- a/src/parser/parser_exception.h
+++ b/src/parser/parser_exception.h
@@ -14,24 +14,25 @@
 #define __CVC4__PARSER__PARSER_EXCEPTION_H
 
 #include "util/exception.h"
+#include "cvc4_config.h"
 #include <string>
 #include <iostream>
 
 namespace CVC4 {
 namespace parser {
 
-  class ParserException: public Exception {
-  public:
-    // Constructors
-    ParserException() { }
-    ParserException(const std::string& msg): Exception(msg) { }
-    ParserException(const char* msg): Exception(msg) { }
-    // Destructor
-    virtual ~ParserException() { }
-    virtual std::string toString() const {
-      return "Parse Error: " + d_msg;
-    }
-  }; // end of class ParserException
+class CVC4_PUBLIC ParserException: public Exception {
+public:
+  // Constructors
+  ParserException() { }
+  ParserException(const std::string& msg): Exception(msg) { }
+  ParserException(const char* msg): Exception(msg) { }
+  // Destructor
+  virtual ~ParserException() { }
+  virtual std::string toString() const {
+    return "Parse Error: " + d_msg;
+  }
+}; // end of class ParserException
 
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
diff --git a/src/parser/parser_state.cpp b/src/parser/parser_state.cpp
new file mode 100644
index 000000000..654fbfe32
--- /dev/null
+++ b/src/parser/parser_state.cpp
@@ -0,0 +1,25 @@
+/*********************                                           -*- C++ -*-  */
+/** parser_state.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.
+ **
+ ** Parser state implementation.
+ **/
+
+#include <string>
+#include "parser/parser_state.h"
+#include "parser/parser_exception.h"
+
+namespace CVC4 {
+namespace parser {
+
+void ParserState::error(const std::string& s) throw(ParserException*) {
+  throw new ParserException(s);
+}
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h
index 0fbedb958..2bcc08bef 100644
--- a/src/parser/parser_state.h
+++ b/src/parser/parser_state.h
@@ -22,6 +22,7 @@
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
 #include "parser/symbol_table.h"
+#include "parser/parser_exception.h"
 #include "util/exception.h"
 
 namespace CVC4 {
@@ -41,8 +42,8 @@ private:
   // The currently used prompt
   std::string prompt;
 public:
-  SmtEngine* smtEngine;
-  ExprManager* exprManager;
+  CVC4::SmtEngine* smtEngine;
+  CVC4::ExprManager* exprManager;
   SymbolTable* symbolTable;
   std::istream* is;
   // The current input line
@@ -50,7 +51,7 @@ public:
   // File name
   std::string fileName;
   // The last parsed Expr
-  Expr expr;
+  CVC4::Expr expr;
   // Whether we are done or not
   bool done;
   // Whether we are running interactive
@@ -64,37 +65,38 @@ public:
   // Did we encounter a formula query (smtlib)
   bool queryParsed;
   // Default constructor
-  ParserState() : d_uid(0),
-                  prompt1("CVC> "),
-                  prompt2("- "),
-                  prompt("CVC> "),
-                  smtEngine(0),
-                  exprManager(0),
-                  symbolTable(0),
-                  is(0),
-                  lineNum(1),
-                  fileName(),
-                  expr(Expr::null()),
-                  done(false),
-                  interactive(false),
-                  arrFlag(false),
-                  bvFlag(false),
-                  bvSize(0),
-                  queryParsed(false) { }
+  ParserState() throw()
+    : d_uid(0),
+      prompt1("CVC> "),
+      prompt2("- "),
+      prompt("CVC> "),
+      smtEngine(0),
+      exprManager(0),
+      symbolTable(0),
+      is(0),
+      lineNum(1),
+      fileName(),
+      expr(CVC4::Expr::null()),
+      done(false),
+      interactive(false),
+      arrFlag(false),
+      bvFlag(false),
+      bvSize(0),
+      queryParsed(false) { }
   // Parser error handling (implemented in parser.cpp)
-  int error(const std::string& s);
+  void error(const std::string& s) throw(ParserException*) __attribute__((noreturn));
   // Get the next uniqueID as a string
-  std::string uniqueID() {
+  std::string uniqueID() throw() {
     std::ostringstream ss;
     ss << d_uid++;
     return ss.str();
   }
   // Get the current prompt
-  std::string getPrompt() { return prompt; }
+  std::string getPrompt() throw() { return prompt; }
   // Set the prompt to the main one
-  void setPrompt1() { prompt = prompt1; }
+  void setPrompt1() throw() { prompt = prompt1; }
   // Set the prompt to the secondary one
-  void setPrompt2() { prompt = prompt2; }
+  void setPrompt2() throw() { prompt = prompt2; }
 };
 
 }/* CVC4::parser namespace */
diff --git a/src/parser/pl.ypp b/src/parser/pl.ypp
index 20687b783..a4aa7ef70 100644
--- a/src/parser/pl.ypp
+++ b/src/parser/pl.ypp
@@ -54,7 +54,8 @@ int PLerror(const char *s)
   std::ostringstream ss;
   ss << CVC4::parser::parserState->fileName << ":" << CVC4::parser::parserState->lineNum
      << ": " << s;
-  return CVC4::parser::parserState->error(ss.str());
+  CVC4::parser::parserState->error(ss.str());
+  return 0;// dead code; error() above throws an exception
 }
 
 #define YYLTYPE_IS_TRIVIAL 1
diff --git a/src/parser/symbol_table.cpp b/src/parser/symbol_table.cpp
new file mode 100644
index 000000000..296c07731
--- /dev/null
+++ b/src/parser/symbol_table.cpp
@@ -0,0 +1,37 @@
+/*********************                                           -*- C++ -*-  */
+/** symbol_table.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.
+ **
+ **/
+
+#include <string>
+#include <list>
+#include <vector>
+
+#include "expr/expr.h"
+#include "parser/symbol_table.h"
+
+namespace CVC4 {
+namespace parser {
+
+void SymbolTable::defineVar(const std::string, const void*) throw() {
+  
+}
+
+void SymbolTable::defineVarList(const std::list<std::string>*, const void*) throw() {
+}
+
+void SymbolTable::defineVarList(const std::vector<std::string>*, const void*) throw() {
+}
+
+// Type& SymbolTable::lookupType(const std::string&);
+Expr& SymbolTable::lookupVar(const std::string*) throw() {
+}
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h
index 3339ab67a..9135343f5 100644
--- a/src/parser/symbol_table.h
+++ b/src/parser/symbol_table.h
@@ -7,11 +7,6 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** Extra state of the parser shared by the lexer and parser.
- **
- ** The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
  **/
 
 #include <string>
@@ -21,17 +16,19 @@
 #include "expr/expr.h"
 
 namespace CVC4 {
+namespace parser {
 
 class SymbolTable {
 public:
   // FIXME: No definitions for Type yet
   // void defineType(const std::string&, const Type&);
-  void defineVar(const std::string, const void*);
-  void defineVarList(const std::list<std::string>*, const void*);
-  void defineVarList(const std::vector<std::string>*, const void*);
+  void defineVar(const std::string, const void*) throw();
+  void defineVarList(const std::list<std::string>*, const void*) throw();
+  void defineVarList(const std::vector<std::string>*, const void*) throw();
 
   // Type& lookupType(const std::string&);
-  Expr& lookupVar(const std::string*);
+  Expr& lookupVar(const std::string*) throw();
 };
 
-}
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f6b81465b..f9ebc713d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -10,8 +10,17 @@
  **/
 
 #include "smt/smt_engine.h"
+#include "util/exception.h"
+#include "util/command.h"
 
 namespace CVC4 {
 
+void doCommand(Command* c) {
+  if(c->getSmtEngine() != this)
+    throw new IllegalArgumentException("SmtEngine does not match Command");
+
+  c->invoke();
+}
+
 
 }/* CVC4 namespace */
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 149de058e..af2f45c23 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -15,7 +15,6 @@
 #include <vector>
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
-#include "util/command.h"
 #include "util/result.h"
 #include "util/model.h"
 #include "util/options.h"
@@ -26,6 +25,8 @@
 
 namespace CVC4 {
 
+class Command;
+
 // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
 // hood): use a type parameter and have check() delegate, or subclass
 // SmtEngine and override check()?
@@ -84,7 +85,7 @@ public:
   /*
    * Construct an SmtEngine with the given expression manager and user options.
    */
-  SmtEngine(ExprManager* em, Options* opts) : d_em(em), d_opts(opts) {}
+  SmtEngine(ExprManager* em, Options* opts) throw() : d_em(em), d_opts(opts) {}
 
   /**
    * Execute a command.
@@ -106,6 +107,12 @@ public:
   Result query(Expr);
 
   /**
+   * Add a formula to the current context and call check().  Returns
+   * true iff consistent.
+   */
+  Result checkSat(Expr);
+
+  /**
    * Simplify a formula without doing "much" work.  Requires assist
    * from the SAT Engine.
    */
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 4fe483c98..c70553c3e 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -4,4 +4,5 @@ AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 
 noinst_LTLIBRARIES = libutil.la
 
-libutil_la_SOURCES =
+libutil_la_SOURCES = \
+	command.cpp
diff --git a/src/util/assert.h b/src/util/assert.h
index 6691c1b04..4a164716c 100644
--- a/src/util/assert.h
+++ b/src/util/assert.h
@@ -20,20 +20,27 @@
 
 namespace CVC4 {
 
-class AssertionException : public Exception {
+class CVC4_PUBLIC AssertionException : public Exception {
 public:
   AssertionException() : Exception() {}
   AssertionException(std::string msg) : Exception(msg) {}
   AssertionException(const char* msg) : Exception(msg) {}
 };/* class AssertionException */
 
-class UnreachableCodeException : public AssertionException {
+class CVC4_PUBLIC UnreachableCodeException : public AssertionException {
 public:
   UnreachableCodeException() : AssertionException() {}
   UnreachableCodeException(std::string msg) : AssertionException(msg) {}
   UnreachableCodeException(const char* msg) : AssertionException(msg) {}
 };/* class UnreachableCodeException */
 
+class CVC4_PUBLIC UnhandledCaseException : public UnreachableCodeException {
+public:
+  UnhandledCaseException() : UnreachableCodeException() {}
+  UnhandledCaseException(std::string msg) : UnreachableCodeException(msg) {}
+  UnhandledCaseException(const char* msg) : UnreachableCodeException(msg) {}
+};/* class UnhandledCaseException */
+
 #ifdef CVC4_ASSERTIONS
 #  define Assert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ":  " #cond, __builtin_expect((cond), 1), ## msg)
 #else /* ! CVC4_ASSERTIONS */
@@ -41,10 +48,12 @@ public:
 #endif /* CVC4_ASSERTIONS */
 
 #define AlwaysAssert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ":  " #cond, __builtin_expect((cond), 1), ## msg)
-#define Unreachable(cond, msg...) __CVC4_UNREACHABLEGLUE("Hit a section of unreachable code at " __FILE__ ":", __LINE__, __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, cond, msg...) AssertImpl(str #line, 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 ))
@@ -79,6 +88,24 @@ inline void UnreachableImpl(const char* info) {
   throw new 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 new UnhandledCaseException(std::string(info) + "\n" + msg);
+}
+
+inline void UnhandledImpl(const char* info, const char* msg) {
+  throw new UnhandledCaseException(std::string(info) + "\n" + msg);
+}
+
+inline void UnhandledImpl(const char* info) {
+  throw new UnhandledCaseException(info);
+}
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__ASSERT_H */
diff --git a/src/util/command.cpp b/src/util/command.cpp
new file mode 100644
index 000000000..db03a9189
--- /dev/null
+++ b/src/util/command.cpp
@@ -0,0 +1,18 @@
+/*********************                                           -*- C++ -*-  */
+/** command.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.
+ **
+ **/
+
+#include "util/command.h"
+#include "smt/smt_engine.h"
+
+namespace CVC4 {
+
+
+}/* CVC4 namespace */
diff --git a/src/util/command.h b/src/util/command.h
index 976e2b3d7..6de87c9f2 100644
--- a/src/util/command.h
+++ b/src/util/command.h
@@ -13,39 +13,48 @@
 #define __CVC4__COMMAND_H
 
 #include "expr/expr.h"
+#include "smt/smt_engine.h"
 
 namespace CVC4 {
 
-class SmtEngine;
-
 class Command {
+protected:
   SmtEngine* d_smt;
 
 public:
   Command(CVC4::SmtEngine* smt) : d_smt(smt) {}
+  SmtEngine* getSmtEngine() { return d_smt; }
   virtual void invoke() = 0;
 };
 
 class AssertCommand : public Command {
+protected:
+  Expr d_expr;
+
 public:
-  AssertCommand(const Expr&);
-  void invoke() { }
+  AssertCommand(CVC4::SmtEngine* smt, const Expr& e) : Command(smt), d_expr(e) {}
+  void invoke() { d_smt->assert(d_expr); }
 };
 
 class CheckSatCommand : public Command {
+protected:
+  Expr d_expr;
+
 public:
-  CheckSatCommand(void);
-  CheckSatCommand(const Expr&);
-  void invoke() { }
+  CheckSatCommand(CVC4::SmtEngine* smt) : Command(smt), d_expr(Expr::null()) {}
+  CheckSatCommand(CVC4::SmtEngine* smt, const Expr& e) : Command(smt), d_expr(e) {}
+  void invoke() { d_smt->checkSat(d_expr); }
 };
 
 class QueryCommand : public Command {
+protected:
+  Expr d_expr;
+
 public:
-  QueryCommand(const Expr&);
-  void invoke() { }
+  QueryCommand(CVC4::SmtEngine* smt, const Expr& e) : Command(smt), d_expr(e) {}
+  void invoke() { d_smt->query(d_expr); }
 };
 
-
 }/* CVC4 namespace */
 
 #endif /* __CVC4__COMMAND_H */
diff --git a/src/util/exception.h b/src/util/exception.h
index e3b8f2293..76eabe67e 100644
--- a/src/util/exception.h
+++ b/src/util/exception.h
@@ -15,19 +15,20 @@
 
 #include <string>
 #include <iostream>
+#include "cvc4_config.h"
 
 namespace CVC4 {
 
-class Exception {
+class CVC4_PUBLIC Exception {
 protected:
   std::string d_msg;
 public:
   // Constructors
-  Exception(): d_msg("Unknown exception") { }
-  Exception(const std::string& msg): d_msg(msg) { }
-  Exception(const char* msg): d_msg(msg) { }
+  Exception() : d_msg("Unknown exception") {}
+  Exception(const std::string& msg) : d_msg(msg) {}
+  Exception(const char* msg) : d_msg(msg) {}
   // Destructor
-  virtual ~Exception() { }
+  virtual ~Exception() {}
   // NON-VIRTUAL METHODs for setting and printing the error message
   void setMessage(const std::string& msg) { d_msg = msg; }
   // Printing: feel free to redefine toString().  When inherited,
@@ -36,13 +37,22 @@ public:
   virtual std::string toString() const { return d_msg; }
   // No need to overload operator<< for the inherited classes
   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 */
 
-}; // end of class Exception
 
 inline std::ostream& operator<<(std::ostream& os, const Exception& e) {
   return os << e.toString();
 }
 
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__EXCEPTION_H */