Bugfix. The c-api calls ~STP and ~STPMgr. The changes I made to the destructors in...

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index f54429447953bcf80a097ebcd8f3a3859fb8b307..7051eddd25036c5540bb424871a9dc890e983631 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -270,7 +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);
+    //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 fd2551fcf304b8c0d1a4b9ab18e8dab66aa2257a..6c2a160d993fe3887e4db241990a2da2843e3cc0 100644 (file)
--- a/src/STPManager/STP.h
+++ b/src/STPManager/STP.h
@@ -67,7 +67,7 @@ namespace BEEV
       delete arrayTransformer;
       delete tosat;
       delete simp;
-      delete bm;
+      //delete bm;
     }
 
     /****************************************************************

diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h
index d463ffe37e4368b59b0f0b6188fc36f7681d2a35..bf68c34791f4b0a8b35efc24bedc432cc56db191 100644 (file)
--- a/src/STPManager/STPManager.h
+++ b/src/STPManager/STPManager.h
@@ -425,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();
@@ -437,51 +437,45 @@ namespace BEEV
       ListOfDeclaredVars.clear();
     } //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.
+    // 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()
     {
-      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();
+      ClearAllTables();
 
       vector<IntToASTVecMap*>::iterator it    = _asserts.begin();
       vector<IntToASTVecMap*>::iterator itend = _asserts.end();
@@ -503,8 +497,7 @@ namespace BEEV
         CONSTANTBV::BitVector_Destroy(CreateBVConstVal);
 
       delete hashingNodeFactory;
-      */
-    //}
+    }
   };//End of Class STPMgr
 };//end of namespace
 #endif