Move statistics from the driver into the SmtEngine (#6170)

This PR does some refactoring on how we handle statistics in the driver, and some minor cleanup along the way.

    The SmtEngine now has dedicated statistics for the data collected within the driver and provides utility functions to set them.
    The driver pushes the collected statistics to the SmtEngine instead of adding them itself to the statistics registry.
    The node manager no longer holds a statistics registry (that nobody used anymore anyway)
    The command executor no longer holds a pointer to the SmtEngine itself. The pointer is not necessary and seems to become stale after we call reset on the command executor (which, luckily, we don't seem to do usually)

The main motivation for this change is to make the whole statistics infrastructure private to the library and not exporting it to the outside world.

1 files changed, 5 insertions, 29 deletions

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 846bef5be..d2b676e82 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -15,6 +15,7 @@
 #include <stdio.h>
 #include <unistd.h>
 
+#include <chrono>
 #include <cstdlib>
 #include <cstring>
 #include <fstream>
@@ -38,7 +39,6 @@
 #include "parser/parser_builder.h"
 #include "smt/command.h"
 #include "util/result.h"
-#include "util/statistics_registry.h"
 
 using namespace std;
 using namespace CVC4;
@@ -59,9 +59,6 @@ namespace CVC4 {
     /** A pointer to the CommandExecutor (the signal handlers need it) */
     CVC4::main::CommandExecutor* pExecutor = nullptr;
 
-    /** A pointer to the totalTime driver stat (the signal handlers need it) */
-    CVC4::TimerStat* pTotalTime = nullptr;
-
   }/* CVC4::main namespace */
 }/* CVC4 namespace */
 
@@ -82,10 +79,7 @@ void printUsage(Options& opts, bool full) {
 
 int runCvc4(int argc, char* argv[], Options& opts) {
 
-  // Timer statistic
-  pTotalTime = new TimerStat("driver::totalTime");
-  pTotalTime->start();
-
+  std::chrono::time_point totalTimeStart = std::chrono::steady_clock::now();
   // For the signal handlers' benefit
   pOptions = &opts;
 
@@ -186,14 +180,6 @@ int runCvc4(int argc, char* argv[], Options& opts) {
 
   int returnValue = 0;
   {
-    // Timer statistic
-    RegisterStatistic statTotalTime(&pExecutor->getStatisticsRegistry(),
-                                    pTotalTime);
-
-    // Filename statistics
-    ReferenceStat<std::string> s_statFilename("driver::filename", filenameStr);
-    RegisterStatistic statFilenameReg(&pExecutor->getStatisticsRegistry(),
-                                      &s_statFilename);
     // notify SmtEngine that we are starting to parse
     pExecutor->getSmtEngine()->notifyStartParsing(filenameStr);
 
@@ -471,16 +457,10 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     // or other on_exit/atexit stuff.
     _exit(returnValue);
 #endif /* CVC4_COMPETITION_MODE */
+    pExecutor->getSmtEngine()->setResultStatistic(result.toString());
+    std::chrono::duration totalTime = std::chrono::steady_clock::now() - totalTimeStart;
+    pExecutor->getSmtEngine()->setTotalTimeStatistic(std::chrono::duration<double>(totalTime).count());
 
-    ReferenceStat<api::Result> s_statSatResult("driver::sat/unsat", result);
-    RegisterStatistic statSatResultReg(&pExecutor->getStatisticsRegistry(),
-                                       &s_statSatResult);
-
-    pTotalTime->stop();
-
-    // Tim: I think that following comment is out of date?
-    // Set the global executor pointer to nullptr first.  If we get a
-    // signal while dumping statistics, we don't want to try again.
     pExecutor->flushOutputStreams();
 
 #ifdef CVC4_DEBUG
@@ -494,12 +474,8 @@ int runCvc4(int argc, char* argv[], Options& opts) {
 #endif /* CVC4_DEBUG */
   }
 
-  // On exceptional exit, these are leaked, but that's okay... they
-  // need to be around in that case for main() to print statistics.
-  delete pTotalTime;
   delete pExecutor;
 
-  pTotalTime = nullptr;
   pExecutor = nullptr;
 
   signal_handlers::cleanup();