1 files changed, 7 insertions, 29 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index adc4daeee..7cb15ca97 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -26,7 +26,6 @@
 #include "base/cvc4_assert.h"
 #include "context/cdhashset.h"
 #include "expr/node.h"
-#include "expr/statistics_registry.h"
 #include "options/options.h"
 #include "options/smt_options.h"
 #include "prop/prop_engine.h"
@@ -44,6 +43,7 @@
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/valuation.h"
+#include "util/statistics_registry.h"
 #include "util/unsafe_interrupt_exception.h"
 
 namespace CVC4 {
@@ -225,30 +225,8 @@ class TheoryEngine {
 
     IntStat conflicts, propagations, lemmas, requirePhase, flipDecision, restartDemands;
 
-    Statistics(theory::TheoryId theory):
-      conflicts(mkName("theory<", theory, ">::conflicts"), 0),
-      propagations(mkName("theory<", theory, ">::propagations"), 0),
-      lemmas(mkName("theory<", theory, ">::lemmas"), 0),
-      requirePhase(mkName("theory<", theory, ">::requirePhase"), 0),
-      flipDecision(mkName("theory<", theory, ">::flipDecision"), 0),
-      restartDemands(mkName("theory<", theory, ">::restartDemands"), 0)
-    {
-      StatisticsRegistry::registerStat(&conflicts);
-      StatisticsRegistry::registerStat(&propagations);
-      StatisticsRegistry::registerStat(&lemmas);
-      StatisticsRegistry::registerStat(&requirePhase);
-      StatisticsRegistry::registerStat(&flipDecision);
-      StatisticsRegistry::registerStat(&restartDemands);
-    }
-
-    ~Statistics() {
-      StatisticsRegistry::unregisterStat(&conflicts);
-      StatisticsRegistry::unregisterStat(&propagations);
-      StatisticsRegistry::unregisterStat(&lemmas);
-      StatisticsRegistry::unregisterStat(&requirePhase);
-      StatisticsRegistry::unregisterStat(&flipDecision);
-      StatisticsRegistry::unregisterStat(&restartDemands);
-    }
+    Statistics(theory::TheoryId theory);
+    ~Statistics();
   };/* class TheoryEngine::Statistics */
 
 
@@ -764,7 +742,7 @@ public:
   inline bool isTheoryEnabled(theory::TheoryId theoryId) const {
     return d_logicInfo.isTheoryEnabled(theoryId);
   }
-  
+
   /**
    * Returns the equality status of the two terms, from the theory
    * that owns the domain type.  The types of a and b must be the same.
@@ -791,7 +769,7 @@ public:
    * Print solution for synthesis conjectures found by ce_guided_instantiation module
    */
   void printSynthSolution( std::ostream& out );
-  
+
   /**
    * Forwards an entailment check according to the given theoryOfMode.
    * See theory.h for documentation on entailmentCheck().
@@ -835,11 +813,11 @@ public:
   SharedTermsDatabase* getSharedTermsDatabase() { return &d_sharedTerms; }
 
   theory::eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; }
-  
+
   RemoveITE* getIteRemover() { return &d_iteRemover; }
 
   SortInference* getSortInference() { return &d_sortInfer; }
-  
+
   /** Prints the assertions to the debug stream */
   void printAssertions(const char* tag);