1 files changed, 20 insertions, 38 deletions

diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index e84325897..55209b248 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -21,20 +21,18 @@
 #include "options/decision_options.h"
 #include "options/prop_options.h"
 #include "options/smt_options.h"
-#include "prop/minisat/simp/SimpSolver.h"
 #include "proof/clause_id.h"
 #include "proof/sat_proof.h"
-#include "util/statistics_registry.h"
+#include "prop/minisat/simp/SimpSolver.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace prop {
 
 //// DPllMinisatSatSolver
 
-MinisatSatSolver::MinisatSatSolver(StatisticsRegistry* registry) :
-  d_minisat(NULL),
-  d_context(NULL),
-  d_statistics(registry)
+MinisatSatSolver::MinisatSatSolver(StatisticsRegistry& registry)
+    : d_minisat(NULL), d_context(NULL), d_statistics(registry)
 {}
 
 MinisatSatSolver::~MinisatSatSolver()
@@ -254,39 +252,23 @@ void MinisatSatSolver::resetTrail() { d_minisat->resetTrail(); }
 
 /// Statistics for MinisatSatSolver
 
-MinisatSatSolver::Statistics::Statistics(StatisticsRegistry* registry) :
-    d_registry(registry),
-    d_statStarts("sat::starts"),
-    d_statDecisions("sat::decisions"),
-    d_statRndDecisions("sat::rnd_decisions"),
-    d_statPropagations("sat::propagations"),
-    d_statConflicts("sat::conflicts"),
-    d_statClausesLiterals("sat::clauses_literals"),
-    d_statLearntsLiterals("sat::learnts_literals"),
-    d_statMaxLiterals("sat::max_literals"),
-    d_statTotLiterals("sat::tot_literals")
+MinisatSatSolver::Statistics::Statistics(StatisticsRegistry& registry)
+    : d_statStarts(registry.registerReference<int64_t>("sat::starts")),
+      d_statDecisions(registry.registerReference<int64_t>("sat::decisions")),
+      d_statRndDecisions(
+          registry.registerReference<int64_t>("sat::rnd_decisions")),
+      d_statPropagations(
+          registry.registerReference<int64_t>("sat::propagations")),
+      d_statConflicts(registry.registerReference<int64_t>("sat::conflicts")),
+      d_statClausesLiterals(
+          registry.registerReference<int64_t>("sat::clauses_literals")),
+      d_statLearntsLiterals(
+          registry.registerReference<int64_t>("sat::learnts_literals")),
+      d_statMaxLiterals(
+          registry.registerReference<int64_t>("sat::max_literals")),
+      d_statTotLiterals(
+          registry.registerReference<int64_t>("sat::tot_literals"))
 {
-  d_registry->registerStat(&d_statStarts);
-  d_registry->registerStat(&d_statDecisions);
-  d_registry->registerStat(&d_statRndDecisions);
-  d_registry->registerStat(&d_statPropagations);
-  d_registry->registerStat(&d_statConflicts);
-  d_registry->registerStat(&d_statClausesLiterals);
-  d_registry->registerStat(&d_statLearntsLiterals);
-  d_registry->registerStat(&d_statMaxLiterals);
-  d_registry->registerStat(&d_statTotLiterals);
-}
-
-MinisatSatSolver::Statistics::~Statistics() {
-  d_registry->unregisterStat(&d_statStarts);
-  d_registry->unregisterStat(&d_statDecisions);
-  d_registry->unregisterStat(&d_statRndDecisions);
-  d_registry->unregisterStat(&d_statPropagations);
-  d_registry->unregisterStat(&d_statConflicts);
-  d_registry->unregisterStat(&d_statClausesLiterals);
-  d_registry->unregisterStat(&d_statLearntsLiterals);
-  d_registry->unregisterStat(&d_statMaxLiterals);
-  d_registry->unregisterStat(&d_statTotLiterals);
 }
 
 void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* minisat){