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

3 files changed, 19 insertions, 11 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>