First refactoring of statistics classes (#6105)
authorGereon Kremer <gkremer@stanford.edu>
Thu, 11 Mar 2021 20:20:19 +0000 (21:20 +0100)
committerGitHub <noreply@github.com>
Thu, 11 Mar 2021 20:20:19 +0000 (20:20 +0000)
commit42d5d8950d849aa4b855aa62834cd5fdee1a91a8
tree2cbb6d9b283c05fc12ba9ad8495fa84a57375af6
parentdc679ed380aabc62aadfbb4033c02c5a27ae903c
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.
51 files changed:
src/api/cvc4cpp.cpp
src/decision/justification_heuristic.h
src/expr/proof_checker.h
src/main/command_executor.cpp
src/main/driver_unified.cpp
src/main/main.h
src/preprocessing/passes/ite_simp.h
src/preprocessing/preprocessing_pass.h
src/preprocessing/util/ite_utilities.h
src/proof/sat_proof.h
src/prop/bvminisat/bvminisat.cpp
src/prop/bvminisat/bvminisat.h
src/prop/minisat/minisat.cpp
src/smt/proof_post_processor.h
src/smt/smt_engine_stats.h
src/theory/arith/approx_simplex.cpp
src/theory/arith/approx_simplex.h
src/theory/arith/dio_solver.h
src/theory/arith/linear_equality.h
src/theory/arith/simplex.cpp
src/theory/arith/simplex.h
src/theory/arith/theory_arith_private.cpp
src/theory/arrays/array_info.cpp
src/theory/arrays/array_info.h
src/theory/bags/bags_rewriter.h
src/theory/bags/bags_statistics.h
src/theory/bv/abstraction.cpp
src/theory/bv/abstraction.h
src/theory/bv/bv_quick_check.cpp
src/theory/bv/bv_quick_check.h
src/theory/bv/bv_solver_lazy.cpp
src/theory/bv/bv_subtheory_algebraic.cpp
src/theory/quantifiers/quant_conflict_find.cpp
src/theory/strings/sequences_stats.h
src/theory/theory.h
src/theory/theory_inference_manager.h
src/theory/uf/symmetry_breaker.h
src/util/CMakeLists.txt
src/util/resource_manager.cpp
src/util/statistics.cpp
src/util/statistics.h
src/util/statistics_registry.cpp
src/util/statistics_registry.h
src/util/stats_base.cpp [new file with mode: 0644]
src/util/stats_base.h [new file with mode: 0644]
src/util/stats_histogram.h [new file with mode: 0644]
src/util/stats_timer.cpp [new file with mode: 0644]
src/util/stats_timer.h [new file with mode: 0644]
src/util/stats_utils.cpp [new file with mode: 0644]
src/util/stats_utils.h [new file with mode: 0644]
test/unit/util/stats_black.cpp