diff options
| author | Gereon Kremer <gkremer@stanford.edu> | 2021-03-11 21:20:19 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-11 20:20:19 +0000 |
| commit | 42d5d8950d849aa4b855aa62834cd5fdee1a91a8 (patch) | |
| tree | 2cbb6d9b283c05fc12ba9ad8495fa84a57375af6 /src/main | |
| parent | dc679ed380aabc62aadfbb4033c02c5a27ae903c (diff) | |
First refactoring of statistics classes (#6105)
This PR does a first round of refactoring on the statistics, in particular the Stat class and derived classes.
It significantly shrinks the class hierarchy, modernizes some code (e.g. use std::chrono instead of clock_gettime), removes unused features (e.g. nesting of statistics) and does some general cleanup and consolidation.
Subsequent PRs are planned to change the ownership model (right now every module owns the Stat object) which makes the whole register / unregister mechanism obsolete.
Diffstat (limited to 'src/main')
| -rw-r--r-- | src/main/command_executor.cpp | 2 | ||||
| -rw-r--r-- | src/main/driver_unified.cpp | 6 | ||||
| -rw-r--r-- | src/main/main.h | 1 |
3 files changed, 5 insertions, 4 deletions
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index e80ed7749..a343b4a37 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -52,7 +52,7 @@ CommandExecutor::CommandExecutor(Options& options) d_symman(new SymbolManager(d_solver.get())), d_smtEngine(d_solver->getSmtEngine()), d_options(options), - d_stats("driver"), + d_stats(), d_result() { } diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 70e6b7b39..88f23ec36 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -84,7 +84,7 @@ void printUsage(Options& opts, bool full) { int runCvc4(int argc, char* argv[], Options& opts) { // Timer statistic - pTotalTime = new TimerStat("totalTime"); + pTotalTime = new TimerStat("driver::totalTime"); pTotalTime->start(); // For the signal handlers' benefit @@ -192,7 +192,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { pTotalTime); // Filename statistics - ReferenceStat<std::string> s_statFilename("filename", filenameStr); + ReferenceStat<std::string> s_statFilename("driver::filename", filenameStr); RegisterStatistic statFilenameReg(&pExecutor->getStatisticsRegistry(), &s_statFilename); // notify SmtEngine that we are starting to parse @@ -473,7 +473,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { _exit(returnValue); #endif /* CVC4_COMPETITION_MODE */ - ReferenceStat<api::Result> s_statSatResult("sat/unsat", result); + ReferenceStat<api::Result> s_statSatResult("driver::sat/unsat", result); RegisterStatistic statSatResultReg(&pExecutor->getStatisticsRegistry(), &s_statSatResult); diff --git a/src/main/main.h b/src/main/main.h index 202c74204..37430b507 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -22,6 +22,7 @@ #include "options/options.h" #include "util/statistics.h" #include "util/statistics_registry.h" +#include "util/stats_timer.h" #ifndef CVC4__MAIN__MAIN_H #define CVC4__MAIN__MAIN_H |