Fix a leak in _asserts. I know of no other leaks.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1141 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/STPManager/STP.h b/src/STPManager/STP.h
index e5ee70f5c0ffb7cb87592530fb9e248afa02f3f8..8c365e73a73ee04f038cb04e1b8ece06a0aa1c52 100644 (file)
--- a/src/STPManager/STP.h
+++ b/src/STPManager/STP.h
@@ -77,9 +77,13 @@ namespace BEEV
     {
       ClearAllTables();
       delete Ctr_Example;
+      Ctr_Example = NULL;
       delete arrayTransformer;
+      arrayTransformer = NULL;
       delete tosat;
+      tosat = NULL;
       delete simp;
+      simp = NULL;
       //delete bm;
     }
 
@@ -106,12 +110,16 @@ namespace BEEV
          
     void ClearAllTables(void)
     {
-      simp->ClearAllTables();
-      arrayTransformer->ClearAllTables();
-      tosat->ClearAllTables();
-      Ctr_Example->ClearAllTables();
-      //bm->ClearAllTables();
-    }
+               if (simp != NULL)
+                       simp->ClearAllTables();
+               if (arrayTransformer != NULL)
+                       arrayTransformer->ClearAllTables();
+               if (tosat != NULL)
+                       tosat->ClearAllTables();
+               if (Ctr_Example != NULL)
+                       Ctr_Example->ClearAllTables();
+               //bm->ClearAllTables();
+       }
   }; //End of Class STP
 };//end of namespace
 #endif

diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp
index 8eab3db649b68a581b30a46ba14fdf676758f4d6..31c1527bd573e1abb67de6cdef42b6b3e465b45c 100644 (file)
--- a/src/STPManager/STPManager.cpp
+++ b/src/STPManager/STPManager.cpp
@@ -14,6 +14,7 @@
 #include <inttypes.h>
 #include <cmath>
 #include "../STPManager/STPManager.h"
+#include "../printer/SMTLIBPrinter.h"
 
 namespace BEEV
 {
@@ -726,6 +727,50 @@ namespace BEEV
   } // End of NewParameterized_BooleanVar()
 
   
-
+  //If ASTNode remain with references (somewhere), this will segfault.
+  STPMgr::~STPMgr() {
+               ClearAllTables();
+
+                 printer::NodeLetVarMap.clear();
+                 printer::NodeLetVarVec.clear();
+                 printer::NodeLetVarMap1.clear();
+
+               delete runTimes;
+               runTimes = NULL;
+               ASTFalse = ASTNode(0);
+               ASTTrue = ASTNode(0);
+               ASTUndefined = ASTNode(0);
+               _current_query = ASTNode(0);
+               dummy_node = ASTNode(0);
+
+               zeroes.clear();
+               ones.clear();
+               max.clear();
+
+               if (NULL != CreateBVConstVal)
+                       CONSTANTBV::BitVector_Destroy(CreateBVConstVal);
+
+               Introduced_SymbolsSet.clear();
+               _symbol_unique_table.clear();
+               _bvconst_unique_table.clear();
+
+               vector<IntToASTVecMap*>::iterator it = _asserts.begin();
+               vector<IntToASTVecMap*>::iterator itend = _asserts.end();
+
+               for (; it != itend; it++) {
+                       IntToASTVecMap * j = (*it);
+                       for (IntToASTVecMap::iterator it2 = j->begin(); it2 != j->end(); it2++) {
+                               it2->second->clear();
+                               delete (it2->second);
+                       }
+                       j->clear();
+                       delete j;
+               }
+               _asserts.clear();
+
+               delete hashingNodeFactory;
+
+               _interior_unique_table.clear();
+       }
 }; // end namespace beev
 

diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h
index 6650852bfb959fe3aa655b02478f4b3625304471..ac9242698e4dba1ba578a7445fa4fd83ed801d5d 100644 (file)
--- a/src/STPManager/STPManager.h
+++ b/src/STPManager/STPManager.h
@@ -437,67 +437,8 @@ namespace BEEV
       ListOfDeclaredVars.clear();
     } //End of ClearAllTables()
 
+    ~STPMgr();
 
-    // This will exit cleanly even if nodes remain around in memory.
-    // So it's a partial safe destructor.
-    void cleanup()
-       {
-         ClearAllTables();
-
-         delete runTimes;
-         runTimes = NULL;
-         ASTFalse     = ASTNode(0);
-         ASTTrue      = ASTNode(0);
-         ASTUndefined = ASTNode(0);
-         _current_query = ASTNode(0);
-         dummy_node =  ASTNode(0);
-
-         zeroes.clear();
-         ones.clear();
-         max.clear();
-
-         Introduced_SymbolsSet.clear();
-         _symbol_unique_table.clear();
-
-         vector<IntToASTVecMap*>::iterator it    = _asserts.begin();
-         vector<IntToASTVecMap*>::iterator itend = _asserts.end();
-         for(;it!=itend;it++)
-               {
-                 IntToASTVecMap * j = (*it);
-                 j->clear();
-                 delete j;
-               }
-         _asserts.clear();
-
-         delete hashingNodeFactory;
-       }
-
-    // If ASTNode remain with references (somewhere), this will segfault.
-    ~STPMgr()
-    {
-      ClearAllTables();
-
-      vector<IntToASTVecMap*>::iterator it    = _asserts.begin();
-      vector<IntToASTVecMap*>::iterator itend = _asserts.end();
-      for(;it!=itend;it++) 
-        {
-          IntToASTVecMap * j = (*it);
-          j->clear();
-          delete j;
-        }
-      _asserts.clear();
-
-      delete runTimes;
-          
-      _interior_unique_table.clear();
-      _bvconst_unique_table.clear();
-      _symbol_unique_table.clear();
-
-      if (NULL != CreateBVConstVal)
-        CONSTANTBV::BitVector_Destroy(CreateBVConstVal);
-
-      delete hashingNodeFactory;
-    }
   };//End of Class STPMgr
 };//end of namespace
 #endif

diff --git a/src/main/main.cpp b/src/main/main.cpp
index c7b4688d26c923eaf36d97a8083b35d2aa1fc2ef..77f2b67b4fb3d196cb81c91d62202a9b6364fa10 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -1,3 +1,4 @@
+
 /********************************************************************
  * AUTHORS: Vijay Ganesh
  *
@@ -597,7 +598,17 @@ int main(int argc, char ** argv) {
   delete AssertsQuery;
   asserts = ASTNode();
   query = ASTNode();
-  bm->cleanup();
+  _empty_ASTVec.clear();
+
+  simpCleaner.release();
+  atClearner.release();
+  tosatCleaner.release();
+  ctrCleaner.release();
+
+  delete GlobalSTP;
+  delete ParserBM;
+
+
 
 
   return 0;