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.

8 files changed, 12 insertions, 13 deletions

diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index df9c9e19f..7b6c2fab5 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -19,10 +19,10 @@
 #include <string>
 
 #include "expr/expr_manager.h"
-#include "expr/statistics_registry.h"
 #include "options/options.h"
 #include "smt/smt_engine.h"
 #include "smt_util/command.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace main {
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index cdd20c05a..9d0042694 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -63,8 +63,8 @@ CommandExecutorPortfolio::CommandExecutorPortfolio
   assert(d_threadOptions.size() == d_numThreads);
 
   d_statLastWinner.setData(d_lastWinner);
-  d_stats.registerStat_(&d_statLastWinner);
-  d_stats.registerStat_(&d_statWaitTime);
+  d_stats.registerStat(&d_statLastWinner);
+  d_stats.registerStat(&d_statWaitTime);
 
   /* Duplication, individualization */
   d_exprMgrs.push_back(&d_exprMgr);
@@ -99,8 +99,8 @@ CommandExecutorPortfolio::~CommandExecutorPortfolio()
   d_exprMgrs.clear();
   d_smts.clear();
 
-  d_stats.unregisterStat_(&d_statLastWinner);
-  d_stats.unregisterStat_(&d_statWaitTime);
+  d_stats.unregisterStat(&d_statLastWinner);
+  d_stats.unregisterStat(&d_statWaitTime);
 }
 
 void CommandExecutorPortfolio::lemmaSharingInit()
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index c110ffa4f..71f47906d 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -28,7 +28,6 @@
 #include "base/output.h"
 #include "expr/expr_iomanip.h"
 #include "expr/expr_manager.h"
-#include "expr/statistics_registry.h"
 #include "main/command_executor.h"
 
 #ifdef PORTFOLIO_BUILD
@@ -50,6 +49,7 @@
 #include "smt_util/command.h"
 #include "util/configuration.h"
 #include "util/result.h"
+#include "util/statistics_registry.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/src/main/main.cpp b/src/main/main.cpp
index f8cb0677c..92902ac11 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -24,7 +24,6 @@
 
 #include "base/output.h"
 #include "expr/expr_manager.h"
-#include "expr/statistics.h"
 #include "main/command_executor.h"
 #include "main/interactive_shell.h"
 #include "options/base_options.h"
@@ -37,6 +36,7 @@
 #include "smt_util/command.h"
 #include "util/configuration.h"
 #include "util/result.h"
+#include "util/statistics.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/src/main/main.h b/src/main/main.h
index 7dda429af..2ba688a98 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -21,10 +21,10 @@
 #include "base/tls.h"
 #include "cvc4autoconfig.h"
 #include "expr/expr_manager.h"
-#include "expr/statistics.h"
-#include "expr/statistics_registry.h"
 #include "options/options.h"
 #include "smt/smt_engine.h"
+#include "util/statistics.h"
+#include "util/statistics_registry.h"
 
 #ifndef __CVC4__MAIN__MAIN_H
 #define __CVC4__MAIN__MAIN_H
diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp
index ea7e3d458..22f3a67ae 100644
--- a/src/main/portfolio.cpp
+++ b/src/main/portfolio.cpp
@@ -20,11 +20,10 @@
 #include <boost/exception_ptr.hpp>
 
 #include "base/output.h"
-#include "expr/statistics_registry.h"
 #include "options/options.h"
 #include "smt/smt_engine.h"
 #include "util/result.h"
-
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 
diff --git a/src/main/portfolio.h b/src/main/portfolio.h
index 5a730c005..cab8bda3c 100644
--- a/src/main/portfolio.h
+++ b/src/main/portfolio.h
@@ -19,10 +19,10 @@
 #include <boost/function.hpp>
 #include <utility>
 
-#include "expr/statistics_registry.h"
 #include "options/options.h"
 #include "smt/smt_engine.h"
 #include "smt_util/command.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 
diff --git a/src/main/util.cpp b/src/main/util.cpp
index bc3d45287..abcdcc7c5 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -31,12 +31,12 @@
 #include "base/exception.h"
 #include "base/tls.h"
 #include "cvc4autoconfig.h"
-#include "expr/statistics.h"
 #include "main/command_executor.h"
 #include "main/main.h"
 #include "options/base_options.h"
 #include "options/options.h"
 #include "smt/smt_engine.h"
+#include "util/statistics.h"
 
 using CVC4::Exception;
 using namespace std;