From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 28 Oct 2009 16:27:35 +0000 (+0000)
Subject: improved the clearalltables() functions in various classes, and also the deletion... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=2874877b1a98aef1ed6bfe775196dc75f2e10ca6;p=francis%2Fstp.git

improved the clearalltables() functions in various classes, and also the deletion of the pointers when STP class gets destroyed

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

diff --git a/src/AST/ArrayTransformer.h b/src/AST/ArrayTransformer.h
index e2fd543..dc2773d 100644
--- a/src/AST/ArrayTransformer.h
+++ b/src/AST/ArrayTransformer.h
@@ -136,6 +136,18 @@ namespace BEEV
     // Destructor
     ~ArrayTransformer()
     {
+      Arrayread_IteMap->clear();
+      delete Arrayread_IteMap;
+      Introduced_SymbolsSet.clear();
+      ArrayWrite_RemainingAxioms.clear();
+      ASTNodeToVecMap::iterator it= Arrayname_ReadindicesMap->begin();
+      ASTNodeToVecMap::iterator itend= Arrayname_ReadindicesMap->end();
+      for(;it!=itend;it++)
+	{
+	  ((*it).second).clear();
+	}
+      Arrayname_ReadindicesMap->clear();
+      delete Arrayname_ReadindicesMap;
     }
 
     // Takes a formula, transforms it by replacing array reads with
diff --git a/src/STPManager/STP.h b/src/STPManager/STP.h
index 4c9899d..83882ae 100644
--- a/src/STPManager/STP.h
+++ b/src/STPManager/STP.h
@@ -61,7 +61,13 @@ namespace BEEV
 
     ~STP()
     {
-      ClearAllTables();   
+      ClearAllTables();
+      // delete bvsolver;
+      //       delete Ctr_Example;
+      //       delete arrayTransformer;            
+      //       delete tosat;
+      //       delete simp;
+      //       delete bm;   
     }
 
     /****************************************************************
diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h
index 478068f..9985e02 100644
--- a/src/STPManager/STPManager.h
+++ b/src/STPManager/STPManager.h
@@ -375,14 +375,24 @@ namespace BEEV
       PLPrintNodeSet.clear();
       AlreadyPrintedSet.clear();
       StatInfoSet.clear();
-      
-      //DO NOT UNCOMMENT
-      //   _asserts.clear();
-      //   _interior_unique_table.clear();
-      //   _bvconst_unique_table.clear();
-      //   _symbol_unique_table.clear();      
+      TermsAlreadySeenMap.clear();
     } //End of ClearAllTables()
 
+    ~STPMgr()
+    {
+      vector<ASTVec*>::iterator it    = _asserts.begin();
+      vector<ASTVec*>::iterator itend = _asserts.end();
+      for(;it!=itend;it++) 
+	{
+	  ASTVec * j = (*it);
+	  j->clear();
+	}
+      _asserts.clear();
+
+      _interior_unique_table.clear();
+      _bvconst_unique_table.clear();
+      _symbol_unique_table.clear();
+    }
   };//End of Class STPMgr
 };//end of namespace
 #endif
diff --git a/src/absrefine_counterexample/AbsRefine_CounterExample.h b/src/absrefine_counterexample/AbsRefine_CounterExample.h
index b03cf11..71760e8 100644
--- a/src/absrefine_counterexample/AbsRefine_CounterExample.h
+++ b/src/absrefine_counterexample/AbsRefine_CounterExample.h
@@ -185,6 +185,12 @@ namespace BEEV
       _ASTNode_to_BitvectorMap.clear();
       ComputeFormulaMap.clear();
     } //End of ClearAllTables()
+
+    ~AbsRefine_CounterExample()
+    {
+      ClearAllTables();
+    } //End of destructor
+
   };//End of Class CounterExample
 
   class CompleteCounterExample
diff --git a/src/to-sat/BitBlast.h b/src/to-sat/BitBlast.h
index 6b210b7..8e818ca 100644
--- a/src/to-sat/BitBlast.h
+++ b/src/to-sat/BitBlast.h
@@ -110,6 +110,8 @@ namespace BEEV
 
     ~BitBlaster()
     {
+      BBTermMemo.clear();
+      BBFormMemo.clear();
     }
     
 
diff --git a/src/to-sat/ToSAT.h b/src/to-sat/ToSAT.h
index 65271bb..a424b5a 100644
--- a/src/to-sat/ToSAT.h
+++ b/src/to-sat/ToSAT.h
@@ -124,6 +124,14 @@ namespace BEEV
       _ASTNode_to_SATVar_Map.clear();
       _SATVar_to_AST_Vector.clear();
     }
+
+    ~ToSAT()
+    {
+      _ASTNode_to_SATVar_Map.clear();
+      RepLitMap.clear();
+      CheckBBandCNFMemo.clear();
+      _SATVar_to_AST_Vector.clear();
+    }
   }; //end of class ToSAT
 }; //end of namespace