From ef88e39841eee4e15b1f3abc6058171b7e4b4f79 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 28 Apr 2010 10:53:16 +0000 Subject: [PATCH] Refactoring. This creates a separate ClauseList class that holds the pointers to the CNF's clauses. I've just moved stuff around, so nothing should break/ work better. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@729 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/AST.h | 8 +- src/to-sat/ClauseList.cpp | 33 +++++++ src/to-sat/ClauseList.h | 156 ++++++++++++++++++++++++++++++++ src/to-sat/Makefile | 2 +- src/to-sat/ToCNF.cpp | 186 ++++++++++++-------------------------- src/to-sat/ToCNF.h | 15 +-- src/to-sat/ToSAT.cpp | 17 ++-- 7 files changed, 262 insertions(+), 155 deletions(-) create mode 100644 src/to-sat/ClauseList.cpp create mode 100644 src/to-sat/ClauseList.h diff --git a/src/AST/AST.h b/src/AST/AST.h index ac9e829..1946d67 100644 --- 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* ClausePtr; - - // Datatype for Clauselists - typedef vector 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 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 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 + +namespace BEEV +{ + +typedef vector* ClausePtr; +typedef vector ClauseNoPtr; +typedef deque 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 836869d..6724a66 100644 --- 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 6273953..2b07f46 100644 --- 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 (**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 (); - 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 a4631c6..9428785 100644 --- a/src/to-sat/ToCNF.h +++ b/src/to-sat/ToCNF.h @@ -14,6 +14,7 @@ #include #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 8bf3f85..555660e 100644 --- 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::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; } -- 2.47.3