1 files changed, 11 insertions, 47 deletions

diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index f14788ed5..3e479e0f9 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -27,8 +27,8 @@
 #include "context/cdlist.h"
 #include "context/cdhashmap.h"
 #include "expr/node.h"
-#include "expr/statistics_registry.h"
 #include "util/ntuple.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
@@ -163,54 +163,18 @@ public:
     d_callsMergeInfo("theory::arrays::callsMergeInfo",0),
     d_maxList("theory::arrays::maxList",0),
     d_tableSize("theory::arrays::infoTableSize", info_map) {
-  StatisticsRegistry::registerStat(&d_mergeInfoTimer);
-  StatisticsRegistry::registerStat(&d_avgIndexListLength);
-  StatisticsRegistry::registerStat(&d_avgStoresListLength);
-  StatisticsRegistry::registerStat(&d_avgInStoresListLength);
-  StatisticsRegistry::registerStat(&d_listsCount);
-  StatisticsRegistry::registerStat(&d_callsMergeInfo);
-  StatisticsRegistry::registerStat(&d_maxList);
-  StatisticsRegistry::registerStat(&d_tableSize);
+  currentStatisticsRegistry()->registerStat(&d_mergeInfoTimer);
+  currentStatisticsRegistry()->registerStat(&d_avgIndexListLength);
+  currentStatisticsRegistry()->registerStat(&d_avgStoresListLength);
+  currentStatisticsRegistry()->registerStat(&d_avgInStoresListLength);
+  currentStatisticsRegistry()->registerStat(&d_listsCount);
+  currentStatisticsRegistry()->registerStat(&d_callsMergeInfo);
+  currentStatisticsRegistry()->registerStat(&d_maxList);
+  currentStatisticsRegistry()->registerStat(&d_tableSize);
   }*/
-  ArrayInfo(context::Context* c, Backtracker<TNode>* b): ct(c), bck(b), info_map(),
-      d_mergeInfoTimer("theory::arrays::mergeInfoTimer"),
-      d_avgIndexListLength("theory::arrays::avgIndexListLength"),
-      d_avgStoresListLength("theory::arrays::avgStoresListLength"),
-      d_avgInStoresListLength("theory::arrays::avgInStoresListLength"),
-      d_listsCount("theory::arrays::listsCount",0),
-      d_callsMergeInfo("theory::arrays::callsMergeInfo",0),
-      d_maxList("theory::arrays::maxList",0),
-      d_tableSize("theory::arrays::infoTableSize", info_map) {
-    emptyList = new(true) CTNodeList(ct);
-    emptyInfo = new Info(ct, bck);
-    StatisticsRegistry::registerStat(&d_mergeInfoTimer);
-    StatisticsRegistry::registerStat(&d_avgIndexListLength);
-    StatisticsRegistry::registerStat(&d_avgStoresListLength);
-    StatisticsRegistry::registerStat(&d_avgInStoresListLength);
-    StatisticsRegistry::registerStat(&d_listsCount);
-    StatisticsRegistry::registerStat(&d_callsMergeInfo);
-    StatisticsRegistry::registerStat(&d_maxList);
-    StatisticsRegistry::registerStat(&d_tableSize);
-  }
+  ArrayInfo(context::Context* c, Backtracker<TNode>* b);
 
-  ~ArrayInfo() {
-    CNodeInfoMap::iterator it = info_map.begin();
-    for( ; it != info_map.end(); it++ ) {
-      if((*it).second!= emptyInfo) {
-        delete (*it).second;
-      }
-    }
-    emptyList->deleteSelf();
-    delete emptyInfo;
-    StatisticsRegistry::unregisterStat(&d_mergeInfoTimer);
-    StatisticsRegistry::unregisterStat(&d_avgIndexListLength);
-    StatisticsRegistry::unregisterStat(&d_avgStoresListLength);
-    StatisticsRegistry::unregisterStat(&d_avgInStoresListLength);
-    StatisticsRegistry::unregisterStat(&d_listsCount);
-    StatisticsRegistry::unregisterStat(&d_callsMergeInfo);
-    StatisticsRegistry::unregisterStat(&d_maxList);
-    StatisticsRegistry::unregisterStat(&d_tableSize);
-  };
+  ~ArrayInfo();
 
   /**
    * adds the node a to the map if it does not exist