Improvement. Cleanup memory better at the end.

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

diff --git a/src/AST/RunTimes.cpp b/src/AST/RunTimes.cpp
index 3b02cdc2a1b761c8a0bae92add81cf357ea6a39f..acee0c4964cef62dd511bfbfd4c0815c5aa8d469 100644 (file)
--- a/src/AST/RunTimes.cpp
+++ b/src/AST/RunTimes.cpp
@@ -69,8 +69,8 @@ void RunTimes::print()
   std::cerr << "CPU Time Used   : " << Minisat::cpuTime() << "s" << std::endl;
   std::cerr << "Peak Memory Used: " << Minisat::memUsedPeak() << "MB" << std::endl;
 
+  clear();
 
-  // iterator
 }
 
 void RunTimes::addTime(Category c, long milliseconds)

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index e1ea85525720173a0c420e4c0ba3d7ab05c49606..f54429447953bcf80a097ebcd8f3a3859fb8b307 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -270,6 +270,7 @@ namespace BEEV {
     // Deleting it clears out all the buckets associated with hashmaps etc. too.
     delete bvsolver;
     bvsolver = new BVSolver(bm,simp);
+    auto_ptr<BVSolver> bvCleaner(bvsolver);
 
     if(bm->UserFlags.stats_flag)
        simp->printCacheStatus();

diff --git a/src/STPManager/STP.h b/src/STPManager/STP.h
index 24379658705a2396cb4cc05dde45fee4a7c38bbd..fd2551fcf304b8c0d1a4b9ab18e8dab66aa2257a 100644 (file)
--- a/src/STPManager/STP.h
+++ b/src/STPManager/STP.h
@@ -64,10 +64,10 @@ namespace BEEV
       ClearAllTables();
       delete bvsolver;
       delete Ctr_Example;
-      delete arrayTransformer;            
+      delete arrayTransformer;
       delete tosat;
       delete simp;
-      //       delete bm;   
+      delete bm;
     }
 
     /****************************************************************

diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h
index f6649fba2e36b83b12a093a73b88dd93759f2a41..d463ffe37e4368b59b0f0b6188fc36f7681d2a35 100644 (file)
--- a/src/STPManager/STPManager.h
+++ b/src/STPManager/STPManager.h
@@ -413,8 +413,6 @@ namespace BEEV
       return false;
     } // End of IntroduceSymbolSet
 
-
-
     bool VarSeenInTerm(const ASTNode& var, const ASTNode& term);
 
     ASTNode NewParameterized_BooleanVar(const ASTNode& var,
@@ -427,7 +425,7 @@ namespace BEEV
 
     // This is called before SAT solving, so only junk that isn't needed
     // after SAT solving should be cleaned out.
-    void ClearAllTables(void) 
+    void ClearAllTables(void)
     {
       NodeLetVarMap.clear();
       NodeLetVarMap1.clear();
@@ -440,8 +438,50 @@ namespace BEEV
     } //End of ClearAllTables()
 
     ~STPMgr()
+        {}
+
+    // The ASTNodes are garbage collected. This object can only be deleted, when every node has been
+    // cleaned up already. Unfortunately, some references are remaining somewhere to nodes. The
+    // destructor will look like this.
+    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();
+      NodeLetVarMap.clear();
+      NodeLetVarMap1.clear();
+      PLPrintNodeSet.clear();
+      AlreadyPrintedSet.clear();
+      StatInfoSet.clear();
+      TermsAlreadySeenMap.clear();
+      NodeLetVarVec.clear();
+      ListOfDeclaredVars.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;
+    }
+       /*
+       ClearAllTables();
 
       vector<IntToASTVecMap*>::iterator it    = _asserts.begin();
       vector<IntToASTVecMap*>::iterator itend = _asserts.end();
@@ -463,7 +503,8 @@ namespace BEEV
         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 e431b169c5797c0814edfa2e84b295cc78ba7510..e53c8793d5630dc10357dabaef2a0c05ce6277c3 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -15,6 +15,7 @@
 #include "../AST/NodeFactory/SimplifyingNodeFactory.h"
 #include "../parser/ParserInterface.h"
 #include <sys/time.h>
+#include <memory>
 
 
 #ifdef EXT_HASH_MAP
@@ -92,12 +93,21 @@ int main(int argc, char ** argv) {
 
 
   STPMgr * bm       = new STPMgr();
+
   Simplifier * simp  = new Simplifier(bm);
+  auto_ptr<Simplifier> simpCleaner(simp);
+
   BVSolver* bvsolver = new BVSolver(bm, simp);
+
   ArrayTransformer * arrayTransformer = new ArrayTransformer(bm, simp);
+  auto_ptr<ArrayTransformer> atClearner(arrayTransformer);
+
   ToSAT * tosat      = new ToSAT(bm);
-  AbsRefine_CounterExample * Ctr_Example = 
-    new AbsRefine_CounterExample(bm, simp, arrayTransformer);
+  auto_ptr<ToSAT> tosatCleaner(tosat);
+
+  AbsRefine_CounterExample * Ctr_Example = new AbsRefine_CounterExample(bm, simp, arrayTransformer);
+  auto_ptr<AbsRefine_CounterExample> ctrCleaner(Ctr_Example);
+
   itimerval timeout; 
 
   ParserBM          = bm;
@@ -109,6 +119,7 @@ int main(int argc, char ** argv) {
             tosat, 
             Ctr_Example);
   
+
   //populate the help string
   helpstring += 
     "STP version            : " + version + "\n\n";
@@ -579,12 +590,18 @@ int main(int argc, char ** argv) {
   }
 
   SOLVER_RETURN_TYPE ret = GlobalSTP->TopLevelSTP(asserts, query);
-  if (bm->UserFlags.quick_statistics_flag) 
+  if (bm->UserFlags.quick_statistics_flag)
     {
       bm->GetRunTimes()->print();
     }
   (GlobalSTP->tosat)->PrintOutput(ret);
 
+  AssertsQuery->clear();
   delete AssertsQuery;
+  asserts = ASTNode();
+  query = ASTNode();
+  bm->cleanup();
+
+
   return 0;
 }//end of Main