Fix memory leak in TheorySetsRels. Minor cleanup.

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 26ab2f2da5b48fb47755cf7fd7a858e8b50e3473..537fc2b1abd58b64fd0c425af64badd81c3ef26c 100644 (file)
--- 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 1eb94140d3ab174c8725303ff922bddcb708b944..470a6eeca0d02be4fb05e30dfd4b25e55f85565d 100644 (file)
--- 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 2e6792bdd9f380fb376f80790376415ab0a2a539..34f2960be59ed43daabdd92c56d159c6147f6bab 100644 (file)
--- 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 1e5ac84b442d5ffd976c1ba2fd45b9d41c9dd543..e3a0533afea80c43954dcfd86524f810abae492f 100644 (file)
--- 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 c7ec0821049b4a26965b283dd565af3b9c0e7a5e..6fb7412da1a23c8fbac64aed29af46a850c8a711 100644 (file)
--- 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;