Removing StatisticsRegistry's static functions current() and registerStat().

- The functionality the get the StatisticsRegistry attached to the SmtEngine was previously through StatisticsRegistry::current(). This is the dominant StatisticsRegistry in the code. (There is another StatisticsRegistry attached to the NodeManager.) Having this be a static function on StatisticsRegistry requires the use of an SmtEngine in the wrong compilation unit.
- Usages of StatisticsRegistry::current() that were visible in prop/{bvminisat,minisat} has been removed. A pointer to the relevant StatisticsRegistry should be passed instead into the constructor.
- The function StatisticsRegistry::current() has been replaced by SmtScope::currentStatisticsRegistry(). SmtScope is in the libcvc4 package, where SmtEngine is available in the compilation unit.
- The function smtStatisticsRegistry() is a synonym for SmtScope::currentStatisticsRegistry() in smt/smt_statistics_registry.h. This header has fewer include dependencies than the one for SmtScope.
- Correspondingly, the static functions StatisticsRegistry::{registerStat, unregisterStat} have been removed. One should instead use smtStatisticsRegistry()->{registerStat,unregisterStat} instead.
- The KEEP_STATISTIC macro has been moved into smt/smt_statistics_registry.h.
- Documents the reason StatisticsRegistry is CVC4_PUBLIC. This lets me remove the warning I added.
- Removing most operators for timespec from statistics_registry.h file. These a bit error prone in clang.
- Most of the really confusing ifdef's in util/statistics_registry.h are gone.

5 files changed, 44 insertions, 38 deletions

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index cd6459a3c..828d53144 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -17,10 +17,32 @@
 
 #include "theory/uf/equality_engine.h"
 
+#include "smt/smt_statistics_registry.h"
+
 namespace CVC4 {
 namespace theory {
 namespace eq {
 
+EqualityEngine::Statistics::Statistics(std::string name)
+    : mergesCount(name + "::mergesCount", 0),
+      termsCount(name + "::termsCount", 0),
+      functionTermsCount(name + "::functionTermsCount", 0),
+      constantTermsCount(name + "::constantTermsCount", 0)
+{
+  smtStatisticsRegistry()->registerStat(&mergesCount);
+  smtStatisticsRegistry()->registerStat(&termsCount);
+  smtStatisticsRegistry()->registerStat(&functionTermsCount);
+  smtStatisticsRegistry()->registerStat(&constantTermsCount);
+}
+
+EqualityEngine::Statistics::~Statistics() {
+  smtStatisticsRegistry()->unregisterStat(&mergesCount);
+  smtStatisticsRegistry()->unregisterStat(&termsCount);
+  smtStatisticsRegistry()->unregisterStat(&functionTermsCount);
+  smtStatisticsRegistry()->unregisterStat(&constantTermsCount);
+}
+
+
 /**
  * Data used in the BFS search through the equality graph.
  */
@@ -2058,4 +2080,3 @@ void EqProof::debug_print( const char * c, unsigned tb ){
 } // Namespace uf
 } // Namespace theory
 } // Namespace CVC4
-
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index f7f7f9ddd..87074aebc 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -29,10 +29,10 @@
 #include "context/cdo.h"
 #include "expr/kind_map.h"
 #include "expr/node.h"
-#include "expr/statistics_registry.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine_types.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
@@ -193,24 +193,9 @@ public:
     /** Number of constant terms managed by the system */
     IntStat constantTermsCount;
 
-    Statistics(std::string name)
-    : mergesCount(name + "::mergesCount", 0),
-      termsCount(name + "::termsCount", 0),
-      functionTermsCount(name + "::functionTermsCount", 0),
-      constantTermsCount(name + "::constantTermsCount", 0)
-    {
-      StatisticsRegistry::registerStat(&mergesCount);
-      StatisticsRegistry::registerStat(&termsCount);
-      StatisticsRegistry::registerStat(&functionTermsCount);
-      StatisticsRegistry::registerStat(&constantTermsCount);
-    }
+    Statistics(std::string name);
 
-    ~Statistics() {
-      StatisticsRegistry::unregisterStat(&mergesCount);
-      StatisticsRegistry::unregisterStat(&termsCount);
-      StatisticsRegistry::unregisterStat(&functionTermsCount);
-      StatisticsRegistry::unregisterStat(&constantTermsCount);
-    }
+    ~Statistics();
   };/* struct EqualityEngine::statistics */
 
 private:
@@ -900,4 +885,3 @@ public:
 } // Namespace eq
 } // Namespace theory
 } // Namespace CVC4
-
diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h
index e49b4652a..763ced650 100644
--- a/src/theory/uf/symmetry_breaker.h
+++ b/src/theory/uf/symmetry_breaker.h
@@ -52,7 +52,8 @@
 #include "context/context.h"
 #include "expr/node.h"
 #include "expr/node_builder.h"
-#include "expr/statistics_registry.h"
+#include "smt/smt_statistics_registry.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 0f8ccf49a..9fceedc96 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -2058,23 +2058,23 @@ StrongSolverTheoryUF::Statistics::Statistics():
   d_totality_lemmas("StrongSolverTheoryUF::Totality_Lemmas", 0),
   d_max_model_size("StrongSolverTheoryUF::Max_Model_Size", 1)
 {
-  StatisticsRegistry::registerStat(&d_clique_conflicts);
-  StatisticsRegistry::registerStat(&d_clique_lemmas);
-  StatisticsRegistry::registerStat(&d_split_lemmas);
-  StatisticsRegistry::registerStat(&d_disamb_term_lemmas);
-  StatisticsRegistry::registerStat(&d_sym_break_lemmas);
-  StatisticsRegistry::registerStat(&d_totality_lemmas);
-  StatisticsRegistry::registerStat(&d_max_model_size);
+  smtStatisticsRegistry()->registerStat(&d_clique_conflicts);
+  smtStatisticsRegistry()->registerStat(&d_clique_lemmas);
+  smtStatisticsRegistry()->registerStat(&d_split_lemmas);
+  smtStatisticsRegistry()->registerStat(&d_disamb_term_lemmas);
+  smtStatisticsRegistry()->registerStat(&d_sym_break_lemmas);
+  smtStatisticsRegistry()->registerStat(&d_totality_lemmas);
+  smtStatisticsRegistry()->registerStat(&d_max_model_size);
 }
 
 StrongSolverTheoryUF::Statistics::~Statistics(){
-  StatisticsRegistry::unregisterStat(&d_clique_conflicts);
-  StatisticsRegistry::unregisterStat(&d_clique_lemmas);
-  StatisticsRegistry::unregisterStat(&d_split_lemmas);
-  StatisticsRegistry::unregisterStat(&d_disamb_term_lemmas);
-  StatisticsRegistry::unregisterStat(&d_sym_break_lemmas);
-  StatisticsRegistry::unregisterStat(&d_totality_lemmas);
-  StatisticsRegistry::unregisterStat(&d_max_model_size);
+  smtStatisticsRegistry()->unregisterStat(&d_clique_conflicts);
+  smtStatisticsRegistry()->unregisterStat(&d_clique_lemmas);
+  smtStatisticsRegistry()->unregisterStat(&d_split_lemmas);
+  smtStatisticsRegistry()->unregisterStat(&d_disamb_term_lemmas);
+  smtStatisticsRegistry()->unregisterStat(&d_sym_break_lemmas);
+  smtStatisticsRegistry()->unregisterStat(&d_totality_lemmas);
+  smtStatisticsRegistry()->unregisterStat(&d_max_model_size);
 }
 
 
@@ -2141,9 +2141,9 @@ void DisequalityPropagator::assertPredicate( Node p, bool polarity ) {
 DisequalityPropagator::Statistics::Statistics():
    d_propagations("StrongSolverTheoryUF::Disequality_Propagations", 0)
 {
-  StatisticsRegistry::registerStat(& d_propagations);
+  smtStatisticsRegistry()->registerStat(& d_propagations);
 }
 
 DisequalityPropagator::Statistics::~Statistics(){
-  StatisticsRegistry::unregisterStat(& d_propagations);
+  smtStatisticsRegistry()->unregisterStat(& d_propagations);
 }
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index 45d7fc3cc..24d7f840f 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -21,8 +21,8 @@
 #include "context/cdhashmap.h"
 #include "context/context.h"
 #include "context/context_mm.h"
-#include "expr/statistics_registry.h"
 #include "theory/theory.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {