From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 10 May 2010 02:45:50 +0000 (+0000)
Subject: When sending clauses to the SAT solver, create fewer objects. This speeds up sending... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=bd325cac8921e30a6db90a337c6a2dadb040af81;p=francis%2Fstp.git

When sending clauses to the SAT solver, create fewer objects. This speeds up sending to the sat solver by about 15%.

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

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 8c95135..72a23d8 100644
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -91,14 +91,14 @@ namespace BEEV
       }
 
 	ClauseContainer& cc = *cll.asList();
+    //Clause for the SATSolver
+	MINISAT::vec<MINISAT::Lit> satSolverClause;
 
     //iterate through the list (conjunction) of ASTclauses cll
     ClauseContainer::const_iterator i = cc.begin(), iend = cc.end();
     for (int count=0, flag=0; i != iend; i++)
       {
-        //Clause for the SATSolver
-        MINISAT::vec<MINISAT::Lit> satSolverClause;
-        satSolverClause.capacity((*i)->size());        
+        satSolverClause.clear();
         vector<const ASTNode*>::const_iterator j    = (*i)->begin(); 
         vector<const ASTNode*>::const_iterator jend = (*i)->end();      
         //ASTVec  clauseVec;