Mostly resolves bug #561 memory leaks, and more.

4 files changed, 26 insertions, 9 deletions

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 2a2a60391..cb4a32ee7 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -69,7 +69,9 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext
   d_theoryEngine(te),
   d_decisionEngine(de),
   d_context(satContext),
+  d_theoryProxy(NULL),
   d_satSolver(NULL),
+  d_registrar(NULL),
   d_cnfStream(NULL),
   d_satTimer(*this),
   d_interrupted(false) {
@@ -78,16 +80,17 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext
 
   d_satSolver = SatSolverFactory::createDPLLMinisat(); 
 
-  theory::TheoryRegistrar* registrar = new theory::TheoryRegistrar(d_theoryEngine);
+  d_registrar = new theory::TheoryRegistrar(d_theoryEngine);
   d_cnfStream = new CVC4::prop::TseitinCnfStream
-    (d_satSolver, registrar, 
+    (d_satSolver, d_registrar,
      userContext,
      // fullLitToNode Map = 
      options::threads() > 1 || 
      options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY
      );
 
-  d_satSolver->initialize(d_context, new TheoryProxy(this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream));
+  d_theoryProxy = new TheoryProxy(this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream);
+  d_satSolver->initialize(d_context, d_theoryProxy);
 
   d_decisionEngine->setSatSolver(d_satSolver);
   d_decisionEngine->setCnfStream(d_cnfStream);
@@ -97,7 +100,9 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext
 PropEngine::~PropEngine() {
   Debug("prop") << "Destructing the PropEngine" << endl;
   delete d_cnfStream;
+  delete d_registrar;
   delete d_satSolver;
+  delete d_theoryProxy;
 }
 
 void PropEngine::assertFormula(TNode node) {
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 39182204c..753890087 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -32,6 +32,10 @@ namespace CVC4 {
 class DecisionEngine;
 class TheoryEngine;
 
+namespace theory {
+  class TheoryRegistrar;
+}/* CVC4::theory namespace */
+
 namespace prop {
 
 class CnfStream;
@@ -132,12 +136,18 @@ class PropEngine {
   /** The context */
   context::Context* d_context;
 
+  /** SAT solver's proxy back to theories; kept around for dtor cleanup */
+  TheoryProxy* d_theoryProxy;
+
   /** The SAT solver proxy */
   DPLLSatSolverInterface* d_satSolver;
 
   /** List of all of the assertions that need to be made */
   std::vector<Node> d_assertionList;
 
+  /** Theory registrar; kept around for destructor cleanup */
+  theory::TheoryRegistrar* d_registrar;
+
   /** The CNF converter in use */
   CnfStream* d_cnfStream;
 
diff --git a/src/prop/registrar.h b/src/prop/registrar.h
index 0cb3accf1..4fe04f062 100644
--- a/src/prop/registrar.h
+++ b/src/prop/registrar.h
@@ -5,7 +5,7 @@
  ** Major contributors: Tim King, Morgan Deters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
@@ -32,13 +32,11 @@ public:
 
 };/* class Registrar */
 
-class NullRegistrar: public Registrar {
+class NullRegistrar : public Registrar {
 public:
-  void preRegister(Node n) {};
-
-};/* class Registrar */
-
+  void preRegister(Node n) {}
 
+};/* class NullRegistrar */
 
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index f84aecbac..92c81616b 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -139,6 +139,10 @@ inline TheoryProxy::TheoryProxy(PropEngine* propEngine,
   d_queue(context)
 {}
 
+inline TheoryProxy::~TheoryProxy() {
+  /* nothing to do for now */
+}
+
 }/* CVC4::prop namespace */
 
 }/* CVC4 namespace */