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`).

4 files changed, 4 insertions, 40 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);
   }
 }