diff options
Diffstat (limited to 'src/prop/cryptominisat/Solver/ClauseAllocator.cpp')
-rw-r--r-- | src/prop/cryptominisat/Solver/ClauseAllocator.cpp | 572 |
1 files changed, 572 insertions, 0 deletions
diff --git a/src/prop/cryptominisat/Solver/ClauseAllocator.cpp b/src/prop/cryptominisat/Solver/ClauseAllocator.cpp new file mode 100644 index 000000000..f1576e7fe --- /dev/null +++ b/src/prop/cryptominisat/Solver/ClauseAllocator.cpp @@ -0,0 +1,572 @@ +/*********************************************************************** +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 <http://www.gnu.org/licenses/>. +************************************************************************/ + +#include "ClauseAllocator.h" + +#include <string.h> +#include <limits> +#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 "Gaussian.h" + +#ifndef _MSC_VER +#include <sys/mman.h> +#endif //_MSC_VER + + +//For mild debug info: +//#define DEBUG_CLAUSEALLOCATOR + +//For listing each and every clause location: +//#define DEBUG_CLAUSEALLOCATOR2 + +#define MIN_LIST_SIZE (300000 * (sizeof(Clause) + 4*sizeof(Lit))/sizeof(BASE_DATA_TYPE)) +//#define MIN_LIST_SIZE (100 * (sizeof(Clause) + 4*sizeof(Lit))/sizeof(BASE_DATA_TYPE)) +#define ALLOC_GROW_MULT 8 +//We shift stuff around in Watched, so not all of 32 bits are useable. +#define EFFECTIVELY_USEABLE_BITS 30 +#define MAXSIZE ((1 << (EFFECTIVELY_USEABLE_BITS-NUM_BITS_OUTER_OFFSET))-1) + +using namespace CMSat; + +ClauseAllocator::ClauseAllocator() +{ + assert(MIN_LIST_SIZE < MAXSIZE); + assert(sizeof(Clause) + 2*sizeof(Lit) >= sizeof(NewPointerAndOffset)); +} + +/** +@brief Frees all stacks +*/ +ClauseAllocator::~ClauseAllocator() +{ + for (uint32_t i = 0; i < dataStarts.size(); i++) { + free(dataStarts[i]); + } +} + +/** +@brief Allocates space&initializes a clause +*/ +template<class T> +Clause* ClauseAllocator::Clause_new(const T& ps, const bool learnt) +{ + assert(ps.size() > 2); + void* mem = allocEnough(ps.size()); + Clause* real= new (mem) Clause(ps, learnt); + //assert(!(ps.size() == 2 && !real->wasBin())); + + return real; +} + +template Clause* ClauseAllocator::Clause_new(const vec<Lit>& ps, const bool learnt); +template Clause* ClauseAllocator::Clause_new(const Clause& ps, const bool learnt); +template Clause* ClauseAllocator::Clause_new(const XorClause& ps, const bool learnt); + +/** +@brief Allocates space&initializes an xor clause +*/ +template<class T> +XorClause* ClauseAllocator::XorClause_new(const T& ps, const bool xorEqualFalse) +{ + assert(ps.size() > 2); + void* mem = allocEnough(ps.size()); + XorClause* real= new (mem) XorClause(ps, xorEqualFalse); + + return real; +} +template XorClause* ClauseAllocator::XorClause_new(const vec<Lit>& ps, const bool inverted); +template XorClause* ClauseAllocator::XorClause_new(const XorClause& ps, const bool inverted); + +/** +@brief Allocates space for a new clause & copies a give clause to it +*/ +Clause* ClauseAllocator::Clause_new(Clause& c) +{ + assert(c.size() > 2); + void* mem = allocEnough(c.size()); + memcpy(mem, &c, sizeof(Clause)+sizeof(Lit)*c.size()); + + return (Clause*)mem; +} + +/** +@brief Allocates enough space for a new clause + +It tries to add the clause to the end of any already created stacks +if that is impossible, it creates a new stack, and adds the clause there +*/ +void* ClauseAllocator::allocEnough(const uint32_t size) throw (std::bad_alloc) +{ + assert(sizes.size() == dataStarts.size()); + assert(maxSizes.size() == dataStarts.size()); + assert(origClauseSizes.size() == dataStarts.size()); + + assert(size > 2 && "Clause size cannot be 2 or less, those are stored natively"); + + const uint32_t needed = sizeof(Clause) + sizeof(Lit)*size; + bool found = false; + uint32_t which = std::numeric_limits<uint32_t>::max(); + for (uint32_t i = 0; i < sizes.size(); i++) { + if (sizes[i] + needed < maxSizes[i]) { + found = true; + which = i; + break; + } + } + + if (!found) { + //Checking whether we are out of memory, because the offset that we can + //store is too little + if (dataStarts.size() == (1<<NUM_BITS_OUTER_OFFSET)) + throw std::bad_alloc(); + + uint32_t nextSize; //number of BYTES to allocate + if (maxSizes.size() != 0) { + nextSize = std::min((uint32_t)(maxSizes[maxSizes.size()-1]*ALLOC_GROW_MULT), (uint32_t)MAXSIZE); + nextSize = std::max(nextSize, (uint32_t)MIN_LIST_SIZE*2); + } else { + nextSize = (uint32_t)MIN_LIST_SIZE; + } + assert(needed < nextSize); + assert(nextSize <= MAXSIZE); + + #ifdef DEBUG_CLAUSEALLOCATOR + std::cout << "c New list in ClauseAllocator. Size: " << nextSize + << " (maxSize: " << MAXSIZE + << ")" << std::endl; + #endif //DEBUG_CLAUSEALLOCATOR + + BASE_DATA_TYPE *dataStart; + dataStart = (BASE_DATA_TYPE *)malloc(sizeof(BASE_DATA_TYPE) * nextSize); + + dataStarts.push(dataStart); + sizes.push(0); + maxSizes.push(nextSize); + origClauseSizes.push(); + currentlyUsedSizes.push(0); + which = dataStarts.size()-1; + } + #ifdef DEBUG_CLAUSEALLOCATOR2 + std::cout + << "selected list = " << which + << " size = " << sizes[which] + << " maxsize = " << maxSizes[which] + << " diff = " << maxSizes[which] - sizes[which] << std::endl; + #endif //DEBUG_CLAUSEALLOCATOR + + assert(which != std::numeric_limits<uint32_t>::max()); + Clause* pointer = (Clause*)(dataStarts[which] + sizes[which]); + sizes[which] += needed; + currentlyUsedSizes[which] += needed; + origClauseSizes[which].push(needed); + + return pointer; +} + +/** +@brief Given the pointer of the clause it finds a 32-bit offset for it + +Calculates the stack frame and the position of the pointer in the stack, and +rerturns a 32-bit value that is a concatenation of these two +*/ +ClauseOffset ClauseAllocator::getOffset(const Clause* ptr) const +{ + uint32_t outerOffset = getOuterOffset(ptr); + uint32_t interOffset = getInterOffset(ptr, outerOffset); + return combineOuterInterOffsets(outerOffset, interOffset); +} + +/** +@brief Combines the stack number and the internal offset into one 32-bit number +*/ +inline ClauseOffset ClauseAllocator::combineOuterInterOffsets(const uint32_t outerOffset, const uint32_t interOffset) const +{ + return (outerOffset | (interOffset << NUM_BITS_OUTER_OFFSET)); +} + +/** +@brief Given a pointer, finds which stack it's in +*/ +inline uint32_t ClauseAllocator::getOuterOffset(const Clause* ptr) const +{ + uint32_t which = std::numeric_limits<uint32_t>::max(); + for (uint32_t i = 0; i < sizes.size(); i++) { + if ((BASE_DATA_TYPE*)ptr >= dataStarts[i] && (BASE_DATA_TYPE*)ptr < dataStarts[i] + maxSizes[i]) { + which = i; + break; + } + } + assert(which != std::numeric_limits<uint32_t>::max()); + + return which; +} + +/** +@brief Given a pointer and its stack number, returns its position inside the stack +*/ +inline uint32_t ClauseAllocator::getInterOffset(const Clause* ptr, uint32_t outerOffset) const +{ + return ((BASE_DATA_TYPE*)ptr - dataStarts[outerOffset]); +} + +/** +@brief Frees a clause + +If clause was binary, it frees it in quite a normal way. If it isn't, then it +needs to set the data in the Clause that it has been freed, and updates the +stack it belongs to such that the stack can now that its effectively used size +is smaller + +NOTE: The size of claues can change. Therefore, currentlyUsedSizes can in fact +be incorrect, since it was incremented by the ORIGINAL size of the clause, but +when the clause is "freed", it is decremented by the POTENTIALLY SMALLER size +of the clause. Therefore, the "currentlyUsedSizes" is an overestimation!! +*/ +void ClauseAllocator::clauseFree(Clause* c) +{ + assert(!c->getFreed()); + + c->setFreed(); + uint32_t outerOffset = getOuterOffset(c); + //uint32_t interOffset = getInterOffset(c, outerOffset); + currentlyUsedSizes[outerOffset] -= sizeof(Clause) + c->size()*sizeof(Lit); + //above should be + //origClauseSizes[outerOffset][interOffset] + //but it cannot be :( +} + +/** +@brief If needed, compacts stacks, removing unused clauses + +Firstly, the algorithm determines if the number of useless slots is large or +small compared to the problem size. If it is small, it does nothing. If it is +large, then it allocates new stacks, copies the non-freed clauses to these new +stacks, updates all pointers and offsets, and frees the original stacks. +*/ +void ClauseAllocator::consolidate(Solver* solver, const bool force) throw (std::bad_alloc) +{ + double myTime = cpuTime(); + #ifdef DEBUG_PROPAGATEFROM + checkGoodPropBy(solver); + #endif + + uint32_t sum = 0; + for (uint32_t i = 0; i < sizes.size(); i++) { + sum += currentlyUsedSizes[i]; + } + uint32_t sumAlloc = 0; + for (uint32_t i = 0; i < sizes.size(); i++) { + sumAlloc += sizes[i]; + } + + #ifdef DEBUG_CLAUSEALLOCATOR + std::cout << "c ratio:" << (double)sum/(double)sumAlloc << std::endl; + #endif //DEBUG_CLAUSEALLOCATOR + + //If re-allocation is not really neccessary, don't do it + //Neccesities: + //1) There is too much memory allocated. Re-allocation will save space + // Avoiding segfault (max is 16 outerOffsets, more than 10 is near) + //2) There is too much empty, unused space (>30%) + if (!force + && ((double)sum/(double)sumAlloc > 0.7 && sizes.size() < 10) + ) { + if (solver->conf.verbosity >= 3) { + std::cout << "c Not consolidating memory." << std::endl; + } + return; + } + + #ifdef DEBUG_CLAUSEALLOCATOR + std::cout << "c ------ Consolidating Memory ------------" << std::endl; + #endif //DEBUG_CLAUSEALLOCATOR + int64_t newMaxSizeNeed = (double)sum*1.2 + MIN_LIST_SIZE; + #ifdef DEBUG_CLAUSEALLOCATOR + std::cout << "c newMaxSizeNeed = " << newMaxSizeNeed << std::endl; + #endif //DEBUG_CLAUSEALLOCATOR + vec<uint32_t> newMaxSizes; + for (uint32_t i = 0; i < (1 << NUM_BITS_OUTER_OFFSET); i++) { + if (newMaxSizeNeed <= 0) break; + + uint32_t thisMaxSize = std::min(newMaxSizeNeed, (int64_t)MAXSIZE); + if (i == 0) { + thisMaxSize = std::max(thisMaxSize, (uint32_t)MIN_LIST_SIZE); + } else { + assert(i > 0); + thisMaxSize = std::max(thisMaxSize, newMaxSizes[i-1]/2); + thisMaxSize = std::max(thisMaxSize, (uint32_t)MIN_LIST_SIZE*2); + } + newMaxSizeNeed -= thisMaxSize; + assert(thisMaxSize <= MAXSIZE); + newMaxSizes.push(thisMaxSize); + //because the clauses don't always fit + //it might occur that there is enough place in total + //but the very last clause would need to be fragmented + //over multiple lists' ends :O + //So this "magic" constant could take care of that.... + //or maybe not (if _very_ large clauses are used, always + //bad chance, etc. :O ) + //NOTE: the + MIN_LIST_SIZE should take care of this above at + // newMaxSizeNeed = sum + MIN_LIST_SIZE; + #ifdef DEBUG_CLAUSEALLOCATOR + std::cout << "c NEW MaxSizes:" << newMaxSizes[i] << std::endl; + #endif //DEBUG_CLAUSEALLOCATOR + } + #ifdef DEBUG_CLAUSEALLOCATOR + std::cout << "c ------------------" << std::endl; + #endif //DEBUG_CLAUSEALLOCATOR + + if (newMaxSizeNeed > 0) + throw std::bad_alloc(); + + vec<uint32_t> newSizes; + vec<vec<uint32_t> > newOrigClauseSizes; + vec<BASE_DATA_TYPE*> newDataStartsPointers; + vec<BASE_DATA_TYPE*> newDataStarts; + for (uint32_t i = 0; i < newMaxSizes.size(); i++) { + newSizes.push(0); + newOrigClauseSizes.push(); + BASE_DATA_TYPE* pointer; + pointer = (BASE_DATA_TYPE*)malloc(newMaxSizes[i]); + newDataStartsPointers.push(pointer); + newDataStarts.push(pointer); + } + + vector<Clause*> clauses; + 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->getFreed()) { + clauses.push_back(oldPointer); + } else { + (*((NewPointerAndOffset*)(oldPointer))).newOffset = std::numeric_limits<uint32_t>::max(); + } + currentLoc += origClauseSizes[i][i2]; + } + } + + putClausesIntoDatastruct(clauses); + + uint32_t outerPart = 0; + //uint64_t skippedNum = 0; + for (uint32_t i = 0; i < clauses.size(); i++) { + Clause* clause = getClause(); + + uint32_t sizeNeeded = (sizeof(Clause) + clause->size()*sizeof(Lit))/sizeof(BASE_DATA_TYPE); + + //Next line is needed, because in case of isRemoved() + //, the size of the clause could become 0, thus having less + // than enough space to carry the NewPointerAndOffset info + sizeNeeded = std::max(sizeNeeded, (uint32_t)((sizeof(Clause) + 2*sizeof(Lit))/sizeof(BASE_DATA_TYPE))); + + if (newSizes[outerPart] + sizeNeeded > newMaxSizes[outerPart]) { + outerPart++; + assert(outerPart < newMaxSizes.size()); + } + memcpy(newDataStartsPointers[outerPart], (BASE_DATA_TYPE*)clause, sizeNeeded*sizeof(BASE_DATA_TYPE)); + + NewPointerAndOffset& ptr = *((NewPointerAndOffset*)clause); + ptr.newOffset = combineOuterInterOffsets(outerPart, newSizes[outerPart]); + ptr.newPointer = (Clause*)newDataStartsPointers[outerPart]; + + newSizes[outerPart] += sizeNeeded; + newOrigClauseSizes[outerPart].push(sizeNeeded); + newDataStartsPointers[outerPart] += sizeNeeded; + } + + updateAllOffsetsAndPointers(solver); + + for (uint32_t i = 0; i < dataStarts.size(); i++) + free(dataStarts[i]); + + dataStarts.clear(); + maxSizes.clear(); + sizes.clear(); + origClauseSizes.clear(); + currentlyUsedSizes.clear(); + origClauseSizes.clear(); + + for (uint32_t i = 0; i < newMaxSizes.size(); i++) { + dataStarts.push(newDataStarts[i]); + maxSizes.push(newMaxSizes[i]); + sizes.push(newSizes[i]); + currentlyUsedSizes.push(newSizes[i]); + } + newOrigClauseSizes.moveTo(origClauseSizes); + + if (solver->conf.verbosity >= 3) { + std::cout << "c Consolidated memory. Time: " + << cpuTime() - myTime << std::endl; + } +} + +void ClauseAllocator::putClausesIntoDatastruct(std::vector<Clause*>& clauses) +{ + otherClauses.clear(); + threeLongClauses.clear(); + for (uint32_t i = 0; i < clauses.size(); i++) { + Clause* c = clauses[i]; + if (c->size() <= 3) { + threeLongClauses.push_back(c); + } else { + otherClauses.push_back(c); + } + } +} + +Clause* ClauseAllocator::getClause() +{ + if (!threeLongClauses.empty()) { + Clause* tmp = threeLongClauses[threeLongClauses.size()-1]; + threeLongClauses.pop_back(); + return tmp; + } + + assert(!otherClauses.empty()); + Clause* tmp = otherClauses[otherClauses.size()-1]; + otherClauses.pop_back(); + return tmp; +} + +void ClauseAllocator::checkGoodPropBy(const Solver* solver) +{ + const vec<PropBy>& reason = solver->reason; + Var var = 0; + for (const PropBy *it = reason.getData(), *end = reason.getDataEnd(); it != end; it++, var++) { + if ((uint32_t)solver->level[var] > solver->decisionLevel() + || solver->level[var] == 0 + || solver->value(var) == l_Undef + ) { + continue; + } + + if (it->isClause() && !it->isNULL()) { + assert(!getPointer(it->getClause())->getFreed()); + assert(!getPointer(it->getClause())->getRemoved()); + } + } +} + + +void ClauseAllocator::updateAllOffsetsAndPointers(Solver* solver) +{ + updateOffsets(solver->watches); + + updatePointers(solver->clauses); + updatePointers(solver->learnts); + updatePointers(solver->xorclauses); + updatePointers(solver->freeLater); + #ifdef ENABLE_UNWIND_GLUE + updatePointers(solver->unWindGlue); + #endif //ENABLE_UNWIND_GLUE + + //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); + + #ifdef USE_GAUSS + for (uint32_t i = 0; i < solver->gauss_matrixes.size(); i++) { + updatePointers(solver->gauss_matrixes[i]->xorclauses); + updatePointers(solver->gauss_matrixes[i]->clauses_toclear); + } + #endif //USE_GAUSS + + vec<PropBy>& reason = solver->reason; + Var var = 0; + for (PropBy *it = reason.getData(), *end = reason.getDataEnd(); it != end; it++, var++) { + if ((uint32_t)solver->level[var] > solver->decisionLevel() + || solver->level[var] == 0 + || solver->value(var) == l_Undef) { + *it = PropBy(); + continue; + } + + if (it->isClause() && !it->isNULL()) { + assert(((NewPointerAndOffset*)(getPointer(it->getClause())))->newOffset != std::numeric_limits<uint32_t>::max()); + *it = PropBy(((NewPointerAndOffset*)(getPointer(it->getClause())))->newOffset); + } + } +} + +/** +@brief A dumb helper function to update offsets +*/ +void ClauseAllocator::updateOffsets(vec<vec<Watched> >& watches) +{ + for (uint32_t i = 0; i < watches.size(); i++) { + vec<Watched>& list = watches[i]; + for (vec<Watched>::iterator it = list.getData(), end = list.getDataEnd(); it != end; it++) { + if (!it->isClause() && !it->isXorClause()) continue; + if (it->isClause()) { + it->setNormOffset(((NewPointerAndOffset*)(getPointer(it->getNormOffset())))->newOffset); + } else { + it->setXorOffset(((NewPointerAndOffset*)(getPointer(it->getXorOffset())))->newOffset); + } + } + } +} + +/** +@brief A dumb helper function to update pointers +*/ +template<class T> +void ClauseAllocator::updatePointers(vec<T*>& toUpdate) +{ + for (T **it = toUpdate.getData(), **end = toUpdate.getDataEnd(); it != end; it++) { + if (*it != NULL) { + *it = (T*)(((NewPointerAndOffset*)(*it))->newPointer); + } + } +} + +/** +@brief A dumb helper function to update pointers +*/ +void ClauseAllocator::updatePointers(vector<Clause*>& toUpdate) +{ + for (vector<Clause*>::iterator it = toUpdate.begin(), end = toUpdate.end(); it != end; it++) { + *it = (((NewPointerAndOffset*)(*it))->newPointer); + } +} + +/** +@brief A dumb helper function to update pointers +*/ +void ClauseAllocator::updatePointers(vector<XorClause*>& toUpdate) +{ + for (vector<XorClause*>::iterator it = toUpdate.begin(), end = toUpdate.end(); it != end; it++) { + *it = (XorClause*)(((NewPointerAndOffset*)(*it))->newPointer); + } +} + +/** +@brief A dumb helper function to update pointers +*/ +void ClauseAllocator::updatePointers(vector<pair<Clause*, uint32_t> >& toUpdate) +{ + for (vector<pair<Clause*, uint32_t> >::iterator it = toUpdate.begin(), end = toUpdate.end(); it != end; it++) { + it->first = (((NewPointerAndOffset*)(it->first))->newPointer); + } +} |