00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020 #ifndef CLASP_SOLVER_TYPES_H_INCLUDED
00021 #define CLASP_SOLVER_TYPES_H_INCLUDED
00022 #ifdef _MSC_VER
00023 #pragma once
00024 #endif
00025
00026 #include <clasp/literal.h>
00027 #include <clasp/constraint.h>
00028 #include <clasp/util/left_right_sequence.h>
00029 #include <clasp/util/misc_types.h>
00030 #include <clasp/util/type_manip.h>
00031 #include <numeric>
00036 namespace Clasp {
00037 class SharedLiterals;
00038
00043
00045
00047 inline double ratio(uint64 x, uint64 y) {
00048 if (!x || !y) return 0.0;
00049 return static_cast<double>(x) / static_cast<double>(y);
00050 }
00051 inline double percent(uint64 x, uint64 y) { return ratio(x, y) * 100.0; }
00052
00053 inline bool matchStatPath(const char*& x, const char* path, std::size_t len) {
00054 return std::strncmp(x, path, len) == 0 && (!x[len] || x[len++] == '.') && ((x += len) != 0);
00055 }
00056 inline bool matchStatPath(const char*& x, const char* path) {
00057 return matchStatPath(x, path, std::strlen(path));
00058 }
00059
00060 #define CLASP_STAT_ACCU(m, k, a, accu) accu;
00061 #define CLASP_STAT_DEFINE(m, k, a, accu) m
00062 #define CLASP_STAT_GET(m, k, a, accu) if (std::strcmp(key, k) == 0) { return double( (a) ); }
00063 #define CLASP_STAT_KEY(m, k, a, accu) k "\0"
00064 #define NO_ARG
00065
00067
00071 struct CoreStats {
00072 #define CLASP_CORE_STATS(STAT, SELF, OTHER) \
00073 STAT(uint64 choices; , STRING(choices) , SELF.choices , SELF.choices += OTHER.choices )\
00074 STAT(uint64 conflicts; , STRING(conflicts) , SELF.conflicts , SELF.conflicts += OTHER.conflicts )\
00075 STAT(uint64 analyzed; , STRING(analyzed) , SELF.analyzed , SELF.analyzed += OTHER.analyzed )\
00076 STAT(uint64 restarts; , STRING(restarts) , SELF.restarts , SELF.restarts += OTHER.restarts )\
00077 STAT(uint64 lastRestart;, STRING(lastRestart), SELF.lastRestart, SELF.lastRestart = std::max(SELF.lastRestart, OTHER.lastRestart))
00078
00079 CoreStats() { reset(); }
00080 void reset() { std::memset(this, 0, sizeof(CoreStats)); }
00081 void accu(const CoreStats& o) {
00082 CLASP_CORE_STATS(CLASP_STAT_ACCU, (*this), o)
00083 }
00084 double operator[](const char* key) const {
00085 CLASP_CORE_STATS(CLASP_STAT_GET, (*this), NO_ARG)
00086 return -1.0;
00087 }
00088 static const char* keys(const char* path) {
00089 if (!path || !*path) return CLASP_CORE_STATS(CLASP_STAT_KEY,NO_ARG,NO_ARG);
00090 return 0;
00091 }
00092 uint64 backtracks() const { return conflicts-analyzed; }
00093 uint64 backjumps() const { return analyzed; }
00094 double avgRestart() const { return ratio(analyzed, restarts); }
00095 CLASP_CORE_STATS(CLASP_STAT_DEFINE, NO_ARG, NO_ARG)
00096 };
00097
00099 struct ExtendedStats {
00100 typedef ConstraintType type_t;
00101 typedef uint64 Array[Constraint_t::max_value];
00102 #define CLASP_EXTENDED_STATS(STAT, SELF, OTHER) \
00103 STAT(uint64 domChoices; , STRING(domChoices) , SELF.domChoices , SELF.domChoices += OTHER.domChoices) \
00104 STAT(uint64 models; , STRING(models) , SELF.models , SELF.models += OTHER.models) \
00105 STAT(uint64 modelLits; , STRING(modelLits) , SELF.modelLits , SELF.modelLits += OTHER.modelLits) \
00106 STAT(uint64 hccTests; , STRING(hccTests) , SELF.hccTests , SELF.hccTests += OTHER.hccTests) \
00107 STAT(uint64 hccPartial; , STRING(hccPartial) , SELF.hccPartial , SELF.hccPartial += OTHER.hccPartial) \
00108 STAT(uint64 deleted; , STRING(deleted) , SELF.deleted , SELF.deleted += OTHER.deleted) \
00109 STAT(uint64 distributed;, STRING(distributed), SELF.distributed, SELF.distributed+= OTHER.distributed)\
00110 STAT(uint64 sumDistLbd; , STRING(sumDistLbd) , SELF.sumDistLbd , SELF.sumDistLbd += OTHER.sumDistLbd) \
00111 STAT(uint64 integrated; , STRING(integrated) , SELF.integrated , SELF.integrated += OTHER.integrated) \
00112 STAT(Array learnts; , "lemmas" , SELF.lemmas() , NO_ARG) \
00113 STAT(Array lits; , "learntLits" , SELF.learntLits(), NO_ARG) \
00114 STAT(uint32 binary; , STRING(binary) , SELF.binary , SELF.binary += OTHER.binary) \
00115 STAT(uint32 ternary; , STRING(ternary) , SELF.ternary , SELF.ternary += OTHER.ternary) \
00116 STAT(double cpuTime; , STRING(cpuTime) , SELF.cpuTime , SELF.cpuTime += OTHER.cpuTime) \
00117 STAT(uint64 intImps; , STRING(intImps) , SELF.intImps , SELF.intImps+= OTHER.intImps) \
00118 STAT(uint64 intJumps; , STRING(intJumps) , SELF.intJumps, SELF.intJumps+=OTHER.intJumps) \
00119 STAT(uint64 gpLits; , STRING(gpLits) , SELF.gpLits , SELF.gpLits += OTHER.gpLits) \
00120 STAT(uint32 gps; , STRING(gps) , SELF.gps , SELF.gps += OTHER.gps) \
00121 STAT(uint32 splits; , STRING(splits) , SELF.splits , SELF.splits += OTHER.splits) \
00122 STAT(NO_ARG , "conflictLemmas", SELF.lemmas(Constraint_t::learnt_conflict), SELF.learnts[0] += OTHER.learnts[0]) \
00123 STAT(NO_ARG , "loopLemmas" , SELF.lemmas(Constraint_t::learnt_loop) , SELF.learnts[1] += OTHER.learnts[1]) \
00124 STAT(NO_ARG , "otherLemmas" , SELF.lemmas(Constraint_t::learnt_other) , SELF.learnts[2] += OTHER.learnts[2]) \
00125 STAT(NO_ARG , "conflictLits" , SELF.lits[Constraint_t::learnt_conflict-1], SELF.lits[0] += OTHER.lits[0]) \
00126 STAT(NO_ARG , "loopLits" , SELF.lits[Constraint_t::learnt_loop-1] , SELF.lits[1] += OTHER.lits[1]) \
00127 STAT(NO_ARG , "otherLits" , SELF.lits[Constraint_t::learnt_other-1] , SELF.lits[2] += OTHER.lits[2])
00128
00129 ExtendedStats() { reset(); }
00130 void reset() { std::memset(this, 0, sizeof(ExtendedStats)); }
00131 void accu(const ExtendedStats& o) {
00132 CLASP_EXTENDED_STATS(CLASP_STAT_ACCU, (*this), o)
00133 }
00134 double operator[](const char* key) const {
00135 CLASP_EXTENDED_STATS(CLASP_STAT_GET, (*this), NO_ARG)
00136 return -1.0;
00137 }
00138 static const char* keys(const char* path) {
00139 if (!path || !*path) { return CLASP_EXTENDED_STATS(CLASP_STAT_KEY,NO_ARG,NO_ARG); }
00140 return 0;
00141 }
00142 void addLearnt(uint32 size, type_t t) {
00143 assert(t != Constraint_t::static_constraint && t <= Constraint_t::max_value);
00144 learnts[t-1]+= 1;
00145 lits[t-1] += size;
00146 binary += (size == 2);
00147 ternary += (size == 3);
00148 }
00149 uint64 lemmas() const { return std::accumulate(learnts, learnts+Constraint_t::max_value, uint64(0)); }
00150 uint64 learntLits() const { return std::accumulate(lits, lits+Constraint_t::max_value, uint64(0)); }
00151 uint64 lemmas(type_t t)const { return learnts[t-1]; }
00152 double avgLen(type_t t)const { return ratio(lits[t-1], lemmas(t)); }
00153 double avgModel() const { return ratio(modelLits, models); }
00154 double distRatio() const { return ratio(distributed, learnts[0] + learnts[1]); }
00155 double avgDistLbd() const { return ratio(sumDistLbd, distributed); }
00156 double avgIntJump() const { return ratio(intJumps, intImps); }
00157 double avgGp() const { return ratio(gpLits, gps); }
00158 double intRatio() const { return ratio(integrated, distributed); }
00159 CLASP_EXTENDED_STATS(CLASP_STAT_DEFINE,NO_ARG,NO_ARG)
00160 };
00161
00163 struct JumpStats {
00164 #define CLASP_JUMP_STATS(STAT, SELF, OTHER) \
00165 STAT(uint64 jumps; , STRING(jumps) , SELF.jumps , SELF.jumps += OTHER.jumps) \
00166 STAT(uint64 bounded; , STRING(bounded) , SELF.bounded , SELF.bounded += OTHER.bounded) \
00167 STAT(uint64 jumpSum; , STRING(jumpSum) , SELF.jumpSum , SELF.jumpSum += OTHER.jumpSum) \
00168 STAT(uint64 boundSum; , STRING(boundSum) , SELF.boundSum , SELF.boundSum += OTHER.boundSum) \
00169 STAT(uint32 maxJump; , STRING(maxJump) , SELF.maxJump , MAX_MEM(SELF.maxJump, OTHER.maxJump)) \
00170 STAT(uint32 maxJumpEx;, STRING(maxJumpEx), SELF.maxJumpEx, MAX_MEM(SELF.maxJumpEx,OTHER.maxJumpEx)) \
00171 STAT(uint32 maxBound; , STRING(maxBound) , SELF.maxBound , MAX_MEM(SELF.maxBound, OTHER.maxBound))
00172
00173 JumpStats() { reset(); }
00174 void reset(){ std::memset(this, 0, sizeof(*this)); }
00175 void accu(const JumpStats& o) {
00176 #define MAX_MEM(X,Y) X = std::max((X), (Y))
00177 CLASP_JUMP_STATS(CLASP_STAT_ACCU, (*this), o)
00178 #undef MAX_MEM
00179 }
00180 double operator[](const char* key) const {
00181 CLASP_JUMP_STATS(CLASP_STAT_GET, (*this), NO_ARG)
00182 return -1.0;
00183 }
00184 static const char* keys(const char* path) {
00185 if (!path || !*path) { return CLASP_JUMP_STATS(CLASP_STAT_KEY,NO_ARG,NO_ARG); }
00186 return 0;
00187 }
00188 void update(uint32 dl, uint32 uipLevel, uint32 bLevel) {
00189 ++jumps;
00190 jumpSum += dl - uipLevel;
00191 maxJump = std::max(maxJump, dl - uipLevel);
00192 if (uipLevel < bLevel) {
00193 ++bounded;
00194 boundSum += bLevel - uipLevel;
00195 maxJumpEx = std::max(maxJumpEx, dl - bLevel);
00196 maxBound = std::max(maxBound, bLevel - uipLevel);
00197 }
00198 else { maxJumpEx = maxJump; }
00199 }
00200 uint64 jumped() const { return jumpSum - boundSum; }
00201 double jumpedRatio()const { return ratio(jumped(), jumpSum); }
00202 double avgBound() const { return ratio(boundSum, bounded); }
00203 double avgJump() const { return ratio(jumpSum, jumps); }
00204 double avgJumpEx() const { return ratio(jumped(), jumps); }
00205 CLASP_JUMP_STATS(CLASP_STAT_DEFINE,NO_ARG,NO_ARG)
00206 };
00207
00208 struct QueueImpl {
00209 explicit QueueImpl(uint32 size) : maxSize(size), wp(0), rp(0) {}
00210 bool full() const { return size() == maxSize; }
00211 uint32 size() const { return ((rp > wp) * cap()) + wp - rp;}
00212 uint32 cap() const { return maxSize + 1; }
00213 void clear() { wp = rp = 0; }
00214 uint32 top() const { return buffer[rp]; }
00215 void push(uint32 x){ buffer[wp] = x; if (++wp == cap()) { wp = 0; } }
00216 void pop() { if (++rp == cap()) { rp = 0; } }
00217 uint32 maxSize;
00218 uint32 wp;
00219 uint32 rp;
00220 uint32 buffer[1];
00221 };
00222
00223 struct SumQueue {
00224 static SumQueue* create(uint32 size) {
00225 void* m = ::operator new(sizeof(SumQueue) + (size*sizeof(uint32)));
00226 return new (m) SumQueue(size);
00227 }
00228 void dynamicRestarts(float x, bool xLbd) {
00229 upForce = 16000;
00230 upCfl = 0;
00231 nRestart = 0;
00232 lim = x;
00233 lbd = xLbd;
00234 }
00235 void destroy() { this->~SumQueue(); ::operator delete(this); }
00236 void resetQueue() { sumLbd = sumCfl = samples = 0; queue.clear(); }
00237 void resetGlobal() { globalSumLbd = globalSumCfl = globalSamples = 0; resetQueue(); }
00238 void update(uint32 dl, uint32 lbd) {
00239 if (samples++ >= queue.maxSize) {
00240 uint32 y = queue.top();
00241 sumLbd -= (y & 127u);
00242 sumCfl -= (y >> 7u);
00243 queue.pop();
00244 }
00245 sumLbd += lbd;
00246 sumCfl += dl;
00247 ++upCfl;
00248 ++globalSamples;
00249 globalSumLbd += lbd;
00250 globalSumCfl += dl;
00251 queue.push((dl << 7) + lbd);
00252 }
00253 double avgLbd() const { return sumLbd / (double)queue.maxSize; }
00254 double avgCfl() const { return sumCfl / (double)queue.maxSize; }
00255 uint32 maxSize()const { return queue.maxSize; }
00256 bool full() const { return queue.full(); }
00257 double globalAvgLbd() const { return ratio(globalSumLbd, globalSamples); }
00258 double globalAvgCfl() const { return ratio(globalSumCfl, globalSamples); }
00259 bool isRestart() const { return full() && (lbd ? (avgLbd()*lim) > globalAvgLbd() : (avgCfl() * lim) > globalAvgCfl()); }
00260 uint32 restart(uint32 maxLBD, float xLim);
00261
00262 uint64 globalSumLbd;
00263 uint64 globalSumCfl;
00264 uint64 globalSamples;
00265 uint32 sumLbd;
00266 uint32 sumCfl;
00267 uint32 samples;
00268
00269 uint32 upForce;
00270 uint32 upCfl;
00271 uint32 nRestart;
00272 float lim;
00273 bool lbd;
00274
00275 QueueImpl queue;
00276 private:
00277 SumQueue(uint32 size)
00278 : globalSumLbd(0), globalSumCfl(0), globalSamples(0), sumLbd(0), sumCfl(0), samples(0)
00279 , upForce(16000), upCfl(0), nRestart(0), lim(0.0f), lbd(true)
00280 , queue(size) {
00281 }
00282 SumQueue(const SumQueue&);
00283 SumQueue& operator=(const SumQueue&);
00284 };
00285
00287 struct SolverStats : public CoreStats {
00288 SolverStats() : queue(0), extra(0), jumps(0) {}
00289 SolverStats(const SolverStats& o) : CoreStats(o), queue(0), extra(0), jumps(0) {
00290 if (o.queue) enableQueue(o.queue->maxSize());
00291 enableStats(o);
00292 }
00293 ~SolverStats() { delete jumps; delete extra; if (queue) queue->destroy(); }
00294 bool enableStats(const SolverStats& other);
00295 int level() const { return (extra != 0) + (jumps != 0); }
00296 bool enableExtended();
00297 bool enableJump();
00298 void enableQueue(uint32 size);
00299 void reset();
00300 void accu(const SolverStats& o);
00301 void swapStats(SolverStats& o);
00302 double operator[](const char* key) const;
00303 const char* subKeys(const char* p) const;
00304 const char* keys(const char* path) const {
00305 if (!path || !*path) {
00306 if (jumps && extra) { return "jumps.\0extra.\0" CLASP_CORE_STATS(CLASP_STAT_KEY,NO_ARG,NO_ARG); }
00307 if (extra) { return "extra.\0" CLASP_CORE_STATS(CLASP_STAT_KEY,NO_ARG,NO_ARG); }
00308 if (jumps) { return "jumps.\0" CLASP_CORE_STATS(CLASP_STAT_KEY,NO_ARG,NO_ARG); }
00309 return CoreStats::keys(path);
00310 }
00311 return subKeys(path);
00312 }
00313 inline void addLearnt(uint32 size, ConstraintType t);
00314 inline void updateJumps(uint32 dl, uint32 uipLevel, uint32 bLevel, uint32 lbd);
00315 inline void addDeleted(uint32 num);
00316 inline void addDistributed(uint32 lbd, ConstraintType t);
00317 inline void addTest(bool partial);
00318 inline void addModel(uint32 decisionLevel);
00319 inline void addCpuTime(double t);
00320 inline void addSplit(uint32 num = 1);
00321 inline void addDomChoice(uint32 num = 1);
00322 inline void addIntegratedAsserting(uint32 receivedDL, uint32 jumpDL);
00323 inline void addIntegrated(uint32 num = 1);
00324 inline void removeIntegrated(uint32 num = 1);
00325 inline void addPath(const LitVec::size_type& sz);
00326 SumQueue* queue;
00327 ExtendedStats* extra;
00328 JumpStats* jumps;
00329 private: SolverStats& operator=(const SolverStats&);
00330 };
00331 inline void SolverStats::addLearnt(uint32 size, ConstraintType t) { if (extra) { extra->addLearnt(size, t); } }
00332 inline void SolverStats::addDeleted(uint32 num) { if (extra) { extra->deleted += num; } }
00333 inline void SolverStats::addDistributed(uint32 lbd, ConstraintType){ if (extra) { ++extra->distributed; extra->sumDistLbd += lbd; } }
00334 inline void SolverStats::addIntegrated(uint32 n) { if (extra) { extra->integrated += n;} }
00335 inline void SolverStats::removeIntegrated(uint32 n) { if (extra) { extra->integrated -= n;} }
00336 inline void SolverStats::addCpuTime(double t) { if (extra) { extra->cpuTime += t; } }
00337 inline void SolverStats::addSplit(uint32 num) { if (extra) { extra->splits += num; } }
00338 inline void SolverStats::addPath(const LitVec::size_type& sz) { if (extra) { ++extra->gps; extra->gpLits += sz; } }
00339 inline void SolverStats::addTest(bool partial) { if (extra) { ++extra->hccTests; extra->hccPartial += (uint32)partial; } }
00340 inline void SolverStats::addModel(uint32 DL) { if (extra) { ++extra->models; extra->modelLits += DL; } }
00341 inline void SolverStats::addDomChoice(uint32 n) { if (extra) { extra->domChoices += n; } }
00342 inline void SolverStats::addIntegratedAsserting(uint32 rDL, uint32 jDL) {
00343 if (extra) { ++extra->intImps; extra->intJumps += (rDL - jDL); }
00344 }
00345 inline void SolverStats::updateJumps(uint32 dl, uint32 uipLevel, uint32 bLevel, uint32 lbd) {
00346 ++analyzed;
00347 if (queue) { queue->update(dl, lbd); }
00348 if (jumps) { jumps->update(dl, uipLevel, bLevel); }
00349 }
00350 #undef CLASP_STAT_ACCU
00351 #undef CLASP_STAT_DEFINE
00352 #undef CLASP_STAT_GET
00353 #undef CLASP_STAT_KEY
00354 #undef CLASP_CORE_STATS
00355 #undef CLASP_EXTENDED_STATS
00356 #undef CLASP_JUMP_STATS
00357 #undef NO_ARG
00358
00359
00362 class ClauseInfo {
00363 public:
00364 typedef ClauseInfo self_type;
00365 enum { MAX_LBD = Activity::MAX_LBD, MAX_ACTIVITY = (1<<21)-1 };
00366 ClauseInfo(ConstraintType t = Constraint_t::static_constraint) : act_(0), lbd_(MAX_LBD), type_(t), tag_(0), aux_(0) {
00367 static_assert(sizeof(self_type) == sizeof(uint32), "Unsupported padding");
00368 }
00369 bool learnt() const { return type() != Constraint_t::static_constraint; }
00370 ConstraintType type() const { return static_cast<ConstraintType>(type_); }
00371 uint32 activity() const { return static_cast<uint32>(act_); }
00372 uint32 lbd() const { return static_cast<uint32>(lbd_); }
00373 bool tagged() const { return tag_ != 0; }
00374 bool aux() const { return tagged() || aux_ != 0; }
00375 self_type& setType(ConstraintType t) { type_ = static_cast<uint32>(t); return *this; }
00376 self_type& setActivity(uint32 act) { act_ = std::min(act, (uint32)MAX_ACTIVITY); return *this; }
00377 self_type& setTagged(bool b) { tag_ = static_cast<uint32>(b); return *this; }
00378 self_type& setLbd(uint32 a_lbd) { lbd_ = std::min(a_lbd, (uint32)MAX_LBD); return *this; }
00379 self_type& setAux(bool b) { aux_ = static_cast<uint32>(b); return *this; }
00380 private:
00381 uint32 act_ : 21;
00382 uint32 lbd_ : 7;
00383 uint32 type_: 2;
00384 uint32 tag_ : 1;
00385 uint32 aux_ : 1;
00386 };
00388 struct ClauseRep {
00389 static ClauseRep create(Literal* cl, uint32 sz, const ClauseInfo& i = ClauseInfo()) { return ClauseRep(cl, sz, false, i);}
00390 static ClauseRep prepared(Literal* cl, uint32 sz, const ClauseInfo& i = ClauseInfo()){ return ClauseRep(cl, sz, true, i); }
00391 ClauseRep(Literal* cl = 0, uint32 sz = 0, bool p = false, const ClauseInfo& i = ClauseInfo()) : info(i), size(sz), prep(uint32(p)), lits(cl) {}
00392 ClauseInfo info;
00393 uint32 size:31;
00394 uint32 prep: 1;
00395 Literal* lits;
00396 bool isImp() const { return size > 1 && size < 4; }
00397 };
00398
00400
00407 class ClauseHead : public LearntConstraint {
00408 public:
00409 enum { HEAD_LITS = 3, MAX_SHORT_LEN = 5, MAX_LBD = (1<<5)-1, TAGGED_CLAUSE = 1023, MAX_ACTIVITY = (1<<15)-1 };
00410 explicit ClauseHead(const ClauseInfo& init);
00411
00413 PropResult propagate(Solver& s, Literal, uint32& data);
00415 ConstraintType type() const { return ConstraintType(info_.data.type); }
00417 bool locked(const Solver& s) const;
00419 Activity activity() const { return Activity(info_.data.act, info_.data.lbd); }
00421 void decreaseActivity() { info_.data.act >>= 1; }
00422 void resetActivity(Activity a){ info_.data.act = std::min(a.activity(),uint32(MAX_ACTIVITY)); info_.data.lbd = std::min(a.lbd(), uint32(MAX_LBD)); }
00424 ClauseHead* clause() { return this; }
00425
00426
00427 typedef std::pair<bool, bool> BoolPair;
00429 void bumpActivity() { info_.data.act += (info_.data.act != MAX_ACTIVITY); }
00431 void attach(Solver& s);
00433 bool satisfied(const Solver& s);
00435 bool tagged() const { return info_.data.key == uint32(TAGGED_CLAUSE); }
00436 bool learnt() const { return info_.data.type!= 0; }
00437 uint32 lbd() const { return info_.data.lbd; }
00438 void lbd(uint32 x) { info_.data.lbd = std::min(x, uint32(MAX_LBD)); }
00440 virtual void detach(Solver& s);
00442 virtual uint32 size() const = 0;
00444 virtual void toLits(LitVec& out) const = 0;
00446 virtual bool isReverseReason(const Solver& s, Literal p, uint32 maxL, uint32 maxN) = 0;
00448
00455 virtual BoolPair strengthen(Solver& s, Literal p, bool allowToShort = true) = 0;
00456 protected:
00457 friend struct ClauseWatch;
00458 bool toImplication(Solver& s);
00459 void clearTagged() { info_.data.key = 0; }
00460 void setLbd(uint32 x){ info_.data.lbd = x; }
00461 bool hasLbd() const { return info_.data.type != Constraint_t::learnt_other || lbd() != MAX_LBD; }
00463
00468 virtual bool updateWatch(Solver& s, uint32 pos) = 0;
00469 union Data {
00470 SharedLiterals* shared;
00471 struct LocalClause {
00472 uint32 sizeExt;
00473 uint32 idx;
00474 void init(uint32 size) {
00475 if (size <= ClauseHead::MAX_SHORT_LEN){ sizeExt = idx = negLit(0).asUint(); }
00476 else { sizeExt = (size << 3) + 1; idx = 0; }
00477 }
00478 bool isSmall() const { return (sizeExt & 1u) == 0u; }
00479 bool contracted() const { return (sizeExt & 3u) == 3u; }
00480 bool strengthened()const { return (sizeExt & 5u) == 5u; }
00481 uint32 size() const { return sizeExt >> 3; }
00482 void setSize(uint32 size) { sizeExt = (size << 3) | (sizeExt & 7u); }
00483 void markContracted() { sizeExt |= 2u; }
00484 void markStrengthened() { sizeExt |= 4u; }
00485 void clearContracted() { sizeExt &= ~2u; }
00486 } local;
00487 uint32 lits[2];
00488 } data_;
00489 union Info {
00490 Info() : rep(0) {}
00491 explicit Info(const ClauseInfo& i);
00492 struct {
00493 uint32 act : 15;
00494 uint32 key : 10;
00495 uint32 lbd : 5;
00496 uint32 type: 2;
00497 } data;
00498 uint32 rep;
00499 } info_;
00500 Literal head_[HEAD_LITS];
00501 };
00503 class SmallClauseAlloc {
00504 public:
00505 SmallClauseAlloc();
00506 ~SmallClauseAlloc();
00507 void* allocate() {
00508 if(freeList_ == 0) {
00509 allocBlock();
00510 }
00511 Chunk* r = freeList_;
00512 freeList_ = r->next;
00513 return r;
00514 }
00515 void free(void* mem) {
00516 Chunk* b = reinterpret_cast<Chunk*>(mem);
00517 b->next = freeList_;
00518 freeList_= b;
00519 }
00520 private:
00521 SmallClauseAlloc(const SmallClauseAlloc&);
00522 SmallClauseAlloc& operator=(const SmallClauseAlloc&);
00523 struct Chunk {
00524 Chunk* next;
00525 unsigned char mem[32 - sizeof(Chunk*)];
00526 };
00527 struct Block {
00528 enum { num_chunks = 1023 };
00529 Block* next;
00530 unsigned char pad[32-sizeof(Block*)];
00531 Chunk chunk[num_chunks];
00532 };
00533 void allocBlock();
00534 Block* blocks_;
00535 Chunk* freeList_;
00536 };
00538
00541 struct ClauseWatch {
00543 explicit ClauseWatch(ClauseHead* a_head) : head(a_head) { }
00544 ClauseHead* head;
00545 struct EqHead {
00546 explicit EqHead(ClauseHead* h) : head(h) {}
00547 bool operator()(const ClauseWatch& w) const { return head == w.head; }
00548 ClauseHead* head;
00549 };
00550 };
00551
00553 struct GenericWatch {
00555 explicit GenericWatch(Constraint* a_con, uint32 a_data = 0) : con(a_con), data(a_data) {}
00557 Constraint::PropResult propagate(Solver& s, Literal p) { return con->propagate(s, p, data); }
00558
00559 Constraint* con;
00560 uint32 data;
00562 struct EqConstraint {
00563 explicit EqConstraint(Constraint* c) : con(c) {}
00564 bool operator()(const GenericWatch& w) const { return con == w.con; }
00565 Constraint* con;
00566 };
00567 };
00568
00570 typedef bk_lib::left_right_sequence<ClauseWatch, GenericWatch, 0> WatchList;
00571 inline void releaseVec(WatchList& w) { w.clear(true); }
00572
00574
00576
00579
00582 struct ReasonStore32 : PodVector<Antecedent>::type {
00583 uint32 dataSize() const { return (uint32)size(); }
00584 void dataResize(uint32) {}
00585 uint32 data(uint32 v) const { return decode((*this)[v]);}
00586 void setData(uint32 v, uint32 data) { encode((*this)[v], data); }
00587 static void encode(Antecedent& a, uint32 data) {
00588 a.asUint() = (uint64(data)<<32) | static_cast<uint32>(a.asUint());
00589 }
00590 static uint32 decode(const Antecedent& a) {
00591 return static_cast<uint32>(a.asUint()>>32);
00592 }
00593 struct value_type {
00594 value_type(const Antecedent& a, uint32 d) : ante_(a) {
00595 if (d != UINT32_MAX) { encode(ante_, d); assert(data() == d && ante_.type() == Antecedent::generic_constraint); }
00596 }
00597 const Antecedent& ante() const { return ante_; }
00598 uint32 data() const { return ante_.type() == Antecedent::generic_constraint ? decode(ante_) : UINT32_MAX; }
00599 Antecedent ante_;
00600 };
00601 };
00602
00604
00605
00606
00607 struct ReasonStore64 : PodVector<Antecedent>::type {
00608 uint32 dataSize() const { return (uint32)data_.size(); }
00609 void dataResize(uint32 nv) { if (nv > dataSize()) data_.resize(nv, UINT32_MAX); }
00610 uint32 data(uint32 v) const { return data_[v]; }
00611 void setData(uint32 v, uint32 data) { dataResize(v+1); data_[v] = data; }
00612 VarVec data_;
00613 struct value_type : std::pair<Antecedent, uint32> {
00614 value_type(const Antecedent& a, uint32 d) : std::pair<Antecedent, uint32>(a, d) {}
00615 const Antecedent& ante() const { return first; }
00616 uint32 data() const { return second; }
00617 };
00618 };
00619
00621
00629 struct ValueSet {
00630 ValueSet() : rep(0) {}
00631 enum Value { user_value = 0x03u, saved_value = 0x0Cu, pref_value = 0x30u, def_value = 0xC0u };
00632 bool sign() const { return (right_most_bit(rep) & 0xAAu) != 0; }
00633 bool empty() const { return rep == 0; }
00634 bool has(Value v) const { return (rep & v) != 0; }
00635 bool has(uint32 f)const { return (rep & f) != 0; }
00636 ValueRep get(Value v) const { return static_cast<ValueRep>((rep & v) / right_most_bit(v)); }
00637 void set(Value which, ValueRep to) { rep &= ~which; rep |= (to * right_most_bit(which)); }
00638 void save(ValueRep x) { rep &= ~saved_value; rep |= (x << 2); }
00639 uint8 rep;
00640 };
00641
00643
00653 class Assignment {
00654 public:
00655 typedef PodVector<uint32>::type AssignVec;
00656 typedef PodVector<ValueSet>::type PrefVec;
00657 typedef bk_lib::detail::if_then_else<
00658 sizeof(Constraint*)==sizeof(uint64)
00659 , ReasonStore64
00660 , ReasonStore32>::type ReasonVec;
00661 typedef ReasonVec::value_type ReasonWithData;
00662 Assignment() : front(0), elims_(0), units_(0) { }
00663 LitVec trail;
00664 LitVec::size_type front;
00665 bool qEmpty() const { return front == trail.size(); }
00666 uint32 qSize() const { return (uint32)trail.size() - front; }
00667 Literal qPop() { return trail[front++]; }
00668 void qReset() { front = trail.size(); }
00669
00671 uint32 numVars() const { return (uint32)assign_.size(); }
00673 uint32 assigned() const { return (uint32)trail.size(); }
00675 uint32 free() const { return numVars() - (assigned()+elims_); }
00677 uint32 maxLevel() const { return (1u<<28)-2; }
00679 ValueRep value(Var v) const { return ValueRep(assign_[v] & 3u); }
00681 uint32 level(Var v) const { return assign_[v] >> 4u; }
00683 bool valid(Var v) const { return (assign_[v] & elim_mask) != elim_mask; }
00685 const ValueSet pref(Var v) const { return v < pref_.size() ? pref_[v] : ValueSet(); }
00687 const Antecedent& reason(Var v)const { return reason_[v]; }
00689 uint32 numData() const { return reason_.dataSize(); }
00691 uint32 data(Var v) const { assert(v < reason_.dataSize()); return reason_.data(v); }
00692
00694 void resize(uint32 nv) {
00695 assign_.resize(nv);
00696 reason_.resize(nv);
00697 }
00699 Var addVar() {
00700 assign_.push_back(0);
00701 reason_.push_back(0);
00702 return numVars()-1;
00703 }
00705 void requestPrefs() {
00706 if (pref_.size() != assign_.size()) { pref_.resize(assign_.size()); }
00707 }
00709 void requestData(uint32 nv) {
00710 reason_.dataResize(nv);
00711 }
00713 void eliminate(Var v) {
00714 assert(value(v) == value_free && "Can not eliminate assigned var!\n");
00715 if (valid(v)) { assign_[v] = elim_mask|value_true; ++elims_; }
00716 }
00718
00722 bool assign(Literal p, uint32 lev, const Antecedent& x) {
00723 const Var v = p.var();
00724 const ValueRep val = value(v);
00725 if (val == value_free) {
00726 assert(valid(v));
00727 assign_[v] = (lev<<4) + trueValue(p);
00728 reason_[v] = x;
00729 trail.push_back(p);
00730 return true;
00731 }
00732 return val == trueValue(p);
00733 }
00734 bool assign(Literal p, uint32 lev, Constraint* c, uint32 data) {
00735 const Var v = p.var();
00736 const ValueRep val = value(v);
00737 if (val == value_free) {
00738 assert(valid(v));
00739 assign_[v] = (lev<<4) + trueValue(p);
00740 reason_[v] = c;
00741 reason_.setData(v, data);
00742 trail.push_back(p);
00743 return true;
00744 }
00745 return val == trueValue(p);
00746 }
00748
00752 void undoTrail(LitVec::size_type first, bool save) {
00753 if (!save) { popUntil<&Assignment::clear>(trail[first]); }
00754 else { requestPrefs(); popUntil<&Assignment::saveAndClear>(trail[first]); }
00755 qReset();
00756 }
00758 void undoLast() { clear(trail.back().var()); trail.pop_back(); }
00760 Literal last() const { return trail.back(); }
00761 Literal&last() { return trail.back(); }
00768 uint32 units() const { return units_; }
00769 bool seen(Var v, uint8 m) const { return (assign_[v] & (m<<2)) != 0; }
00770 void setSeen(Var v, uint8 m) { assign_[v] |= (m<<2); }
00771 void clearSeen(Var v) { assign_[v] &= ~uint32(12); }
00772 void clearValue(Var v) { assign_[v] &= ~uint32(3); }
00773 void setValue(Var v, ValueRep val) {
00774 assert(value(v) == val || value(v) == value_free);
00775 assign_[v] |= val;
00776 }
00777 void setReason(Var v, const Antecedent& a) { reason_[v] = a; }
00778 void setData(Var v, uint32 data) { reason_.setData(v, data); }
00779 void setPref(Var v, ValueSet::Value which, ValueRep to) { pref_[v].set(which, to); }
00780 void copyAssignment(Assignment& o) const { o.assign_ = assign_; }
00781 bool markUnits() { while (units_ != front) { setSeen(trail[units_++].var(), 3u); } return true; }
00782 void setUnits(uint32 ts) { units_ = ts; }
00784 private:
00785 static const uint32 elim_mask = uint32(0xFFFFFFF0u);
00786 Assignment(const Assignment&);
00787 Assignment& operator=(const Assignment&);
00788 void clear(Var v) { assign_[v]= 0; }
00789 void saveAndClear(Var v) { pref_[v].save(value(v)); clear(v); }
00790 template <void (Assignment::*op)(Var v)>
00791 void popUntil(Literal stop) {
00792 Literal p;
00793 do {
00794 p = trail.back(); trail.pop_back();
00795 (this->*op)(p.var());
00796 } while (p != stop);
00797 }
00798 AssignVec assign_;
00799 ReasonVec reason_;
00800 PrefVec pref_;
00801 uint32 elims_;
00802 uint32 units_;
00803 };
00804
00806 struct ImpliedLiteral {
00807 typedef Assignment::ReasonWithData AnteInfo;
00808 ImpliedLiteral(Literal a_lit, uint32 a_level, const Antecedent& a_ante, uint32 a_data = UINT32_MAX)
00809 : lit(a_lit)
00810 , level(a_level)
00811 , ante(a_ante, a_data) {
00812 }
00813 Literal lit;
00814 uint32 level;
00815 AnteInfo ante;
00816 };
00818 struct ImpliedList {
00819 typedef PodVector<ImpliedLiteral>::type VecType;
00820 typedef VecType::const_iterator iterator;
00821 ImpliedList() : level(0), front(0) {}
00823 ImpliedLiteral* find(Literal p) {
00824 for (uint32 i = 0, end = lits.size(); i != end; ++i) {
00825 if (lits[i].lit == p) { return &lits[i]; }
00826 }
00827 return 0;
00828 }
00830 void add(uint32 dl, const ImpliedLiteral& n) {
00831 if (dl > level) { level = dl; }
00832 lits.push_back(n);
00833 }
00835 bool active(uint32 dl) const { return dl < level && front != lits.size(); }
00837 bool assign(Solver& s);
00838 iterator begin() const { return lits.begin(); }
00839 iterator end() const { return lits.end(); }
00840 VecType lits;
00841 uint32 level;
00842 uint32 front;
00843 };
00844
00845 struct CCMinRecursive {
00846 enum State { state_open = 0, state_poison = 1, state_removable = 2 };
00847 void init(uint32 numV) { extra.resize(numV,0); }
00848 State state(Literal p) const { return State(extra[p.var()]); }
00849 bool checkRecursive(Literal p) {
00850 if (state(p) == state_open) { p.clearWatch(); dfsStack.push_back(p); }
00851 return state(p) != state_poison;
00852 }
00853 void markVisited(Literal p, State st) {
00854 if (state(p) == state_open) {
00855 visited.push_back(p.var());
00856 }
00857 extra[p.var()] = static_cast<uint8>(st);
00858 }
00859 void clear() {
00860 for (; !visited.empty(); visited.pop_back()) {
00861 extra[visited.back()] = 0;
00862 }
00863 }
00864 typedef PodVector<uint8>::type DfsState;
00865 LitVec dfsStack;
00866 VarVec visited;
00867 DfsState extra;
00868 };
00870 }
00871 #endif