diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-04-28 20:01:15 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-28 18:01:15 +0000 |
commit | 0683b708c4752c1d0e894f19e8011a256ef6df7e (patch) | |
tree | 2f832d72c3b7b83519bf030a692bc0b91278b2d6 | |
parent | b5ac06abf4b2cc6b027dedd045595187589bcc35 (diff) |
Make sure reference stats are reset properly (#6457)
This PR adds a reset() method to the ReferenceStat class. It then uses it to properly reset such statistics in the minisat solvers where lifetime is an issue.
-rw-r--r-- | src/prop/bvminisat/bvminisat.cpp | 23 | ||||
-rw-r--r-- | src/prop/bvminisat/bvminisat.h | 1 | ||||
-rw-r--r-- | src/prop/minisat/minisat.cpp | 13 | ||||
-rw-r--r-- | src/prop/minisat/minisat.h | 1 | ||||
-rw-r--r-- | src/util/statistics_stats.h | 9 |
5 files changed, 44 insertions, 3 deletions
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index 1d8bf8f17..77b8c68e0 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -38,9 +38,7 @@ BVMinisatSatSolver::BVMinisatSatSolver(StatisticsRegistry& registry, d_statistics.init(d_minisat.get()); } - -BVMinisatSatSolver::~BVMinisatSatSolver() { -} +BVMinisatSatSolver::~BVMinisatSatSolver() { d_statistics.deinit(); } void BVMinisatSatSolver::MinisatNotify::notify( BVMinisat::vec<BVMinisat::Lit>& clause) @@ -278,5 +276,24 @@ void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){ d_statEliminatedVars.set(minisat->eliminated_vars); } +void BVMinisatSatSolver::Statistics::deinit() +{ + if (!d_registerStats) + { + return; + } + + d_statStarts.reset(); + d_statDecisions.reset(); + d_statRndDecisions.reset(); + d_statPropagations.reset(); + d_statConflicts.reset(); + d_statClausesLiterals.reset(); + d_statLearntsLiterals.reset(); + d_statMaxLiterals.reset(); + d_statTotLiterals.reset(); + d_statEliminatedVars.reset(); +} + } // namespace prop } // namespace cvc5 diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index ea509ece6..6ec43025e 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -141,6 +141,7 @@ public: bool d_registerStats; Statistics(StatisticsRegistry& registry, const std::string& prefix); void init(BVMinisat::SimpSolver* minisat); + void deinit(); }; Statistics d_statistics; diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index 611416dbc..b09ffd685 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -37,6 +37,7 @@ MinisatSatSolver::MinisatSatSolver(StatisticsRegistry& registry) MinisatSatSolver::~MinisatSatSolver() { + d_statistics.deinit(); delete d_minisat; } @@ -316,6 +317,18 @@ void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* minisat){ d_statMaxLiterals.set(minisat->max_literals); d_statTotLiterals.set(minisat->tot_literals); } +void MinisatSatSolver::Statistics::deinit() +{ + d_statStarts.reset(); + d_statDecisions.reset(); + d_statRndDecisions.reset(); + d_statPropagations.reset(); + d_statConflicts.reset(); + d_statClausesLiterals.reset(); + d_statLearntsLiterals.reset(); + d_statMaxLiterals.reset(); + d_statTotLiterals.reset(); +} } // namespace prop } // namespace cvc5 diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index 74b7ab749..a4bd1e7a0 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -123,6 +123,7 @@ class MinisatSatSolver : public CDCLTSatSolverInterface public: Statistics(StatisticsRegistry& registry); void init(Minisat::SimpSolver* d_minisat); + void deinit(); };/* class MinisatSatSolver::Statistics */ Statistics d_statistics; diff --git a/src/util/statistics_stats.h b/src/util/statistics_stats.h index 4821dda60..982190b79 100644 --- a/src/util/statistics_stats.h +++ b/src/util/statistics_stats.h @@ -131,6 +131,15 @@ class ReferenceStat d_data->d_value = &t; } } + /** Commit the value currently pointed to and release it. */ + void reset() + { + if constexpr (Configuration::isStatisticsBuild()) + { + d_data->commit(); + d_data->d_value = nullptr; + } + } /** Copy the current value of the referenced object. */ ~ReferenceStat() { |