summaryrefslogtreecommitdiff
path: root/src/prop/bvminisat/bvminisat.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/bvminisat/bvminisat.cpp')
-rw-r--r--src/prop/bvminisat/bvminisat.cpp23
1 files changed, 20 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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback