From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 18 Oct 2009 11:34:38 +0000 (+0000)
Subject: Speed up grep0084.stp.cvc & grep0117.stp.cvc, by reducing unnecessary memory copying... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=09ff03f6189f47226c45db769fec2ef18d964114;p=francis%2Fstp.git

Speed up grep0084.stp.cvc & grep0117.stp.cvc, by reducing unnecessary memory copying in the CNF generator




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 f6e1718..dff89b1 100644
--- 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()