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).

20 files changed, 264 insertions, 128 deletions

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_white.h
index 70c306a6d..cc7ea9bf6 100644
--- a/test/unit/prop/cnf_stream_black.h
+++ b/test/unit/prop/cnf_stream_white.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file cnf_stream_black.h
+/*! \file cnf_stream_white.h
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: mdeters
@@ -22,7 +22,6 @@
 
 #include "util/Assert.h"
 
-
 #include "expr/expr_manager.h"
 #include "expr/node_manager.h"
 #include "context/context.h"
@@ -30,6 +29,7 @@
 #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"
@@ -42,6 +42,8 @@
 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. */
@@ -118,19 +120,13 @@ public:
 
 };/* class FakeSatSolver */
 
-class CnfStreamBlack : public CxxTest::TestSuite {
+class CnfStreamWhite : 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;
 
@@ -143,31 +139,32 @@ class CnfStreamBlack : public CxxTest::TestSuite {
   /** The node manager */
   NodeManager* d_nodeManager;
 
+  ExprManager* d_exprManager;
+  SmtScope* d_scope;
+  SmtEngine* d_smt;
+
   void setUp() {
-    d_context = new Context();
-    d_userContext = new UserContext();
-    d_nodeManager = new NodeManager(d_context, NULL);
-    NodeManagerScope nms(d_nodeManager);
+    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_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;
+    delete d_scope;
+    delete d_smt;
+    delete d_exprManager;
   }
 
 public:
@@ -291,8 +288,7 @@ public:
     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...
+    // 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_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_black.h b/test/unit/theory/theory_white.h
index 74f5870a3..5b46aee4f 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_white.h
@@ -19,9 +19,12 @@
 #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>
 
@@ -29,6 +32,7 @@ using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::expr;
 using namespace CVC4::context;
+using namespace CVC4::smt;
 
 using namespace std;
 
@@ -159,7 +163,9 @@ class TheoryBlack : public CxxTest::TestSuite {
   Context* d_ctxt;
   UserContext* d_uctxt;
   NodeManager* d_nm;
-  NodeManagerScope* d_scope;
+  ExprManager* d_em;
+  SmtScope* d_scope;
+  SmtEngine* d_smt;
   LogicInfo* d_logicInfo;
 
   TestOutputChannel d_outputChannel;
@@ -172,12 +178,21 @@ class TheoryBlack : public CxxTest::TestSuite {
 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_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);
@@ -190,9 +205,8 @@ public:
     delete d_dummy;
     delete d_logicInfo;
     delete d_scope;
-    delete d_nm;
-    delete d_uctxt;
-    delete d_ctxt;
+    delete d_smt;
+    delete d_em;
   }
 
   void testEffort(){