From 44528cd42df4153b67f85a7aab9c5e1a5c67fdf5 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 1 Nov 2016 14:31:41 -0500
Subject: [PATCH] Fix memory leak in TheorySetsRels.  Minor cleanup.

---
 src/expr/datatype.cpp                | 1 -
 src/expr/expr_manager_template.cpp   | 8 +-------
 src/expr/node_manager.cpp            | 1 -
 src/smt/smt_engine.cpp               | 3 ---
 src/theory/sets/theory_sets_rels.cpp | 9 ++++++++-
 5 files changed, 9 insertions(+), 13 deletions(-)

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 26ab2f2da..537fc2b1a 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -52,7 +52,6 @@ typedef expr::Attribute<expr::attr::DatatypeUFiniteTag, bool> DatatypeUFiniteAtt
 typedef expr::Attribute<expr::attr::DatatypeUFiniteComputedTag, bool> DatatypeUFiniteComputedAttr;
 
 Datatype::~Datatype(){
-  Trace("ajr-temp") << "delete datatype " << getName() << " " << this << std::endl;
   delete d_record;
 }
 
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 1eb94140d..470a6eeca 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -665,7 +665,6 @@ std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(std::vector<Datatyp
   std::map<std::string, DatatypeType> nameResolutions;
   std::vector<DatatypeType> dtts;
 
-  Trace("ajr-temp") << "Build datatypes..." << std::endl;
   //have to build deep copy so that datatypes will live in NodeManager
   std::vector< Datatype* > dt_copies;
   for(std::vector<Datatype>::iterator i = datatypes.begin(), i_end = datatypes.end(); i != i_end; ++i) {
@@ -710,7 +709,6 @@ std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(std::vector<Datatyp
     //Assert( dtt.getDatatype()==(*i) );
   }
 
-  Trace("ajr-temp") << "Set up map..." << std::endl;
   // Second, set up the type substitution map for complex type
   // resolution (e.g. if "list" is the type we're defining, and it has
   // a selector of type "ARRAY INT OF list", this can't be taken care
@@ -753,14 +751,12 @@ std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(std::vector<Datatyp
     }
   }
 
-  Trace("ajr-temp") << "Resolve..." << std::endl;
   // Lastly, perform the final resolutions and checks.
   for(std::vector<DatatypeType>::iterator i = dtts.begin(),
         i_end = dtts.end();
       i != i_end;
       ++i) {
     const Datatype& dt = (*i).getDatatype();
-    Trace("ajr-temp") << "Resolve " << dt.getName() << std::endl;
     if(!dt.isResolved()) {
       const_cast<Datatype&>(dt).resolve(this, nameResolutions,
                                         placeholders, replacements,
@@ -772,12 +768,10 @@ std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(std::vector<Datatyp
     checkResolvedDatatype(*i);
   }
 
-  Trace("ajr-temp") << "Notify..." << std::endl;
   for(std::vector<NodeManagerListener*>::iterator i = d_nodeManager->d_listeners.begin(); i != d_nodeManager->d_listeners.end(); ++i) {
     (*i)->nmNotifyNewDatatypes(dtts);
   }
-
-  Trace("ajr-temp") << "Finish..." << std::endl;
+  
   return dtts;
 }
 
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 2e6792bdd..34f2960be 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -220,7 +220,6 @@ NodeManager::~NodeManager() {
 }
 
 unsigned NodeManager::registerDatatype(Datatype* dt) {
-  Trace("ajr-temp") << "Register datatype : " << dt->getName() << " " << dt << std::endl;
   unsigned sz = d_ownedDatatypes.size();
   d_ownedDatatypes.push_back( dt );
   return sz;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1e5ac84b4..e3a0533af 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -784,11 +784,8 @@ public:
   }
 
   void nmNotifyNewDatatypes(const std::vector<DatatypeType>& dtts) {
-    Trace("ajr-temp") << "Notify " << dtts.size() << " datatypes." << std::endl;
     DatatypeDeclarationCommand c(dtts);
-    Trace("ajr-temp") << "dump command" << std::endl;
     d_smt.addToModelCommandAndDump(c);
-    Trace("ajr-temp") << "Finish" << std::endl;
   }
 
   void nmNotifyNewVar(TNode n, uint32_t flags) {
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index c7ec08210..6fb7412da 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -1181,7 +1181,14 @@ int TheorySetsRels::EqcInfo::counter        = 0;
     d_eqEngine->addFunctionKind(kind::TCLOSURE);
   }
 
-  TheorySetsRels::~TheorySetsRels() {}
+  TheorySetsRels::~TheorySetsRels() {
+    for(std::map< Node, EqcInfo* >::iterator i = d_eqc_info.begin(), iend = d_eqc_info.end();
+        i != iend; ++i){
+      EqcInfo* current = (*i).second;
+      Assert(current != NULL);
+      delete current;
+    }
+  }
 
   std::vector<Node> TupleTrie::findTerms( std::vector< Node >& reps, int argIndex ) {
     std::vector<Node>                           nodes;
-- 
2.30.2