From 89ed50fd35e6425ed7f1fa4ca5ec560acee1358e Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 7 Nov 2014 17:24:35 -0500
Subject: [PATCH] Fix memory issues in bitvector theory, which is now
 valgrind-clean (mostly resolves bug #594).

---
 src/theory/bv/bitblaster_template.h |  5 +++--
 src/theory/bv/bv_quick_check.cpp    | 16 ++++++++--------
 src/theory/bv/bv_quick_check.h      |  2 +-
 src/theory/bv/lazy_bitblaster.cpp   | 16 ++++++++++------
 src/theory/bv/theory_bv.cpp         |  1 +
 5 files changed, 23 insertions(+), 17 deletions(-)

diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index ea31e3821..0ff12da95 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -143,8 +143,9 @@ class TLazyBitblaster :  public TBitblaster<Node> {
   prop::NullRegistrar* d_nullRegistrar;
   context::Context* d_nullContext;
   // sat solver used for bitblasting and associated CnfStream
-  prop::BVSatSolverInterface*        d_satSolver;
-  prop::CnfStream*                   d_cnfStream;
+  prop::BVSatSolverInterface*         d_satSolver;
+  prop::BVSatSolverInterface::Notify* d_satSolverNotify;
+  prop::CnfStream*                    d_cnfStream;
 
   AssertionList* d_assertedAtoms; /**< context dependent list storing the atoms
                                      currently asserted by the DPLL SAT solver. */
diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp
index cc294306a..5c67bb3cb 100644
--- a/src/theory/bv/bv_quick_check.cpp
+++ b/src/theory/bv/bv_quick_check.cpp
@@ -25,10 +25,10 @@ using namespace CVC4::theory::bv;
 using namespace CVC4::prop;
 
 BVQuickCheck::BVQuickCheck(const std::string& name, theory::bv::TheoryBV* bv)
-  : d_ctx(new context::Context())
-  , d_bitblaster(new TLazyBitblaster(d_ctx, bv, name, true))
+  : d_ctx()
+  , d_bitblaster(new TLazyBitblaster(&d_ctx, bv, name, true))
   , d_conflict()
-  , d_inConflict(d_ctx, false)
+  , d_inConflict(&d_ctx, false)
 {}
 
 
@@ -100,11 +100,11 @@ bool BVQuickCheck::addAssertion(TNode assertion) {
 
 
 void BVQuickCheck::push() {
-  d_ctx->push();
+  d_ctx.push();
 }
 
 void BVQuickCheck::pop() {
-  d_ctx->pop();
+  d_ctx.pop();
 }
 
 BVQuickCheck::vars_iterator BVQuickCheck::beginVars() {
@@ -130,8 +130,8 @@ void BVQuickCheck::clearSolver() {
 }
 
 void BVQuickCheck::popToZero() {
-  while (d_ctx->getLevel() > 0) {
-    d_ctx->pop();
+  while (d_ctx.getLevel() > 0) {
+    d_ctx.pop();
   }
 }
 
@@ -140,8 +140,8 @@ void BVQuickCheck::collectModelInfo(theory::TheoryModel* model, bool fullModel)
 }
 
 BVQuickCheck::~BVQuickCheck() {
+  clearSolver();
   delete d_bitblaster;
-  delete d_ctx;
 }
 
 QuickXPlain::QuickXPlain(const std::string& name, BVQuickCheck* solver, unsigned long budget)
diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
index 6c32fbb4d..61d6baf83 100644
--- a/src/theory/bv/bv_quick_check.h
+++ b/src/theory/bv/bv_quick_check.h
@@ -39,7 +39,7 @@ class TLazyBitblaster;
 class TheoryBV;
 
 class BVQuickCheck {
-  context::Context* d_ctx;
+  context::Context d_ctx;
   TLazyBitblaster* d_bitblaster;
   Node d_conflict;
   context::CDO<bool> d_inConflict;
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index f8927284f..b74506e4d 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -51,11 +51,11 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const st
                                            d_nullRegistrar,
                                            d_nullContext);
   
-  prop::BVSatSolverInterface::Notify* notify = d_emptyNotify ?
+  d_satSolverNotify = d_emptyNotify ?
     (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() :
     (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, bv, this);
 
-  d_satSolver->setNotify(notify);
+  d_satSolver->setNotify(d_satSolverNotify);
 }
 
 void TLazyBitblaster::setAbstraction(AbstractionModule* abs) {
@@ -67,6 +67,9 @@ TLazyBitblaster::~TLazyBitblaster() {
   delete d_nullRegistrar;
   delete d_nullContext;
   delete d_satSolver;
+  delete d_satSolverNotify;
+  d_assertedAtoms->deleteSelf();
+  d_explanations->deleteSelf();
 }
 
 
@@ -475,6 +478,7 @@ void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
 void TLazyBitblaster::clearSolver() {
   Assert (d_ctx->getLevel() == 0); 
   delete d_satSolver;
+  delete d_satSolverNotify;
   delete d_cnfStream;
   d_assertedAtoms->deleteSelf();
   d_assertedAtoms = new(true) context::CDList<prop::SatLiteral>(d_ctx);
@@ -487,11 +491,11 @@ void TLazyBitblaster::clearSolver() {
   // recreate sat solver
   d_satSolver = prop::SatSolverFactory::createMinisat(d_ctx);
   d_cnfStream = new prop::TseitinCnfStream(d_satSolver,
-                                           new prop::NullRegistrar(),
-                                           new context::Context());
+                                           d_nullRegistrar,
+                                           d_nullContext);
 
-  prop::BVSatSolverInterface::Notify* notify = d_emptyNotify ?
+  d_satSolverNotify = d_emptyNotify ?
     (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() :
     (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, d_bv, this);
-  d_satSolver->setNotify(notify);
+  d_satSolver->setNotify(d_satSolverNotify);
 }
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 91150f663..99bc764dd 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -95,6 +95,7 @@ TheoryBV::~TheoryBV() {
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
     delete d_subtheories[i];
   }
+  delete d_abstractionModule;
 }
 
 void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
-- 
2.30.2