class Clause;
-template <class T>
-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
}
};
+#endif //CSET_H
+
}; //NAMESPACE MINISAT
-#endif //CSET_H
\ No newline at end of file
#ifdef _MSC_VER
#include <msvc/stdint.h>
#else
-#include "SmallPtr.h"
#include <stdint.h>
#endif //_MSC_VER
+
#include <cstdio>
#include <vector>
#include <sys/types.h>
#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 <class T>
+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
{
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;
template<class V>
Clause(const V& ps, const uint _group, const bool learnt)
{
+ wasBinInternal = (ps.size() == 2);
+ isFreed = false;
isXorClause = false;
strenghtened = false;
sorted = false;
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<class T>
- 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;
return oldActivityInter;
}
-
const bool getStrenghtened() const {
return strenghtened;
}
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;
}
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;
{
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 {
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<class V>
XorClause(const V& ps, const bool inverted, const uint _group) :
}
public:
- #ifndef _MSC_VER
- // -- use this function instead:
- template<class V>
- 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
{
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<class T>
-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<class T>
-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<class T>
-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<Clause> ClausePtr;
-typedef sptr<XorClause> 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)
--- /dev/null
+/***********************************************************************
+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 "PartHandler.h"
+
+namespace MINISAT
+{
+using namespace MINISAT;
+
+ClauseAllocator::ClauseAllocator() :
+ clausePoolBin(sizeof(Clause) + 2*sizeof(Lit))
+{}
+
+template<class T>
+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<Lit>& 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<class T>
+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<Lit>& 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<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) {
+ //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<uint32_t>::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<uint32_t>::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<uint32_t>::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<uint32_t> newOrigClauseSizes;
+ //}
+
+ map<Clause*, Clause*> oldToNewPointer;
+ map<uint32_t, uint32_t> 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<Var, vector<Clause*> >::iterator it = solver->subsumer->elimedOutVar.begin(); it != solver->subsumer->elimedOutVar.end(); it++) {
+ updatePointers(it->second, oldToNewPointer);
+ }
+ for(map<Var, vector<XorClause*> >::iterator it = solver->xorSubsumer->elimedOutVar.begin(); it != solver->xorSubsumer->elimedOutVar.end(); it++) {
+ updatePointers(it->second, oldToNewPointer);
+ }
+
+
+ vec<PropagatedFrom>& 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<class T>
+void ClauseAllocator::updateOffsets(vec<vec<T> >& watches, const map<ClauseOffset, ClauseOffset>& oldToNewOffset)
+{
+ for (uint32_t i = 0; i < watches.size(); i++) {
+ vec<T>& list = watches[i];
+ for (T *it = list.getData(), *end = list.getDataEnd(); it != end; it++) {
+ map<ClauseOffset, ClauseOffset>::const_iterator it2 = oldToNewOffset.find(it->clause);
+ assert(it2 != oldToNewOffset.end());
+ it->clause = it2->second;
+ }
+ }
+}
+
+template<class T>
+void ClauseAllocator::updateOffsetsXor(vec<vec<T> >& watches, const map<ClauseOffset, ClauseOffset>& oldToNewOffset)
+{
+ for (uint32_t i = 0; i < watches.size(); i++) {
+ vec<T>& list = watches[i];
+ for (T *it = list.getData(), *end = list.getDataEnd(); it != end; it++) {
+ map<ClauseOffset, ClauseOffset>::const_iterator it2 = oldToNewOffset.find(*it);
+ assert(it2 != oldToNewOffset.end());
+ *it = it2->second;
+ }
+ }
+}
+
+template<class T>
+void ClauseAllocator::updatePointers(vec<T*>& toUpdate, const map<Clause*, Clause*>& oldToNewPointer)
+{
+ for (T **it = toUpdate.getData(), **end = toUpdate.getDataEnd(); it != end; it++) {
+ if (!(*it)->wasBin()) {
+ //assert(oldToNewPointer.find((TT*)*it) != oldToNewPointer.end());
+ map<Clause*, Clause*>::const_iterator it2 = oldToNewPointer.find((Clause*)*it);
+ *it = (T*)it2->second;
+ }
+ }
+}
+
+void ClauseAllocator::updatePointers(vector<Clause*>& toUpdate, const map<Clause*, Clause*>& oldToNewPointer)
+{
+ for (vector<Clause*>::iterator it = toUpdate.begin(), end = toUpdate.end(); it != end; it++) {
+ if (!(*it)->wasBin()) {
+ //assert(oldToNewPointer.find((TT*)*it) != oldToNewPointer.end());
+ map<Clause*, Clause*>::const_iterator it2 = oldToNewPointer.find((Clause*)*it);
+ *it = it2->second;
+ }
+ }
+}
+
+void ClauseAllocator::updatePointers(vector<XorClause*>& toUpdate, const map<Clause*, Clause*>& oldToNewPointer)
+{
+ for (vector<XorClause*>::iterator it = toUpdate.begin(), end = toUpdate.end(); it != end; it++) {
+ if (!(*it)->wasBin()) {
+ //assert(oldToNewPointer.find((TT*)*it) != oldToNewPointer.end());
+ map<Clause*, Clause*>::const_iterator it2 = oldToNewPointer.find((Clause*)*it);
+ *it = (XorClause*)it2->second;
+ }
+ }
+}
+
+}; //NAMESPACE MINISAT
--- /dev/null
+/***********************************************************************
+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/>.
+************************************************************************/
+
+#ifndef CLAUSEALLOCATOR_H
+#define CLAUSEALLOCATOR_H
+
+#ifdef _MSC_VER
+#include <msvc/stdint.h>
+#else
+#include <stdint.h>
+#endif //_MSC_VER
+
+#include "Vec.h"
+#include <boost/pool/pool.hpp>
+#include <map>
+#include <vector>
+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<class T>
+ Clause* Clause_new(const T& ps, const uint group, const bool learnt = false);
+ template<class T>
+ 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<class T>
+ void updatePointers(vec<T*>& toUpdate, const map<Clause*, Clause*>& oldToNewPointer);
+ void updatePointers(vector<Clause*>& toUpdate, const map<Clause*, Clause*>& oldToNewPointer);
+ void updatePointers(vector<XorClause*>& toUpdate, const map<Clause*, Clause*>& oldToNewPointer);
+
+ template<class T>
+ void updateOffsets(vec<vec<T> >& watches, const map<ClauseOffset, ClauseOffset>& oldToNewOffset);
+ template<class T>
+ void updateOffsetsXor(vec<vec<T> >& watches, const map<ClauseOffset, ClauseOffset>& oldToNewOffset);
+
+ vec<uint32_t*> dataStarts;
+ vec<size_t> sizes;
+ vec<vec<uint32_t> > origClauseSizes;
+ vec<size_t> maxSizes;
+ vec<size_t> currentlyUsedSize;
+ vec<uint32_t> origSizes;
+
+ boost::pool<> clausePoolBin;
+
+ void* allocEnough(const uint32_t size);
+};
+
+}; //NAMESPACE MINISAT
+
+#endif //CLAUSEALLOCATOR_H
+
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);
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) {
}
if (val == l_True) {
- subs.unlinkModifiedClause(origClause, cc);
- clauseFree(cc.clause);
+ subs.unlinkModifiedClause(origClause, cc, true);
+ solver.clauseAllocator.clauseFree(cc.clause);
return true;
}
}
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);
}
switch(c.size()) {
case 0: {
subs.unlinkModifiedClause(origClause, cc);
- clauseFree(cc.clause);
+ solver.clauseAllocator.clauseFree(cc.clause);
return true;
}
case 2: {
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:
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);
+++ /dev/null
-/***********************************************************************************
-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 "Conglomerate.h"
-#include "VarReplacer.h"
-#include "ClauseCleaner.h"
-
-#include <utility>
-#include <algorithm>
-#include <cstring>
-#include "time_mem.h"
-#include <iomanip>
-using std::make_pair;
-
-//#define VERBOSE_DEBUG
-
-#ifdef VERBOSE_DEBUG
-#include <iostream>
-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<Clause*>& 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<pair<XorClause*, uint32_t> >::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<vector<Lit> >& newSet, vector<pair<XorClause*, uint32_t> >& 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<vector<Lit> > newSet;
- while(varToXor.begin() != varToXor.end()) {
- varToXorMap::iterator it = varToXor.begin();
- vector<pair<XorClause*, uint32_t> >& 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<vector<Lit> > newSet;
- while(varToXor.begin() != varToXor.end()) {
- varToXorMap::iterator it = varToXor.begin();
- vector<pair<XorClause*, uint32_t> >& 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<Lit>& 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<Lit> 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<Lit>& 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<Lit> 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
+++ /dev/null
-/***********************************************************************************
-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/>.
-**************************************************************************************************/
-
-#ifndef CONGLOMERATE_H
-#define CONGLOMERATE_H
-
-#include <vector>
-#include <map>
-#include <set>
-#ifdef _MSC_VER
-#include <msvc/stdint.h>
-#else
-#include <stdint.h>
-#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(); ///<Add clauses that have been removed. Used if solve() is called multiple times
- void extendModel(Solver& solver2); ///<Calculate variables removed during conglomeration
-
- const vec<XorClause*>& getCalcAtFinish() const;
- vec<XorClause*>& getCalcAtFinish();
- const vec<bool>& getRemovedVars() const;
- const bool needCalcAtFinish() const;
-
- void newVar();
-
-private:
-
- struct ClauseSetSorter {
- bool operator () (const pair<XorClause*, uint32_t>& a, const pair<XorClause*, uint32_t>& b) {
- return a.first->size() < b.first->size();
- }
- };
-
- const bool conglomerateXors();
- const bool heuleProcess();
-
- void fillNewSet(vector<vector<Lit> >& newSet, vector<pair<XorClause*, uint32_t> >& clauseSet) const;
-
- void removeVar(const Var var);
- void processClause(XorClause& x, uint32_t num, Var remove_var);
- void blockVars();
- void fillVarToXor();
- void clearDouble(vector<Lit>& ps) const;
- void clearToRemove();
- void clearLearntsFromToRemove();
- bool dealWithNewClause(vector<Lit>& ps, const bool inverted, const uint old_group);
-
- typedef map<uint, vector<pair<XorClause*, uint32_t> > > varToXorMap;
- varToXorMap varToXor;
- vector<bool> blocked;
- vector<bool> toRemove;
-
- vec<bool> removedVars;
- vec<Var> madeVarNonDecision;
-
- vec<XorClause*> calcAtFinish;
- uint found;
-
- Solver& solver;
-};
-
-inline void Conglomerate::newVar()
-{
- removedVars.push(false);
-}
-
-inline const vec<bool>& Conglomerate::getRemovedVars() const
-{
- return removedVars;
-}
-
-inline const vec<XorClause*>& Conglomerate::getCalcAtFinish() const
-{
- return calcAtFinish;
-}
-
-inline vec<XorClause*>& Conglomerate::getCalcAtFinish()
-{
- return calcAtFinish;
-}
-
-inline const bool Conglomerate::needCalcAtFinish() const
-{
- return calcAtFinish.size();
-}
-
-}; //NAMESPACE MINISAT
-
-#endif //CONGLOMERATE_H
Heap<Solver::VarOrderLt> 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;
}
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;
}
}
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;
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;
}
}
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<bool startUp>
-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<startUp>(lit)) {
- fixed = true;
- solver.cancelUntil(0);
- solver.uncheckedEnqueue(~lit);
- solver.ok = (solver.propagate() == NULL);
- if (!solver.ok) return false;
- continue;
- }
-
- lit = ~lit;
- if (!removeUselessBinaries<startUp>(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;
}
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 {
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 {
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;
solver.newDecisionLevel();
solver.uncheckedEnqueueLight(lit);
- failed = (solver.propagateBin() != NULL);
+ failed = (!solver.propagateBin().isNULL());
assert(!failed);
assert(solver.decisionLevel() > 0);
{
solver.newDecisionLevel();
solver.uncheckedEnqueue(lit);
- failed = (solver.propagateLight() != NULL);
+ failed = (!solver.propagate().isNULL());
assert(!failed);
assert(solver.decisionLevel() > 0);
solver.cancelUntil(0);
}
-template<bool startUp>
-const bool FailedVarSearcher::fillBinImpliesMinusLast(const Lit& origLit, const Lit& lit, vec<Lit>& wrong)
-{
- solver.newDecisionLevel();
- solver.uncheckedEnqueueLight(lit);
- //if it's a cycle, it doesn't work, so don't propagate origLit
- failed = (solver.propagateBinExcept<startUp>(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
assert(solver.ok);
}
-template<bool startUp>
-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<startUp>() != 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<startUp>(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 <true>(const Lit& lit);
-template const bool FailedVarSearcher::removeUselessBinaries <false>(const Lit& lit);
-template const bool FailedVarSearcher::fillBinImpliesMinusLast <true>(const Lit& origLit, const Lit& lit, vec<Lit>& wrong);
-template const bool FailedVarSearcher::fillBinImpliesMinusLast <false>(const Lit& origLit, const Lit& lit, vec<Lit>& wrong);
-template const bool FailedVarSearcher::removeUslessBinFull <true>();
-template const bool FailedVarSearcher::removeUslessBinFull <false>();
-
-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<WatchedBin>& 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<WatchedBin>& 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<class T>
inline void FailedVarSearcher::cleanAndAttachClauses(vec<T*>& cs)
{
solver.attachClause(**i);
*j++ = *i;
} else {
- clauseFree(*i);
+ solver.clauseAllocator.clauseFree(*i);
}
}
cs.shrink(i-j);
FailedVarSearcher(Solver& _solver);
const bool search(uint64_t numProps);
- template<bool startUp>
- const bool removeUslessBinFull();
private:
//For 2-long xor
void printResults(const double myTime) const;
Solver& solver;
-
- //Time
- uint32_t extraTime;
//For failure
bool failed;
uint64_t maxHyperBinProps;
uint64_t binClauseAdded;
- //Remove useless binaries
- template<bool startUp>
- const bool fillBinImpliesMinusLast(const Lit& origLit, const Lit& lit, vec<Lit>& wrong);
- template<bool startUp>
- const bool removeUselessBinaries(const Lit& lit);
- void removeBin(const Lit& lit1, const Lit& lit2);
- vec<char> toDeleteSet;
- vec<Lit> oneHopAway;
- vec<Lit> wrong;
-
//Temporaries
vec<Lit> tmpPs;
}; //NAMESPACE MINISAT
-#endif //FAILEDVARSEARCHER_H
\ No newline at end of file
+#endif //FAILEDVARSEARCHER_H
+
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()
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:
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)
#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();
if (cla.size() == 1) {
solver.cancelUntil(0);
solver.uncheckedEnqueue(cla[0]);
- clauseFree(&cla);
+ solver.clauseAllocator.clauseFree(&cla);
return unit_propagation;
}
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;
unit_truths++;
useful_confl++;
if (confl->size() == 0) {
- clauseFree(confl);
+ solver.clauseAllocator.clauseFree(confl);
return l_False;
}
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:
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);
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
--- /dev/null
+/***********************************************************************
+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 "OnlyNonLearntBins.h"
+
+#include <iomanip>
+#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<WatchedBin> & 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<WatchedBin> & 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<WatchedBin> & 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
--- /dev/null
+/***********************************************************************
+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/>.
+************************************************************************/
+
+#ifndef ONLYNONLEARNTBINS_H
+#define ONLYNONLEARNTBINS_H
+
+#include "Solver.h"
+#include <set>
+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<vec<WatchedBin> > binwatches;
+ set<uint64_t> toRemove;
+
+ Solver& solver;
+};
+
+}; //NAMESPACE MINISAT
+
+#endif //ONLYNONLEARNTBINS_H
+
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;
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++;
}
#include "VarReplacer.h"
#include <iostream>
#include <assert.h>
+#include <iomanip>
//#define VERBOSE_DEBUG
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++) {
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++) {
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));
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();
void newVar();
void addSavedState();
void readdRemovedClauses();
+
+ friend class ClauseAllocator;
private:
struct sort_pred {
+++ /dev/null
-/*
-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
+++ /dev/null
-/*
-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 <boost/static_assert.hpp>
-
-#include <cstring>
-#include <stdlib.h>
-#include "singleton.hpp"
-//#include <boost/thread/mutex.hpp>
-//#include <boost/thread/locks.hpp>
-
-#ifdef _MSC_VER
-#include <msvc/stdint.h>
-#else
-#include <stdint.h>
-#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 <exception>
-
-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<<ALIGNMENT_BITS);
- static const uintptr_t ALIGNMENT_MASK = ALIGNMENT - 1;
-
-protected:
- static uintptr_t _seg_map[ALIGNMENT];
- static uintptr_t _segs;
- //static boost::mutex _m;
-
- inline static uintptr_t ptr2seg(uintptr_t p)
- {
- p &= ~0xFFFFFFFFULL; // Keep only high part
- uintptr_t s = _segs;
- uintptr_t i = 0;
- for (; i < s; ++i)
- if (_seg_map[i] == p)
- return i;
-
- // Not found - now we do it the "right" way (mutex and all)
- //boost::lock_guard<boost::mutex> 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 TYPE>
-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<TYPE>& 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<class O>
- sptr(const sptr<O>& o)
- : _ptr(encode(static_cast<TYPE*>(o.get())))
- {
- }
-
- template<class O>
- sptr(const O* p)
- : _ptr(encode(static_cast<const TYPE*>(p)))
- {
- }
-
- sptr<TYPE>& operator=(const sptr<TYPE>& o) throw()
- {
- _ptr = o._ptr;
- return *this;
- }
-
- template<class O>
- sptr<TYPE>& operator=(const sptr<O>& o)
- {
- _ptr = encode(static_cast<const TYPE*>(o.get()));
- return *this;
- }
-
-private:
- inline uint32_t encode(const_native_pointer_type ptr) const
- {
-#ifdef USE64
-
- uintptr_t p = reinterpret_cast<uintptr_t>(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<uint32_t>(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<native_pointer_type>(ptr);
-#else
- return reinterpret_cast<native_pointer_type>(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<class O>
- bool operator==(const sptr<O>& o) const
- {
- return o._ptr == this->_ptr;
- }
-
- operator TYPE*() const { return get(); }
-
- sptr<TYPE>& operator++( )
- {
- inc_sptr(_ptr);
- return *this;
- }
-
- sptr<TYPE> operator++( int )
- {
- sptr<TYPE> p = *this;
- inc_sptr(_ptr);
- return p;
- }
-
- sptr<TYPE>& operator--( )
- {
- dec_sptr(_ptr);
- return *this;
- }
- sptr<TYPE> operator--( int )
- {
- sptr<TYPE> p = *this;
- dec_sptr(_ptr);
- return p;
- }
-
- sptr<TYPE>& operator+=(size_t offset)
- {
- inc_sptr(_ptr, offset);
- return *this;
- }
-
- sptr<TYPE>& operator-=(size_t offset)
- {
- dec_sptr(_ptr, offset);
- return *this;
- }
-
-private:
- uint32_t _ptr;
-};
-
-}; //NAMESPACE MINISAT
-
-#endif
-
#include "PartHandler.h"
#include "XorSubsumer.h"
#include "StateSaver.h"
+#include "UselessBinRemover.h"
+#include "OnlyNonLearntBins.h"
#ifdef USE_GAUSS
#include "Gaussian.h"
, doVarElim (true)
, doSubsume1 (true)
, failedVarSearch (true)
- , readdOldLearnts (false)
, addExtraBins (true)
, removeUselessBins(true)
, regularRemoveUselessBins(true)
, 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)
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;
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);
insertVarOrder(v);
varReplacer->newVar();
- partHandler->newVar();
- subsumer->newVar();
- xorSubsumer->newVar();
+ if (doPartHandler) partHandler->newVar();
+ if (doSubsumption) subsumer->newVar();
+ if (doXorSubsumption) xorSubsumer->newVar();
insertVarOrder(v);
}
case 1: {
uncheckedEnqueue(Lit(ps[0].var(), xor_clause_inverted));
- ok = (propagate() == NULL);
+ ok = (propagate().isNULL());
return NULL;
}
case 2: {
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;
}
}
#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)
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;
}
#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)
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();
}
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();
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();
}
{
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();
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;
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;
}
tallyVotes(xorclauses, votes);
Var i = 0;
+ uint32_t posPolars = 0;
+ uint32_t undecidedPolars = 0;
for (vector<double>::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());
| Effect:
| Will undo part of the trail, upto but not beyond the assumption of the current decision level.
|________________________________________________________________________________________________@*/
-Clause* Solver::analyze(Clause* confl, vec<Lit>& out_learnt, int& out_btlevel, uint32_t &nbLevels, const bool update)
+Clause* Solver::analyze(PropagatedFrom confl, vec<Lit>& out_learnt, int& out_btlevel, uint32_t &nbLevels, const bool update)
{
int pathC = 0;
Lit p = lit_Undef;
- Clause* oldConfl = NULL;
// Generate conflict clause:
//
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) {
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 {
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--;
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();
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();
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;
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);
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;
}
}
-void Solver::uncheckedEnqueue(Lit p, ClausePtr from)
+void Solver::uncheckedEnqueue(const Lit p, const PropagatedFrom& from)
{
#ifdef DEBUG_UNCHECKEDENQUEUE_LEVEL0
| 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
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.
#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]:
// 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 {
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)
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;
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<WatchedBin> & 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<Watched>& 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++];
//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<WatchedBin> & 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<bool dontCareLearnt>
-Clause* Solver::propagateBinExcept(const Lit& exceptLit)
-{
- while (qhead < trail.size()) {
- Lit p = trail[qhead++];
- vec<WatchedBin> & 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 <true>(const Lit& exceptLit);
-template Clause* Solver::propagateBinExcept <false>(const Lit& exceptLit);
-template<bool dontCareLearnt>
-Clause* Solver::propagateBinOneLevel()
-{
- Lit p = trail[qhead];
- vec<WatchedBin> & 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 <true>();
-template Clause* Solver::propagateBinOneLevel <false>();
-
template<class T>
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<XorClausePtr>& ws = xorwatches[p.var()];
- XorClausePtr *i, *j, *end;
+ vec<ClauseOffset>& 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()) {
#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;
}
{
// Did not find watch -- clause is unit under assignment:
- *j++ = &c;
+ *j++ = origClauseOffset;
#ifdef VERBOSE_DEBUG_XOR
cout << "final: " << std::boolalpha << final << " - ";
cout << endl << endl;
#endif
- confl = (Clause*)&c;
+ confl = PropagatedFrom((Clause*)&c);
qhead = trail.size();
// Copy the remaining watches:
while (i < end)
//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];
}
learnts[j++] = learnts[i];
}
learnts.shrink(i - j);
+
+ clauseAllocator.consolidate(this);
}
const vec<Clause*>& Solver::get_learnts() const
#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<Lit>& 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<Lit>& 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");
learnts[i]->print(outfile);
}
}
+
+ end:
fclose(outfile);
}
testAllClauseAttach();
assert(decisionLevel() == 0);
- if (!ok || propagate() != NULL) {
+ if (!ok || !propagate().isNULL()) {
ok = false;
return false;
}
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 {
return l_Nothing;
}
-llbool Solver::handle_conflict(vec<Lit>& learnt_clause, Clause* confl, int& conflictC, const bool update)
+llbool Solver::handle_conflict(vec<Lit>& learnt_clause, PropagatedFrom confl, int& conflictC, const bool update)
{
#ifdef VERBOSE_DEBUG
cout << "Handling conflict: ";
}
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");
}
testAllClauseAttach();
- if (regularRemoveUselessBins
- && !failedVarSearcher->removeUslessBinFull<false>()) {
- 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;
}
if (performReplace && !varReplacer->performReplace()) return;
- if (conflicts == 0 && learnts.size() == 0
- && noLearntBinaries()) {
- if (subsumeWithNonExistBinaries && !subsumer->subsumeWithBinaries(true)) return;
- if (removeUselessBins && !failedVarSearcher->removeUslessBinFull<true>()) 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<true>()) 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;
#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;
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]);
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);
{
#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
class PartHandler;
class RestartTypeChooser;
class StateSaver;
+class UselessBinRemover;
#ifdef VERBOSE_DEBUG
#define DEBUG_UNCHECKEDENQUEUE_LEVEL0
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
{
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
template<class T>
bool addLearntClause(T& ps, const uint group, const uint32_t activity);
template<class T>
- void removeWatchedCl(vec<T> &ws, const Clause *c);
+ void removeWatchedCl(vec<T> &ws, const ClauseOffset c);
template<class T>
- bool findWatchedCl(const vec<T>& ws, const Clause *c) const;
+ bool findWatchedCl(const vec<T>& ws, const ClauseOffset c) const;
template<class T>
- void removeWatchedBinCl(vec<T> &ws, const Clause *c);
+ void removeWatchedBinCl(vec<T> &ws, const Lit impliedLit);
template<class T>
- bool findWatchedBinCl(const vec<T>& ws, const Clause *c) const;
+ void removeWatchedBinClAll(vec<T> &ws, const Lit impliedLit);
+ template<class T>
+ bool findWatchedBinCl(const vec<T>& ws, const Lit impliedLit) const;
// Helper structures:
//
// Solver state:
//
bool ok; // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used!
+ ClauseAllocator clauseAllocator;
vec<Clause*> clauses; // List of problem clauses.
vec<Clause*> binaryClauses; // Binary clauses are regularly moved here
vec<XorClause*> xorclauses; // List of problem xor-clauses. Will be freed
vec<Clause*> learnts; // List of learnt clauses.
- vec<Clause*> removedLearnts; // Clauses that have been learnt, then removed
vec<XorClause*> freeLater; // xor clauses that need to be freed later due to Gauss
vec<uint32_t> 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<vec<Watched> > watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
- vec<vec<XorClausePtr> > xorwatches; // 'xorwatches[var]' is a list of constraints watching var in XOR clauses.
+ vec<vec<ClauseOffset> > xorwatches; // 'xorwatches[var]' is a list of constraints watching var in XOR clauses.
vec<vec<WatchedBin> > binwatches;
vec<lbool> assigns; // The current assignments
vector<bool> polarity; // The preferred polarity of each variable.
vector<bool> decision_var; // Declares if a variable is eligible for selection in the decision heuristic.
vec<Lit> trail; // Assignment stack; stores all assigments made in the order they were made.
vec<uint32_t> trail_lim; // Separator indices for different decision levels in 'trail'.
- vec<ClausePtr> reason; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none.
+ vec<PropagatedFrom> reason; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none.
vec<int32_t> 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<Lit> assumptions; // Current set of assumptions provided to solve by the user.
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<bool dontCareLearnt>
- Clause* propagateBinExcept(const Lit& exceptLit);
+ PropagatedFrom propagateBinExcept(const Lit& exceptLit);
template<bool dontCareLearnt>
- 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<Lit>& out_learnt, int& out_btlevel, uint32_t &nblevels, const bool update); // (bt = backtrack)
+ Clause* analyze (PropagatedFrom confl, vec<Lit>& out_learnt, int& out_btlevel, uint32_t &nblevels, const bool update); // (bt = backtrack)
void analyzeFinal (Lit p, vec<Lit>& 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<Lit>& learnt_clause, Clause* confl, int& conflictC, const bool update);// Handles the conflict clause
+ llbool handle_conflict (vec<Lit>& 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:
template<class T>
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;
friend class XorSubsumer;
friend class PartHandler;
friend class StateSaver;
+ friend class UselessBinRemover;
+ friend class OnlyNonLearntBins;
+ friend class ClauseAllocator;
Conglomerate* conglomerate;
VarReplacer* varReplacer;
ClauseCleaner* clauseCleaner;
//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()
{
return trail.size();
}
template <class T>
-inline void Solver::removeWatchedCl(vec<T> &ws, const Clause *c) {
+inline void Solver::removeWatchedCl(vec<T> &ws, const ClauseOffset c) {
uint32_t j = 0;
for (; j < ws.size() && ws[j].clause != c; j++);
assert(j < ws.size());
ws.pop();
}
template <class T>
-inline void Solver::removeWatchedBinCl(vec<T> &ws, const Clause *c) {
+inline void Solver::removeWatchedBinCl(vec<T> &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 <class T>
+inline void Solver::removeWatchedBinClAll(vec<T> &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<class T>
-inline bool Solver::findWatchedCl(const vec<T>& ws, const Clause *c) const
+inline bool Solver::findWatchedCl(const vec<T>& ws, const ClauseOffset c) const
{
uint32_t j = 0;
for (; j < ws.size() && ws[j].clause != c; j++);
return j < ws.size();
}
template<class T>
-inline bool Solver::findWatchedBinCl(const vec<T>& ws, const Clause *c) const
+inline bool Solver::findWatchedBinCl(const vec<T>& 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);
inline void Solver::removeClause(T& c)
{
detachClause(c);
- clauseFree(&c);
+ clauseAllocator.clauseFree(&c);
}
//=================================================================================================
{
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.
#include <algorithm>
#include "VarReplacer.h"
#include "XorFinder.h"
+#include "OnlyNonLearntBins.h"
#ifdef _MSC_VER
#define __builtin_prefetch(a,b,c)
#endif
//#define BIT_MORE_VERBOSITY
-//#define HYPER_DEBUG
-//#define HYPER_DEBUG2
//#define TOUCH_LESS
#ifdef VERBOSE_DEBUG
solver.libraryCNFFile = NULL;
for (vector<Clause*>::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);
template<class T>
uint32_t Subsumer::subsume0Orig(const T& ps, uint32_t abs)
{
+ subsumedNonLearnt = false;
uint32_t retIndex = std::numeric_limits<uint32_t>::max();
vec<ClauseSimp> subs;
findSubsumed(ps, abs, subs);
#endif
Clause* tmp = subs[i].clause;
+ subsumedNonLearnt |= !tmp->learnt();
retIndex = subs[i].index;
unlinkClause(subs[i]);
- clauseFree(tmp);
+ solver.clauseAllocator.clauseFree(tmp);
}
return retIndex;
Clause* tmp = subs[i].clause;
unlinkClause(subs[i]);
- clauseFree(tmp);
+ solver.clauseAllocator.clauseFree(tmp);
}
if (subs2.size() == 0) return;
#ifdef VERBOSE_DEBUG
std::cout << "--> Clause was satisfied." << std::endl;
#endif
- clauseFree(&cl);
+ solver.clauseAllocator.clauseFree(&cl);
goto endS;
}
}
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);
} 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;
#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:;
}
clauses[c.index].clause = NULL;
}
-void Subsumer::unlinkModifiedClause(vec<Lit>& origClause, ClauseSimp c)
+void Subsumer::unlinkModifiedClause(vec<Lit>& origClause, ClauseSimp c, bool detachAndNull)
{
for (uint32_t i = 0; i < origClause.size(); i++) {
maybeRemove(occur[origClause[i].toInt()], c.clause);
#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<ClauseSimp>& cs = *iter_vecs[i];
// Remove clause from clause touched set:
cl_touched.exclude(c);
cl_added.exclude(c);
-
- clauses[c.index].clause = NULL;
-}
-void Subsumer::unlinkModifiedClauseNoDetachNoNULL(vec<Lit>& 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<ClauseSimp>& 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)
#ifdef VERBOSE_DEBUG
std::cout << "--> Clause was satisfied." << std::endl;
#endif
- clauseFree(&cl);
+ solver.clauseAllocator.clauseFree(&cl);
goto endS;
}
}
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);
} 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);
#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:;
}
#ifdef VERBOSE_DEBUG
std::cout << "--> Clause was satisfied." << std::endl;
#endif
- clauseFree(&cl);
+ solver.clauseAllocator.clauseFree(&cl);
goto endS;
}
}
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);
} 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;
#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:;
}
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);
}
}
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;
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);
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);
// 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);
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
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);
if (var_elimed[l->var()]) {
remove = true;
solver.detachClause(c);
- clauseFree(&c);
+ solver.clauseAllocator.clauseFree(&c);
break;
}
}
#endif
}
-void Subsumer::subsume0LearntSet(vec<Clause*>& 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<uint32_t>::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;
}
#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) <<solver.trail.size() - origTrailSize
<< " time: " << std::setprecision(2) << std::setw(5) << cpuTime() - myTime << " s"
- << " |" << std::endl;
+ << std::setw(17) << " |" << std::endl;
}
- if (!subsWNonExistBinsFull(startUp)) return false;
+ if (!subsWNonExistBinsFull(onlyNonLearntBins)) return false;
#ifdef DEBUG_BINARIES
for (uint32_t i = 0; i < clauses.size(); i++) {
#endif //DEBUG_BINARIES
addBackToSolver();
for (uint32_t i = 0; i < addBinaryClauses.size(); i++) {
- solver.binaryClauses.push(addBinaryClauses[i]);
+ Clause& c = *addBinaryClauses[i];
+ solver.detachClause(c);
+ Clause *c2 = solver.clauseAllocator.Clause_new(c);
+ solver.clauseAllocator.clauseFree(&c);
+ solver.attachClause(*c2);
+ solver.becameBinary++;
+ solver.binaryClauses.push(c2);
}
addBinaryClauses.clear();
+ freeMemory();
if (solver.verbosity >= 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));
#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;
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);
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;
}
//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;
}
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();
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);
cl_touched.clear();
}
-const bool Subsumer::simplifyBySubsumption()
+const bool Subsumer::simplifyBySubsumption(const bool alsoLearnt)
{
if (solver.nClauses() > 20000000) return true;
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<true>(solver.clauses);
+ addFromSolver<true>(solver.clauses, alsoLearnt);
solver.clauseCleaner->removeSatisfied(solver.binaryClauses, ClauseCleaner::binaryClauses);
- addFromSolver<true>(solver.binaryClauses);
+ addFromSolver<true>(solver.binaryClauses, alsoLearnt);
//Limits
if (clauses.size() > 3500000) {
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<int64_t>::max();
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;
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;
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;
#ifndef NDEBUG
verifyIntegrity();
#endif
-
- //vector<char> 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
}
}
-const bool Subsumer::hyperUtility(vec<ClauseSimp>& iter, const Lit lit, BitArray& inside, vec<Clause*>& 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<Lit> lits(1);
- lits[0] = lit;
- solver.addClauseInt(lits, cl.getGroup());
- if (!solver.ok) return false;
- }
-
- if (notIn == 1 && !inside[(~notInLit).toInt()]) {
- vec<Lit> cs(2);
- cs[0] = lit;
- cs[1] = notInLit;
- //uint32_t index = subsume0(cs, calcAbstraction(cs));
- /*if (index != std::numeric_limits<uint32_t>::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<Clause*> addToClauses;
- vec<Lit> addedToInside;
- uint64_t totalClausesChecked = 0;
-
- vec<Var> varsToCheck;
-
- if (clauses.size() > 500000 || solver.order_heap.size() > 50000) {
- Heap<Solver::VarOrderLt> 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<ClauseSimp>& 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<ClauseSimp>& 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<uint> occurNum(solver.nVars()*2, 0);
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<ClauseSimp> 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<ClauseSimp> 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
using namespace MINISAT;
class ClauseCleaner;
+class OnlyNonLearntBins;
class Subsumer
{
~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<Lit>& origClause, ClauseSimp c);
- void unlinkModifiedClauseNoDetachNoNULL(vec<Lit>& origClause, ClauseSimp c);
+ void unlinkModifiedClause(vec<Lit>& origClause, ClauseSimp c, const bool detachAndNull);
void unlinkClause(ClauseSimp cc, Var elim = var_Undef);
ClauseSimp linkInClause(Clause& cl);
void linkInAlreadyClause(ClauseSimp& c);
private:
friend class ClauseCleaner;
+ friend class ClauseAllocator;
//Main
vec<ClauseSimp> clauses;
//Start-up
template<bool UseCL>
void addFromSolver(vec<Clause*>& cs, bool alsoLearnt = false);
+ void fillCannotEliminate();
+ void clearAll();
+
+ //Finish-up
+ void freeMemory();
void addBackToSolver();
void removeWrong(vec<Clause*>& cs);
void removeAssignedVarsFromEliminated();
- void fillCannotEliminate();
- const bool treatLearnts();
- void clearAll();
//Iterations
void registerIteration (CSet& iter_set) { iter_sets.push(&iter_set); }
uint32_t subsume0(T& ps, uint32_t abs);
template<class T>
uint32_t subsume0Orig(const T& ps, uint32_t abs);
+ bool subsumedNonLearnt;
void subsume0BIN(const Lit lit, const vec<char>& lits);
- void subsume0LearntSet(vec<Clause*>& cs);
void subsume1(ClauseSimp& ps);
void smaller_database();
void almost_all_database();
bool subsetAbst(uint32_t A, uint32_t B);
void orderVarsForElim(vec<Var>& order);
- int substitute(Lit x, Clause& def, vec<Clause*>& poss, vec<Clause*>& negs, vec<Clause*>& new_clauses);
bool maybeEliminate(Var x);
void MigrateToPsNs(vec<ClauseSimp>& poss, vec<ClauseSimp>& negs, vec<ClauseSimp>& ps, vec<ClauseSimp>& ns, const Var x);
void DeallocPsNs(vec<ClauseSimp>& ps, vec<ClauseSimp>& ns);
bool merge(const Clause& ps, const Clause& qs, const Lit without_p, const Lit without_q, vec<Lit>& 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<class T>
void subsume1Partial(const T& ps);
uint32_t subsNonExistentNum;
vec<char> toVisitAll;
vec<Lit> ps2;
- //hyperBinRes
- void addFromSolverAll(vec<Clause*>& cs);
- const bool hyperBinRes();
- const bool hyperUtility(vec<ClauseSimp>& iter, const Lit lit, BitArray& inside, vec<Clause*>& addToClauses);
-
- //merging
- //vector<char> merge();
- //const bool checkIfSame(const Lit var1, const Lit var2);
-
class VarOcc {
public:
VarOcc(const Var& v, const uint32_t num) :
--- /dev/null
+/***********************************************************************************
+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 <iomanip>
+#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<Lit>& 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
--- /dev/null
+/***********************************************************************************
+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/>.
+**************************************************************************************************/
+
+#ifndef USELESSBINREMOVER_H
+#define USELESSBINREMOVER_H
+
+#include "Vec.h"
+#include "Solver.h"
+#include "OnlyNonLearntBins.h"
+#include <stdint.h>
+
+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<Lit>& wrong);
+ const bool removeUselessBinaries(const Lit& lit);
+ void removeBin(const Lit& lit1, const Lit& lit2);
+ vec<char> toDeleteSet;
+ vec<Lit> oneHopAway;
+ vec<Lit> wrong;
+
+ Solver& solver;
+ OnlyNonLearntBins& onlyNonLearntBins;
+};
+
+#endif //USELESSBINREMOVER_H
+
+}; //NAMESPACE MINISAT
CryptoMiniSat
-GIT revision: ef1086af7fca458d28352cdda8ebe74339ed5817
+GIT revision: d1a89e619d41131629e6c4e74f9424453225ba2d
VarReplacer::~VarReplacer()
{
for (uint i = 0; i != clauses.size(); i++)
- clauseFree(clauses[i]);
+ solver.clauseAllocator.clauseFree(clauses[i]);
}
const bool VarReplacer::performReplaceInternal()
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;
}
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);
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;
}
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);
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);
}
}
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++;
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++;
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();
}; //NAMESPACE MINISAT
-#endif //XSET_H
\ No newline at end of file
+#endif //XSET_H
#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) {
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);
};
// 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<Lit> origClause(ps.clause->size());
- std::copy(ps.clause->getData(), ps.clause->getDataEnd(), origClause.getData());
- const bool origClauseInverted = ps.clause->xor_clause_inverted();
-
+
vec<Lit> unmatchedPart;
- bool needUnlinkPS = false;
-
vec<XorClauseSimp> 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;
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<Lit>& A, XorClause& B, vec<Lit>& unmatchedPart)
+template<class T>
+void XorSubsumer::findUnMatched(const T& A, const T& B, vec<Lit>& unmatchedPart)
{
for (uint32_t i = 0; i != B.size(); i++)
seen_tmp[B[i].var()] = 1;
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)
void XorSubsumer::unlinkModifiedClause(vec<Lit>& 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);
void XorSubsumer::unlinkModifiedClauseNoDetachNoNULL(vec<Lit>& 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);
}
}
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();
return true;
}
-void XorSubsumer::clearDouble(vec<Lit>& ps) const
+template<class T>
+void XorSubsumer::xorTwoClauses(const T& c1, const T& c2, vec<Lit>& 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<Clause*>& cs)
if (var_elimed[l->var()]) {
remove = true;
solver.detachClause(c);
- clauseFree(&c);
+ solver.clauseAllocator.clauseFree(&c);
break;
}
}
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;
for (vector<XorClause*>::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);
}
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;
return true;
}
-}; //NAMESPACE MINISAT
\ No newline at end of file
+}; //NAMESPACE MINISAT
private:
friend class ClauseCleaner;
+ friend class ClauseAllocator;
//Main
vec<XorClauseSimp> clauses;
// Subsumption:
void findSubsumed(XorClause& ps, vec<XorClauseSimp>& out_subsumed);
bool isSubsumed(XorClause& ps);
- void subsume0(XorClauseSimp& ps);
+ void subsume0(XorClauseSimp ps);
template<class T1, class T2>
bool subset(const T1& A, const T2& B);
bool subsetAbst(uint32_t A, uint32_t B);
- void findUnMatched(vec<Lit>& A, XorClause& B, vec<Lit>& unmatchedPart);
+ template<class T>
+ void findUnMatched(const T& A, const T& B, vec<Lit>& unmatchedPart);
//helper
void testAllClauseAttach() const;
uint32_t numElimed;
//Heule-process
- void clearDouble(vec<Lit>& ps) const;
+ template<class T>
+ void xorTwoClauses(const T& c1, const T& c2, vec<Lit>& xored);
const bool localSubstitute();
uint32_t localSubstituteUseful;
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
//#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
+++ /dev/null
-// 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 <boost/config.hpp> // for workarounds
-
-// std::less, std::less_equal, std::greater
-#include <functional>
-// new[], delete[], std::nothrow
-#include <new>
-// std::size_t, std::ptrdiff_t
-#include <cstddef>
-// std::malloc, std::free
-#include <cstdlib>
-// std::invalid_argument
-#include <exception>
-// std::max
-#include <algorithm>
-
-#include "poolfwd.hpp"
-
-// boost::details::pool::ct_lcm
-#include <boost/pool/detail/ct_gcd_lcm.hpp>
-// boost::details::pool::lcm
-#include <boost/pool/detail/gcd_lcm.hpp>
-// boost::simple_segregated_storage
-#include <boost/pool/simple_segregated_storage.hpp>
-
-#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<char *>(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 <typename SizeType>
-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<sizeof(size_type), sizeof(void *)>::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<sizeof(size_type), sizeof(void *)>::value);
- }
-
- size_type & next_size() const
- { return *(reinterpret_cast<size_type *>(ptr_next_size())); }
- char * & next_ptr() const
- { return *(reinterpret_cast<char **>(ptr_next_ptr())); }
-
- PODptr next() const
- { return PODptr<size_type>(next_ptr(), next_size()); }
- void next(const PODptr & arg) const
- {
- next_ptr() = arg.begin();
- next_size() = arg.total_size();
- }
-};
-
-} // namespace details
-
-template <typename UserAllocator>
-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<sizeof(void *), sizeof(size_type)>::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<size_type> list;
-
- simple_segregated_storage<size_type> & store() { return *this; }
- const simple_segregated_storage<size_type> & 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<size_type> 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<void *>()(static_cast<void *>(i), chunk)
-// && std::less<void *>()(chunk,
-// static_cast<void *>(i + sizeof_i)));
- std::less_equal<void *> lt_eq;
- std::less<void *> 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<size_type>(requested_size, min_size);
- }
-
- // for the sake of code readability :)
- static void * & nextof(void * const ptr)
- { return *(static_cast<void **>(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 <typename UserAllocator>
-bool pool<UserAllocator>::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<size_type> ptr = list;
- details::PODptr<size_type> 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<size_type> next = ptr.next();
-
- if (!all_chunks_free)
- {
- if (is_from(free_p, ptr.begin(), ptr.element_size()))
- {
- std::less<void *> 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 <typename UserAllocator>
-bool pool<UserAllocator>::purge_memory()
-{
- details::PODptr<size_type> iter = list;
-
- if (!iter.valid())
- return false;
-
- do
- {
- // hold "next" pointer
- const details::PODptr<size_type> 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 <typename UserAllocator>
-void * pool<UserAllocator>::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<sizeof(size_type), sizeof(void *)>::value + sizeof(size_type);
- char * const ptr = UserAllocator::malloc(POD_size);
- if (ptr == 0)
- return 0;
- const details::PODptr<size_type> 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 <typename UserAllocator>
-void * pool<UserAllocator>::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<sizeof(size_type), sizeof(void *)>::value + sizeof(size_type);
- char * const ptr = UserAllocator::malloc(POD_size);
- if (ptr == 0)
- return 0;
- const details::PODptr<size_type> 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<void *>()(list.begin(), node.begin()))
- {
- node.next(list);
- list = node;
- }
- else
- {
- details::PODptr<size_type> 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<void *>()(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 <typename UserAllocator>
-void * pool<UserAllocator>::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<sizeof(size_type), sizeof(void *)>::value + sizeof(size_type);
- char * const ptr = UserAllocator::malloc(POD_size);
- if (ptr == 0)
- return 0;
- const details::PODptr<size_type> 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<void *>()(list.begin(), node.begin()))
- {
- node.next(list);
- list = node;
- }
- else
- {
- details::PODptr<size_type> 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<void *>()(prev.next_ptr(), node.begin()))
- break;
-
- prev = prev.next();
- }
-
- node.next(prev.next());
- prev.next(node);
- }
-
- // and return it.
- return node.begin();
-}
-
-template <typename UserAllocator>
-details::PODptr<typename pool<UserAllocator>::size_type>
-pool<UserAllocator>::find_POD(void * const chunk) const
-{
- // We have to find which storage this chunk is from.
- details::PODptr<size_type> iter = list;
- while (iter.valid())
- {
- if (is_from(chunk, iter.begin(), iter.element_size()))
- return iter;
- iter = iter.next();
- }
-
- return iter;
-}
-
-} // namespace boost
-
-#endif
+++ /dev/null
-// 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 <boost/config.hpp> // for workarounds
-
-// std::size_t
-#include <cstddef>
-
-// boost::details::pool::default_mutex
-//#include <boost/pool/detail/mutex.hpp>
-
-namespace boost {
-
-//
-// Location: <boost/pool/simple_segregated_storage.hpp>
-//
-template <typename SizeType = std::size_t>
-class simple_segregated_storage;
-
-//
-// Location: <boost/pool/pool.hpp>
-//
-struct default_user_allocator_new_delete;
-struct default_user_allocator_malloc_free;
-
-template <typename UserAllocator = default_user_allocator_new_delete>
-class pool;
-
-//
-// Location: <boost/pool/object_pool.hpp>
-//
-template <typename T, typename UserAllocator = default_user_allocator_new_delete>
-class object_pool;
-
-//
-// Location: <boost/pool/singleton_pool.hpp>
-//
-template <typename Tag, unsigned RequestedSize,
- typename UserAllocator = default_user_allocator_new_delete,
- unsigned NextSize = 32>
-struct singleton_pool;
-
-//
-// Location: <boost/pool/pool_alloc.hpp>
-//
-struct pool_allocator_tag;
-
-template <typename T,
- typename UserAllocator = default_user_allocator_new_delete,
- unsigned NextSize = 32>
-class pool_allocator;
-
-struct fast_pool_allocator_tag;
-
-template <typename T,
- typename UserAllocator = default_user_allocator_new_delete,
- unsigned NextSize = 32>
-class fast_pool_allocator;
-
-} // namespace boost
-
-#endif
+++ /dev/null
-// 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<T>::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 <typename T>
-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<T>::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<T>::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<T>::create_object, whose constructor is
- // called before main() begins.
- create_object.do_nothing();
-
- return obj;
- }
-};
-template <typename T>
-typename singleton_default<T>::object_creator
-singleton_default<T>::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
projects / francis / stp.git / commitdiff