From bcc0197552d52bf8baa35521aea9d0950016eb45 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 3 Feb 2011 01:57:49 +0000
Subject: [PATCH] Bugfix. The c-api calls ~STP and ~STPMgr. The changes I made
 to the destructors in r1115 broke the c-api.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1116 e59a4935-1847-0410-ae03-e826735625c1
---
 src/STPManager/STP.cpp      |  2 +-
 src/STPManager/STP.h        |  2 +-
 src/STPManager/STPManager.h | 83 +++++++++++++++++--------------------
 3 files changed, 40 insertions(+), 47 deletions(-)

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index f544294..7051edd 100644
--- 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 fd2551f..6c2a160 100644
--- 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 d463ffe..bf68c34 100644
--- 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
-- 
2.47.3