From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Tue, 30 Mar 2021 01:06:14 +0000 (+0200)
Subject: Fix total time statistic (#6233)
X-Git-Tag: cvc5-1.0.0~2013
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c7a8c32825af7dceb6cee631523a480a5b2cc6ba;p=cvc5.git

Fix total time statistic (#6233)

Since one of the last changes to the total time collection in the driver, this collection fails when the solver terminates unexpectedly (either by a signal or an exception). This PR fixes this issue and does some cleanup along the way.
---

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index d2b676e82..2bca01e08 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -57,7 +57,20 @@ namespace CVC4 {
     const std::string *progName;
 
     /** A pointer to the CommandExecutor (the signal handlers need it) */
-    CVC4::main::CommandExecutor* pExecutor = nullptr;
+    std::unique_ptr<CVC4::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());
+      }
+    }
 
   }/* CVC4::main namespace */
 }/* CVC4 namespace */
@@ -78,8 +91,7 @@ void printUsage(Options& opts, bool full) {
 }
 
 int runCvc4(int argc, char* argv[], Options& opts) {
-
-  std::chrono::time_point totalTimeStart = std::chrono::steady_clock::now();
+  main::totalTime = std::make_unique<TotalTimer>();
   // For the signal handlers' benefit
   pOptions = &opts;
 
@@ -176,7 +188,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   (*(opts.getOut())) << language::SetLanguage(opts.getOutputLanguage());
 
   // Create the command executor to execute the parsed commands
-  pExecutor = new CommandExecutor(opts);
+  pExecutor = std::make_unique<CommandExecutor>(opts);
 
   int returnValue = 0;
   {
@@ -457,10 +469,8 @@ 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());
 
+    totalTime.reset();
     pExecutor->flushOutputStreams();
 
 #ifdef CVC4_DEBUG
@@ -474,9 +484,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
 #endif /* CVC4_DEBUG */
   }
 
-  delete pExecutor;
-
-  pExecutor = nullptr;
+  pExecutor.reset();
 
   signal_handlers::cleanup();
 
diff --git a/src/main/main.cpp b/src/main/main.cpp
index eb313c3bd..65b341a12 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -66,7 +66,9 @@ int main(int argc, char* argv[]) {
     } else {
       *opts.getErr() << "(error \"" << e << "\")" << endl;
     }
-    if(opts.getStatistics() && pExecutor != NULL) {
+    if (opts.getStatistics() && pExecutor != nullptr)
+    {
+      totalTime.reset();
       pExecutor->flushStatistics(*opts.getErr());
     }
   }
diff --git a/src/main/main.h b/src/main/main.h
index b769bee7d..518145577 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -14,7 +14,9 @@
  ** Header for main CVC4 driver.
  **/
 
+#include <chrono>
 #include <exception>
+#include <memory>
 #include <string>
 
 #include "base/exception.h"
@@ -36,7 +38,20 @@ extern const char* progPath;
 extern const std::string* progName;
 
 /** A reference for use by the signal handlers to print statistics */
-extern CVC4::main::CommandExecutor* pExecutor;
+extern std::unique_ptr<CVC4::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 CVC4_DEBUG is on.
diff --git a/src/main/signal_handlers.cpp b/src/main/signal_handlers.cpp
index ccd6c0b19..93014b256 100644
--- a/src/main/signal_handlers.cpp
+++ b/src/main/signal_handlers.cpp
@@ -60,6 +60,7 @@ void print_statistics()
 {
   if (pOptions != NULL && pOptions->getStatistics() && pExecutor != NULL)
   {
+    totalTime.reset();
     pExecutor->safeFlushStatistics(STDERR_FILENO);
   }
 }