improved the clearalltables() functions in various classes, and also the deletion...

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 e2fd54352298469661ccdb546f301e9c3a1abb05..dc2773dc88f3f81ca20f5712020db6a1eb42d8d9 100644 (file)
--- 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 4c9899dc4c7a40eb311fc00f81a25006c0bb6f7d..83882ae0805a33e647618ed8f37159945a163789 100644 (file)
--- 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 478068fd18634926e76546711d2c566e0a820b1d..9985e0270ee14c95be6f3553abe99fafb059bf1e 100644 (file)
--- 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 b03cf11b4a5df7088aae3ed88faa200297e538ad..71760e86820b380def2c4a838481366b7ec9aea9 100644 (file)
--- 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 6b210b7b0e38850d812bac58268dd763b8f87290..8e818ca2bd1bbcbbf71e24315e0bcae9c398d06f 100644 (file)
--- 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 65271bb61d8b860329f6300082b23643c42ff20c..a424b5a058d00f8ff3460a13a02cdcb403a7c139 100644 (file)
--- 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