From: Gereon Kremer Date: Wed, 1 Sep 2021 02:00:58 +0000 (-0700) Subject: Make driver::totalTime a TimerStat (#7089) X-Git-Tag: cvc5-1.0.0~1308 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5303c2c85c2d57a2e7c180e639661b071e18f2bc;p=cvc5.git 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 25726f458..6c991ce29 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -16,7 +16,6 @@ #include #include -#include #include #include #include @@ -57,21 +56,8 @@ std::string progName; /** A pointer to the CommandExecutor (the signal handlers need it) */ std::unique_ptr pExecutor; -/** The time point the binary started, accessible to signal handlers */ -std::unique_ptr totalTime; - -TotalTimer::~TotalTimer() -{ - if (pExecutor != nullptr) - { - auto duration = std::chrono::steady_clock::now() - d_start; - pExecutor->getSmtEngine()->setTotalTimeStatistic( - std::chrono::duration(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& solver) { - main::totalTime = std::make_unique(); - // Initialize the signal handlers signal_handlers::install(); @@ -196,8 +180,8 @@ int runCvc5(int argc, char* argv[], std::unique_ptr& 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 cmd; @@ -310,7 +294,6 @@ int runCvc5(int argc, char* argv[], std::unique_ptr& 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 -#include #include #include #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 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 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(*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("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 @@ -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 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::TERM", false); reg.registerValue("driver::filename", false); - reg.registerValue("driver::totalTime", false); + reg.registerTimer("global::totalTime", false); for (theory::TheoryId id = theory::THEORY_FIRST; id != theory::THEORY_LAST; ++id)