From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 8 Dec 2009 10:10:20 +0000 (+0000)
Subject: work on propositional layer, expression builder support for large expressions, output... 
X-Git-Tag: cvc5-1.0.0~9388
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2163539a8b839acf98bda0e1a65f1fcca5232fb2;p=cvc5.git

work on propositional layer, expression builder support for large expressions, output classes, and minisat
---

diff --git a/Makefile.builds.in b/Makefile.builds.in
index f6e17b4ca..0955518bf 100644
--- a/Makefile.builds.in
+++ b/Makefile.builds.in
@@ -23,8 +23,8 @@ all:
 	thelibdir="$(abs_builddir)$(libdir)"; progdir="$(abs_builddir)$(bindir)"; file=cvc4; \
 		eval `grep '^relink_command=' $(CURRENT_BUILD)/src/main/cvc4 | sed 's:-Wl,-rpath:-Wl,-rpath -Wl,\\\\$$thelibdir -Wl,-rpath:'`; \
 		eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)"
-	ln -sfv "$(abs_builddir)$(libdir)" $(CURRENT_BUILD)/lib
-	ln -sfv "$(abs_builddir)$(bindir)" $(CURRENT_BUILD)/bin
+	test -e $(CURRENT_BUILD)/lib || ln -sfv "$(abs_builddir)$(libdir)" $(CURRENT_BUILD)/lib
+	test -e $(CURRENT_BUILD)/bin || ln -sfv "$(abs_builddir)$(bindir)" $(CURRENT_BUILD)/bin
 	# populate builds/bin and builds/lib
 	mkdir -pv ".$(bindir)" ".$(libdir)"
 	$(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/libcvc4.la "`pwd`$(libdir)"
@@ -32,8 +32,8 @@ all:
 	thelibdir="`pwd`$(libdir)"; progdir="`pwd`$(bindir)"; file=cvc4; \
 		eval `grep '^relink_command=' $(CURRENT_BUILD)/src/main/cvc4 | sed 's:-Wl,-rpath:-Wl,-rpath -Wl,\\\\$$thelibdir -Wl,-rpath:'`; \
 		eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)"
-	ln -sfv ".$(libdir)" lib
-	ln -sfv ".$(bindir)" bin
+	test -e lib || ln -sfv ".$(libdir)" lib
+	test -e bin || ln -sfv ".$(bindir)" bin
 
 %:
 	(cd $(CURRENT_BUILD) && $(MAKE) $@)
diff --git a/configure.ac b/configure.ac
index 8f844f75d..f8e789ab8 100644
--- a/configure.ac
+++ b/configure.ac
@@ -101,7 +101,7 @@ elif test -e src/include/cvc4_config.h; then
   echo Setting up "builds/$target/$build_type"...
   rm -fv config.log config.status confdefs.h
   mkdir -pv "builds/$target/$build_type"
-  test -e builds/Makefile || ln -sfv "$target/$build_type/Makefile.builds" builds/Makefile
+  ln -sfv "$target/$build_type/Makefile.builds" builds/Makefile
   echo Creating builds/current...
   (echo "# This is the most-recently-configured CVC4 build"; \
    echo "# 'make' in the top-level source directory applies to this build"; \
diff --git a/contrib/dimacs_to_smt.pl b/contrib/dimacs_to_smt.pl
new file mode 100755
index 000000000..305db1d8e
--- /dev/null
+++ b/contrib/dimacs_to_smt.pl
@@ -0,0 +1,36 @@
+#!/usr/bin/perl -w
+# DIMACS to SMT
+# Morgan Deters 2009
+
+use strict;
+
+my ($nvars, $nclauses);
+while(<>) {
+    next if /^c/;
+
+    if(/^p cnf (\d+) (\d+)/) {
+        ($nvars, $nclauses) = ($1, $2);
+        print "(benchmark b\n";
+        print ":status unknown\n";
+        print ":logic QF_UF\n";
+        for(my $i = 1; $i <= $nvars; ++$i) {
+            print ":extrapreds ((x$i))\n";
+        }
+        print ":formula (and\n";
+        next;
+    }
+
+    print "(or";
+    chomp;
+    @_ = split(/ /);
+    for(my $i = 0; $i < $#_; ++$i) {
+        if($_[$i] < 0) {
+            print " (not x" . -$_[$i] . ")";
+        } else {
+            print " x" . $_[$i];
+        }
+    }
+    print ")\n";
+}
+
+print "))\n";
diff --git a/src/expr/expr.h b/src/expr/expr.h
index a16ffee13..013888baa 100644
--- a/src/expr/expr.h
+++ b/src/expr/expr.h
@@ -60,19 +60,23 @@ class CVC4_PUBLIC Expr {
 public:
 
   /** Default constructor, makes a null expression. */
-  CVC4_PUBLIC Expr();
+  Expr();
 
-  CVC4_PUBLIC Expr(const Expr&);
+  Expr(const Expr&);
 
   /** Destructor.  Decrements the reference count and, if zero,
    *  collects the ExprValue. */
-  CVC4_PUBLIC ~Expr();
+  ~Expr();
 
-  Expr& operator=(const Expr&) CVC4_PUBLIC;
+  bool operator==(const Expr& e) const { return d_ev == e.d_ev; }
+  bool operator!=(const Expr& e) const { return d_ev != e.d_ev; }
+  bool operator<(const Expr& e) const { return d_ev < e.d_ev; }// for map key
+
+  Expr& operator=(const Expr&);
 
   /** Access to the encapsulated expression.
    *  @return the encapsulated expression. */
-  ExprValue* operator->() const CVC4_PUBLIC;
+  ExprValue* operator->() const;
 
   uint64_t hash() const;
 
diff --git a/src/expr/expr_builder.cpp b/src/expr/expr_builder.cpp
index be9c60199..4de22f987 100644
--- a/src/expr/expr_builder.cpp
+++ b/src/expr/expr_builder.cpp
@@ -12,7 +12,8 @@
 #include "expr_builder.h"
 #include "expr_manager.h"
 #include "expr_value.h"
-#include "util/assert.h"
+#include "util/Assert.h"
+#include "util/output.h"
 
 using namespace std;
 
@@ -159,15 +160,19 @@ ExprBuilder& ExprBuilder::xorExpr(const Expr& right) {
 
 // "Stream" expression constructor syntax
 ExprBuilder& ExprBuilder::operator<<(const Kind& op) {
+  d_kind = op;
   return *this;
 }
 
 ExprBuilder& ExprBuilder::operator<<(const Expr& child) {
+  addChild(child);
   return *this;
 }
 
 void ExprBuilder::addChild(const Expr& e) {
+  Debug("expr") << "adding child E " << e << endl;
   if(d_nchildren == nchild_thresh) {
+    Debug("expr") << "reached thresh " << nchild_thresh << ", copying" << endl;
     vector<Expr>* v = new vector<Expr>();
     v->reserve(nchild_thresh + 5);
     for(ExprValue** i = d_children.u_arr; i != d_children.u_arr + nchild_thresh; ++i) {
@@ -178,9 +183,11 @@ void ExprBuilder::addChild(const Expr& e) {
     d_children.u_vec = v;
     ++d_nchildren;
   } else if(d_nchildren > nchild_thresh) {
+    Debug("expr") << "over thresh " << d_nchildren << " > " << nchild_thresh << endl;
     d_children.u_vec->push_back(e);
     ++d_nchildren;
   } else {
+    Debug("expr") << "under thresh " << d_nchildren << " < " << nchild_thresh << endl;
     ExprValue *ev = e.d_ev;
     d_children.u_arr[d_nchildren] = ev;
     ev->inc();
@@ -189,7 +196,9 @@ void ExprBuilder::addChild(const Expr& e) {
 }
 
 void ExprBuilder::addChild(ExprValue* ev) {
+  Debug("expr") << "adding child ev " << ev << endl;
   if(d_nchildren == nchild_thresh) {
+    Debug("expr") << "reached thresh " << nchild_thresh << ", copying" << endl;
     vector<Expr>* v = new vector<Expr>();
     v->reserve(nchild_thresh + 5);
     for(ExprValue** i = d_children.u_arr; i != d_children.u_arr + nchild_thresh; ++i) {
@@ -200,9 +209,11 @@ void ExprBuilder::addChild(ExprValue* ev) {
     d_children.u_vec = v;
     ++d_nchildren;
   } else if(d_nchildren > nchild_thresh) {
+    Debug("expr") << "over thresh " << d_nchildren << " > " << nchild_thresh << endl;
     d_children.u_vec->push_back(Expr(ev));
     ++d_nchildren;
   } else {
+    Debug("expr") << "under thresh " << d_nchildren << " < " << nchild_thresh << endl;
     d_children.u_arr[d_nchildren] = ev;
     ev->inc();
     ++d_nchildren;
@@ -214,6 +225,7 @@ ExprBuilder& ExprBuilder::collapse() {
     vector<Expr>* v = new vector<Expr>();
     v->reserve(nchild_thresh + 5);
     //
+    Unreachable();// unimplemented
   }
   return *this;
 }
diff --git a/src/expr/expr_builder.h b/src/expr/expr_builder.h
index 5c6019de1..d70acb1fb 100644
--- a/src/expr/expr_builder.h
+++ b/src/expr/expr_builder.h
@@ -96,7 +96,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); }
+  ExprBuilder& append(Expr child) { return append(&child, (&child) + 1); }
   template <class Iterator> ExprBuilder& append(const Iterator& begin, const Iterator& end);
 
   operator Expr();// not const
@@ -193,24 +193,47 @@ public:
 
 template <class Iterator>
 inline ExprBuilder& ExprBuilder::append(const Iterator& begin, const Iterator& end) {
+  for(Iterator i = begin; i != end; ++i)
+    addChild(*i);
   return *this;
 }
 
 // not const
 inline ExprBuilder::operator Expr() {
-  uint64_t hash = d_kind;
-
-  for(ev_iterator i = ev_begin(); i != ev_end(); ++i)
-    hash = ((hash << 3) | ((hash & 0xE000000000000000ull) >> 61)) ^ (*i)->hash();
+  ExprValue *ev;
+  uint64_t hash;
+
+  // variables are permitted to be duplicates (from POV of the expression manager)
+  if(d_kind == VARIABLE) {
+    ev = new ExprValue;
+    hash = reinterpret_cast<uint64_t>(ev);
+  } else {
+    hash = d_kind;
+
+    if(d_nchildren <= nchild_thresh) {
+      for(ev_iterator i = ev_begin(); i != ev_end(); ++i)
+        hash = ((hash << 3) | ((hash & 0xE000000000000000ull) >> 61)) ^ (*i)->hash();
+
+      void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Expr));
+      ev = new (space) ExprValue;
+      size_t nc = 0;
+      for(ev_iterator i = ev_begin(); i != ev_end(); ++i)
+        ev->d_children[nc++] = Expr(*i);
+    } else {
+      for(std::vector<Expr>::iterator i = d_children.u_vec->begin(); i != d_children.u_vec->end(); ++i)
+        hash = ((hash << 3) | ((hash & 0xE000000000000000ull) >> 61)) ^ (*i)->hash();
+
+      void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Expr));
+      ev = new (space) ExprValue;
+      size_t nc = 0;
+      for(std::vector<Expr>::iterator i = d_children.u_vec->begin(); i != d_children.u_vec->end(); ++i)
+        ev->d_children[nc++] = Expr(*i);
+    }
+  }
 
-  void *space = std::malloc(sizeof(ExprValue) + d_nchildren * sizeof(Expr));
-  ExprValue *ev = new (space) ExprValue;
-  size_t nc = 0;
-  for(ev_iterator i = ev_begin(); i != ev_end(); ++i)
-    ev->d_children[nc++] = Expr(*i);
   ev->d_nchildren = d_nchildren;
   ev->d_kind = d_kind;
-  ev->d_id = ExprValue::next_id++;
+  ev->d_id = ExprValue::next_id++;// FIXME multithreading
   ev->d_rc = 0;
   Expr e(ev);
 
diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp
index 3aeab8049..9b7697e4f 100644
--- a/src/expr/expr_manager.cpp
+++ b/src/expr/expr_manager.cpp
@@ -18,6 +18,42 @@ namespace CVC4 {
 
 __thread ExprManager* ExprManager::s_current = 0;
 
+Expr ExprManager::lookup(uint64_t hash, const Expr& e) {
+  hash_t::iterator i = d_hash.find(hash);
+  if(i == d_hash.end()) {
+    // insert
+    std::vector<Expr> v;
+    v.push_back(e);
+    d_hash.insert(std::make_pair(hash, v));
+    return e;
+  } else {
+    for(std::vector<Expr>::iterator j = i->second.begin(); j != i->second.end(); ++j) {
+      if(e.getKind() != j->getKind())
+        continue;
+
+      if(e.numChildren() != j->numChildren())
+        continue;
+
+      Expr::iterator c1 = e.begin();
+      Expr::iterator c2 = j->begin();
+      for(; c1 != e.end() && c2 != j->end(); ++c1, ++c2) {
+        if(c1->d_ev != c2->d_ev)
+          break;
+      }
+
+      if(c1 != e.end() || c2 != j->end())
+        continue;
+
+      return *j;
+    }
+    // didn't find it, insert
+    std::vector<Expr> v;
+    v.push_back(e);
+    d_hash.insert(std::make_pair(hash, v));
+    return e;
+  }
+}
+
 // general expression-builders
 
 Expr ExprManager::mkExpr(Kind kind) {
@@ -49,4 +85,8 @@ Expr ExprManager::mkExpr(Kind kind, std::vector<Expr> children) {
   return ExprBuilder(this, kind).append(children);
 }
 
+Expr ExprManager::mkVar() {
+  return ExprBuilder(this, VARIABLE);
+}
+
 }/* CVC4 namespace */
diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h
index ee18ddc01..d311445f3 100644
--- a/src/expr/expr_manager.h
+++ b/src/expr/expr_manager.h
@@ -32,41 +32,7 @@ class CVC4_PUBLIC ExprManager {
   typedef std::map<uint64_t, std::vector<Expr> > hash_t;
   hash_t d_hash;
 
-  Expr lookup(uint64_t hash, const Expr& e) {
-    hash_t::iterator i = d_hash.find(hash);
-    if(i == d_hash.end()) {
-      // insert
-      std::vector<Expr> v;
-      v.push_back(e);
-      d_hash.insert(std::make_pair(hash, v));
-      return e;
-    } else {
-      for(std::vector<Expr>::iterator j = i->second.begin(); j != i->second.end(); ++j) {
-        if(e.getKind() != j->getKind())
-          continue;
-
-        if(e.numChildren() != j->numChildren())
-          continue;
-
-        Expr::iterator c1 = e.begin();
-        Expr::iterator c2 = j->begin();
-        while(c1 != e.end() && c2 != j->end()) {
-          if(c1->d_ev != c2->d_ev)
-            break;
-        }
-
-        if(c1 != e.end() || c2 != j->end())
-          continue;
-
-        return *j;
-      }
-      // didn't find it, insert
-      std::vector<Expr> v;
-      v.push_back(e);
-      d_hash.insert(std::make_pair(hash, v));
-      return e;
-    }
-  }
+  Expr lookup(uint64_t hash, const Expr& e);
 
 public:
   static ExprManager* currentEM() { return s_current; }
@@ -81,6 +47,9 @@ public:
   // N-ary version
   Expr mkExpr(Kind kind, std::vector<Expr> children);
 
+  // variables are special, because duplicates are permitted
+  Expr mkVar();
+
   // TODO: these use the current EM (but must be renamed)
   /*
   static Expr mkExpr(Kind kind)
diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp
index c511c580a..250803281 100644
--- a/src/expr/expr_value.cpp
+++ b/src/expr/expr_value.cpp
@@ -18,12 +18,12 @@
 
 namespace CVC4 {
 
+size_t ExprValue::next_id = 1;
+
 ExprValue::ExprValue() :
   d_id(0), d_rc(MAX_RC), d_kind(NULL_EXPR), d_nchildren(0) {
 }
 
-size_t ExprValue::next_id = 1;
-
 uint64_t ExprValue::hash() const {
   uint64_t hash = d_kind;
 
@@ -82,4 +82,18 @@ ExprValue::const_iterator ExprValue::rend() const {
   return d_children - 1;
 }
 
+void ExprValue::toString(std::ostream& out) const {
+  out << "(" << Kind(d_kind);
+  if(d_kind == VARIABLE) {
+    out << ":" << this;
+  } else {
+    for(const_iterator i = begin(); i != end(); ++i) {
+      if(i != end())
+        out << " ";
+      out << *i;
+    }
+  }
+  out << ")";
+}
+
 }/* CVC4 namespace */
diff --git a/src/expr/expr_value.h b/src/expr/expr_value.h
index 6df7ad76f..18ad84073 100644
--- a/src/expr/expr_value.h
+++ b/src/expr/expr_value.h
@@ -21,7 +21,9 @@
 #ifndef __CVC4__EXPR__EXPR_VALUE_H
 #define __CVC4__EXPR__EXPR_VALUE_H
 
+#include "cvc4_config.h"
 #include <stdint.h>
+#include "kind.h"
 
 namespace CVC4 {
 
@@ -92,9 +94,7 @@ public:
   const_iterator rbegin() const;
   const_iterator rend() const;
 
-  void toString(std::ostream& out) {
-    out << Kind(d_kind);
-  }
+  void CVC4_PUBLIC toString(std::ostream& out) const;
 };
 
 }/* CVC4::expr namespace */
diff --git a/src/expr/kind.h b/src/expr/kind.h
index 49321b47f..5ac02ca7c 100644
--- a/src/expr/kind.h
+++ b/src/expr/kind.h
@@ -51,15 +51,16 @@ enum Kind {
 
 };/* enum Kind */
 
-}/* CVC4 namespace */
-
-inline std::ostream& operator<<(std::ostream&, const CVC4::Kind&) CVC4_PUBLIC;
-inline std::ostream& operator<<(std::ostream& out, const CVC4::Kind& k) {
+inline std::ostream& operator<<(std::ostream&, CVC4::Kind) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& out, CVC4::Kind k) {
   using namespace CVC4;
 
   switch(k) {
+
+  /* special cases */
   case UNDEFINED_KIND: out << "UNDEFINED_KIND"; break;
   case NULL_EXPR:      out << "NULL";           break;
+
   case EQUAL:          out << "EQUAL";          break;
   case ITE:            out << "ITE";            break;
   case SKOLEM:         out << "SKOLEM";         break;
@@ -88,4 +89,6 @@ inline std::ostream& operator<<(std::ostream& out, const CVC4::Kind& k) {
   return out;
 }
 
+}/* CVC4 namespace */
+
 #endif /* __CVC4__KIND_H */
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index 2daead11b..7f515c58b 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -25,6 +25,7 @@
 #include "util/exception.h"
 #include "usage.h"
 #include "about.h"
+#include "util/output.h"
 
 using namespace std;
 using namespace CVC4;
@@ -66,7 +67,7 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti
     progName = x + 1;
   opts->binary_name = string(progName);
 
-  while((c = getopt_long(argc, argv, "+:hVvqL:", cmdlineOptions, NULL)) != -1) {
+  while((c = getopt_long(argc, argv, "+:hVvqL:d:", cmdlineOptions, NULL)) != -1) {
     switch(c) {
 
     case 'h':
@@ -104,6 +105,9 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti
       fputs(lang_help, stdout);
       exit(1);
 
+    case 'd':
+      Debug.on(optarg);
+
     case STATS:
       opts->statistics = true;
       break;
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 4c3a21811..d4ee8fd0d 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -13,6 +13,7 @@
 #include <iostream>
 #include <fstream>
 #include <cstdlib>
+#include <cstring>
 #include <new>
 
 #include "config.h"
@@ -22,6 +23,7 @@
 #include "expr/expr_manager.h"
 #include "smt/smt_engine.h"
 #include "util/command.h"
+#include "util/output.h"
 
 using namespace std;
 using namespace CVC4;
@@ -44,18 +46,42 @@ int main(int argc, char *argv[]) {
     if(options.smtcomp_mode)
       cout << unitbuf;
 
-        // We only accept one input file
+    // We only accept one input file
     if(argc > firstArgIndex + 1)
       throw new Exception("Too many input files specified.");
 
     // Create the expression manager
     ExprManager exprMgr;
+
     // Create the SmtEngine
     SmtEngine smt(&exprMgr, &options);
 
     // If no file supplied we read from standard input
     bool inputFromStdin = firstArgIndex >= argc;
 
+    if(!inputFromStdin && options.lang == Options::LANG_AUTO) {
+      if(!strcmp(".smt", argv[firstArgIndex] + strlen(argv[firstArgIndex]) - 4))
+        options.lang = Options::LANG_SMTLIB;
+      else if(!strcmp(".cvc", argv[firstArgIndex] + strlen(argv[firstArgIndex]) - 4) ||
+              !strcmp(".cvc4", argv[firstArgIndex] + strlen(argv[firstArgIndex]) - 5))
+        options.lang = Options::LANG_CVC4;
+    }
+
+    if(options.smtcomp_mode) {
+      Debug.setStream(CVC4::null_os);
+      Trace.setStream(CVC4::null_os);
+      Notice.setStream(CVC4::null_os);
+      Chat.setStream(CVC4::null_os);
+      Warning.setStream(CVC4::null_os);
+    } else {
+      if(options.verbosity < 2)
+        Chat.setStream(CVC4::null_os);
+      if(options.verbosity < 1)
+        Notice.setStream(CVC4::null_os);
+      if(options.verbosity < 0)
+        Warning.setStream(CVC4::null_os);
+    }
+
     // Create the parser
     Parser* parser;
     switch(options.lang) {
@@ -79,7 +105,7 @@ int main(int argc, char *argv[]) {
       abort();
     }
 
-    // Parse the and execute commands until we are done
+    // Parse and execute commands until we are done
     while(!parser->done()) {
       // Parse the next command
       Command *cmd = parser->parseNextCommand();
diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index 52f3c4668..04a82f721 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -9,12 +9,16 @@
 
 #include "antlr_parser.h"
 #include "expr/expr_manager.h"
+#include "util/output.h"
 
 using namespace std;
 using namespace CVC4;
 using namespace CVC4::parser;
 
-ostream& operator <<(ostream& out, AntlrParser::BenchmarkStatus status) {
+namespace CVC4 {
+namespace parser {
+
+ostream& operator<<(ostream& out, AntlrParser::BenchmarkStatus status) {
   switch(status) {
   case AntlrParser::SMT_SATISFIABLE:
     out << "sat";
@@ -63,7 +67,9 @@ AntlrParser::AntlrParser(antlr::TokenStream& lexer, int k) :
 }
 
 Expr AntlrParser::getVariable(std::string var_name) {
-  return d_var_symbol_table.getObject(var_name);
+  Expr e = d_var_symbol_table.getObject(var_name);
+  Debug("parser") << "getvar " << var_name << " gives " << e << endl;
+  return e;
 }
 
 Expr AntlrParser::getTrueExpr() const {
@@ -89,7 +95,7 @@ Expr AntlrParser::newExpression(Kind kind, const std::vector<Expr>& children) {
 void AntlrParser::newPredicate(std::string p_name, const std::vector<
     std::string>& p_sorts) {
   if(p_sorts.size() == 0)
-    d_var_symbol_table.bindName(p_name, d_expr_manager->mkExpr(VARIABLE));
+    d_var_symbol_table.bindName(p_name, d_expr_manager->mkVar());
   else
     Unhandled("Non unary predicate not supported yet!");
 }
@@ -161,3 +167,6 @@ Expr AntlrParser::createPrecedenceExpr(const std::vector<Expr>& exprs,
   Expr child_2 = createPrecedenceExpr(exprs, kinds, pivot + 1, end_index);
   return d_expr_manager->mkExpr(kinds[pivot], child_1, child_2);
 }
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h
index 0db12a0f0..ad23d45f8 100644
--- a/src/parser/antlr_parser.h
+++ b/src/parser/antlr_parser.h
@@ -18,7 +18,7 @@
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
 #include "util/command.h"
-#include "util/assert.h"
+#include "util/Assert.h"
 #include "parser/symbol_table.h"
 
 namespace CVC4 {
diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am
index 4c1a5d92b..b132ede5c 100644
--- a/src/parser/cvc/Makefile.am
+++ b/src/parser/cvc/Makefile.am
@@ -18,7 +18,9 @@ libparsercvc_la_SOURCES = \
 BUILT_SOURCES = $(ANTLR_STUFF)
 CLEAN_FILES = $(ANTLR_STUFF)
 
-AntlrCvcLexer.cpp AntlrCvcLexer.hpp: CvcLexer.g
+AntlrCvcLexer.cpp: CvcLexer.g
 	$(ANTLR) -o "@builddir@" "$<"
-AntlrCvcParser.cpp AntlrCvcParser.hpp: CvcParser.g
+AntlrCvcParser.cpp: CvcParser.g CvcVocabularyTokenTypes.hpp CvcVocabularyTokenTypes.txt
 	$(ANTLR) -o "@builddir@" "$<"
+AntlrCvcLexer.hpp CvcVocabularyTokenTypes.hpp CvcVocabularyTokenTypes.txt: AntlrCvcLexer.cpp
+AntlrCvcParser.hpp: AntlrCvcParser.cpp
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 65a5d11c1..4c7e28dc0 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -15,7 +15,7 @@
 
 #include "parser.h"
 #include "util/command.h"
-#include "util/assert.h"
+#include "util/Assert.h"
 #include "parser_exception.h"
 #include "parser/antlr_parser.h"
 #include "parser/smt/AntlrSmtParser.hpp"
diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am
index 6017409fd..9769fabcb 100644
--- a/src/parser/smt/Makefile.am
+++ b/src/parser/smt/Makefile.am
@@ -18,7 +18,9 @@ libparsersmt_la_SOURCES = \
 BUILT_SOURCES = $(ANTLR_STUFF)
 CLEAN_FILES = $(ANTLR_STUFF)
 
-AntlrSmtLexer.cpp AntlrSmtLexer.hpp: SmtLexer.g
+AntlrSmtLexer.cpp: SmtLexer.g
 	$(ANTLR) -o "@builddir@" "$<"
-AntlrSmtParser.cpp AntlrSmtParser.hpp: SmtParser.g
+AntlrSmtParser.cpp: SmtParser.g SmtVocabularyTokenTypes.hpp SmtVocabularyTokenTypes.txt
 	$(ANTLR) -o "@builddir@" "$<"
+AntlrSmtLexer.hpp SmtVocabularyTokenTypes.hpp SmtVocabularyTokenTypes.txt: AntlrSmtLexer.cpp
+AntlrSmtParser.hpp: AntlrSmtParser.cpp
diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h
index 3b08aa5f5..32532c734 100644
--- a/src/parser/symbol_table.h
+++ b/src/parser/symbol_table.h
@@ -9,6 +9,9 @@
  **
  **/
 
+#ifndef __CVC4__PARSER__SYMBOL_TABLE_H
+#define __CVC4__PARSER__SYMBOL_TABLE_H
+
 #include <string>
 #include <stack>
 #include <ext/hash_map>
@@ -31,63 +34,65 @@ namespace parser {
  * Generic symbol table for looking up variables by name.
  */
 template<typename ObjectType>
-  class SymbolTable {
+class SymbolTable {
 
-  private:
+private:
 
-    /** The name to expression bindings */
-    typedef __gnu_cxx ::hash_map<std::string, std::stack<ObjectType> >
-        LookupTable;
-    /** The table iterator */
-    typedef typename LookupTable::iterator table_iterator;
-    /** The table iterator */
-    typedef typename LookupTable::const_iterator const_table_iterator;
+  /** The name to expression bindings */
+  typedef __gnu_cxx ::hash_map<std::string, std::stack<ObjectType> >
+  LookupTable;
+  /** The table iterator */
+  typedef typename LookupTable::iterator table_iterator;
+  /** The table iterator */
+  typedef typename LookupTable::const_iterator const_table_iterator;
 
-    /** Bindings for the names */
-    LookupTable d_name_bindings;
+  /** Bindings for the names */
+  LookupTable d_name_bindings;
 
-  public:
+public:
 
-    /**
-     * Bind the name of the variable to the given expression. If the variable
-     * has been bind before, this will redefine it until its undefined.
-     */
-    void bindName(const std::string name, const ObjectType& obj) throw () {
-      d_name_bindings[name].push(obj);
-    }
+  /**
+   * Bind the name of the variable to the given expression. If the variable
+   * has been bind before, this will redefine it until its undefined.
+   */
+  void bindName(const std::string name, const ObjectType& obj) throw () {
+    d_name_bindings[name].push(obj);
+  }
 
-    /**
-     * Unbinds the last binding of the name to the expression.
-     */
-    void unbindName(const std::string name) throw () {
-      table_iterator find = d_name_bindings.find(name);
-      if(find != d_name_bindings.end()) {
-        find->second.pop();
-        if(find->second.empty()) {
-          d_name_bindings.erase(find);
-        }
+  /**
+   * Unbinds the last binding of the name to the expression.
+   */
+  void unbindName(const std::string name) throw () {
+    table_iterator find = d_name_bindings.find(name);
+    if(find != d_name_bindings.end()) {
+      find->second.pop();
+      if(find->second.empty()) {
+        d_name_bindings.erase(find);
       }
     }
+  }
 
-    /**
-     * Returns the last binding expression of the name.
-     */
-    ObjectType getObject(const std::string name) throw () {
-      ObjectType result;
-      table_iterator find = d_name_bindings.find(name);
-      if(find != d_name_bindings.end())
-        result = find->second.top();
-      return result;
-    }
+  /**
+   * Returns the last binding expression of the name.
+   */
+  ObjectType getObject(const std::string name) throw () {
+    ObjectType result;
+    table_iterator find = d_name_bindings.find(name);
+    if(find != d_name_bindings.end())
+      result = find->second.top();
+    return result;
+  }
 
-    /**
-     * Returns true is name is bound to an expression.
-     */
-    bool isBound(const std::string name) const throw () {
-      const_table_iterator find = d_name_bindings.find(name);
-      return (find != d_name_bindings.end());
-    }
-  };
+  /**
+   * Returns true is name is bound to an expression.
+   */
+  bool isBound(const std::string name) const throw () {
+    const_table_iterator find = d_name_bindings.find(name);
+    return (find != d_name_bindings.end());
+  }
+};
 
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
+
+#endif /* __CVC4__PARSER__SYMBOL_TABLE_H */
diff --git a/src/prop/minisat/core/Solver.C b/src/prop/minisat/core/Solver.C
index d7a7bf8e1..4ea33e101 100644
--- a/src/prop/minisat/core/Solver.C
+++ b/src/prop/minisat/core/Solver.C
@@ -25,7 +25,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 // Constructor/Destructor:
 
 namespace CVC4 {
-namespace MiniSat {
+namespace prop {
+namespace minisat {
 
 Solver::Solver() :
 
@@ -741,6 +742,7 @@ void Solver::checkLiteralCount()
     }
 }
 
-}/* CVC4::MiniSat namespace */
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index e53cefc24..2383fd68c 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -17,14 +17,16 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#ifndef CVC4_MiniSat_Solver_h
-#define CVC4_MiniSat_Solver_h
+#ifndef __CVC4__PROP__MINISAT__SOLVER_H
+#define __CVC4__PROP__MINISAT__SOLVER_H
 
 #include <cstdio>
+#include <cassert>
 
-#include "Vec.h"
-#include "Heap.h"
-#include "Alg.h"
+#include "cvc4_config.h"
+#include "../mtl/Vec.h"
+#include "../mtl/Heap.h"
+#include "../mtl/Alg.h"
 
 #include "SolverTypes.h"
 
@@ -33,7 +35,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 // Solver -- the main class:
 
 namespace CVC4 {
-namespace MiniSat {
+namespace prop {
+namespace minisat {
 
 class Solver {
 public:
@@ -41,7 +44,7 @@ public:
     // Constructor/Destructor:
     //
     Solver();
-    ~Solver();
+    CVC4_PUBLIC ~Solver();
 
     // Problem specification:
     //
@@ -56,7 +59,7 @@ public:
     bool    okay         () const;                  // FALSE means solver is in a conflicting state
 
     // Variable mode:
-    // 
+    //
     void    setPolarity    (Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.
     void    setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic.
 
@@ -258,6 +261,7 @@ inline bool     Solver::okay          ()      const   { return ok; }
 
 
 #define reportf(format, args...) ( fflush(stdout), fprintf(stderr, format, ## args), fflush(stderr) )
+//#define reportf(format, args...) do {} while(0)
 
 static inline void logLit(FILE* f, Lit l)
 {
@@ -299,8 +303,9 @@ inline void Solver::printClause(const C& c)
     }
 }
 
-}/* CVC4::MiniSat namespace */
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
 //=================================================================================================
-#endif /* CVC4_MiniSat_Solver_h */
+#endif /* __CVC4__PROP__MINISAT__SOLVER_H */
diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h
index 55e6d75fd..8860693e6 100644
--- a/src/prop/minisat/core/SolverTypes.h
+++ b/src/prop/minisat/core/SolverTypes.h
@@ -17,14 +17,15 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#ifndef CVC4_MiniSat_SolverTypes_h
-#define CVC4_MiniSat_SolverTypes_h
+#ifndef __CVC4__PROP__MINISAT__SOLVERTYPES_H
+#define __CVC4__PROP__MINISAT__SOLVERTYPES_H
 
 #include <cassert>
 #include <stdint.h>
 
 namespace CVC4 {
-namespace MiniSat {
+namespace prop {
+namespace minisat {
 
 //=================================================================================================
 // Variables, literals, lifted booleans, clauses:
@@ -196,7 +197,8 @@ inline void Clause::strengthen(Lit p)
     calcAbstraction();
 }
 
-}/* CVC4::MiniSat namespace */
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
-#endif /* CVC4_MiniSat_SolverTypes_h */
+#endif /* __CVC4__PROP__MINISAT__SOLVERTYPES_H */
diff --git a/src/prop/minisat/mtl/Alg.h b/src/prop/minisat/mtl/Alg.h
index a4ca4403b..0fe6d84c7 100644
--- a/src/prop/minisat/mtl/Alg.h
+++ b/src/prop/minisat/mtl/Alg.h
@@ -20,8 +20,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef CVC4_MiniSat_Alg_h
 #define CVC4_MiniSat_Alg_h
 
+#include <cassert>
+
 namespace CVC4 {
-namespace MiniSat {
+namespace prop {
+namespace minisat {
 
 //=================================================================================================
 // Useful functions on vectors
@@ -57,7 +60,8 @@ static inline bool find(V& ts, const T& t)
     return j < ts.size();
 }
 
-}/* CVC4::MiniSat namespace */
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
 #endif /* CVC4_MiniSat_Alg_h */
diff --git a/src/prop/minisat/mtl/BasicHeap.h b/src/prop/minisat/mtl/BasicHeap.h
index b22a35ada..39d825411 100644
--- a/src/prop/minisat/mtl/BasicHeap.h
+++ b/src/prop/minisat/mtl/BasicHeap.h
@@ -23,7 +23,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "Vec.h"
 
 namespace CVC4 {
-namespace MiniSat {
+namespace prop {
+namespace minisat {
 
 //=================================================================================================
 // A heap implementation with support for decrease/increase key.
@@ -99,7 +100,8 @@ class BasicHeap {
 
 //=================================================================================================
 
-}/* CVC4::MiniSat namespace */
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
 #endif /* CVC4_MiniSat_BasicHeap_h */
diff --git a/src/prop/minisat/mtl/BoxedVec.h b/src/prop/minisat/mtl/BoxedVec.h
index 7c5b10e4c..05b801004 100644
--- a/src/prop/minisat/mtl/BoxedVec.h
+++ b/src/prop/minisat/mtl/BoxedVec.h
@@ -25,7 +25,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <new>
 
 namespace CVC4 {
-namespace MiniSat {
+namespace prop {
+namespace minisat {
 
 //=================================================================================================
 // Automatically resizable arrays
@@ -53,7 +54,7 @@ class bvec {
             x->cap = size;
             return x;
         }
-        
+
     };
 
     Vec_t* ref;
@@ -79,16 +80,16 @@ class bvec {
     altvec (altvec<T>& other)                  { assert(0); }
 
 public:
-    void     clear  (bool dealloc = false) { 
+    void     clear  (bool dealloc = false) {
         if (ref != NULL){
-            for (int i = 0; i < ref->sz; i++) 
+            for (int i = 0; i < ref->sz; i++)
                 (*ref).data[i].~T();
 
-            if (dealloc) { 
-                free(ref); ref = NULL; 
-            }else 
+            if (dealloc) {
+                free(ref); ref = NULL;
+            }else
                 ref->sz = 0;
-        } 
+        }
     }
 
     // Constructors:
@@ -110,11 +111,11 @@ public:
         int cap  = ref != NULL ? ref->cap : 0;
         if (size == cap){
             cap = cap != 0 ? nextSize(cap) : init_size;
-            ref = Vec_t::alloc(ref, cap); 
+            ref = Vec_t::alloc(ref, cap);
         }
-        //new (&ref->data[size]) T(elem); 
-        ref->data[size] = elem; 
-        ref->sz = size+1; 
+        //new (&ref->data[size]) T(elem);
+        ref->data[size] = elem;
+        ref->sz = size+1;
     }
 
     void     push   () {
@@ -122,10 +123,10 @@ public:
         int cap  = ref != NULL ? ref->cap : 0;
         if (size == cap){
             cap = cap != 0 ? nextSize(cap) : init_size;
-            ref = Vec_t::alloc(ref, cap); 
+            ref = Vec_t::alloc(ref, cap);
         }
-        new (&ref->data[size]) T(); 
-        ref->sz = size+1; 
+        new (&ref->data[size]) T();
+        ref->sz = size+1;
     }
 
     void     shrink (int nelems)             { for (int i = 0; i < nelems; i++) pop(); }
@@ -146,7 +147,8 @@ public:
 
 };
 
-}/* CVC4::MiniSat namespace */
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
 #endif /* CVC4_MiniSat_BoxedVec_h */
diff --git a/src/prop/minisat/mtl/Heap.h b/src/prop/minisat/mtl/Heap.h
index 84234705c..0c2019b65 100644
--- a/src/prop/minisat/mtl/Heap.h
+++ b/src/prop/minisat/mtl/Heap.h
@@ -21,9 +21,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #define CVC4_MiniSat_Heap_h
 
 #include "Vec.h"
+#include <cassert>
 
 namespace CVC4 {
-namespace MiniSat {
+namespace prop {
+namespace minisat {
 
 //=================================================================================================
 // A heap implementation with support for decrease/increase key.
@@ -95,7 +97,7 @@ class Heap {
 
         indices[n] = heap.size();
         heap.push(n);
-        percolateUp(indices[n]); 
+        percolateUp(indices[n]);
     }
 
 
@@ -107,19 +109,19 @@ class Heap {
         indices[x]       = -1;
         heap.pop();
         if (heap.size() > 1) percolateDown(0);
-        return x; 
+        return x;
     }
 
 
-    void clear(bool dealloc = false) 
-    { 
+    void clear(bool dealloc = false)
+    {
         for (int i = 0; i < heap.size(); i++)
             indices[heap[i]] = -1;
 #ifdef NDEBUG
         for (int i = 0; i < indices.size(); i++)
             assert(indices[i] == -1);
 #endif
-        heap.clear(dealloc); 
+        heap.clear(dealloc);
     }
 
 
@@ -167,7 +169,8 @@ class Heap {
 
 };
 
-}/* CVC4::MiniSat namespace */
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
 //=================================================================================================
diff --git a/src/prop/minisat/mtl/Map.h b/src/prop/minisat/mtl/Map.h
index f69fca6d5..9168dde0e 100644
--- a/src/prop/minisat/mtl/Map.h
+++ b/src/prop/minisat/mtl/Map.h
@@ -25,7 +25,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "Vec.h"
 
 namespace CVC4 {
-namespace MiniSat {
+namespace prop {
+namespace minisat {
 
 //=================================================================================================
 // Default hash/equals functions
@@ -83,7 +84,7 @@ class Map {
         cap = newsize;
     }
 
-    
+
     public:
 
      Map () : table(NULL), cap(0), size(0) {}
@@ -97,7 +98,7 @@ class Map {
         for (int i = 0; i < ps.size(); i++)
             if (equals(ps[i].key, k)){
                 d = ps[i].data;
-                return true; } 
+                return true; }
         return false;
     }
 
@@ -118,7 +119,8 @@ class Map {
     }
 };
 
-}/* CVC4::MiniSat namespace */
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
 #endif /* CVC4_MiniSat_Map_h */
diff --git a/src/prop/minisat/mtl/Queue.h b/src/prop/minisat/mtl/Queue.h
index e4e7e2159..e02ac7222 100644
--- a/src/prop/minisat/mtl/Queue.h
+++ b/src/prop/minisat/mtl/Queue.h
@@ -23,7 +23,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "Vec.h"
 
 namespace CVC4 {
-namespace MiniSat {
+namespace prop {
+namespace minisat {
 
 //=================================================================================================
 
@@ -83,7 +84,8 @@ public:
 
 //=================================================================================================
 
-}/* CVC4::MiniSat namespace */
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
 #endif /* CVC4_MiniSat_Queue_h */
diff --git a/src/prop/minisat/mtl/Sort.h b/src/prop/minisat/mtl/Sort.h
index df5261a06..2b9d5bb15 100644
--- a/src/prop/minisat/mtl/Sort.h
+++ b/src/prop/minisat/mtl/Sort.h
@@ -23,7 +23,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "Vec.h"
 
 namespace CVC4 {
-namespace MiniSat {
+namespace prop {
+namespace minisat {
 
 //=================================================================================================
 // Some sorting algorithms for vec's
@@ -94,7 +95,8 @@ template <class T> void sort(vec<T>& v) {
 
 //=================================================================================================
 
-}/* CVC4::MiniSat namespace */
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
 #endif /* CVC4_MiniSat_Sort_h */
diff --git a/src/prop/minisat/mtl/Vec.h b/src/prop/minisat/mtl/Vec.h
index 1a07cc334..fae1d0c5d 100644
--- a/src/prop/minisat/mtl/Vec.h
+++ b/src/prop/minisat/mtl/Vec.h
@@ -25,7 +25,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <new>
 
 namespace CVC4 {
-namespace MiniSat {
+namespace prop {
+namespace minisat {
 
 //=================================================================================================
 // Automatically resizable arrays
@@ -132,7 +133,8 @@ void vec<T>::clear(bool dealloc) {
         sz = 0;
         if (dealloc) free(data), data = NULL, cap = 0; } }
 
-}/* CVC4::MiniSat namespace */
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
 #endif /* CVC4_MiniSat_Vec_h */
diff --git a/src/prop/minisat/simp/SimpSolver.C b/src/prop/minisat/simp/SimpSolver.C
index 14b64b555..063332e74 100644
--- a/src/prop/minisat/simp/SimpSolver.C
+++ b/src/prop/minisat/simp/SimpSolver.C
@@ -25,7 +25,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 // Constructor/Destructor:
 
 namespace CVC4 {
-namespace MiniSat {
+namespace prop {
+namespace minisat {
 
 SimpSolver::SimpSolver() :
     grow               (0)
@@ -226,11 +227,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& ou
     for (int i = 0; i < qs.size(); i++){
         if (var(qs[i]) != v){
             for (int j = 0; j < ps.size(); j++)
-                if (var(ps[j]) == var(qs[i]))
+                if (var(ps[j]) == var(qs[i])) {
                     if (ps[j] == ~qs[i])
                         return false;
                     else
                         goto next;
+                }
             out_clause.push(qs[i]);
         }
         next:;
@@ -258,11 +260,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v)
     for (int i = 0; i < qs.size(); i++){
         if (var(__qs[i]) != v){
             for (int j = 0; j < ps.size(); j++)
-                if (var(__ps[j]) == var(__qs[i]))
+                if (var(__ps[j]) == var(__qs[i])) {
                     if (__ps[j] == ~__qs[i])
                         return false;
                     else
                         goto next;
+                }
         }
         next:;
     }
@@ -701,5 +704,6 @@ void SimpSolver::toDimacs(const char* file)
         fprintf(stderr, "could not open file %s\n", file);
 }
 
-}/* CVC4::MiniSat namespace */
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
 }/* CVC4 namespace */
diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index 221b4c6e2..f9e9b0387 100644
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -17,23 +17,25 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#ifndef CVC4_MiniSat_SimpSolver_h
-#define CVC4_MiniSat_SimpSolver_h
+#ifndef __CVC4__PROP__MINISAT__SIMP_SOLVER_H
+#define __CVC4__PROP__MINISAT__SIMP_SOLVER_H
 
 #include <cstdio>
+#include <cassert>
 
-#include "Queue.h"
-#include "Solver.h"
+#include "../mtl/Queue.h"
+#include "../core/Solver.h"
 
 namespace CVC4 {
-namespace MiniSat {
+namespace prop {
+namespace minisat {
 
 class SimpSolver : public Solver {
  public:
     // Constructor/Destructor:
     //
     SimpSolver();
-    ~SimpSolver();
+    CVC4_PUBLIC ~SimpSolver();
 
     // Problem specification:
     //
@@ -159,8 +161,9 @@ inline bool  SimpSolver::isEliminated (Var v) const { return v < elimtable.size(
 inline void  SimpSolver::setFrozen    (Var v, bool b) { frozen[v] = (char)b; if (b) { updateElimHeap(v); } }
 inline bool  SimpSolver::solve        (bool do_simp, bool turn_off_simp) { vec<Lit> tmp; return solve(tmp, do_simp, turn_off_simp); }
 
-}/* CVC4::MiniSat namespace */
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
 //=================================================================================================
-#endif /* CVC4_MiniSat_SimpSolver_h */
+#endif /* __CVC4__PROP__MINISAT__SIMP_SOLVER_H */
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index e69de29bb..2fb73cbed 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -0,0 +1,123 @@
+/*********************                                           -*- C++ -*-  */
+/** prop_engine.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.
+ **
+ **/
+
+#include "prop/prop_engine.h"
+#include "theory/theory_engine.h"
+#include "util/decision_engine.h"
+#include "prop/minisat/mtl/Vec.h"
+#include "prop/minisat/simp/SimpSolver.h"
+#include "prop/minisat/core/SolverTypes.h"
+#include "util/Assert.h"
+#include "util/output.h"
+
+#include <utility>
+#include <map>
+
+using namespace CVC4::prop::minisat;
+using namespace std;
+
+namespace CVC4 {
+
+PropEngine::PropEngine(DecisionEngine& de, TheoryEngine& te) :
+  d_de(de), d_te(te), d_sat() {
+}
+
+void PropEngine::addVars(Expr e) {
+  Debug("prop") << "adding vars to " << e << endl;
+  for(Expr::iterator i = e.begin(); i != e.end(); ++i) {
+    Debug("prop") << "expr " << *i << endl;
+    if(i->getKind() == VARIABLE) {
+      if(d_vars.find(*i) == d_vars.end()) {
+        Var v = d_sat.newVar();
+        Debug("prop") << "adding var " << *i << " <--> " << v << endl;
+        d_vars.insert(make_pair(*i, v));
+        d_varsReverse.insert(make_pair(v, *i));
+      } else Debug("prop") << "using var " << *i << " <--> " << d_vars[*i] << endl;
+    } else addVars(*i);
+  }
+}
+
+static void doAtom(SimpSolver* minisat, map<Expr, Var>* vars, Expr e, vec<Lit>* c) {
+  if(e.getKind() == VARIABLE) {
+    map<Expr, Var>::iterator v = vars->find(e);
+    Assert(v != vars->end());
+    c->push(Lit(v->second, false));
+    return;
+  }
+  if(e.getKind() == NOT) {
+    Assert(e.numChildren() == 1);
+    Expr child = *e.begin();
+    Assert(child.getKind() == VARIABLE);
+    map<Expr, Var>::iterator v = vars->find(child);
+    Assert(v != vars->end());
+    c->push(Lit(v->second, true));
+    return;
+  }
+  Unhandled();
+}
+
+static void doClause(SimpSolver* minisat, map<Expr, Var>* vars, map<Var, Expr>* varsReverse, Expr e) {
+  vec<Lit> c;
+  Debug("prop") << "  " << e << endl;
+  if(e.getKind() == VARIABLE || e.getKind() == NOT) {
+    doAtom(minisat, vars, e, &c);
+  } else {
+    Assert(e.getKind() == OR);
+    for(Expr::iterator i = e.begin(); i != e.end(); ++i) {
+      Debug("prop") << "    " << *i << endl;
+      doAtom(minisat, vars, *i, &c);
+    }
+  }
+  Notice() << "added clause of length " << c.size() << endl;
+  for(int i = 0; i < c.size(); ++i)
+    Notice() << " " << (sign(c[i]) ? "-" : "") << var(c[i]);
+  Notice() << " [[";
+  for(int i = 0; i < c.size(); ++i)
+    Notice() << " " << (sign(c[i]) ? "-" : "") << (*varsReverse)[var(c[i])];
+  Notice() << " ]] " << endl;
+  minisat->addClause(c);
+}
+
+void PropEngine::solve(Expr e) {
+  Debug("prop") << "SOLVING " << e << endl;
+  addVars(e);
+  if(e.getKind() == AND) {
+    Debug("prop") << "AND" << endl;
+    for(Expr::iterator i = e.begin(); i != e.end(); ++i)
+      doClause(&d_sat, &d_vars, &d_varsReverse, *i);
+  } else doClause(&d_sat, &d_vars, &d_varsReverse, e);
+
+  d_sat.verbosity = 1;
+  bool result = d_sat.solve();
+
+  Notice() << "result is " << (result ? "sat" : "unsat") << endl;
+  if(result) {
+    Notice() << "model:" << endl;
+    for(int i = 0; i < d_sat.model.size(); ++i)
+      Notice() << " " << toInt(d_sat.model[i]);
+    Notice() << endl;
+    for(int i = 0; i < d_sat.model.size(); ++i)
+      Notice() << " " << d_varsReverse[i] << " is "
+               << (d_sat.model[i] == l_False ? "FALSE" :
+                   (d_sat.model[i] == l_Undef ? "UNDEF" :
+                    "TRUE")) << endl;
+  } else {
+    Notice() << "conflict:" << endl;
+    for(int i = 0; i < d_sat.conflict.size(); ++i)
+      Notice() << " " << (sign(d_sat.conflict[i]) ? "-" : "") << var(d_sat.conflict[i]);
+    Notice() << " [[";
+    for(int i = 0; i < d_sat.conflict.size(); ++i)
+      Notice() << " " << (sign(d_sat.conflict[i]) ? "-" : "") << d_varsReverse[var(d_sat.conflict[i])];
+    Notice() << " ]] " << endl;
+  }
+}
+
+}/* CVC4 namespace */
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 5969e82d1..a3355bf89 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -9,28 +9,38 @@
  **
  **/
 
-#ifndef __CVC4__PROP__PROP_ENGINE_H
-#define __CVC4__PROP__PROP_ENGINE_H
+#ifndef __CVC4__PROP_ENGINE_H
+#define __CVC4__PROP_ENGINE_H
 
+#include "cvc4_config.h"
 #include "expr/expr.h"
 #include "util/decision_engine.h"
 #include "theory/theory_engine.h"
+#include "prop/minisat/simp/SimpSolver.h"
+#include "prop/minisat/core/SolverTypes.h"
+
+#include <map>
 
 namespace CVC4 {
-namespace prop {
 
 // In terms of abstraction, this is below (and provides services to)
 // Prover and above (and requires the services of) a specific
 // propositional solver, DPLL or otherwise.
 
 class PropEngine {
-  DecisionEngine* d_de;
+  DecisionEngine &d_de;
+  TheoryEngine &d_te;
+  CVC4::prop::minisat::SimpSolver d_sat;
+  std::map<Expr, CVC4::prop::minisat::Var> d_vars;
+  std::map<CVC4::prop::minisat::Var, Expr> d_varsReverse;
+
+  void addVars(Expr);
 
 public:
   /**
    * Create a PropEngine with a particular decision and theory engine.
    */
-  PropEngine(DecisionEngine*, TheoryEngine*);
+  CVC4_PUBLIC PropEngine(CVC4::DecisionEngine&, CVC4::TheoryEngine&);
 
   /**
    * Converts to CNF if necessary.
@@ -39,7 +49,6 @@ public:
 
 };/* class PropEngine */
 
-}/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__PROP__PROP_ENGINE_H */
+#endif /* __CVC4__PROP_ENGINE_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 05ee12462..412c0f3af 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -27,11 +27,12 @@ void SmtEngine::processAssertionList() {
   for(std::vector<Expr>::iterator i = d_assertions.begin();
       i != d_assertions.end();
       ++i)
-    ;//d_expr = d_expr.isNull() ? *i : d_expr.andExpr(*i);
+    d_expr = d_expr.isNull() ? *i : d_expr.andExpr(*i);
 }
 
 Result SmtEngine::check() {
   processAssertionList();
+  d_prop.solve(d_expr);
   return Result(Result::VALIDITY_UNKNOWN);
 }
 
@@ -56,7 +57,7 @@ Result SmtEngine::query(Expr e) {
   return check();
 }
 
-Result SmtEngine::assert(Expr e) {
+Result SmtEngine::assertFormula(Expr e) {
   e = preprocess(e);
   addFormula(e);
   return quickCheck();
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index ab3fc816a..30786511e 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -20,6 +20,8 @@
 #include "util/result.h"
 #include "util/model.h"
 #include "util/options.h"
+#include "prop/prop_engine.h"
+#include "util/decision_engine.h"
 
 // In terms of abstraction, this is below (and provides services to)
 // ValidityChecker and above (and requires the services of)
@@ -54,6 +56,15 @@ class SmtEngine {
   /** Expression built-up for handing off to the propagation engine */
   Expr d_expr;
 
+  /** The decision engine */
+  DecisionEngine d_de;
+
+  /** The decision engine */
+  TheoryEngine d_te;
+
+  /** The propositional engine */
+  PropEngine d_prop;
+
   /**
    * Pre-process an Expr.  This is expected to be highly-variable,
    * with a lot of "source-level configurability" to add multiple
@@ -90,7 +101,14 @@ public:
   /*
    * Construct an SmtEngine with the given expression manager and user options.
    */
-  SmtEngine(ExprManager* em, Options* opts) throw() : d_em(em), d_opts(opts), d_expr(Expr::null()) {}
+  SmtEngine(ExprManager* em, Options* opts) throw() :
+    d_em(em),
+    d_opts(opts),
+    d_expr(Expr::null()),
+    d_de(),
+    d_te(),
+    d_prop(d_de, d_te) {
+  }
 
   /**
    * Execute a command.
@@ -103,7 +121,7 @@ public:
    * literals and conjunction of literals.  Returns false iff
    * inconsistent.
    */
-  Result assert(Expr);
+  Result assertFormula(Expr);
 
   /**
    * Add a formula to the current context and call check().  Returns
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index fead8e224..d6d8691b2 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -9,11 +9,10 @@
  **
  **/
 
-#ifndef __CVC4__THEORY__THEORY_ENGINE_H
-#define __CVC4__THEORY__THEORY_ENGINE_H
+#ifndef __CVC4__THEORY_ENGINE_H
+#define __CVC4__THEORY_ENGINE_H
 
 namespace CVC4 {
-namespace theory {
 
 // In terms of abstraction, this is below (and provides services to)
 // PropEngine.
@@ -28,7 +27,6 @@ class TheoryEngine {
 public:
 };/* class TheoryEngine */
 
-}/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__THEORY_ENGINE_H */
+#endif /* __CVC4__THEORY_ENGINE_H */
diff --git a/src/util/Assert.h b/src/util/Assert.h
new file mode 100644
index 000000000..8fd970c6c
--- /dev/null
+++ b/src/util/Assert.h
@@ -0,0 +1,111 @@
+/*********************                                           -*- C++ -*-  */
+/** 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
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Assertion utility classes, functions, and exceptions.
+ **/
+
+#ifndef __CVC4__ASSERT_H
+#define __CVC4__ASSERT_H
+
+#include <string>
+#include "util/exception.h"
+#include "cvc4_config.h"
+#include "config.h"
+
+namespace CVC4 {
+
+class CVC4_PUBLIC AssertionException : public Exception {
+public:
+  AssertionException() : Exception() {}
+  AssertionException(std::string msg) : Exception(msg) {}
+  AssertionException(const char* msg) : Exception(msg) {}
+};/* class 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 */
+#  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 c70553c3e..8baf872d2 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -5,4 +5,6 @@ AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 noinst_LTLIBRARIES = libutil.la
 
 libutil_la_SOURCES = \
-	command.cpp
+	command.cpp \
+	decision_engine.cpp \
+	output.cpp
diff --git a/src/util/assert.h b/src/util/assert.h
deleted file mode 100644
index 8fd970c6c..000000000
--- a/src/util/assert.h
+++ /dev/null
@@ -1,111 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** 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
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.
- **
- ** Assertion utility classes, functions, and exceptions.
- **/
-
-#ifndef __CVC4__ASSERT_H
-#define __CVC4__ASSERT_H
-
-#include <string>
-#include "util/exception.h"
-#include "cvc4_config.h"
-#include "config.h"
-
-namespace CVC4 {
-
-class CVC4_PUBLIC AssertionException : public Exception {
-public:
-  AssertionException() : Exception() {}
-  AssertionException(std::string msg) : Exception(msg) {}
-  AssertionException(const char* msg) : Exception(msg) {}
-};/* class 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 */
-#  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/command.cpp b/src/util/command.cpp
index 190f794da..c78fbc089 100644
--- a/src/util/command.cpp
+++ b/src/util/command.cpp
@@ -31,7 +31,7 @@ AssertCommand::AssertCommand(const Expr& e) :
 }
 
 void AssertCommand::invoke(SmtEngine* smt_engine) {
-  smt_engine->assert(d_expr);
+  smt_engine->assertFormula(d_expr);
 }
 
 CheckSatCommand::CheckSatCommand() {
diff --git a/src/util/decision_engine.cpp b/src/util/decision_engine.cpp
new file mode 100644
index 000000000..ae79f920d
--- /dev/null
+++ b/src/util/decision_engine.cpp
@@ -0,0 +1,29 @@
+/*********************                                           -*- C++ -*-  */
+/** decision_engine.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/decision_engine.h"
+#include "util/Assert.h"
+#include "util/literal.h"
+
+namespace CVC4 {
+
+DecisionEngine::~DecisionEngine() {
+}
+
+/**
+ * Only here to permit compilation and linkage.  This may be pure
+ * virtual in the final design (?)
+ */
+Literal DecisionEngine::nextDecision() {
+  Unreachable();
+}
+
+}/* CVC4 namespace */
diff --git a/src/util/decision_engine.h b/src/util/decision_engine.h
index a6f8596dd..3a093211c 100644
--- a/src/util/decision_engine.h
+++ b/src/util/decision_engine.h
@@ -12,6 +12,7 @@
 #ifndef __CVC4__DECISION_ENGINE_H
 #define __CVC4__DECISION_ENGINE_H
 
+#include "cvc4_config.h"
 #include "util/literal.h"
 
 namespace CVC4 {
@@ -22,12 +23,17 @@ namespace CVC4 {
 /**
  * A decision mechanism for the next decision.
  */
-class DecisionEngine {
+class CVC4_PUBLIC DecisionEngine {
 public:
+  /**
+   * Destructor.
+   */
+  virtual ~DecisionEngine();
+
   /**
    * Get the next decision.
    */
-  virtual Literal nextDecision() = 0;
+  virtual Literal nextDecision();// = 0
 
   // TODO: design decision: decision engine should be notified of
   // propagated lits, and also why(?) (so that it can make decisions
diff --git a/src/util/literal.h b/src/util/literal.h
index 7af9826bb..3ec216a6a 100644
--- a/src/util/literal.h
+++ b/src/util/literal.h
@@ -14,7 +14,8 @@
 
 namespace CVC4 {
 
-class Literal;
+class Literal {
+};
 
 }/* CVC4 namespace */
 
diff --git a/src/util/output.cpp b/src/util/output.cpp
new file mode 100644
index 000000000..e07f32a66
--- /dev/null
+++ b/src/util/output.cpp
@@ -0,0 +1,29 @@
+/*********************                                           -*- C++ -*-  */
+/** output.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.
+ **
+ ** Output utility classes and functions.
+ **/
+
+#include "cvc4_config.h"
+
+#include <iostream>
+#include "util/output.h"
+
+namespace CVC4 {
+
+null_streambuf null_sb;
+std::ostream null_os(&null_sb);
+
+DebugC   Debug  (&std::cout);
+WarningC Warning(&std::cerr);
+NoticeC  Notice (&std::cout);
+ChatC    Chat   (&std::cout);
+TraceC   Trace  (&std::cout);
+
+}/* CVC4 namespace */
diff --git a/src/util/output.h b/src/util/output.h
index 21b7b6e4c..b6532b93a 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -13,125 +13,164 @@
 #ifndef __CVC4__OUTPUT_H
 #define __CVC4__OUTPUT_H
 
+#include "cvc4_config.h"
+
 #include <iostream>
 #include <string>
+#include <cstdio>
+#include <cstdarg>
 #include <set>
+
 #include "util/exception.h"
 
 namespace CVC4 {
 
-class Debug {
+class null_streambuf : public std::streambuf {
+public:
+  int overflow(int c) { return c; }
+};/* class null_streambuf */
+
+extern null_streambuf null_sb;
+extern std::ostream null_os CVC4_PUBLIC;
+
+class CVC4_PUBLIC DebugC {
   std::set<std::string> d_tags;
-  std::ostream &d_out;
+  std::ostream *d_os;
 
 public:
-  static void operator()(const char* tag, const char*);
-  static void operator()(const char* tag, std::string);
-  static void operator()(string tag, const char*);
-  static void operator()(string tag, std::string);
-  static void operator()(const char*);// Yeting option
-  static void operator()(std::string);// Yeting option
+  DebugC(std::ostream* os) : d_os(os) {}
+
+  void operator()(const char* tag, const char*);
+  void operator()(const char* tag, std::string);
+  void operator()(std::string tag, const char*);
+  void operator()(std::string tag, std::string);
+  //void operator()(const char*);// Yeting option
+  //void operator()(std::string);// Yeting option
 
   static void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
-  static void printf(const char* tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3)));
   static void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
-  static void printf(std::string tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3)));
   // Yeting option not possible here
 
-  static std::ostream& operator()(const char* tag);
-  static std::ostream& operator()(std::string tag);
-  static std::ostream& operator()();// Yeting option
+  std::ostream& operator()(const char* tag) {
+    if(d_tags.find(tag) != d_tags.end())
+      return *d_os;
+    else return null_os;
+  }
+  std::ostream& operator()(std::string tag) {
+    if(d_tags.find(tag) != d_tags.end())
+      return *d_os;
+    else return null_os;
+  }
+  std::ostream& operator()();// Yeting option
 
-  static void on (const char* tag) { d_tags.insert(std::string(tag)); }
-  static void on (std::string tag) { d_tags.insert(tag);              }
-  static void off(const char* tag) { d_tags.erase (std::string(tag)); }
-  static void off(std::string tag) { d_tags.erase (tag);              }
+  void on (const char* tag) { d_tags.insert(std::string(tag)); }
+  void on (std::string tag) { d_tags.insert(tag);              }
+  void off(const char* tag) { d_tags.erase (std::string(tag)); }
+  void off(std::string tag) { d_tags.erase (tag);              }
 
-  static void setStream(std::ostream& os) { d_out = os; }
+  void setStream(std::ostream& os) { d_os = &os; }
 };/* class Debug */
 
+extern DebugC Debug CVC4_PUBLIC;
 
-class Warning {
-  std::ostream &d_out;
+class CVC4_PUBLIC WarningC {
+  std::ostream *d_os;
 
 public:
-  static void operator()(const char*);
-  static void operator()(std::string);
+  WarningC(std::ostream* os) : d_os(os) {}
 
-  static void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
-  static void printf(std::string fmt, ...) __attribute__ ((format(printf, 2, 3)));
+  void operator()(const char* s) { *d_os << s; }
+  void operator()(std::string s) { *d_os << s; }
 
-  static std::ostream& operator()();
+  void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
 
-  static void setStream(std::ostream& os) { d_out = os; }
+  std::ostream& operator()() { return *d_os; }
+
+  void setStream(std::ostream& os) { d_os = &os; }
 };/* class Warning */
 
+extern WarningC Warning CVC4_PUBLIC;
 
-class Notice {
-  std::ostream &d_os;
+class CVC4_PUBLIC NoticeC {
+  std::ostream *d_os;
 
 public:
-  static void operator()(const char*);
-  static void operator()(std::string);
+  NoticeC(std::ostream* os) : d_os(os) {}
+
+  void operator()(const char*);
+  void operator()(std::string);
 
-  static void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
-  static void printf(std::string fmt, ...) __attribute__ ((format(printf, 2, 3)));
+  void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
 
-  static std::ostream& operator()();
+  std::ostream& operator()() { return *d_os; }
 
-  static void setStream(std::ostream& os) { d_out = os; }
+  void setStream(std::ostream& os) { d_os = &os; }
 };/* class Notice */
 
+extern NoticeC Notice CVC4_PUBLIC;
 
-class Chat {
-  std::ostream &d_os;
+class CVC4_PUBLIC ChatC {
+  std::ostream *d_os;
 
 public:
-  static void operator()(const char*);
-  static void operator()(std::string);
+  ChatC(std::ostream* os) : d_os(os) {}
 
-  static void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
-  static void printf(std::string fmt, ...) __attribute__ ((format(printf, 2, 3)));
+  void operator()(const char*);
+  void operator()(std::string);
 
-  static std::ostream& operator()();
+  void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
 
-  static void setStream(std::ostream& os) { d_out = os; }
+  std::ostream& operator()() { return *d_os; }
+
+  void setStream(std::ostream& os) { d_os = &os; }
 };/* class Chat */
 
+extern ChatC Chat CVC4_PUBLIC;
 
-class Trace {
-  std::ostream &d_os;
+class CVC4_PUBLIC TraceC {
+  std::ostream *d_os;
+  std::set<std::string> d_tags;
 
 public:
-  static void operator()(const char* tag, const char*);
-  static void operator()(const char* tag, std::string);
-  static void operator()(string tag, const char*);
-  static void operator()(string tag, std::string);
+  TraceC(std::ostream* os) : d_os(os) {}
 
-  static void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3))) {
+  void operator()(const char* tag, const char*);
+  void operator()(const char* tag, std::string);
+  void operator()(std::string tag, const char*);
+  void operator()(std::string tag, std::string);
+
+  void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))) {
+    char buf[1024];
     va_list vl;
     va_start(vl, fmt);
-    vfprintf(buf, 1024, fmt, vl);
+    vsnprintf(buf, sizeof(buf), fmt, vl);
     va_end(vl);
+    *d_os << buf;
   }
-  static void printf(const char* tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3))) {
-  }
-  static void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3))) {
+  void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))) {
   }
-  static void printf(std::string tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3))) {
+
+  std::ostream& operator()(const char* tag) {
+    if(d_tags.find(tag) != d_tags.end())
+      return *d_os;
+    else return null_os;
   }
 
-  static std::ostream& operator()(const char* tag);
-  static std::ostream& operator()(std::string tag);
+  std::ostream& operator()(std::string tag) {
+    if(d_tags.find(tag) != d_tags.end())
+      return *d_os;
+    else return null_os;
+  }
 
-  static void on (const char* tag) { d_tags.insert(std::string(tag)); };
-  static void on (std::string tag) { d_tags.insert(tag);              };
-  static void off(const char* tag) { d_tags.erase (std::string(tag)); };
-  static void off(std::string tag) { d_tags.erase (tag);              };
+  void on (const char* tag) { d_tags.insert(std::string(tag)); };
+  void on (std::string tag) { d_tags.insert(tag);              };
+  void off(const char* tag) { d_tags.erase (std::string(tag)); };
+  void off(std::string tag) { d_tags.erase (tag);              };
 
-  static void setStream(std::ostream& os) { d_out = os; }
+  void setStream(std::ostream& os) { d_os = &os; }
 };/* class Trace */
 
+extern TraceC Trace CVC4_PUBLIC;
 
 }/* CVC4 namespace */