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.

7 files changed, 11 insertions, 7 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(); }