diff options
author | Gereon Kremer <nafur42@gmail.com> | 2021-08-31 19:00:58 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-09-01 02:00:58 +0000 |
commit | 5303c2c85c2d57a2e7c180e639661b071e18f2bc (patch) | |
tree | 024ce6fb07e6ff5475fc9c2ec76dbf745c1a58cd /src/util | |
parent | a6cdf2b085aaa9789f47757329a7803053ceb36a (diff) |
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`).
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/statistics_public.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
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) |