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.

diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 1d8bf8f176e668f4e99882a9c97fc2cde0bc8f63..77b8c68e0b68914f6b1c87b6d9e57b663dbe4798 100644 (file)
--- 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 ea509ece63822b7bec22f0331c79a6aa98b6eda9..6ec43025e2f83addbff9fa4c41af139052849fc2 100644 (file)
--- 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 611416dbc6ccd0f2a22345d748ba333b98e69a17..b09ffd685d5364829d7df6e2a26c3ac68a6a6527 100644 (file)
--- 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 74b7ab74910c2f506355c2a5a322b93c7a4238f6..a4bd1e7a0800f2cf22199ddc66b7dc14de068f7c 100644 (file)
--- 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 4821dda601741e4842da1dcebbeb067ecfbb0103..982190b7970c5d963793a843a6eaf77e520552f3 100644 (file)
--- 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()
   {