Speed up grep0084.stp.cvc & grep0117.stp.cvc, by reducing unnecessary memory copying...

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

diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp
index f6e171812e7313adf712e8a93350ca647d2f86a6..dff89b1a42f8b7b91425e0b996073d33b1d45eb9 100644 (file)
--- a/src/to-sat/ToCNF.cpp
+++ b/src/to-sat/ToCNF.cpp
@@ -1423,12 +1423,27 @@ namespace BEEV
     convertFormulaToCNF(*it, defs);
     ClauseList* psi = COPY(*(info[*it]->clausesneg));
     reduceMemoryFootprintNeg(*it);
-    for (it++; it != varphi.GetChildren().end(); it++)
-      {
-        convertFormulaToCNF(*it, defs);
-        INPLACE_UNION(psi, *(info[*it]->clausesneg));
-        reduceMemoryFootprintNeg(*it);
-      }
+    for (it++; it != varphi.GetChildren().end(); it++) {
+               convertFormulaToCNF(*it, defs);
+               CNFInfo* x = info[*it];
+
+               if (sharesNeg(*x) != 1) {
+                       INPLACE_UNION(psi, *(x->clausesneg));
+                       reduceMemoryFootprintNeg(*it);
+               } else {
+                       // If this is the only use of "clausesneg", no reason to make a copy.
+                       psi->insert(psi->end(), x->clausesneg->begin(),
+                                       x->clausesneg->end());
+                       // Copied from reduceMemoryFootprintNeg
+                       delete x->clausesneg;
+                       x->clausesneg = NULL;
+                       if (x->clausespos == NULL) {
+                               delete x;
+                               info.erase(*it);
+                       }
+               }
+
+       }
 
     info[varphi]->clausesneg = psi;
   } //End of convertFormulaToCNFNegOR()