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/theory/theory_inference_manager.h | |
| 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/theory/theory_inference_manager.h')
| -rw-r--r-- | src/theory/theory_inference_manager.h | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index 89c4aec3f..a785af186 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -26,8 +26,7 @@ #include "theory/inference_id.h" #include "theory/output_channel.h" #include "theory/trust_node.h" -#include "util/statistics_registry.h" -#include "util/stats_histogram.h" +#include "util/statistics_stats.h" namespace cvc5 { @@ -79,8 +78,8 @@ class TheoryInferenceManager * @param state The state of the theory * @param pnm The proof node manager, which if non-null, enables proofs for * this inference manager - * @param name The name of the inference manager, which is used for giving - * unique names for statistics, + * @param statsName The name of the inference manager, which is used for + * giving unique names for statistics, * @param cacheLemmas Whether all lemmas sent using this theory inference * manager are added to a user-context dependent cache. This means that * only lemmas that are unique after rewriting are sent to the theory engine @@ -89,7 +88,7 @@ class TheoryInferenceManager TheoryInferenceManager(Theory& t, TheoryState& state, ProofNodeManager* pnm, - const std::string& name, + const std::string& statsName, bool cacheLemmas = true); virtual ~TheoryInferenceManager(); //--------------------------------------- initialization @@ -454,11 +453,11 @@ class TheoryInferenceManager /** The number of internal facts added since the last call to reset. */ uint32_t d_numCurrentFacts; /** Statistics for conflicts sent via this inference manager. */ - IntegralHistogramStat<InferenceId> d_conflictIdStats; + HistogramStat<InferenceId> d_conflictIdStats; /** Statistics for facts sent via this inference manager. */ - IntegralHistogramStat<InferenceId> d_factIdStats; + HistogramStat<InferenceId> d_factIdStats; /** Statistics for lemmas sent via this inference manager. */ - IntegralHistogramStat<InferenceId> d_lemmaIdStats; + HistogramStat<InferenceId> d_lemmaIdStats; }; } // namespace theory |