diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-04-14 21:37:12 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-14 19:37:12 +0000 |
| commit | 9f14a0d6feca8d8ba727f88ef7dda5268183bb56 (patch) | |
| tree | 54d1500f368312ade8abb1fb9962976ae61bedfc /src/options | |
| parent | e5c26181dab76704ad9a47126585fe2ec9d6cac2 (diff) | |
Refactor / reimplement statistics (#6162)
This PR refactors how we collect statistics.
It splits the current statistic values into the values and a proxy object. The actual values now live inside the registry (making the ownership model way easier) while the proxy object are handed to whoever wants to collect a new statistic.
It also extends the C++ API to obtain and inspect the statistics.
To change the ownership, this PR needs to touch every single statistic in the whole codebase and change how it is registered.
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/base_options.toml | 17 | ||||
| -rw-r--r-- | src/options/options.h | 1 | ||||
| -rw-r--r-- | src/options/options_public_functions.cpp | 4 |
3 files changed, 4 insertions, 18 deletions
diff --git a/src/options/base_options.toml b/src/options/base_options.toml index 17050cd06..9c02a51d1 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -104,14 +104,14 @@ header = "options/base_options.h" help = "print expert (non-public) statistics as well" [[option]] - name = "statisticsUnset" - smt_name = "stats-unset" - long = "stats-unset" + name = "statisticsAll" + smt_name = "stats-all" + long = "stats-all" category = "expert" type = "bool" predicates = ["statsEnabledBuild"] read_only = true - help = "print unset statistics as well" + help = "print unchanged (defaulted) statistics as well" [[option]] name = "statisticsEveryQuery" @@ -125,15 +125,6 @@ header = "options/base_options.h" help = "in incremental mode, print stats after every satisfiability or validity query" [[option]] - name = "statsHideZeros" - category = "regular" - long = "stats-hide-zeros" - type = "bool" - default = "false" - read_only = true - help = "hide statistics which are zero" - -[[option]] name = "parseOnly" category = "regular" long = "parse-only" diff --git a/src/options/options.h b/src/options/options.h index 804110f1d..79b00de30 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -171,7 +171,6 @@ public: bool getSemanticChecks() const; bool getStatistics() const; bool getStatsEveryQuery() const; - bool getStatsHideZeros() const; bool getStrictParsing() const; int getTearDownIncremental() const; unsigned long getCumulativeTimeLimit() const; diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp index 3d9c2b669..f70c1ce3b 100644 --- a/src/options/options_public_functions.cpp +++ b/src/options/options_public_functions.cpp @@ -133,10 +133,6 @@ bool Options::getStatsEveryQuery() const{ return (*this)[options::statisticsEveryQuery]; } -bool Options::getStatsHideZeros() const{ - return (*this)[options::statsHideZeros]; -} - bool Options::getStrictParsing() const{ return (*this)[options::strictParsing]; } |