From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 28 Apr 2010 11:38:00 +0000 (+0000)
Subject: Remove some unnecesarry memory churn. Extra objects were created and destroyed that... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=59accd5d00dbe96f1bd7c7e83eaa99ea8e8f8faa;p=francis%2Fstp.git

Remove some unnecesarry memory churn. Extra objects were created and destroyed that didn't need to be.

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

diff --git a/src/to-sat/ClauseList.cpp b/src/to-sat/ClauseList.cpp
index ba71a5e..eef4a78 100644
--- a/src/to-sat/ClauseList.cpp
+++ b/src/to-sat/ClauseList.cpp
@@ -12,7 +12,7 @@ void ClauseList::appendToAllClauses(const ASTNode* n) {
 }
 
 // expects varphi2 to be just a single clause.
-void ClauseList::productInPlace(const ClauseList& varphi2) {
+void ClauseList::INPLACE_PRODUCT(const ClauseList& varphi2) {
 	assert(1 == varphi2.size());
 	ClauseList& varphi1 = *this;
 
diff --git a/src/to-sat/ClauseList.h b/src/to-sat/ClauseList.h
index fe832f1..074801b 100644
--- a/src/to-sat/ClauseList.h
+++ b/src/to-sat/ClauseList.h
@@ -26,7 +26,7 @@ class ClauseList
   public:
 
 	void appendToAllClauses(const ASTNode* n);
-	void productInPlace(const ClauseList& varphi2);
+	void INPLACE_PRODUCT(const ClauseList& varphi2);
 
 	ClauseContainer* asList() {
 		return &cont;
@@ -105,7 +105,6 @@ class ClauseList
 
     static void INPLACE_UNION(ClauseList* varphi1, const ClauseList& varphi2)
     {
-
       ClauseList* psi2 = ClauseList::COPY(varphi2);
       varphi1->insert( psi2);
       delete psi2;
diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp
index 2b07f46..b5ea9cb 100644
--- a/src/to-sat/ToCNF.cpp
+++ b/src/to-sat/ToCNF.cpp
@@ -621,13 +621,11 @@ namespace BEEV
     // step 2, add defs
     //########################################
     
-    ClauseList* cl1;
-    cl1 = SINGLETON(bm->CreateNode(NOT, psi));
-    ClauseList* cl2 = ClauseList::PRODUCT(*(info[varphi]->clausespos), *cl1);
-    defs->insert(cl2);
-    DELETE(info[varphi]->clausespos);
-    DELETE(cl1);
-    delete cl2;
+    ASTNode* copy = ASTNodeToASTNodePtr(bm->CreateNode(NOT, psi));
+    ClauseList* cl = info[varphi]->clausespos;
+    cl->appendToAllClauses(copy);
+    defs->insert(cl);
+    delete cl;
     
     //########################################
     // step 3, update info[varphi]
@@ -721,14 +719,12 @@ namespace BEEV
     // step 3, add defs
     //########################################
     
-    ClauseList* cl1;
-    cl1 = SINGLETON(psi);
-    ClauseList* cl2 = ClauseList::PRODUCT(*(info[varphi]->clausesneg), *cl1);
-    defs->insert(cl2);
-    DELETE(info[varphi]->clausesneg);
-    DELETE(cl1);
-    delete cl2;
-    
+    ASTNode* copy = ASTNodeToASTNodePtr(psi);
+    ClauseList* cl = info[varphi]->clausesneg;
+    cl->appendToAllClauses(copy);
+    defs->insert(cl);
+    delete cl;
+
     //########################################
     // step 4, update info[varphi]
     //########################################