projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2506e17) | patch
New statistics registry (#6210)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Fri, 2 Apr 2021 18:29:27 +0000 (20:29 +0200)
committerGitHub <noreply@github.com>
Fri, 2 Apr 2021 18:29:27 +0000 (18:29 +0000)
commit5516d995582f5ccfa6e8dcc17d6b7e3f0c56551a
treeb1a6366ac1928e85dc0d499ab9cb1fe354e6917dtree
parent2506e17ca86c42b7590f65326b70a69b0efdb0bdcommit | 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.*.
src/options/base_options.toml diff | blob | history
src/options/options_public_functions.cpp diff | blob | history
src/util/CMakeLists.txt diff | blob | history
src/util/statistics_public.cpp [new file with mode: 0644] blob
src/util/statistics_public.h [new file with mode: 0644] blob
src/util/statistics_reg.cpp [new file with mode: 0644] blob
src/util/statistics_reg.h [new file with mode: 0644] blob