diff options
Diffstat (limited to 'src/prop/bvminisat/bvminisat.cpp')
-rw-r--r-- | src/prop/bvminisat/bvminisat.cpp | 23 |
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 |