various fixes and updates to use and support parser

19 files changed, 264 insertions, 149 deletions

diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl
index a270e7362..5c1f605c9 100755
--- a/contrib/update-copyright.pl
+++ b/contrib/update-copyright.pl
@@ -27,6 +27,24 @@ my $excluded_directories = '^(minisat|CVS)$';
 # "1985, 1987, 1992, 1997, 2008" or "2006-2009" or whatever.
 my $years = '2009';
 
+my $standard_template = <<EOF;
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) $years 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.
+EOF
+
+my $public_template = <<EOF;
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) $years 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.
+EOF
+
 ## end config ##
 
 use strict;
@@ -92,12 +110,7 @@ sub recurse {
           print $OUT "/*********************                                           -*- C++ -*-  */\n";
         }
         print $OUT "/** $file\n";
-        print $OUT " ** This file is part of the CVC4 prototype.\n";
-        print $OUT " ** Copyright (c) $years The Analysis of Computer Systems Group (ACSys)\n";
-        print $OUT " ** Courant Institute of Mathematical Sciences\n";
-        print $OUT " ** New York University\n";
-        print $OUT " ** See the file COPYING in the top-level source directory for licensing\n";
-        print $OUT " ** information.\n";
+        print $OUT $standard_template;
         print $OUT " **\n";
         while(my $line = <$IN>) {
           last if $line =~ /^ \*\*\s*$/;
@@ -111,12 +124,7 @@ sub recurse {
           print $OUT "/*********************                                           -*- C++ -*-  */\n";
         }
         print $OUT "/** $file\n";
-        print $OUT " ** This file is part of the CVC4 prototype.\n";
-        print $OUT " ** Copyright (c) $years The Analysis of Computer Systems Group (ACSys)\n";
-        print $OUT " ** Courant Institute of Mathematical Sciences\n";
-        print $OUT " ** New York University\n";
-        print $OUT " ** See the file COPYING in the top-level source directory for licensing\n";
-        print $OUT " ** information.\n";
+        print $OUT $standard_template;
         print $OUT " **\n";
         print $OUT " ** [[ Add file-specific comments here ]]\n";
         print $OUT " **/\n\n";
diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
index e25cf8595..f94a3c438 100644
--- a/src/expr/expr.cpp
+++ b/src/expr/expr.cpp
@@ -86,13 +86,4 @@ Expr Expr::xorExpr(const Expr& right) const {
   return ExprBuilder(*this).xorExpr(right);
 }
 
-Expr Expr::skolemExpr(int i) const {
-  return ExprBuilder(*this).skolemExpr(i);
-}
-
-Expr Expr::substExpr(const std::vector<Expr>& oldTerms,
-                     const std::vector<Expr>& newTerms) const {
-  return ExprBuilder(*this).substExpr(oldTerms, newTerms);
-}
-
 }/* CVC4 namespace */
diff --git a/src/expr/expr.h b/src/expr/expr.h
index d99708991..19f02650e 100644
--- a/src/expr/expr.h
+++ b/src/expr/expr.h
@@ -10,8 +10,8 @@
  ** Reference-counted encapsulation of a pointer to an expression.
  **/
 
-#ifndef __CVC4_EXPR_H
-#define __CVC4_EXPR_H
+#ifndef __CVC4__EXPR_H
+#define __CVC4__EXPR_H
 
 #include <vector>
 #include <stdint.h>
@@ -74,9 +74,6 @@ public:
   Expr iffExpr(const Expr& right) const;
   Expr impExpr(const Expr& right) const;
   Expr xorExpr(const Expr& right) const;
-  Expr skolemExpr(int i) const;
-  Expr substExpr(const std::vector<Expr>& oldTerms,
-                 const std::vector<Expr>& newTerms) const;
 
   Expr plusExpr(const Expr& right) const;
   Expr uMinusExpr() const;
@@ -100,4 +97,4 @@ inline Kind Expr::getKind() const {
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4_EXPR_H */
+#endif /* __CVC4__EXPR_H */
diff --git a/src/expr/expr_builder.cpp b/src/expr/expr_builder.cpp
index bf572cfbc..be9c60199 100644
--- a/src/expr/expr_builder.cpp
+++ b/src/expr/expr_builder.cpp
@@ -157,14 +157,6 @@ ExprBuilder& ExprBuilder::xorExpr(const Expr& right) {
   return *this;
 }
 
-ExprBuilder& ExprBuilder::skolemExpr(int i) {
-  Assert( d_kind != UNDEFINED_KIND );
-  collapse();
-  d_kind = SKOLEM;
-  //addChild(i);//FIXME: int constant
-  return *this;
-}
-
 // "Stream" expression constructor syntax
 ExprBuilder& ExprBuilder::operator<<(const Kind& op) {
   return *this;
@@ -217,37 +209,13 @@ void ExprBuilder::addChild(ExprValue* ev) {
   }
 }
 
-void ExprBuilder::collapse() {
+ExprBuilder& ExprBuilder::collapse() {
   if(d_nchildren == nchild_thresh) {
     vector<Expr>* v = new vector<Expr>();
     v->reserve(nchild_thresh + 5);
-    
+    //
   }
-}
-
-// not const
-ExprBuilder::operator Expr() {
-  // FIXME
-}
-
-AndExprBuilder   ExprBuilder::operator&&(Expr e) {
-  return AndExprBuilder(*this) && e;
-}
-
-OrExprBuilder    ExprBuilder::operator||(Expr e) {
-  return OrExprBuilder(*this) || e;
-}
-
-PlusExprBuilder  ExprBuilder::operator+ (Expr e) {
-  return PlusExprBuilder(*this) + e;
-}
-
-PlusExprBuilder  ExprBuilder::operator- (Expr e) {
-  return PlusExprBuilder(*this) - e;
-}
-
-MultExprBuilder  ExprBuilder::operator* (Expr e) {
-  return MultExprBuilder(*this) * e;
+  return *this;
 }
 
 }/* CVC4 namespace */
diff --git a/src/expr/expr_builder.h b/src/expr/expr_builder.h
index 97f18ca6d..13f196dd0 100644
--- a/src/expr/expr_builder.h
+++ b/src/expr/expr_builder.h
@@ -43,7 +43,7 @@ class ExprBuilder {
 
   void addChild(const Expr&);
   void addChild(ExprValue*);
-  void collapse();
+  ExprBuilder& collapse();
 
   typedef ExprValue** ev_iterator;
   typedef ExprValue const** const_ev_iterator;
@@ -74,12 +74,6 @@ public:
   ExprBuilder& iffExpr(const Expr& right);
   ExprBuilder& impExpr(const Expr& right);
   ExprBuilder& xorExpr(const Expr& right);
-  ExprBuilder& skolemExpr(int i);
-  ExprBuilder& substExpr(const std::vector<Expr>& oldTerms,
-                         const std::vector<Expr>& newTerms);
-  /*
-  ExprBuilder& substExpr(const ExprHashMap<Expr>& oldToNew);
-  */
 
   /* TODO design: these modify ExprBuilder */
   ExprBuilder& operator!() { return notExpr(); }
@@ -92,6 +86,7 @@ public:
 
   // For pushing sequences of children
   ExprBuilder& append(const std::vector<Expr>& children) { return append(children.begin(), children.end()); }
+  ExprBuilder& append(Expr child) { return append(&child, &(child)+1); }
   template <class Iterator> ExprBuilder& append(const Iterator& begin, const Iterator& end);
 
   operator Expr();// not const
@@ -102,71 +97,167 @@ public:
   PlusExprBuilder  operator- (Expr);
   MultExprBuilder  operator* (Expr);
 
+  friend class AndExprBuilder;
+  friend class OrExprBuilder;
+  friend class PlusExprBuilder;
+  friend class MultExprBuilder;
 };/* class ExprBuilder */
 
 class AndExprBuilder {
-  ExprManager* d_em;
+  ExprBuilder d_eb;
 
 public:
 
-  AndExprBuilder(const ExprBuilder&);
+  AndExprBuilder(const ExprBuilder& eb) : d_eb(eb) {
+    if(d_eb.d_kind != AND) {
+      d_eb.collapse();
+      d_eb.d_kind = AND;
+    }
+  }
 
   AndExprBuilder&   operator&&(Expr);
   OrExprBuilder     operator||(Expr);
 
-  operator ExprBuilder();
+  operator ExprBuilder() { return d_eb; }
 
 };/* class AndExprBuilder */
 
 class OrExprBuilder {
-  ExprManager* d_em;
+  ExprBuilder d_eb;
 
 public:
 
-  OrExprBuilder(const ExprBuilder&);
+  OrExprBuilder(const ExprBuilder& eb) : d_eb(eb) {
+    if(d_eb.d_kind != OR) {
+      d_eb.collapse();
+      d_eb.d_kind = OR;
+    }
+  }
 
   AndExprBuilder    operator&&(Expr);
   OrExprBuilder&    operator||(Expr);
 
-  operator ExprBuilder();
+  operator ExprBuilder() { return d_eb; }
 
 };/* class OrExprBuilder */
 
 class PlusExprBuilder {
-  ExprManager* d_em;
+  ExprBuilder d_eb;
 
 public:
 
-  PlusExprBuilder(const ExprBuilder&);
+  PlusExprBuilder(const ExprBuilder& eb) : d_eb(eb) {
+    if(d_eb.d_kind != PLUS) {
+      d_eb.collapse();
+      d_eb.d_kind = PLUS;
+    }
+  }
 
   PlusExprBuilder&  operator+(Expr);
   PlusExprBuilder&  operator-(Expr);
   MultExprBuilder   operator*(Expr);
 
-  operator ExprBuilder();
+  operator ExprBuilder() { return d_eb; }
 
 };/* class PlusExprBuilder */
 
 class MultExprBuilder {
-  ExprManager* d_em;
+  ExprBuilder d_eb;
 
 public:
 
-  MultExprBuilder(const ExprBuilder&);
+  MultExprBuilder(const ExprBuilder& eb) : d_eb(eb) {
+    if(d_eb.d_kind != MULT) {
+      d_eb.collapse();
+      d_eb.d_kind = MULT;
+    }
+  }
 
   PlusExprBuilder   operator+(Expr);
   PlusExprBuilder   operator-(Expr);
   MultExprBuilder&  operator*(Expr);
 
-  operator ExprBuilder();
+  operator ExprBuilder() { return d_eb; }
 
 };/* class MultExprBuilder */
 
 template <class Iterator>
-ExprBuilder& ExprBuilder::append(const Iterator& begin, const Iterator& end) {
+inline ExprBuilder& ExprBuilder::append(const Iterator& begin, const Iterator& end) {
+  return *this;
+}
+
+// not const
+inline ExprBuilder::operator Expr() {
+  // FIXME
+  return Expr::s_null;
+}
+
+inline AndExprBuilder   ExprBuilder::operator&&(Expr e) {
+  return AndExprBuilder(*this) && e;
+}
+
+inline OrExprBuilder    ExprBuilder::operator||(Expr e) {
+  return OrExprBuilder(*this) || e;
+}
+
+inline PlusExprBuilder  ExprBuilder::operator+ (Expr e) {
+  return PlusExprBuilder(*this) + e;
+}
+
+inline PlusExprBuilder  ExprBuilder::operator- (Expr e) {
+  return PlusExprBuilder(*this) - e;
+}
+
+inline MultExprBuilder  ExprBuilder::operator* (Expr e) {
+  return MultExprBuilder(*this) * e;
+}
+
+inline AndExprBuilder&  AndExprBuilder::operator&&(Expr e) {
+  d_eb.append(e);
+  return *this;
+}
+
+inline OrExprBuilder    AndExprBuilder::operator||(Expr e) {
+  return OrExprBuilder(d_eb.collapse()) || e;
+}
+
+inline AndExprBuilder   OrExprBuilder::operator&&(Expr e) {
+  return AndExprBuilder(d_eb.collapse()) && e;
+}
+
+inline OrExprBuilder&   OrExprBuilder::operator||(Expr e) {
+  d_eb.append(e);
+  return *this;
+}
+
+inline PlusExprBuilder& PlusExprBuilder::operator+(Expr e) {
+  d_eb.append(e);
+  return *this;
+}
+
+inline PlusExprBuilder& PlusExprBuilder::operator-(Expr e) {
+  d_eb.append(e.negate());
   return *this;
 }
 
+inline MultExprBuilder  PlusExprBuilder::operator*(Expr e) {
+  return MultExprBuilder(d_eb.collapse()) * e;
+}
+
+inline PlusExprBuilder  MultExprBuilder::operator+(Expr e) {
+  return MultExprBuilder(d_eb.collapse()) + e;
+}
+
+inline PlusExprBuilder  MultExprBuilder::operator-(Expr e) {
+  return MultExprBuilder(d_eb.collapse()) - e;
+}
+
+inline MultExprBuilder& MultExprBuilder::operator*(Expr e) {
+  d_eb.append(e);
+  return *this;
+}
+
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__EXPR_BUILDER_H */
diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp
index a65a2f3cd..3aeab8049 100644
--- a/src/expr/expr_manager.cpp
+++ b/src/expr/expr_manager.cpp
@@ -12,7 +12,7 @@
 
 #include "expr_builder.h"
 #include "expr_manager.h"
-#include "cvc4_expr.h"
+#include "expr/expr.h"
 
 namespace CVC4 {
 
diff --git a/src/include/cvc4.h b/src/include/cvc4.h
index 7b068228f..5d33fa838 100644
--- a/src/include/cvc4.h
+++ b/src/include/cvc4.h
@@ -18,29 +18,19 @@
 #include "util/result.h"
 #include "util/model.h"
 
-// In terms of abstraction, this is below (and provides services to)
-// ValidityChecker and above (and requires the services of)
-// PropEngine.
-
 namespace CVC4 {
 
-// 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()?
-//
-// Probably better than that is to have a configuration object that
-// indicates which passes are desired.  The configuration occurs
-// elsewhere (and can even occur at runtime).  A simple "pass manager"
-// of sorts determines check()'s behavior.
-//
-// The CNF conversion can go on in PropEngine.
-
 class SmtEngine {
   /** Current set of assertions. */
   // TODO: make context-aware to handle user-level push/pop.
   std::vector<Expr> d_assertList;
 
-private:
+  /** Our expression manager */
+  ExprManager *d_em;
+
+  /** User-level options */
+  Options *opts;
+
   /**
    * Pre-process an Expr.  This is expected to be highly-variable,
    * with a lot of "source-level configurability" to add multiple
@@ -74,10 +64,15 @@ private:
   void processAssertionList();
 
 public:
+  /*
+   * Construct an SmtEngine with the given expression manager and user options.
+   */
+  SmtEngine(ExprManager*, Options*);
+
   /**
-   * Execute a command
+   * Execute a command.
    */
-  void doCommand(Command c);
+  void doCommand(Command*);
 
   /**
    * Add a formula to the current context: preprocess, do per-theory
diff --git a/src/include/cvc4_expr.h b/src/include/cvc4_expr.h
index d99708991..863097123 100644
--- a/src/include/cvc4_expr.h
+++ b/src/include/cvc4_expr.h
@@ -74,9 +74,6 @@ public:
   Expr iffExpr(const Expr& right) const;
   Expr impExpr(const Expr& right) const;
   Expr xorExpr(const Expr& right) const;
-  Expr skolemExpr(int i) const;
-  Expr substExpr(const std::vector<Expr>& oldTerms,
-                 const std::vector<Expr>& newTerms) const;
 
   Expr plusExpr(const Expr& right) const;
   Expr uMinusExpr() const;
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index dcb23c303..5af3b5d21 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -25,9 +25,11 @@
 #include "util/exception.h"
 #include "usage.h"
 #include "about.h"
+#include "parser/language.h"
 
 using namespace std;
 using namespace CVC4;
+using namespace CVC4::parser;
 
 namespace CVC4 {
 namespace main {
@@ -39,12 +41,6 @@ Languages currently supported to the -L / --lang option:\n\
   smt | smtlib  SMT-LIB format\n\
 ";
 
-enum Language {
-  AUTO = 0,
-  PL,
-  SMTLIB,
-};/* enum Language */
-
 enum OptionValue {
   SMTCOMP = 256, /* no clash with char options */
   STATS
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 8529f2ca2..1fc616fe6 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -10,6 +10,8 @@
  ** [[ Add file-specific comments here ]]
  **/
 
+#include <iostream>
+#include <fstream>
 #include <cstdio>
 #include <cstdlib>
 #include <cerrno>
@@ -23,9 +25,14 @@
 #include "config.h"
 #include "main.h"
 #include "usage.h"
+#include "parser/parser.h"
+#include "expr/expr_manager.h"
+#include "smt/smt_engine.h"
+#include "parser/language.h"
 
 using namespace std;
 using namespace CVC4;
+using namespace CVC4::parser;
 using namespace CVC4::main;
 
 int main(int argc, char *argv[]) {
@@ -36,28 +43,37 @@ int main(int argc, char *argv[]) {
 
     int firstArgIndex = parseOptions(argc, argv, &opts);
 
-    FILE *infile;
+    istream *in;
+    ifstream infile;
+    Language lang = PL;
 
     if(firstArgIndex >= argc) {
-      infile = stdin;
+      in = &cin;
     } else if(argc > firstArgIndex + 1) {
       throw new Exception("Too many input files specified.");
     } else {
-      infile = fopen(argv[firstArgIndex], "r");
+      in = &infile;
+      if(strlen(argv[firstArgIndex]) >= 4 && !strcmp(argv[firstArgIndex] + strlen(argv[firstArgIndex]) - 4, ".smt"))
+        lang = SMTLIB;
+      infile.open(argv[firstArgIndex], ifstream::in);
+
       if(!infile) {
         throw new Exception(string("Could not open input file `") + argv[firstArgIndex] + "' for reading: " + strerror(errno));
         exit(1);
       }
+    }
 
-      // ExprManager *exprMgr = ...;
-      // SmtEngine smt(exprMgr, &opts);
-      // Parser parser(infile, exprMgr, &opts);
-      // while(!parser.done) {
-      //   Command *cmd = parser.get();
-      //   cmd->invoke(smt);
-      //   delete cmd;
-      // }
+    ExprManager *exprMgr = new ExprManager();
+    SmtEngine smt(exprMgr, &opts);
+    Parser parser(&smt, lang, *in, &opts);
+    while(!parser.done()) {
+      Command *cmd = parser.next();
+      cmd->invoke();
+      delete cmd;
     }
+
+    if(infile)
+      infile.close();
   } catch(CVC4::main::OptionException* e) {
     if(opts.smtcomp_mode) {
       printf("unknown");
diff --git a/src/parser/language.h b/src/parser/language.h
new file mode 100644
index 000000000..7ea6547cd
--- /dev/null
+++ b/src/parser/language.h
@@ -0,0 +1,31 @@
+/*********************                                           -*- C++ -*-  */
+/** language.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.
+ **
+ ** Input languages.
+ **/
+
+#ifndef __CVC4__PARSER__LANGUAGE_H
+#define __CVC4__PARSER__LANGUAGE_H
+
+#include "util/exception.h"
+#include "parser/language.h"
+
+namespace CVC4 {
+namespace parser {
+
+enum Language {
+  AUTO = 0,
+  PL,
+  SMTLIB,
+};/* enum Language */
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PARSER__LANGUAGE_H */
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 36b8c34eb..73565b8c4 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -13,13 +13,13 @@
 #ifndef __CVC4__PARSER__PARSER_H
 #define __CVC4__PARSER__PARSER_H
 
-#include "core/exception.h"
-#include "core/lang.h"
+#include "util/exception.h"
+#include "parser/language.h"
+#include "util/command.h"
 
 namespace CVC4 {
 namespace parser {
 
-  class ValidityChecker;
   class Expr;
   
   // Internal parser state and other data
@@ -33,16 +33,11 @@ namespace parser {
     void deleteParser();
   public:
     // Constructors
-    Parser(ValidityChecker* vc, InputLanguage lang,
-	   // The 'interactive' flag is ignored when fileName != ""
-	   bool interactive = true,
-	   const std::string& fileName = "");
-    Parser(ValidityChecker* vc, InputLanguage lang, std::istream& is,
-	   bool interactive = false);
+    Parser(CVC4::SmtEngine* smt, Language lang, std::istream& is, Options* opts, bool interactive = false);
     // Destructor
     ~Parser();
     // Read the next command.  
-    Expr next();
+    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
diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h
index 4eda5eb38..1d013a0b4 100644
--- a/src/parser/parser_state.h
+++ b/src/parser/parser_state.h
@@ -19,7 +19,7 @@
 
 #include <iostream>
 #include <sstream>
-#include "cvc4_expr.h"
+#include "expr/expr.h"
 #include "expr/expr_manager.h"
 #include "util/exception.h"
 
diff --git a/src/parser/pl.ypp b/src/parser/pl.ypp
index e7d752419..b59c7c69e 100644
--- a/src/parser/pl.ypp
+++ b/src/parser/pl.ypp
@@ -13,10 +13,10 @@
 
 %{
 
-#include "cvc4.h"
-#include "cvc4_expr.h"
+#include "smt/smt_engine.h"
 #include "parser/parser_exception.h"
 #include "parser/parser_state.h"
+#include "expr/expr.h"
 #include "expr/expr_builder.h"
 #include "expr/expr_manager.h"
 #include "util/command.h"
diff --git a/src/parser/smtlib.ypp b/src/parser/smtlib.ypp
index 692a9cda5..e616b3a65 100644
--- a/src/parser/smtlib.ypp
+++ b/src/parser/smtlib.ypp
@@ -11,10 +11,12 @@
  ** commands in SMT-LIB language.
  **/
 
-#include "cvc4.h"
+#include "smt/smt_engine.h"
 #include "parser/parser_exception.h"
 #include "parser/parser_state.h"
 
+#include <vector>
+
 // Exported shared data
 namespace CVC4 {
   extern ParserState* parserState;
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 08d485882..5969e82d1 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -12,7 +12,7 @@
 #ifndef __CVC4__PROP__PROP_ENGINE_H
 #define __CVC4__PROP__PROP_ENGINE_H
 
-#include "cvc4_expr.h"
+#include "expr/expr.h"
 #include "util/decision_engine.h"
 #include "theory/theory_engine.h"
 
diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am
index 325999db2..b8fc81961 100644
--- a/src/smt/Makefile.am
+++ b/src/smt/Makefile.am
@@ -4,4 +4,5 @@ AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 
 noinst_LTLIBRARIES = libsmt.la
 
-libsmt_la_SOURCES =
+libsmt_la_SOURCES = \
+	smt_engine.cpp
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 078bf9cde..149de058e 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -1,5 +1,5 @@
 /*********************                                           -*- C++ -*-  */
-/** prover.h
+/** cvc4.h
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -9,20 +9,22 @@
  **
  **/
 
-#ifndef __CVC4__SMT__SMT_ENGINE_H
-#define __CVC4__SMT__SMT_ENGINE_H
+#ifndef __CVC4__SMT_ENGINE_H
+#define __CVC4__SMT_ENGINE_H
 
 #include <vector>
-#include "core/cvc4_expr.h"
-#include "core/result.h"
-#include "core/model.h"
+#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"
 
 // In terms of abstraction, this is below (and provides services to)
 // ValidityChecker and above (and requires the services of)
 // PropEngine.
 
 namespace CVC4 {
-namespace smt {
 
 // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
 // hood): use a type parameter and have check() delegate, or subclass
@@ -40,7 +42,12 @@ class SmtEngine {
   // TODO: make context-aware to handle user-level push/pop.
   std::vector<Expr> d_assertList;
 
-private:
+  /** Our expression manager */
+  ExprManager *d_em;
+
+  /** User-level options */
+  Options *d_opts;
+
   /**
    * Pre-process an Expr.  This is expected to be highly-variable,
    * with a lot of "source-level configurability" to add multiple
@@ -74,6 +81,16 @@ private:
   void processAssertionList();
 
 public:
+  /*
+   * Construct an SmtEngine with the given expression manager and user options.
+   */
+  SmtEngine(ExprManager* em, Options* opts) : d_em(em), d_opts(opts) {}
+
+  /**
+   * Execute a command.
+   */
+  void doCommand(Command*);
+
   /**
    * Add a formula to the current context: preprocess, do per-theory
    * setup, use processAssertionList(), asserting to T-solver for
@@ -110,7 +127,6 @@ public:
   void pop();
 };/* class SmtEngine */
 
-}/* CVC4::smt namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__SMT__SMT_ENGINE_H */
+#endif /* __CVC4__SMT_ENGINE_H */
diff --git a/src/util/command.h b/src/util/command.h
index 804d37717..976e2b3d7 100644
--- a/src/util/command.h
+++ b/src/util/command.h
@@ -12,26 +12,37 @@
 #ifndef __CVC4__COMMAND_H
 #define __CVC4__COMMAND_H
 
+#include "expr/expr.h"
+
 namespace CVC4 {
 
-class Command { 
-   // distinct from Exprs
+class SmtEngine;
+
+class Command {
+  SmtEngine* d_smt;
+
+public:
+  Command(CVC4::SmtEngine* smt) : d_smt(smt) {}
+  virtual void invoke() = 0;
 };
 
 class AssertCommand : public Command {
 public:
   AssertCommand(const Expr&);
+  void invoke() { }
 };
 
 class CheckSatCommand : public Command {
 public:
   CheckSatCommand(void);
   CheckSatCommand(const Expr&);
+  void invoke() { }
 };
 
 class QueryCommand : public Command {
 public:
   QueryCommand(const Expr&);
+  void invoke() { }
 };