From 9f14a0d6feca8d8ba727f88ef7dda5268183bb56 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 14 Apr 2021 21:37:12 +0200 Subject: 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. --- src/decision/justification_heuristic.cpp | 17 +++++------------ src/decision/justification_heuristic.h | 3 +-- 2 files changed, 6 insertions(+), 14 deletions(-) (limited to 'src/decision') diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index 2332fa9fd..42e4cb7b0 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -40,9 +40,10 @@ JustificationHeuristic::JustificationHeuristic(cvc5::DecisionEngine* de, d_exploredThreshold(c), d_prvsIndex(c, 0), d_threshPrvsIndex(c, 0), - d_helpfulness("decision::jh::helpfulness", 0), - d_giveup("decision::jh::giveup", 0), - d_timestat("decision::jh::time"), + d_helpfulness( + smtStatisticsRegistry().registerInt("decision::jh::helpfulness")), + d_giveup(smtStatisticsRegistry().registerInt("decision::jh::giveup")), + d_timestat(smtStatisticsRegistry().registerTimer("decision::jh::time")), d_assertions(uc), d_skolemAssertions(uc), d_skolemCache(uc), @@ -54,18 +55,10 @@ JustificationHeuristic::JustificationHeuristic(cvc5::DecisionEngine* de, d_weightCache(uc), d_startIndexCache(c) { - smtStatisticsRegistry()->registerStat(&d_helpfulness); - smtStatisticsRegistry()->registerStat(&d_giveup); - smtStatisticsRegistry()->registerStat(&d_timestat); Trace("decision") << "Justification heuristic enabled" << std::endl; } -JustificationHeuristic::~JustificationHeuristic() -{ - smtStatisticsRegistry()->unregisterStat(&d_helpfulness); - smtStatisticsRegistry()->unregisterStat(&d_giveup); - smtStatisticsRegistry()->unregisterStat(&d_timestat); -} +JustificationHeuristic::~JustificationHeuristic() {} cvc5::prop::SatLiteral JustificationHeuristic::getNext(bool& stopSearch) { diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 728c0a10d..a7c82646d 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -35,8 +35,7 @@ #include "expr/node.h" #include "options/decision_weight.h" #include "prop/sat_solver_types.h" -#include "util/statistics_registry.h" -#include "util/stats_timer.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace decision { -- cgit v1.2.3