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.

1 files changed, 4 insertions, 4 deletions

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index ba41b2ca3..aa770ad67 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -24,12 +24,12 @@
 #include "context/cdchunk_list.h"
 #include "context/cdhashset.h"
 #include "expr/attribute.h"
-#include "expr/statistics_registry.h"
 #include "options/quantifiers_modes.h"
 #include "theory/quantifiers/inst_match.h"
 #include "theory/quantifiers/quant_util.h"
 #include "theory/theory.h"
 #include "util/hash.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 
@@ -206,8 +206,7 @@ private:
   NodeList d_presolve_cache;
   BoolList d_presolve_cache_wq;
   BoolList d_presolve_cache_wic;
-private:
-  KEEP_STATISTIC(TimerStat, d_time, "theory::QuantifiersEngine::time");
+
 public:
   QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te);
   ~QuantifiersEngine();
@@ -346,6 +345,7 @@ public:
   /** statistics class */
   class Statistics {
   public:
+    TimerStat d_time;
     IntStat d_num_quant;
     IntStat d_instantiation_rounds;
     IntStat d_instantiation_rounds_lc;
@@ -382,7 +382,7 @@ private:
   std::map< Node, int > d_rep_score;
   /** reset count */
   int d_reset_count;
-private:
+
   /** node contains */
   Node getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache );
   /** get score */