Make driver::totalTime a TimerStat (#7089)

This makes the `driver::totalTime` statistic a `TimerStat`. This eliminates the need to obtain the overall runtime in the driver and write it to the statistics towards the end of the runtime. This not only eliminates some code in the driver, but also gets rid of the call to `getSmtEngine()` that goes around the API.
One disclaimer: The statistics output changes from seconds as a double (i.e. `1.234`) to milliseconds (i.e. `1234ms`).

8 files changed, 6 insertions, 51 deletions

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 25726f458..6c991ce29 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -16,7 +16,6 @@
 #include <stdio.h>
 #include <unistd.h>
 
-#include <chrono>
 #include <cstdlib>
 #include <cstring>
 #include <fstream>
@@ -57,21 +56,8 @@ std::string progName;
 /** A pointer to the CommandExecutor (the signal handlers need it) */
 std::unique_ptr<cvc5::main::CommandExecutor> pExecutor;
 
-/** The time point the binary started, accessible to signal handlers */
-std::unique_ptr<TotalTimer> totalTime;
-
-TotalTimer::~TotalTimer()
-{
-  if (pExecutor != nullptr)
-  {
-    auto duration = std::chrono::steady_clock::now() - d_start;
-    pExecutor->getSmtEngine()->setTotalTimeStatistic(
-        std::chrono::duration<double>(duration).count());
-  }
-    }
-
-    }  // namespace main
-    }  // namespace cvc5
+}  // namespace main
+}  // namespace cvc5
 
     void printUsage(const api::DriverOptions& dopts, bool full)
     {
@@ -95,8 +81,6 @@ TotalTimer::~TotalTimer()
 
 int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
 {
-  main::totalTime = std::make_unique<TotalTimer>();
-
   // Initialize the signal handlers
   signal_handlers::install();
 
@@ -196,8 +180,8 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
 
   int returnValue = 0;
   {
-    // notify SmtEngine that we are starting to parse
-    pExecutor->getSmtEngine()->setInfo("filename", filenameStr);
+    // pass filename to solver (options & statistics)
+    solver->setInfo("filename", filenameStr);
 
     // Parse and execute commands until we are done
     std::unique_ptr<Command> cmd;
@@ -310,7 +294,6 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
     _exit(returnValue);
 #endif /* CVC5_COMPETITION_MODE */
 
-    totalTime.reset();
     pExecutor->flushOutputStreams();
 
 #ifdef CVC5_DEBUG
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 18be1b406..bbc0b6ece 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -92,7 +92,6 @@ int main(int argc, char* argv[])
     if (solver->getOptionInfo("stats").boolValue()
         && main::pExecutor != nullptr)
     {
-      totalTime.reset();
       pExecutor->printStatistics(solver->getDriverOptions().err());
     }
   }
diff --git a/src/main/main.h b/src/main/main.h
index 5643588e1..765e85abb 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -13,15 +13,11 @@
  * Header for main cvc5 driver.
  */
 
-#include <chrono>
-#include <exception>
 #include <memory>
 #include <string>
 
 #include "api/cpp/cvc5.h"
 #include "base/cvc5config.h"
-#include "base/exception.h"
-#include "options/options.h"
 
 #ifndef CVC5__MAIN__MAIN_H
 #define CVC5__MAIN__MAIN_H
@@ -40,19 +36,6 @@ extern std::string progName;
 /** A reference for use by the signal handlers to print statistics */
 extern std::unique_ptr<cvc5::main::CommandExecutor> pExecutor;
 
-/** Manages a custom timer for the total runtime in RAII-style. */
-class TotalTimer
-{
- public:
-  TotalTimer() : d_start(std::chrono::steady_clock::now()) {}
-  ~TotalTimer();
-
- private:
-  std::chrono::steady_clock::time_point d_start;
-};
-/** The time point the binary started, accessible to signal handlers */
-extern std::unique_ptr<TotalTimer> totalTime;
-
 /**
  * If true, will not spin on segfault even when CVC5_DEBUG is on.
  * Useful for nightly regressions, noninteractive performance runs
diff --git a/src/main/signal_handlers.cpp b/src/main/signal_handlers.cpp
index cff8b47d3..666b90ee2 100644
--- a/src/main/signal_handlers.cpp
+++ b/src/main/signal_handlers.cpp
@@ -57,7 +57,6 @@ void print_statistics()
 {
   if (pExecutor != nullptr)
   {
-    totalTime.reset();
     pExecutor->printStatisticsSafe(STDERR_FILENO);
   }
 }
diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index 9f647f7c9..30158799d 100644
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -51,6 +51,7 @@ Env::Env(NodeManager* nm, const Options* opts)
   {
     d_options.copyValues(*opts);
   }
+  d_statisticsRegistry->registerTimer("global::totalTime").start();
   d_resourceManager = std::make_unique<ResourceManager>(*d_statisticsRegistry, d_options);
 }
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8ecf171bd..2276956b5 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -375,11 +375,6 @@ LogicInfo SmtEngine::getUserLogicInfo() const
   return res;
 }
 
-void SmtEngine::setTotalTimeStatistic(double seconds) {
-  d_env->getStatisticsRegistry().registerValue<double>("driver::totalTime",
-                                                       seconds);
-}
-
 void SmtEngine::setLogicInternal()
 {
   Assert(!d_state->isFullyInited())
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 353d96da8..84501d35e 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -227,11 +227,6 @@ class CVC5_EXPORT SmtEngine
   bool isInternalSubsolver() const;
 
   /**
-   * Helper method for the API to put the total runtime into the statistics.
-   */
-  void setTotalTimeStatistic(double seconds) CVC5_EXPORT;
-
-  /**
    * Get the model (only if immediately preceded by a SAT or NOT_ENTAILED
    * query).  Only permitted if produce-models is on.
    *
diff --git a/src/util/statistics_public.cpp b/src/util/statistics_public.cpp
index 5d17ae792..386169046 100644
--- a/src/util/statistics_public.cpp
+++ b/src/util/statistics_public.cpp
@@ -30,7 +30,7 @@ void registerPublicStatistics(StatisticsRegistry& reg)
   reg.registerHistogram<api::Kind>("api::TERM", false);
 
   reg.registerValue<std::string>("driver::filename", false);
-  reg.registerValue<double>("driver::totalTime", false);
+  reg.registerTimer("global::totalTime", false);
 
   for (theory::TheoryId id = theory::THEORY_FIRST; id != theory::THEORY_LAST;
        ++id)