From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 10 Feb 2011 06:57:44 +0000 (+0000)
Subject: Fix a leak in _asserts. I know of no other leaks.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=89576b232bc7b8ea0b1c9cee24769aa94a042bc7;p=francis%2Fstp.git

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 e5ee70f..8c365e7 100644
--- 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 8eab3db..31c1527 100644
--- 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 6650852..ac92426 100644
--- 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 c7b4688..77f2b67 100644
--- 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;