Remove some unnecesarry memory churn. Extra objects were created and destroyed that...

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 ba71a5ee42e1f42bed37a0d04567fdf18f163004..eef4a78452ee122389d94e03de0f2843070011fa 100644 (file)
--- 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 fe832f197e7709fe037c20c0341c52afbd732573..074801b8c3e26eb43555a1203a2db92f3ea2dfbf 100644 (file)
--- 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 2b07f46c61cad65784fdf84d4e8f7ba80f0dfb99..b5ea9cb86728c9eb8b69b6875b713c4d9cb5b5e1 100644 (file)
--- 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]
     //########################################