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 406ae2bd737df8cbfb77305b6c4610e2c3e42ed2..0af39f7463fdc4847ecead7e98f858818ab7e0d5 100644 (file)
--- 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 62d450f6eb7d6d78624f7abdbdaa84648b1f748a..76afc0c8961a55cd9747a63cef117127775d57d1 100644 (file)
--- 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 02db33fb9175551e94e76c8def46b1bbe2d0b4d2..c3c2de5cc9e8988554175ce222a1434f6b051e89 100644 (file)
--- 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 dfc0667d17dcac9039bb456cf8cedfda4ffa716c..ddea9d8cec15b1e2767bd2de4bb4453b992e84ad 100644 (file)
--- 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
  *