diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-04-02 20:29:27 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-02 18:29:27 +0000 |
| commit | 5516d995582f5ccfa6e8dcc17d6b7e3f0c56551a (patch) | |
| tree | b1a6366ac1928e85dc0d499ab9cb1fe354e6917d /src/options | |
| parent | 2506e17ca86c42b7590f65326b70a69b0efdb0bd (diff) | |
New statistics registry (#6210)
This PR adds the next part of the new statistics setup: the registry.
The new statistics registry owns the actual data and only issues proxy objects that can be used to modify the internally stored data.
Once we replace the old statistics setup, the files should be renamed from statistics_reg.* to statistics_registry.*.
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/base_options.toml | 28 | ||||
| -rw-r--r-- | src/options/options_public_functions.cpp | 4 |
2 files changed, 27 insertions, 5 deletions
diff --git a/src/options/base_options.toml b/src/options/base_options.toml index cab4332b8..17050cd06 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -86,18 +86,40 @@ header = "options/base_options.h" [[option]] name = "statistics" smt_name = "statistics" - category = "common" long = "stats" + category = "common" type = "bool" predicates = ["statsEnabledBuild"] read_only = true help = "give statistics on exit" [[option]] - name = "statsEveryQuery" - category = "regular" + name = "statisticsExpert" + smt_name = "stats-expert" + long = "stats-expert" + category = "expert" + type = "bool" + predicates = ["statsEnabledBuild"] + read_only = true + help = "print expert (non-public) statistics as well" + +[[option]] + name = "statisticsUnset" + smt_name = "stats-unset" + long = "stats-unset" + category = "expert" + type = "bool" + predicates = ["statsEnabledBuild"] + read_only = true + help = "print unset statistics as well" + +[[option]] + name = "statisticsEveryQuery" + smt_name = "stats-every-query" long = "stats-every-query" + category = "regular" type = "bool" + predicates = ["statsEnabledBuild"] default = "false" read_only = true help = "in incremental mode, print stats after every satisfiability or validity query" diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp index 1bccc283f..3ccf3b744 100644 --- a/src/options/options_public_functions.cpp +++ b/src/options/options_public_functions.cpp @@ -126,11 +126,11 @@ bool Options::getSemanticChecks() const{ bool Options::getStatistics() const{ // statsEveryQuery enables stats - return (*this)[options::statistics] || (*this)[options::statsEveryQuery]; + return (*this)[options::statistics] || (*this)[options::statisticsEveryQuery]; } bool Options::getStatsEveryQuery() const{ - return (*this)[options::statsEveryQuery]; + return (*this)[options::statisticsEveryQuery]; } bool Options::getStatsHideZeros() const{ |