From 42d5d8950d849aa4b855aa62834cd5fdee1a91a8 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 11 Mar 2021 21:20:19 +0100 Subject: 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. --- src/prop/bvminisat/bvminisat.cpp | 20 ++++++++++---------- src/prop/bvminisat/bvminisat.h | 1 + src/prop/minisat/minisat.cpp | 18 +++++++++--------- 3 files changed, 20 insertions(+), 19 deletions(-) (limited to 'src/prop') diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index e3571a868..e58060191 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -285,16 +285,16 @@ void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){ return; } - d_statStarts.setData(minisat->starts); - d_statDecisions.setData(minisat->decisions); - d_statRndDecisions.setData(minisat->rnd_decisions); - d_statPropagations.setData(minisat->propagations); - d_statConflicts.setData(minisat->conflicts); - d_statClausesLiterals.setData(minisat->clauses_literals); - d_statLearntsLiterals.setData(minisat->learnts_literals); - d_statMaxLiterals.setData(minisat->max_literals); - d_statTotLiterals.setData(minisat->tot_literals); - d_statEliminatedVars.setData(minisat->eliminated_vars); + d_statStarts.set(minisat->starts); + d_statDecisions.set(minisat->decisions); + d_statRndDecisions.set(minisat->rnd_decisions); + d_statPropagations.set(minisat->propagations); + d_statConflicts.set(minisat->conflicts); + d_statClausesLiterals.set(minisat->clauses_literals); + d_statLearntsLiterals.set(minisat->learnts_literals); + d_statMaxLiterals.set(minisat->max_literals); + d_statTotLiterals.set(minisat->tot_literals); + d_statEliminatedVars.set(minisat->eliminated_vars); } } /* namespace CVC4::prop */ diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index 7661cb423..f91ed4d1d 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -26,6 +26,7 @@ #include "prop/sat_solver.h" #include "util/resource_manager.h" #include "util/statistics_registry.h" +#include "util/stats_timer.h" namespace CVC4 { namespace prop { diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index fd2c00fc1..935c08e9b 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -289,15 +289,15 @@ MinisatSatSolver::Statistics::~Statistics() { } void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* minisat){ - d_statStarts.setData(minisat->starts); - d_statDecisions.setData(minisat->decisions); - d_statRndDecisions.setData(minisat->rnd_decisions); - d_statPropagations.setData(minisat->propagations); - d_statConflicts.setData(minisat->conflicts); - d_statClausesLiterals.setData(minisat->clauses_literals); - d_statLearntsLiterals.setData(minisat->learnts_literals); - d_statMaxLiterals.setData(minisat->max_literals); - d_statTotLiterals.setData(minisat->tot_literals); + d_statStarts.set(minisat->starts); + d_statDecisions.set(minisat->decisions); + d_statRndDecisions.set(minisat->rnd_decisions); + d_statPropagations.set(minisat->propagations); + d_statConflicts.set(minisat->conflicts); + d_statClausesLiterals.set(minisat->clauses_literals); + d_statLearntsLiterals.set(minisat->learnts_literals); + d_statMaxLiterals.set(minisat->max_literals); + d_statTotLiterals.set(minisat->tot_literals); } } /* namespace CVC4::prop */ -- cgit v1.2.3