Garbage collecting the EqcInfo s in TheoryDatatypes::d_eqc_info.

2 files changed, 14 insertions, 7 deletions

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 26ca50897..8123fe39c 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -75,6 +75,12 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
 }
 
 TheoryDatatypes::~TheoryDatatypes() {
+  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;
+  }
 }
 
 void TheoryDatatypes::setMasterEqualityEngine(eq::EqualityEngine* eq) {
@@ -91,7 +97,7 @@ TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( TNode n, bool doMak
 
       std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n );
       EqcInfo* ei;
-      if( eqc_i!=d_eqc_info.end() ){
+      if( eqc_i != d_eqc_info.end() ){
         ei = eqc_i->second;
       }else{
         ei = new EqcInfo( getSatContext() );
@@ -901,10 +907,11 @@ void TheoryDatatypes::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){
 
 }
 
-TheoryDatatypes::EqcInfo::EqcInfo( context::Context* c ) :
-d_inst( c, false ), d_constructor( c, Node::null() ), d_selectors( c, false ){
-
-}
+TheoryDatatypes::EqcInfo::EqcInfo( context::Context* c )
+    : d_inst( c, false )
+    , d_constructor( c, Node::null() )
+    , d_selectors( c, false )
+{}
 
 bool TheoryDatatypes::hasLabel( EqcInfo* eqc, Node n ){
   return ( eqc && !eqc->d_constructor.get().isNull() ) || !getLabel( n ).isNull();
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 0f110b369..0a038f0ed 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -133,8 +133,8 @@ private:
   void getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >& cons );
   void getSelectorsForCons( Node r, std::map< int, bool >& sels );
   /** mkExpDefSkolem */
-  void mkExpDefSkolem( Node sel, TypeNode dt, TypeNode rt );  
-  /** skolems for terms */  
+  void mkExpDefSkolem( Node sel, TypeNode dt, TypeNode rt );
+  /** skolems for terms */
   NodeMap d_term_sk;
   Node getTermSkolemFor( Node n );
 private: