Refactoring. This creates a separate ClauseList class that holds the pointers to...

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

diff --git a/src/AST/AST.h b/src/AST/AST.h
index ac9e8292b712de389b56c2729b45a33c0b084ace..1946d67b7ee528f6c6ed48892bba1abc76555406 100644 (file)
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -75,12 +75,6 @@ namespace BEEV
     ASTNode::ASTNodeHasher, 
     ASTNode::ASTNodeEqual> ASTNodeToVecMap;
 
-  // Datatype for clauses
-  typedef vector<const ASTNode*>* ClausePtr;
-  
-  // Datatype for Clauselists
-  typedef vector<ClausePtr> ClauseList;
-
   //Needed for defining the MAP below
   struct ltint
   {
@@ -90,6 +84,8 @@ namespace BEEV
     }
   };
 
+  class ClauseList;
+
   //Datatype for ClauseLists
   typedef MAP<
     int,

diff --git a/src/to-sat/ClauseList.cpp b/src/to-sat/ClauseList.cpp
new file mode 100644 (file)
index 0000000..ba71a5e
--- /dev/null
+++ b/src/to-sat/ClauseList.cpp
@@ -0,0 +1,33 @@
+#include "ClauseList.h"
+#include "../AST/AST.h"
+
+namespace BEEV
+{
+
+// inplace PRODUCT of "this".
+void ClauseList::appendToAllClauses(const ASTNode* n) {
+       ClauseContainer::iterator it1 = cont.begin();
+       for (; it1 != cont.end(); it1++)
+               (*it1)->push_back(n);
+}
+
+// expects varphi2 to be just a single clause.
+void ClauseList::productInPlace(const ClauseList& varphi2) {
+       assert(1 == varphi2.size());
+       ClauseList& varphi1 = *this;
+
+       ClauseContainer::iterator it1 = varphi1.cont.begin();
+       ClauseContainer::iterator this_end = varphi1.cont.end();
+       const ClauseNoPtr::const_iterator& insert_end =
+                       varphi2.cont.front()->end();
+       const ClauseNoPtr::const_iterator& insert_begin =
+                       varphi2.cont.front()->begin();
+
+       for (; it1 != this_end; it1++) {
+               ClausePtr p = *it1;
+               p->insert(p->end(), insert_begin, insert_end);
+       }
+}
+
+
+}

diff --git a/src/to-sat/ClauseList.h b/src/to-sat/ClauseList.h
new file mode 100644 (file)
index 0000000..fe832f1
--- /dev/null
+++ b/src/to-sat/ClauseList.h
@@ -0,0 +1,156 @@
+#ifndef CLAUSELIST_H_
+#define CLAUSELIST_H_
+
+#include "../AST/AST.h"
+#include <cassert>
+
+namespace BEEV
+{
+
+typedef vector<const ASTNode*>* ClausePtr;
+typedef vector<const ASTNode*> ClauseNoPtr;
+typedef deque<ClausePtr> ClauseContainer;
+
+static bool vectorsizesort(const ClausePtr& a, const ClausePtr& b)
+{
+       return a->size() < b->size();
+}
+
+class ClauseList
+  {
+       ClauseContainer cont;
+       // No copy constructor or assignment.
+       ClauseList&  operator = (const ClauseList& other);
+       ClauseList(const ClauseList& other);
+
+  public:
+
+       void appendToAllClauses(const ASTNode* n);
+       void productInPlace(const ClauseList& varphi2);
+
+       ClauseContainer* asList() {
+               return &cont;
+       }
+
+       bool isUnit() const
+       {
+               return size() ==1 && cont[0]->size() ==1;
+       }
+
+       int size() const {
+               return cont.size();
+       }
+
+       ClauseList()
+       {
+       }
+
+       void sort()
+       {
+               std::sort (cont.begin(), cont.end(), vectorsizesort);
+       }
+
+       //Putting: cont.reserve(l->size() + cont.size());
+       // in here is a terrible idea.
+       // reserve() will increase the size of the vector to the amount reserved.
+       // If you are adding 10 clauselists of size 2, then it will increase
+       // the base container by 2, 10 times.
+       // However if you use the default growth strategy, it will grow in chunks,
+       // perhaps doubling the backing arrays size. Requiring fewer memmoves.
+       void insert(ClauseList* l) {
+               cont.insert(cont.end(), l->cont.begin(), l->cont.end());
+       }
+
+       void insertAtFront(ClauseList* l) {
+                       cont.insert(cont.begin(), l->cont.begin(), l->cont.end());
+               }
+
+       // This deletes all the clausePtrs this container points to.
+       // This isn't part of the destructor because for instance, in
+       // INPLACE_UNION, the clausePtrs are already pointed to by
+       // another ClauseContainer.
+       void deleteJustVectors() {
+               ClauseContainer::const_iterator it = cont.begin();
+               for (; it != cont.end(); it++) {
+                       delete *it;
+               }
+               cont.clear();
+       }
+
+       void push_back(ClausePtr p) {
+               cont.push_back(p);
+       }
+
+       void reserve(int v) {
+               //cont.reserve(v);
+       }
+
+       static ClauseList* UNION(const ClauseList& varphi1, const ClauseList& varphi2)
+    {
+      ClauseList* psi1 = ClauseList::COPY(varphi1);
+      ClauseList* psi2 = ClauseList::COPY(varphi2);
+      if (psi1->size() < psi2->size())
+      {
+         psi2->insert(psi1);
+         delete psi1;
+         return psi2;
+      }
+      else
+      {
+          psi1->insert(psi2);
+          delete psi2;
+          return psi1;
+      }
+    }
+
+    static void INPLACE_UNION(ClauseList* varphi1, const ClauseList& varphi2)
+    {
+
+      ClauseList* psi2 = ClauseList::COPY(varphi2);
+      varphi1->insert( psi2);
+      delete psi2;
+    }
+
+    static void NOCOPY_INPLACE_UNION(ClauseList* varphi1, ClauseList* varphi2)
+    {
+      varphi1->insert(varphi2);
+      delete varphi2;
+    }
+
+       static ClauseList* PRODUCT(const ClauseList& varphi1,
+                       const ClauseList& varphi2) {
+
+               ClauseList* psi = new ClauseList();
+               psi->reserve(varphi1.size() * varphi2.size());
+
+               ClauseContainer::const_iterator it1 = varphi1.cont.begin();
+               for (; it1 != varphi1.cont.end(); it1++) {
+                       const ClausePtr& clause1 = *it1;
+                       ClauseContainer::const_iterator it2 = varphi2.cont.begin();
+                       for (; it2 != varphi2.cont.end(); it2++) {
+                               const ClausePtr& clause2 = *it2;
+                               ClausePtr clause = new ClauseNoPtr();
+                               clause->reserve(clause1->size() + clause2->size());
+                               clause->insert(clause->end(), clause1->begin(), clause1->end());
+                               clause->insert(clause->end(), clause2->begin(), clause2->end());
+                               psi->push_back(clause);
+                       }
+               }
+               return psi;
+       }
+
+       static ClauseList* COPY(const ClauseList& varphi) {
+
+               ClauseList* psi = new ClauseList();
+               psi->reserve(varphi.size());
+
+               ClauseContainer::const_iterator it = varphi.cont.begin();
+               for (; it != varphi.cont.end(); it++) {
+                       psi->push_back(new ClauseNoPtr(**it));
+               }
+
+               return psi;
+       }
+  };
+}
+#endif /* CLAUSELIST_H_ */

diff --git a/src/to-sat/Makefile b/src/to-sat/Makefile
index 836869df9df3165b3be5b78d1f30c342fe9069dd..6724a66d55b77ff8ef483af308a71df71117226e 100644 (file)
--- a/src/to-sat/Makefile
+++ b/src/to-sat/Makefile
@@ -16,4 +16,4 @@ clean:
 depend: $(SRCS)
        @$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@
 
-#-include depend               
\ No newline at end of file
+-include depend                

diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp
index 62739539bcc3ce6816a2ac0b92ca19b83129434f..2b07f46c61cad65784fdf84d4e8f7ba80f0dfb99 100644 (file)
--- a/src/to-sat/ToCNF.cpp
+++ b/src/to-sat/ToCNF.cpp
@@ -17,16 +17,6 @@ namespace BEEV
   //############################################################
   //############################################################
 
-  void CNFMgr::DeleteClauseList(ClauseList cllp)
-  {
-    ClauseList::const_iterator iend = cllp.end();
-    for (ClauseList::const_iterator i = cllp.begin(); i < iend; i++)
-      {
-        delete *i;
-      }
-    cllp.clear();
-  } //End of DeleteClauseList
-
   bool CNFMgr::onChildDoPos(const ASTNode& varphi, unsigned int idx)
   {
     bool result = true;
@@ -255,20 +245,6 @@ namespace BEEV
   //########################################
   //utilities for clause sets
   
-
-  ClauseList* CNFMgr::COPY(const ClauseList& varphi)
-  {
-    ClauseList* psi = new ClauseList();
-    
-    ClauseList::const_iterator it = varphi.begin();
-    for (; it != varphi.end(); it++)
-      {
-        psi->push_back(new vector<const ASTNode*> (**it));
-      }
-    
-    return psi;
-  } //End of COPY()
-  
   ClauseList* CNFMgr::SINGLETON(const ASTNode& varphi)
   {
     ASTNode* copy = ASTNodeToASTNodePtr(varphi);
@@ -283,62 +259,11 @@ namespace BEEV
 
   static ASTNode GetNodeFrom_SINGLETON(ClauseList *cl)
   {
-    ClausePtr c = (*cl)[0];
+    ClausePtr c = (*(*cl).asList())[0];
     const ASTNode * a = (*c)[0];
     return *a;
   }
 
-  ClauseList* CNFMgr::UNION(const ClauseList& varphi1, 
-                            const ClauseList& varphi2)
-  {    
-    ClauseList* psi1 = COPY(varphi1);
-    ClauseList* psi2 = COPY(varphi2);
-    psi1->insert(psi1->end(), psi2->begin(), psi2->end());
-    delete psi2;
-    
-    return psi1;    
-  } //End of UNION()
-
-  void CNFMgr::INPLACE_UNION(ClauseList* varphi1, 
-                             const ClauseList& varphi2)
-  {    
-    ClauseList* psi2 = COPY(varphi2);
-    varphi1->insert(varphi1->end(), psi2->begin(), psi2->end());
-    delete psi2;
-  } //End of INPLACE_UNION()
-
-  void CNFMgr::NOCOPY_INPLACE_UNION(ClauseList* varphi1, 
-                                    ClauseList* varphi2)
-  {    
-    varphi1->insert(varphi1->end(), varphi2->begin(), varphi2->end());
-    delete varphi2;
-  } //End of NOCOPY_INPLACE_UNION
-
-  ClauseList* CNFMgr::PRODUCT(const ClauseList& varphi1, 
-                              const ClauseList& varphi2)
-  {    
-    ClauseList* psi = new ClauseList();
-    psi->reserve(varphi1.size() * varphi2.size());
-    
-    ClauseList::const_iterator it1 = varphi1.begin();
-    for (; it1 != varphi1.end(); it1++)
-      {
-        ClausePtr clause1 = *it1;
-        ClauseList::const_iterator it2 = varphi2.begin();
-        for (; it2 != varphi2.end(); it2++)
-          {
-            ClausePtr clause2 = *it2;
-            ClausePtr clause = new vector<const ASTNode*> ();
-            clause->reserve(clause1->size() + clause2->size());
-            clause->insert(clause->end(), clause1->begin(), clause1->end());
-            clause->insert(clause->end(), clause2->begin(), clause2->end());
-            psi->push_back(clause);
-          }
-      }
-    
-    return psi;
-  } //End of Product
-
   //########################################
   //########################################
   //prep. for cnf conversion
@@ -668,14 +593,14 @@ namespace BEEV
     //########################################
     
     ClauseList* cl1 = SINGLETON(bm->CreateNode(EQ, psi, t1));
-    ClauseList* cl2 = PRODUCT(*(info[varphi[0]]->clausesneg), *cl1);
+    ClauseList* cl2 = ClauseList::PRODUCT(*(info[varphi[0]]->clausesneg), *cl1);
     DELETE(cl1);
-    defs->insert(defs->end(), cl2->begin(), cl2->end());
+    defs->insert(cl2);
     
     ClauseList* cl3 = SINGLETON(bm->CreateNode(EQ, psi, t2));
-    ClauseList* cl4 = PRODUCT(*(info[varphi[0]]->clausespos), *cl3);
+    ClauseList* cl4 = ClauseList::PRODUCT(*(info[varphi[0]]->clausespos), *cl3);
     DELETE(cl3);
-    defs->insert(defs->end(), cl4->begin(), cl4->end());
+    defs->insert(cl4);
     
     return ASTNodeToASTNodePtr(psi);
   }//End of doRenameITE()
@@ -698,8 +623,8 @@ namespace BEEV
     
     ClauseList* cl1;
     cl1 = SINGLETON(bm->CreateNode(NOT, psi));
-    ClauseList* cl2 = PRODUCT(*(info[varphi]->clausespos), *cl1);
-    defs->insert(defs->end(), cl2->begin(), cl2->end());
+    ClauseList* cl2 = ClauseList::PRODUCT(*(info[varphi]->clausespos), *cl1);
+    defs->insert(cl2);
     DELETE(info[varphi]->clausespos);
     DELETE(cl1);
     delete cl2;
@@ -798,8 +723,8 @@ namespace BEEV
     
     ClauseList* cl1;
     cl1 = SINGLETON(psi);
-    ClauseList* cl2 = PRODUCT(*(info[varphi]->clausesneg), *cl1);
-    defs->insert(defs->end(), cl2->begin(), cl2->end());
+    ClauseList* cl2 = ClauseList::PRODUCT(*(info[varphi]->clausesneg), *cl1);
+    defs->insert(cl2);
     DELETE(info[varphi]->clausesneg);
     DELETE(cl1);
     delete cl2;
@@ -1030,7 +955,7 @@ namespace BEEV
                                          ClauseList* defs)
   {
     convertFormulaToCNF(varphi[0], defs);
-    info[varphi]->clausespos = COPY(*(info[varphi[0]]->clausesneg));
+    info[varphi]->clausespos = ClauseList::COPY(*(info[varphi[0]]->clausesneg));
     reduceMemoryFootprintNeg(varphi[0]);
   } //End of convertFormulaToCNFPosNOT()
 
@@ -1042,14 +967,14 @@ namespace BEEV
 
     ASTVec::const_iterator it = varphi.GetChildren().begin();
     convertFormulaToCNF(*it, defs);
-    ClauseList* psi = COPY(*(info[*it]->clausespos));
+    ClauseList* psi = ClauseList::COPY(*(info[*it]->clausespos));
 
     for (it++; it != varphi.GetChildren().end(); it++) {
       convertFormulaToCNF(*it, defs);
       CNFInfo* x = info[*it];
 
       if (sharesPos(*x) == 1) {
-        psi->insert(psi->end(),x->clausespos->begin(), x->clausespos->end());
+        psi->insert(x->clausespos);
         delete (x->clausespos);
         x->clausespos = NULL;
         if (x->clausesneg == NULL) {
@@ -1057,7 +982,7 @@ namespace BEEV
           info.erase(*it);
         }
       } else {
-        INPLACE_UNION(psi, *(x->clausespos));
+       ClauseList::INPLACE_UNION(psi, *(x->clausespos));
         reduceMemoryFootprintPos(*it);
       }
     }
@@ -1088,7 +1013,7 @@ namespace BEEV
       {
         renamesibs = true;
       }
-    psi = COPY(*clauses);
+    psi = ClauseList::COPY(*clauses);
     reduceMemoryFootprintNeg(*it);
 
     for (it++; it != varphi.GetChildren().end(); it++)
@@ -1104,7 +1029,7 @@ namespace BEEV
             renamesibs = true;
           }
         oldpsi = psi;
-        psi = PRODUCT(*psi, *clauses);
+        psi = ClauseList::PRODUCT(*psi, *clauses);
         reduceMemoryFootprintNeg(*it);
         DELETE(oldpsi);
       }
@@ -1130,7 +1055,7 @@ namespace BEEV
       {
         renamesibs = true;
       }
-    psi = COPY(*clauses);
+    psi = ClauseList::COPY(*clauses);
     reduceMemoryFootprintPos(*it);
 
     for (it++; it != varphi.GetChildren().end(); it++)
@@ -1146,7 +1071,7 @@ namespace BEEV
             renamesibs = true;
           }
         oldpsi = psi;
-        psi = PRODUCT(*psi, *clauses);
+        psi = ClauseList::PRODUCT(*psi, *clauses);
         reduceMemoryFootprintPos(*it);
         DELETE(oldpsi);
       }
@@ -1162,12 +1087,12 @@ namespace BEEV
     //****************************************
     ASTVec::const_iterator it = varphi.GetChildren().begin();
     convertFormulaToCNF(*it, defs);
-    ClauseList* psi = COPY(*(info[*it]->clausesneg));
+    ClauseList* psi = ClauseList::COPY(*(info[*it]->clausesneg));
     reduceMemoryFootprintNeg(*it);
     for (it++; it != varphi.GetChildren().end(); it++)
       {
         convertFormulaToCNF(*it, defs);
-        INPLACE_UNION(psi, *(info[*it]->clausesneg));
+        ClauseList::INPLACE_UNION(psi, *(info[*it]->clausesneg));
         reduceMemoryFootprintNeg(*it);
       }
 
@@ -1188,7 +1113,7 @@ namespace BEEV
         setDoSibRenamingPos(*x1);
       }
     convertFormulaToCNF(varphi[1], defs);
-    ClauseList* psi = PRODUCT(*(x0->clausesneg), *(x1->clausespos));
+    ClauseList* psi = ClauseList::PRODUCT(*(x0->clausesneg), *(x1->clausespos));
     reduceMemoryFootprintNeg(varphi[0]);
     reduceMemoryFootprintPos(varphi[1]);
     info[varphi]->clausespos = psi;
@@ -1215,9 +1140,9 @@ namespace BEEV
         setDoSibRenamingPos(*x2);
       }
     convertFormulaToCNF(varphi[2], defs);
-    ClauseList* psi1 = PRODUCT(*(x0->clausesneg), *(x1->clausespos));
-    ClauseList* psi2 = PRODUCT(*(x0->clausespos), *(x2->clausespos));
-    NOCOPY_INPLACE_UNION(psi1, psi2);
+    ClauseList* psi1 = ClauseList::PRODUCT(*(x0->clausesneg), *(x1->clausespos));
+    ClauseList* psi2 = ClauseList::PRODUCT(*(x0->clausespos), *(x2->clausespos));
+    ClauseList::NOCOPY_INPLACE_UNION(psi1, psi2);
     reduceMemoryFootprintNeg(varphi[0]);
     reduceMemoryFootprintPos(varphi[1]);
     reduceMemoryFootprintPos(varphi[0]);
@@ -1313,12 +1238,12 @@ namespace BEEV
           }
 
         psi1 = 
-          PRODUCT(*(info[varphi[idx]]->clausespos), 
+                       ClauseList::PRODUCT(*(info[varphi[idx]]->clausespos),
                   *(info[varphi[idx + 1]]->clausespos));
         psi2 = 
-          PRODUCT(*(info[varphi[idx]]->clausesneg), 
+                       ClauseList::PRODUCT(*(info[varphi[idx]]->clausesneg),
                   *(info[varphi[idx + 1]]->clausesneg));
-        NOCOPY_INPLACE_UNION(psi1, psi2);
+        ClauseList::NOCOPY_INPLACE_UNION(psi1, psi2);
 
         psi = psi1;
       }
@@ -1344,11 +1269,11 @@ namespace BEEV
             setDoSibRenamingNeg(*info[varphi[idx]]);
           }
 
-        psi1 = PRODUCT(*(info[varphi[idx]]->clausespos), *theta1);
-        psi2 = PRODUCT(*(info[varphi[idx]]->clausesneg), *theta2);
+        psi1 = ClauseList::PRODUCT(*(info[varphi[idx]]->clausespos), *theta1);
+        psi2 = ClauseList::PRODUCT(*(info[varphi[idx]]->clausesneg), *theta2);
         DELETE(theta1);
         DELETE(theta2);
-        NOCOPY_INPLACE_UNION(psi1, psi2);
+        ClauseList::NOCOPY_INPLACE_UNION(psi1, psi2);
 
         psi = psi1;
       }
@@ -1406,7 +1331,7 @@ namespace BEEV
                                          ClauseList* defs)
   {
     convertFormulaToCNF(varphi[0], defs);
-    info[varphi]->clausesneg = COPY(*(info[varphi[0]]->clausespos));
+    info[varphi]->clausesneg = ClauseList::COPY(*(info[varphi[0]]->clausespos));
     reduceMemoryFootprintPos(varphi[0]);
   } //End of convertFormulaToCNFNegNOT()
 
@@ -1429,7 +1354,7 @@ namespace BEEV
       {
         renamesibs = true;
       }
-    psi = COPY(*clauses);
+    psi = ClauseList::COPY(*clauses);
     reduceMemoryFootprintNeg(*it);
 
     for (it++; it != varphi.GetChildren().end(); it++)
@@ -1445,7 +1370,7 @@ namespace BEEV
             renamesibs = true;
           }
         oldpsi = psi;
-        psi = PRODUCT(*psi, *clauses);
+        psi = ClauseList::PRODUCT(*psi, *clauses);
         reduceMemoryFootprintNeg(*it);
         DELETE(oldpsi);
       }
@@ -1461,12 +1386,12 @@ namespace BEEV
     //****************************************
     ASTVec::const_iterator it = varphi.GetChildren().begin();
     convertFormulaToCNF(*it, defs);
-    ClauseList* psi = COPY(*(info[*it]->clausespos));
+    ClauseList* psi = ClauseList::COPY(*(info[*it]->clausespos));
     reduceMemoryFootprintPos(*it);
     for (it++; it != varphi.GetChildren().end(); it++)
       {
         convertFormulaToCNF(*it, defs);
-        INPLACE_UNION(psi, *(info[*it]->clausespos));
+        ClauseList::INPLACE_UNION(psi, *(info[*it]->clausespos));
         reduceMemoryFootprintPos(*it);
       }
 
@@ -1481,19 +1406,18 @@ namespace BEEV
     //****************************************
     ASTVec::const_iterator it = varphi.GetChildren().begin();
     convertFormulaToCNF(*it, defs);
-    ClauseList* psi = COPY(*(info[*it]->clausesneg));
+    ClauseList* psi = ClauseList::COPY(*(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));
+         ClauseList::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());
+        psi->insert(x->clausesneg);
         // Copied from reduceMemoryFootprintNeg
         delete x->clausesneg;
         x->clausesneg = NULL;
@@ -1526,7 +1450,7 @@ namespace BEEV
       {
         renamesibs = true;
       }
-    psi = COPY(*clauses);
+    psi = ClauseList::COPY(*clauses);
     reduceMemoryFootprintPos(*it);
 
     for (it++; it != varphi.GetChildren().end(); it++)
@@ -1542,7 +1466,7 @@ namespace BEEV
             renamesibs = true;
           }
         oldpsi = psi;
-        psi = PRODUCT(*psi, *clauses);
+        psi = ClauseList::PRODUCT(*psi, *clauses);
         reduceMemoryFootprintPos(*it);
         DELETE(oldpsi);
       }
@@ -1560,7 +1484,7 @@ namespace BEEV
     CNFInfo* x1 = info[varphi[1]];
     convertFormulaToCNF(varphi[0], defs);
     convertFormulaToCNF(varphi[1], defs);
-    ClauseList* psi = UNION(*(x0->clausespos), *(x1->clausesneg));
+    ClauseList* psi = ClauseList::UNION(*(x0->clausespos), *(x1->clausesneg));
     info[varphi]->clausesneg = psi;
     reduceMemoryFootprintPos(varphi[0]);
     reduceMemoryFootprintNeg(varphi[1]);
@@ -1587,9 +1511,9 @@ namespace BEEV
         setDoSibRenamingNeg(*x2);
       }
     convertFormulaToCNF(varphi[2], defs);
-    ClauseList* psi1 = PRODUCT(*(x0->clausesneg), *(x1->clausesneg));
-    ClauseList* psi2 = PRODUCT(*(x0->clausespos), *(x2->clausesneg));
-    NOCOPY_INPLACE_UNION(psi1, psi2);
+    ClauseList* psi1 = ClauseList::PRODUCT(*(x0->clausesneg), *(x1->clausesneg));
+    ClauseList* psi2 = ClauseList::PRODUCT(*(x0->clausespos), *(x2->clausesneg));
+    ClauseList::NOCOPY_INPLACE_UNION(psi1, psi2);
     reduceMemoryFootprintNeg(varphi[0]);
     reduceMemoryFootprintNeg(varphi[1]);
     reduceMemoryFootprintPos(varphi[0]);
@@ -1689,12 +1613,12 @@ namespace BEEV
           }
 
         psi1 = 
-          PRODUCT(*(info[varphi[idx]]->clausesneg),
+          ClauseList::PRODUCT(*(info[varphi[idx]]->clausesneg),
                   *(info[varphi[idx + 1]]->clausespos));
         psi2 = 
-          PRODUCT(*(info[varphi[idx]]->clausespos),
+                       ClauseList::PRODUCT(*(info[varphi[idx]]->clausespos),
                   *(info[varphi[idx + 1]]->clausesneg));
-        NOCOPY_INPLACE_UNION(psi1, psi2);
+        ClauseList::NOCOPY_INPLACE_UNION(psi1, psi2);
 
         psi = psi1;
       }
@@ -1722,11 +1646,11 @@ namespace BEEV
             setDoSibRenamingPos(*info[varphi[idx]]);
           }
 
-        psi1 = PRODUCT(*(info[varphi[idx]]->clausesneg), *theta1);
-        psi2 = PRODUCT(*(info[varphi[idx]]->clausespos), *theta2);
+        psi1 = ClauseList::PRODUCT(*(info[varphi[idx]]->clausesneg), *theta1);
+        psi2 = ClauseList::PRODUCT(*(info[varphi[idx]]->clausespos), *theta2);
         DELETE(theta1);
         DELETE(theta2);
-        NOCOPY_INPLACE_UNION(psi1, psi2);
+        ClauseList::NOCOPY_INPLACE_UNION(psi1, psi2);
 
         psi = psi1;
       }
@@ -1856,7 +1780,7 @@ namespace BEEV
     ClauseList* defs = SINGLETON(dummy_true_var);
     convertFormulaToCNF(varphi, defs);
     ClauseList* top = info[varphi]->clausespos;
-    defs->insert(defs->begin() + 1, top->begin(), top->end());
+    defs->insertAtFront(top);
 
     cleanup(varphi);
     bm->GetRunTimes()->stop(RunTimes::CNFConversion);
@@ -1878,13 +1802,16 @@ namespace BEEV
     return clausesxor;
   }
 
+  //
   void CNFMgr::DELETE(ClauseList* varphi)
   {
-    DeleteClauseList(*varphi);
-    delete varphi;
+        varphi->deleteJustVectors();
+     delete varphi;
+     varphi = NULL;
   } //End of DELETE()
 
 
+  /*
   void CNFMgr::PrintClauseList(ostream& os, ClauseList& cll)
   {
     int num_clauses = cll.size();
@@ -1900,5 +1827,6 @@ namespace BEEV
         os << endl 
            << "-------------------------------------------" << endl;
       }
-  } //end of PrintClauseList()  
+  } //end of PrintClauseList()
+  */
 } // end namespace BEEV

diff --git a/src/to-sat/ToCNF.h b/src/to-sat/ToCNF.h
index a4631c63f74ab4f3b258c1c99a145e57c88f0b06..9428785929869a9babb4d6a18124b05a3de8d3fb 100644 (file)
--- a/src/to-sat/ToCNF.h
+++ b/src/to-sat/ToCNF.h
@@ -14,6 +14,7 @@
 #include <cassert>
 #include "../AST/AST.h"
 #include "../STPManager/STPManager.h"
+#include "ClauseList.h"
 
 namespace BEEV
 {
@@ -132,19 +133,9 @@ namespace BEEV
     //########################################
     //utilities for clause sets
 
-    ClauseList* COPY(const ClauseList& varphi);    
 
     ClauseList* SINGLETON(const ASTNode& varphi);    
 
-    ClauseList* UNION(const ClauseList& varphi1, const ClauseList& varphi2);    
-
-    void INPLACE_UNION(ClauseList* varphi1, const ClauseList& varphi2);    
-
-    void NOCOPY_INPLACE_UNION(ClauseList* varphi1, ClauseList* varphi2);   
-
-    ClauseList* PRODUCT(const ClauseList& varphi1, 
-                        const ClauseList& varphi2);    
-
     //########################################
     //########################################
     //prep. for cnf conversion
@@ -260,10 +251,10 @@ namespace BEEV
 
     // 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);
+    //void PrintClauseList(ostream& os, ClauseList& cll);
   }; // end of CNFMgr class
 };//end of namespace
 #endif

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 8bf3f85c48b6da334653dc9694d6c1887505dbb4..555660ebf2f8b830a3e9f58615ccc6ae1dbb54c9 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -90,8 +90,10 @@ namespace BEEV
 #endif
       }
 
+       ClauseContainer& cc = *cll.asList();
+
     //iterate through the list (conjunction) of ASTclauses cll
-    ClauseList::const_iterator i = cll.begin(), iend = cll.end();    
+    ClauseContainer::const_iterator i = cc.begin(), iend = cc.end();
     for (int count=0, flag=0; i != iend; i++)
       {
         //Clause for the SATSolver
@@ -166,7 +168,7 @@ namespace BEEV
           {
             bm->PrintStats(newSolver);
             bm->GetRunTimes()->stop(RunTimes::SendingToSAT);
-            CNFMgr::DeleteClauseList(cll);
+            cll.deleteJustVectors();
             return false;
           }     
       } // End of For-loop adding the clauses 
@@ -186,7 +188,7 @@ namespace BEEV
                file.open(fileName.str().c_str());
 
                file << "p cnf " << newSolver.nVars() << " " << cll.size() << endl;
-               i = cll.begin(), iend = cll.end();
+               i = cc.begin(), iend = cc.end();
                for (; i != iend; i++)
                {
                        vector<const ASTNode*>::iterator j = (*i)->begin(), jend =
@@ -214,7 +216,7 @@ namespace BEEV
        }
 
     // Free the clause list before SAT solving.
-    CNFMgr::DeleteClauseList(cll);
+    cll.deleteJustVectors();
 
     bm->GetRunTimes()->stop(RunTimes::SendingToSAT);
     bm->GetRunTimes()->start(RunTimes::Solving);    
@@ -231,9 +233,10 @@ namespace BEEV
   static ClauseBuckets * Sort_ClauseList_IntoBuckets(ClauseList * cl)
   {
     ClauseBuckets * cb = new ClauseBuckets();
+    ClauseContainer* cc = cl->asList();
 
     //Sort the clauses, and bucketize by the size of the clauses
-    for(ClauseList::iterator it = cl->begin(), itend = cl->end();
+    for(ClauseContainer::iterator it = cc->begin(), itend = cc->end();
         it!=itend; it++)
       {
         ClausePtr cptr = *it;
@@ -318,7 +321,7 @@ namespace BEEV
     ClauseList* xorcl = cm.ReturnXorClauses();
 
     ClauseBuckets * cb = Sort_ClauseList_IntoBuckets(cl);
-    cl->clear(); // clause buckets now point to the clauses.
+    cl->asList()->clear(); // clause buckets now point to the clauses.
     delete cl;
     bool sat = CallSAT_On_ClauseBuckets(SatSolver, cb);
 
@@ -328,7 +331,7 @@ namespace BEEV
 
     if(!sat)
       {
-        CNFMgr::DeleteClauseList(*xorcl);
+       xorcl->deleteJustVectors();
        delete xorcl;
        return sat;
       }