标签:next factor orm gen 计数 alt size mem numbers
clause.hpp
clause.cpp
clause.hpp
声明了常用类型的别名:
/*------------------------------------------------------------------------*/ typedef int * literal_iterator; /*------------------------------------------------------------------------*/ |
|
定义结构类型Clause、clause_smaller_size、clause_lit_less_than
1 // The ‘Clause‘ data structure is very important. There are usually many 2 // clauses and accessing them is a hot-spot. Thus we use common 3 // optimizations to reduce memory and improve cache usage, even though this 4 // induces some complexity in understanding the code. 5 // 6 // The most important optimization is to ‘embed‘ the actual literals in the 7 // clause. This requires a variadic size structure and thus strictly is not 8 // ‘C‘ conform, but supported by all compilers we used. The alternative is 9 // to store the actual literals somewhere else, which not only needs more 10 // memory but more importantly also requires another memory access and thus 11 // is very costly.
|
|
1 struct clause_smaller_size { 2 bool operator () (const Clause * a, const Clause * b) { 3 return a->size < b->size; 4 } 5 }; |
|
1 // Place literals over the same variable close to each other. This would 2 // allow eager removal of identical literals and detection of tautological 3 // clauses but is only currently used for better logging (see also 4 // ‘opts.logsort‘ in ‘logging.cpp‘). 5 6 struct clause_lit_less_than { 7 bool operator () (int a, int b) const { 8 int s = abs (a), t = abs (b); 9 return s < t || (s == t && a < b); 10 } 11 }; |
|
关于Clause属性的解读
一、 | 布尔型的数据成员——记录子句的状态 |
1. bool conditioned:1; // Tried for globally blocked clause elimination. 尝试消除全局阻塞子句
2. 已考虑消除
3. 在回溯队列中排队
4. 冻结(适用子句消除)。
5. 可以被垃圾收集,除非是“reason”子句
6. 译文:门的子句(函数定义)
7. 译文:冗余超二进制或三元分解
8. 试图实例化
9. 总是保留这个条款(如果多余的话)
10. 在垃圾回收期间移动(‘copy‘有效)
11. 译文:原因/先行条款不能收取
12. 译文:也就是" learned "而不是" irredundant "(原文)
13. 译文:已检查传递约简
14. 译文:上一轮归结没有登记
15.
16. |
|
二、 | 表示具体数值的数据成员------表示状态的计数等 |
1. 译文:在冲突分析中解决,自上次“减少”以来
2. int glue;
3. int size; // Actual size of ‘literals‘ (at least 2).
4. |
|
三、 | 子句中相关文字的数据成员 |
union { int literals[2]; // Of variadic ‘size‘ (shrunken if strengthened). 可变尺寸(增强后缩小) Clause * copy; // Only valid if ‘moved‘, then that‘s where to. “copy”字段仅对移动垃圾收集器“copy_non_garbage_clauses”中的“moved”子句有效,用于将子句紧凑地保存在一个连续的内存竞技场中。否则,大多数时候,“literals”是有效的。细节见‘collect.cpp‘ .
|
|
关于Clause类型的操作函数的解读
注: Clause类型有很多数据成员,缺没有针对他们的访问操作函数;也没有声明一个友元类?——结构体默认公有访问权限
1 |
literal_iterator begin () { return literals; } const_literal_iterator begin () const { return literals; } 以上访问子句中文字所在位置,用整型指针表示; |
2 |
两个重载的函数bytes
static size_t bytes (int size) { // Memory sanitizer insists that clauses put into consecutive memory in 该函数返回子句的字节数;调用宏align,按8或8的倍数对齐计算, 如7则按8算;13则按16算;
size_t bytes () const { return bytes (size); } // Check whether this clause is ready to be collected and deleted. The |
3 | bool collect () const { return !reason && garbage; } |
Clause.cpp函数并不对应类型声明的定义代码,这里收集了关于子句被操作的函数,这些函数是分属于不同的类的成员函数。
1.完整函数代码
10-26行中的若干for语句很雷人!!!
1 #include "internal.hpp" 2 3 namespace CaDiCaL { 4 5 /*------------------------------------------------------------------------*/ 6 7 // Signed marking or unmarking of a clause or the global ‘clause‘. 8 9 void Internal::mark (Clause * c) { 10 for (const auto & lit : *c) mark (lit); 11 } 12 13 void Internal::mark2 (Clause * c) { 14 for (const auto & lit : *c) mark2 (lit); 15 } 16 17 void Internal::unmark (Clause * c) { 18 for (const auto & lit : *c) unmark (lit); 19 } 20 21 void Internal::mark_clause () { 22 for (const auto & lit : clause) mark (lit); 23 } 24 25 void Internal::unmark_clause () { 26 for (const auto & lit : clause) unmark (lit); 27 } 28 29 /*------------------------------------------------------------------------*/ 30 31 // Mark the variables of an irredundant clause to ‘have been removed‘, which 32 // will trigger these variables to be considered again in the next bounded 33 // variable elimination phase. This is called from ‘mark_garbage‘ below. 34 // Note that ‘mark_removed (int lit)‘ will also mark the blocking flag of 35 // ‘-lit‘ to trigger reconsidering blocking clauses on ‘-lit‘. 36 37 void Internal::mark_removed (Clause * c, int except) { 38 LOG (c, "marking removed"); 39 assert (!c->redundant); 40 for (const auto & lit : *c) 41 if (lit != except) 42 mark_removed (lit); 43 } 44 45 // Mark the variables of a (redundant or irredundant) clause to ‘have been 46 // added‘, which triggers clauses with such a variables, to be considered 47 // both as a subsumed or subsuming clause in the next subsumption phase. 48 // This function is called from ‘new_clause‘ below as well as in situations 49 // where a clause is shrunken (and thus needs to be at least considered 50 // again to subsume a larger clause). We also use this to tell 51 // ‘ternary‘ preprocessing reconsider clauses on an added literal as well as 52 // trying to block clauses on it. 53 54 inline void Internal::mark_added (int lit, int size, bool redundant) { 55 mark_subsume (lit); 56 if (size == 3) 57 mark_ternary (lit); 58 if (!redundant) 59 mark_block (lit); 60 } 61 62 void Internal::mark_added (Clause * c) { 63 LOG (c, "marking added"); 64 assert (likely_to_be_kept_clause (c)); 65 for (const auto & lit : *c) 66 mark_added (lit, c->size, c->redundant); 67 } 68 69 /*------------------------------------------------------------------------*/ 70 71 Clause * Internal::new_clause (bool red, int glue) { 72 73 assert (clause.size () <= (size_t) INT_MAX); 74 const int size = (int) clause.size (); 75 assert (size >= 2); 76 77 if (glue > size) glue = size; 78 79 // Determine whether this clauses should be kept all the time. 80 // 81 bool keep; 82 if (!red) keep = true; 83 else if (glue <= opts.reducetier1glue) keep = true; 84 else keep = false; 85 86 size_t bytes = Clause::bytes (size); 87 Clause * c = (Clause *) new char[bytes]; 88 89 stats.added.total++; 90 #ifdef LOGGING 91 c->id = stats.added.total; 92 #endif 93 94 c->conditioned = false; 95 c->covered = false; 96 c->enqueued = false; 97 c->frozen = false; 98 c->garbage = false; 99 c->gate = false; 100 c->hyper = false; 101 c->instantiated = false; 102 c->keep = keep; 103 c->moved = false; 104 c->reason = false; 105 c->redundant = red; 106 c->transred = false; 107 c->subsume = false; 108 c->vivified = false; 109 c->vivify = false; 110 c->used = 0; 111 112 c->glue = glue; 113 c->size = size; 114 c->pos = 2; 115 116 for (int i = 0; i < size; i++) c->literals[i] = clause[i]; 117 118 // Just checking that we did not mess up our sophisticated memory layout. 119 // This might be compiler dependent though. Crucial for correctness. 120 // 121 assert (c->bytes () == bytes); 122 123 stats.current.total++; 124 stats.added.total++; 125 126 if (red) { 127 stats.current.redundant++; 128 stats.added.redundant++; 129 } else { 130 stats.irrbytes += bytes; 131 stats.current.irredundant++; 132 stats.added.irredundant++; 133 } 134 135 clauses.push_back (c); 136 LOG (c, "new pointer %p", c); 137 138 if (likely_to_be_kept_clause (c)) mark_added (c); 139 140 return c; 141 } 142 143 /*------------------------------------------------------------------------*/ 144 145 void Internal::promote_clause (Clause * c, int new_glue) { 146 assert (c->redundant); 147 if (c->keep) return; 148 if (c->hyper) return; 149 int old_glue = c->glue; 150 if (new_glue >= old_glue) return; 151 if (!c->keep && new_glue <= opts.reducetier1glue) { 152 LOG (c, "promoting with new glue %d to tier1", new_glue); 153 stats.promoted1++; 154 c->keep = true; 155 } else if (old_glue > opts.reducetier2glue && 156 new_glue <= opts.reducetier2glue) { 157 LOG (c, "promoting with new glue %d to tier2", new_glue); 158 stats.promoted2++; 159 c->used = 2; 160 } else if (c->keep) 161 LOG (c, "keeping with new glue %d in tier1", new_glue); 162 else if (old_glue <= opts.reducetier2glue) 163 LOG (c, "keeping with new glue %d in tier2", new_glue); 164 else 165 LOG (c, "keeping with new glue %d in tier3", new_glue); 166 stats.improvedglue++; 167 c->glue = new_glue; 168 } 169 170 /*------------------------------------------------------------------------*/ 171 172 // Shrinking a clause, e.g., removing one or more literals, requires to fix 173 // the ‘pos‘ field, if it exists and points after the new last literal, has 174 // to adjust the global statistics counter of allocated bytes for 175 // irredundant clauses, and also adjust the glue value of redundant clauses 176 // if the size becomes smaller than the glue. Also mark the literals in the 177 // resulting clause as ‘added‘. The result is the number of (aligned) 178 // removed bytes, resulting from shrinking the clause. 179 // 180 size_t Internal::shrink_clause (Clause * c, int new_size) { 181 182 assert (new_size >= 2); 183 assert (new_size < c->size); 184 #ifndef NDEBUG 185 for (int i = c->size; i < new_size; i++) 186 c->literals[i] = 0; 187 #endif 188 189 if (c->pos >= new_size) c->pos = 2; 190 191 size_t old_bytes = c->bytes (); 192 c->size = new_size; 193 size_t new_bytes = c->bytes (); 194 size_t res = old_bytes - new_bytes; 195 196 if (c->redundant) promote_clause (c, min (c->size-1, c->glue)); 197 else if (old_bytes > new_bytes) { 198 assert (stats.irrbytes >= (int64_t) res); 199 stats.irrbytes -= res; 200 } 201 202 if (likely_to_be_kept_clause (c)) mark_added (c); 203 204 return res; 205 } 206 207 // This is the ‘raw‘ deallocation of a clause. If the clause is in the 208 // arena nothing happens. If the clause is not in the arena its memory is 209 // reclaimed immediately. 210 211 void Internal::deallocate_clause (Clause * c) { 212 char * p = (char*) c; 213 if (arena.contains (p)) return; 214 LOG (c, "deallocate pointer %p", c); 215 delete [] p; 216 } 217 218 void Internal::delete_clause (Clause * c) { 219 LOG (c, "delete pointer %p", c); 220 size_t bytes = c->bytes (); 221 stats.collected += bytes; 222 if (c->garbage) { 223 assert (stats.garbage >= (int64_t) bytes); 224 stats.garbage -= bytes; 225 226 // See the discussion in ‘propagate‘ on avoiding to eagerly trace binary 227 // clauses as deleted (produce ‘d ...‘ lines) as soon they are marked 228 // garbage. We avoid this and only trace them as deleted when they are 229 // actually deleted here. This allows the solver to propagate binary 230 // garbage clauses without producing incorrect ‘d‘ lines. The effect 231 // from the proof perspective is that the deletion of these binary 232 // clauses occurs later in the proof file. 233 // 234 if (proof && c->size == 2) 235 proof->delete_clause (c); 236 } 237 deallocate_clause (c); 238 } 239 240 // We want to eagerly update statistics as soon clauses are marked garbage. 241 // Otherwise ‘report‘ for instance gives wrong numbers after ‘subsume‘ 242 // before the next ‘reduce‘. Thus we factored out marking and accounting 243 // for garbage clauses. 244 // 245 // Eagerly deleting clauses instead is problematic, since references to these 246 // clauses need to be flushed, which is too costly to do eagerly. 247 // 248 // We also update garbage statistics at this point. This helps to 249 // determine whether the garbage collector should be called during for 250 // instance bounded variable elimination, which usually generates lots of 251 // garbage clauses. 252 // 253 // In order not to miss any update to these clause statistics we call 254 // ‘check_clause_stats‘ after garbage collection in debugging mode. 255 // 256 void Internal::mark_garbage (Clause * c) { 257 258 assert (!c->garbage); 259 260 // Delay tracing deletion of binary clauses. See the discussion above in 261 // ‘delete_clause‘ and also in ‘propagate‘. 262 // 263 if (proof && c->size != 2) 264 proof->delete_clause (c); 265 266 assert (stats.current.total > 0); 267 stats.current.total--; 268 269 size_t bytes = c->bytes (); 270 if (c->redundant) { 271 assert (stats.current.redundant > 0); 272 stats.current.redundant--; 273 } else { 274 assert (stats.current.irredundant > 0); 275 stats.current.irredundant--; 276 assert (stats.irrbytes >= (int64_t) bytes); 277 stats.irrbytes -= bytes; 278 mark_removed (c); 279 } 280 stats.garbage += bytes; 281 c->garbage = true; 282 c->used = 0; 283 284 LOG (c, "marked garbage pointer %p", c); 285 } 286 287 /*------------------------------------------------------------------------*/ 288 289 // Almost the same function as ‘search_assign‘ except that we do not pretend 290 // to learn a new unit clause (which was confusing in log files). 291 292 void Internal::assign_original_unit (int lit) { 293 assert (!level); 294 const int idx = vidx (lit); 295 assert (!vals[idx]); 296 assert (!flags (idx).eliminated ()); 297 Var & v = var (idx); 298 v.level = level; 299 v.trail = (int) trail.size (); 300 v.reason = 0; 301 const signed char tmp = sign (lit); 302 vals[idx] = tmp; 303 vals[-idx] = -tmp; 304 assert (val (lit) > 0); 305 assert (val (-lit) < 0); 306 trail.push_back (lit); 307 LOG ("original unit assign %d", lit); 308 mark_fixed (lit); 309 if (propagate ()) return; 310 LOG ("propagation of original unit results in conflict"); 311 learn_empty_clause (); 312 } 313 314 // New clause added through the API, e.g., while parsing a DIMACS file. 315 // 316 void Internal::add_new_original_clause () { 317 if (level) backtrack (); 318 LOG (original, "original clause"); 319 bool skip = false; 320 if (unsat) { 321 LOG ("skipping clause since formula already inconsistent"); 322 skip = true; 323 } else { 324 assert (clause.empty ()); 325 for (const auto & lit : original) { 326 int tmp = marked (lit); 327 if (tmp > 0) { 328 LOG ("removing duplicated literal %d", lit); 329 } else if (tmp < 0) { 330 LOG ("tautological since both %d and %d occur", -lit, lit); 331 skip = true; 332 } else { 333 mark (lit); 334 tmp = val (lit); 335 if (tmp < 0) { 336 LOG ("removing falsified literal %d", lit); 337 } else if (tmp > 0) { 338 LOG ("satisfied since literal %d true", lit); 339 skip = true; 340 } else { 341 clause.push_back (lit); 342 assert (flags (lit).status != Flags::UNUSED); 343 } 344 } 345 } 346 for (const auto & lit : original) 347 unmark (lit); 348 } 349 if (skip) { 350 if (proof) proof->delete_clause (original); 351 } else { 352 size_t size = clause.size (); 353 if (!size) { 354 if (!unsat) { 355 if (!original.size ()) VERBOSE (1, "found empty original clause"); 356 else MSG ("found falsified original clause"); 357 unsat = true; 358 } 359 } else if (size == 1) { 360 assign_original_unit (clause[0]); 361 } else { 362 Clause * c = new_clause (false); 363 watch_clause (c); 364 } 365 if (original.size () > size) { 366 external->check_learned_clause (); 367 if (proof) { 368 proof->add_derived_clause (clause); 369 proof->delete_clause (original); 370 } 371 } 372 } 373 clause.clear (); 374 } 375 376 // Add learned new clause during conflict analysis and watch it. Requires 377 // that the clause is at least of size 2, and the first two literals 378 // are assigned at the highest decision level. 379 // 380 Clause * Internal::new_learned_redundant_clause (int glue) { 381 assert (clause.size () > 1); 382 #ifndef NDEBUG 383 for (size_t i = 2; i < clause.size (); i++) 384 assert (var (clause[0]).level >= var (clause[i]).level), 385 assert (var (clause[1]).level >= var (clause[i]).level); 386 #endif 387 external->check_learned_clause (); 388 Clause * res = new_clause (true, glue); 389 if (proof) proof->add_derived_clause (res); 390 assert (watching ()); 391 watch_clause (res); 392 return res; 393 } 394 395 // Add hyper binary resolved clause during ‘probing‘. 396 // 397 Clause * Internal::new_hyper_binary_resolved_clause (bool red, int glue) { 398 external->check_learned_clause (); 399 Clause * res = new_clause (red, glue); 400 if (proof) proof->add_derived_clause (res); 401 assert (watching ()); 402 watch_clause (res); 403 return res; 404 } 405 406 // Add hyper ternary resolved clause during ‘ternary‘. 407 // 408 Clause * Internal::new_hyper_ternary_resolved_clause (bool red) { 409 external->check_learned_clause (); 410 size_t size = clause.size (); 411 Clause * res = new_clause (red, size); 412 if (proof) proof->add_derived_clause (res); 413 assert (!watching ()); 414 return res; 415 } 416 417 // Add a new clause with same glue and redundancy as ‘orig‘ but literals are 418 // assumed to be in ‘clause‘ in ‘decompose‘ and ‘vivify‘. 419 // 420 Clause * Internal::new_clause_as (const Clause * orig) { 421 external->check_learned_clause (); 422 const int new_glue = orig->glue; 423 Clause * res = new_clause (orig->redundant, new_glue); 424 assert (!orig->redundant || !orig->keep || res->keep); 425 if (proof) proof->add_derived_clause (res); 426 assert (watching ()); 427 watch_clause (res); 428 return res; 429 } 430 431 // Add resolved clause during resolution, e.g., bounded variable 432 // elimination, but do not connect its occurrences here. 433 // 434 Clause * Internal::new_resolved_irredundant_clause () { 435 external->check_learned_clause (); 436 Clause * res = new_clause (false); 437 if (proof) proof->add_derived_clause (res); 438 assert (!watching ()); 439 return res; 440 } 441 442 }
|
|
2.分段解析
一、 | 有关子句mark操作函数 |
/*------------------------------------------------------------------------*/ // Signed marking or unmarking of a clause or the global ‘clause‘. void Internal::mark (Clause * c) { for (const auto & lit : *c) mark (lit); } void Internal::mark2 (Clause * c) { for (const auto & lit : *c) mark2 (lit); } void Internal::unmark (Clause * c) { for (const auto & lit : *c) unmark (lit); } void Internal::mark_clause () { for (const auto & lit : clause) mark (lit); } void Internal::unmark_clause () { for (const auto & lit : clause) unmark (lit); } /*------------------------------------------------------------------------*/ // Mark the variables of an irredundant clause to ‘have been removed‘, which // will trigger these variables to be considered again in the next bounded // variable elimination phase. This is called from ‘mark_garbage‘ below. // Note that ‘mark_removed (int lit)‘ will also mark the blocking flag of // ‘-lit‘ to trigger reconsidering blocking clauses on ‘-lit‘. void Internal::mark_removed (Clause * c, int except) { LOG (c, "marking removed"); assert (!c->redundant); for (const auto & lit : *c) if (lit != except) mark_removed (lit); } // Mark the variables of a (redundant or irredundant) clause to ‘have been // added‘, which triggers clauses with such a variables, to be considered // both as a subsumed or subsuming clause in the next subsumption phase. // This function is called from ‘new_clause‘ below as well as in situations // where a clause is shrunken (and thus needs to be at least considered // again to subsume a larger clause). We also use this to tell // ‘ternary‘ preprocessing reconsider clauses on an added literal as well as // trying to block clauses on it. inline void Internal::mark_added (int lit, int size, bool redundant) { mark_subsume (lit); if (size == 3) mark_ternary (lit); if (!redundant) mark_block (lit); } void Internal::mark_added (Clause * c) { LOG (c, "marking added"); assert (likely_to_be_kept_clause (c)); for (const auto & lit : *c) mark_added (lit, c->size, c->redundant); } /*------------------------------------------------------------------------*/
|
|
二、 | 子句构建 |
1 Clause * Internal::new_clause (bool red, int glue) { 2 3 assert (clause.size () <= (size_t) INT_MAX);
|
|
三 | 子句提升、沉降 和 删除与内存释放 |
1 void Internal::promote_clause (Clause * c, int new_glue) { 2 assert (c->redundant); 3 if (c->keep) return; 4 if (c->hyper) return; 5 int old_glue = c->glue; 6 if (new_glue >= old_glue) return; 7 if (!c->keep && new_glue <= opts.reducetier1glue) { 8 LOG (c, "promoting with new glue %d to tier1", new_glue); 9 stats.promoted1++; 10 c->keep = true; 11 } else if (old_glue > opts.reducetier2glue && 12 new_glue <= opts.reducetier2glue) { 13 LOG (c, "promoting with new glue %d to tier2", new_glue); 14 stats.promoted2++; 15 c->used = 2; 16 } else if (c->keep) 17 LOG (c, "keeping with new glue %d in tier1", new_glue); 18 else if (old_glue <= opts.reducetier2glue) 19 LOG (c, "keeping with new glue %d in tier2", new_glue); 20 else 21 LOG (c, "keeping with new glue %d in tier3", new_glue); 22 stats.improvedglue++; 23 c->glue = new_glue; 24 }
|
|
1 // Shrinking a clause, e.g., removing one or more literals, requires to fix 2 // the ‘pos‘ field, if it exists and points after the new last literal, has 3 // to adjust the global statistics counter of allocated bytes for 4 // irredundant clauses, and also adjust the glue value of redundant clauses 5 // if the size becomes smaller than the glue. Also mark the literals in the 6 // resulting clause as ‘added‘. The result is the number of (aligned) 7 // removed bytes, resulting from shrinking the clause. 8 // 9 size_t Internal::shrink_clause (Clause * c, int new_size) { 10 11 assert (new_size >= 2); 12 assert (new_size < c->size); 13 #ifndef NDEBUG 14 for (int i = c->size; i < new_size; i++) 15 c->literals[i] = 0; 16 #endif 17 18 if (c->pos >= new_size) c->pos = 2; 19 20 size_t old_bytes = c->bytes (); 21 c->size = new_size; 22 size_t new_bytes = c->bytes (); 23 size_t res = old_bytes - new_bytes; 24 25 if (c->redundant) promote_clause (c, min (c->size-1, c->glue)); 26 else if (old_bytes > new_bytes) { 27 assert (stats.irrbytes >= (int64_t) res); 28 stats.irrbytes -= res; 29 } 30 31 if (likely_to_be_kept_clause (c)) mark_added (c); 32 33 return res; 34 }
|
|
1 // This is the ‘raw‘ deallocation of a clause. If the clause is in the 2 // arena nothing happens. If the clause is not in the arena its memory is 3 // reclaimed immediately. 4 5 void Internal::deallocate_clause (Clause * c) { 6 char * p = (char*) c; 7 if (arena.contains (p)) return; 8 LOG (c, "deallocate pointer %p", c); 9 delete [] p; 10 } 11 12 void Internal::delete_clause (Clause * c) { 13 LOG (c, "delete pointer %p", c); 14 size_t bytes = c->bytes (); 15 stats.collected += bytes; 16 if (c->garbage) { 17 assert (stats.garbage >= (int64_t) bytes); 18 stats.garbage -= bytes; 19 20 // See the discussion in ‘propagate‘ on avoiding to eagerly trace binary 21 // clauses as deleted (produce ‘d ...‘ lines) as soon they are marked 22 // garbage. We avoid this and only trace them as deleted when they are 23 // actually deleted here. This allows the solver to propagate binary 24 // garbage clauses without producing incorrect ‘d‘ lines. The effect 25 // from the proof perspective is that the deletion of these binary 26 // clauses occurs later in the proof file. 27 // 28 if (proof && c->size == 2) 29 proof->delete_clause (c); 30 } 31 deallocate_clause (c); 32 } 33 34 // We want to eagerly update statistics as soon clauses are marked garbage. 35 // Otherwise ‘report‘ for instance gives wrong numbers after ‘subsume‘ 36 // before the next ‘reduce‘. Thus we factored out marking and accounting 37 // for garbage clauses. 38 // 39 // Eagerly deleting clauses instead is problematic, since references to these 40 // clauses need to be flushed, which is too costly to do eagerly. 41 // 42 // We also update garbage statistics at this point. This helps to 43 // determine whether the garbage collector should be called during for 44 // instance bounded variable elimination, which usually generates lots of 45 // garbage clauses. 46 // 47 // In order not to miss any update to these clause statistics we call 48 // ‘check_clause_stats‘ after garbage collection in debugging mode. 49 // 50 void Internal::mark_garbage (Clause * c) { 51 52 assert (!c->garbage); 53 54 // Delay tracing deletion of binary clauses. See the discussion above in 55 // ‘delete_clause‘ and also in ‘propagate‘. 56 // 57 if (proof && c->size != 2) 58 proof->delete_clause (c); 59 60 assert (stats.current.total > 0); 61 stats.current.total--; 62 63 size_t bytes = c->bytes (); 64 if (c->redundant) { 65 assert (stats.current.redundant > 0); 66 stats.current.redundant--; 67 } else { 68 assert (stats.current.irredundant > 0); 69 stats.current.irredundant--; 70 assert (stats.irrbytes >= (int64_t) bytes); 71 stats.irrbytes -= bytes; 72 mark_removed (c); 73 } 74 stats.garbage += bytes; 75 c->garbage = true; 76 c->used = 0; 77 78 LOG (c, "marked garbage pointer %p", c); 79 }
|
|
四 | 原始子句相关操作 |
1 // Almost the same function as ‘search_assign‘ except that we do not pretend 2 // to learn a new unit clause (which was confusing in log files). 3 4 void Internal::assign_original_unit (int lit) { 5 assert (!level); 6 const int idx = vidx (lit); 7 assert (!vals[idx]); 8 assert (!flags (idx).eliminated ()); 9 Var & v = var (idx); 10 v.level = level; 11 v.trail = (int) trail.size (); 12 v.reason = 0; 13 const signed char tmp = sign (lit); 14 vals[idx] = tmp; 15 vals[-idx] = -tmp; 16 assert (val (lit) > 0); 17 assert (val (-lit) < 0); 18 trail.push_back (lit); 19 LOG ("original unit assign %d", lit); 20 mark_fixed (lit); 21 if (propagate ()) return; 22 LOG ("propagation of original unit results in conflict"); 23 learn_empty_clause (); 24 }
|
|
1 // New clause added through the API, e.g., while parsing a DIMACS file. 2 // 3 void Internal::add_new_original_clause () { 4 if (level) backtrack (); 5 LOG (original, "original clause"); 6 bool skip = false; 7 if (unsat) { 8 LOG ("skipping clause since formula already inconsistent"); 9 skip = true; 10 } else { 11 assert (clause.empty ()); 12 for (const auto & lit : original) { 13 int tmp = marked (lit); 14 if (tmp > 0) { 15 LOG ("removing duplicated literal %d", lit); 16 } else if (tmp < 0) { 17 LOG ("tautological since both %d and %d occur", -lit, lit); 18 skip = true; 19 } else { 20 mark (lit); 21 tmp = val (lit); 22 if (tmp < 0) { 23 LOG ("removing falsified literal %d", lit); 24 } else if (tmp > 0) { 25 LOG ("satisfied since literal %d true", lit); 26 skip = true; 27 } else { 28 clause.push_back (lit); 29 assert (flags (lit).status != Flags::UNUSED); 30 } 31 } 32 } 33 for (const auto & lit : original) 34 unmark (lit); 35 } 36 if (skip) { 37 if (proof) proof->delete_clause (original); 38 } else { 39 size_t size = clause.size (); 40 if (!size) { 41 if (!unsat) { 42 if (!original.size ()) VERBOSE (1, "found empty original clause"); 43 else MSG ("found falsified original clause"); 44 unsat = true; 45 } 46 } else if (size == 1) { 47 assign_original_unit (clause[0]); 48 } else { 49 Clause * c = new_clause (false); 50 watch_clause (c); 51 } 52 if (original.size () > size) { 53 external->check_learned_clause (); 54 if (proof) { 55 proof->add_derived_clause (clause); 56 proof->delete_clause (original); 57 } 58 } 59 } 60 clause.clear (); 61 }
|
|
1 // Add learned new clause during conflict analysis and watch it. Requires 2 // that the clause is at least of size 2, and the first two literals 3 // are assigned at the highest decision level. 4 // 5 Clause * Internal::new_learned_redundant_clause (int glue) { 6 assert (clause.size () > 1); 7 #ifndef NDEBUG 8 for (size_t i = 2; i < clause.size (); i++) 9 assert (var (clause[0]).level >= var (clause[i]).level), 10 assert (var (clause[1]).level >= var (clause[i]).level); 11 #endif 12 external->check_learned_clause (); 13 Clause * res = new_clause (true, glue); 14 if (proof) proof->add_derived_clause (res); 15 assert (watching ()); 16 watch_clause (res); 17 return res; 18 }
|
|
1 // Add hyper binary resolved clause during ‘probing‘. 2 // 3 Clause * Internal::new_hyper_binary_resolved_clause (bool red, int glue) { 4 external->check_learned_clause (); 5 Clause * res = new_clause (red, glue); 6 if (proof) proof->add_derived_clause (res); 7 assert (watching ()); 8 watch_clause (res); 9 return res; 10 }
|
|
1 // Add hyper ternary resolved clause during ‘ternary‘. 2 // 3 Clause * Internal::new_hyper_ternary_resolved_clause (bool red) { 4 external->check_learned_clause (); 5 size_t size = clause.size (); 6 Clause * res = new_clause (red, size); 7 if (proof) proof->add_derived_clause (res); 8 assert (!watching ()); 9 return res; 10 }
|
|
1 // Add a new clause with same glue and redundancy as ‘orig‘ but literals are 2 // assumed to be in ‘clause‘ in ‘decompose‘ and ‘vivify‘. 3 // 4 Clause * Internal::new_clause_as (const Clause * orig) { 5 external->check_learned_clause (); 6 const int new_glue = orig->glue; 7 Clause * res = new_clause (orig->redundant, new_glue); 8 assert (!orig->redundant || !orig->keep || res->keep); 9 if (proof) proof->add_derived_clause (res); 10 assert (watching ()); 11 watch_clause (res); 12 return res; 13 }
|
|
1 // Add resolved clause during resolution, e.g., bounded variable 2 // elimination, but do not connect its occurrences here. 3 // 4 Clause * Internal::new_resolved_irredundant_clause () { 5 external->check_learned_clause (); 6 Clause * res = new_clause (false); 7 if (proof) proof->add_derived_clause (res); 8 assert (!watching ()); 9 return res; 10 }
|
|
5.CaDiCal代码解读——CaDiCal的internal相关代码--clause.hpp--clause.cpp
标签:next factor orm gen 计数 alt size mem numbers
原文地址:https://www.cnblogs.com/yuweng1689/p/13399372.html