From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 16 Jul 2012 15:53:22 +0000 (+0000)
Subject: Support for having two SmtEngines with the same ExprManager.
X-Git-Tag: cvc5-1.0.0~7925
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=36615c5e7332e26645b33ce9b6bab25439a5108e;p=cvc5.git

Support for having two SmtEngines with the same ExprManager.

Basically, this involves creating a separate StatisticsRegistry for the
ExprManager and for the SmtEngine.  Otherwise, theories register the
same statistic twice.  This is a larger problem, though, for creating
multiple instances of theories, and that is unaddressed.  Still,
separating out the expr statistics into a separate registry is probably
a good idea, since the expr package is somewhat separate anyway (and in
the short term it allows two SmtEngines to co-exist).
---

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 1db534dc4..25578399f 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -40,7 +40,7 @@ ${includes}
       stringstream statName; \
       statName << "expr::ExprManager::" << kind; \
       d_exprStatistics[kind] = new IntStat(statName.str(), 0); \
-      StatisticsRegistry::registerStat(d_exprStatistics[kind]); \
+      d_nodeManager->getStatisticsRegistry()->registerStat_(d_exprStatistics[kind]); \
     } \
     ++ *(d_exprStatistics[kind]); \
   }
@@ -56,7 +56,7 @@ ${includes}
         statName << "expr::ExprManager::VARIABLE:" << type; \
       } \
       d_exprStatisticsVars[type] = new IntStat(statName.str(), 0); \
-      StatisticsRegistry::registerStat(d_exprStatisticsVars[type]); \
+      d_nodeManager->getStatisticsRegistry()->registerStat_(d_exprStatisticsVars[type]); \
     } \
     ++ *(d_exprStatisticsVars[type]); \
   }
@@ -78,7 +78,7 @@ ExprManager::ExprManager() :
   for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
     d_exprStatistics[i] = NULL;
   }
-  for (unsigned i = 0; i <= LAST_TYPE; ++ i) {
+  for (unsigned i = 0; i < LAST_TYPE; ++ i) {
     d_exprStatisticsVars[i] = NULL;
   }
 #endif
@@ -88,7 +88,7 @@ ExprManager::ExprManager(const Options& options) :
   d_ctxt(new Context()),
   d_nodeManager(new NodeManager(d_ctxt, this, options)) {
 #ifdef CVC4_STATISTICS_ON
-  for (unsigned i = 0; i <= LAST_TYPE; ++ i) {
+  for (unsigned i = 0; i < LAST_TYPE; ++ i) {
     d_exprStatisticsVars[i] = NULL;
   }
   for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
@@ -105,13 +105,13 @@ ExprManager::~ExprManager() throw() {
 #ifdef CVC4_STATISTICS_ON
     for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
       if (d_exprStatistics[i] != NULL) {
-        StatisticsRegistry::unregisterStat(d_exprStatistics[i]);
+        d_nodeManager->getStatisticsRegistry()->unregisterStat_(d_exprStatistics[i]);
         delete d_exprStatistics[i];
       }
     }
-    for (unsigned i = 0; i <= LAST_TYPE; ++ i) {
+    for (unsigned i = 0; i < LAST_TYPE; ++ i) {
       if (d_exprStatisticsVars[i] != NULL) {
-        StatisticsRegistry::unregisterStat(d_exprStatisticsVars[i]);
+        d_nodeManager->getStatisticsRegistry()->unregisterStat_(d_exprStatisticsVars[i]);
         delete d_exprStatisticsVars[i];
       }
     }
@@ -886,6 +886,10 @@ Context* ExprManager::getContext() const {
   return d_ctxt;
 }
 
+StatisticsRegistry* ExprManager::getStatisticsRegistry() const throw() {
+  return d_nodeManager->getStatisticsRegistry();
+}
+
 namespace expr {
 
 Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap);
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 9d0b8d34a..fdc1e1159 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -27,6 +27,7 @@
 #include "expr/type.h"
 #include "expr/expr.h"
 #include "util/subrange_bound.h"
+#include "util/stats.h"
 
 ${includes}
 
@@ -34,7 +35,7 @@ ${includes}
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 38 "${template}"
+#line 39 "${template}"
 
 namespace CVC4 {
 
@@ -64,7 +65,7 @@ private:
   NodeManager* d_nodeManager;
 
   /** Counts of expressions and variables created of a given kind */
-  IntStat* d_exprStatisticsVars[LAST_TYPE + 1];
+  IntStat* d_exprStatisticsVars[LAST_TYPE];
   IntStat* d_exprStatistics[kind::LAST_KIND];
 
   /**
@@ -450,6 +451,9 @@ public:
   Expr mkVar(const std::string& name, Type type);
   Expr mkVar(Type type);
 
+  /** Get a reference to the statistics registry for this ExprManager */
+  StatisticsRegistry* getStatisticsRegistry() const throw();
+
   /** Export an expr to a different ExprManager */
   //static Expr exportExpr(const Expr& e, ExprManager* em);
   /** Export a type to a different ExprManager */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 6ce96e70a..6c34eb4a3 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -277,7 +277,7 @@ public:
   }
 
   /** Get this node manager's statistics registry */
-  StatisticsRegistry* getStatisticsRegistry() const {
+  StatisticsRegistry* getStatisticsRegistry() const throw() {
     return d_statisticsRegistry;
   }
 
@@ -802,7 +802,7 @@ public:
     Debug("current") << "node manager scope: "
                      << "returning to " << NodeManager::s_current << "\n";
   }
-};
+};/* class NodeManagerScope */
 
 
 template <class AttrKind>
diff --git a/src/main/driver.cpp b/src/main/driver.cpp
index eda5df2ca..f24526e6c 100644
--- a/src/main/driver.cpp
+++ b/src/main/driver.cpp
@@ -240,6 +240,7 @@ int runCvc4(int argc, char* argv[], Options& options) {
 
   // signal handlers need access
   pStatistics = smt.getStatisticsRegistry();
+  pStatistics->registerStat_(exprMgr.getStatisticsRegistry());
 
   // Timer statistic
   RegisterStatistic statTotalTime(exprMgr, &s_totalTime);
diff --git a/src/main/driver_portfolio.cpp b/src/main/driver_portfolio.cpp
index 0698d5157..d93e9f872 100644
--- a/src/main/driver_portfolio.cpp
+++ b/src/main/driver_portfolio.cpp
@@ -409,7 +409,7 @@ int runCvc4(int argc, char *argv[], Options& options) {
   theStatisticsRegistry.registerStat_((&driverStatisticsRegistry));
 
   // Timer statistic
-  RegisterStatistic* statTotatTime =
+  RegisterStatistic* statTotalTime =
     new RegisterStatistic(&driverStatisticsRegistry, &s_totalTime);
   RegisterStatistic* statBeforePortfolioTime =
     new RegisterStatistic(&driverStatisticsRegistry, &s_beforePortfolioTime);
@@ -521,7 +521,8 @@ int runCvc4(int argc, char *argv[], Options& options) {
     // Register the statistics registry of the thread
     string tag = "thread #" + boost::lexical_cast<string>(threadOptions[i].thread_id);
     smts[i]->getStatisticsRegistry()->setName(tag);
-    theStatisticsRegistry.registerStat_( (Stat*)smts[i]->getStatisticsRegistry() );
+    theStatisticsRegistry.registerStat_( smts[i]->getStatisticsRegistry() );
+    theStatisticsRegistry.registerStat_( exprMgrs[i]->getStatisticsRegistry() );
   }
 
   /************************* Lemma sharing init ************************/
@@ -635,7 +636,7 @@ int runCvc4(int argc, char *argv[], Options& options) {
 
   //delete vmaps;
 
-  delete statTotatTime;
+  delete statTotalTime;
   delete statBeforePortfolioTime;
   delete statFilenameReg;
 
diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am
index 3e777ec89..5cc0cedd1 100644
--- a/src/smt/Makefile.am
+++ b/src/smt/Makefile.am
@@ -8,6 +8,8 @@ noinst_LTLIBRARIES = libsmt.la
 libsmt_la_SOURCES = \
 	smt_engine.cpp \
 	smt_engine.h \
+	smt_engine_scope.cpp \
+	smt_engine_scope.h \
 	modal_exception.h \
 	bad_option_exception.h \
 	no_such_function_exception.h
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4cccb8d10..01ce73be1 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -38,6 +38,7 @@
 #include "smt/modal_exception.h"
 #include "smt/no_such_function_exception.h"
 #include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
 #include "theory/theory_engine.h"
 #include "proof/proof_manager.h"
 #include "util/proof.h"
@@ -48,16 +49,9 @@
 #include "util/output.h"
 #include "util/hash.h"
 #include "theory/substitutions.h"
-#include "theory/builtin/theory_builtin.h"
-#include "theory/booleans/theory_bool.h"
-#include "theory/booleans/circuit_propagator.h"
-#include "theory/uf/theory_uf.h"
-#include "theory/arith/theory_arith.h"
-#include "theory/arrays/theory_arrays.h"
-#include "theory/bv/theory_bv.h"
-#include "theory/datatypes/theory_datatypes.h"
 #include "theory/theory_traits.h"
 #include "theory/logic_info.h"
+#include "theory/booleans/circuit_propagator.h"
 #include "util/ite_removal.h"
 #include "theory/model.h"
 
@@ -265,6 +259,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   d_cumulativeResourceUsed(0),
   d_status(),
   d_private(new smt::SmtEnginePrivate(*this)),
+  d_statisticsRegistry(new StatisticsRegistry()),
   d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
   d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"),
   d_numConstantProps("smt::SmtEngine::numConstantProps", 0),
@@ -277,7 +272,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
   d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0) {
 
-  NodeManagerScope nms(d_nodeManager);
+  SmtScope smts(this);
 
   StatisticsRegistry::registerStat(&d_definitionExpansionTime);
   StatisticsRegistry::registerStat(&d_nonclausalSimplificationTime);
@@ -382,7 +377,7 @@ void SmtEngine::shutdown() {
 }
 
 SmtEngine::~SmtEngine() throw() {
-  NodeManagerScope nms(d_nodeManager);
+  SmtScope smts(this);
 
   try {
     while(Options::current()->incrementalSolving && d_userContext->getLevel() > 1) {
@@ -424,6 +419,9 @@ SmtEngine::~SmtEngine() throw() {
     delete d_theoryEngine;
     delete d_propEngine;
     //delete d_decisionEngine;
+
+    delete d_statisticsRegistry;
+
   } catch(Exception& e) {
     Warning() << "CVC4 threw an exception during cleanup." << endl
               << e << endl;
@@ -431,7 +429,7 @@ SmtEngine::~SmtEngine() throw() {
 }
 
 void SmtEngine::setLogic(const LogicInfo& logic) throw(ModalException) {
-  NodeManagerScope nms(d_nodeManager);
+  SmtScope smts(this);
 
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << SetBenchmarkLogicCommand(logic.getLogicString());
@@ -442,7 +440,7 @@ void SmtEngine::setLogic(const LogicInfo& logic) throw(ModalException) {
 }
 
 void SmtEngine::setLogic(const std::string& s) throw(ModalException) {
-  NodeManagerScope nms(d_nodeManager);
+  SmtScope smts(this);
 
   setLogic(LogicInfo(s));
 }
@@ -605,7 +603,7 @@ void SmtEngine::setLogicInternal() throw(AssertionException) {
 void SmtEngine::setInfo(const std::string& key, const SExpr& value)
   throw(BadOptionException, ModalException) {
 
-  NodeManagerScope nms(d_nodeManager);
+  SmtScope smts(this);
 
   Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl;
   if(Dump.isOn("benchmark")) {
@@ -629,7 +627,7 @@ void SmtEngine::setInfo(const std::string& key, const SExpr& value)
         if(! value.isAtom()) {
           throw BadOptionException("argument to (set-info :cvc4-logic ..) must be a string");
         }
-        NodeManagerScope nms(d_nodeManager);
+        SmtScope smts(this);
         d_logic = value.getValue();
         setLogicInternal();
         return;
@@ -664,7 +662,7 @@ void SmtEngine::setInfo(const std::string& key, const SExpr& value)
 SExpr SmtEngine::getInfo(const std::string& key) const
   throw(BadOptionException) {
 
-  NodeManagerScope nms(d_nodeManager);
+  SmtScope smts(this);
 
   Trace("smt") << "SMT getInfo(" << key << ")" << endl;
   if(key == ":all-statistics") {
@@ -705,7 +703,7 @@ SExpr SmtEngine::getInfo(const std::string& key) const
 void SmtEngine::setOption(const std::string& key, const SExpr& value)
   throw(BadOptionException, ModalException) {
 
-  NodeManagerScope nms(d_nodeManager);
+  SmtScope smts(this);
 
   Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
   if(Dump.isOn("benchmark")) {
@@ -757,7 +755,7 @@ void SmtEngine::setOption(const std::string& key, const SExpr& value)
 SExpr SmtEngine::getOption(const std::string& key) const
   throw(BadOptionException) {
 
-  NodeManagerScope nms(d_nodeManager);
+  SmtScope smts(this);
 
   Trace("smt") << "SMT getOption(" << key << ")" << endl;
   if(Dump.isOn("benchmark")) {
@@ -804,7 +802,7 @@ void SmtEngine::defineFunction(Expr func,
        << func;
     Dump("declarations") << DefineFunctionCommand(ss.str(), func, formals, formula);
   }
-  NodeManagerScope nms(d_nodeManager);
+  SmtScope smts(this);
 
   // type check body
   Type formulaType = formula.getType(Options::current()->typeChecking);
@@ -1606,7 +1604,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) {
 
   Assert(e.isNull() || e.getExprManager() == d_exprManager);
 
-  NodeManagerScope nms(d_nodeManager);
+  SmtScope smts(this);
 
   finalOptionsAreSet();
 
@@ -1669,7 +1667,7 @@ Result SmtEngine::query(const BoolExpr& e) {
   Assert(!e.isNull());
   Assert(e.getExprManager() == d_exprManager);
 
-  NodeManagerScope nms(d_nodeManager);
+  SmtScope smts(this);
 
   finalOptionsAreSet();
 
@@ -1725,7 +1723,7 @@ Result SmtEngine::query(const BoolExpr& e) {
 
 Result SmtEngine::assertFormula(const BoolExpr& e) {
   Assert(e.getExprManager() == d_exprManager);
-  NodeManagerScope nms(d_nodeManager);
+  SmtScope smts(this);
   finalOptionsAreSet();
   Trace("smt") << "SmtEngine::assertFormula(" << e << ")" << endl;
   ensureBoolean(e);
@@ -1738,7 +1736,7 @@ Result SmtEngine::assertFormula(const BoolExpr& e) {
 
 Expr SmtEngine::simplify(const Expr& e) {
   Assert(e.getExprManager() == d_exprManager);
-  NodeManagerScope nms(d_nodeManager);
+  SmtScope smts(this);
   finalOptionsAreSet();
   if( Options::current()->typeChecking ) {
     e.getType(true);// ensure expr is type-checked at this point
@@ -1753,7 +1751,7 @@ Expr SmtEngine::simplify(const Expr& e) {
 Expr SmtEngine::getValue(const Expr& e)
   throw(ModalException, AssertionException) {
   Assert(e.getExprManager() == d_exprManager);
-  NodeManagerScope nms(d_nodeManager);
+  SmtScope smts(this);
 
   // ensure expr is type-checked at this point
   Type type = e.getType(Options::current()->typeChecking);
@@ -1799,7 +1797,7 @@ Expr SmtEngine::getValue(const Expr& e)
 }
 
 bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
-  NodeManagerScope nms(d_nodeManager);
+  SmtScope smts(this);
   finalOptionsAreSet();
   Type type = e.getType(Options::current()->typeChecking);
   // must be Boolean
@@ -1828,7 +1826,7 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
 
 SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
   Trace("smt") << "SMT getAssignment()" << endl;
-  NodeManagerScope nms(d_nodeManager);
+  SmtScope smts(this);
   finalOptionsAreSet();
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << GetAssignmentCommand();
@@ -1890,7 +1888,7 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
 
 void SmtEngine::addToModelType( Type& t ){
   Trace("smt") << "SMT addToModelType(" << t << ")" << endl;
-  NodeManagerScope nms(d_nodeManager);
+  SmtScope smts(this);
   if( Options::current()->produceModels ) {
     d_theoryEngine->getModel()->addDefineType( TypeNode::fromType( t ) );
   }
@@ -1898,7 +1896,7 @@ void SmtEngine::addToModelType( Type& t ){
 
 void SmtEngine::addToModelFunction( Expr& e ){
   Trace("smt") << "SMT addToModelFunction(" << e << ")" << endl;
-  NodeManagerScope nms(d_nodeManager);
+  SmtScope smts(this);
   if( Options::current()->produceModels ) {
     d_theoryEngine->getModel()->addDefineFunction( e.getNode() );
   }
@@ -1907,7 +1905,7 @@ void SmtEngine::addToModelFunction( Expr& e ){
 
 Model* SmtEngine::getModel() throw(ModalException, AssertionException){
   Trace("smt") << "SMT getModel()" << endl;
-  NodeManagerScope nms(d_nodeManager);
+  SmtScope smts(this);
 
   if(!Options::current()->produceModels) {
     const char* msg =
@@ -1928,7 +1926,7 @@ Model* SmtEngine::getModel() throw(ModalException, AssertionException){
 
 Proof* SmtEngine::getProof() throw(ModalException, AssertionException) {
   Trace("smt") << "SMT getProof()" << endl;
-  NodeManagerScope nms(d_nodeManager);
+  SmtScope smts(this);
   finalOptionsAreSet();
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << GetProofCommand();
@@ -1958,7 +1956,7 @@ vector<Expr> SmtEngine::getAssertions()
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << GetAssertionsCommand();
   }
-  NodeManagerScope nms(d_nodeManager);
+  SmtScope smts(this);
   Trace("smt") << "SMT getAssertions()" << endl;
   if(!Options::current()->interactive) {
     const char* msg =
@@ -1970,13 +1968,13 @@ vector<Expr> SmtEngine::getAssertions()
 }
 
 size_t SmtEngine::getStackLevel() const {
-  NodeManagerScope nms(d_nodeManager);
+  SmtScope smts(this);
   Trace("smt") << "SMT getStackLevel()" << endl;
   return d_context->getLevel();
 }
 
 void SmtEngine::push() {
-  NodeManagerScope nms(d_nodeManager);
+  SmtScope smts(this);
   finalOptionsAreSet();
   Trace("smt") << "SMT push()" << endl;
   d_private->processAssertions();
@@ -2000,7 +1998,7 @@ void SmtEngine::push() {
 }
 
 void SmtEngine::pop() {
-  NodeManagerScope nms(d_nodeManager);
+  SmtScope smts(this);
   finalOptionsAreSet();
   Trace("smt") << "SMT pop()" << endl;
   if(Dump.isOn("benchmark")) {
@@ -2108,11 +2106,11 @@ unsigned long SmtEngine::getTimeRemaining() const throw(ModalException) {
 }
 
 StatisticsRegistry* SmtEngine::getStatisticsRegistry() const {
-  return d_exprManager->d_nodeManager->getStatisticsRegistry();
+  return d_statisticsRegistry;
 }
 
 void SmtEngine::printModel( std::ostream& out, Model* m ){
-  NodeManagerScope nms(d_nodeManager);
+  SmtScope smts(this);
   m->toStream(out);
 }
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index aef98d75b..4df9054a7 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -76,6 +76,7 @@ namespace smt {
   class DefinedFunction;
 
   class SmtEnginePrivate;
+  class SmtScope;
 }/* CVC4::smt namespace */
 
 // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
@@ -248,6 +249,9 @@ class CVC4_PUBLIC SmtEngine {
   void setLogicInternal() throw(AssertionException);
 
   friend class ::CVC4::smt::SmtEnginePrivate;
+  friend class ::CVC4::smt::SmtScope;
+
+  StatisticsRegistry* d_statisticsRegistry;
 
   // === STATISTICS ===
   /** time spent in definition-expansion */
diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp
new file mode 100644
index 000000000..03298e99a
--- /dev/null
+++ b/src/smt/smt_engine_scope.cpp
@@ -0,0 +1,10 @@
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+
+namespace CVC4 {
+namespace smt {
+
+CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current = NULL;
+
+}
+}
diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
new file mode 100644
index 000000000..bcdaefd9f
--- /dev/null
+++ b/src/smt/smt_engine_scope.h
@@ -0,0 +1,40 @@
+#include "smt/smt_engine.h"
+#include "util/tls.h"
+#include "util/Assert.h"
+#include "expr/node_manager.h"
+#include "util/output.h"
+
+#pragma once
+
+namespace CVC4 {
+namespace smt {
+
+extern CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current;
+
+inline SmtEngine* currentSmtEngine() {
+  Assert(s_smtEngine_current != NULL);
+  return s_smtEngine_current;
+}
+
+class SmtScope : public NodeManagerScope {
+  /** The old NodeManager, to be restored on destruction. */
+  SmtEngine* d_oldSmtEngine;
+
+public:
+
+  SmtScope(const SmtEngine* smt) :
+    NodeManagerScope(smt->d_nodeManager),
+    d_oldSmtEngine(s_smtEngine_current) {
+    Assert(smt != NULL);
+    s_smtEngine_current = const_cast<SmtEngine*>(smt);
+    Debug("current") << "smt scope: " << s_smtEngine_current << std::endl;
+  }
+
+  ~SmtScope() {
+    s_smtEngine_current = d_oldSmtEngine;
+    Debug("current") << "smt scope: returning to " << s_smtEngine_current << std::endl;
+  }
+};/* class SmtScope */
+
+}
+}
diff --git a/src/util/stats.cpp b/src/util/stats.cpp
index b030495c5..96e300197 100644
--- a/src/util/stats.cpp
+++ b/src/util/stats.cpp
@@ -20,7 +20,10 @@
 #include "util/stats.h"
 #include "expr/node_manager.h"
 #include "expr/expr_manager_scope.h"
+#include "expr/expr_manager.h"
 #include "lib/clock_gettime.h"
+#include "smt/smt_engine_scope.h"
+#include "smt/smt_engine.h"
 
 #ifdef CVC4_STATISTICS_ON
 #  define __CVC4_USE_STATISTICS true
@@ -34,12 +37,12 @@ std::string Stat::s_delim(",");
 std::string StatisticsRegistry::s_regDelim("::");
 
 StatisticsRegistry* StatisticsRegistry::current() {
-  return NodeManager::currentNM()->getStatisticsRegistry();
+  return smt::currentSmtEngine()->getStatisticsRegistry();
 }
 
 void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) {
 #ifdef CVC4_STATISTICS_ON
-  StatSet& registeredStats = NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats;
+  StatSet& registeredStats = current()->d_registeredStats;
   AlwaysAssert(registeredStats.find(s) == registeredStats.end(),
                "Statistic `%s' was already registered with this registry.", s->getName().c_str());
   registeredStats.insert(s);
@@ -55,7 +58,7 @@ void StatisticsRegistry::registerStat_(Stat* s) throw(AssertionException) {
 
 void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) {
 #ifdef CVC4_STATISTICS_ON
-  StatSet& registeredStats = NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats;
+  StatSet& registeredStats = current()->d_registeredStats;
   AlwaysAssert(registeredStats.find(s) != registeredStats.end(),
                "Statistic `%s' was not registered with this registry.", s->getName().c_str());
   registeredStats.erase(s);
@@ -91,11 +94,11 @@ void StatisticsRegistry::flushStat(std::ostream &out) const {;
 }
 
 StatisticsRegistry::const_iterator StatisticsRegistry::begin() {
-  return NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats.begin();
+  return current()->d_registeredStats.begin();
 }/* StatisticsRegistry::begin() */
 
 StatisticsRegistry::const_iterator StatisticsRegistry::end() {
-  return NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats.end();
+  return current()->d_registeredStats.end();
 }/* StatisticsRegistry::end() */
 
 void TimerStat::start() {
@@ -117,9 +120,14 @@ void TimerStat::stop() {
 }/* TimerStat::stop() */
 
 RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) :
-  d_reg(NULL),
+  d_reg(em.getStatisticsRegistry()),
   d_stat(stat) {
-  ExprManagerScope ems(em);
-  d_reg = StatisticsRegistry::current();
   d_reg->registerStat_(d_stat);
 }
+
+RegisterStatistic::RegisterStatistic(SmtEngine& smt, Stat* stat) :
+  d_reg(smt.getStatisticsRegistry()),
+  d_stat(stat) {
+  d_reg->registerStat_(d_stat);
+}
+
diff --git a/src/util/stats.h b/src/util/stats.h
index 63e732305..aabf04dc0 100644
--- a/src/util/stats.h
+++ b/src/util/stats.h
@@ -43,6 +43,7 @@ namespace CVC4 {
 #endif
 
 class ExprManager;
+class SmtEngine;
 
 class CVC4_PUBLIC Stat;
 
@@ -803,6 +804,8 @@ public:
 
   RegisterStatistic(ExprManager& em, Stat* stat);
 
+  RegisterStatistic(SmtEngine& smt, Stat* stat);
+
   ~RegisterStatistic() {
     d_reg->unregisterStat_(d_stat);
   }
diff --git a/test/system/Makefile.am b/test/system/Makefile.am
index 7fa7b4a68..070f69639 100644
--- a/test/system/Makefile.am
+++ b/test/system/Makefile.am
@@ -2,7 +2,8 @@ TESTS_ENVIRONMENT =
 TEST_EXTENSIONS = .class
 CPLUSPLUS_TESTS = \
 	boilerplate \
-	ouroborous
+	ouroborous \
+	two_smt_engines
 #	cvc3_main
 
 TESTS = $(CPLUSPLUS_TESTS)
diff --git a/test/system/boilerplate.cpp b/test/system/boilerplate.cpp
index c64c1463e..18a560c0e 100644
--- a/test/system/boilerplate.cpp
+++ b/test/system/boilerplate.cpp
@@ -30,6 +30,7 @@ using namespace std;
 int main() {
   ExprManager em;
   Options opts;
+  cout << "foo: " << opts.threadArgv.size() << endl;
   SmtEngine smt(&em);
   Result r = smt.query(em.mkConst(true));
 
diff --git a/test/system/two_smt_engines.cpp b/test/system/two_smt_engines.cpp
new file mode 100644
index 000000000..35d6c92cf
--- /dev/null
+++ b/test/system/two_smt_engines.cpp
@@ -0,0 +1,37 @@
+/*********************                                                        */
+/*! \file two_smt_engines.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  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.\endverbatim
+ **
+ ** \brief A simple test of multiple SmtEngines
+ **
+ ** A simple test of multiple SmtEngines.
+ **/
+
+#include <iostream>
+#include <sstream>
+
+#include "expr/expr.h"
+#include "smt/smt_engine.h"
+
+using namespace CVC4;
+using namespace std;
+
+int main() {
+  ExprManager em;
+  Options opts;
+  SmtEngine smt(&em);
+  SmtEngine smt2(&em);
+  Result r = smt.query(em.mkConst(true));
+
+  return r == Result::VALID ? 0 : 1;
+}
+
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index bb8cdf7fe..dc53bff61 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -2,7 +2,7 @@
 UNIT_TESTS = \
 	theory/logic_info_white \
 	theory/theory_engine_white \
-	theory/theory_black \
+	theory/theory_white \
 	theory/theory_arith_white \
 	theory/union_find_black \
 	theory/theory_bv_white \
@@ -24,7 +24,7 @@ UNIT_TESTS = \
 	expr/type_node_white \
 	parser/parser_black \
 	parser/parser_builder_black \
-	prop/cnf_stream_black \
+	prop/cnf_stream_white \
 	context/context_black \
 	context/context_white \
 	context/context_mm_black \
diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h
deleted file mode 100644
index 70c306a6d..000000000
--- a/test/unit/prop/cnf_stream_black.h
+++ /dev/null
@@ -1,299 +0,0 @@
-/*********************                                                        */
-/*! \file cnf_stream_black.h
- ** \verbatim
- ** Original author: cconway
- ** Major contributors: mdeters
- ** Minor contributors (to current version): taking, dejan
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  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.\endverbatim
- **
- ** \brief White box testing of CVC4::prop::CnfStream.
- **
- ** White box testing of CVC4::prop::CnfStream.
- **/
-
-#include <cxxtest/TestSuite.h>
-/* #include <gmock/gmock.h> */
-/* #include <gtest/gtest.h> */
-
-#include "util/Assert.h"
-
-
-#include "expr/expr_manager.h"
-#include "expr/node_manager.h"
-#include "context/context.h"
-#include "prop/cnf_stream.h"
-#include "prop/prop_engine.h"
-#include "prop/theory_proxy.h"
-#include "smt/smt_engine.h"
-
-#include "theory/theory.h"
-#include "theory/theory_engine.h"
-#include "theory/theory_registrar.h"
-
-#include "theory/builtin/theory_builtin.h"
-#include "theory/booleans/theory_bool.h"
-#include "theory/arith/theory_arith.h"
-
-using namespace CVC4;
-using namespace CVC4::context;
-using namespace CVC4::prop;
-using namespace std;
-
-/* This fake class relies on the face that a MiniSat variable is just an int. */
-class FakeSatSolver : public SatSolver {
-  SatVariable d_nextVar;
-  bool d_addClauseCalled;
-
-public:
-  FakeSatSolver() :
-    d_nextVar(0),
-    d_addClauseCalled(false) {
-  }
-
-  SatVariable newVar(bool theoryAtom) {
-    return d_nextVar++;
-  }
-
-  SatVariable trueVar() {
-    return d_nextVar++;
-  }
-
-  SatVariable falseVar() {
-    return d_nextVar++;
-  }
-
-  void addClause(SatClause& c, bool lemma) {
-    d_addClauseCalled = true;
-  }
-
-  void reset() {
-    d_addClauseCalled = false;
-  }
-
-  unsigned int addClauseCalled() {
-    return d_addClauseCalled;
-  }
-
-  unsigned getAssertionLevel() const {
-    return 0;
-  }
-
-  bool isDecision(Node) const {
-    return false;
-  }
-
-  void unregisterVar(SatLiteral lit) {
-  }
-
-  void renewVar(SatLiteral lit, int level = -1) {
-  }
-
-  void interrupt() {
-  }
-  
-  SatValue solve() {
-    return SAT_VALUE_UNKNOWN;
-  }
-
-  SatValue solve(long unsigned int& resource) {
-    return SAT_VALUE_UNKNOWN;
-  }
-
-  SatValue value(SatLiteral l) {
-    return SAT_VALUE_UNKNOWN;
-  }
-
-  SatValue modelValue(SatLiteral l) {
-    return SAT_VALUE_UNKNOWN;
-  }
-
-  bool properExplanation(SatLiteral lit, SatLiteral expl) const {
-    return true;
-  }
-
-};/* class FakeSatSolver */
-
-class CnfStreamBlack : public CxxTest::TestSuite {
-  /** The SAT solver proxy */
-  FakeSatSolver* d_satSolver;
-
-  /** The logic info */
-  LogicInfo* d_logicInfo;
-
-  /** The theory engine */
-  TheoryEngine* d_theoryEngine;
-
-  /** The output channel */
-  theory::OutputChannel* d_outputChannel;
-
-  /** The CNF converter in use */
-  CnfStream* d_cnfStream;
-
-  /** The context */
-  Context* d_context;
-
-  /** The user context */
-  UserContext* d_userContext;
-
-  /** The node manager */
-  NodeManager* d_nodeManager;
-
-  void setUp() {
-    d_context = new Context();
-    d_userContext = new UserContext();
-    d_nodeManager = new NodeManager(d_context, NULL);
-    NodeManagerScope nms(d_nodeManager);
-    d_satSolver = new FakeSatSolver();
-    d_logicInfo = new LogicInfo();
-    d_logicInfo->lock();
-    d_theoryEngine = new TheoryEngine(d_context, d_userContext, *d_logicInfo);
-    d_theoryEngine->addTheory<theory::builtin::TheoryBuiltin>(theory::THEORY_BUILTIN);
-    d_theoryEngine->addTheory<theory::booleans::TheoryBool>(theory::THEORY_BOOL);
-    d_theoryEngine->addTheory<theory::arith::TheoryArith>(theory::THEORY_ARITH);
-    d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, new theory::TheoryRegistrar(d_theoryEngine));
-  }
-
-  void tearDown() {
-    NodeManagerScope nms(d_nodeManager);
-    delete d_cnfStream;
-    d_theoryEngine->shutdown();
-    delete d_theoryEngine;
-    delete d_logicInfo;
-    delete d_satSolver;
-    delete d_nodeManager;
-    delete d_userContext;
-    delete d_context;
-  }
-
-public:
-
-  /* [chris 5/26/2010] In the tests below, we don't attempt to delve into the
-   * deep structure of the CNF conversion. Firstly, we just want to make sure
-   * that the conversion doesn't choke on any boolean Exprs. We'll also check
-   * that addClause got called. We won't check that it gets called a particular
-   * number of times, or with what.
-   */
-
-  void testAnd() {
-    NodeManagerScope nms(d_nodeManager);
-    Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::AND, a, b, c), false, false);
-    TS_ASSERT( d_satSolver->addClauseCalled() );
-  }
-
-  void testComplexExpr() {
-    NodeManagerScope nms(d_nodeManager);
-    Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    Node d = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    Node e = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    Node f = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::IMPLIES,
-                                                        d_nodeManager->mkNode(kind::AND, a, b),
-                                                        d_nodeManager->mkNode(kind::IFF,
-                                                                              d_nodeManager->mkNode(kind::OR, c, d),
-                                                                              d_nodeManager->mkNode(kind::NOT,
-                                                                                                    d_nodeManager->mkNode(kind::XOR, e, f)))), false, false );
-    TS_ASSERT( d_satSolver->addClauseCalled() );
-  }
-
-  void testTrue() {
-    NodeManagerScope nms(d_nodeManager);
-    d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false, false );
-    TS_ASSERT( d_satSolver->addClauseCalled() );
-  }
-
-  void testFalse() {
-    NodeManagerScope nms(d_nodeManager);
-    d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false, false );
-    TS_ASSERT( d_satSolver->addClauseCalled() );
-  }
-
-  void testIff() {
-    NodeManagerScope nms(d_nodeManager);
-    Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::IFF, a, b), false, false );
-    TS_ASSERT( d_satSolver->addClauseCalled() );
-  }
-
-  void testImplies() {
-    NodeManagerScope nms(d_nodeManager);
-    Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false );
-    TS_ASSERT( d_satSolver->addClauseCalled() );
-  }
-
-  // ITEs should be removed before going to CNF
-  //void testIte() {
-  //  NodeManagerScope nms(d_nodeManager);
-  //  d_cnfStream->convertAndAssert(
-  //      d_nodeManager->mkNode(
-  //          kind::EQUAL,
-  //          d_nodeManager->mkNode(
-  //              kind::ITE,
-  //              d_nodeManager->mkVar(d_nodeManager->booleanType()),
-  //              d_nodeManager->mkVar(d_nodeManager->integerType()),
-  //              d_nodeManager->mkVar(d_nodeManager->integerType())
-  //          ),
-  //          d_nodeManager->mkVar(d_nodeManager->integerType())
-  //                            ), false, false);
-  //
-  //}
-
-  void testNot() {
-    NodeManagerScope nms(d_nodeManager);
-    Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::NOT, a), false, false );
-    TS_ASSERT( d_satSolver->addClauseCalled() );
-  }
-
-  void testOr() {
-    NodeManagerScope nms(d_nodeManager);
-    Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::OR, a, b, c), false, false );
-    TS_ASSERT( d_satSolver->addClauseCalled() );
-  }
-
-  void testVar() {
-    NodeManagerScope nms(d_nodeManager);
-    Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    d_cnfStream->convertAndAssert(a, false, false);
-    TS_ASSERT( d_satSolver->addClauseCalled() );
-    d_satSolver->reset();
-    d_cnfStream->convertAndAssert(b, false, false);
-    TS_ASSERT( d_satSolver->addClauseCalled() );
-  }
-
-  void testXor() {
-    NodeManagerScope nms(d_nodeManager);
-    Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::XOR, a, b), false, false );
-    TS_ASSERT( d_satSolver->addClauseCalled() );
-  }
-
-  void testEnsureLiteral() {
-    NodeManagerScope nms(d_nodeManager);
-    Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    Node a_and_b = d_nodeManager->mkNode(kind::AND, a, b);
-    d_cnfStream->ensureLiteral(a_and_b);
-    // Clauses are necessary to "literal-ize" a_and_b; this perhaps
-    // doesn't belong in a black-box test though...
-    TS_ASSERT( d_satSolver->addClauseCalled() );
-    TS_ASSERT( d_cnfStream->hasLiteral(a_and_b) );
-  }
-};
diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h
new file mode 100644
index 000000000..cc7ea9bf6
--- /dev/null
+++ b/test/unit/prop/cnf_stream_white.h
@@ -0,0 +1,295 @@
+/*********************                                                        */
+/*! \file cnf_stream_white.h
+ ** \verbatim
+ ** Original author: cconway
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): taking, dejan
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  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.\endverbatim
+ **
+ ** \brief White box testing of CVC4::prop::CnfStream.
+ **
+ ** White box testing of CVC4::prop::CnfStream.
+ **/
+
+#include <cxxtest/TestSuite.h>
+/* #include <gmock/gmock.h> */
+/* #include <gtest/gtest.h> */
+
+#include "util/Assert.h"
+
+#include "expr/expr_manager.h"
+#include "expr/node_manager.h"
+#include "context/context.h"
+#include "prop/cnf_stream.h"
+#include "prop/prop_engine.h"
+#include "prop/theory_proxy.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+
+#include "theory/theory.h"
+#include "theory/theory_engine.h"
+#include "theory/theory_registrar.h"
+
+#include "theory/builtin/theory_builtin.h"
+#include "theory/booleans/theory_bool.h"
+#include "theory/arith/theory_arith.h"
+
+using namespace CVC4;
+using namespace CVC4::context;
+using namespace CVC4::prop;
+using namespace CVC4::smt;
+using namespace CVC4::theory;
+using namespace std;
+
+/* This fake class relies on the face that a MiniSat variable is just an int. */
+class FakeSatSolver : public SatSolver {
+  SatVariable d_nextVar;
+  bool d_addClauseCalled;
+
+public:
+  FakeSatSolver() :
+    d_nextVar(0),
+    d_addClauseCalled(false) {
+  }
+
+  SatVariable newVar(bool theoryAtom) {
+    return d_nextVar++;
+  }
+
+  SatVariable trueVar() {
+    return d_nextVar++;
+  }
+
+  SatVariable falseVar() {
+    return d_nextVar++;
+  }
+
+  void addClause(SatClause& c, bool lemma) {
+    d_addClauseCalled = true;
+  }
+
+  void reset() {
+    d_addClauseCalled = false;
+  }
+
+  unsigned int addClauseCalled() {
+    return d_addClauseCalled;
+  }
+
+  unsigned getAssertionLevel() const {
+    return 0;
+  }
+
+  bool isDecision(Node) const {
+    return false;
+  }
+
+  void unregisterVar(SatLiteral lit) {
+  }
+
+  void renewVar(SatLiteral lit, int level = -1) {
+  }
+
+  void interrupt() {
+  }
+  
+  SatValue solve() {
+    return SAT_VALUE_UNKNOWN;
+  }
+
+  SatValue solve(long unsigned int& resource) {
+    return SAT_VALUE_UNKNOWN;
+  }
+
+  SatValue value(SatLiteral l) {
+    return SAT_VALUE_UNKNOWN;
+  }
+
+  SatValue modelValue(SatLiteral l) {
+    return SAT_VALUE_UNKNOWN;
+  }
+
+  bool properExplanation(SatLiteral lit, SatLiteral expl) const {
+    return true;
+  }
+
+};/* class FakeSatSolver */
+
+class CnfStreamWhite : public CxxTest::TestSuite {
+  /** The SAT solver proxy */
+  FakeSatSolver* d_satSolver;
+
+  /** The theory engine */
+  TheoryEngine* d_theoryEngine;
+
+  /** The CNF converter in use */
+  CnfStream* d_cnfStream;
+
+  /** The context */
+  Context* d_context;
+
+  /** The user context */
+  UserContext* d_userContext;
+
+  /** The node manager */
+  NodeManager* d_nodeManager;
+
+  ExprManager* d_exprManager;
+  SmtScope* d_scope;
+  SmtEngine* d_smt;
+
+  void setUp() {
+    d_exprManager = new ExprManager();
+    d_smt = new SmtEngine(d_exprManager);
+    d_smt->d_logic.lock();
+    d_nodeManager = NodeManager::fromExprManager(d_exprManager);
+    d_scope = new SmtScope(d_smt);
+
+    d_context = d_smt->d_context;
+    d_userContext = d_smt->d_userContext;
+
+    d_theoryEngine = d_smt->d_theoryEngine;
+
+    d_satSolver = new FakeSatSolver();
+    d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, new theory::TheoryRegistrar(d_theoryEngine));
+  }
+
+  void tearDown() {
+    delete d_cnfStream;
+    delete d_satSolver;
+    delete d_scope;
+    delete d_smt;
+    delete d_exprManager;
+  }
+
+public:
+
+  /* [chris 5/26/2010] In the tests below, we don't attempt to delve into the
+   * deep structure of the CNF conversion. Firstly, we just want to make sure
+   * that the conversion doesn't choke on any boolean Exprs. We'll also check
+   * that addClause got called. We won't check that it gets called a particular
+   * number of times, or with what.
+   */
+
+  void testAnd() {
+    NodeManagerScope nms(d_nodeManager);
+    Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
+    Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
+    Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
+    d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::AND, a, b, c), false, false);
+    TS_ASSERT( d_satSolver->addClauseCalled() );
+  }
+
+  void testComplexExpr() {
+    NodeManagerScope nms(d_nodeManager);
+    Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
+    Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
+    Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
+    Node d = d_nodeManager->mkVar(d_nodeManager->booleanType());
+    Node e = d_nodeManager->mkVar(d_nodeManager->booleanType());
+    Node f = d_nodeManager->mkVar(d_nodeManager->booleanType());
+    d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::IMPLIES,
+                                                        d_nodeManager->mkNode(kind::AND, a, b),
+                                                        d_nodeManager->mkNode(kind::IFF,
+                                                                              d_nodeManager->mkNode(kind::OR, c, d),
+                                                                              d_nodeManager->mkNode(kind::NOT,
+                                                                                                    d_nodeManager->mkNode(kind::XOR, e, f)))), false, false );
+    TS_ASSERT( d_satSolver->addClauseCalled() );
+  }
+
+  void testTrue() {
+    NodeManagerScope nms(d_nodeManager);
+    d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false, false );
+    TS_ASSERT( d_satSolver->addClauseCalled() );
+  }
+
+  void testFalse() {
+    NodeManagerScope nms(d_nodeManager);
+    d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false, false );
+    TS_ASSERT( d_satSolver->addClauseCalled() );
+  }
+
+  void testIff() {
+    NodeManagerScope nms(d_nodeManager);
+    Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
+    Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
+    d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::IFF, a, b), false, false );
+    TS_ASSERT( d_satSolver->addClauseCalled() );
+  }
+
+  void testImplies() {
+    NodeManagerScope nms(d_nodeManager);
+    Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
+    Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
+    d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false );
+    TS_ASSERT( d_satSolver->addClauseCalled() );
+  }
+
+  // ITEs should be removed before going to CNF
+  //void testIte() {
+  //  NodeManagerScope nms(d_nodeManager);
+  //  d_cnfStream->convertAndAssert(
+  //      d_nodeManager->mkNode(
+  //          kind::EQUAL,
+  //          d_nodeManager->mkNode(
+  //              kind::ITE,
+  //              d_nodeManager->mkVar(d_nodeManager->booleanType()),
+  //              d_nodeManager->mkVar(d_nodeManager->integerType()),
+  //              d_nodeManager->mkVar(d_nodeManager->integerType())
+  //          ),
+  //          d_nodeManager->mkVar(d_nodeManager->integerType())
+  //                            ), false, false);
+  //
+  //}
+
+  void testNot() {
+    NodeManagerScope nms(d_nodeManager);
+    Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
+    d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::NOT, a), false, false );
+    TS_ASSERT( d_satSolver->addClauseCalled() );
+  }
+
+  void testOr() {
+    NodeManagerScope nms(d_nodeManager);
+    Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
+    Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
+    Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
+    d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::OR, a, b, c), false, false );
+    TS_ASSERT( d_satSolver->addClauseCalled() );
+  }
+
+  void testVar() {
+    NodeManagerScope nms(d_nodeManager);
+    Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
+    Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
+    d_cnfStream->convertAndAssert(a, false, false);
+    TS_ASSERT( d_satSolver->addClauseCalled() );
+    d_satSolver->reset();
+    d_cnfStream->convertAndAssert(b, false, false);
+    TS_ASSERT( d_satSolver->addClauseCalled() );
+  }
+
+  void testXor() {
+    NodeManagerScope nms(d_nodeManager);
+    Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
+    Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
+    d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::XOR, a, b), false, false );
+    TS_ASSERT( d_satSolver->addClauseCalled() );
+  }
+
+  void testEnsureLiteral() {
+    NodeManagerScope nms(d_nodeManager);
+    Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
+    Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
+    Node a_and_b = d_nodeManager->mkNode(kind::AND, a, b);
+    d_cnfStream->ensureLiteral(a_and_b);
+    // Clauses are necessary to "literal-ize" a_and_b
+    TS_ASSERT( d_satSolver->addClauseCalled() );
+    TS_ASSERT( d_cnfStream->hasLiteral(a_and_b) );
+  }
+};
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index 48b9b2d35..fe922a6e1 100644
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -21,12 +21,15 @@
 #include <cxxtest/TestSuite.h>
 
 #include "theory/theory.h"
+#include "theory/theory_engine.h"
 #include "theory/arith/theory_arith.h"
 #include "theory/quantifiers_engine.h"
 #include "expr/node.h"
 #include "expr/node_manager.h"
 #include "context/context.h"
 #include "util/rational.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
 
 #include "theory/theory_test_utils.h"
 
@@ -38,6 +41,7 @@ using namespace CVC4::theory::arith;
 using namespace CVC4::expr;
 using namespace CVC4::context;
 using namespace CVC4::kind;
+using namespace CVC4::smt;
 
 using namespace std;
 
@@ -45,14 +49,15 @@ class TheoryArithWhite : public CxxTest::TestSuite {
 
   Context* d_ctxt;
   UserContext* d_uctxt;
+  ExprManager* d_em;
   NodeManager* d_nm;
-  NodeManagerScope* d_scope;
+  SmtScope* d_scope;
+  SmtEngine* d_smt;
 
   TestOutputChannel d_outputChannel;
   LogicInfo d_logicInfo;
   Theory::Effort d_level;
 
-  QuantifiersEngine* d_quantifiersEngine;
   TheoryArith* d_arith;
 
   TypeNode* d_booleanType;
@@ -96,14 +101,22 @@ public:
   }
 
   void setUp() {
-    d_ctxt = new Context();
-    d_uctxt = new UserContext();
-    d_nm = new NodeManager(d_ctxt, NULL);
-    d_scope = new NodeManagerScope(d_nm);
+    d_em = new ExprManager();
+    d_nm = NodeManager::fromExprManager(d_em);
+    d_smt = new SmtEngine(d_em);
+    d_ctxt = d_smt->d_context;
+    d_uctxt = d_smt->d_userContext;
+    d_scope = new SmtScope(d_smt);
     d_outputChannel.clear();
     d_logicInfo.lock();
-    d_quantifiersEngine = new QuantifiersEngine(d_ctxt, NULL);
-    d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), d_logicInfo, d_quantifiersEngine);
+
+    // guard against duplicate statistics assertion errors
+    delete d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH];
+    delete d_smt->d_theoryEngine->d_theoryOut[THEORY_ARITH];
+    d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH] = NULL;
+    d_smt->d_theoryEngine->d_theoryOut[THEORY_ARITH] = NULL;
+
+    d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), d_logicInfo, d_smt->d_theoryEngine->d_quantEngine);
 
     preregistered = new std::set<Node>();
 
@@ -119,12 +132,10 @@ public:
     delete preregistered;
 
     delete d_arith;
-    delete d_quantifiersEngine;
     d_outputChannel.clear();
     delete d_scope;
-    delete d_nm;
-    delete d_uctxt;
-    delete d_ctxt;
+    delete d_smt;
+    delete d_em;
   }
 
   void testAssert() {
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
deleted file mode 100644
index 74f5870a3..000000000
--- a/test/unit/theory/theory_black.h
+++ /dev/null
@@ -1,295 +0,0 @@
-/*********************                                                        */
-/*! \file theory_black.h
- ** \verbatim
- ** Original author: taking
- ** Major contributors: barrett, mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  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.\endverbatim
- **
- ** \brief Black box testing of CVC4::theory::Theory.
- **
- ** Black box testing of CVC4::theory::Theory.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include "theory/theory.h"
-#include "expr/node.h"
-#include "expr/node_manager.h"
-#include "context/context.h"
-
-#include <vector>
-
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::expr;
-using namespace CVC4::context;
-
-using namespace std;
-
-/**
- * Very basic OutputChannel for testing simple Theory Behaviour.
- * Stores a call sequence for the output channel
- */
-enum OutputChannelCallType{CONFLICT, PROPAGATE, LEMMA, EXPLANATION};
-class TestOutputChannel : public OutputChannel {
-private:
-  void push(OutputChannelCallType call, TNode n) {
-    d_callHistory.push_back(make_pair(call, n));
-  }
-
-public:
-  vector< pair<OutputChannelCallType, Node> > d_callHistory;
-
-  TestOutputChannel() {}
-
-  ~TestOutputChannel() {}
-
-  void safePoint() throw(Interrupted, AssertionException) {}
-
-  void conflict(TNode n)
-    throw(AssertionException) {
-    push(CONFLICT, n);
-  }
-
-  bool propagate(TNode n)
-    throw(AssertionException) {
-    push(PROPAGATE, n);
-    return true;
-  }
-
-  void propagateAsDecision(TNode n)
-    throw(AssertionException) {
-    // ignore
-  }
-
-  LemmaStatus lemma(TNode n, bool removable)
-    throw(AssertionException) {
-    push(LEMMA, n);
-    return LemmaStatus(Node::null(), 0);
-  }
-
-  void requirePhase(TNode, bool)
-    throw(Interrupted, AssertionException) {
-    Unreachable();
-  }
-
-  bool flipDecision()
-    throw(Interrupted, AssertionException) {
-    Unreachable();
-  }
-
-  void setIncomplete()
-    throw(AssertionException) {
-    Unreachable();
-  }
-
-  void clear() {
-    d_callHistory.clear();
-  }
-
-  Node getIthNode(int i) {
-    Node tmp = (d_callHistory[i]).second;
-    return tmp;
-  }
-
-  OutputChannelCallType getIthCallType(int i) {
-    return (d_callHistory[i]).first;
-  }
-
-  unsigned getNumCalls() {
-    return d_callHistory.size();
-  }
-};
-
-class DummyTheory : public Theory {
-public:
-  set<Node> d_registered;
-  vector<Node> d_getSequence;
-
-  DummyTheory(Context* ctxt, UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
-    Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo, qe) {
-  }
-
-  void registerTerm(TNode n) {
-    // check that we registerTerm() a term only once
-    TS_ASSERT(d_registered.find(n) == d_registered.end());
-
-    for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
-      // check that registerTerm() is called in reverse topological order
-      TS_ASSERT(d_registered.find(*i) != d_registered.end());
-    }
-
-    d_registered.insert(n);
-  }
-
-  Node getWrapper() {
-    Node n = get();
-    d_getSequence.push_back(n);
-    return n;
-  }
-
-  bool doneWrapper() {
-    return done();
-  }
-
-  void check(Effort e) {
-    while(!done()) {
-      getWrapper();
-    }
-  }
-
-  void presolve() {
-    Unimplemented();
-  }
-  void preRegisterTerm(TNode n) {}
-  void propagate(Effort level) {}
-  void explain(TNode n, Effort level) {}
-  Node getValue(TNode n) { return Node::null(); }
-  string identify() const { return "DummyTheory"; }
-};/* class DummyTheory */
-
-class TheoryBlack : public CxxTest::TestSuite {
-
-  Context* d_ctxt;
-  UserContext* d_uctxt;
-  NodeManager* d_nm;
-  NodeManagerScope* d_scope;
-  LogicInfo* d_logicInfo;
-
-  TestOutputChannel d_outputChannel;
-
-  DummyTheory* d_dummy;
-
-  Node atom0;
-  Node atom1;
-
-public:
-
-  void setUp() {
-    d_ctxt = new Context();
-    d_uctxt = new UserContext();
-    d_nm = new NodeManager(d_ctxt, NULL);
-    d_scope = new NodeManagerScope(d_nm);
-    d_logicInfo = new LogicInfo();
-    d_logicInfo->lock();
-    d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), *d_logicInfo, NULL);
-    d_outputChannel.clear();
-    atom0 = d_nm->mkConst(true);
-    atom1 = d_nm->mkConst(false);
-  }
-
-  void tearDown() {
-    atom1 = Node::null();
-    atom0 = Node::null();
-    delete d_dummy;
-    delete d_logicInfo;
-    delete d_scope;
-    delete d_nm;
-    delete d_uctxt;
-    delete d_ctxt;
-  }
-
-  void testEffort(){
-    Theory::Effort s = Theory::EFFORT_STANDARD;
-    Theory::Effort f = Theory::EFFORT_FULL;
-
-    TS_ASSERT( Theory::standardEffortOnly(s));
-    TS_ASSERT(!Theory::standardEffortOnly(f));
-
-    TS_ASSERT(!Theory::fullEffort(s));
-    TS_ASSERT( Theory::fullEffort(f));
-
-    TS_ASSERT( Theory::standardEffortOrMore(s));
-    TS_ASSERT( Theory::standardEffortOrMore(f));
-  }
-
-  void testDone() {
-    TS_ASSERT(d_dummy->doneWrapper());
-
-    d_dummy->assertFact(atom0, true);
-    d_dummy->assertFact(atom1, true);
-
-    TS_ASSERT(!d_dummy->doneWrapper());
-
-    d_dummy->check(Theory::EFFORT_FULL);
-
-    TS_ASSERT(d_dummy->doneWrapper());
-  }
-
-  // FIXME: move this to theory_engine test?
-//   void testRegisterTerm() {
-//     TS_ASSERT(d_dummy->doneWrapper());
-
-//     TypeNode typeX = d_nm->booleanType();
-//     TypeNode typeF = d_nm->mkFunctionType(typeX, typeX);
-
-//     Node x = d_nm->mkVar("x",typeX);
-//     Node f = d_nm->mkVar("f",typeF);
-//     Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
-//     Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
-//     Node f_x_eq_x = f_x.eqNode(x);
-//     Node x_eq_f_f_x = x.eqNode(f_f_x);
-
-//     d_dummy->assertFact(f_x_eq_x);
-//     d_dummy->assertFact(x_eq_f_f_x);
-
-//     Node got = d_dummy->getWrapper();
-
-//     TS_ASSERT_EQUALS(got, f_x_eq_x);
-
-//     TS_ASSERT_EQUALS(5u, d_dummy->d_registered.size());
-//     TS_ASSERT(d_dummy->d_registered.find(x) != d_dummy->d_registered.end());
-//     TS_ASSERT(d_dummy->d_registered.find(f) != d_dummy->d_registered.end());
-//     TS_ASSERT(d_dummy->d_registered.find(f_x) != d_dummy->d_registered.end());
-//     TS_ASSERT(d_dummy->d_registered.find(f_x_eq_x) != d_dummy->d_registered.end());
-//     TS_ASSERT(d_dummy->d_registered.find(d_nm->operatorOf(kind::EQUAL)) != d_dummy->d_registered.end());
-//     TS_ASSERT(d_dummy->d_registered.find(f_f_x) == d_dummy->d_registered.end());
-//     TS_ASSERT(d_dummy->d_registered.find(x_eq_f_f_x) == d_dummy->d_registered.end());
-
-//     TS_ASSERT(!d_dummy->doneWrapper());
-
-//     got = d_dummy->getWrapper();
-
-//     TS_ASSERT_EQUALS(got, x_eq_f_f_x);
-
-//     TS_ASSERT_EQUALS(7u, d_dummy->d_registered.size());
-//     TS_ASSERT(d_dummy->d_registered.find(f_f_x) != d_dummy->d_registered.end());
-//     TS_ASSERT(d_dummy->d_registered.find(x_eq_f_f_x) != d_dummy->d_registered.end());
-
-//     TS_ASSERT(d_dummy->doneWrapper());
-//   }
-
-  void testOutputChannelAccessors() {
-    /* void setOutputChannel(OutputChannel& out)  */
-    /* OutputChannel& getOutputChannel() */
-
-    TestOutputChannel theOtherChannel;
-
-    TS_ASSERT_EQUALS(&(d_dummy->getOutputChannel()), &d_outputChannel);
-
-    d_dummy->setOutputChannel(theOtherChannel);
-
-    TS_ASSERT_EQUALS(&(d_dummy->getOutputChannel()), &theOtherChannel);
-
-    const OutputChannel& oc = d_dummy->getOutputChannel();
-
-    TS_ASSERT_EQUALS(&oc, &theOtherChannel);
-  }
-
-  void testOutputChannel() {
-    Node n = atom0.orNode(atom1);
-    d_outputChannel.lemma(n, false);
-    d_outputChannel.split(atom0);
-    Node s = atom0.orNode(atom0.notNode());
-    TS_ASSERT_EQUALS(d_outputChannel.d_callHistory.size(), 2u);
-    TS_ASSERT_EQUALS(d_outputChannel.d_callHistory[0], make_pair(LEMMA, n));
-    TS_ASSERT_EQUALS(d_outputChannel.d_callHistory[1], make_pair(LEMMA, s));
-    d_outputChannel.d_callHistory.clear();
-  }
-};
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index ae61bd0d3..ee637daac 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -34,6 +34,8 @@
 #include "expr/node_manager.h"
 #include "expr/kind.h"
 #include "context/context.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
 #include "util/rational.h"
 #include "util/integer.h"
 #include "util/options.h"
@@ -44,6 +46,7 @@ using namespace CVC4::theory;
 using namespace CVC4::expr;
 using namespace CVC4::context;
 using namespace CVC4::kind;
+using namespace CVC4::smt;
 
 using namespace std;
 
@@ -233,49 +236,47 @@ class TheoryEngineWhite : public CxxTest::TestSuite {
   Context* d_ctxt;
   UserContext* d_uctxt;
 
+  ExprManager* d_em;
   NodeManager* d_nm;
-  NodeManagerScope* d_scope;
+  SmtEngine* d_smt;
+  SmtScope* d_scope;
   FakeOutputChannel *d_nullChannel;
   TheoryEngine* d_theoryEngine;
-  LogicInfo* d_logicInfo;
 
 public:
 
   void setUp() {
-    d_ctxt = new Context();
-    d_uctxt = new UserContext();
+    d_em = new ExprManager();
+    d_smt = new SmtEngine(d_em);
+    d_nm = NodeManager::fromExprManager(d_em);
+    d_scope = new SmtScope(d_smt);
 
-    d_nm = new NodeManager(d_ctxt, NULL);
-    d_scope = new NodeManagerScope(d_nm);
+    d_ctxt = d_smt->d_context;
+    d_uctxt = d_smt->d_userContext;
 
     d_nullChannel = new FakeOutputChannel();
 
-    // create the TheoryEngine
-    d_logicInfo = new LogicInfo();
-    d_theoryEngine = new TheoryEngine(d_ctxt, d_uctxt, *d_logicInfo);
-
+    d_theoryEngine = d_smt->d_theoryEngine;
+    for(TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++id) {
+      delete d_theoryEngine->d_theoryOut[id];
+      delete d_theoryEngine->d_theoryTable[id];
+      d_theoryEngine->d_theoryOut[id] = NULL;
+      d_theoryEngine->d_theoryTable[id] = NULL;
+    }
     d_theoryEngine->addTheory< FakeTheory<THEORY_BUILTIN> >(THEORY_BUILTIN);
     d_theoryEngine->addTheory< FakeTheory<THEORY_BOOL> >(THEORY_BOOL);
     d_theoryEngine->addTheory< FakeTheory<THEORY_UF> >(THEORY_UF);
     d_theoryEngine->addTheory< FakeTheory<THEORY_ARITH> >(THEORY_ARITH);
     d_theoryEngine->addTheory< FakeTheory<THEORY_ARRAY> >(THEORY_ARRAY);
     d_theoryEngine->addTheory< FakeTheory<THEORY_BV> >(THEORY_BV);
-
-    //Debug.on("theory-rewrite");
   }
 
   void tearDown() {
-    d_theoryEngine->shutdown();
-    delete d_theoryEngine;
-    delete d_logicInfo;
-
     delete d_nullChannel;
 
     delete d_scope;
-    delete d_nm;
-
-    delete d_uctxt;
-    delete d_ctxt;
+    delete d_smt;
+    delete d_em;
   }
 
   void testRewriterSimple() {
diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
new file mode 100644
index 000000000..5b46aee4f
--- /dev/null
+++ b/test/unit/theory/theory_white.h
@@ -0,0 +1,309 @@
+/*********************                                                        */
+/*! \file theory_black.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: barrett, mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  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.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::theory::Theory.
+ **
+ ** Black box testing of CVC4::theory::Theory.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "theory/theory.h"
+#include "theory/theory_engine.h"
+#include "expr/node.h"
+#include "expr/node_manager.h"
+#include "context/context.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+
+#include <vector>
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::expr;
+using namespace CVC4::context;
+using namespace CVC4::smt;
+
+using namespace std;
+
+/**
+ * Very basic OutputChannel for testing simple Theory Behaviour.
+ * Stores a call sequence for the output channel
+ */
+enum OutputChannelCallType{CONFLICT, PROPAGATE, LEMMA, EXPLANATION};
+class TestOutputChannel : public OutputChannel {
+private:
+  void push(OutputChannelCallType call, TNode n) {
+    d_callHistory.push_back(make_pair(call, n));
+  }
+
+public:
+  vector< pair<OutputChannelCallType, Node> > d_callHistory;
+
+  TestOutputChannel() {}
+
+  ~TestOutputChannel() {}
+
+  void safePoint() throw(Interrupted, AssertionException) {}
+
+  void conflict(TNode n)
+    throw(AssertionException) {
+    push(CONFLICT, n);
+  }
+
+  bool propagate(TNode n)
+    throw(AssertionException) {
+    push(PROPAGATE, n);
+    return true;
+  }
+
+  void propagateAsDecision(TNode n)
+    throw(AssertionException) {
+    // ignore
+  }
+
+  LemmaStatus lemma(TNode n, bool removable)
+    throw(AssertionException) {
+    push(LEMMA, n);
+    return LemmaStatus(Node::null(), 0);
+  }
+
+  void requirePhase(TNode, bool)
+    throw(Interrupted, AssertionException) {
+    Unreachable();
+  }
+
+  bool flipDecision()
+    throw(Interrupted, AssertionException) {
+    Unreachable();
+  }
+
+  void setIncomplete()
+    throw(AssertionException) {
+    Unreachable();
+  }
+
+  void clear() {
+    d_callHistory.clear();
+  }
+
+  Node getIthNode(int i) {
+    Node tmp = (d_callHistory[i]).second;
+    return tmp;
+  }
+
+  OutputChannelCallType getIthCallType(int i) {
+    return (d_callHistory[i]).first;
+  }
+
+  unsigned getNumCalls() {
+    return d_callHistory.size();
+  }
+};
+
+class DummyTheory : public Theory {
+public:
+  set<Node> d_registered;
+  vector<Node> d_getSequence;
+
+  DummyTheory(Context* ctxt, UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
+    Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo, qe) {
+  }
+
+  void registerTerm(TNode n) {
+    // check that we registerTerm() a term only once
+    TS_ASSERT(d_registered.find(n) == d_registered.end());
+
+    for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
+      // check that registerTerm() is called in reverse topological order
+      TS_ASSERT(d_registered.find(*i) != d_registered.end());
+    }
+
+    d_registered.insert(n);
+  }
+
+  Node getWrapper() {
+    Node n = get();
+    d_getSequence.push_back(n);
+    return n;
+  }
+
+  bool doneWrapper() {
+    return done();
+  }
+
+  void check(Effort e) {
+    while(!done()) {
+      getWrapper();
+    }
+  }
+
+  void presolve() {
+    Unimplemented();
+  }
+  void preRegisterTerm(TNode n) {}
+  void propagate(Effort level) {}
+  void explain(TNode n, Effort level) {}
+  Node getValue(TNode n) { return Node::null(); }
+  string identify() const { return "DummyTheory"; }
+};/* class DummyTheory */
+
+class TheoryBlack : public CxxTest::TestSuite {
+
+  Context* d_ctxt;
+  UserContext* d_uctxt;
+  NodeManager* d_nm;
+  ExprManager* d_em;
+  SmtScope* d_scope;
+  SmtEngine* d_smt;
+  LogicInfo* d_logicInfo;
+
+  TestOutputChannel d_outputChannel;
+
+  DummyTheory* d_dummy;
+
+  Node atom0;
+  Node atom1;
+
+public:
+
+  void setUp() {
+    d_em = new ExprManager();
+    d_nm = NodeManager::fromExprManager(d_em);
+    d_smt = new SmtEngine(d_em);
+    d_ctxt = d_smt->d_context;
+    d_uctxt = d_smt->d_userContext;
+    d_scope = new SmtScope(d_smt);
+    d_logicInfo = new LogicInfo();
+    d_logicInfo->lock();
+
+    // guard against duplicate statistics assertion errors
+    delete d_smt->d_theoryEngine->d_theoryTable[THEORY_BUILTIN];
+    delete d_smt->d_theoryEngine->d_theoryOut[THEORY_BUILTIN];
+    d_smt->d_theoryEngine->d_theoryTable[THEORY_BUILTIN] = NULL;
+    d_smt->d_theoryEngine->d_theoryOut[THEORY_BUILTIN] = NULL;
+
+    d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), *d_logicInfo, NULL);
+    d_outputChannel.clear();
+    atom0 = d_nm->mkConst(true);
+    atom1 = d_nm->mkConst(false);
+  }
+
+  void tearDown() {
+    atom1 = Node::null();
+    atom0 = Node::null();
+    delete d_dummy;
+    delete d_logicInfo;
+    delete d_scope;
+    delete d_smt;
+    delete d_em;
+  }
+
+  void testEffort(){
+    Theory::Effort s = Theory::EFFORT_STANDARD;
+    Theory::Effort f = Theory::EFFORT_FULL;
+
+    TS_ASSERT( Theory::standardEffortOnly(s));
+    TS_ASSERT(!Theory::standardEffortOnly(f));
+
+    TS_ASSERT(!Theory::fullEffort(s));
+    TS_ASSERT( Theory::fullEffort(f));
+
+    TS_ASSERT( Theory::standardEffortOrMore(s));
+    TS_ASSERT( Theory::standardEffortOrMore(f));
+  }
+
+  void testDone() {
+    TS_ASSERT(d_dummy->doneWrapper());
+
+    d_dummy->assertFact(atom0, true);
+    d_dummy->assertFact(atom1, true);
+
+    TS_ASSERT(!d_dummy->doneWrapper());
+
+    d_dummy->check(Theory::EFFORT_FULL);
+
+    TS_ASSERT(d_dummy->doneWrapper());
+  }
+
+  // FIXME: move this to theory_engine test?
+//   void testRegisterTerm() {
+//     TS_ASSERT(d_dummy->doneWrapper());
+
+//     TypeNode typeX = d_nm->booleanType();
+//     TypeNode typeF = d_nm->mkFunctionType(typeX, typeX);
+
+//     Node x = d_nm->mkVar("x",typeX);
+//     Node f = d_nm->mkVar("f",typeF);
+//     Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
+//     Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
+//     Node f_x_eq_x = f_x.eqNode(x);
+//     Node x_eq_f_f_x = x.eqNode(f_f_x);
+
+//     d_dummy->assertFact(f_x_eq_x);
+//     d_dummy->assertFact(x_eq_f_f_x);
+
+//     Node got = d_dummy->getWrapper();
+
+//     TS_ASSERT_EQUALS(got, f_x_eq_x);
+
+//     TS_ASSERT_EQUALS(5u, d_dummy->d_registered.size());
+//     TS_ASSERT(d_dummy->d_registered.find(x) != d_dummy->d_registered.end());
+//     TS_ASSERT(d_dummy->d_registered.find(f) != d_dummy->d_registered.end());
+//     TS_ASSERT(d_dummy->d_registered.find(f_x) != d_dummy->d_registered.end());
+//     TS_ASSERT(d_dummy->d_registered.find(f_x_eq_x) != d_dummy->d_registered.end());
+//     TS_ASSERT(d_dummy->d_registered.find(d_nm->operatorOf(kind::EQUAL)) != d_dummy->d_registered.end());
+//     TS_ASSERT(d_dummy->d_registered.find(f_f_x) == d_dummy->d_registered.end());
+//     TS_ASSERT(d_dummy->d_registered.find(x_eq_f_f_x) == d_dummy->d_registered.end());
+
+//     TS_ASSERT(!d_dummy->doneWrapper());
+
+//     got = d_dummy->getWrapper();
+
+//     TS_ASSERT_EQUALS(got, x_eq_f_f_x);
+
+//     TS_ASSERT_EQUALS(7u, d_dummy->d_registered.size());
+//     TS_ASSERT(d_dummy->d_registered.find(f_f_x) != d_dummy->d_registered.end());
+//     TS_ASSERT(d_dummy->d_registered.find(x_eq_f_f_x) != d_dummy->d_registered.end());
+
+//     TS_ASSERT(d_dummy->doneWrapper());
+//   }
+
+  void testOutputChannelAccessors() {
+    /* void setOutputChannel(OutputChannel& out)  */
+    /* OutputChannel& getOutputChannel() */
+
+    TestOutputChannel theOtherChannel;
+
+    TS_ASSERT_EQUALS(&(d_dummy->getOutputChannel()), &d_outputChannel);
+
+    d_dummy->setOutputChannel(theOtherChannel);
+
+    TS_ASSERT_EQUALS(&(d_dummy->getOutputChannel()), &theOtherChannel);
+
+    const OutputChannel& oc = d_dummy->getOutputChannel();
+
+    TS_ASSERT_EQUALS(&oc, &theOtherChannel);
+  }
+
+  void testOutputChannel() {
+    Node n = atom0.orNode(atom1);
+    d_outputChannel.lemma(n, false);
+    d_outputChannel.split(atom0);
+    Node s = atom0.orNode(atom0.notNode());
+    TS_ASSERT_EQUALS(d_outputChannel.d_callHistory.size(), 2u);
+    TS_ASSERT_EQUALS(d_outputChannel.d_callHistory[0], make_pair(LEMMA, n));
+    TS_ASSERT_EQUALS(d_outputChannel.d_callHistory[1], make_pair(LEMMA, s));
+    d_outputChannel.d_callHistory.clear();
+  }
+};