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

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 25726f45826864de5d98f5f8094f29264290845f..6c991ce29e3c99cf94bdb095e5bd9e92a2befdf8 100644 (file)
--- 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 18be1b406f7b4b0b8ec6341357cf24b5e230e5d4..bbc0b6ecebf530854c6bfaf134f53bfdfadae407 100644 (file)
--- 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 5643588e190b856b5e7e610ddb9299ac31623c89..765e85abba9a9a9416ba0ffd88a21a606e571167 100644 (file)
--- 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 cff8b47d3e815c6cce5de0a55637c658a34eec59..666b90ee2173dd71ff5acee1f9ea6a7efaaeee67 100644 (file)
--- 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 9f647f7c95cd18e19e790294b5636feece9ef508..30158799d58f2b5b9db10c75788fb56a02b9559c 100644 (file)
--- 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 8ecf171bdcb97da42ccc486f27f1bbeadc570993..2276956b59fcbf7532c2904b2d346f0815f729e2 100644 (file)
--- 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 353d96da8f429250dcabb0b0ac2ec56437774286..84501d35e660d985b165ee1bf9d954a1f286a501 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -226,11 +226,6 @@ class CVC5_EXPORT SmtEngine
   /** Is this an internal subsolver? */
   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 5d17ae7925b2721f652b5dc83160e0dc8b1ae1be..38616904672270411714187f9c31480200cd450a 100644 (file)
--- 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)