summaryrefslogtreecommitdiff
path: root/src/prop/sat.h
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2010-09-21 21:51:25 +0000
committerMorgan Deters <mdeters@gmail.com>2010-09-21 21:51:25 +0000
commit2b2d9092eea1f50b468e459029dcfdd88e2232da (patch)
tree82de73997d5e7193fb32d730cdfa00719b95052b /src/prop/sat.h
parent9dbc683d057288a23109075d806a5398252eaa12 (diff)
fix statistics-registry-related memory leaks
Diffstat (limited to 'src/prop/sat.h')
-rw-r--r--src/prop/sat.h13
1 files changed, 12 insertions, 1 deletions
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 7229b3565..63c17f513 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -126,7 +126,7 @@ class SatSolver : public SatInputInterface {
/** Remember the options */
Options* d_options;
-
+
/* Pointer to the concrete SAT solver. Including this via the
preprocessor saves us a level of indirection vs, e.g., defining a
sub-class for each solver. */
@@ -165,6 +165,17 @@ class SatSolver : public SatInputInterface {
StatisticsRegistry::registerStat(&d_statMaxLiterals);
StatisticsRegistry::registerStat(&d_statTotLiterals);
}
+ ~Statistics() {
+ StatisticsRegistry::unregisterStat(&d_statStarts);
+ StatisticsRegistry::unregisterStat(&d_statDecisions);
+ StatisticsRegistry::unregisterStat(&d_statRndDecisions);
+ StatisticsRegistry::unregisterStat(&d_statPropagations);
+ StatisticsRegistry::unregisterStat(&d_statConflicts);
+ StatisticsRegistry::unregisterStat(&d_statClausesLiterals);
+ StatisticsRegistry::unregisterStat(&d_statLearntsLiterals);
+ StatisticsRegistry::unregisterStat(&d_statMaxLiterals);
+ StatisticsRegistry::unregisterStat(&d_statTotLiterals);
+ }
void init(Minisat::SimpSolver* d_minisat){
d_statStarts.setData(d_minisat->starts);
d_statDecisions.setData(d_minisat->decisions);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback