diff options
Diffstat (limited to 'src/prop/cadical.cpp')
| -rw-r--r-- | src/prop/cadical.cpp | 27 |
1 files changed, 8 insertions, 19 deletions
diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp index 9cbf067a6..3cce2a7f5 100644 --- a/src/prop/cadical.cpp +++ b/src/prop/cadical.cpp @@ -20,6 +20,7 @@ #ifdef CVC5_USE_CADICAL #include "base/check.h" +#include "util/statistics_registry.h" namespace cvc5 { namespace prop { @@ -56,7 +57,7 @@ CadicalVar toCadicalVar(SatVariable var) { return var; } } // namespace helper functions -CadicalSolver::CadicalSolver(StatisticsRegistry* registry, +CadicalSolver::CadicalSolver(StatisticsRegistry& registry, const std::string& name) : d_solver(new CaDiCaL::Solver()), // Note: CaDiCaL variables start with index 1 rather than 0 since negated @@ -179,25 +180,13 @@ unsigned CadicalSolver::getAssertionLevel() const bool CadicalSolver::ok() const { return d_inSatMode; } -CadicalSolver::Statistics::Statistics(StatisticsRegistry* registry, +CadicalSolver::Statistics::Statistics(StatisticsRegistry& registry, const std::string& prefix) - : d_registry(registry), - d_numSatCalls("theory::bv::" + prefix + "::cadical::calls_to_solve", 0), - d_numVariables("theory::bv::" + prefix + "::cadical::variables", 0), - d_numClauses("theory::bv::" + prefix + "::cadical::clauses", 0), - d_solveTime("theory::bv::" + prefix + "::cadical::solve_time") -{ - d_registry->registerStat(&d_numSatCalls); - d_registry->registerStat(&d_numVariables); - d_registry->registerStat(&d_numClauses); - d_registry->registerStat(&d_solveTime); -} - -CadicalSolver::Statistics::~Statistics() { - d_registry->unregisterStat(&d_numSatCalls); - d_registry->unregisterStat(&d_numVariables); - d_registry->unregisterStat(&d_numClauses); - d_registry->unregisterStat(&d_solveTime); + : d_numSatCalls(registry.registerInt(prefix + "cadical::calls_to_solve", 0)), + d_numVariables(registry.registerInt(prefix + "cadical::variables", 0)), + d_numClauses(registry.registerInt(prefix + "cadical::clauses", 0)), + d_solveTime(registry.registerTimer(prefix + "cadical::solve_time")) + { } } // namespace prop |