First refactoring of statistics classes (#6105)

This PR does a first round of refactoring on the statistics, in particular the Stat class and derived classes.
It significantly shrinks the class hierarchy, modernizes some code (e.g. use std::chrono instead of clock_gettime), removes unused features (e.g. nesting of statistics) and does some general cleanup and consolidation.

Subsequent PRs are planned to change the ownership model (right now every module owns the Stat object) which makes the whole register / unregister mechanism obsolete.

22 files changed, 29 insertions, 16 deletions

diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index ed781fd5e..8d98475ce 100644
--- a/src/theory/arith/approx_simplex.cpp
+++ b/src/theory/arith/approx_simplex.cpp
@@ -3001,7 +3001,7 @@ bool ApproxGLPK::guessCoefficientsConstructTableRow(int nid, int M, const Primit
   for(size_t i=0; i < d_denomGuesses.size(); ++i){
     const Integer& D = d_denomGuesses[i];
     if(!guessCoefficientsConstructTableRow(nid, M, vec, D)){
-      d_stats.d_averageGuesses.addEntry(i+1);
+      d_stats.d_averageGuesses << i+1;
       Debug("approx::gmi") << "guesseditat " << i << " D=" << D << endl;
       return false;
     }
diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h
index 46e252ec7..a9b179e31 100644
--- a/src/theory/arith/approx_simplex.h
+++ b/src/theory/arith/approx_simplex.h
@@ -26,6 +26,7 @@
 #include "util/maybe.h"
 #include "util/rational.h"
 #include "util/statistics_registry.h"
+#include "util/stats_timer.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h
index 3ce7199c0..dc4711800 100644
--- a/src/theory/arith/dio_solver.h
+++ b/src/theory/arith/dio_solver.h
@@ -31,6 +31,7 @@
 #include "theory/arith/normal_form.h"
 #include "util/rational.h"
 #include "util/statistics_registry.h"
+#include "util/stats_timer.h"
 
 namespace CVC4 {
 namespace context {
diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h
index 3cfbfe5db..df4e5f30e 100644
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -38,6 +38,7 @@
 #include "theory/arith/tableau.h"
 #include "util/maybe.h"
 #include "util/statistics_registry.h"
+#include "util/stats_timer.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index fc3d919c3..df399d686 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -70,7 +70,7 @@ bool SimplexDecisionProcedure::standardProcessSignals(TimerStat &timer, IntStat&
 
         Debug("recentlyViolated")
           << "It worked? "
-          << conflicts.getData()
+          << conflicts.get()
           << " " << curr
           << " "  << checkBasicForConflict(curr) << endl;
         reportConflict(curr);
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 110093068..5edfc1608 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -62,6 +62,7 @@
 #include "util/dense_map.h"
 #include "util/result.h"
 #include "util/statistics_registry.h"
+#include "util/stats_timer.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 1cf4a2993..1faad2a7a 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -2457,7 +2457,7 @@ void TheoryArithPrivate::subsumption(
 std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex* approx, int nid, ConstraintP bc, int depth){
   ++(d_statistics.d_replayLogRecCount);
   Debug("approx::replayLogRec") << "replayLogRec()"
-                                << d_statistics.d_replayLogRecCount.getData() << std::endl;
+                                << d_statistics.d_replayLogRecCount.get() << std::endl;
 
   size_t rpvars_size = d_replayVariables.size();
   size_t rpcons_size = d_replayConstraints.size();
@@ -2892,7 +2892,7 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){
   TimerStat::CodeTimer codeTimer0(d_statistics.d_solveIntTimer);
 
   ++(d_statistics.d_solveIntCalls);
-  d_statistics.d_inSolveInteger.setData(1);
+  d_statistics.d_inSolveInteger.set(1);
 
   if(!Theory::fullEffort(effortLevel)){
     d_solveIntAttempts++;
@@ -3018,7 +3018,7 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){
     }
   }
 
-  d_statistics.d_inSolveInteger.setData(0);
+  d_statistics.d_inSolveInteger.set(0);
 }
 
 SimplexDecisionProcedure& TheoryArithPrivate::selectSimplex(bool pass1){
@@ -3532,7 +3532,7 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
   default:
     Unimplemented();
   }
-  d_statistics.d_avgUnknownsInARow.addEntry(d_unknownsInARow);
+  d_statistics.d_avgUnknownsInARow << d_unknownsInARow;
 
   size_t nPivots =
       options::useFC() ? d_fcSimplex.getPivots() : d_dualSimplex.getPivots();
@@ -4366,7 +4366,7 @@ bool TheoryArithPrivate::unenqueuedVariablesAreConsistent(){
 void TheoryArithPrivate::presolve(){
   TimerStat::CodeTimer codeTimer(d_statistics.d_presolveTime);
 
-  d_statistics.d_initialTableauSize.setData(d_tableau.size());
+  d_statistics.d_initialTableauSize.set(d_tableau.size());
 
   if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
 
diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp
index 16126b88c..7919892c6 100644
--- a/src/theory/arrays/array_info.cpp
+++ b/src/theory/arrays/array_info.cpp
@@ -470,20 +470,20 @@ void ArrayInfo::mergeInfo(const TNode a, const TNode b){
 
 
       if(s!= 0) {
-        d_avgIndexListLength.addEntry(s);
+        d_avgIndexListLength << s;
         ++d_listsCount;
       }
       s = lista_st->size();
       d_maxList.maxAssign(s);
       if(s!= 0) {
-        d_avgStoresListLength.addEntry(s);
+        d_avgStoresListLength << s;
         ++d_listsCount;
       }
 
       s = lista_inst->size();
       d_maxList.maxAssign(s);
       if(s!=0) {
-        d_avgInStoresListLength.addEntry(s);
+        d_avgInStoresListLength << s;
         ++d_listsCount;
       }
 
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index 499f96bfb..174980474 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -25,6 +25,7 @@
 #include "context/cdlist.h"
 #include "expr/node.h"
 #include "util/statistics_registry.h"
+#include "util/stats_timer.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h
index 51b2e5438..309b06009 100644
--- a/src/theory/bags/bags_rewriter.h
+++ b/src/theory/bags/bags_rewriter.h
@@ -20,6 +20,7 @@
 #include "theory/bags/rewrites.h"
 #include "theory/theory_rewriter.h"
 #include "util/statistics_registry.h"
+#include "util/stats_histogram.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/bags/bags_statistics.h b/src/theory/bags/bags_statistics.h
index f59c43cb6..c6b6c7e7a 100644
--- a/src/theory/bags/bags_statistics.h
+++ b/src/theory/bags/bags_statistics.h
@@ -19,6 +19,7 @@
 
 #include "theory/bags/rewrites.h"
 #include "util/statistics_registry.h"
+#include "util/stats_histogram.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index 157985cf1..3b9df3518 100644
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -528,7 +528,7 @@ void AbstractionModule::finalizeSignatures()
     d_funcToSignature[abs_func] = signature;
   }
 
-  d_statistics.d_numFunctionsAbstracted.setData(d_signatureToFunc.size());
+  d_statistics.d_numFunctionsAbstracted.set(d_signatureToFunc.size());
 
   Debug("bv-abstraction") << "AbstractionModule::finalizeSignatures abstracted "
                           << d_signatureToFunc.size() << " signatures. \n";
diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h
index 726cfd983..e22e221f2 100644
--- a/src/theory/bv/abstraction.h
+++ b/src/theory/bv/abstraction.h
@@ -25,6 +25,7 @@
 #include "expr/node.h"
 #include "theory/substitutions.h"
 #include "util/statistics_registry.h"
+#include "util/stats_timer.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp
index f9b5e80d2..36e77b0b7 100644
--- a/src/theory/bv/bv_quick_check.cpp
+++ b/src/theory/bv/bv_quick_check.cpp
@@ -347,7 +347,7 @@ Node QuickXPlain::minimizeConflict(TNode confl) {
   // if (1.5* d_statistics.d_numUnknown.getData() > d_statistics.d_numSolved.getData()) {
   //   d_period = d_period * 2;
   // }
-  d_statistics.d_avgMinimizationRatio.addEntry(minimization_ratio);
+  d_statistics.d_avgMinimizationRatio << minimization_ratio;
   return utils::mkAnd(minimized); 
 }
 
diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
index b10eb2811..f509c3cb4 100644
--- a/src/theory/bv/bv_quick_check.h
+++ b/src/theory/bv/bv_quick_check.h
@@ -27,6 +27,7 @@
 #include "prop/sat_solver_types.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "util/statistics_registry.h"
+#include "util/stats_timer.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp
index 7094c831e..9562b69c7 100644
--- a/src/theory/bv/bv_solver_lazy.cpp
+++ b/src/theory/bv/bv_solver_lazy.cpp
@@ -198,7 +198,7 @@ void BVSolverLazy::sendConflict()
     Debug("bitvector") << indent() << "BVSolverLazy::check(): conflict "
                        << d_conflictNode << std::endl;
     d_im.conflict(d_conflictNode, InferenceId::BV_LAZY_CONFLICT);
-    d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren());
+    d_statistics.d_avgConflictSize << d_conflictNode.getNumChildren();
     d_conflictNode = Node::null();
   }
 }
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 38d94ea27..8f774e552 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -668,7 +668,7 @@ bool AlgebraicSolver::useHeuristic() {
     return true;
 
   double success_rate = double(d_numSolved)/double(d_numCalls);
-  d_statistics.d_useHeuristic.setData(success_rate);
+  d_statistics.d_useHeuristic.set(success_rate);
   return success_rate > 0.8;
 }
 
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 17081bb7b..0aafbde56 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -2001,7 +2001,7 @@ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e)
   int prevEt = 0;
   if (Trace.isOn("qcf-engine"))
   {
-    prevEt = d_statistics.d_entailment_checks.getData();
+    prevEt = d_statistics.d_entailment_checks.get();
     clSet = double(clock()) / double(CLOCKS_PER_SEC);
     Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level
                         << "---" << std::endl;
@@ -2070,7 +2070,7 @@ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e)
       Trace("qcf-engine") << ", addedLemmas = " << addedLemmas;
     }
     Trace("qcf-engine") << std::endl;
-    int currEt = d_statistics.d_entailment_checks.getData();
+    int currEt = d_statistics.d_entailment_checks.get();
     if (currEt != prevEt)
     {
       Trace("qcf-engine") << "  Entailment checks = " << (currEt - prevEt)
diff --git a/src/theory/strings/sequences_stats.h b/src/theory/strings/sequences_stats.h
index 1597e32a6..e4d122faf 100644
--- a/src/theory/strings/sequences_stats.h
+++ b/src/theory/strings/sequences_stats.h
@@ -21,6 +21,7 @@
 #include "theory/strings/infer_info.h"
 #include "theory/strings/rewrites.h"
 #include "util/statistics_registry.h"
+#include "util/stats_histogram.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 68a2e1436..1c23d9041 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -37,6 +37,7 @@
 #include "theory/trust_node.h"
 #include "theory/valuation.h"
 #include "util/statistics_registry.h"
+#include "util/stats_timer.h"
 
 namespace CVC4 {
 
diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index a599afa23..549d81c16 100644
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -26,6 +26,7 @@
 #include "theory/output_channel.h"
 #include "theory/trust_node.h"
 #include "util/statistics_registry.h"
+#include "util/stats_histogram.h"
 
 namespace CVC4 {
 
diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h
index 9b9cc79d0..2a95e5bc7 100644
--- a/src/theory/uf/symmetry_breaker.h
+++ b/src/theory/uf/symmetry_breaker.h
@@ -55,6 +55,7 @@
 #include "expr/node_builder.h"
 #include "smt/smt_statistics_registry.h"
 #include "util/statistics_registry.h"
+#include "util/stats_timer.h"
 
 namespace CVC4 {
 namespace theory {