From ccec2c7806cddbdd3c8b729e84bc409fdabd2ab5 Mon Sep 17 00:00:00 2001 From: msoos Date: Fri, 2 Jul 2010 14:35:28 +0000 Subject: [PATCH] Updating CryptoMiniSat2 git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@907 e59a4935-1847-0410-ae03-e826735625c1 --- src/sat/cryptominisat2/CSet.h | 11 +- src/sat/cryptominisat2/Clause.h | 234 ++------ src/sat/cryptominisat2/ClauseAllocator.cpp | 361 ++++++++++++ src/sat/cryptominisat2/ClauseAllocator.h | 95 +++ src/sat/cryptominisat2/ClauseCleaner.cpp | 31 +- src/sat/cryptominisat2/Conglomerate.cpp | 526 ----------------- src/sat/cryptominisat2/Conglomerate.h | 125 ---- src/sat/cryptominisat2/FailedVarSearcher.cpp | 320 +--------- src/sat/cryptominisat2/FailedVarSearcher.h | 18 +- src/sat/cryptominisat2/Gaussian.cpp | 18 +- src/sat/cryptominisat2/Gaussian.h | 2 +- src/sat/cryptominisat2/Makefile | 8 +- src/sat/cryptominisat2/OnlyNonLearntBins.cpp | 155 +++++ src/sat/cryptominisat2/OnlyNonLearntBins.h | 54 ++ src/sat/cryptominisat2/PartFinder.cpp | 5 +- src/sat/cryptominisat2/PartHandler.cpp | 15 +- src/sat/cryptominisat2/PartHandler.h | 2 + src/sat/cryptominisat2/SmallPtr.cpp | 17 - src/sat/cryptominisat2/SmallPtr.h | 277 --------- src/sat/cryptominisat2/Solver.cpp | 573 ++++++++---------- src/sat/cryptominisat2/Solver.h | 164 +++++- src/sat/cryptominisat2/SolverTypes.h | 4 + src/sat/cryptominisat2/Subsumer.cpp | 589 ++++--------------- src/sat/cryptominisat2/Subsumer.h | 33 +- src/sat/cryptominisat2/UselessBinRemover.cpp | 199 +++++++ src/sat/cryptominisat2/UselessBinRemover.h | 53 ++ src/sat/cryptominisat2/VERSION | 2 +- src/sat/cryptominisat2/VarReplacer.cpp | 22 +- src/sat/cryptominisat2/VarReplacer.h | 4 + src/sat/cryptominisat2/XSet.h | 2 +- src/sat/cryptominisat2/XorFinder.cpp | 4 +- src/sat/cryptominisat2/XorSubsumer.cpp | 86 ++- src/sat/cryptominisat2/XorSubsumer.h | 9 +- src/sat/cryptominisat2/constants.h | 8 +- src/sat/cryptominisat2/pool.hpp | 584 ------------------ src/sat/cryptominisat2/poolfwd.hpp | 70 --- src/sat/cryptominisat2/singleton.hpp | 107 ---- 37 files changed, 1619 insertions(+), 3168 deletions(-) create mode 100644 src/sat/cryptominisat2/ClauseAllocator.cpp create mode 100644 src/sat/cryptominisat2/ClauseAllocator.h delete mode 100644 src/sat/cryptominisat2/Conglomerate.cpp delete mode 100644 src/sat/cryptominisat2/Conglomerate.h create mode 100644 src/sat/cryptominisat2/OnlyNonLearntBins.cpp create mode 100644 src/sat/cryptominisat2/OnlyNonLearntBins.h delete mode 100644 src/sat/cryptominisat2/SmallPtr.cpp delete mode 100644 src/sat/cryptominisat2/SmallPtr.h create mode 100644 src/sat/cryptominisat2/UselessBinRemover.cpp create mode 100644 src/sat/cryptominisat2/UselessBinRemover.h delete mode 100644 src/sat/cryptominisat2/pool.hpp delete mode 100644 src/sat/cryptominisat2/poolfwd.hpp delete mode 100644 src/sat/cryptominisat2/singleton.hpp diff --git a/src/sat/cryptominisat2/CSet.h b/src/sat/cryptominisat2/CSet.h index cf8661a..fb6f84b 100644 --- a/src/sat/cryptominisat2/CSet.h +++ b/src/sat/cryptominisat2/CSet.h @@ -19,14 +19,6 @@ using namespace MINISAT; class Clause; -template -uint32_t calcAbstraction(const T& ps) { - uint32_t abstraction = 0; - for (uint32_t i = 0; i != ps.size(); i++) - abstraction |= 1 << (ps[i].toInt() & 31); - return abstraction; -} - //#pragma pack(push) //#pragma pack(1) class ClauseSimp @@ -131,6 +123,7 @@ class CSet { } }; +#endif //CSET_H + }; //NAMESPACE MINISAT -#endif //CSET_H \ No newline at end of file diff --git a/src/sat/cryptominisat2/Clause.h b/src/sat/cryptominisat2/Clause.h index fab2159..ec515fc 100644 --- a/src/sat/cryptominisat2/Clause.h +++ b/src/sat/cryptominisat2/Clause.h @@ -24,9 +24,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifdef _MSC_VER #include #else -#include "SmallPtr.h" #include #endif //_MSC_VER + #include #include #include @@ -34,17 +34,15 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "SolverTypes.h" #include "PackedRow.h" #include "constants.h" -#include "SmallPtr.h" -#ifdef USE_POOLS -#include "pool.hpp" -#endif //USE_POOLS -#ifndef uint -#define uint unsigned int -#endif - -//#define USE_4POOLS - -using std::vector; +#include "ClauseAllocator.h" + +template +uint32_t calcAbstraction(const T& ps) { + uint32_t abstraction = 0; + for (uint32_t i = 0; i != ps.size(); i++) + abstraction |= 1 << (ps[i].toInt() & 31); + return abstraction; +} namespace MINISAT { @@ -71,13 +69,8 @@ protected: uint32_t isXorClause:1; uint32_t subsume0Done:1; uint32_t isRemoved:1; - #ifdef USE_POOLS - uint32_t wasTriOriginallyInt:1; - uint32_t wasBinOriginallyInt:1; - #ifdef USE_4POOLS - uint32_t wasQuadOriginallyInt:1; - #endif //USE_4POOLS - #endif //USE_POOLS + uint32_t isFreed:1; + uint32_t wasBinInternal:1; uint32_t mySize:20; union {uint32_t act; uint32_t abst;} extra; @@ -94,6 +87,8 @@ public: template Clause(const V& ps, const uint _group, const bool learnt) { + wasBinInternal = (ps.size() == 2); + isFreed = false; isXorClause = false; strenghtened = false; sorted = false; @@ -103,25 +98,17 @@ public: isLearnt = learnt; isRemoved = false; setGroup(_group); - #ifdef USE_POOLS - setAllocSize(); - #endif //USE_POOLS - for (uint i = 0; i < ps.size(); i++) data[i] = ps[i]; + memcpy(data, ps.getData(), ps.size()*sizeof(Lit)); if (learnt) { extra.act = 0; oldActivityInter = 0; } else - calcAbstraction(); + calcAbstractionClause(); } public: - #ifndef _MSC_VER - // -- use this function instead: - template - friend Clause* Clause_new(const T& ps, const uint group, const bool learnt = false); - friend Clause* Clause_new(Clause& c); - #endif //_MSC_VER + friend class ClauseAllocator; const uint size () const { return mySize; @@ -150,7 +137,6 @@ public: return oldActivityInter; } - const bool getStrenghtened() const { return strenghtened; } @@ -189,14 +175,14 @@ public: return subsume0Done; } - Lit& operator [] (uint32_t i) { + Lit& operator [] (uint32_t i) { return data[i]; } - const Lit& operator [] (uint32_t i) const { + const Lit& operator [] (uint32_t i) const { return data[i]; } - void setActivity(uint32_t i) { + void setActivity(uint32_t i) { extra.act = i; } @@ -204,13 +190,13 @@ public: return extra.act; } - void makeNonLearnt() { + void makeNonLearnt() { assert(isLearnt); isLearnt = false; - calcAbstraction(); + calcAbstractionClause(); } - void makeLearnt(const uint32_t newActivity) { + void makeLearnt(const uint32_t newActivity) { extra.act = newActivity; oldActivityInter = 0; isLearnt = true; @@ -220,19 +206,20 @@ public: { remove(*this, p); sorted = false; - calcAbstraction(); + calcAbstractionClause(); } - void calcAbstraction() { + void calcAbstractionClause() { assert(!learnt()); - extra.abst = 0; - for (uint32_t i = 0; i != size(); i++) - extra.abst |= 1 << (data[i].toInt() & 31); + extra.abst = calcAbstraction(*this);; } uint32_t getAbst() { - return extra.abst; + if (learnt()) + return calcAbstraction(*this); + else + return extra.abst; } const Lit* getData () const { @@ -284,57 +271,27 @@ public: const bool removed() const { return isRemoved; } - #ifdef USE_POOLS - const bool wasTriOriginally() const - { - return wasTriOriginallyInt; + + void setFreed() { + isFreed = true; } - const bool wasBinOriginally() const - { - return wasBinOriginallyInt; + + const bool freed() const { + return isFreed; } - #ifdef USE_4POOLS - const bool wasQuadOriginally() const - { - return wasQuadOriginallyInt; + + const bool wasBin() const { + return wasBinInternal; } - #endif //USE_4POOLS - void setAllocSize() - { - wasTriOriginallyInt = false; - wasBinOriginallyInt = false; - #ifdef USE_4POOLS - wasQuadOriginallyInt = false; - #endif //USE_4POOLS - switch(size()) { - case 2: - wasBinOriginallyInt = true; - break; - case 3: - wasTriOriginallyInt = true; - break; - #ifdef USE_4POOLS - case 4: - wasQuadOriginallyInt = true; - break; - case 5: - wasQuadOriginallyInt = true; - break; - #endif //USE_4POOLS - } + + void setWasBin(const bool toSet) { + wasBinInternal = toSet; } - #endif //USE_POOLS }; class XorClause : public Clause { - -#ifdef _MSC_VER -public: -#else //_MSC_VER protected: -#endif //_MSC_VER - // NOTE: This constructor cannot be used directly (doesn't allocate enough memory). template XorClause(const V& ps, const bool inverted, const uint _group) : @@ -346,11 +303,7 @@ protected: } public: - #ifndef _MSC_VER - // -- use this function instead: - template - friend XorClause* XorClause_new(const V& ps, const bool inverted, const uint group); - #endif //_MSC_VER + friend class ClauseAllocator; inline bool xor_clause_inverted() const { @@ -384,109 +337,18 @@ public: friend class MatrixFinder; }; -#ifdef USE_POOLS -extern boost::pool<> clausePoolTri; -extern boost::pool<> clausePoolBin; -#ifdef USE_4POOLS -extern boost::pool<> clausePoolQuad; -#endif //USE_4POOLS -#endif //USE_POOLS - -template -inline void* allocEnough(const T& ps) -{ - void* mem; - switch(ps.size()) { - #ifdef USE_POOLS - case 2: - mem = clausePoolBin.malloc(); - break; - case 3: - mem = clausePoolTri.malloc(); - break; - #ifdef USE_4POOLS - case 4: - mem = clausePoolQuad.malloc(); - break; - case 5: - mem = clausePoolQuad.malloc(); - break; - #endif //USE_4POOLS - #endif //USE_POOLS - default: - mem = malloc(sizeof(Clause) + sizeof(Lit)*(ps.size())); - break; - } - - return mem; -} - -template -Clause* Clause_new(const T& ps, const uint group, const bool learnt = false) -{ - void* mem = allocEnough(ps); - Clause* real= new (mem) Clause(ps, group, learnt); - return real; -} - -template -XorClause* XorClause_new(const T& ps, const bool inverted, const uint group) -{ - void* mem = allocEnough(ps); - XorClause* real= new (mem) XorClause(ps, inverted, group); - return real; -} - -inline Clause* Clause_new(Clause& c) -{ - void* mem = allocEnough(c); - //Clause* real= new (mem) Clause(ps, group, learnt); - memcpy(mem, &c, sizeof(Clause)+sizeof(Lit)*c.size()); - Clause& c2 = *(Clause*)mem; - #ifdef USE_POOLS - c2.setAllocSize(); - #endif //USE_POOLS - - return &c2; -} - -inline void clauseFree(Clause* c) -{ - #ifdef USE_POOLS - if (c->wasTriOriginally()) - clausePoolTri.free(c); - else if (c->wasBinOriginally()) - clausePoolBin.free(c); - #ifdef USE_4POOLS - else if (c->wasQuadOriginally()) - clausePoolQuad.free(c); - #endif //USE_4POOLS - else - #endif //USE_POOLS - free(c); -} - -#ifdef _MSC_VER -typedef Clause* ClausePtr; -typedef XorClause* XorClausePtr; -#else -typedef sptr ClausePtr; -typedef sptr XorClausePtr; -#endif //_MSC_VER - -#pragma pack(push) -#pragma pack(1) class WatchedBin { public: - WatchedBin(Clause *_clause, Lit _impliedLit) : clause(_clause), impliedLit(_impliedLit) {}; - ClausePtr clause; + WatchedBin(Lit _impliedLit) : impliedLit(_impliedLit) {}; Lit impliedLit; }; +#pragma pack(push) +#pragma pack(1) class Watched { public: - Watched(Clause *_clause, Lit _blockedLit) : clause(_clause), blockedLit(_blockedLit) {}; - ClausePtr clause; + Watched(ClauseOffset _clause, Lit _blockedLit) : clause(_clause), blockedLit(_blockedLit) {}; + ClauseOffset clause; Lit blockedLit; }; #pragma pack(pop) diff --git a/src/sat/cryptominisat2/ClauseAllocator.cpp b/src/sat/cryptominisat2/ClauseAllocator.cpp new file mode 100644 index 0000000..826ae72 --- /dev/null +++ b/src/sat/cryptominisat2/ClauseAllocator.cpp @@ -0,0 +1,361 @@ +/*********************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +This program is free software: you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation, either version 3 of the License, or +(at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program. If not, see . +************************************************************************/ + +#include "ClauseAllocator.h" + +#include +#include +#include "assert.h" +#include "SolverTypes.h" +#include "Clause.h" +#include "Solver.h" +#include "time_mem.h" +#include "Subsumer.h" +#include "XorSubsumer.h" +//#include "VarReplacer.h" +#include "PartHandler.h" + +namespace MINISAT +{ +using namespace MINISAT; + +ClauseAllocator::ClauseAllocator() : + clausePoolBin(sizeof(Clause) + 2*sizeof(Lit)) +{} + +template +Clause* ClauseAllocator::Clause_new(const T& ps, const unsigned int group, const bool learnt) +{ + void* mem = allocEnough(ps.size()); + Clause* real= new (mem) Clause(ps, group, learnt); + //assert(!(ps.size() == 2 && !real->wasBin())); + + return real; +} +template Clause* ClauseAllocator::Clause_new(const vec& ps, const unsigned int group, const bool learnt); +template Clause* ClauseAllocator::Clause_new(const Clause& ps, const unsigned int group, const bool learnt); +template Clause* ClauseAllocator::Clause_new(const XorClause& ps, const unsigned int group, const bool learnt); + +template +XorClause* ClauseAllocator::XorClause_new(const T& ps, const bool inverted, const unsigned int group) +{ + void* mem = allocEnough(ps.size()); + XorClause* real= new (mem) XorClause(ps, inverted, group); + //assert(!(ps.size() == 2 && !real->wasBin())); + + return real; +} +template XorClause* ClauseAllocator::XorClause_new(const vec& ps, const bool inverted, const unsigned int group); +template XorClause* ClauseAllocator::XorClause_new(const XorClause& ps, const bool inverted, const unsigned int group); + +Clause* ClauseAllocator::Clause_new(Clause& c) +{ + void* mem = allocEnough(c.size()); + memcpy(mem, &c, sizeof(Clause)+sizeof(Lit)*c.size()); + Clause& c2 = *(Clause*)mem; + c2.setWasBin(c.size() == 2); + //assert(!(c.size() == 2 && !c2.wasBin())); + + return &c2; +} + +#define MIN_LIST_SIZE (300000 * (sizeof(Clause) + 4*sizeof(Lit))) + +void* ClauseAllocator::allocEnough(const uint32_t size) +{ + assert(sizes.size() == dataStarts.size()); + assert(maxSizes.size() == dataStarts.size()); + assert(origClauseSizes.size() == dataStarts.size()); + + assert(sizeof(Clause)%sizeof(uint32_t) == 0); + assert(sizeof(Lit)%sizeof(uint32_t) == 0); + + if (size == 2) { + return clausePoolBin.malloc(); + } + + uint32_t needed = sizeof(Clause)+sizeof(Lit)*size; + bool found = false; + uint32_t which = std::numeric_limits::max(); + for (uint32_t i = 0; i < sizes.size(); i++) { + if (sizes[i] + needed < maxSizes[i]) { + found = true; + which = i; + break; + } + } + + if (!found) { + //std::cout << "c New list in ClauseAllocator" << std::endl; + uint32_t nextSize; //number of BYTES to allocate + if (maxSizes.size() != 0) + nextSize = maxSizes[maxSizes.size()-1]*3*sizeof(uint32_t); + else + nextSize = MIN_LIST_SIZE; + assert(needed < nextSize); + + uint32_t *dataStart = (uint32_t*)malloc(nextSize); + assert(dataStart != NULL); + dataStarts.push(dataStart); + sizes.push(0); + maxSizes.push(nextSize/sizeof(uint32_t)); + origClauseSizes.push(); + currentlyUsedSize.push(0); + which = dataStarts.size()-1; + } + /*std::cout + << "selected list = " << which + << " size = " << sizes[which] + << " maxsize = " << maxSizes[which] + << " diff = " << maxSizes[which] - sizes[which] << std::endl;*/ + + assert(which != std::numeric_limits::max()); + Clause* pointer = (Clause*)(dataStarts[which] + sizes[which]); + sizes[which] += needed/sizeof(uint32_t); + currentlyUsedSize[which] += needed/sizeof(uint32_t); + origClauseSizes[which].push(needed/sizeof(uint32_t)); + + return pointer; +} + +const ClauseOffset ClauseAllocator::getOffset(const Clause* ptr) const +{ + uint32_t outerOffset = getOuterOffset(ptr); + uint32_t interOffset = getInterOffset(ptr, outerOffset); + return combineOuterInterOffsets(outerOffset, interOffset); +} + +inline const ClauseOffset ClauseAllocator::combineOuterInterOffsets(const uint32_t outerOffset, const uint32_t interOffset) const +{ + return (outerOffset | (interOffset<<4)); +} + +inline uint32_t ClauseAllocator::getOuterOffset(const Clause* ptr) const +{ + uint32_t which = std::numeric_limits::max(); + for (uint32_t i = 0; i < sizes.size(); i++) { + if ((uint32_t*)ptr >= dataStarts[i] && (uint32_t*)ptr < dataStarts[i] + maxSizes[i]) + which = i; + } + assert(which != std::numeric_limits::max()); + + return which; +} + +inline uint32_t ClauseAllocator::getInterOffset(const Clause* ptr, uint32_t outerOffset) const +{ + return ((uint32_t*)ptr - dataStarts[outerOffset]); +} + +void ClauseAllocator::clauseFree(Clause* c) +{ + if (c->wasBin()) { + clausePoolBin.free(c); + } else { + c->setFreed(); + uint32_t outerOffset = getOuterOffset(c); + //uint32_t interOffset = getInterOffset(c, outerOffset); + currentlyUsedSize[outerOffset] -= (sizeof(Clause) + c->size()*sizeof(Lit))/sizeof(uint32_t); + //above should be + //origClauseSizes[outerOffset][interOffset] + //but it cannot be :( + } +} + +struct NewPointerAndOffset { + Clause* newPointer; + uint32_t newOffset; +}; + +void ClauseAllocator::consolidate(Solver* solver) +{ + double myTime = cpuTime(); + + //if (dataStarts.size() > 2) { + uint32_t sum = 0; + for (uint32_t i = 0; i < sizes.size(); i++) { + sum += currentlyUsedSize[i]; + } + uint32_t sumAlloc = 0; + for (uint32_t i = 0; i < sizes.size(); i++) { + sumAlloc += sizes[i]; + } + + //std::cout << "c ratio:" << (double)sum/(double)sumAlloc << std::endl; + + if ((double)sum/(double)sumAlloc > 0.7 /*&& sum > 10000000*/) { + if (solver->verbosity >= 2) { + std::cout << "c Not consolidating memory." << std::endl; + } + return; + } + + + uint32_t newMaxSize = std::max(sum*2*sizeof(uint32_t), MIN_LIST_SIZE); + uint32_t* newDataStarts = (uint32_t*)malloc(newMaxSize); + newMaxSize /= sizeof(uint32_t); + uint32_t newSize = 0; + vec newOrigClauseSizes; + //} + + map oldToNewPointer; + map oldToNewOffset; + + uint32_t* newDataStartsPointer = newDataStarts; + for (uint32_t i = 0; i < dataStarts.size(); i++) { + uint32_t currentLoc = 0; + for (uint32_t i2 = 0; i2 < origClauseSizes[i].size(); i2++) { + Clause* oldPointer = (Clause*)(dataStarts[i] + currentLoc); + if (!oldPointer->freed()) { + uint32_t sizeNeeded = sizeof(Clause) + oldPointer->size()*sizeof(Lit); + memcpy(newDataStartsPointer, dataStarts[i] + currentLoc, sizeNeeded); + + oldToNewPointer[oldPointer] = (Clause*)newDataStartsPointer; + oldToNewOffset[combineOuterInterOffsets(i, currentLoc)] = combineOuterInterOffsets(0, newSize); + + newSize += sizeNeeded/sizeof(uint32_t); + newOrigClauseSizes.push(sizeNeeded/sizeof(uint32_t)); + newDataStartsPointer += sizeNeeded/sizeof(uint32_t); + } + + currentLoc += origClauseSizes[i][i2]; + } + } + assert(newSize < newMaxSize); + assert(newSize <= newMaxSize/2); + + updateOffsets(solver->watches, oldToNewOffset); + updateOffsetsXor(solver->xorwatches, oldToNewOffset); + + updatePointers(solver->clauses, oldToNewPointer); + updatePointers(solver->learnts, oldToNewPointer); + updatePointers(solver->binaryClauses, oldToNewPointer); + updatePointers(solver->xorclauses, oldToNewPointer); + + //No need to update varreplacer, since it only stores binary clauses that + //must have been allocated such as to use the pool + //updatePointers(solver->varReplacer->clauses, oldToNewPointer); + updatePointers(solver->partHandler->clausesRemoved, oldToNewPointer); + updatePointers(solver->partHandler->xorClausesRemoved, oldToNewPointer); + for(map >::iterator it = solver->subsumer->elimedOutVar.begin(); it != solver->subsumer->elimedOutVar.end(); it++) { + updatePointers(it->second, oldToNewPointer); + } + for(map >::iterator it = solver->xorSubsumer->elimedOutVar.begin(); it != solver->xorSubsumer->elimedOutVar.end(); it++) { + updatePointers(it->second, oldToNewPointer); + } + + + vec& reason = solver->reason; + for (PropagatedFrom *it = reason.getData(), *end = reason.getDataEnd(); it != end; it++) { + if (!it->isBinary() && !it->isNULL()) { + /*if ((it == reason.getData() + (*it->getClause())[0].var()) + && (solver->value((*it->getClause())[0]) == l_True)) { + assert(oldToNewPointer.find(it->getClause()) != oldToNewPointer.end()); + *it = PropagatedFrom(oldToNewPointer[it->getClause()]); + } else { + *it = PropagatedFrom(); + }*/ + if (oldToNewPointer.find(it->getClause()) != oldToNewPointer.end()) { + *it = PropagatedFrom(oldToNewPointer[it->getClause()]); + } + } + } + + for (uint32_t i = 0; i < dataStarts.size(); i++) + free(dataStarts[i]); + + dataStarts.clear(); + maxSizes.clear(); + sizes.clear(); + origClauseSizes.clear(); + + dataStarts.push(newDataStarts); + maxSizes.push(newMaxSize); + sizes.push(newSize); + currentlyUsedSize.clear(); + currentlyUsedSize.push(newSize); + origClauseSizes.clear(); + origClauseSizes.push(); + newOrigClauseSizes.moveTo(origClauseSizes[0]); + + if (solver->verbosity >= 1) { + std::cout << "c Consolidated memory. Time: " + << cpuTime() - myTime << std::endl; + } +} + +template +void ClauseAllocator::updateOffsets(vec >& watches, const map& oldToNewOffset) +{ + for (uint32_t i = 0; i < watches.size(); i++) { + vec& list = watches[i]; + for (T *it = list.getData(), *end = list.getDataEnd(); it != end; it++) { + map::const_iterator it2 = oldToNewOffset.find(it->clause); + assert(it2 != oldToNewOffset.end()); + it->clause = it2->second; + } + } +} + +template +void ClauseAllocator::updateOffsetsXor(vec >& watches, const map& oldToNewOffset) +{ + for (uint32_t i = 0; i < watches.size(); i++) { + vec& list = watches[i]; + for (T *it = list.getData(), *end = list.getDataEnd(); it != end; it++) { + map::const_iterator it2 = oldToNewOffset.find(*it); + assert(it2 != oldToNewOffset.end()); + *it = it2->second; + } + } +} + +template +void ClauseAllocator::updatePointers(vec& toUpdate, const map& oldToNewPointer) +{ + for (T **it = toUpdate.getData(), **end = toUpdate.getDataEnd(); it != end; it++) { + if (!(*it)->wasBin()) { + //assert(oldToNewPointer.find((TT*)*it) != oldToNewPointer.end()); + map::const_iterator it2 = oldToNewPointer.find((Clause*)*it); + *it = (T*)it2->second; + } + } +} + +void ClauseAllocator::updatePointers(vector& toUpdate, const map& oldToNewPointer) +{ + for (vector::iterator it = toUpdate.begin(), end = toUpdate.end(); it != end; it++) { + if (!(*it)->wasBin()) { + //assert(oldToNewPointer.find((TT*)*it) != oldToNewPointer.end()); + map::const_iterator it2 = oldToNewPointer.find((Clause*)*it); + *it = it2->second; + } + } +} + +void ClauseAllocator::updatePointers(vector& toUpdate, const map& oldToNewPointer) +{ + for (vector::iterator it = toUpdate.begin(), end = toUpdate.end(); it != end; it++) { + if (!(*it)->wasBin()) { + //assert(oldToNewPointer.find((TT*)*it) != oldToNewPointer.end()); + map::const_iterator it2 = oldToNewPointer.find((Clause*)*it); + *it = (XorClause*)it2->second; + } + } +} + +}; //NAMESPACE MINISAT diff --git a/src/sat/cryptominisat2/ClauseAllocator.h b/src/sat/cryptominisat2/ClauseAllocator.h new file mode 100644 index 0000000..71c479f --- /dev/null +++ b/src/sat/cryptominisat2/ClauseAllocator.h @@ -0,0 +1,95 @@ +/*********************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +This program is free software: you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation, either version 3 of the License, or +(at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program. If not, see . +************************************************************************/ + +#ifndef CLAUSEALLOCATOR_H +#define CLAUSEALLOCATOR_H + +#ifdef _MSC_VER +#include +#else +#include +#endif //_MSC_VER + +#include "Vec.h" +#include +#include +#include +using std::map; +using std::vector; + +namespace MINISAT +{ +using namespace MINISAT; + +class Clause; +class XorClause; +class Solver; + +typedef uint32_t ClauseOffset; + +class ClauseAllocator { + public: + ClauseAllocator(); + + template + Clause* Clause_new(const T& ps, const uint group, const bool learnt = false); + template + XorClause* XorClause_new(const T& ps, const bool inverted, const uint group); + Clause* Clause_new(Clause& c); + + const ClauseOffset getOffset(const Clause* ptr) const; + + inline Clause* getPointer(const uint32_t offset) + { + return (Clause*)(dataStarts[offset&15]+(offset>>4)); + } + + void clauseFree(Clause* c); + + void consolidate(Solver* solver); + + private: + uint32_t getOuterOffset(const Clause* c) const; + uint32_t getInterOffset(const Clause* c, const uint32_t outerOffset) const; + const ClauseOffset combineOuterInterOffsets(const uint32_t outerOffset, const uint32_t interOffset) const; + + template + void updatePointers(vec& toUpdate, const map& oldToNewPointer); + void updatePointers(vector& toUpdate, const map& oldToNewPointer); + void updatePointers(vector& toUpdate, const map& oldToNewPointer); + + template + void updateOffsets(vec >& watches, const map& oldToNewOffset); + template + void updateOffsetsXor(vec >& watches, const map& oldToNewOffset); + + vec dataStarts; + vec sizes; + vec > origClauseSizes; + vec maxSizes; + vec currentlyUsedSize; + vec origSizes; + + boost::pool<> clausePoolBin; + + void* allocEnough(const uint32_t size); +}; + +}; //NAMESPACE MINISAT + +#endif //CLAUSEALLOCATOR_H + diff --git a/src/sat/cryptominisat2/ClauseCleaner.cpp b/src/sat/cryptominisat2/ClauseCleaner.cpp index 42ff1a6..58baec5 100644 --- a/src/sat/cryptominisat2/ClauseCleaner.cpp +++ b/src/sat/cryptominisat2/ClauseCleaner.cpp @@ -99,7 +99,7 @@ void ClauseCleaner::cleanClauses(vec& cs, ClauseSetType type, const uin if (s+1 != end) __builtin_prefetch(*(s+1), 1, 0); if (cleanClause(*s)) { - clauseFree(*s); + solver.clauseAllocator.clauseFree(*s); s++; } else if (type != ClauseCleaner::binaryClauses && (*s)->size() == 2) { solver.binaryClauses.push(*s); @@ -145,8 +145,8 @@ inline const bool ClauseCleaner::cleanClause(Clause*& cc) c.setStrenghtened(); if (c.size() == 2) { solver.detachModifiedClause(origLit1, origLit2, origSize, &c); - Clause *c2 = Clause_new(c); - clauseFree(&c); + Clause *c2 = solver.clauseAllocator.Clause_new(c); + solver.clauseAllocator.clauseFree(&c); cc = c2; solver.attachClause(*c2); /*} else if (c.size() == 3) { @@ -287,8 +287,8 @@ inline const bool ClauseCleaner::cleanClauseBewareNULL(ClauseSimp cc, Subsumer& } if (val == l_True) { - subs.unlinkModifiedClause(origClause, cc); - clauseFree(cc.clause); + subs.unlinkModifiedClause(origClause, cc, true); + solver.clauseAllocator.clauseFree(cc.clause); return true; } } @@ -296,21 +296,21 @@ inline const bool ClauseCleaner::cleanClauseBewareNULL(ClauseSimp cc, Subsumer& if (i != j) { c.setStrenghtened(); if (origClause.size() > 2 && origClause.size()-(i-j) == 2) { - subs.unlinkModifiedClause(origClause, cc); + subs.unlinkModifiedClause(origClause, cc, true); subs.clauses[cc.index] = cc; c.shrink(i-j); solver.attachClause(c); subs.linkInAlreadyClause(cc); } else { c.shrink(i-j); - subs.unlinkModifiedClauseNoDetachNoNULL(origClause, cc); + subs.unlinkModifiedClause(origClause, cc, false); subs.linkInAlreadyClause(cc); if (c.learnt()) solver.learnts_literals -= i-j; else solver.clauses_literals -= i-j; } - c.calcAbstraction(); + if (!c.learnt()) c.calcAbstractionClause(); subs.updateClause(cc); } @@ -357,7 +357,7 @@ inline const bool ClauseCleaner::cleanXorClauseBewareNULL(XorClauseSimp cc, XorS switch(c.size()) { case 0: { subs.unlinkModifiedClause(origClause, cc); - clauseFree(cc.clause); + solver.clauseAllocator.clauseFree(cc.clause); return true; } case 2: { @@ -366,7 +366,7 @@ inline const bool ClauseCleaner::cleanXorClauseBewareNULL(XorClauseSimp cc, XorS ps[1] = c[1].unsign(); solver.varReplacer->replace(ps, c.xor_clause_inverted(), c.getGroup()); subs.unlinkModifiedClause(origClause, cc); - clauseFree(cc.clause); + solver.clauseAllocator.clauseFree(cc.clause); return true; } default: @@ -410,9 +410,14 @@ void ClauseCleaner::moveBinClausesToBinClauses() if (s+1 != end) __builtin_prefetch(*(s+1), 1, 0); - if ((**s).size() == 2) - solver.binaryClauses.push(*s); - else + if ((**s).size() == 2) { + solver.detachClause(**s); + Clause *c2 = solver.clauseAllocator.Clause_new(**s); + solver.clauseAllocator.clauseFree(*s); + solver.attachClause(*c2); + solver.becameBinary++; + solver.binaryClauses.push(c2); + } else *ss++ = *s; } cs.shrink(s-ss); diff --git a/src/sat/cryptominisat2/Conglomerate.cpp b/src/sat/cryptominisat2/Conglomerate.cpp deleted file mode 100644 index 96855d7..0000000 --- a/src/sat/cryptominisat2/Conglomerate.cpp +++ /dev/null @@ -1,526 +0,0 @@ -/*********************************************************************************** -CryptoMiniSat -- Copyright (c) 2009 Mate Soos - -This program is free software: you can redistribute it and/or modify -it under the terms of the GNU General Public License as published by -the Free Software Foundation, either version 3 of the License, or -(at your option) any later version. - -This program is distributed in the hope that it will be useful, -but WITHOUT ANY WARRANTY; without even the implied warranty of -MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -GNU General Public License for more details. - -You should have received a copy of the GNU General Public License -along with this program. If not, see . -**************************************************************************************************/ - -#include "Conglomerate.h" -#include "VarReplacer.h" -#include "ClauseCleaner.h" - -#include -#include -#include -#include "time_mem.h" -#include -using std::make_pair; - -//#define VERBOSE_DEBUG - -#ifdef VERBOSE_DEBUG -#include -using std::cout; -using std::endl; -#endif - -namespace MINISAT -{ -using namespace MINISAT; - -Conglomerate::Conglomerate(Solver& _solver) : - found(0) - , solver(_solver) -{} - -Conglomerate::~Conglomerate() -{ - for(uint i = 0; i < calcAtFinish.size(); i++) - free(calcAtFinish[i]); -} - -void Conglomerate::blockVars() -{ - for (Clause *const*it = solver.clauses.getData(), *const*end = it + solver.clauses.size(); it != end; it++) { - const Clause& c = **it; - for (const Lit* a = &c[0], *end = a + c.size(); a != end; a++) { - blocked[a->var()] = true; - } - } - - for (Clause *const*it = solver.binaryClauses.getData(), *const*end = it + solver.binaryClauses.size(); it != end; it++) { - const Clause& c = **it; - blocked[c[0].var()] = true; - blocked[c[1].var()] = true; - } - - for (Lit* it = &(solver.trail[0]), *end = it + solver.trail.size(); it != end; it++) - blocked[it->var()] = true; - - const vec& clauses = solver.varReplacer->getClauses(); - for (Clause *const*it = clauses.getData(), *const*end = it + clauses.size(); it != end; it++) { - const Clause& c = **it; - for (const Lit* a = &c[0], *end = a + c.size(); a != end; a++) { - blocked[a->var()] = true; - } - } -} - -void Conglomerate::fillVarToXor() -{ - varToXor.clear(); - - uint i = 0; - for (XorClause* const* it = solver.xorclauses.getData(), *const*end = it + solver.xorclauses.size(); it != end; it++, i++) { - const XorClause& c = **it; - for (const Lit * a = &c[0], *end = a + c.size(); a != end; a++) { - if (!blocked[a->var()]) - varToXor[a->var()].push_back(make_pair(*it, i)); - } - } -} - -void Conglomerate::removeVar(const Var var) -{ - solver.activity[var] = 0.0; - solver.order_heap.update(var); - removedVars[var] = true; - if (solver.decision_var[var]) { - madeVarNonDecision.push(var); - solver.setDecisionVar(var, false); - } - found++; -} - -void Conglomerate::processClause(XorClause& x, uint32_t num, Var remove_var) -{ - for (const Lit* a = &x[0], *end = a + x.size(); a != end; a++) { - Var var = a->var(); - if (var != remove_var) { - varToXorMap::iterator finder = varToXor.find(var); - if (finder != varToXor.end()) { - vector >::iterator it = - std::find(finder->second.begin(), finder->second.end(), make_pair(&x, num)); - finder->second.erase(it); - } - } - } -} - -const bool Conglomerate::heuleProcessFull() -{ - #ifdef VERBOSE_DEBUG - cout << "Heule XOR-ing started" << endl; - #endif - - double time = cpuTime(); - found = 0; - uint oldToReplaceVars = solver.varReplacer->getNewToReplaceVars(); - solver.clauseCleaner->cleanClauses(solver.xorclauses, ClauseCleaner::xorclauses); - if (solver.ok == false) - return false; - - toRemove.clear(); - toRemove.resize(solver.xorclauses.size(), false); - blocked.clear(); - blocked.resize(solver.nVars(), false); - fillVarToXor(); - if (!heuleProcess()) - goto end; - - if (solver.verbosity >=1) { - std::cout << "c | Heule-processings XORs:" << std::setw(8) << std::setprecision(2) << std::fixed << cpuTime()-time - << " Found smaller XOR-s: " << std::setw(6) << found - << " New bin anti/eq-s: " << std::setw(3) << solver.varReplacer->getNewToReplaceVars() - oldToReplaceVars - << std::setw(0) << " |" << std::endl; - } - -end: - - clearToRemove(); - - return solver.ok; -} - -const bool Conglomerate::conglomerateXorsFull() -{ - #ifdef VERBOSE_DEBUG - cout << "Finding conglomerate xors started" << endl; - #endif - - double time = cpuTime(); - found = 0; - uint32_t origNumClauses = solver.xorclauses.size(); - - solver.clauseCleaner->cleanClauses(solver.xorclauses, ClauseCleaner::xorclauses); - if (solver.ok == false) - return false; - - toRemove.clear(); - toRemove.resize(solver.xorclauses.size(), false); - blocked.clear(); - blocked.resize(solver.nVars(), false); - blockVars(); - fillVarToXor(); - if (conglomerateXors() == false) - goto end; - -end: - - clearToRemove(); - assert(origNumClauses >= solver.xorclauses.size()); - if (solver.verbosity >=1) { - std::cout << "c | Conglomerating XORs:" << std::setw(8) << std::setprecision(2) << std::fixed << cpuTime()-time << " s " - << " removed " << std::setw(8) << found << " vars" - << " removed " << std::setw(8) << origNumClauses-solver.xorclauses.size() << " clauses" - << std::setw(0) << " |" << std::endl; - } - - clearLearntsFromToRemove(); - solver.order_heap.filter(Solver::VarFilter(solver)); - - return solver.ok; -} - -void Conglomerate::fillNewSet(vector >& newSet, vector >& clauseSet) const -{ - newSet.clear(); - newSet.resize(clauseSet.size()); - - XorClause& firstXorClause = *(clauseSet[0].first); - newSet[0].resize(firstXorClause.size()); - memcpy(&newSet[0][0], firstXorClause.getData(), sizeof(Lit)*firstXorClause.size()); - - for (uint i = 1; i < clauseSet.size(); i++) { - XorClause& thisXorClause = *clauseSet[i].first; - newSet[i] = newSet[0]; - newSet[i].resize(firstXorClause.size()+thisXorClause.size()); - memcpy(&newSet[i][firstXorClause.size()], thisXorClause.getData(), sizeof(Lit)*thisXorClause.size()); - clearDouble(newSet[i]); - } -} - -const bool Conglomerate::heuleProcess() -{ - vector > newSet; - while(varToXor.begin() != varToXor.end()) { - varToXorMap::iterator it = varToXor.begin(); - vector >& clauseSet = it->second; - const Var var = it->first; - - if (blocked[var] || clauseSet.size() == 1) { - varToXor.erase(it); - blocked[var] = true; - continue; - } - blocked[var] = true; - - std::sort(clauseSet.begin(), clauseSet.end(), ClauseSetSorter()); - fillNewSet(newSet, clauseSet); - - for (uint i = 1; i < newSet.size(); i++) if (newSet[i].size() <= 2) { - found++; - XorClause& thisXorClause = *clauseSet[i].first; - const bool inverted = !clauseSet[0].first->xor_clause_inverted() ^ thisXorClause.xor_clause_inverted(); - const uint old_group = thisXorClause.getGroup(); - - #ifdef VERBOSE_DEBUG - cout << "- XOR1:"; - clauseSet[0].first->plainPrint(); - cout << "- XOR2:"; - thisXorClause.plainPrint(); - #endif - - if (!dealWithNewClause(newSet[i], inverted, old_group)) - return false; - assert(newSet.size() == clauseSet.size()); - } - - varToXor.erase(it); - } - - return (solver.ok = (solver.propagate() == NULL)); -} - -const bool Conglomerate::conglomerateXors() -{ - vector > newSet; - while(varToXor.begin() != varToXor.end()) { - varToXorMap::iterator it = varToXor.begin(); - vector >& clauseSet = it->second; - const Var var = it->first; - - //We blocked the var during dealWithNewClause (it was in a 2-long xor-clause) - if (blocked[var]) { - varToXor.erase(it); - continue; - } - - if (clauseSet.size() == 0) { - removeVar(var); - varToXor.erase(it); - continue; - } - - std::sort(clauseSet.begin(), clauseSet.end(), ClauseSetSorter()); - fillNewSet(newSet, clauseSet); - - int diff = 0; - for (size_t i = 1; i < newSet.size(); i++) - diff += (int)newSet[i].size()-(int)clauseSet[i].first->size(); - - if (newSet.size() > 2) { - blocked[var] = true; - varToXor.erase(it); - continue; - } - - XorClause& firstXorClause = *(clauseSet[0].first); - bool first_inverted = !firstXorClause.xor_clause_inverted(); - removeVar(var); - - #ifdef VERBOSE_DEBUG - cout << "--- New conglomerate set ---" << endl; - cout << "- Removing: "; - firstXorClause.plainPrint(); - cout << "Adding var " << var+1 << " to calcAtFinish" << endl; - #endif - - assert(!toRemove[clauseSet[0].second]); - toRemove[clauseSet[0].second] = true; - processClause(firstXorClause, clauseSet[0].second, var); - solver.detachClause(firstXorClause); - calcAtFinish.push(&firstXorClause); - - for (uint i = 1; i < clauseSet.size(); i++) { - XorClause& thisXorClause = *clauseSet[i].first; - #ifdef VERBOSE_DEBUG - cout << "- Removing: "; - thisXorClause.plainPrint(); - #endif - - const uint old_group = thisXorClause.getGroup(); - const bool inverted = first_inverted ^ thisXorClause.xor_clause_inverted(); - assert(!toRemove[clauseSet[i].second]); - toRemove[clauseSet[i].second] = true; - processClause(thisXorClause, clauseSet[i].second, var); - solver.removeClause(thisXorClause); - - if (!dealWithNewClause(newSet[i], inverted, old_group)) - return false; - assert(newSet.size() == clauseSet.size()); - } - - varToXor.erase(it); - } - - return (solver.ok = (solver.propagate() == NULL)); -} - -bool Conglomerate::dealWithNewClause(vector& ps, const bool inverted, const uint old_group) -{ - switch(ps.size()) { - case 0: { - #ifdef VERBOSE_DEBUG - cout << "--> xor is 0-long" << endl; - #endif - - if (!inverted) { - solver.ok = false; - return false; - } - break; - } - case 1: { - #ifdef VERBOSE_DEBUG - cout << "--> xor is 1-long, attempting to set variable " << ps[0].var()+1 << endl; - #endif - - if (solver.assigns[ps[0].var()] == l_Undef) { - assert(solver.decisionLevel() == 0); - blocked[ps[0].var()] = true; - solver.uncheckedEnqueue(Lit(ps[0].var(), inverted)); - } else if (solver.assigns[ps[0].var()] != boolToLBool(!inverted)) { - #ifdef VERBOSE_DEBUG - cout << "Conflict. Aborting."; - #endif - solver.ok = false; - return false; - } else { - #ifdef VERBOSE_DEBUG - cout << "Variable already set to correct value"; - #endif - } - break; - } - - case 2: { - #ifdef VERBOSE_DEBUG - cout << "--> xor is 2-long, must later replace variable" << endl; - XorClause* newX = XorClause_new(ps, inverted, old_group); - newX->plainPrint(); - free(newX); - #endif - - vec tmpPS(2); - tmpPS[0] = ps[0]; - tmpPS[1] = ps[1]; - if (solver.varReplacer->replace(tmpPS, inverted, old_group) == false) - return false; - blocked[ps[0].var()] = true; - blocked[ps[1].var()] = true; - break; - } - - default: { - XorClause* newX = XorClause_new(ps, inverted, old_group); - - #ifdef VERBOSE_DEBUG - cout << "- Adding: "; - newX->plainPrint(); - #endif - - solver.xorclauses.push(newX); - toRemove.push_back(false); - solver.attachClause(*newX); - for (const Lit * a = &((*newX)[0]), *end = a + newX->size(); a != end; a++) { - if (!blocked[a->var()]) - varToXor[a->var()].push_back(make_pair(newX, (uint32_t)(toRemove.size()-1))); - } - break; - } - } - - return true; -} - -void Conglomerate::clearDouble(vector& ps) const -{ - std::sort(ps.begin(), ps.end()); - Lit p; - uint32_t i, j; - for (i = j = 0, p = lit_Undef; i != ps.size(); i++) { - ps[i] = ps[i].unsign(); - if (ps[i] == p) { - //added, but easily removed - j--; - p = lit_Undef; - } else - ps[j++] = p = ps[i]; - } - ps.resize(ps.size() - (i - j)); -} - -void Conglomerate::clearToRemove() -{ - assert(toRemove.size() == solver.xorclauses.size()); - - XorClause **a = solver.xorclauses.getData(); - XorClause **r = a; - XorClause **end = a + solver.xorclauses.size(); - for (uint i = 0; r != end; i++) { - if (!toRemove[i]) - *a++ = *r++; - else { - r++; - } - } - solver.xorclauses.shrink(r-a); -} - -void Conglomerate::clearLearntsFromToRemove() -{ - Clause **a = solver.learnts.getData(); - Clause **r = a; - Clause **end = a + solver.learnts.size(); - for (; r != end;) { - const Clause& c = **r; - bool inside = false; - if (!solver.locked(c)) { - for (uint i = 0; i < c.size(); i++) { - if (removedVars[c[i].var()]) { - inside = true; - break; - } - } - } - if (!inside) - *a++ = *r++; - else { - solver.removeClause(**r); - r++; - } - } - solver.learnts.shrink(r-a); -} - -void Conglomerate::extendModel(Solver& solver2) -{ - #ifdef VERBOSE_DEBUG - cout << "Executing doCalcAtFinish" << endl; - #endif - - vec ps; - for (int i = (int)(calcAtFinish.size())-1; i >= 0; i--) { - XorClause& c = *calcAtFinish[i]; - assert(c.size() > 2); - - ps.clear(); - for (Lit *l = c.getData(), *end = c.getDataEnd(); l != end; l++) { - ps.push(l->unsign()); - } - - solver2.addXorClause(ps, c.xor_clause_inverted(), c.getGroup()); - assert(solver2.ok); - } -} - -const bool Conglomerate::addRemovedClauses() -{ - #ifdef VERBOSE_DEBUG - cout << "Executing addRemovedClauses" << endl; - #endif - - for(XorClause **it = calcAtFinish.getData(), **end = calcAtFinish.getDataEnd(); it != end; it++) - { - XorClause& c = **it; - #ifdef VERBOSE_DEBUG - cout << "readding already removed (conglomerated) clause: "; - c.plainPrint(); - #endif - - for(Lit *l = c.getData(), *end2 = c.getDataEnd(); l != end2 ; l++) - *l = l->unsign(); - - FILE* backup_libraryCNFfile = solver.libraryCNFFile; - solver.libraryCNFFile = NULL; - if (!solver.addXorClause(c, c.xor_clause_inverted(), c.getGroup())) { - for (;it != end; it++) free(*it); - calcAtFinish.clear(); - return false; - } - solver.libraryCNFFile = backup_libraryCNFfile; - free(&c); - } - calcAtFinish.clear(); - - std::fill(removedVars.getData(), removedVars.getDataEnd(), false); - for (Var *v = madeVarNonDecision.getData(), *end = madeVarNonDecision.getDataEnd(); v != end; v++) { - solver.setDecisionVar(*v, true); - } - madeVarNonDecision.clear(); - - return true; -} - -}; //NAMESPACE MINISAT diff --git a/src/sat/cryptominisat2/Conglomerate.h b/src/sat/cryptominisat2/Conglomerate.h deleted file mode 100644 index 50972d4..0000000 --- a/src/sat/cryptominisat2/Conglomerate.h +++ /dev/null @@ -1,125 +0,0 @@ -/*********************************************************************************** -CryptoMiniSat -- Copyright (c) 2009 Mate Soos - -This program is free software: you can redistribute it and/or modify -it under the terms of the GNU General Public License as published by -the Free Software Foundation, either version 3 of the License, or -(at your option) any later version. - -This program is distributed in the hope that it will be useful, -but WITHOUT ANY WARRANTY; without even the implied warranty of -MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -GNU General Public License for more details. - -You should have received a copy of the GNU General Public License -along with this program. If not, see . -**************************************************************************************************/ - -#ifndef CONGLOMERATE_H -#define CONGLOMERATE_H - -#include -#include -#include -#ifdef _MSC_VER -#include -#else -#include -#endif //_MSC_VER - -#include "Clause.h" -#include "VarReplacer.h" -#include "Solver.h" - -using std::vector; -using std::pair; -using std::map; -using std::set; - -namespace MINISAT -{ -using namespace MINISAT; - -class Solver; - -class Conglomerate -{ -public: - Conglomerate(Solver& solver); - ~Conglomerate(); - const bool conglomerateXorsFull(); - const bool heuleProcessFull(); - const bool addRemovedClauses(); ///& getCalcAtFinish() const; - vec& getCalcAtFinish(); - const vec& getRemovedVars() const; - const bool needCalcAtFinish() const; - - void newVar(); - -private: - - struct ClauseSetSorter { - bool operator () (const pair& a, const pair& b) { - return a.first->size() < b.first->size(); - } - }; - - const bool conglomerateXors(); - const bool heuleProcess(); - - void fillNewSet(vector >& newSet, vector >& clauseSet) const; - - void removeVar(const Var var); - void processClause(XorClause& x, uint32_t num, Var remove_var); - void blockVars(); - void fillVarToXor(); - void clearDouble(vector& ps) const; - void clearToRemove(); - void clearLearntsFromToRemove(); - bool dealWithNewClause(vector& ps, const bool inverted, const uint old_group); - - typedef map > > varToXorMap; - varToXorMap varToXor; - vector blocked; - vector toRemove; - - vec removedVars; - vec madeVarNonDecision; - - vec calcAtFinish; - uint found; - - Solver& solver; -}; - -inline void Conglomerate::newVar() -{ - removedVars.push(false); -} - -inline const vec& Conglomerate::getRemovedVars() const -{ - return removedVars; -} - -inline const vec& Conglomerate::getCalcAtFinish() const -{ - return calcAtFinish; -} - -inline vec& Conglomerate::getCalcAtFinish() -{ - return calcAtFinish; -} - -inline const bool Conglomerate::needCalcAtFinish() const -{ - return calcAtFinish.size(); -} - -}; //NAMESPACE MINISAT - -#endif //CONGLOMERATE_H diff --git a/src/sat/cryptominisat2/FailedVarSearcher.cpp b/src/sat/cryptominisat2/FailedVarSearcher.cpp index 4b273f7..0b98a12 100644 --- a/src/sat/cryptominisat2/FailedVarSearcher.cpp +++ b/src/sat/cryptominisat2/FailedVarSearcher.cpp @@ -137,8 +137,6 @@ const bool FailedVarSearcher::search(uint64_t numProps) Heap order_heap_copy(solver.order_heap); //for hyperbin uint64_t origBinClauses = solver.binaryClauses.size(); - if (solver.readdOldLearnts && !readdRemovedLearnts()) goto end; - //General Stats numFailed = 0; goodBothSame = 0; @@ -280,15 +278,7 @@ end: } if (solver.verbosity >= 1 && numFailed + goodBothSame > 100) { std::cout << "c | Cleaning up after failed var search: " << std::setw(8) << std::fixed << std::setprecision(2) << cpuTime() - time << " s " - << std::setw(33) << " | " << std::endl; - } - } - - if (solver.ok && solver.readdOldLearnts && !removedOldLearnts) { - if (solver.removedLearnts.size() < 100000) { - removeOldLearnts(); - } else { - completelyDetachAndReattach(); + << std::setw(39) << " | " << std::endl; } } @@ -335,8 +325,8 @@ const bool FailedVarSearcher::orderLits() uint64_t oldProps = solver.propagations; double myTime = cpuTime(); uint32_t numChecked = 0; - litDegrees.clear(); - litDegrees.resize(solver.nVars()*2, 0); + if (litDegrees.size() != solver.nVars()) + litDegrees.resize(solver.nVars()*2, 0); BitArray alreadyTested; alreadyTested.resize(solver.nVars()*2, 0); uint32_t i; @@ -353,11 +343,11 @@ const bool FailedVarSearcher::orderLits() numChecked++; solver.newDecisionLevel(); solver.uncheckedEnqueueLight(randLit); - failed = (solver.propagateBin() != NULL); + failed = (!solver.propagateBin().isNULL()); if (failed) { solver.cancelUntil(0); solver.uncheckedEnqueue(~randLit); - solver.ok = (solver.propagate() == NULL); + solver.ok = (solver.propagate().isNULL()); if (!solver.ok) return false; continue; } @@ -368,132 +358,15 @@ const bool FailedVarSearcher::orderLits() } solver.cancelUntil(0); } - std::cout << "c binary Degree finding time: " << cpuTime() - myTime << " s num checked: " << numChecked << " i: " << i << " props: " << (solver.propagations - oldProps) << std::endl; - solver.propagations = oldProps; - - return true; -} - -void FailedVarSearcher::removeOldLearnts() -{ - for (Clause **it = solver.removedLearnts.getData(), **end = solver.removedLearnts.getDataEnd(); it != end; it++) { - solver.detachClause(**it); - } -} - -struct reduceDB_ltOldLearnt -{ - bool operator () (const Clause* x, const Clause* y) { - return x->size() > y->size(); - } -}; - -const bool FailedVarSearcher::readdRemovedLearnts() -{ - uint32_t toRemove = (solver.removedLearnts.size() > MAX_OLD_LEARNTS) ? (solver.removedLearnts.size() - MAX_OLD_LEARNTS/4) : 0; - if (toRemove > 0) - std::sort(solver.removedLearnts.getData(), solver.removedLearnts.getDataEnd(), reduceDB_ltOldLearnt()); - - Clause **it1, **it2; - it1 = it2 = solver.removedLearnts.getData(); - for (Clause **end = solver.removedLearnts.getDataEnd(); it1 != end; it1++) { - if (toRemove > 0) { - clauseFree(*it1); - toRemove--; - continue; - } - - Clause* c = solver.addClauseInt(**it1, (**it1).getGroup()); - clauseFree(*it1); - if (c != NULL) { - *it2 = c; - it2++; - } - if (!solver.ok) { - it1++; - for (; it1 != end; it1++) clauseFree(*it1); - } - } - solver.removedLearnts.shrink(it1-it2); - //std::cout << "Readded old learnts. New facts:" << (int)origHeapSize - (int)solver.order_heap.size() << std::endl; - - return solver.ok; -} - -#define MAX_REMOVE_BIN_FULL_PROPS 20000000 -#define EXTRATIME_DIVIDER 3 - -template -const bool FailedVarSearcher::removeUslessBinFull() -{ - if (!solver.performReplace) return true; - while (solver.performReplace && solver.varReplacer->getClauses().size() > 0) { - if (!solver.varReplacer->performReplace(true)) return false; - solver.clauseCleaner->removeAndCleanAll(true); - } - assert(solver.varReplacer->getClauses().size() == 0); - solver.testAllClauseAttach(); - if (startUp) { - solver.clauseCleaner->moveBinClausesToBinClauses(); - } - - double myTime = cpuTime(); - toDeleteSet.clear(); - toDeleteSet.growTo(solver.nVars()*2, 0); - uint32_t origHeapSize = solver.order_heap.size(); - uint64_t origProps = solver.propagations; - bool fixed = false; - uint32_t extraTime = solver.binaryClauses.size() / EXTRATIME_DIVIDER; - - uint32_t startFrom = solver.mtrand.randInt(solver.order_heap.size()); - for (uint32_t i = 0; i != solver.order_heap.size(); i++) { - Var var = solver.order_heap[(i+startFrom)%solver.order_heap.size()]; - if (solver.propagations - origProps + extraTime > MAX_REMOVE_BIN_FULL_PROPS) break; - if (solver.assigns[var] != l_Undef || !solver.decision_var[var]) continue; - - Lit lit(var, true); - if (!removeUselessBinaries(lit)) { - fixed = true; - solver.cancelUntil(0); - solver.uncheckedEnqueue(~lit); - solver.ok = (solver.propagate() == NULL); - if (!solver.ok) return false; - continue; - } - - lit = ~lit; - if (!removeUselessBinaries(lit)) { - fixed = true; - solver.cancelUntil(0); - solver.uncheckedEnqueue(~lit); - solver.ok = (solver.propagate() == NULL); - if (!solver.ok) return false; - continue; - } - } - - Clause **i, **j; - i = j = solver.binaryClauses.getData(); - uint32_t num = 0; - for (Clause **end = solver.binaryClauses.getDataEnd(); i != end; i++, num++) { - if (!(*i)->removed()) { - *j++ = *i; - } else { - clauseFree(*i); - } - } - uint32_t removedUselessBin = i - j; - solver.binaryClauses.shrink(i - j); - - if (fixed) solver.order_heap.filter(Solver::VarFilter(solver)); - if (solver.verbosity >= 1) { - std::cout - << "c Removed useless bin:" << std::setw(8) << removedUselessBin - << " fixed: " << std::setw(4) << (origHeapSize - solver.order_heap.size()) - << " props: " << std::fixed << std::setprecision(2) << std::setw(4) << (double)(solver.propagations - origProps)/1000000.0 << "M" - << " time: " << std::fixed << std::setprecision(2) << std::setw(5) << cpuTime() - myTime << std::endl; + std::cout << "c binary deg approx." + << " time: " << std::fixed << std::setw(5) << std::setprecision(2) << cpuTime() - myTime << " s" + << " num checked: " << std::setw(6) << numChecked + << " i: " << std::setw(7) << i + << " props: " << std::setw(4) << (solver.propagations - oldProps)/1000 << "k" + << std::setw(13) << " |" << std::endl; } + solver.propagations = oldProps; return true; } @@ -519,12 +392,12 @@ const bool FailedVarSearcher::tryBoth(const Lit lit1, const Lit lit2) solver.newDecisionLevel(); solver.uncheckedEnqueueLight(lit1); - failed = (solver.propagateLight() != NULL); + failed = (!solver.propagate().isNULL()); if (failed) { solver.cancelUntil(0); numFailed++; solver.uncheckedEnqueue(~lit1); - solver.ok = (solver.propagate(false) == NULL); + solver.ok = (solver.propagate(false).isNULL()); if (!solver.ok) return false; return true; } else { @@ -563,12 +436,12 @@ const bool FailedVarSearcher::tryBoth(const Lit lit1, const Lit lit2) solver.newDecisionLevel(); solver.uncheckedEnqueueLight(lit2); - failed = (solver.propagateLight() != NULL); + failed = (!solver.propagate().isNULL()); if (failed) { solver.cancelUntil(0); numFailed++; solver.uncheckedEnqueue(~lit2); - solver.ok = (solver.propagate(false) == NULL); + solver.ok = (solver.propagate(false).isNULL()); if (!solver.ok) return false; return true; } else { @@ -636,7 +509,7 @@ const bool FailedVarSearcher::tryBoth(const Lit lit1, const Lit lit2) solver.uncheckedEnqueue(bothSame[i]); } goodBothSame += bothSame.size(); - solver.ok = (solver.propagate(false) == NULL); + solver.ok = (solver.propagate(false).isNULL()); if (!solver.ok) return false; return true; @@ -665,7 +538,7 @@ void FailedVarSearcher::addBinClauses(const Lit& lit) solver.newDecisionLevel(); solver.uncheckedEnqueueLight(lit); - failed = (solver.propagateBin() != NULL); + failed = (!solver.propagateBin().isNULL()); assert(!failed); assert(solver.decisionLevel() > 0); @@ -731,7 +604,7 @@ void FailedVarSearcher::fillImplies(const Lit& lit) { solver.newDecisionLevel(); solver.uncheckedEnqueue(lit); - failed = (solver.propagateLight() != NULL); + failed = (!solver.propagate().isNULL()); assert(!failed); assert(solver.decisionLevel() > 0); @@ -743,36 +616,6 @@ void FailedVarSearcher::fillImplies(const Lit& lit) solver.cancelUntil(0); } -template -const bool FailedVarSearcher::fillBinImpliesMinusLast(const Lit& origLit, const Lit& lit, vec& wrong) -{ - solver.newDecisionLevel(); - solver.uncheckedEnqueueLight(lit); - //if it's a cycle, it doesn't work, so don't propagate origLit - failed = (solver.propagateBinExcept(origLit) != NULL); - if (failed) return false; - - assert(solver.decisionLevel() > 0); - int c; - extraTime += (solver.trail.size() - solver.trail_lim[0]) / EXTRATIME_DIVIDER; - for (c = solver.trail.size()-1; c > (int)solver.trail_lim[0]; c--) { - Lit x = solver.trail[c]; - if (toDeleteSet[x.toInt()]) { - wrong.push(x); - toDeleteSet[x.toInt()] = false; - }; - solver.assigns[x.var()] = l_Undef; - } - solver.assigns[solver.trail[c].var()] = l_Undef; - - solver.qhead = solver.trail_lim[0]; - solver.trail.shrink_(solver.trail.size() - solver.trail_lim[0]); - solver.trail_lim.clear(); - //solver.cancelUntil(0); - - return true; -} - void FailedVarSearcher::addBin(const Lit& lit1, const Lit& lit2) { #ifdef VERBOSE_DEBUG @@ -787,129 +630,6 @@ void FailedVarSearcher::addBin(const Lit& lit1, const Lit& lit2) assert(solver.ok); } -template -const bool FailedVarSearcher::removeUselessBinaries(const Lit& lit) -{ - //Nothing can be learnt at this point! - //Otherwise, it might happen that the path to X has learnts, - //but binary clause to X is not learnt. - //So we remove X , then we might remove - //the path (since it's learnt) -- removing a FACT!! - //[note:removal can be through variable elimination - //, and removeWrong() will happily remove it - assert(!startUp || solver.learnts.size() == 0); - - solver.newDecisionLevel(); - solver.uncheckedEnqueueLight(lit); - failed = (solver.propagateBinOneLevel() != NULL); - if (failed) return false; - bool ret = true; - - oneHopAway.clear(); - assert(solver.decisionLevel() > 0); - int c; - if (solver.trail.size()-solver.trail_lim[0] == 0) { - solver.cancelUntil(0); - goto end; - } - extraTime += (solver.trail.size() - solver.trail_lim[0]) / EXTRATIME_DIVIDER; - for (c = solver.trail.size()-1; c > (int)solver.trail_lim[0]; c--) { - Lit x = solver.trail[c]; - toDeleteSet[x.toInt()] = true; - oneHopAway.push(x); - solver.assigns[x.var()] = l_Undef; - } - solver.assigns[solver.trail[c].var()] = l_Undef; - - solver.qhead = solver.trail_lim[0]; - solver.trail.shrink_(solver.trail.size() - solver.trail_lim[0]); - solver.trail_lim.clear(); - //solver.cancelUntil(0); - - wrong.clear(); - for(uint32_t i = 0; i < oneHopAway.size(); i++) { - //no need to visit it if it already queued for removal - //basically, we check if it's in 'wrong' - if (toDeleteSet[oneHopAway[i].toInt()]) { - if (!fillBinImpliesMinusLast(lit, oneHopAway[i], wrong)) { - ret = false; - goto end; - } - } - } - - for (uint32_t i = 0; i < wrong.size(); i++) { - removeBin(~lit, wrong[i]); - } - - end: - for(uint32_t i = 0; i < oneHopAway.size(); i++) { - toDeleteSet[oneHopAway[i].toInt()] = false; - } - - return ret; -} -template const bool FailedVarSearcher::removeUselessBinaries (const Lit& lit); -template const bool FailedVarSearcher::removeUselessBinaries (const Lit& lit); -template const bool FailedVarSearcher::fillBinImpliesMinusLast (const Lit& origLit, const Lit& lit, vec& wrong); -template const bool FailedVarSearcher::fillBinImpliesMinusLast (const Lit& origLit, const Lit& lit, vec& wrong); -template const bool FailedVarSearcher::removeUslessBinFull (); -template const bool FailedVarSearcher::removeUslessBinFull (); - -void FailedVarSearcher::removeBin(const Lit& lit1, const Lit& lit2) -{ - /******************* - Lit litFind1 = lit_Undef; - Lit litFind2 = lit_Undef; - - if (solver.binwatches[(~lit1).toInt()].size() < solver.binwatches[(~lit2).toInt()].size()) { - litFind1 = lit1; - litFind2 = lit2; - } else { - litFind1 = lit2; - litFind2 = lit1; - } - ********************/ - - //Find AND remove from watches - vec& bwin = solver.binwatches[(~lit1).toInt()]; - extraTime += bwin.size() / EXTRATIME_DIVIDER; - Clause *cl = NULL; - WatchedBin *i, *j; - i = j = bwin.getData(); - for (const WatchedBin *end = bwin.getDataEnd(); i != end; i++) { - if (i->impliedLit == lit2 && cl == NULL) { - cl = i->clause; - } else { - *j++ = *i; - } - } - bwin.shrink(1); - assert(cl != NULL); - - bool found = false; - vec& bwin2 = solver.binwatches[(~lit2).toInt()]; - extraTime += bwin2.size() / EXTRATIME_DIVIDER; - i = j = bwin2.getData(); - for (const WatchedBin *end = bwin2.getDataEnd(); i != end; i++) { - if (i->clause == cl) { - found = true; - } else { - *j++ = *i; - } - } - bwin2.shrink(1); - assert(found); - - #ifdef VERBOSE_DEBUG - std::cout << "Removing useless bin: "; - cl->plainPrint(); - #endif //VERBOSE_DEBUG - - cl->setRemoved(); - solver.clauses_literals -= 2; -} - template inline void FailedVarSearcher::cleanAndAttachClauses(vec& cs) { @@ -920,7 +640,7 @@ inline void FailedVarSearcher::cleanAndAttachClauses(vec& cs) solver.attachClause(**i); *j++ = *i; } else { - clauseFree(*i); + solver.clauseAllocator.clauseFree(*i); } } cs.shrink(i-j); diff --git a/src/sat/cryptominisat2/FailedVarSearcher.h b/src/sat/cryptominisat2/FailedVarSearcher.h index 9f714ea..5ea4c1e 100644 --- a/src/sat/cryptominisat2/FailedVarSearcher.h +++ b/src/sat/cryptominisat2/FailedVarSearcher.h @@ -64,8 +64,6 @@ class FailedVarSearcher { FailedVarSearcher(Solver& _solver); const bool search(uint64_t numProps); - template - const bool removeUslessBinFull(); private: //For 2-long xor @@ -90,9 +88,6 @@ class FailedVarSearcher { void printResults(const double myTime) const; Solver& solver; - - //Time - uint32_t extraTime; //For failure bool failed; @@ -132,16 +127,6 @@ class FailedVarSearcher { uint64_t maxHyperBinProps; uint64_t binClauseAdded; - //Remove useless binaries - template - const bool fillBinImpliesMinusLast(const Lit& origLit, const Lit& lit, vec& wrong); - template - const bool removeUselessBinaries(const Lit& lit); - void removeBin(const Lit& lit1, const Lit& lit2); - vec toDeleteSet; - vec oneHopAway; - vec wrong; - //Temporaries vec tmpPs; @@ -166,4 +151,5 @@ class FailedVarSearcher { }; //NAMESPACE MINISAT -#endif //FAILEDVARSEARCHER_H \ No newline at end of file +#endif //FAILEDVARSEARCHER_H + diff --git a/src/sat/cryptominisat2/Gaussian.cpp b/src/sat/cryptominisat2/Gaussian.cpp index 4b7b905..e5edc50 100644 --- a/src/sat/cryptominisat2/Gaussian.cpp +++ b/src/sat/cryptominisat2/Gaussian.cpp @@ -65,7 +65,7 @@ Gaussian::Gaussian(Solver& _solver, const GaussianConfig& _config, const uint _m Gaussian::~Gaussian() { for (uint i = 0; i < clauses_toclear.size(); i++) - clauseFree(clauses_toclear[i].first); + solver.clauseAllocator.clauseFree(clauses_toclear[i].first); } inline void Gaussian::set_matrixset_to_cur() @@ -104,7 +104,7 @@ const bool Gaussian::full_init() case propagation: unit_truths += last_trail_size - solver.trail.size(); do_again_gauss = true; - solver.ok = (solver.propagate() == NULL); + solver.ok = (solver.propagate().isNULL()); if (!solver.ok) return false; break; case nothing: @@ -566,7 +566,7 @@ Gaussian::gaussian_ret Gaussian::handle_matrix_confl(Clause*& confl, const matri assert(best_row != UINT_MAX); m.matrix.getVarsetAt(best_row).fill(tmp_clause, solver.assigns, col_to_var_original); - confl = (Clause*)XorClause_new(tmp_clause, false, solver.learnt_clause_group++); + confl = (Clause*)solver.clauseAllocator.XorClause_new(tmp_clause, false, solver.learnt_clause_group++); Clause& cla = *confl; #ifdef STATS_NEEDED if (solver.dynamic_behaviour_analysis) @@ -783,7 +783,7 @@ Gaussian::gaussian_ret Gaussian::handle_matrix_prop(matrixset& m, const uint row #endif m.matrix.getVarsetAt(row).fill(tmp_clause, solver.assigns, col_to_var_original); - Clause& cla = *(Clause*)XorClause_new(tmp_clause, false, solver.learnt_clause_group++); + Clause& cla = *(Clause*)solver.clauseAllocator.XorClause_new(tmp_clause, false, solver.learnt_clause_group++); #ifdef VERBOSE_DEBUG cout << "(" << matrix_no << ")matrix prop clause: "; cla.plainPrint(); @@ -795,7 +795,7 @@ Gaussian::gaussian_ret Gaussian::handle_matrix_prop(matrixset& m, const uint row if (cla.size() == 1) { solver.cancelUntil(0); solver.uncheckedEnqueue(cla[0]); - clauseFree(&cla); + solver.clauseAllocator.clauseFree(&cla); return unit_propagation; } @@ -832,7 +832,7 @@ llbool Gaussian::find_truths(vec& learnt_clause, int& conflictC) case conflict: { useful_confl++; llbool ret = solver.handle_conflict(learnt_clause, confl, conflictC, true); - clauseFree(confl); + solver.clauseAllocator.clauseFree(confl); if (ret != l_Nothing) return ret; return l_Continue; @@ -846,7 +846,7 @@ llbool Gaussian::find_truths(vec& learnt_clause, int& conflictC) unit_truths++; useful_confl++; if (confl->size() == 0) { - clauseFree(confl); + solver.clauseAllocator.clauseFree(confl); return l_False; } @@ -859,13 +859,13 @@ llbool Gaussian::find_truths(vec& learnt_clause, int& conflictC) solver.cancelUntil(0); if (solver.assigns[lit.var()].isDef()) { - clauseFree(confl); + solver.clauseAllocator.clauseFree(confl); return l_False; } solver.uncheckedEnqueue(lit); - clauseFree(confl); + solver.clauseAllocator.clauseFree(confl); return l_Continue; } case nothing: diff --git a/src/sat/cryptominisat2/Gaussian.h b/src/sat/cryptominisat2/Gaussian.h index 2a80e94..6dc8b0d 100644 --- a/src/sat/cryptominisat2/Gaussian.h +++ b/src/sat/cryptominisat2/Gaussian.h @@ -186,7 +186,7 @@ inline void Gaussian::canceling(const uint sublevel) return; uint a = 0; for (int i = clauses_toclear.size()-1; i >= 0 && clauses_toclear[i].second > sublevel; i--) { - clauseFree(clauses_toclear[i].first); + solver.clauseAllocator.clauseFree(clauses_toclear[i].first); a++; } clauses_toclear.resize(clauses_toclear.size()-a); diff --git a/src/sat/cryptominisat2/Makefile b/src/sat/cryptominisat2/Makefile index b5b64e5..bfc96a5 100644 --- a/src/sat/cryptominisat2/Makefile +++ b/src/sat/cryptominisat2/Makefile @@ -4,11 +4,13 @@ include $(TOP)/scripts/Makefile.common MTL = mtl MTRAND = MTRand SOURCES = Logger.cpp Solver.cpp PackedRow.cpp \ - XorFinder.cpp Conglomerate.cpp VarReplacer.cpp \ + XorFinder.cpp VarReplacer.cpp \ FindUndef.cpp ClauseCleaner.cpp RestartTypeChooser.cpp \ Clause.cpp FailedVarSearcher.cpp PartFinder.cpp \ - Subsumer.cpp PartHandler.cpp XorSubsumer.cpp SmallPtr.cpp \ - Gaussian.cpp MatrixFinder.cpp StateSaver.cpp + Subsumer.cpp PartHandler.cpp XorSubsumer.cpp \ + Gaussian.cpp MatrixFinder.cpp StateSaver.cpp \ + ClauseAllocator.cpp UselessBinRemover.cpp \ + OnlyNonLearntBins.cpp OBJECTS = $(SOURCES:.cpp=.o) LIB = libminisat.a CFLAGS += -I$(MTL) -I$(MTRAND) -DEXT_HASH_MAP -ffloat-store $(CFLAGS_M32) -c diff --git a/src/sat/cryptominisat2/OnlyNonLearntBins.cpp b/src/sat/cryptominisat2/OnlyNonLearntBins.cpp new file mode 100644 index 0000000..785d7e9 --- /dev/null +++ b/src/sat/cryptominisat2/OnlyNonLearntBins.cpp @@ -0,0 +1,155 @@ +/*********************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +This program is free software: you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation, either version 3 of the License, or +(at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program. If not, see . +************************************************************************/ + +#include "OnlyNonLearntBins.h" + +#include +#include "Solver.h" +#include "Clause.h" +#include "VarReplacer.h" +#include "ClauseCleaner.h" +#include "time_mem.h" + +namespace MINISAT +{ +using namespace MINISAT; + +OnlyNonLearntBins::OnlyNonLearntBins(Solver& _solver) : + solver(_solver) +{} + +const bool OnlyNonLearntBins::propagate() +{ + while (solver.qhead < solver.trail.size()) { + Lit p = solver.trail[solver.qhead++]; + vec & wbin = binwatches[p.toInt()]; + solver.propagations += wbin.size()/2; + for(WatchedBin *k = wbin.getData(), *end = wbin.getDataEnd(); k != end; k++) { + lbool val = solver.value(k->impliedLit); + if (val.isUndef()) { + solver.uncheckedEnqueueLight(k->impliedLit); + } else if (val == l_False) { + return false; + } + } + } + + return true; +} + +const bool OnlyNonLearntBins::propagateBinExcept(const Lit& exceptLit) +{ + while (solver.qhead < solver.trail.size()) { + Lit p = solver.trail[solver.qhead++]; + vec & wbin = binwatches[p.toInt()]; + solver.propagations += wbin.size()/2; + for(WatchedBin *k = wbin.getData(), *end = wbin.getDataEnd(); k != end; k++) { + lbool val = solver.value(k->impliedLit); + if (val.isUndef() && k->impliedLit != exceptLit) { + solver.uncheckedEnqueueLight(k->impliedLit); + } else if (val == l_False) { + return false; + } + } + } + + return true; +} + +const bool OnlyNonLearntBins::propagateBinOneLevel() +{ + Lit p = solver.trail[solver.qhead]; + vec & wbin = binwatches[p.toInt()]; + solver.propagations += wbin.size()/2; + for(WatchedBin *k = wbin.getData(), *end = wbin.getDataEnd(); k != end; k++) { + lbool val = solver.value(k->impliedLit); + if (val.isUndef()) { + solver.uncheckedEnqueueLight(k->impliedLit); + } else if (val == l_False) { + return false; + } + } + + return true; +} + +const bool OnlyNonLearntBins::fill() +{ + double myTime = cpuTime(); + assert(solver.performReplace); + while (solver.performReplace && solver.varReplacer->getClauses().size() > 0) { + if (!solver.varReplacer->performReplace(true)) return false; + solver.clauseCleaner->removeAndCleanAll(true); + } + assert(solver.varReplacer->getClauses().size() == 0); + solver.clauseCleaner->moveBinClausesToBinClauses(); + binwatches.growTo(solver.nVars()*2); + + for(Clause **i = solver.binaryClauses.getData(), **end = solver.binaryClauses.getDataEnd(); i != end; i++) { + Clause& c = **i; + if (c.learnt()) continue; + + binwatches[(~c[0]).toInt()].push(WatchedBin(c[1])); + binwatches[(~c[1]).toInt()].push(WatchedBin(c[0])); + } + + if (solver.verbosity >= 2) { + std::cout << "c Time to fill non-learnt binary watchlists:" + << std::fixed << std::setprecision(2) << std::setw(5) + << cpuTime() - myTime << " s" << std::endl; + } + + return true; +} + +void OnlyNonLearntBins::removeBin(Lit lit1, Lit lit2) +{ + uint32_t index0 = lit1.toInt(); + uint32_t index1 = lit2.toInt(); + if (index1 > index0) std::swap(index0, index1); + uint64_t final = index0; + final |= ((uint64_t)index1) << 32; + toRemove.insert(final); + + solver.removeWatchedBinClAll(binwatches[(~lit1).toInt()], lit2); + solver.removeWatchedBinClAll(binwatches[(~lit2).toInt()], lit1); +} + +const uint32_t OnlyNonLearntBins::removeBins() +{ + Clause **i, **j; + i = j = solver.binaryClauses.getData(); + uint32_t num = 0; + for (Clause **end = solver.binaryClauses.getDataEnd(); i != end; i++, num++) { + Clause& c = **i; + uint32_t index0 = c[0].toInt(); + uint32_t index1 = c[1].toInt(); + if (index1 > index0) std::swap(index0, index1); + uint64_t final = index0; + final |= ((uint64_t)index1) << 32; + + if (toRemove.find(final) == toRemove.end()) { + *j++ = *i; + } else { + solver.clauseAllocator.clauseFree(*i); + } + } + solver.binaryClauses.shrink(i-j); + return (i - j); +} + +}; //NAMESPACE MINISAT diff --git a/src/sat/cryptominisat2/OnlyNonLearntBins.h b/src/sat/cryptominisat2/OnlyNonLearntBins.h new file mode 100644 index 0000000..ed73cc2 --- /dev/null +++ b/src/sat/cryptominisat2/OnlyNonLearntBins.h @@ -0,0 +1,54 @@ +/*********************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +This program is free software: you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation, either version 3 of the License, or +(at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program. If not, see . +************************************************************************/ + +#ifndef ONLYNONLEARNTBINS_H +#define ONLYNONLEARNTBINS_H + +#include "Solver.h" +#include +using std::set; + +namespace MINISAT +{ +using namespace MINISAT; + +class OnlyNonLearntBins { + public: + OnlyNonLearntBins(Solver& solver); + + //propagation + const bool propagate(); + const bool propagateBinExcept(const Lit& exceptLit); + const bool propagateBinOneLevel(); + + //Management of clauses + const bool fill(); + void removeBin(Lit lit1, Lit lit2); + void removeClause(Clause& c); + const uint32_t removeBins(); + + private: + vec > binwatches; + set toRemove; + + Solver& solver; +}; + +}; //NAMESPACE MINISAT + +#endif //ONLYNONLEARNTBINS_H + diff --git a/src/sat/cryptominisat2/PartFinder.cpp b/src/sat/cryptominisat2/PartFinder.cpp index 534032f..969afe6 100644 --- a/src/sat/cryptominisat2/PartFinder.cpp +++ b/src/sat/cryptominisat2/PartFinder.cpp @@ -86,7 +86,7 @@ const bool PartFinder::findParts() if (solver.verbosity >= 2 || (solver.verbosity >=1 && parts > 1)) { std::cout << "c | Found parts: " << std::setw(10) << parts << " time: " << std::setprecision(2) << std::setw(4) << cpuTime() - time - << " s" << std::setw(28) << " |" << std::endl; + << " s" << std::setw(51) << " |" << std::endl; } return true; @@ -147,7 +147,8 @@ const uint PartFinder::setParts() std::cout << "c | Found part " << std::setw(8) << i << " vars: " << std::setw(10) << reverseTable[i].size() << " clauses:" << std::setw(10) << numClauseInPart[i] - << " lits size:" << std::setw(10) << sumLitsInPart[i] << std::endl; + << " lits size:" << std::setw(10) << sumLitsInPart[i] + << std::setw(12) << " | " << std::endl; } parts++; } diff --git a/src/sat/cryptominisat2/PartHandler.cpp b/src/sat/cryptominisat2/PartHandler.cpp index 27c5674..94e1cc9 100644 --- a/src/sat/cryptominisat2/PartHandler.cpp +++ b/src/sat/cryptominisat2/PartHandler.cpp @@ -19,6 +19,7 @@ along with this program. If not, see . #include "VarReplacer.h" #include #include +#include //#define VERBOSE_DEBUG @@ -85,6 +86,13 @@ const bool PartHandler::handle() newSolver.fixRestartType = solver.fixRestartType; newSolver.var_inc = solver.var_inc; newSolver.polarity_mode = solver.polarity_mode; + + //Memory-usage reduction + newSolver.schedSimplification = false; + newSolver.doSubsumption = false; + newSolver.doXorSubsumption = false; + newSolver.doPartHandler = false; + std::sort(vars.begin(), vars.end()); uint32_t i2 = 0; for (Var var = 0; var < solver.nVars(); var++) { @@ -137,7 +145,7 @@ const bool PartHandler::handle() for (uint32_t i = 0; i < newSolver.trail.size(); i++) { solver.uncheckedEnqueue(newSolver.trail[i]); } - solver.ok = (solver.propagate() == NULL); + solver.ok = (solver.propagate().isNULL()); assert(solver.ok); for (Var var = 0; var < newSolver.nVars(); var++) { @@ -156,7 +164,8 @@ const bool PartHandler::handle() std::cout << "c Solved part" << std::endl; } if (solver.verbosity >= 1) - std::cout << "c Coming back to original instance" << std::endl; + std::cout << "c Coming back to original instance" + << std::setw(57) << " |" << std::endl; solver.order_heap.filter(Solver::VarFilter(solver)); @@ -279,7 +288,7 @@ void PartHandler::moveLearntClauses(vec& cs, Solver& newSolver, const u solver.detachClause(c); newSolver.addLearntClause(c, c.getGroup(), c.activity()); - clauseFree(&c); + solver.clauseAllocator.clauseFree(&c); } else { #ifdef VERBOSE_DEBUG std::cout << "Learnt clause in other part:"; c.plainPrint(); diff --git a/src/sat/cryptominisat2/PartHandler.h b/src/sat/cryptominisat2/PartHandler.h index a1fe6c1..f73bc98 100644 --- a/src/sat/cryptominisat2/PartHandler.h +++ b/src/sat/cryptominisat2/PartHandler.h @@ -42,6 +42,8 @@ class PartHandler void newVar(); void addSavedState(); void readdRemovedClauses(); + + friend class ClauseAllocator; private: struct sort_pred { diff --git a/src/sat/cryptominisat2/SmallPtr.cpp b/src/sat/cryptominisat2/SmallPtr.cpp deleted file mode 100644 index 6fca7bc..0000000 --- a/src/sat/cryptominisat2/SmallPtr.cpp +++ /dev/null @@ -1,17 +0,0 @@ -/* -Please see LICENSE-CPOL.html in the root directory for the licencing of this file. -Originally by: cppnow -Link: http://www.codeproject.com/KB/cpp/smallptr.aspx -*/ - -#include "SmallPtr.h" - -namespace MINISAT -{ -using namespace MINISAT; - -uintptr_t sptr_base::_segs = 1; -//boost::mutex sptr_base::_m; -uintptr_t sptr_base::_seg_map[sptr_base::ALIGNMENT] = { 0 }; - -}; //NAMESPACE MINISAT diff --git a/src/sat/cryptominisat2/SmallPtr.h b/src/sat/cryptominisat2/SmallPtr.h deleted file mode 100644 index a530c54..0000000 --- a/src/sat/cryptominisat2/SmallPtr.h +++ /dev/null @@ -1,277 +0,0 @@ -/* -Please see LICENSE-CPOL.html in the root directory for the licencing of this file. -Originally by: cppnow -Link: http://www.codeproject.com/KB/cpp/smallptr.aspx -*/ - -#ifndef __SMALL_PTR_H__ -#define __SMALL_PTR_H__ - -//#include - -#include -#include -#include "singleton.hpp" -//#include -//#include - -#ifdef _MSC_VER -#include -#else -#include -#endif //_MSC_VER - -#define is_n_aligned(T, N) ((sizeof(T) % (N)) == 0) - -#ifdef WIN32 -# ifdef WIN64 -# define USE64 -# else -# define USE32 -# endif -#endif - -#ifdef __GNUG__ -# if defined(__amd64__) || defined(__x86_64__) -# define USE64 -# elif defined(__i386__) -# define USE32 -# endif -#endif - -#include - -namespace MINISAT -{ -using namespace MINISAT; - -class bad_alignment : public std::exception -{ -public: - bad_alignment(const char *const& w) {} -}; -class bad_segment : public std::exception -{ -public: - bad_segment(const char *const& w) {} -}; - -class sptr_base -{ -protected: - static const uint32_t ALIGNMENT_BITS = 2; - static const uint32_t ALIGNMENT = (1< lock(_m); - for (i = 0; i < s; ++i) - if (_seg_map[i] == p) - return i; - - i = _segs++; - if (_segs > ALIGNMENT) { - //throw bad_segment("Segment out of range"); - exit(-1); - } - - _seg_map[i] = p; - return i; - } - -}; - -template -class sptr : public sptr_base -{ -public: - typedef TYPE type; - typedef TYPE* native_pointer_type; - typedef const TYPE* const_native_pointer_type; - - sptr() throw() - : _ptr(0) - {} - - // Copy constructor - sptr(const sptr& o) throw() - : _ptr(o._ptr) - { - } - - // Copy from a related pointer type - // Although just copying _ptr would be more efficient - it may - // also be wrong - e.g. multiple inheritence - template - sptr(const sptr& o) - : _ptr(encode(static_cast(o.get()))) - { - } - - template - sptr(const O* p) - : _ptr(encode(static_cast(p))) - { - } - - sptr& operator=(const sptr& o) throw() - { - _ptr = o._ptr; - return *this; - } - - template - sptr& operator=(const sptr& o) - { - _ptr = encode(static_cast(o.get())); - return *this; - } - -private: - inline uint32_t encode(const_native_pointer_type ptr) const - { -#ifdef USE64 - - uintptr_t p = reinterpret_cast(ptr); - - if ((p & ALIGNMENT_MASK) != 0) { - //throw bad_alignment("Pointer is not aligned"); - exit(-1); - } - - return (uint32_t)(ptr2seg(p) + p); - -#else // 32 bit machine - return reinterpret_cast(ptr); -#endif - } - - inline native_pointer_type decode(uint32_t e) const - { -#ifdef USE64 - uintptr_t el = e; - uintptr_t ptr = (_seg_map[el & ALIGNMENT_MASK] + el) & ~ALIGNMENT_MASK; - - return reinterpret_cast(ptr); -#else - return reinterpret_cast(e); -#endif - } - - void check_alignment() const - { - //BOOST_STATIC_ASSERT(is_n_aligned(TYPE, ALIGNMENT)); - } - - void inc_sptr(uint32_t& e, uintptr_t offset = 1) - { - check_alignment(); -#ifdef USE64 - uintptr_t el = e; - uintptr_t seg = el & ALIGNMENT_MASK; - el += offset*ALIGNMENT; - - // check for overflow - if (el > 0xFFFFFFFFULL) - return encode(decode(e)+1); - e = (uint32_t)el; -#else - e+= (uint32_t)offset; -#endif - } - - void dec_sptr(uint32_t& e, size_t offset = 1) - { - check_alignment(); -#ifdef USE64 - uintptr_t el = e; - uintptr_t seg = el & ALIGNMENT_MASK; - e-= offset*ALIGNMENT; - - // check for underflow - if (el > 0xFFFFFFFFULL) - return encode(decode(e)-1); - e = (uint32_t)el; -#else - e -= (uint32_t)offset; -#endif - } -public: - - TYPE* get() const throw() { return decode(_ptr); } - - // Pointer operators - - TYPE& operator*() { return *decode(_ptr); } - const TYPE& operator*() const { return *decode(_ptr); } - - TYPE* operator->() { return decode(_ptr); } - const TYPE* operator->() const { return decode(_ptr); } - - template - bool operator==(const sptr& o) const - { - return o._ptr == this->_ptr; - } - - operator TYPE*() const { return get(); } - - sptr& operator++( ) - { - inc_sptr(_ptr); - return *this; - } - - sptr operator++( int ) - { - sptr p = *this; - inc_sptr(_ptr); - return p; - } - - sptr& operator--( ) - { - dec_sptr(_ptr); - return *this; - } - sptr operator--( int ) - { - sptr p = *this; - dec_sptr(_ptr); - return p; - } - - sptr& operator+=(size_t offset) - { - inc_sptr(_ptr, offset); - return *this; - } - - sptr& operator-=(size_t offset) - { - dec_sptr(_ptr, offset); - return *this; - } - -private: - uint32_t _ptr; -}; - -}; //NAMESPACE MINISAT - -#endif - diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp index 2da63b2..cb7ee3e 100644 --- a/src/sat/cryptominisat2/Solver.cpp +++ b/src/sat/cryptominisat2/Solver.cpp @@ -40,6 +40,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "PartHandler.h" #include "XorSubsumer.h" #include "StateSaver.h" +#include "UselessBinRemover.h" +#include "OnlyNonLearntBins.h" #ifdef USE_GAUSS #include "Gaussian.h" @@ -90,7 +92,6 @@ Solver::Solver() : , doVarElim (true) , doSubsume1 (true) , failedVarSearch (true) - , readdOldLearnts (false) , addExtraBins (true) , removeUselessBins(true) , regularRemoveUselessBins(true) @@ -107,11 +108,12 @@ Solver::Solver() : , nbDL2(0), nbBin(0), lastNbBin(0), becameBinary(0), lastSearchForBinaryXor(0), nbReduceDB(0) , improvedClauseNo(0), improvedClauseSize(0) - + #ifdef USE_GAUSS , sum_gauss_called (0) , sum_gauss_confl (0) , sum_gauss_prop (0) , sum_gauss_unit_truths (0) + #endif //USE_GAUSS , ok (true) , var_inc (128) , cla_inc (1) @@ -157,16 +159,15 @@ Solver::Solver() : Solver::~Solver() { - for (uint32_t i = 0; i != learnts.size(); i++) clauseFree(learnts[i]); - for (uint32_t i = 0; i != clauses.size(); i++) clauseFree(clauses[i]); - for (uint32_t i = 0; i != binaryClauses.size(); i++) clauseFree(binaryClauses[i]); - for (uint32_t i = 0; i != xorclauses.size(); i++) clauseFree(xorclauses[i]); - for (uint32_t i = 0; i != removedLearnts.size(); i++) clauseFree(removedLearnts[i]); + for (uint32_t i = 0; i != learnts.size(); i++) clauseAllocator.clauseFree(learnts[i]); + for (uint32_t i = 0; i != clauses.size(); i++) clauseAllocator.clauseFree(clauses[i]); + for (uint32_t i = 0; i != binaryClauses.size(); i++) clauseAllocator.clauseFree(binaryClauses[i]); + for (uint32_t i = 0; i != xorclauses.size(); i++) clauseAllocator.clauseFree(xorclauses[i]); #ifdef USE_GAUSS clearGaussMatrixes(); delete matrixFinder; #endif - for (uint32_t i = 0; i != freeLater.size(); i++) clauseFree(freeLater[i]); + //for (uint32_t i = 0; i != freeLater.size(); i++) clauseAllocator.clauseFree(freeLater[i]); delete varReplacer; delete clauseCleaner; @@ -194,7 +195,7 @@ Var Solver::newVar(bool dvar) binwatches.push(); // (list for positive literal) binwatches.push(); // (list for negative literal) xorwatches.push(); // (list for variables in xors) - reason .push((Clause*)NULL); + reason .push(PropagatedFrom()); assigns .push(l_Undef); level .push(-1); activity .push(0); @@ -211,9 +212,9 @@ Var Solver::newVar(bool dvar) insertVarOrder(v); varReplacer->newVar(); - partHandler->newVar(); - subsumer->newVar(); - xorSubsumer->newVar(); + if (doPartHandler) partHandler->newVar(); + if (doSubsumption) subsumer->newVar(); + if (doXorSubsumption) xorSubsumer->newVar(); insertVarOrder(v); @@ -262,7 +263,7 @@ XorClause* Solver::addXorClauseInt(T& ps, bool xor_clause_inverted, const uint32 } case 1: { uncheckedEnqueue(Lit(ps[0].var(), xor_clause_inverted)); - ok = (propagate() == NULL); + ok = (propagate().isNULL()); return NULL; } case 2: { @@ -270,15 +271,13 @@ XorClause* Solver::addXorClauseInt(T& ps, bool xor_clause_inverted, const uint32 cout << "--> xor is 2-long, replacing var " << ps[0].var()+1 << " with " << (!xor_clause_inverted ? "-" : "") << ps[1].var()+1 << endl; #endif - learnt_clause_group = std::max(group+1, learnt_clause_group); ps[0] = ps[0].unsign(); ps[1] = ps[1].unsign(); varReplacer->replace(ps, xor_clause_inverted, group); return NULL; } default: { - learnt_clause_group = std::max(group+1, learnt_clause_group); - XorClause* c = XorClause_new(ps, xor_clause_inverted, group); + XorClause* c = clauseAllocator.XorClause_new(ps, xor_clause_inverted, group); attachClause(*c); return c; } @@ -304,8 +303,10 @@ bool Solver::addXorClause(T& ps, bool xor_clause_inverted, const uint group, cha } #ifdef STATS_NEEDED - if (dynamic_behaviour_analysis) + if (dynamic_behaviour_analysis) { logger.set_group_name(group, group_name); + learnt_clause_group = std::max(group+1, learnt_clause_group); + } #endif if (!ok) @@ -382,12 +383,11 @@ Clause* Solver::addClauseInt(T& ps, uint group) return NULL; } else if (ps.size() == 1) { uncheckedEnqueue(ps[0]); - ok = (propagate() == NULL); + ok = (propagate().isNULL()); return NULL; } - - learnt_clause_group = std::max(group+1, learnt_clause_group); - Clause* c = Clause_new(ps, group); + + Clause* c = clauseAllocator.Clause_new(ps, group); attachClause(*c); return c; @@ -411,8 +411,10 @@ bool Solver::addClause(T& ps, const uint group, char* group_name) } #ifdef STATS_NEEDED - if (dynamic_behaviour_analysis) + if (dynamic_behaviour_analysis) { logger.set_group_name(group, group_name); + learnt_clause_group = std::max(group+1, learnt_clause_group); + } #endif if (!ok) @@ -452,8 +454,8 @@ void Solver::attachClause(XorClause& c) assert(assigns[c[1].var()] == l_Undef); #endif //DEBUG_ATTACH - xorwatches[c[0].var()].push(&c); - xorwatches[c[1].var()].push(&c); + xorwatches[c[0].var()].push(clauseAllocator.getOffset((Clause*)&c)); + xorwatches[c[1].var()].push(clauseAllocator.getOffset((Clause*)&c)); clauses_literals += c.size(); } @@ -461,15 +463,16 @@ void Solver::attachClause(XorClause& c) void Solver::attachClause(Clause& c) { assert(c.size() > 1); - int index0 = (~c[0]).toInt(); - int index1 = (~c[1]).toInt(); + uint32_t index0 = (~c[0]).toInt(); + uint32_t index1 = (~c[1]).toInt(); if (c.size() == 2) { - binwatches[index0].push(WatchedBin(&c, c[1])); - binwatches[index1].push(WatchedBin(&c, c[0])); + binwatches[index0].push(WatchedBin(c[1])); + binwatches[index1].push(WatchedBin(c[0])); } else { - watches[index0].push(Watched(&c, c[c.size()/2])); - watches[index1].push(Watched(&c, c[c.size()/2])); + ClauseOffset offset = clauseAllocator.getOffset(&c); + watches[index0].push(Watched(offset, c[c.size()/2])); + watches[index1].push(Watched(offset, c[c.size()/2])); } if (c.learnt()) learnts_literals += c.size(); @@ -480,10 +483,11 @@ void Solver::attachClause(Clause& c) void Solver::detachClause(const XorClause& c) { assert(c.size() > 1); - assert(find(xorwatches[c[0].var()], &c)); - assert(find(xorwatches[c[1].var()], &c)); - remove(xorwatches[c[0].var()], &c); - remove(xorwatches[c[1].var()], &c); + ClauseOffset offset = clauseAllocator.getOffset(&c); + assert(find(xorwatches[c[0].var()], offset)); + assert(find(xorwatches[c[1].var()], offset)); + remove(xorwatches[c[0].var()], offset); + remove(xorwatches[c[1].var()], offset); clauses_literals -= c.size(); } @@ -492,17 +496,19 @@ void Solver::detachClause(const Clause& c) { assert(c.size() > 1); if (c.size() == 2) { - assert(findWatchedBinCl(binwatches[(~c[0]).toInt()], &c)); - assert(findWatchedBinCl(binwatches[(~c[1]).toInt()], &c)); + assert(findWatchedBinCl(binwatches[(~c[0]).toInt()], c[1])); + assert(findWatchedBinCl(binwatches[(~c[1]).toInt()], c[0])); - removeWatchedBinCl(binwatches[(~c[0]).toInt()], &c); - removeWatchedBinCl(binwatches[(~c[1]).toInt()], &c); + removeWatchedBinCl(binwatches[(~c[0]).toInt()], c[1]); + removeWatchedBinCl(binwatches[(~c[1]).toInt()], c[0]); } else { - assert(findWatchedCl(watches[(~c[0]).toInt()], &c)); - assert(findWatchedCl(watches[(~c[1]).toInt()], &c)); + ClauseOffset offset = clauseAllocator.getOffset(&c); - removeWatchedCl(watches[(~c[0]).toInt()], &c); - removeWatchedCl(watches[(~c[1]).toInt()], &c); + assert(findWatchedCl(watches[(~c[0]).toInt()], offset)); + assert(findWatchedCl(watches[(~c[1]).toInt()], offset)); + + removeWatchedCl(watches[(~c[0]).toInt()], offset); + removeWatchedCl(watches[(~c[1]).toInt()], offset); } if (c.learnt()) learnts_literals -= c.size(); @@ -514,15 +520,16 @@ void Solver::detachModifiedClause(const Lit lit1, const Lit lit2, const uint ori assert(origSize > 1); if (origSize == 2) { - assert(findWatchedBinCl(binwatches[(~lit1).toInt()], address)); - assert(findWatchedBinCl(binwatches[(~lit2).toInt()], address)); - removeWatchedBinCl(binwatches[(~lit1).toInt()], address); - removeWatchedBinCl(binwatches[(~lit2).toInt()], address); + assert(findWatchedBinCl(binwatches[(~lit1).toInt()], lit2)); + assert(findWatchedBinCl(binwatches[(~lit2).toInt()], lit1)); + removeWatchedBinCl(binwatches[(~lit1).toInt()], lit2); + removeWatchedBinCl(binwatches[(~lit2).toInt()], lit1); } else { - assert(findW(watches[(~lit1).toInt()], address)); - assert(findW(watches[(~lit2).toInt()], address)); - removeW(watches[(~lit1).toInt()], address); - removeW(watches[(~lit2).toInt()], address); + ClauseOffset offset = clauseAllocator.getOffset(address); + assert(findW(watches[(~lit1).toInt()], offset)); + assert(findW(watches[(~lit2).toInt()], offset)); + removeW(watches[(~lit1).toInt()], offset); + removeW(watches[(~lit2).toInt()], offset); } if (address->learnt()) learnts_literals -= origSize; else clauses_literals -= origSize; @@ -531,11 +538,12 @@ void Solver::detachModifiedClause(const Lit lit1, const Lit lit2, const uint ori void Solver::detachModifiedClause(const Var var1, const Var var2, const uint origSize, const XorClause* address) { assert(origSize > 2); - - assert(find(xorwatches[var1], address)); - assert(find(xorwatches[var2], address)); - remove(xorwatches[var1], address); - remove(xorwatches[var2], address); + + ClauseOffset offset = clauseAllocator.getOffset(address); + assert(find(xorwatches[var1], offset)); + assert(find(xorwatches[var2], offset)); + remove(xorwatches[var1], offset); + remove(xorwatches[var2], offset); clauses_literals -= origSize; } @@ -665,17 +673,24 @@ void Solver::calculateDefaultPolarities() tallyVotes(xorclauses, votes); Var i = 0; + uint32_t posPolars = 0; + uint32_t undecidedPolars = 0; for (vector::const_iterator it = votes.begin(), end = votes.end(); it != end; it++, i++) { polarity[i] = (*it >= 0.0); + posPolars += (*it < 0.0); + undecidedPolars += (*it == 0.0); #ifdef VERBOSE_DEBUG_POLARITIES std::cout << !defaultPolarities[i] << ", "; #endif //VERBOSE_DEBUG_POLARITIES } if (verbosity >= 2) { - std::cout << "c | Calc-ed default polarities: " - << std::fixed << std::setw(6) << std::setprecision(2) << cpuTime()-time << " s" - << " |" << std:: endl; + std::cout << "c | Calc default polars - " + << " time: " << std::fixed << std::setw(6) << std::setprecision(2) << cpuTime()-time << " s" + << " pos: " << std::setw(7) << posPolars + << " undec: " << std::setw(7) << undecidedPolars + << " neg: " << std::setw(7) << nVars()- undecidedPolars - posPolars + << std::setw(8) << " |" << std:: endl; } } else { std::fill(polarity.begin(), polarity.end(), defaultPolarity()); @@ -784,11 +799,10 @@ bool subset(const T1& A, const T2& B, vector& seen) | Effect: | Will undo part of the trail, upto but not beyond the assumption of the current decision level. |________________________________________________________________________________________________@*/ -Clause* Solver::analyze(Clause* confl, vec& out_learnt, int& out_btlevel, uint32_t &nbLevels, const bool update) +Clause* Solver::analyze(PropagatedFrom confl, vec& out_learnt, int& out_btlevel, uint32_t &nbLevels, const bool update) { int pathC = 0; Lit p = lit_Undef; - Clause* oldConfl = NULL; // Generate conflict clause: // @@ -796,17 +810,18 @@ Clause* Solver::analyze(Clause* confl, vec& out_learnt, int& out_btlevel, u int index = trail.size() - 1; out_btlevel = 0; + PropagatedFrom oldConfl; + do { - assert(confl != NULL); // (otherwise should be UIP) - Clause& c = *confl; - if (p != lit_Undef) - reverse_binary_clause(c); + assert(!confl.isNULL()); // (otherwise should be UIP) - if (update && restartType == static_restart && c.learnt()) - claBumpActivity(c); + if (update && restartType == static_restart && !confl.isBinary() && confl.getClause()->learnt()) + claBumpActivity(*confl.getClause()); - for (uint j = (p == lit_Undef) ? 0 : 1; j != c.size(); j++) { - const Lit& q = c[j]; + for (uint j = (p == lit_Undef) ? 0 : 1, size = confl.size(); j != size; j++) { + Lit q; + if (j == 0 && confl.isBinary()) q = failBinLit; + else q = confl[j]; const Var my_var = q.var(); if (!seen[my_var] && level[my_var] > 0) { @@ -815,7 +830,10 @@ Clause* Solver::analyze(Clause* confl, vec& out_learnt, int& out_btlevel, u if (level[my_var] >= (int)decisionLevel()) { pathC++; #ifdef UPDATEVARACTIVITY - if (lastSelectedRestartType == dynamic_restart && reason[q.var()] != NULL && reason[q.var()]->learnt()) + if (lastSelectedRestartType == dynamic_restart + && !reason[q.var()].isBinary() + && !reason[q.var()].isNULL() + && reason[q.var()].getClause()->learnt()) lastDecisionLevel.push(q.var()); #endif } else { @@ -831,7 +849,7 @@ Clause* Solver::analyze(Clause* confl, vec& out_learnt, int& out_btlevel, u p = trail[index+1]; oldConfl = confl; confl = reason[p.var()]; - __builtin_prefetch(confl, 1, 0); + if (!confl.isBinary()) __builtin_prefetch(confl.getClause(), 1, 0); seen[p.var()] = 0; pathC--; @@ -848,19 +866,19 @@ Clause* Solver::analyze(Clause* confl, vec& out_learnt, int& out_btlevel, u out_learnt.copyTo(analyze_toclear); for (i = j = 1; i < out_learnt.size(); i++) - if (reason[out_learnt[i].var()] == NULL || !litRedundant(out_learnt[i], abstract_level)) + if (reason[out_learnt[i].var()].isNULL() || !litRedundant(out_learnt[i], abstract_level)) out_learnt[j++] = out_learnt[i]; } else { out_learnt.copyTo(analyze_toclear); for (i = j = 1; i < out_learnt.size(); i++) { - Clause& c = *reason[out_learnt[i].var()]; - reverse_binary_clause(c); - - for (uint k = 1; k < c.size(); k++) + PropagatedFrom c(reason[out_learnt[i].var()]); + + for (uint k = 1, size = c.size(); k < size; k++) { if (!seen[c[k].var()] && level[c[k].var()] > 0) { out_learnt[j++] = out_learnt[i]; break; } + } } } max_literals += out_learnt.size(); @@ -886,7 +904,8 @@ Clause* Solver::analyze(Clause* confl, vec& out_learnt, int& out_btlevel, u nbLevels = calcNBLevels(out_learnt); #ifdef UPDATEVARACTIVITY for(uint32_t i = 0; i != lastDecisionLevel.size(); i++) { - if (reason[lastDecisionLevel[i]]->activity() < nbLevels) + PropagatedFrom cl = reason[lastDecisionLevel[i]]; + if (!cl.isBinary() && cl.getClause()->activity() < nbLevels) varBumpActivity(lastDecisionLevel[i]); } lastDecisionLevel.clear(); @@ -898,14 +917,15 @@ Clause* Solver::analyze(Clause* confl, vec& out_learnt, int& out_btlevel, u for (uint32_t j = 0; j != analyze_toclear.size(); j++) seen[analyze_toclear[j].var()] = 0; // ('seen[]' is now cleared) - if (out_learnt.size() == 1) - return NULL; + if (out_learnt.size() == 1) return NULL; - if (!oldConfl->isXor() && out_learnt.size() < oldConfl->size()) { - if (!subset(out_learnt, *oldConfl, seen)) return NULL; + if (!oldConfl.isBinary() && !oldConfl.getClause()->isXor() + && out_learnt.size() < oldConfl.getClause()->size()) { + if (!subset(out_learnt, *oldConfl.getClause(), seen)) + return NULL; improvedClauseNo++; - improvedClauseSize += oldConfl->size() - out_learnt.size(); - return oldConfl; + improvedClauseSize += oldConfl.getClause()->size() - out_learnt.size(); + return oldConfl.getClause(); } return NULL; @@ -920,16 +940,15 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels) analyze_stack.push(p); int top = analyze_toclear.size(); while (analyze_stack.size() > 0) { - assert(reason[analyze_stack.last().var()] != NULL); - Clause& c = *reason[analyze_stack.last().var()]; - reverse_binary_clause(c); + assert(!reason[analyze_stack.last().var()].isNULL()); + PropagatedFrom c(reason[analyze_stack.last().var()]); analyze_stack.pop(); - for (uint i = 1; i < c.size(); i++) { + for (uint i = 1, size = c.size(); i < size; i++) { Lit p = c[i]; if (!seen[p.var()] && level[p.var()] > 0) { - if (reason[p.var()] != NULL && (abstractLevel(p.var()) & abstract_levels) != 0) { + if (!reason[p.var()].isNULL() && (abstractLevel(p.var()) & abstract_levels) != 0) { seen[p.var()] = 1; analyze_stack.push(p); analyze_toclear.push(p); @@ -969,12 +988,12 @@ void Solver::analyzeFinal(Lit p, vec& out_conflict) for (int32_t i = (int32_t)trail.size()-1; i >= (int32_t)trail_lim[0]; i--) { Var x = trail[i].var(); if (seen[x]) { - if (reason[x] == NULL) { + if (reason[x].isNULL()) { assert(level[x] > 0); out_conflict.push(~trail[i]); } else { - const Clause& c = *reason[x]; - for (uint j = 1; j < c.size(); j++) + PropagatedFrom c = reason[x]; + for (uint j = 1, size = c.size(); j < size; j++) if (level[c[j].var()] > 0) seen[c[j].var()] = 1; } @@ -986,7 +1005,7 @@ void Solver::analyzeFinal(Lit p, vec& out_conflict) } -void Solver::uncheckedEnqueue(Lit p, ClausePtr from) +void Solver::uncheckedEnqueue(const Lit p, const PropagatedFrom& from) { #ifdef DEBUG_UNCHECKEDENQUEUE_LEVEL0 @@ -1026,9 +1045,9 @@ void Solver::uncheckedEnqueue(Lit p, ClausePtr from) | Post-conditions: | * the propagation queue is empty, even if there was a conflict. |________________________________________________________________________________________________@*/ -Clause* Solver::propagate(const bool update) +PropagatedFrom Solver::propagate(const bool update) { - Clause* confl = NULL; + PropagatedFrom confl; uint32_t num_props = 0; #ifdef VERBOSE_DEBUG @@ -1046,15 +1065,17 @@ Clause* Solver::propagate(const bool update) for(WatchedBin *k = wbin.getData(), *end = wbin.getDataEnd(); k != end; k++) { lbool val = value(k->impliedLit); if (val.isUndef()) { - uncheckedEnqueue(k->impliedLit, k->clause); + uncheckedEnqueue(k->impliedLit, PropagatedFrom(p)); } else if (val == l_False) { - confl = k->clause; + confl = PropagatedFrom(p); + failBinLit = k->impliedLit; //goto EndPropagate; } } } - if (confl != NULL) + if (!confl.isNULL()) { goto EndPropagate; + } //Next, propagate normal clauses Lit p = trail[qhead++]; // 'p' is enqueued fact to propagate. @@ -1067,15 +1088,16 @@ Clause* Solver::propagate(const bool update) #endif for (i = j = ws.getData(), end = ws.getDataEnd(); i != end;) { - if (i+1 != end) - __builtin_prefetch((i+1)->clause, 1, 0); + if (i+1 != end && !value((i+1)->blockedLit).getBool()) + __builtin_prefetch(clauseAllocator.getPointer((i+1)->clause), 1, 0); if(value(i->blockedLit).getBool()) { // Clause is sat *j++ = *i++; continue; } Lit bl = i->blockedLit; - Clause& c = *(i->clause); + Clause& c = *clauseAllocator.getPointer(i->clause); + ClauseOffset origClauseOffset = i->clause; i++; // Make sure the false literal is data[1]: @@ -1088,7 +1110,7 @@ Clause* Solver::propagate(const bool update) // If 0th watch is true, then clause is already satisfied. const Lit& first = c[0]; if (value(first).getBool()) { - j->clause = &c; + j->clause = origClauseOffset; j->blockedLit = first; j++; } else { @@ -1097,17 +1119,17 @@ Clause* Solver::propagate(const bool update) if (value(*k) != l_False) { c[1] = *k; *k = false_lit; - watches[(~c[1]).toInt()].push(Watched(&c, c[0])); + watches[(~c[1]).toInt()].push(Watched(origClauseOffset, c[0])); goto FoundWatch; } } // Did not find watch -- clause is unit under assignment: - j->clause = &c; + j->clause = origClauseOffset; j->blockedLit = bl; j++; if (value(first) == l_False) { - confl = &c; + confl = PropagatedFrom(&c); qhead = trail.size(); // Copy the remaining watches: while (i < end) @@ -1129,7 +1151,7 @@ FoundWatch: ws.shrink_(i - j); //Finally, propagate XOR-clauses - if (xorclauses.size() > 0 && !confl) confl = propagate_xors(p); + if (xorclauses.size() > 0 && confl.isNULL()) confl = propagate_xors(p); } EndPropagate: propagations += num_props; @@ -1142,102 +1164,7 @@ EndPropagate: return confl; } -Clause* Solver::propagateLight() -{ - Clause* confl = NULL; - uint32_t num_props = 0; - uint32_t qheadBin = qhead; - - while (qhead < trail.size()) { - - //First propagate binary clauses - while (qheadBin < trail.size()) { - Lit p = trail[qheadBin++]; - vec & wbin = binwatches[p.toInt()]; - num_props += wbin.size()/2; - for(WatchedBin *k = wbin.getData(), *end = wbin.getDataEnd(); k != end; k++) { - lbool val = value(k->impliedLit); - if (val.isUndef()) { - uncheckedEnqueueLight(k->impliedLit); - } else if (val == l_False) { - confl = k->clause; - goto EndPropagate; - } - } - } - - //Next, propagate normal clauses - Lit p = trail[qhead++]; // 'p' is enqueued fact to propagate. - vec& ws = watches[p.toInt()]; - Watched *i, *j, *end; - num_props += ws.size(); - - for (i = j = ws.getData(), end = ws.getDataEnd(); i != end;) { - if (i+1 != end) - __builtin_prefetch((i+1)->clause, 1, 0); - - if(value(i->blockedLit).getBool()) { // Clause is sat - *j++ = *i++; - continue; - } - Lit bl = i->blockedLit; - Clause& c = *(i->clause); - i++; - - // Make sure the false literal is data[1]: - const Lit false_lit(~p); - if (c[0] == false_lit) - c[0] = c[1], c[1] = false_lit; - - assert(c[1] == false_lit); - - // If 0th watch is true, then clause is already satisfied. - const Lit& first = c[0]; - if (value(first).getBool()) { - j->clause = &c; - j->blockedLit = first; - j++; - } else { - // Look for new watch: - for (Lit *k = &c[2], *end2 = c.getDataEnd(); k != end2; k++) { - if (value(*k) != l_False) { - c[1] = *k; - *k = false_lit; - watches[(~c[1]).toInt()].push(Watched(&c, c[0])); - goto FoundWatch; - } - } - - // Did not find watch -- clause is unit under assignment: - j->clause = &c; - j->blockedLit = bl; - j++; - if (value(first) == l_False) { - confl = &c; - qhead = trail.size(); - // Copy the remaining watches: - while (i < end) - *j++ = *i++; - } else { - uncheckedEnqueueLight(first); - } - } - FoundWatch: - ; - } - ws.shrink_(i - j); - - //Finally, propagate XOR-clauses - if (xorclauses.size() > 0 && !confl) confl = propagate_xors(p); - } - EndPropagate: - propagations += num_props; - simpDB_props -= num_props; - - return confl; -} - -Clause* Solver::propagateBin() +PropagatedFrom Solver::propagateBin() { while (qhead < trail.size()) { Lit p = trail[qhead++]; @@ -1249,83 +1176,14 @@ Clause* Solver::propagateBin() //uncheckedEnqueue(k->impliedLit, k->clause); uncheckedEnqueueLight(k->impliedLit); } else if (val == l_False) { - return k->clause; - } - } - } - - return NULL; -} - -Clause* Solver::propagateBinNoLearnts() -{ - while (qhead < trail.size()) { - Lit p = trail[qhead++]; - vec & wbin = binwatches[p.toInt()]; - propagations += wbin.size()/2; - for(WatchedBin *k = wbin.getData(), *end = wbin.getDataEnd(); k != end; k++) { - if (k->clause->learnt()) continue; - lbool val = value(k->impliedLit); - if (val.isUndef()) { - //uncheckedEnqueue(k->impliedLit, k->clause); - uncheckedEnqueueLight(k->impliedLit); - } else if (val == l_False) { - return k->clause; - } - } - } - - return NULL; -} - -template -Clause* Solver::propagateBinExcept(const Lit& exceptLit) -{ - while (qhead < trail.size()) { - Lit p = trail[qhead++]; - vec & wbin = binwatches[p.toInt()]; - propagations += wbin.size()/2; - for(WatchedBin *k = wbin.getData(), *end = wbin.getDataEnd(); k != end; k++) { - if (!dontCareLearnt && k->clause->learnt()) continue; - lbool val = value(k->impliedLit); - if (val.isUndef() && k->impliedLit != exceptLit) { - //uncheckedEnqueue(k->impliedLit, k->clause); - uncheckedEnqueueLight(k->impliedLit); - } else if (val == l_False) { - return k->clause; + return PropagatedFrom(p); } } } - - return NULL; -} - -template Clause* Solver::propagateBinExcept (const Lit& exceptLit); -template Clause* Solver::propagateBinExcept (const Lit& exceptLit); -template -Clause* Solver::propagateBinOneLevel() -{ - Lit p = trail[qhead]; - vec & wbin = binwatches[p.toInt()]; - propagations += wbin.size()/2; - for(WatchedBin *k = wbin.getData(), *end = wbin.getDataEnd(); k != end; k++) { - if (!dontCareLearnt && k->clause->learnt()) continue; - lbool val = value(k->impliedLit); - if (val.isUndef()) { - //uncheckedEnqueue(k->impliedLit, k->clause); - uncheckedEnqueueLight(k->impliedLit); - } else if (val == l_False) { - return k->clause; - } - } - - return NULL; + return PropagatedFrom(); } -template Clause* Solver::propagateBinOneLevel (); -template Clause* Solver::propagateBinOneLevel (); - template inline const uint32_t Solver::calcNBLevels(const T& ps) { @@ -1341,20 +1199,22 @@ inline const uint32_t Solver::calcNBLevels(const T& ps) return nbLevels; } -Clause* Solver::propagate_xors(const Lit& p) +PropagatedFrom Solver::propagate_xors(const Lit& p) { #ifdef VERBOSE_DEBUG_XOR cout << "Xor-Propagating variable " << p.var()+1 << endl; #endif - Clause* confl = NULL; + PropagatedFrom confl; - vec& ws = xorwatches[p.var()]; - XorClausePtr *i, *j, *end; + vec& ws = xorwatches[p.var()]; + ClauseOffset *i, *j, *end; for (i = j = ws.getData(), end = i + ws.size(); i != end;) { - XorClause& c = **i++; + XorClause& c = *(XorClause*)clauseAllocator.getPointer(*i); + ClauseOffset origClauseOffset = *i; + i++; if (i != end) - __builtin_prefetch(*i, 1, 0); + __builtin_prefetch(clauseAllocator.getPointer(*i), 1, 0); // Make sure the false literal is data[1]: if (c[0].var() == p.var()) { @@ -1379,7 +1239,7 @@ Clause* Solver::propagate_xors(const Lit& p) #ifdef VERBOSE_DEBUG_XOR cout << "new watch set" << endl << endl; #endif - xorwatches[c[1].var()].push(&c); + xorwatches[c[1].var()].push(origClauseOffset); goto FoundWatch; } @@ -1390,7 +1250,7 @@ Clause* Solver::propagate_xors(const Lit& p) { // Did not find watch -- clause is unit under assignment: - *j++ = &c; + *j++ = origClauseOffset; #ifdef VERBOSE_DEBUG_XOR cout << "final: " << std::boolalpha << final << " - "; @@ -1416,7 +1276,7 @@ Clause* Solver::propagate_xors(const Lit& p) cout << endl << endl; #endif - confl = (Clause*)&c; + confl = PropagatedFrom((Clause*)&c); qhead = trail.size(); // Copy the remaining watches: while (i < end) @@ -1499,12 +1359,7 @@ void Solver::reduceDB() //NOTE: The next instruciton only works if removeNum < learnts.size() (strictly smaller!!) __builtin_prefetch(learnts[i+1], 0, 0); if (learnts[i]->size() > 2 && !locked(*learnts[i]) && learnts[i]->activity() > 2) { - if (readdOldLearnts) { - detachClause(*learnts[i]); - removedLearnts.push(learnts[i]); - } else { - removeClause(*learnts[i]); - } + removeClause(*learnts[i]); } else learnts[j++] = learnts[i]; } @@ -1512,6 +1367,8 @@ void Solver::reduceDB() learnts[j++] = learnts[i]; } learnts.shrink(i - j); + + clauseAllocator.consolidate(this); } const vec& Solver::get_learnts() const @@ -1559,36 +1416,36 @@ void Solver::dumpSortedLearnts(const char* file, const uint32_t maxSize) #endif //STATS_NEEDED } - fprintf(outfile, "c conflicts %lu\n", conflicts); + fprintf(outfile, "c conflicts %lu\n", (unsigned long)conflicts); + if (maxSize == 1) goto end; fprintf(outfile, "c \nc ---------------------------------\n"); fprintf(outfile, "c learnt clauses from binaryClauses\n"); fprintf(outfile, "c ---------------------------------\n"); - if (maxSize >= 2) { - for (uint i = 0; i != binaryClauses.size(); i++) { - if (binaryClauses[i]->learnt()) { - binaryClauses[i]->print(outfile); - } + for (uint i = 0; i != binaryClauses.size(); i++) { + if (binaryClauses[i]->learnt()) { + binaryClauses[i]->print(outfile); } } fprintf(outfile, "c \nc ---------------------------------------\n"); fprintf(outfile, "c clauses representing 2-long XOR clauses\n"); fprintf(outfile, "c ---------------------------------------\n"); - const vector& table = varReplacer->getReplaceTable(); - for (Var var = 0; var != table.size(); var++) { - Lit lit = table[var]; - if (lit.var() == var) - continue; - - fprintf(outfile, "%s%d %d 0\n", (!lit.sign() ? "-" : ""), lit.var()+1, var+1); - fprintf(outfile, "%s%d -%d 0\n", (lit.sign() ? "-" : ""), lit.var()+1, var+1); - #ifdef STATS_NEEDED - if (dynamic_behaviour_analysis) - fprintf(outfile, "c name of two vars that are anti/equivalent: '%s' and '%s'\n", logger.get_var_name(lit.var()).c_str(), logger.get_var_name(var).c_str()); - #endif //STATS_NEEDED - } + { + const vector& table = varReplacer->getReplaceTable(); + for (Var var = 0; var != table.size(); var++) { + Lit lit = table[var]; + if (lit.var() == var) + continue; + fprintf(outfile, "%s%d %d 0\n", (!lit.sign() ? "-" : ""), lit.var()+1, var+1); + fprintf(outfile, "%s%d -%d 0\n", (lit.sign() ? "-" : ""), lit.var()+1, var+1); + #ifdef STATS_NEEDED + if (dynamic_behaviour_analysis) + fprintf(outfile, "c name of two vars that are anti/equivalent: '%s' and '%s'\n", logger.get_var_name(lit.var()).c_str(), logger.get_var_name(var).c_str()); + #endif //STATS_NEEDED + } + } fprintf(outfile, "c \nc --------------------n"); fprintf(outfile, "c clauses from learnts\n"); fprintf(outfile, "c --------------------n"); @@ -1601,6 +1458,8 @@ void Solver::dumpSortedLearnts(const char* file, const uint32_t maxSize) learnts[i]->print(outfile); } } + + end: fclose(outfile); } @@ -1660,7 +1519,7 @@ const bool Solver::simplify() testAllClauseAttach(); assert(decisionLevel() == 0); - if (!ok || propagate() != NULL) { + if (!ok || !propagate().isNULL()) { ok = false; return false; } @@ -1762,9 +1621,9 @@ lbool Solver::search(int nof_conflicts, int nof_conflicts_fullrestart, const boo testAllClauseAttach(); findAllAttach(); for (;;) { - Clause* confl = propagate(update); + PropagatedFrom confl = propagate(update); - if (confl != NULL) { + if (!confl.isNULL()) { ret = handle_conflict(learnt_clause, confl, conflictC, update); if (ret != l_Nothing) return ret; } else { @@ -1881,7 +1740,7 @@ llbool Solver::new_decision(const int& nof_conflicts, const int& nof_conflicts_f return l_Nothing; } -llbool Solver::handle_conflict(vec& learnt_clause, Clause* confl, int& conflictC, const bool update) +llbool Solver::handle_conflict(vec& learnt_clause, PropagatedFrom confl, int& conflictC, const bool update) { #ifdef VERBOSE_DEBUG cout << "Handling conflict: "; @@ -1948,7 +1807,7 @@ llbool Solver::handle_conflict(vec& learnt_clause, Clause* confl, int& conf } c->setStrenghtened(); } else { - c = Clause_new(learnt_clause, learnt_clause_group++, true); + c = clauseAllocator.Clause_new(learnt_clause, learnt_clause_group++, true); #ifdef STATS_NEEDED if (dynamic_behaviour_analysis) logger.set_group_name(c->getGroup(), "learnt clause"); @@ -2120,19 +1979,31 @@ const lbool Solver::simplifyProblem(const uint32_t numConfls) } testAllClauseAttach(); - if (regularRemoveUselessBins - && !failedVarSearcher->removeUslessBinFull()) { - status = l_False; - goto end; + if (performReplace && (regularRemoveUselessBins || regularSubsumeWithNonExistBinaries)) { + OnlyNonLearntBins onlyNonLearntBins(*this); + if (!onlyNonLearntBins.fill()) { + status = l_False; + goto end; + } + if (regularRemoveUselessBins) { + UselessBinRemover uselessBinRemover(*this, onlyNonLearntBins); + if (!uselessBinRemover.removeUslessBinFull()) { + status = l_False; + goto end; + } + } + if (regularSubsumeWithNonExistBinaries + && !subsumer->subsumeWithBinaries(&onlyNonLearntBins)) { + status = l_False; + goto end; + } } - if (regularSubsumeWithNonExistBinaries - && !subsumer->subsumeWithBinaries(false)) { + if (doSubsumption && !subsumer->simplifyBySubsumption(false)) { status = l_False; goto end; } - - if (doSubsumption && !subsumer->simplifyBySubsumption()) { + if (doSubsumption && !subsumer->simplifyBySubsumption(true)) { status = l_False; goto end; } @@ -2205,33 +2076,46 @@ inline void Solver::performStepsBeforeSolve() if (performReplace && !varReplacer->performReplace()) return; - if (conflicts == 0 && learnts.size() == 0 - && noLearntBinaries()) { - if (subsumeWithNonExistBinaries && !subsumer->subsumeWithBinaries(true)) return; - if (removeUselessBins && !failedVarSearcher->removeUslessBinFull()) return; + if (doSubsumption && !subsumer->simplifyBySubsumption(true)) { + return; } - - testAllClauseAttach(); + + if (performReplace) { + OnlyNonLearntBins onlyNonLearntBins(*this); + if (!onlyNonLearntBins.fill()) return; + if (regularRemoveUselessBins) { + UselessBinRemover uselessBinRemover(*this, onlyNonLearntBins); + if (!uselessBinRemover.removeUslessBinFull()) return; + } + if (subsumeWithNonExistBinaries + && !subsumer->subsumeWithBinaries(&onlyNonLearntBins)) return; + } + if (doSubsumption && !libraryUsage && clauses.size() + binaryClauses.size() + learnts.size() < 4800000 && !subsumer->simplifyBySubsumption()) return; + /* if (conflicts == 0 && learnts.size() == 0 && noLearntBinaries()) { if (subsumeWithNonExistBinaries && !subsumer->subsumeWithBinaries(true)) return; - if (removeUselessBins && !failedVarSearcher->removeUslessBinFull()) return; + OnlyNonLearntBins onlyNonLearntBins(*this); + if (!onlyNonLearntBins.fill()) return; + if (regularRemoveUselessBins) { + UselessBinRemover uselessBinRemover(*this, onlyNonLearntBins); + if (!uselessBinRemover.removeUslessBinFull()) return; + } } - - testAllClauseAttach(); + */ + if (findBinaryXors && binaryClauses.size() < MAX_CLAUSENUM_XORFIND) { XorFinder xorFinder(*this, binaryClauses, ClauseCleaner::binaryClauses); if (!xorFinder.doNoPart(2, 2)) return; if (performReplace && !varReplacer->performReplace(true)) return; } - - testAllClauseAttach(); + if (findNormalXors && clauses.size() < MAX_CLAUSENUM_XORFIND) { XorFinder xorFinder(*this, clauses, ClauseCleaner::clauses); if (!xorFinder.doNoPart(3, 7)) return; @@ -2374,9 +2258,7 @@ lbool Solver::solve(const vec& assumps) #endif if (subsumer->getNumElimed() || xorSubsumer->getNumElimed()) { -#ifdef VERBOSE_DEBUG - std::cout << "Solution needs extension. Extending." << std::endl; -#endif //VERBOSE_DEBUG + std::cout << "c Solution needs extension. Extending." << std::endl; Solver s; s.doSubsumption = false; s.performReplace = false; @@ -2384,6 +2266,10 @@ lbool Solver::solve(const vec& assumps) s.findNormalXors = false; s.failedVarSearch = false; s.conglomerateXors = false; + s.subsumeWithNonExistBinaries = false; + s.regularSubsumeWithNonExistBinaries = false; + s.removeUselessBins = false; + s.regularRemoveUselessBins = false; s.greedyUnbound = greedyUnbound; for (Var var = 0; var < nVars(); var++) { s.newVar(decision_var[var] || subsumer->getVarElimed()[var] || varReplacer->varHasBeenReplaced(var) || xorSubsumer->getVarElimed()[var]); @@ -2412,7 +2298,7 @@ lbool Solver::solve(const vec& assumps) for (Var var = 0; var < nVars(); var++) { if (assigns[var] == l_Undef && s.model[var] != l_Undef) uncheckedEnqueue(Lit(var, s.model[var] == l_False)); } - ok = (propagate() == NULL); + ok = (propagate().isNULL()); if (!ok) { printf("c ERROR! Extension of model failed!\n"); assert(ok); @@ -2579,16 +2465,17 @@ void Solver::printEndSearchStat() { #ifdef STATS_NEEDED if (verbosity >= 1 && !(dynamic_behaviour_analysis && logger.statistics_on)) { - #else - if (verbosity >= 1) { - #endif - printf("c ===================================================================="); - #ifdef USE_GAUSS - print_gauss_sum_stats(); - #else //USE_GAUSS - printf("\n"); - #endif //USE_GAUSS - } + #else + if (verbosity >= 1) { + #endif //STATS_NEEDED + printf("c ===================================================================="); + #ifdef USE_GAUSS + print_gauss_sum_stats(); + if (verbosity == 1) printf("=====================\n"); + #else //USE_GAUSS + printf("\n"); + #endif //USE_GAUSS + } } #ifdef DEBUG_ATTACH diff --git a/src/sat/cryptominisat2/Solver.h b/src/sat/cryptominisat2/Solver.h index 5f477ab..75daea6 100644 --- a/src/sat/cryptominisat2/Solver.h +++ b/src/sat/cryptominisat2/Solver.h @@ -60,6 +60,7 @@ class XorSubsumer; class PartHandler; class RestartTypeChooser; class StateSaver; +class UselessBinRemover; #ifdef VERBOSE_DEBUG #define DEBUG_UNCHECKEDENQUEUE_LEVEL0 @@ -80,6 +81,91 @@ struct reduceDB_ltGlucose bool operator () (const Clause* x, const Clause* y); }; +//#define DEBUG_PROPAGATEFROM + +class PropagatedFrom +{ + private: + union {Clause* clause; uint32_t otherLit;}; + + public: + PropagatedFrom(Clause* c) + { + #ifdef DEBUG_PROPAGATEFROM + assert(c != NULL); + #endif + clause = c; + } + + PropagatedFrom(const Lit& _other) + { + otherLit = _other.toInt() << 1; + otherLit |= 1; + } + + PropagatedFrom() : + clause(NULL) + { + } + + const bool isBinary() const + { + return (otherLit&1); + } + + const Lit getOtherLit() const + { + #ifdef DEBUG_PROPAGATEFROM + assert(isBinary()); + #endif + return Lit::toLit(otherLit>>1); + } + + const Clause* getClause() const + { + #ifdef DEBUG_PROPAGATEFROM + assert(!isBinary()); + #endif + return clause; + } + + Clause* getClause() + { + return clause; + } + + const bool isNULL() const + { + if (isBinary()) return false; + return clause == NULL; + } + + const uint32_t size() const + { + if (isBinary()) return 2; + + #ifdef DEBUG_PROPAGATEFROM + assert(!isNULL()); + #endif + + return getClause()->size(); + } + + const Lit operator[](uint32_t i) const + { + if (isBinary()) { + #ifdef DEBUG_PROPAGATEFROM + assert(i == 1); + #endif + return getOtherLit(); + } + + #ifdef DEBUG_PROPAGATEFROM + assert(!isNULL()); + #endif + return (*getClause())[i]; + } +}; class Solver { @@ -155,7 +241,6 @@ public: bool doVarElim; // Perform variable elimination bool doSubsume1; // Perform clause contraction through resolution bool failedVarSearch; // Should search for failed vars and doulbly propagated vars - bool readdOldLearnts; // Should re-add old learnts for failed variable searching bool addExtraBins; // Should add extra binaries in failed literal probing bool removeUselessBins; // Should try to remove useless binary clauses bool regularRemoveUselessBins; // Should try to remove useless binary clauses regularly @@ -224,13 +309,15 @@ protected: template bool addLearntClause(T& ps, const uint group, const uint32_t activity); template - void removeWatchedCl(vec &ws, const Clause *c); + void removeWatchedCl(vec &ws, const ClauseOffset c); template - bool findWatchedCl(const vec& ws, const Clause *c) const; + bool findWatchedCl(const vec& ws, const ClauseOffset c) const; template - void removeWatchedBinCl(vec &ws, const Clause *c); + void removeWatchedBinCl(vec &ws, const Lit impliedLit); template - bool findWatchedBinCl(const vec& ws, const Clause *c) const; + void removeWatchedBinClAll(vec &ws, const Lit impliedLit); + template + bool findWatchedBinCl(const vec& ws, const Lit impliedLit) const; // Helper structures: // @@ -254,17 +341,17 @@ protected: // Solver state: // bool ok; // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used! + ClauseAllocator clauseAllocator; vec clauses; // List of problem clauses. vec binaryClauses; // Binary clauses are regularly moved here vec xorclauses; // List of problem xor-clauses. Will be freed vec learnts; // List of learnt clauses. - vec removedLearnts; // Clauses that have been learnt, then removed vec freeLater; // xor clauses that need to be freed later due to Gauss vec activity; // A heuristic measurement of the activity of a variable. uint32_t var_inc; // Amount to bump next variable with. double cla_inc; // Amount to bump learnt clause oldActivity with vec > watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). - vec > xorwatches; // 'xorwatches[var]' is a list of constraints watching var in XOR clauses. + vec > xorwatches; // 'xorwatches[var]' is a list of constraints watching var in XOR clauses. vec > binwatches; vec assigns; // The current assignments vector polarity; // The preferred polarity of each variable. @@ -274,12 +361,13 @@ protected: vector decision_var; // Declares if a variable is eligible for selection in the decision heuristic. vec trail; // Assignment stack; stores all assigments made in the order they were made. vec trail_lim; // Separator indices for different decision levels in 'trail'. - vec reason; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none. + vec reason; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none. vec level; // 'level[var]' contains the level at which the assignment was made. uint64_t curRestart; uint32_t nbclausesbeforereduce; uint32_t nbCompensateSubsumer; // Number of learnt clauses that subsumed normal clauses last time subs. was executed uint32_t qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat). + Lit failBinLit; uint32_t simpDB_assigns; // Number of top-level assignments since last execution of 'simplify()'. int64_t simpDB_props; // Remaining number of propagations that must be made before next execution of 'simplify()'. vec assumptions; // Current set of assumptions provided to solve by the user. @@ -330,25 +418,24 @@ protected: void insertVarOrder (Var x); // Insert a variable in the decision order priority queue. Lit pickBranchLit (); // Return the next decision variable. void newDecisionLevel (); // Begins a new decision level. - void uncheckedEnqueue (Lit p, ClausePtr from = (Clause*)NULL); // Enqueue a literal. Assumes value of literal is undefined. + void uncheckedEnqueue (const Lit p, const PropagatedFrom& from = PropagatedFrom()); // Enqueue a literal. Assumes value of literal is undefined. void uncheckedEnqueueLight (const Lit p); - bool enqueue (Lit p, Clause* from = NULL); // Test if fact 'p' contradicts current state, enqueue otherwise. - Clause* propagate (const bool update = true); // Perform unit propagation. Returns possibly conflicting clause. - Clause* propagateLight(); - Clause* propagateBin(); - Clause* propagateBinNoLearnts(); + bool enqueue (Lit p, PropagatedFrom from = PropagatedFrom()); // Test if fact 'p' contradicts current state, enqueue otherwise. + PropagatedFrom propagate (const bool update = true); // Perform unit propagation. Returns possibly conflicting clause. + PropagatedFrom propagateBin(); + PropagatedFrom propagateBinNoLearnts(); template - Clause* propagateBinExcept(const Lit& exceptLit); + PropagatedFrom propagateBinExcept(const Lit& exceptLit); template - Clause* propagateBinOneLevel(); - Clause* propagate_xors (const Lit& p); + PropagatedFrom propagateBinOneLevel(); + PropagatedFrom propagate_xors (const Lit& p); void cancelUntil (int level); // Backtrack until a certain level. - Clause* analyze (Clause* confl, vec& out_learnt, int& out_btlevel, uint32_t &nblevels, const bool update); // (bt = backtrack) + Clause* analyze (PropagatedFrom confl, vec& out_learnt, int& out_btlevel, uint32_t &nblevels, const bool update); // (bt = backtrack) void analyzeFinal (Lit p, vec& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION? bool litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()') lbool search (int nof_conflicts, int nof_conflicts_fullrestart, const bool update = true); // Search for a given number of conflicts. void reduceDB (); // Reduce the set of learnt clauses. - llbool handle_conflict (vec& learnt_clause, Clause* confl, int& conflictC, const bool update);// Handles the conflict clause + llbool handle_conflict (vec& learnt_clause, PropagatedFrom confl, int& conflictC, const bool update);// Handles the conflict clause llbool new_decision (const int& nof_conflicts, const int& nof_conflicts_fullrestart, int& conflictC); // Handles the case when all propagations have been made, and now a decision must be made // Maintaining Variable/Clause activity: @@ -369,7 +456,7 @@ protected: template void removeClause(T& c); // Detach and free a clause. bool locked (const Clause& c) const; // Returns TRUE if a clause is a reason for some implication in the current state. - void reverse_binary_clause(Clause& c) const; // Binary clauses --- the first Lit has to be true + //void reverse_binary_clause(Clause& c) const; // Binary clauses --- the first Lit has to be true void testAllClauseAttach() const; void findAllAttach() const; const bool findClause(XorClause* c) const; @@ -393,6 +480,9 @@ protected: friend class XorSubsumer; friend class PartHandler; friend class StateSaver; + friend class UselessBinRemover; + friend class OnlyNonLearntBins; + friend class ClauseAllocator; Conglomerate* conglomerate; VarReplacer* varReplacer; ClauseCleaner* clauseCleaner; @@ -485,13 +575,15 @@ inline void Solver::claDecayActivity() //cla_inc *= clause_decay; } -inline bool Solver::enqueue (Lit p, Clause* from) +inline bool Solver::enqueue (Lit p, PropagatedFrom from) { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); } inline bool Solver::locked (const Clause& c) const { - return reason[c[0].var()] == &c && value(c[0]) == l_True; + if (c.size() == 2) return true; //we don't know in this case :I + PropagatedFrom from(reason[c[0].var()]); + return !from.isBinary() && from.getClause() == &c && value(c[0]) == l_True; } inline void Solver::newDecisionLevel() { @@ -621,7 +713,7 @@ inline const uint Solver::get_unitary_learnts_num() const return trail.size(); } template -inline void Solver::removeWatchedCl(vec &ws, const Clause *c) { +inline void Solver::removeWatchedCl(vec &ws, const ClauseOffset c) { uint32_t j = 0; for (; j < ws.size() && ws[j].clause != c; j++); assert(j < ws.size()); @@ -629,33 +721,47 @@ inline void Solver::removeWatchedCl(vec &ws, const Clause *c) { ws.pop(); } template -inline void Solver::removeWatchedBinCl(vec &ws, const Clause *c) { +inline void Solver::removeWatchedBinCl(vec &ws, const Lit impliedLit) { uint32_t j = 0; - for (; j < ws.size() && ws[j].clause != c; j++); + for (; j < ws.size() && ws[j].impliedLit != impliedLit; j++); assert(j < ws.size()); for (; j < ws.size()-1; j++) ws[j] = ws[j+1]; ws.pop(); } +template +inline void Solver::removeWatchedBinClAll(vec &ws, const Lit impliedLit) { + T *i = ws.getData(); + T *j = i; + for (T* end = ws.getDataEnd(); i != end; i++) { + if (i->impliedLit != impliedLit) + *j++ = *i; + } + ws.shrink(i-j); +} template -inline bool Solver::findWatchedCl(const vec& ws, const Clause *c) const +inline bool Solver::findWatchedCl(const vec& ws, const ClauseOffset c) const { uint32_t j = 0; for (; j < ws.size() && ws[j].clause != c; j++); return j < ws.size(); } template -inline bool Solver::findWatchedBinCl(const vec& ws, const Clause *c) const +inline bool Solver::findWatchedBinCl(const vec& ws, const Lit impliedLit) const { uint32_t j = 0; - for (; j < ws.size() && ws[j].clause != c; j++); + for (; j < ws.size() && ws[j].impliedLit != impliedLit; j++); return j < ws.size(); } + +/* inline void Solver::reverse_binary_clause(Clause& c) const { if (c.size() == 2 && value(c[0]) == l_False) { assert(value(c[1]) == l_True); std::swap(c[0], c[1]); } } +*/ + /*inline void Solver::calculate_xor_clause(Clause& c2) const { if (c2.isXor() && ((XorClause*)&c2)->updateNeeded()) { XorClause& c = *((XorClause*)&c2); @@ -678,7 +784,7 @@ template inline void Solver::removeClause(T& c) { detachClause(c); - clauseFree(&c); + clauseAllocator.clauseFree(&c); } //================================================================================================= diff --git a/src/sat/cryptominisat2/SolverTypes.h b/src/sat/cryptominisat2/SolverTypes.h index 452097c..6f38ed5 100644 --- a/src/sat/cryptominisat2/SolverTypes.h +++ b/src/sat/cryptominisat2/SolverTypes.h @@ -94,6 +94,10 @@ public: { fprintf(outfile,"%s%d 0\n", sign() ? "-" : "", var()+1); } + static Lit toLit(uint32_t data) + { + return Lit(data); + } }; const Lit lit_Undef(var_Undef, false); // Useful special constants. diff --git a/src/sat/cryptominisat2/Subsumer.cpp b/src/sat/cryptominisat2/Subsumer.cpp index f6cda31..d2b3f0c 100644 --- a/src/sat/cryptominisat2/Subsumer.cpp +++ b/src/sat/cryptominisat2/Subsumer.cpp @@ -13,6 +13,7 @@ Substantially modified by: Mate Soos (2010) #include #include "VarReplacer.h" #include "XorFinder.h" +#include "OnlyNonLearntBins.h" #ifdef _MSC_VER #define __builtin_prefetch(a,b,c) @@ -24,8 +25,6 @@ Substantially modified by: Mate Soos (2010) #endif //#define BIT_MORE_VERBOSITY -//#define HYPER_DEBUG -//#define HYPER_DEBUG2 //#define TOUCH_LESS #ifdef VERBOSE_DEBUG @@ -104,7 +103,7 @@ const bool Subsumer::unEliminate(const Var var) solver.libraryCNFFile = NULL; for (vector::iterator it2 = it->second.begin(), end2 = it->second.end(); it2 != end2; it2++) { solver.addClause(**it2); - clauseFree(*it2); + solver.clauseAllocator.clauseFree(*it2); } solver.libraryCNFFile = backup_libraryCNFfile; elimedOutVar.erase(it); @@ -170,6 +169,7 @@ inline uint32_t Subsumer::subsume0(T& ps, uint32_t abs) template uint32_t Subsumer::subsume0Orig(const T& ps, uint32_t abs) { + subsumedNonLearnt = false; uint32_t retIndex = std::numeric_limits::max(); vec subs; findSubsumed(ps, abs, subs); @@ -181,9 +181,10 @@ uint32_t Subsumer::subsume0Orig(const T& ps, uint32_t abs) #endif Clause* tmp = subs[i].clause; + subsumedNonLearnt |= !tmp->learnt(); retIndex = subs[i].index; unlinkClause(subs[i]); - clauseFree(tmp); + solver.clauseAllocator.clauseFree(tmp); } return retIndex; @@ -229,7 +230,7 @@ void Subsumer::subsume0BIN(const Lit lit1, const vec& lits) Clause* tmp = subs[i].clause; unlinkClause(subs[i]); - clauseFree(tmp); + solver.clauseAllocator.clauseFree(tmp); } if (subs2.size() == 0) return; @@ -256,7 +257,7 @@ void Subsumer::subsume0BIN(const Lit lit1, const vec& lits) #ifdef VERBOSE_DEBUG std::cout << "--> Clause was satisfied." << std::endl; #endif - clauseFree(&cl); + solver.clauseAllocator.clauseFree(&cl); goto endS; } } @@ -271,17 +272,17 @@ void Subsumer::subsume0BIN(const Lit lit1, const vec& lits) if (cl.size() == 0) { solver.ok = false; unregisterIteration(subs2); - clauseFree(&cl); + solver.clauseAllocator.clauseFree(&cl); return; } if (cl.size() > 2) { - cl.calcAbstraction(); + cl.calcAbstractionClause(); linkInAlreadyClause(c); clauses[c.index] = c; solver.attachClause(cl); updateClause(c); } else if (cl.size() == 2) { - cl.calcAbstraction(); + cl.calcAbstractionClause(); solver.attachClause(cl); solver.becameBinary++; addBinaryClauses.push(&cl); @@ -289,7 +290,7 @@ void Subsumer::subsume0BIN(const Lit lit1, const vec& lits) } else { assert(cl.size() == 1); solver.uncheckedEnqueue(cl[0]); - solver.ok = (solver.propagate() == NULL); + solver.ok = (solver.propagate().isNULL()); if (!solver.ok) { unregisterIteration(subs2); return; @@ -297,7 +298,7 @@ void Subsumer::subsume0BIN(const Lit lit1, const vec& lits) #ifdef VERBOSE_DEBUG cout << "--> Found that var " << cl[0].var()+1 << " must be " << std::boolalpha << !cl[0].sign() << endl; #endif - clauseFree(&cl); + solver.clauseAllocator.clauseFree(&cl); } endS:; } @@ -345,7 +346,7 @@ void Subsumer::unlinkClause(ClauseSimp c, Var elim) clauses[c.index].clause = NULL; } -void Subsumer::unlinkModifiedClause(vec& origClause, ClauseSimp c) +void Subsumer::unlinkModifiedClause(vec& origClause, ClauseSimp c, bool detachAndNull) { for (uint32_t i = 0; i < origClause.size(); i++) { maybeRemove(occur[origClause[i].toInt()], c.clause); @@ -354,8 +355,6 @@ void Subsumer::unlinkModifiedClause(vec& origClause, ClauseSimp c) #endif } - solver.detachModifiedClause(origClause[0], origClause[1], origClause.size(), c.clause); - // Remove from iterator vectors/sets: for (uint32_t i = 0; i < iter_vecs.size(); i++){ vec& cs = *iter_vecs[i]; @@ -371,34 +370,11 @@ void Subsumer::unlinkModifiedClause(vec& origClause, ClauseSimp c) // Remove clause from clause touched set: cl_touched.exclude(c); cl_added.exclude(c); - - clauses[c.index].clause = NULL; -} -void Subsumer::unlinkModifiedClauseNoDetachNoNULL(vec& origClause, ClauseSimp c) -{ - for (uint32_t i = 0; i < origClause.size(); i++) { - maybeRemove(occur[origClause[i].toInt()], c.clause); - #ifndef TOUCH_LESS - touch(origClause[i]); - #endif + if (detachAndNull) { + solver.detachModifiedClause(origClause[0], origClause[1], origClause.size(), c.clause); + clauses[c.index].clause = NULL; } - - // Remove from iterator vectors/sets: - for (uint32_t i = 0; i < iter_vecs.size(); i++){ - vec& cs = *iter_vecs[i]; - for (uint32_t j = 0; j < cs.size(); j++) - if (cs[j].clause == c.clause) - cs[j].clause = NULL; - } - for (uint32_t i = 0; i < iter_sets.size(); i++){ - CSet& cs = *iter_sets[i]; - cs.exclude(c); - } - - // Remove clause from clause touched set: - cl_touched.exclude(c); - cl_added.exclude(c); } void Subsumer::subsume1(ClauseSimp& ps) @@ -462,7 +438,7 @@ void Subsumer::subsume1(ClauseSimp& ps) #ifdef VERBOSE_DEBUG std::cout << "--> Clause was satisfied." << std::endl; #endif - clauseFree(&cl); + solver.clauseAllocator.clauseFree(&cl); goto endS; } } @@ -478,11 +454,11 @@ void Subsumer::subsume1(ClauseSimp& ps) solver.ok = false; unregisterIteration(Q); unregisterIteration(subs); - clauseFree(&cl); + solver.clauseAllocator.clauseFree(&cl); return; } if (cl.size() > 1) { - cl.calcAbstraction(); + cl.calcAbstractionClause(); linkInAlreadyClause(c); clauses[c.index] = c; solver.attachClause(cl); @@ -492,7 +468,7 @@ void Subsumer::subsume1(ClauseSimp& ps) } else { assert(cl.size() == 1); solver.uncheckedEnqueue(cl[0]); - solver.ok = (solver.propagate() == NULL); + solver.ok = (solver.propagate().isNULL()); if (!solver.ok) { unregisterIteration(Q); unregisterIteration(subs); @@ -501,7 +477,7 @@ void Subsumer::subsume1(ClauseSimp& ps) #ifdef VERBOSE_DEBUG cout << "--> Found that var " << cl[0].var()+1 << " must be " << std::boolalpha << !cl[0].sign() << endl; #endif - clauseFree(&cl); + solver.clauseAllocator.clauseFree(&cl); } endS:; } @@ -561,7 +537,7 @@ void Subsumer::subsume1Partial(const T& ps) #ifdef VERBOSE_DEBUG std::cout << "--> Clause was satisfied." << std::endl; #endif - clauseFree(&cl); + solver.clauseAllocator.clauseFree(&cl); goto endS; } } @@ -576,17 +552,17 @@ void Subsumer::subsume1Partial(const T& ps) if (cl.size() == 0) { solver.ok = false; unregisterIteration(subsume1PartialSubs); - clauseFree(&cl); + solver.clauseAllocator.clauseFree(&cl); return; } if (cl.size() > 2) { - cl.calcAbstraction(); + cl.calcAbstractionClause(); linkInAlreadyClause(c); clauses[c.index] = c; solver.attachClause(cl); updateClause(c); } else if (cl.size() == 2) { - cl.calcAbstraction(); + cl.calcAbstractionClause(); solver.attachClause(cl); solver.becameBinary++; addBinaryClauses.push(&cl); @@ -594,7 +570,7 @@ void Subsumer::subsume1Partial(const T& ps) } else { assert(cl.size() == 1); solver.uncheckedEnqueue(cl[0]); - solver.ok = (solver.propagate() == NULL); + solver.ok = (solver.propagate().isNULL()); if (!solver.ok) { unregisterIteration(subsume1PartialSubs); return; @@ -602,7 +578,7 @@ void Subsumer::subsume1Partial(const T& ps) #ifdef VERBOSE_DEBUG cout << "--> Found that var " << cl[0].var()+1 << " must be " << std::boolalpha << !cl[0].sign() << endl; #endif - clauseFree(&cl); + solver.clauseAllocator.clauseFree(&cl); } endS:; } @@ -615,7 +591,9 @@ void Subsumer::subsume1Partial(const T& ps) void Subsumer::updateClause(ClauseSimp c) { - if (!c.clause->learnt()) subsume0(*c.clause, c.clause->getAbst()); + subsume0(*c.clause, c.clause->getAbst()); + if (c.clause->learnt() && subsumedNonLearnt) + c.clause->makeNonLearnt(); cl_touched.add(c); } @@ -639,7 +617,7 @@ void Subsumer::almost_all_database() } assert(solver.ok); - solver.ok = (solver.propagate() == NULL); + solver.ok = (solver.propagate().isNULL()); if (!solver.ok) { std::cout << "c (contradiction during subsumption)" << std::endl; return; @@ -673,7 +651,7 @@ void Subsumer::almost_all_database() s1.clear(); if (!solver.ok) return; - solver.ok = (solver.propagate() == NULL); + solver.ok = (solver.propagate().isNULL()); if (!solver.ok) { printf("c (contradiction during subsumption)\n"); unregisterIteration(s1); @@ -760,7 +738,7 @@ void Subsumer::smaller_database() s1.clear(); if (!solver.ok) return; - solver.ok = (solver.propagate() == NULL); + solver.ok = (solver.propagate().isNULL()); if (!solver.ok){ printf("c (contradiction during subsumption)\n"); unregisterIteration(s1); @@ -773,8 +751,10 @@ void Subsumer::smaller_database() // Iteration pass for 0-subsumption: for (CSet::iterator it = s0.begin(), end = s0.end(); it != end; ++it) { - if (it->clause != NULL) + if (it->clause != NULL) { subsume0(*it->clause, it->clause->getAbst()); + if (subsumedNonLearnt && it->clause->learnt()) it->clause->makeNonLearnt(); + } } s0.clear(); unregisterIteration(s0); @@ -836,12 +816,19 @@ void Subsumer::addFromSolver(vec& cs, bool alsoLearnt) else if (cl.getStrenghtened()) cl_touched.add(c); } - if (cl.getVarChanged() || cl.getStrenghtened()) - cl.calcAbstraction(); + if (!cl.learnt() && (cl.getVarChanged() || cl.getStrenghtened())) + cl.calcAbstractionClause(); } cs.shrink(i-j); } +void Subsumer::freeMemory() +{ + for (uint32_t i = 0; i < occur.size(); i++) { + occur[i].clear(true); + } +} + void Subsumer::addBackToSolver() { #ifdef HYPER_DEBUG2 @@ -856,7 +843,16 @@ void Subsumer::addBackToSolver() if (clauses[i].clause->learnt()) binaryLearntAdded++; #endif - solver.binaryClauses.push(clauses[i].clause); + Clause* c = clauses[i].clause; + if (!c->wasBin()) { + solver.detachClause(*c); + Clause *c2 = solver.clauseAllocator.Clause_new(*c); + solver.clauseAllocator.clauseFree(c); + solver.attachClause(*c2); + solver.becameBinary++; + c = c2; + } + solver.binaryClauses.push(c); } else { if (clauses[i].clause->learnt()) solver.learnts.push(clauses[i].clause); @@ -886,7 +882,7 @@ void Subsumer::removeWrong(vec& cs) if (var_elimed[l->var()]) { remove = true; solver.detachClause(c); - clauseFree(&c); + solver.clauseAllocator.clauseFree(&c); break; } } @@ -921,65 +917,7 @@ void Subsumer::fillCannotEliminate() #endif } -void Subsumer::subsume0LearntSet(vec& cs) -{ - Clause** a = cs.getData(); - Clause** b = a; - for (Clause** end = a + cs.size(); a != end; a++) { - if (numMaxSubsume0 > 0 && !(*a)->subsume0IsFinished()) { - numMaxSubsume0--; - uint32_t index = subsume0(**a, calcAbstraction(**a)); - if (index != std::numeric_limits::max()) { - (*a)->makeNonLearnt(); - //solver.nbBin--; - clauses[index].clause = *a; - linkInAlreadyClause(clauses[index]); - solver.learnts_literals -= (*a)->size(); - solver.clauses_literals += (*a)->size(); - cl_added.add(clauses[index]); - continue; - } - if (numMaxSubsume1 > 0 && - (((*a)->size() == 2 && clauses.size() < 3500000) || - ((*a)->size() <= 3 && clauses.size() < 300000) || - ((*a)->size() <= 4 && clauses.size() < 60000))) { - ClauseSimp c(*a, clauseID++); - //(*a)->calcAbstraction(); - //clauses.push(c); - subsume1(c); - numMaxSubsume1--; - if (!solver.ok) { - for (; a != end; a++) - *b++ = *a; - cs.shrink(a-b); - return; - } - //assert(clauses[c.index].clause != NULL); - //clauses.pop(); - clauseID--; - } - } - *b++ = *a; - } - cs.shrink(a-b); -} - -const bool Subsumer::treatLearnts() -{ - subsume0LearntSet(solver.learnts); - if (!solver.ok) return false; - subsume0LearntSet(solver.binaryClauses); - if (!solver.ok) return false; - solver.ok = (solver.propagate() == NULL); - if (!solver.ok){ - printf("c (contradiction during subsumption)\n"); - return false; - } - solver.clauseCleaner->cleanClausesBewareNULL(clauses, ClauseCleaner::simpClauses, *this); - return true; -} - -const bool Subsumer::subsumeWithBinaries(const bool startUp) +const bool Subsumer::subsumeWithBinaries(OnlyNonLearntBins* onlyNonLearntBins) { clearAll(); clauseID = 0; @@ -1002,26 +940,33 @@ const bool Subsumer::subsumeWithBinaries(const bool startUp) } #endif //DEBUG_BINARIES + numMaxSubsume0 = 300000 * (1+numCalls/2); + numMaxSubsume1 = 10000 * (1+numCalls); + for (uint32_t i = 0; i < solver.binaryClauses.size(); i++) { - if (startUp || !solver.binaryClauses[i]->learnt()) { + if (!solver.binaryClauses[i]->learnt() && numMaxSubsume0 > 0) { Clause& c = *solver.binaryClauses[i]; subsume0(c, c.getAbst()); + numMaxSubsume0--; } } for (uint32_t i = 0; i < solver.binaryClauses.size(); i++) { - Clause& c = *solver.binaryClauses[i]; - subsume1Partial(c); - if (!solver.ok) return false; + if (numMaxSubsume1 > 0) { + Clause& c = *solver.binaryClauses[i]; + subsume1Partial(c); + if (!solver.ok) return false; + numMaxSubsume1--; + } } if (solver.verbosity >= 1) { std::cout << "c subs with bin: " << std::setw(8) << clauses_subsumed << " lits-rem: " << std::setw(9) << literals_removed << " v-fix: " << std::setw(4) <= 1) { - std::cout << "c Subs w/ non-existent bins: " << subsNonExistentNum - << " lits-rem: " << subsNonExistentLitsRemoved - << " v-fix: " << subsNonExistentumFailed - << " done: " << doneNum - << " time: " << std::fixed << std::setprecision(2) << std::setw(5) << subsNonExistentTime - << std::endl; + std::cout << "c Subs w/ non-existent bins: " << std::setw(6) << subsNonExistentNum + << " l-rem: " << std::setw(6) << subsNonExistentLitsRemoved + << " v-fix: " << std::setw(5) << subsNonExistentumFailed + << " done: " << std::setw(6) << doneNum + << " time: " << std::fixed << std::setprecision(2) << std::setw(5) << subsNonExistentTime << " s" + << std::setw(2) << " |" << std::endl; } totalTime += cpuTime() - myTime; solver.order_heap.filter(Solver::VarFilter(solver)); @@ -1050,7 +1002,7 @@ const bool Subsumer::subsumeWithBinaries(const bool startUp) #define MAX_BINARY_PROP 40000000 -const bool Subsumer::subsWNonExistBinsFull(const bool startUp) +const bool Subsumer::subsWNonExistBinsFull(OnlyNonLearntBins* onlyNonLearntBins) { uint32_t oldClausesSubusmed = clauses_subsumed; uint32_t oldLitsRemoved = literals_removed; @@ -1058,7 +1010,8 @@ const bool Subsumer::subsWNonExistBinsFull(const bool startUp) uint64_t oldProps = solver.propagations; uint32_t oldTrailSize = solver.trail.size(); uint64_t maxProp = MAX_BINARY_PROP; - if (!startUp) maxProp /= 3; + //if (!startUp) maxProp /= 3; + if (clauses.size() > 2000000) maxProp /= 2; ps2.clear(); ps2.growTo(2); toVisitAll.growTo(solver.nVars()*2, false); @@ -1072,11 +1025,11 @@ const bool Subsumer::subsWNonExistBinsFull(const bool startUp) doneNum++; Lit lit(var, true); - if (!subsWNonExistBins(lit, startUp)) { + if (!subsWNonExistBins(lit, onlyNonLearntBins)) { if (!solver.ok) return false; solver.cancelUntil(0); solver.uncheckedEnqueue(~lit); - solver.ok = (solver.propagate() == NULL); + solver.ok = (solver.propagate().isNULL()); if (!solver.ok) return false; continue; } @@ -1084,11 +1037,11 @@ const bool Subsumer::subsWNonExistBinsFull(const bool startUp) //in the meantime it could have got assigned if (solver.assigns[var] != l_Undef) continue; lit = ~lit; - if (!subsWNonExistBins(lit, startUp)) { + if (!subsWNonExistBins(lit, onlyNonLearntBins)) { if (!solver.ok) return false; solver.cancelUntil(0); solver.uncheckedEnqueue(~lit); - solver.ok = (solver.propagate() == NULL); + solver.ok = (solver.propagate().isNULL()); if (!solver.ok) return false; continue; } @@ -1101,7 +1054,7 @@ const bool Subsumer::subsWNonExistBinsFull(const bool startUp) return true; } -const bool Subsumer::subsWNonExistBins(const Lit& lit, const bool startUp) +const bool Subsumer::subsWNonExistBins(const Lit& lit, OnlyNonLearntBins* onlyNonLearntBins) { #ifdef VERBOSE_DEBUG std::cout << "subsWNonExistBins called with lit "; lit.print(); @@ -1110,12 +1063,7 @@ const bool Subsumer::subsWNonExistBins(const Lit& lit, const bool startUp) toVisit.clear(); solver.newDecisionLevel(); solver.uncheckedEnqueueLight(lit); - bool failed; - if (startUp) { - failed = (solver.propagateBin() != NULL); - } else { - failed = (solver.propagateBinNoLearnts() != NULL); - } + bool failed = !onlyNonLearntBins->propagate(); if (failed) return false; assert(solver.decisionLevel() > 0); @@ -1162,7 +1110,7 @@ void Subsumer::clearAll() cl_touched.clear(); } -const bool Subsumer::simplifyBySubsumption() +const bool Subsumer::simplifyBySubsumption(const bool alsoLearnt) { if (solver.nClauses() > 20000000) return true; @@ -1184,20 +1132,24 @@ const bool Subsumer::simplifyBySubsumption() return false; fillCannotEliminate(); solver.testAllClauseAttach(); - - clauses.reserve(solver.clauses.size() + solver.binaryClauses.size()); - cl_added.reserve(solver.clauses.size() + solver.binaryClauses.size()); - cl_touched.reserve(solver.clauses.size() + solver.binaryClauses.size()); - - if (clauses.size() < 200000) - fullSubsume = true; + + uint32_t expected_size; + if (!alsoLearnt) + expected_size = solver.clauses.size() + solver.binaryClauses.size(); else - fullSubsume = false; + expected_size = solver.clauses.size() + solver.binaryClauses.size() + solver.learnts.size(); + clauses.reserve(expected_size); + cl_added.reserve(expected_size); + cl_touched.reserve(expected_size); + + if (clauses.size() < 200000) fullSubsume = true; + else fullSubsume = false; + if (alsoLearnt) fullSubsume = true; solver.clauseCleaner->cleanClauses(solver.clauses, ClauseCleaner::clauses); - addFromSolver(solver.clauses); + addFromSolver(solver.clauses, alsoLearnt); solver.clauseCleaner->removeSatisfied(solver.binaryClauses, ClauseCleaner::binaryClauses); - addFromSolver(solver.binaryClauses); + addFromSolver(solver.binaryClauses, alsoLearnt); //Limits if (clauses.size() > 3500000) { @@ -1218,15 +1170,20 @@ const bool Subsumer::simplifyBySubsumption() numMaxSubsume1 = 400000 * (1+numCalls/2); numMaxBlockToVisit = (int64_t)(80000.0 * (0.8+(double)(numCalls)/3.0)); } - if (numCalls == 1) numMaxSubsume1 = 0; - - if (!solver.doSubsume1) numMaxSubsume1 = 0; - - if (solver.order_heap.size() > 200000) numMaxBlockVars = (uint32_t)((double)solver.order_heap.size() / 3.5 * (0.8+(double)(numCalls)/4.0)); else numMaxBlockVars = (uint32_t)((double)solver.order_heap.size() / 1.5 * (0.8+(double)(numCalls)/4.0)); + + if (numCalls == 1) numMaxSubsume1 = 0; + if (!solver.doSubsume1) numMaxSubsume1 = 0; + if (alsoLearnt) { + numMaxElim = 0; + numMaxSubsume1 = 0; + numMaxBlockVars = 0; + numMaxBlockToVisit = 0; + fullSubsume = true; + } //For debugging //numMaxBlockToVisit = std::numeric_limits::max(); @@ -1245,16 +1202,15 @@ const bool Subsumer::simplifyBySubsumption() if (clauses[i].clause != NULL && (fullSubsume || !clauses[i].clause->subsume0IsFinished()) - ) { + ) + { subsume0(*clauses[i].clause, clauses[i].clause->getAbst()); + if (subsumedNonLearnt && clauses[i].clause->learnt()) clauses[i].clause->makeNonLearnt(); numMaxSubsume0--; } } origNClauses = clauses.size(); - uint32_t origNLearnts = solver.learnts.size(); - - if (!treatLearnts()) return false; #ifdef BIT_MORE_VERBOSITY std::cout << "c time until pre-subsume0 clauses and subsume1 2-learnts:" << cpuTime()-myTime << std::endl; @@ -1287,7 +1243,7 @@ const bool Subsumer::simplifyBySubsumption() cl_added.clear(); assert(cl_added.size() == 0); assert(solver.ok); - solver.ok = (solver.propagate() == NULL); + solver.ok = (solver.propagate().isNULL()); if (!solver.ok) { printf("c (contradiction during subsumption)\n"); return false; @@ -1355,7 +1311,7 @@ const bool Subsumer::simplifyBySubsumption() endSimplifyBySubsumption: if (!solver.ok) return false; - solver.ok = (solver.propagate() == NULL); + solver.ok = (solver.propagate().isNULL()); if (!solver.ok) { printf("c (contradiction during subsumption)\n"); return false; @@ -1364,21 +1320,15 @@ const bool Subsumer::simplifyBySubsumption() #ifndef NDEBUG verifyIntegrity(); #endif - - //vector var_merged = merge(); + removeWrong(solver.learnts); removeWrong(solver.binaryClauses); removeAssignedVarsFromEliminated(); - - /*solver.clauseCleaner->cleanClausesBewareNULL(clauses, ClauseCleaner::simpClauses, *this); - addFromSolver(solver.learnts, true); - addFromSolver(solver.binaryClauses, true); - if (solver.doHyperBinRes && clauses.size() < 1000000 && numCalls > 1 && !hyperBinRes()) - return false;*/ + solver.order_heap.filter(Solver::VarFilter(solver)); addBackToSolver(); - solver.nbCompensateSubsumer += origNLearnts-solver.learnts.size(); + freeMemory(); if (solver.verbosity >= 1) { std::cout << "c | lits-rem: " << std::setw(9) << literals_removed @@ -1616,219 +1566,6 @@ void Subsumer::orderVarsForElim(vec& order) } } -const bool Subsumer::hyperUtility(vec& iter, const Lit lit, BitArray& inside, vec& addToClauses) -{ - for (ClauseSimp *it = iter.getData(), *end = it + iter.size() ; it != end; it++) { - if (it->clause == NULL) continue; - uint32_t notIn = 0; - Lit notInLit = lit_Undef; - - Clause& cl = *it->clause; - for (uint32_t i = 0; i < cl.size(); i++) { - if (cl[i].var() == lit.var() || cl.size() == 2) { - goto next; - } - if (!inside[cl[i].toInt()]) { - notIn++; - if (notIn > 1) goto next; - notInLit = cl[i]; - } - } - - if (notIn == 0) { - vec lits(1); - lits[0] = lit; - solver.addClauseInt(lits, cl.getGroup()); - if (!solver.ok) return false; - } - - if (notIn == 1 && !inside[(~notInLit).toInt()]) { - vec cs(2); - cs[0] = lit; - cs[1] = notInLit; - //uint32_t index = subsume0(cs, calcAbstraction(cs)); - /*if (index != std::numeric_limits::max()) { - Clause *cl3 = Clause_new(cs, cl.getGroup()); - ClauseSimp c(cl3, index); - addToClauses.push(c); - inside.setBit((~notInLit).toInt()); - #ifdef HYPER_DEBUG - std::cout << "HyperBinRes adding clause: "; - cl3->plainPrint(); - #endif - } else {*/ - Clause *cl3 = Clause_new(cs, cl.getGroup()); - addToClauses.push(cl3); - inside.setBit((~notInLit).toInt()); - //} - } - next:; - } - - return true; -} - -const bool Subsumer::hyperBinRes() -{ - double myTime = cpuTime(); - - BitArray inside; - inside.resize(solver.nVars()*2, 0); - uint32_t hyperBinAdded = 0; - uint32_t oldTrailSize = solver.trail.size(); - vec addToClauses; - vec addedToInside; - uint64_t totalClausesChecked = 0; - - vec varsToCheck; - - if (clauses.size() > 500000 || solver.order_heap.size() > 50000) { - Heap tmp(solver.order_heap); - uint32_t thisTopX = std::min(tmp.size(), 5000U); - for (uint32_t i = 0; i != thisTopX; i++) - varsToCheck.push(tmp.removeMin()); - } else { - for (Var i = 0; i < solver.nVars(); i++) - varsToCheck.push(i); - } - - for (uint32_t test = 0; test < 2*varsToCheck.size(); test++) if (solver.assigns[test/2] == l_Undef && solver.decision_var[test/2]) { - if (totalClausesChecked > 1000000) - break; - - inside.setZero(); - addToClauses.clear(); - addedToInside.clear(); - - Lit lit(varsToCheck[test/2], test&1); - #ifdef HYPER_DEBUG - std::cout << "Resolving with literal:" << (lit.sign() ? "-" : "") << lit.var()+1 << std::endl; - #endif - - //fill inside with binary clauses' literals that this lit is in - //addedToInside now contains the list - vec& set = occur[lit.toInt()]; - totalClausesChecked += occur.size(); - for (ClauseSimp *it = set.getData(), *end = it + set.size() ; it != end; it++) { - if (it->clause == NULL) continue; - Clause& cl2 = *it->clause; - if (cl2.size() > 2) continue; - assert(cl2[0] == lit || cl2[1] == lit); - if (cl2[0] == lit) { - if (!inside[(~cl2[1]).toInt()]) { - inside.setBit((~cl2[1]).toInt()); - addedToInside.push(~cl2[1]); - } - } else { - if (!inside[(~cl2[0]).toInt()]) { - inside.setBit((~cl2[0]).toInt()); - addedToInside.push(~cl2[0]); - } - } - } - - uint32_t sum = 0; - for (uint32_t add = 0; add < addedToInside.size(); add++) { - sum += occur[addedToInside[add].toInt()].size(); - } - - if (sum < clauses.size()) { - totalClausesChecked += sum; - for (uint32_t add = 0; add < addedToInside.size(); add++) { - vec& iter = occur[addedToInside[add].toInt()]; - if (!hyperUtility(iter, lit, inside, addToClauses)) - return false; - } - } else { - totalClausesChecked += clauses.size(); - if (!hyperUtility(clauses, lit, inside, addToClauses)) - return false; - } - - hyperBinAdded += addToClauses.size(); - for (uint32_t i = 0; i < addToClauses.size(); i++) { - Clause *c = solver.addClauseInt(*addToClauses[i], addToClauses[i]->getGroup()); - clauseFree(addToClauses[i]); - if (c != NULL) { - ClauseSimp cc = linkInClause(*c); - subsume1(cc); - } - if (!solver.ok) return false; - } - } - - if (solver.verbosity >= 1) { - std::cout << "c | Hyper-binary res binary added: " << std::setw(5) << hyperBinAdded - << " unitaries: " << std::setw(5) << solver.trail.size() - oldTrailSize - << " time: " << std::setprecision(2) << std::setw(5)<< cpuTime() - myTime << " s" - << " |" << std::endl; - } - - return true; -} - -class varDataStruct -{ - public: - varDataStruct() : - numPosClauses (0) - , numNegClauses (0) - , sumPosClauseSize (0) - , sumNegClauseSize (0) - , posHash(0) - , negHash(0) - {} - const bool operator < (const varDataStruct& other) const - { - if (numPosClauses < other.numPosClauses) return true; - if (numPosClauses > other.numPosClauses) return false; - - if (numNegClauses < other.numNegClauses) return true; - if (numNegClauses > other.numNegClauses) return false; - - if (sumPosClauseSize < other.sumPosClauseSize) return true; - if (sumPosClauseSize > other.sumPosClauseSize) return false; - - if (sumNegClauseSize < other.sumNegClauseSize) return true; - if (sumNegClauseSize > other.sumNegClauseSize) return false; - - if (posHash < other.posHash) return true; - if (posHash > other.posHash) return false; - - if (negHash < other.negHash) return true; - if (negHash > other.negHash) return false; - - return false; - } - - const bool operator == (const varDataStruct& other) const - { - if (numPosClauses == other.numPosClauses && - numNegClauses == other.numNegClauses && - sumPosClauseSize == other.sumPosClauseSize && - sumNegClauseSize == other.sumNegClauseSize && - posHash == other.posHash && - negHash == other.negHash) - return true; - - return false; - } - - void reversePolarity() - { - std::swap(numPosClauses, numNegClauses); - std::swap(sumPosClauseSize, sumNegClauseSize); - std::swap(posHash, negHash); - } - - uint32_t numPosClauses; - uint32_t numNegClauses; - uint32_t sumPosClauseSize; - uint32_t sumNegClauseSize; - int posHash; - int negHash; -}; - void Subsumer::verifyIntegrity() { vector occurNum(solver.nVars()*2, 0); @@ -2147,78 +1884,4 @@ vector Subsumer::merge() return true; }*/ -/*void Subsumer::pureLiteralRemoval() -{ - for (Var var = 0; var < solver.nVars(); var++) if (solver.decision_var[var] && solver.assigns[var] == l_Undef && !cannot_eliminate[var] && !var_elimed[var] && !solver.varReplacer->varHasBeenReplaced(var)) { - uint32_t numPosClauses = occur[Lit(var, false).toInt()].size(); - uint32_t numNegClauses = occur[Lit(var, true).toInt()].size(); - if (numNegClauses > 0 && numPosClauses > 0) continue; - - if (numNegClauses == 0 && numPosClauses == 0) { - if (solver.decision_var[var]) madeVarNonDecision.push(var); - solver.setDecisionVar(var, false); - pureLitRemoved[var] = true; - pureLitsRemovedNum++; - continue; - } - - if (numPosClauses == 0 && numNegClauses > 0) { - if (solver.decision_var[var]) madeVarNonDecision.push(var); - solver.setDecisionVar(var, false); - pureLitRemoved[var] = true; - assignVar.push(Lit(var, true)); - vec occ(occur[Lit(var, true).toInt()]); - for (ClauseSimp *it = occ.getData(), *end = occ.getDataEnd(); it != end; it++) { - unlinkClause(*it); - pureLitClauseRemoved.push(it->clause); - } - pureLitsRemovedNum++; - continue; - } - - if (numNegClauses == 0 && numPosClauses > 0) { - if (solver.decision_var[var]) madeVarNonDecision.push(var); - solver.setDecisionVar(var, false); - pureLitRemoved[var] = true; - assignVar.push(Lit(var, false)); - vec occ(occur[Lit(var, false).toInt()]); - for (ClauseSimp *it = occ.getData(), *end = occ.getDataEnd(); it != end; it++) { - unlinkClause(*it); - pureLitClauseRemoved.push(it->clause); - } - pureLitsRemovedNum++; - continue; - } - } -}*/ - -/*void Subsumer::undoPureLitRemoval() -{ - assert(solver.ok); - for (uint32_t i = 0; i < madeVarNonDecision.size(); i++) { - assert(!solver.decision_var[madeVarNonDecision[i]]); - assert(solver.assigns[madeVarNonDecision[i]] == l_Undef); - solver.setDecisionVar(madeVarNonDecision[i], true); - pureLitRemoved[madeVarNonDecision[i]] = false; - } - madeVarNonDecision.clear(); - - for (Lit *l = assignVar.getData(), *end = assignVar.getDataEnd(); l != end; l++) { - solver.uncheckedEnqueue(*l); - solver.ok = (solver.propagate() == NULL); - assert(solver.ok); - } - assignVar.clear(); -} - -void Subsumer::reAddPureLitClauses() -{ - for (Clause **it = pureLitClauseRemoved.getData(), **end = pureLitClauseRemoved.getDataEnd(); it != end; it++) { - solver.addClause(**it, (*it)->getGroup()); - clauseFree(*it); - assert(solver.ok); - } - pureLitClauseRemoved.clear(); -}*/ - }; //NAMESPACE MINISAT diff --git a/src/sat/cryptominisat2/Subsumer.h b/src/sat/cryptominisat2/Subsumer.h index 098faa9..a36ea7a 100644 --- a/src/sat/cryptominisat2/Subsumer.h +++ b/src/sat/cryptominisat2/Subsumer.h @@ -22,6 +22,7 @@ namespace MINISAT using namespace MINISAT; class ClauseCleaner; +class OnlyNonLearntBins; class Subsumer { @@ -32,13 +33,12 @@ public: ~Subsumer(); //Called from main - const bool simplifyBySubsumption(); - const bool subsumeWithBinaries(const bool startUp); + const bool simplifyBySubsumption(const bool alsoLearnt = false); + const bool subsumeWithBinaries(OnlyNonLearntBins* onlyNonLearntBins); void newVar(); //Used by cleaner - void unlinkModifiedClause(vec& origClause, ClauseSimp c); - void unlinkModifiedClauseNoDetachNoNULL(vec& origClause, ClauseSimp c); + void unlinkModifiedClause(vec& origClause, ClauseSimp c, const bool detachAndNull); void unlinkClause(ClauseSimp cc, Var elim = var_Undef); ClauseSimp linkInClause(Clause& cl); void linkInAlreadyClause(ClauseSimp& c); @@ -59,6 +59,7 @@ public: private: friend class ClauseCleaner; + friend class ClauseAllocator; //Main vec clauses; @@ -95,12 +96,14 @@ private: //Start-up template void addFromSolver(vec& cs, bool alsoLearnt = false); + void fillCannotEliminate(); + void clearAll(); + + //Finish-up + void freeMemory(); void addBackToSolver(); void removeWrong(vec& cs); void removeAssignedVarsFromEliminated(); - void fillCannotEliminate(); - const bool treatLearnts(); - void clearAll(); //Iterations void registerIteration (CSet& iter_set) { iter_sets.push(&iter_set); } @@ -118,8 +121,8 @@ private: uint32_t subsume0(T& ps, uint32_t abs); template uint32_t subsume0Orig(const T& ps, uint32_t abs); + bool subsumedNonLearnt; void subsume0BIN(const Lit lit, const vec& lits); - void subsume0LearntSet(vec& cs); void subsume1(ClauseSimp& ps); void smaller_database(); void almost_all_database(); @@ -128,15 +131,14 @@ private: bool subsetAbst(uint32_t A, uint32_t B); void orderVarsForElim(vec& order); - int substitute(Lit x, Clause& def, vec& poss, vec& negs, vec& new_clauses); bool maybeEliminate(Var x); void MigrateToPsNs(vec& poss, vec& negs, vec& ps, vec& ns, const Var x); void DeallocPsNs(vec& ps, vec& ns); bool merge(const Clause& ps, const Clause& qs, const Lit without_p, const Lit without_q, vec& out_clause); //Subsume with Nonexistent Bins - const bool subsWNonExistBinsFull(const bool startUp); - const bool subsWNonExistBins(const Lit& lit, const bool startUp); + const bool subsWNonExistBinsFull(OnlyNonLearntBins* onlyNonLearntBins); + const bool subsWNonExistBins(const Lit& lit, OnlyNonLearntBins* onlyNonLearntBins); template void subsume1Partial(const T& ps); uint32_t subsNonExistentNum; @@ -152,15 +154,6 @@ private: vec toVisitAll; vec ps2; - //hyperBinRes - void addFromSolverAll(vec& cs); - const bool hyperBinRes(); - const bool hyperUtility(vec& iter, const Lit lit, BitArray& inside, vec& addToClauses); - - //merging - //vector merge(); - //const bool checkIfSame(const Lit var1, const Lit var2); - class VarOcc { public: VarOcc(const Var& v, const uint32_t num) : diff --git a/src/sat/cryptominisat2/UselessBinRemover.cpp b/src/sat/cryptominisat2/UselessBinRemover.cpp new file mode 100644 index 0000000..56fb654 --- /dev/null +++ b/src/sat/cryptominisat2/UselessBinRemover.cpp @@ -0,0 +1,199 @@ +/*********************************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +This program is free software: you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation, either version 3 of the License, or +(at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program. If not, see . +**************************************************************************************************/ + +#include +#include "UselessBinRemover.h" +#include "VarReplacer.h" +#include "ClauseCleaner.h" +#include "time_mem.h" +#include "OnlyNonLearntBins.h" + +namespace MINISAT +{ +using namespace MINISAT; + +UselessBinRemover::UselessBinRemover(Solver& _solver, OnlyNonLearntBins& _onlyNonLearntBins) : + solver(_solver) + , onlyNonLearntBins(_onlyNonLearntBins) +{ +} + +#define MAX_REMOVE_BIN_FULL_PROPS 20000000 +#define EXTRATIME_DIVIDER 2 + +const bool UselessBinRemover::removeUslessBinFull() +{ + double myTime = cpuTime(); + toDeleteSet.clear(); + toDeleteSet.growTo(solver.nVars()*2, 0); + uint32_t origHeapSize = solver.order_heap.size(); + uint64_t origProps = solver.propagations; + bool fixed = false; + uint32_t extraTime = solver.binaryClauses.size() / EXTRATIME_DIVIDER; + + uint32_t startFrom = solver.mtrand.randInt(solver.order_heap.size()); + for (uint32_t i = 0; i != solver.order_heap.size(); i++) { + Var var = solver.order_heap[(i+startFrom)%solver.order_heap.size()]; + if (solver.propagations - origProps + extraTime > MAX_REMOVE_BIN_FULL_PROPS) break; + if (solver.assigns[var] != l_Undef || !solver.decision_var[var]) continue; + + Lit lit(var, true); + if (!removeUselessBinaries(lit)) { + fixed = true; + solver.cancelUntil(0); + solver.uncheckedEnqueue(~lit); + solver.ok = (solver.propagate().isNULL()); + if (!solver.ok) return false; + continue; + } + + lit = ~lit; + if (!removeUselessBinaries(lit)) { + fixed = true; + solver.cancelUntil(0); + solver.uncheckedEnqueue(~lit); + solver.ok = (solver.propagate().isNULL()); + if (!solver.ok) return false; + continue; + } + } + + uint32_t removedUselessBin = onlyNonLearntBins.removeBins(); + + if (fixed) solver.order_heap.filter(Solver::VarFilter(solver)); + + if (solver.verbosity >= 1) { + std::cout + << "c Removed useless bin:" << std::setw(8) << removedUselessBin + << " fixed: " << std::setw(5) << (origHeapSize - solver.order_heap.size()) + << " props: " << std::fixed << std::setprecision(2) << std::setw(6) << (double)(solver.propagations - origProps)/1000000.0 << "M" + << " time: " << std::fixed << std::setprecision(2) << std::setw(5) << cpuTime() - myTime << " s" + << std::setw(16) << " |" << std::endl; + } + + return true; +} + +const bool UselessBinRemover::removeUselessBinaries(const Lit& lit) +{ + solver.newDecisionLevel(); + solver.uncheckedEnqueueLight(lit); + failed = !onlyNonLearntBins.propagateBinOneLevel(); + if (failed) return false; + bool ret = true; + + oneHopAway.clear(); + assert(solver.decisionLevel() > 0); + int c; + if (solver.trail.size()-solver.trail_lim[0] == 0) { + solver.cancelUntil(0); + goto end; + } + extraTime += (solver.trail.size() - solver.trail_lim[0]) / EXTRATIME_DIVIDER; + for (c = solver.trail.size()-1; c > (int)solver.trail_lim[0]; c--) { + Lit x = solver.trail[c]; + toDeleteSet[x.toInt()] = true; + oneHopAway.push(x); + solver.assigns[x.var()] = l_Undef; + } + solver.assigns[solver.trail[c].var()] = l_Undef; + + solver.qhead = solver.trail_lim[0]; + solver.trail.shrink_(solver.trail.size() - solver.trail_lim[0]); + solver.trail_lim.clear(); + //solver.cancelUntil(0); + + wrong.clear(); + for(uint32_t i = 0; i < oneHopAway.size(); i++) { + //no need to visit it if it already queued for removal + //basically, we check if it's in 'wrong' + if (toDeleteSet[oneHopAway[i].toInt()]) { + if (!fillBinImpliesMinusLast(lit, oneHopAway[i], wrong)) { + ret = false; + goto end; + } + } + } + + for (uint32_t i = 0; i < wrong.size(); i++) { + removeBin(~lit, wrong[i]); + } + + end: + for(uint32_t i = 0; i < oneHopAway.size(); i++) { + toDeleteSet[oneHopAway[i].toInt()] = false; + } + + return ret; +} + +void UselessBinRemover::removeBin(const Lit& lit1, const Lit& lit2) +{ + /******************* + Lit litFind1 = lit_Undef; + Lit litFind2 = lit_Undef; + + if (solver.binwatches[(~lit1).toInt()].size() < solver.binwatches[(~lit2).toInt()].size()) { + litFind1 = lit1; + litFind2 = lit2; + } else { + litFind1 = lit2; + litFind2 = lit1; + } + ********************/ + + //Find AND remove from watches + #ifdef VERBOSE_DEBUG + std::cout << "Removing useless bin: "; + lit1.print(); lit2.printFull(); + #endif //VERBOSE_DEBUG + + solver.removeWatchedBinClAll(solver.binwatches[(~lit1).toInt()], lit2); + solver.removeWatchedBinClAll(solver.binwatches[(~lit2).toInt()], lit1); + onlyNonLearntBins.removeBin(lit1, lit2); +} + +const bool UselessBinRemover::fillBinImpliesMinusLast(const Lit& origLit, const Lit& lit, vec& wrong) +{ + solver.newDecisionLevel(); + solver.uncheckedEnqueueLight(lit); + //if it's a cycle, it doesn't work, so don't propagate origLit + failed = !onlyNonLearntBins.propagateBinExcept(origLit); + if (failed) return false; + + assert(solver.decisionLevel() > 0); + int c; + extraTime += (solver.trail.size() - solver.trail_lim[0]) / EXTRATIME_DIVIDER; + for (c = solver.trail.size()-1; c > (int)solver.trail_lim[0]; c--) { + Lit x = solver.trail[c]; + if (toDeleteSet[x.toInt()]) { + wrong.push(x); + toDeleteSet[x.toInt()] = false; + }; + solver.assigns[x.var()] = l_Undef; + } + solver.assigns[solver.trail[c].var()] = l_Undef; + + solver.qhead = solver.trail_lim[0]; + solver.trail.shrink_(solver.trail.size() - solver.trail_lim[0]); + solver.trail_lim.clear(); + //solver.cancelUntil(0); + + return true; +} + +}; //NAMESPACE MINISAT diff --git a/src/sat/cryptominisat2/UselessBinRemover.h b/src/sat/cryptominisat2/UselessBinRemover.h new file mode 100644 index 0000000..771bd1b --- /dev/null +++ b/src/sat/cryptominisat2/UselessBinRemover.h @@ -0,0 +1,53 @@ +/*********************************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +This program is free software: you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation, either version 3 of the License, or +(at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program. If not, see . +**************************************************************************************************/ + +#ifndef USELESSBINREMOVER_H +#define USELESSBINREMOVER_H + +#include "Vec.h" +#include "Solver.h" +#include "OnlyNonLearntBins.h" +#include + +namespace MINISAT +{ +using namespace MINISAT; + +class UselessBinRemover { + public: + UselessBinRemover(Solver& solver, OnlyNonLearntBins& onlyNonLearntBins); + const bool removeUslessBinFull(); + + private: + bool failed; + uint32_t extraTime; + + //Remove useless binaries + const bool fillBinImpliesMinusLast(const Lit& origLit, const Lit& lit, vec& wrong); + const bool removeUselessBinaries(const Lit& lit); + void removeBin(const Lit& lit1, const Lit& lit2); + vec toDeleteSet; + vec oneHopAway; + vec wrong; + + Solver& solver; + OnlyNonLearntBins& onlyNonLearntBins; +}; + +#endif //USELESSBINREMOVER_H + +}; //NAMESPACE MINISAT diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION index 2e8f2e9..75dc444 100644 --- a/src/sat/cryptominisat2/VERSION +++ b/src/sat/cryptominisat2/VERSION @@ -1,2 +1,2 @@ CryptoMiniSat -GIT revision: ef1086af7fca458d28352cdda8ebe74339ed5817 +GIT revision: d1a89e619d41131629e6c4e74f9424453225ba2d diff --git a/src/sat/cryptominisat2/VarReplacer.cpp b/src/sat/cryptominisat2/VarReplacer.cpp index 8e966d1..3fbf609 100644 --- a/src/sat/cryptominisat2/VarReplacer.cpp +++ b/src/sat/cryptominisat2/VarReplacer.cpp @@ -48,7 +48,7 @@ VarReplacer::VarReplacer(Solver& _solver) : VarReplacer::~VarReplacer() { for (uint i = 0; i != clauses.size(); i++) - clauseFree(clauses[i]); + solver.clauseAllocator.clauseFree(clauses[i]); } const bool VarReplacer::performReplaceInternal() @@ -167,7 +167,7 @@ const bool VarReplacer::replace_set(vec& cs) if (changed && handleUpdatedClause(c, origVar1, origVar2)) { if (!solver.ok) { - for(;r != end; r++) clauseFree(*r); + for(;r != end; r++) solver.clauseAllocator.clauseFree(*r); cs.shrink(r-a); return false; } @@ -215,7 +215,7 @@ const bool VarReplacer::handleUpdatedClause(XorClause& c, const Var origVar1, co case 1: solver.detachModifiedClause(origVar1, origVar2, origSize, &c); solver.uncheckedEnqueue(Lit(c[0].var(), c.xor_clause_inverted())); - solver.ok = (solver.propagate() == NULL); + solver.ok = (solver.propagate().isNULL()); return true; case 2: { solver.detachModifiedClause(origVar1, origVar2, origSize, &c); @@ -254,14 +254,18 @@ const bool VarReplacer::replace_set(vec& cs, const bool binClauses) if (changed && handleUpdatedClause(c, origLit1, origLit2)) { if (!solver.ok) { - for(;r != end; r++) clauseFree(*r); + for(;r != end; r++) solver.clauseAllocator.clauseFree(*r); cs.shrink(r-a); return false; } } else { if (!binClauses && c.size() == 2) { + solver.detachClause(c); + Clause *c2 = solver.clauseAllocator.Clause_new(c); + solver.clauseAllocator.clauseFree(&c); + solver.attachClause(*c2); solver.becameBinary++; - solver.binaryClauses.push(&c); + solver.binaryClauses.push(c2); } else *a++ = *r; } @@ -301,7 +305,7 @@ const bool VarReplacer::handleUpdatedClause(Clause& c, const Lit origLit1, const case 1 : solver.detachModifiedClause(origLit1, origLit2, origSize, &c); solver.uncheckedEnqueue(c[0]); - solver.ok = (solver.propagate() == NULL); + solver.ok = (solver.propagate().isNULL()); return true; default: solver.detachModifiedClause(origLit1, origLit2, origSize, &c); @@ -348,7 +352,7 @@ void VarReplacer::extendModelPossible() const assert(solver.assigns[i].getBool() == (solver.assigns[it->var()].getBool() ^ it->sign())); } } - solver.ok = (solver.propagate() == NULL); + solver.ok = (solver.propagate().isNULL()); assert(solver.ok); } } @@ -476,7 +480,7 @@ void VarReplacer::addBinaryXorClause(T& ps, const bool xor_clause_inverted, cons Clause* c; ps[0] ^= xor_clause_inverted; - c = Clause_new(ps, group, false); + c = solver.clauseAllocator.Clause_new(ps, group, false); if (internal) { solver.binaryClauses.push(c); solver.becameBinary++; @@ -486,7 +490,7 @@ void VarReplacer::addBinaryXorClause(T& ps, const bool xor_clause_inverted, cons ps[0] ^= true; ps[1] ^= true; - c = Clause_new(ps, group, false); + c = solver.clauseAllocator.Clause_new(ps, group, false); if (internal) { solver.binaryClauses.push(c); solver.becameBinary++; diff --git a/src/sat/cryptominisat2/VarReplacer.h b/src/sat/cryptominisat2/VarReplacer.h index 6c7abff..4d54d9d 100644 --- a/src/sat/cryptominisat2/VarReplacer.h +++ b/src/sat/cryptominisat2/VarReplacer.h @@ -63,6 +63,10 @@ class VarReplacer const bool varHasBeenReplaced(const Var var) const; const bool replacingVar(const Var var) const; void newVar(); + + //No need to update, only stores binary clauses, that + //have been allocated within pool + //friend class ClauseAllocator; private: const bool performReplaceInternal(); diff --git a/src/sat/cryptominisat2/XSet.h b/src/sat/cryptominisat2/XSet.h index cfe0c19..13fb315 100644 --- a/src/sat/cryptominisat2/XSet.h +++ b/src/sat/cryptominisat2/XSet.h @@ -133,4 +133,4 @@ class XSet { }; //NAMESPACE MINISAT -#endif //XSET_H \ No newline at end of file +#endif //XSET_H diff --git a/src/sat/cryptominisat2/XorFinder.cpp b/src/sat/cryptominisat2/XorFinder.cpp index 53c00db..13c1e65 100644 --- a/src/sat/cryptominisat2/XorFinder.cpp +++ b/src/sat/cryptominisat2/XorFinder.cpp @@ -142,7 +142,7 @@ const bool XorFinder::doNoPart(const uint minSize, const uint maxSize) #endif //DEBUG_XORFIND if (findXors(sumLengths) == false) goto end; - solver.ok = (solver.propagate() == NULL); + solver.ok = (solver.propagate().isNULL()); end: if (minSize == maxSize && minSize == 2) { @@ -222,7 +222,7 @@ const bool XorFinder::findXors(uint& sumLengths) break; } default: { - XorClause* x = XorClause_new(lits, impair, old_group); + XorClause* x = solver.clauseAllocator.XorClause_new(lits, impair, old_group); solver.xorclauses.push(x); solver.attachClause(*x); diff --git a/src/sat/cryptominisat2/XorSubsumer.cpp b/src/sat/cryptominisat2/XorSubsumer.cpp index f7e7fe9..d1f6dd8 100644 --- a/src/sat/cryptominisat2/XorSubsumer.cpp +++ b/src/sat/cryptominisat2/XorSubsumer.cpp @@ -39,35 +39,30 @@ XorSubsumer::XorSubsumer(Solver& s): }; // Will put NULL in 'cs' if clause removed. -void XorSubsumer::subsume0(XorClauseSimp& ps) +void XorSubsumer::subsume0(XorClauseSimp ps) { #ifdef VERBOSE_DEBUGSUBSUME0 cout << "subsume0 orig clause:"; ps.clause->plainPrint(); #endif - - vec origClause(ps.clause->size()); - std::copy(ps.clause->getData(), ps.clause->getDataEnd(), origClause.getData()); - const bool origClauseInverted = ps.clause->xor_clause_inverted(); - + vec unmatchedPart; - bool needUnlinkPS = false; - vec subs; + findSubsumed(*ps.clause, subs); for (uint32_t i = 0; i < subs.size(); i++){ XorClause* tmp = subs[i].clause; - findUnMatched(origClause, *tmp, unmatchedPart); + findUnMatched(*ps.clause, *tmp, unmatchedPart); if (unmatchedPart.size() == 0) { #ifdef VERBOSE_DEBUGSUBSUME0 cout << "subsume0 removing:"; subs[i].clause->plainPrint(); #endif clauses_subsumed++; - assert(tmp->size() == origClause.size()); - if (origClauseInverted == tmp->xor_clause_inverted()) { + assert(tmp->size() == ps.clause->size()); + if (ps.clause->xor_clause_inverted() == tmp->xor_clause_inverted()) { unlinkClause(subs[i]); - clauseFree(tmp); + solver.clauseAllocator.clauseFree(tmp); } else { solver.ok = false; return; @@ -79,24 +74,18 @@ void XorSubsumer::subsume0(XorClauseSimp& ps) std::cout << "Cutting xor-clause:"; subs[i].clause->plainPrint(); #endif //VERBOSE_DEBUG - XorClause *c = solver.addXorClauseInt(unmatchedPart, tmp->xor_clause_inverted() ^ !origClauseInverted, tmp->getGroup()); - if (c != NULL) { + XorClause *c = solver.addXorClauseInt(unmatchedPart, tmp->xor_clause_inverted() ^ !ps.clause->xor_clause_inverted(), tmp->getGroup()); + if (c != NULL) linkInClause(*c); - needUnlinkPS = true; - } + unlinkClause(subs[i]); if (!solver.ok) return; } unmatchedPart.clear(); } - - if (needUnlinkPS) { - XorClause* tmp = ps.clause; - unlinkClause(ps); - clauseFree(tmp); - } } -void XorSubsumer::findUnMatched(vec& A, XorClause& B, vec& unmatchedPart) +template +void XorSubsumer::findUnMatched(const T& A, const T& B, vec& unmatchedPart) { for (uint32_t i = 0; i != B.size(); i++) seen_tmp[B[i].var()] = 1; @@ -115,7 +104,7 @@ void XorSubsumer::unlinkClause(XorClauseSimp c, const Var elim) XorClause& cl = *c.clause; for (uint32_t i = 0; i < cl.size(); i++) { - maybeRemove(occur[cl[i].var()], &cl); + removeW(occur[cl[i].var()], &cl); } if (elim != var_Undef) @@ -129,7 +118,7 @@ void XorSubsumer::unlinkClause(XorClauseSimp c, const Var elim) void XorSubsumer::unlinkModifiedClause(vec& origClause, XorClauseSimp c) { for (uint32_t i = 0; i < origClause.size(); i++) { - maybeRemove(occur[origClause[i].var()], c.clause); + removeW(occur[origClause[i].var()], c.clause); } solver.detachModifiedClause(origClause[0].var(), origClause[1].var(), origClause.size(), c.clause); @@ -140,7 +129,7 @@ void XorSubsumer::unlinkModifiedClause(vec& origClause, XorClauseSimp c) void XorSubsumer::unlinkModifiedClauseNoDetachNoNULL(vec& origClause, XorClauseSimp c) { for (uint32_t i = 0; i < origClause.size(); i++) { - maybeRemove(occur[origClause[i].var()], c.clause); + removeW(occur[origClause[i].var()], c.clause); } } @@ -259,10 +248,7 @@ const bool XorSubsumer::localSubstitute() for (uint32_t i2 = i+1; i2 < occ.size(); i2++) { XorClause& c2 = *occ[i2].clause; tmp.clear(); - tmp.growTo(c1.size() + c2.size()); - std::copy(c1.getData(), c1.getDataEnd(), tmp.getData()); - std::copy(c2.getData(), c2.getDataEnd(), tmp.getData() + c1.size()); - clearDouble(tmp); + xorTwoClauses(c1, c2, tmp); if (tmp.size() <= 2) { #ifdef VERBOSE_DEBUG std::cout << "Local substiuting. Clause1:"; c1.plainPrint(); @@ -287,20 +273,26 @@ const bool XorSubsumer::localSubstitute() return true; } -void XorSubsumer::clearDouble(vec& ps) const +template +void XorSubsumer::xorTwoClauses(const T& c1, const T& c2, vec& xored) { - std::sort(ps.getData(), ps.getDataEnd()); - Lit p; - uint32_t i, j; - for (i = j = 0, p = lit_Undef; i != ps.size(); i++) { - if (ps[i].var() == p.var()) { - //added, but easily removed - j--; - p = lit_Undef; - } else - ps[j++] = p = ps[i]; + for (uint32_t i = 0; i != c1.size(); i++) + seen_tmp[c1[i].var()] = 1; + for (uint32_t i = 0; i != c2.size(); i++) + seen_tmp[c2[i].var()] ^= 1; + + for (uint32_t i = 0; i != c1.size(); i++) { + if (seen_tmp[c1[i].var()] == 1) { + xored.push(Lit(c1[i].var(), false)); + seen_tmp[c1[i].var()] = 0; + } + } + for (uint32_t i = 0; i != c2.size(); i++) { + if (seen_tmp[c2[i].var()] == 1) { + xored.push(Lit(c2[i].var(), false)); + seen_tmp[c2[i].var()] = 0; + } } - ps.shrink(i - j); } void XorSubsumer::removeWrong(vec& cs) @@ -318,7 +310,7 @@ void XorSubsumer::removeWrong(vec& cs) if (var_elimed[l->var()]) { remove = true; solver.detachClause(c); - clauseFree(&c); + solver.clauseAllocator.clauseFree(&c); break; } } @@ -365,7 +357,7 @@ const bool XorSubsumer::removeDependent() XorClauseSimp toUnlink0 = occ[0]; XorClauseSimp toUnlink1 = occ[1]; unlinkClause(toUnlink0); - clauseFree(toUnlink0.clause); + solver.clauseAllocator.clauseFree(toUnlink0.clause); unlinkClause(toUnlink1, var); solver.setDecisionVar(var, false); var_elimed[var] = true; @@ -419,7 +411,7 @@ const bool XorSubsumer::unEliminate(const Var var) for (vector::iterator it2 = it->second.begin(), end2 = it->second.end(); it2 != end2; it2++) { XorClause& c = **it2; solver.addXorClause(c, c.xor_clause_inverted()); - clauseFree(&c); + solver.clauseAllocator.clauseFree(&c); } solver.libraryCNFFile = backup_libraryCNFfile; elimedOutVar.erase(it); @@ -480,7 +472,7 @@ const bool XorSubsumer::simplifyBySubsumption(const bool doFullSubsume) } propagated = (solver.qhead != solver.trail.size()); - solver.ok = (solver.propagate() == NULL); + solver.ok = (solver.propagate().isNULL()); if (!solver.ok) { std::cout << "c (contradiction during subsumption)" << std::endl; return false; @@ -600,4 +592,4 @@ const bool XorSubsumer::checkElimedUnassigned() const return true; } -}; //NAMESPACE MINISAT \ No newline at end of file +}; //NAMESPACE MINISAT diff --git a/src/sat/cryptominisat2/XorSubsumer.h b/src/sat/cryptominisat2/XorSubsumer.h index b603a94..43867fa 100644 --- a/src/sat/cryptominisat2/XorSubsumer.h +++ b/src/sat/cryptominisat2/XorSubsumer.h @@ -38,6 +38,7 @@ public: private: friend class ClauseCleaner; + friend class ClauseAllocator; //Main vec clauses; @@ -55,11 +56,12 @@ private: // Subsumption: void findSubsumed(XorClause& ps, vec& out_subsumed); bool isSubsumed(XorClause& ps); - void subsume0(XorClauseSimp& ps); + void subsume0(XorClauseSimp ps); template bool subset(const T1& A, const T2& B); bool subsetAbst(uint32_t A, uint32_t B); - void findUnMatched(vec& A, XorClause& B, vec& unmatchedPart); + template + void findUnMatched(const T& A, const T& B, vec& unmatchedPart); //helper void testAllClauseAttach() const; @@ -78,7 +80,8 @@ private: uint32_t numElimed; //Heule-process - void clearDouble(vec& ps) const; + template + void xorTwoClauses(const T& c1, const T& c2, vec& xored); const bool localSubstitute(); uint32_t localSubstituteUseful; diff --git a/src/sat/cryptominisat2/constants.h b/src/sat/cryptominisat2/constants.h index 02d5766..436128d 100644 --- a/src/sat/cryptominisat2/constants.h +++ b/src/sat/cryptominisat2/constants.h @@ -18,7 +18,7 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ -#define RATIOREMOVECLAUSES 3 +#define RATIOREMOVECLAUSES 2 #define NBCLAUSESBEFOREREDUCE 20000 #define DYNAMICNBLEVEL #define UPDATEVARACTIVITY @@ -43,4 +43,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA //#define USE_OLD_POLARITIES //#define DEBUG_VARELIM #define BURST_SEARCH -#define USE_POOLS +//#define DEBUG_PROPAGATEFROM + +#ifdef HAVE_CONFIG_H +#include "config.h" +#endif //HAVE_CONFIG_H diff --git a/src/sat/cryptominisat2/pool.hpp b/src/sat/cryptominisat2/pool.hpp deleted file mode 100644 index be1137a..0000000 --- a/src/sat/cryptominisat2/pool.hpp +++ /dev/null @@ -1,584 +0,0 @@ -// Copyright (C) 2000, 2001 Stephen Cleary -// -// Distributed under the Boost Software License, Version 1.0. (See -// accompanying file LICENSE_1_0.txt or copy at -// http://www.boost.org/LICENSE_1_0.txt) -// -// See http://www.boost.org for updates, documentation, and revision history. - -#ifndef BOOST_POOL_HPP -#define BOOST_POOL_HPP - -#include // for workarounds - -// std::less, std::less_equal, std::greater -#include -// new[], delete[], std::nothrow -#include -// std::size_t, std::ptrdiff_t -#include -// std::malloc, std::free -#include -// std::invalid_argument -#include -// std::max -#include - -#include "poolfwd.hpp" - -// boost::details::pool::ct_lcm -#include -// boost::details::pool::lcm -#include -// boost::simple_segregated_storage -#include - -#ifdef BOOST_NO_STDC_NAMESPACE - namespace std { using ::malloc; using ::free; } -#endif - -// There are a few places in this file where the expression "this->m" is used. -// This expression is used to force instantiation-time name lookup, which I am -// informed is required for strict Standard compliance. It's only necessary -// if "m" is a member of a base class that is dependent on a template -// parameter. -// Thanks to Jens Maurer for pointing this out! - -namespace boost { - -struct default_user_allocator_new_delete -{ - typedef std::size_t size_type; - typedef std::ptrdiff_t difference_type; - - static char * malloc(const size_type bytes) - { return new (std::nothrow) char[bytes]; } - static void free(char * const block) - { delete [] block; } -}; - -struct default_user_allocator_malloc_free -{ - typedef std::size_t size_type; - typedef std::ptrdiff_t difference_type; - - static char * malloc(const size_type bytes) - { return reinterpret_cast(std::malloc(bytes)); } - static void free(char * const block) - { std::free(block); } -}; - -namespace details { - -// PODptr is a class that pretends to be a "pointer" to different class types -// that don't really exist. It provides member functions to access the "data" -// of the "object" it points to. Since these "class" types are of variable -// size, and contains some information at the *end* of its memory (for -// alignment reasons), PODptr must contain the size of this "class" as well as -// the pointer to this "object". -template -class PODptr -{ - public: - typedef SizeType size_type; - - private: - char * ptr; - size_type sz; - - char * ptr_next_size() const - { return (ptr + sz - sizeof(size_type)); } - char * ptr_next_ptr() const - { - return (ptr_next_size() - - pool::ct_lcm::value); - } - - public: - PODptr(char * const nptr, const size_type nsize) - :ptr(nptr), sz(nsize) { } - PODptr() - :ptr(0), sz(0) { } - - bool valid() const { return (begin() != 0); } - void invalidate() { begin() = 0; } - char * & begin() { return ptr; } - char * begin() const { return ptr; } - char * end() const { return ptr_next_ptr(); } - size_type total_size() const { return sz; } - size_type element_size() const - { - return (sz - sizeof(size_type) - - pool::ct_lcm::value); - } - - size_type & next_size() const - { return *(reinterpret_cast(ptr_next_size())); } - char * & next_ptr() const - { return *(reinterpret_cast(ptr_next_ptr())); } - - PODptr next() const - { return PODptr(next_ptr(), next_size()); } - void next(const PODptr & arg) const - { - next_ptr() = arg.begin(); - next_size() = arg.total_size(); - } -}; - -} // namespace details - -template -class pool: protected simple_segregated_storage< - typename UserAllocator::size_type> -{ - public: - typedef UserAllocator user_allocator; - typedef typename UserAllocator::size_type size_type; - typedef typename UserAllocator::difference_type difference_type; - - private: - BOOST_STATIC_CONSTANT(unsigned, min_alloc_size = - (::boost::details::pool::ct_lcm::value) ); - - // Returns 0 if out-of-memory - // Called if malloc/ordered_malloc needs to resize the free list - void * malloc_need_resize(); - void * ordered_malloc_need_resize(); - - protected: - details::PODptr list; - - simple_segregated_storage & store() { return *this; } - const simple_segregated_storage & store() const { return *this; } - const size_type requested_size; - size_type next_size; - size_type start_size; - - // finds which POD in the list 'chunk' was allocated from - details::PODptr find_POD(void * const chunk) const; - - // is_from() tests a chunk to determine if it belongs in a block - static bool is_from(void * const chunk, char * const i, - const size_type sizeof_i) - { - // We use std::less_equal and std::less to test 'chunk' - // against the array bounds because standard operators - // may return unspecified results. - // This is to ensure portability. The operators < <= > >= are only - // defined for pointers to objects that are 1) in the same array, or - // 2) subobjects of the same object [5.9/2]. - // The functor objects guarantee a total order for any pointer [20.3.3/8] -//WAS: -// return (std::less_equal()(static_cast(i), chunk) -// && std::less()(chunk, -// static_cast(i + sizeof_i))); - std::less_equal lt_eq; - std::less lt; - return (lt_eq(i, chunk) && lt(chunk, i + sizeof_i)); - } - - size_type alloc_size() const - { - const unsigned min_size = min_alloc_size; - return details::pool::lcm(requested_size, min_size); - } - - // for the sake of code readability :) - static void * & nextof(void * const ptr) - { return *(static_cast(ptr)); } - - public: - // The second parameter here is an extension! - // pre: npartition_size != 0 && nnext_size != 0 - explicit pool(const size_type nrequested_size, - const size_type nnext_size = 32) - :list(0, 0), requested_size(nrequested_size), next_size(nnext_size), start_size(nnext_size) - { } - - ~pool() { purge_memory(); } - - // Releases memory blocks that don't have chunks allocated - // pre: lists are ordered - // Returns true if memory was actually deallocated - bool release_memory(); - - // Releases *all* memory blocks, even if chunks are still allocated - // Returns true if memory was actually deallocated - bool purge_memory(); - - // These functions are extensions! - size_type get_next_size() const { return next_size; } - void set_next_size(const size_type nnext_size) { next_size = start_size = nnext_size; } - size_type get_requested_size() const { return requested_size; } - - // Both malloc and ordered_malloc do a quick inlined check first for any - // free chunks. Only if we need to get another memory block do we call - // the non-inlined *_need_resize() functions. - // Returns 0 if out-of-memory - void * malloc() - { - // Look for a non-empty storage - if (!store().empty()) - return store().malloc(); - return malloc_need_resize(); - } - - void * ordered_malloc() - { - // Look for a non-empty storage - if (!store().empty()) - return store().malloc(); - return ordered_malloc_need_resize(); - } - - // Returns 0 if out-of-memory - // Allocate a contiguous section of n chunks - void * ordered_malloc(size_type n); - - // pre: 'chunk' must have been previously - // returned by *this.malloc(). - void free(void * const chunk) - { store().free(chunk); } - - // pre: 'chunk' must have been previously - // returned by *this.malloc(). - void ordered_free(void * const chunk) - { store().ordered_free(chunk); } - - // pre: 'chunk' must have been previously - // returned by *this.malloc(n). - void free(void * const chunks, const size_type n) - { - const size_type partition_size = alloc_size(); - const size_type total_req_size = n * requested_size; - const size_type num_chunks = total_req_size / partition_size + - ((total_req_size % partition_size) ? true : false); - - store().free_n(chunks, num_chunks, partition_size); - } - - // pre: 'chunk' must have been previously - // returned by *this.malloc(n). - void ordered_free(void * const chunks, const size_type n) - { - const size_type partition_size = alloc_size(); - const size_type total_req_size = n * requested_size; - const size_type num_chunks = total_req_size / partition_size + - ((total_req_size % partition_size) ? true : false); - - store().ordered_free_n(chunks, num_chunks, partition_size); - } - - // is_from() tests a chunk to determine if it was allocated from *this - bool is_from(void * const chunk) const - { - return (find_POD(chunk).valid()); - } -}; - -template -bool pool::release_memory() -{ - // This is the return value: it will be set to true when we actually call - // UserAllocator::free(..) - bool ret = false; - - // This is a current & previous iterator pair over the memory block list - details::PODptr ptr = list; - details::PODptr prev; - - // This is a current & previous iterator pair over the free memory chunk list - // Note that "prev_free" in this case does NOT point to the previous memory - // chunk in the free list, but rather the last free memory chunk before the - // current block. - void * free_p = this->first; - void * prev_free_p = 0; - - const size_type partition_size = alloc_size(); - - // Search through all the all the allocated memory blocks - while (ptr.valid()) - { - // At this point: - // ptr points to a valid memory block - // free_p points to either: - // 0 if there are no more free chunks - // the first free chunk in this or some next memory block - // prev_free_p points to either: - // the last free chunk in some previous memory block - // 0 if there is no such free chunk - // prev is either: - // the PODptr whose next() is ptr - // !valid() if there is no such PODptr - - // If there are no more free memory chunks, then every remaining - // block is allocated out to its fullest capacity, and we can't - // release any more memory - if (free_p == 0) - break; - - // We have to check all the chunks. If they are *all* free (i.e., present - // in the free list), then we can free the block. - bool all_chunks_free = true; - - // Iterate 'i' through all chunks in the memory block - // if free starts in the memory block, be careful to keep it there - void * saved_free = free_p; - for (char * i = ptr.begin(); i != ptr.end(); i += partition_size) - { - // If this chunk is not free - if (i != free_p) - { - // We won't be able to free this block - all_chunks_free = false; - - // free_p might have travelled outside ptr - free_p = saved_free; - // Abort searching the chunks; we won't be able to free this - // block because a chunk is not free. - break; - } - - // We do not increment prev_free_p because we are in the same block - free_p = nextof(free_p); - } - - // post: if the memory block has any chunks, free_p points to one of them - // otherwise, our assertions above are still valid - - const details::PODptr next = ptr.next(); - - if (!all_chunks_free) - { - if (is_from(free_p, ptr.begin(), ptr.element_size())) - { - std::less lt; - void * const end = ptr.end(); - do - { - prev_free_p = free_p; - free_p = nextof(free_p); - } while (free_p && lt(free_p, end)); - } - // This invariant is now restored: - // free_p points to the first free chunk in some next memory block, or - // 0 if there is no such chunk. - // prev_free_p points to the last free chunk in this memory block. - - // We are just about to advance ptr. Maintain the invariant: - // prev is the PODptr whose next() is ptr, or !valid() - // if there is no such PODptr - prev = ptr; - } - else - { - // All chunks from this block are free - - // Remove block from list - if (prev.valid()) - prev.next(next); - else - list = next; - - // Remove all entries in the free list from this block - if (prev_free_p != 0) - nextof(prev_free_p) = free_p; - else - this->first = free_p; - - // And release memory - UserAllocator::free(ptr.begin()); - ret = true; - } - - // Increment ptr - ptr = next; - } - - next_size = start_size; - return ret; -} - -template -bool pool::purge_memory() -{ - details::PODptr iter = list; - - if (!iter.valid()) - return false; - - do - { - // hold "next" pointer - const details::PODptr next = iter.next(); - - // delete the storage - UserAllocator::free(iter.begin()); - - // increment iter - iter = next; - } while (iter.valid()); - - list.invalidate(); - this->first = 0; - next_size = start_size; - - return true; -} - -template -void * pool::malloc_need_resize() -{ - // No memory in any of our storages; make a new storage, - const size_type partition_size = alloc_size(); - const size_type POD_size = next_size * partition_size + - details::pool::ct_lcm::value + sizeof(size_type); - char * const ptr = UserAllocator::malloc(POD_size); - if (ptr == 0) - return 0; - const details::PODptr node(ptr, POD_size); - next_size <<= 1; - - // initialize it, - store().add_block(node.begin(), node.element_size(), partition_size); - - // insert it into the list, - node.next(list); - list = node; - - // and return a chunk from it. - return store().malloc(); -} - -template -void * pool::ordered_malloc_need_resize() -{ - // No memory in any of our storages; make a new storage, - const size_type partition_size = alloc_size(); - const size_type POD_size = next_size * partition_size + - details::pool::ct_lcm::value + sizeof(size_type); - char * const ptr = UserAllocator::malloc(POD_size); - if (ptr == 0) - return 0; - const details::PODptr node(ptr, POD_size); - next_size <<= 1; - - // initialize it, - // (we can use "add_block" here because we know that - // the free list is empty, so we don't have to use - // the slower ordered version) - store().add_block(node.begin(), node.element_size(), partition_size); - - // insert it into the list, - // handle border case - if (!list.valid() || std::greater()(list.begin(), node.begin())) - { - node.next(list); - list = node; - } - else - { - details::PODptr prev = list; - - while (true) - { - // if we're about to hit the end or - // if we've found where "node" goes - if (prev.next_ptr() == 0 - || std::greater()(prev.next_ptr(), node.begin())) - break; - - prev = prev.next(); - } - - node.next(prev.next()); - prev.next(node); - } - - // and return a chunk from it. - return store().malloc(); -} - -template -void * pool::ordered_malloc(const size_type n) -{ - const size_type partition_size = alloc_size(); - const size_type total_req_size = n * requested_size; - const size_type num_chunks = total_req_size / partition_size + - ((total_req_size % partition_size) ? true : false); - - void * ret = store().malloc_n(num_chunks, partition_size); - - if (ret != 0) - return ret; - - // Not enougn memory in our storages; make a new storage, - BOOST_USING_STD_MAX(); - next_size = max BOOST_PREVENT_MACRO_SUBSTITUTION(next_size, num_chunks); - const size_type POD_size = next_size * partition_size + - details::pool::ct_lcm::value + sizeof(size_type); - char * const ptr = UserAllocator::malloc(POD_size); - if (ptr == 0) - return 0; - const details::PODptr node(ptr, POD_size); - - // Split up block so we can use what wasn't requested - // (we can use "add_block" here because we know that - // the free list is empty, so we don't have to use - // the slower ordered version) - if (next_size > num_chunks) - store().add_block(node.begin() + num_chunks * partition_size, - node.element_size() - num_chunks * partition_size, partition_size); - - next_size <<= 1; - - // insert it into the list, - // handle border case - if (!list.valid() || std::greater()(list.begin(), node.begin())) - { - node.next(list); - list = node; - } - else - { - details::PODptr prev = list; - - while (true) - { - // if we're about to hit the end or - // if we've found where "node" goes - if (prev.next_ptr() == 0 - || std::greater()(prev.next_ptr(), node.begin())) - break; - - prev = prev.next(); - } - - node.next(prev.next()); - prev.next(node); - } - - // and return it. - return node.begin(); -} - -template -details::PODptr::size_type> -pool::find_POD(void * const chunk) const -{ - // We have to find which storage this chunk is from. - details::PODptr iter = list; - while (iter.valid()) - { - if (is_from(chunk, iter.begin(), iter.element_size())) - return iter; - iter = iter.next(); - } - - return iter; -} - -} // namespace boost - -#endif diff --git a/src/sat/cryptominisat2/poolfwd.hpp b/src/sat/cryptominisat2/poolfwd.hpp deleted file mode 100644 index 52964f7..0000000 --- a/src/sat/cryptominisat2/poolfwd.hpp +++ /dev/null @@ -1,70 +0,0 @@ -// Copyright (C) 2000, 2001 Stephen Cleary -// -// Distributed under the Boost Software License, Version 1.0. (See -// accompanying file LICENSE_1_0.txt or copy at -// http://www.boost.org/LICENSE_1_0.txt) -// -// See http://www.boost.org for updates, documentation, and revision history. - -#ifndef BOOST_POOLFWD_HPP -#define BOOST_POOLFWD_HPP - -#include // for workarounds - -// std::size_t -#include - -// boost::details::pool::default_mutex -//#include - -namespace boost { - -// -// Location: -// -template -class simple_segregated_storage; - -// -// Location: -// -struct default_user_allocator_new_delete; -struct default_user_allocator_malloc_free; - -template -class pool; - -// -// Location: -// -template -class object_pool; - -// -// Location: -// -template -struct singleton_pool; - -// -// Location: -// -struct pool_allocator_tag; - -template -class pool_allocator; - -struct fast_pool_allocator_tag; - -template -class fast_pool_allocator; - -} // namespace boost - -#endif diff --git a/src/sat/cryptominisat2/singleton.hpp b/src/sat/cryptominisat2/singleton.hpp deleted file mode 100644 index db7ca67..0000000 --- a/src/sat/cryptominisat2/singleton.hpp +++ /dev/null @@ -1,107 +0,0 @@ -// Copyright (C) 2000 Stephen Cleary -// -// Distributed under the Boost Software License, Version 1.0. (See -// accompanying file LICENSE_1_0.txt or copy at -// http://www.boost.org/LICENSE_1_0.txt) -// -// See http://www.boost.org for updates, documentation, and revision history. - -#ifndef BOOST_POOL_SINGLETON_HPP -#define BOOST_POOL_SINGLETON_HPP - -// The following code might be put into some Boost.Config header in a later revision -#ifdef __BORLANDC__ -# pragma option push -w-inl -#endif - -// -// The following helper classes are placeholders for a generic "singleton" -// class. The classes below support usage of singletons, including use in -// program startup/shutdown code, AS LONG AS there is only one thread -// running before main() begins, and only one thread running after main() -// exits. -// -// This class is also limited in that it can only provide singleton usage for -// classes with default constructors. -// - -// The design of this class is somewhat twisted, but can be followed by the -// calling inheritance. Let us assume that there is some user code that -// calls "singleton_default::instance()". The following (convoluted) -// sequence ensures that the same function will be called before main(): -// instance() contains a call to create_object.do_nothing() -// Thus, object_creator is implicitly instantiated, and create_object -// must exist. -// Since create_object is a static member, its constructor must be -// called before main(). -// The constructor contains a call to instance(), thus ensuring that -// instance() will be called before main(). -// The first time instance() is called (i.e., before main()) is the -// latest point in program execution where the object of type T -// can be created. -// Thus, any call to instance() will auto-magically result in a call to -// instance() before main(), unless already present. -// Furthermore, since the instance() function contains the object, instead -// of the singleton_default class containing a static instance of the -// object, that object is guaranteed to be constructed (at the latest) in -// the first call to instance(). This permits calls to instance() from -// static code, even if that code is called before the file-scope objects -// in this file have been initialized. - -namespace boost { - -namespace details { -namespace pool { - -// T must be: no-throw default constructible and no-throw destructible -template -struct singleton_default -{ - private: - struct object_creator - { - // This constructor does nothing more than ensure that instance() - // is called before main() begins, thus creating the static - // T object before multithreading race issues can come up. - object_creator() { singleton_default::instance(); } - inline void do_nothing() const { } - }; - static object_creator create_object; - - singleton_default(); - - public: - typedef T object_type; - - // If, at any point (in user code), singleton_default::instance() - // is called, then the following function is instantiated. - static object_type & instance() - { - // This is the object that we return a reference to. - // It is guaranteed to be created before main() begins because of - // the next line. - static object_type obj; - - // The following line does nothing else than force the instantiation - // of singleton_default::create_object, whose constructor is - // called before main() begins. - create_object.do_nothing(); - - return obj; - } -}; -template -typename singleton_default::object_creator -singleton_default::create_object; - -} // namespace pool -} // namespace details - -} // namespace boost - -// The following code might be put into some Boost.Config header in a later revision -#ifdef __BORLANDC__ -# pragma option pop -#endif - -#endif -- 2.47.3