From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 7 Mar 2010 15:44:00 +0000 (+0000)
Subject: Deleting the contents of the clause list before SAT solving
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=b71a25a6ea4bb5c096232235b24c3a83c60fde67;p=francis%2Fstp.git

Deleting the contents of the clause list before SAT solving

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

diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp
index 406ae2b..0af39f7 100644
--- a/src/to-sat/ToCNF.cpp
+++ b/src/to-sat/ToCNF.cpp
@@ -16,16 +16,18 @@ namespace BEEV
 {
   //############################################################
   //############################################################
-  void DeleteClauseList(ClauseList *cllp)
+
+  void CNFMgr::DeleteClauseList(ClauseList cllp)
   {
-    ClauseList::const_iterator iend = cllp->end();
-    for (ClauseList::const_iterator i = cllp->begin(); i < iend; i++)
+    ClauseList::const_iterator iend = cllp.end();
+    for (ClauseList::const_iterator i = cllp.begin(); i < iend; i++)
       {
         delete *i;
       }
-    delete cllp;
+    cllp.clear();
   } //End of DeleteClauseList
   
+
   bool CNFMgr::isAtom(const ASTNode& varphi)
   {
     bool result;
@@ -1992,12 +1994,7 @@ namespace BEEV
 
   void CNFMgr::DELETE(ClauseList* varphi)
   {
-    ClauseList::const_iterator it = varphi->begin();
-    for (; it != varphi->end(); it++)
-      {
-        delete *it;
-      }
-
+    DeleteClauseList(*varphi);
     delete varphi;
   } //End of DELETE()
 
diff --git a/src/to-sat/ToCNF.h b/src/to-sat/ToCNF.h
index 62d450f..76afc0c 100644
--- a/src/to-sat/ToCNF.h
+++ b/src/to-sat/ToCNF.h
@@ -264,7 +264,10 @@ namespace BEEV
 
     ClauseList* ReturnXorClauses(void);
 
-    void DELETE(ClauseList* varphi);
+    // Destructors that need to be explicitly called...(yuck).
+    // One deletes the thing passed into it.
+    static void DeleteClauseList(ClauseList varphi);
+    static void DELETE(ClauseList* varphi);
 
     void PrintClauseList(ostream& os, ClauseList& cll);
   }; // end of CNFMgr class
diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 02db33f..c3c2de5 100644
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -1,6 +1,6 @@
 // -*- c++ -*-
 /********************************************************************
- * AUTHORS: Vijay Ganesh
+ * AUTHORS: Vijay Ganesh, Trevor Hansen
  *
  * BEGIN DATE: November, 2005
  *
@@ -16,8 +16,6 @@ namespace BEEV
   bool isTseitinVariable(const ASTNode& n) {
     if (n.GetKind() == SYMBOL && n.GetType() == BOOLEAN_TYPE) {
       const char * zz = n.GetName();
-      //if the variables ARE cnf variables then dont make them
-      // decision variables.
       if (0 == strncmp("cnf", zz, 3))
         {
           return true;
@@ -171,10 +169,14 @@ namespace BEEV
           {
             bm->PrintStats(newSolver);
             bm->GetRunTimes()->stop(RunTimes::SendingToSAT);
+            CNFMgr::DeleteClauseList(cll);
             return false;
           }     
       } // End of For-loop adding the clauses 
 
+    // Free the clause list before SAT solving.
+    CNFMgr::DeleteClauseList(cll);
+
     bm->GetRunTimes()->stop(RunTimes::SendingToSAT);
     bm->GetRunTimes()->start(RunTimes::Solving);    
     newSolver.solve();
@@ -201,10 +203,6 @@ namespace BEEV
           {
             cl_size = CLAUSAL_BUCKET_LIMIT;
           }
-// 	else
-// 	  {
-// 	    cl_size = CLAUSAL_BUCKET_LIMIT-1;
-// 	  }
 
         //If no clauses of size cl_size have been seen, then create a
         //bucket for that size
@@ -234,14 +232,8 @@ namespace BEEV
     for(int count=1;it!=itend;it++, count++)
       {
         ClauseList *cl = (*it).second;
-// 	if(CLAUSAL_BUCKET_LIMIT == count)
-// 	  {
-// 	    sat = toSATandSolve(SatSolver,*cl, false, true);
-// 	  }
-// 	else
-	  {
 	    sat = toSATandSolve(SatSolver,*cl);
-	  }
+
         if(!sat)
           {
             return sat;
@@ -271,14 +263,15 @@ namespace BEEV
     bm->ASTNodeStats("after bitblasting: ", BBFormula);
     bm->GetRunTimes()->stop(RunTimes::BitBlasting);
 
-    CNFMgr* cm = new CNFMgr(bm);
-    ClauseList* cl = cm->convertToCNF(BBFormula);
+    CNFMgr cm(bm);
+    ClauseList* cl = cm.convertToCNF(BBFormula);
 
-    ClauseList* xorcl = cm->ReturnXorClauses();
+    ClauseList* xorcl = cm.ReturnXorClauses();
 
     ClauseBuckets * cb = Sort_ClauseList_IntoBuckets(cl);
+    cl->clear(); // clause buckets now point to the clauses.
+    delete cl;
     bool sat = CallSAT_On_ClauseBuckets(SatSolver, cb);
-    //bool sat = toSATandSolve(SatSolver, *cl);
 
     for (ClauseBuckets::iterator it = cb->begin(); it != cb->end(); it++)
     	delete it->second;
@@ -286,9 +279,8 @@ namespace BEEV
 
     if(!sat)
       {
-        cm->DELETE(cl);
-        cm->DELETE(xorcl);
-        delete cm;
+        CNFMgr::DeleteClauseList(*xorcl);
+    	delete xorcl;
     	return sat;
       }
 
@@ -300,9 +292,7 @@ namespace BEEV
 #endif
 
 
-    cm->DELETE(cl);
-    cm->DELETE(xorcl);
-    delete cm;
+    delete xorcl;
     return sat;
   }
 
diff --git a/src/to-sat/ToSAT.h b/src/to-sat/ToSAT.h
index dfc0667..ddea9d8 100644
--- a/src/to-sat/ToSAT.h
+++ b/src/to-sat/ToSAT.h
@@ -1,6 +1,6 @@
 // -*- c++ -*-
 /********************************************************************
- * AUTHORS: Vijay Ganesh
+ * AUTHORS: Vijay Ganesh, Trevor Hansen
  *
  * BEGIN DATE: November, 2005
  *