5.CaDiCal代码解读——CaDiCal的internal相关代码--clause.hpp--clause.cpp

  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.
    最重要的优化是在子句中“嵌入”实际的文字。这需要一个可变大小的结构，因此严格来说不符合“C”，
    但我们使用的所有编译器都支持它。另一种方法是将实际的字面值存储在其他地方，
    这不仅需要更多的内存，而且更重要的是还需要另一次内存访问，因此开销非常大。

 12 
 13 struct Clause {
 14 #ifdef LOGGING
 15   int64_t id;         // Only useful for debugging.
 16 #endif
 17 
 18   bool conditioned:1; // Tried for globally blocked clause elimination.
 19   bool covered:1;     // Already considered for covered clause elimination.
 20   bool enqueued:1;    // Enqueued on backward queue.
 21   bool frozen:1;      // Temporarily frozen (in covered clause elimination).
 22   bool garbage:1;     // can be garbage collected unless it is a ‘reason‘
 23   bool gate:1 ;       // Clause part of a gate (function definition).
 24   bool hyper:1;       // redundant hyper binary or ternary resolved
 25   bool instantiated:1;// tried to instantiate
 26   bool keep:1;        // always keep this clause (if redundant)
 27   bool moved:1;       // moved during garbage collector (‘copy‘ valid)
 28   bool reason:1;      // reason / antecedent clause can not be collected
 29   bool redundant:1;   // aka ‘learned‘ so not ‘irredundant‘ (original)
 30   bool transred:1;    // already checked for transitive reduction
 31   bool subsume:1;     // not checked in last subsumption round
 32   unsigned used:2;    // resolved in conflict analysis since last ‘reduce‘
 33   bool vivified:1;    // clause already vivified
 34   bool vivify:1;      // clause scheduled to be vivified
 35 
 36   // The glucose level (‘LBD‘ or short ‘glue‘) is a heuristic value for the
 37   // expected usefulness of a learned clause, where smaller glue is consider
 38   // more useful.  During learning the ‘glue‘ is determined as the number of
 39   // decisions in the learned clause.  Thus the glue of a clause is a strict
 40   // upper limit on the smallest number of decisions needed to make it
 41   // propagate.  For instance a binary clause will propagate if one of its
 42   // literals is set to false.  Similarly a learned clause with glue 1 can
 43   // propagate after one decision, one with glue 2 after 2 decisions etc.
 44   // In some sense the glue is an abstraction of the size of the clause.
 45   //
 46   // See the IJCAI‘09 paper by Audemard & Simon for more details.  We
 47   // switched back and forth between keeping the glue stored in a clause and
 48   // using it only initially to determine whether it is kept, that is
 49   // survives clause reduction.  The latter strategy is not bad but also
 50   // does not allow to use glue values for instance in ‘reduce‘.
 51   //
 52   // More recently we also update the glue and promote clauses to lower
 53   // level tiers during conflict analysis.  The idea of using three tiers is
 54   // also due to Chanseok Oh and thus used in all recent ‘Maple...‘ solvers.
 55   // Tier one are the always kept clauses with low glue at most
 56   // ‘opts.reducetier1glue‘ (default ‘2‘). The second tier contains all
 57   // clauses with glue larger than ‘opts.reducetier1glue‘ but smaller or
 58   // equal than ‘opts.reducetier2glue‘ (default ‘6‘).  The third tier
 59   // consists of clauses with glue larger than ‘opts.reducetier2glue‘.
 60   //
 61   // Clauses in tier one are not deleted in ‘reduce‘. Clauses in tier
 62   // two require to be unused in two consecutive ‘reduce‘ intervals before
 63   // being collected while for clauses in tier three not being used since
 64   // the last ‘reduce‘ call makes them deletion candidates.  Clauses derived
 65   // by hyper binary or ternary resolution (even though small and thus with
 66   // low glue) are always removed if they remain unused during one interval.
 67   // See ‘mark_useless_redundant_clauses_as_garbage‘ in ‘reduce.cpp‘ and
 68   // ‘bump_clause‘ in ‘analyze.cpp‘.
 69   //
 70   int glue;
 71 
 72   int size;         // Actual size of ‘literals‘ (at least 2).
 73   int pos;          // Position of last watch replacement [Gent‘13].
 74 
 75   union {
 76 
 77     int literals[2];    // Of variadic ‘size‘ (shrunken if strengthened).
 78 
 79     Clause * copy;      // Only valid if ‘moved‘, then that‘s where to.
 80     //
 81     // The ‘copy‘ field is only valid for ‘moved‘ clauses in the moving
 82     // garbage collector ‘copy_non_garbage_clauses‘ for keeping clauses
 83     // compactly in a contiguous memory arena.  Otherwise, most of
 84     // the time, ‘literals‘ is valid.  See ‘collect.cpp‘ for details.
 85   };
 86 
 87   literal_iterator       begin ()       { return literals; }
 88   literal_iterator         end ()       { return literals + size; }
 89 
 90   const_literal_iterator begin () const { return literals; }
 91   const_literal_iterator   end () const { return literals + size; }
 92 
 93   static size_t bytes (int size) {
 94 
 95     // Memory sanitizer insists that clauses put into consecutive memory in
 96     // the arena are still 8 byte aligned.  We could also allocate 8 byte
 97     // aligned memory there.  However, assuming the real memory foot print
 98     // of a clause is 8 bytes anyhow, we just allocate 8 byte aligned memory
 99     // all the time (even if allocated outside of the arena).
100     //
101     assert (size > 1);
102     return align ((size - 2) * sizeof (int) + sizeof (Clause), 8);
103   }
104 
105   size_t bytes () const { return bytes (size); }
106 
107   // Check whether this clause is ready to be collected and deleted.  The
108   // ‘reason‘ flag is only there to protect reason clauses in ‘reduce‘,
109   // which does not backtrack to the root level.  If garbage collection is
110   // triggered from a preprocessor, which backtracks to the root level, then
111   // ‘reason‘ is false for sure. We want to use the same garbage collection
112   // code though for both situations and thus hide here this variance.
113   //
114   bool collect () const { return !reason && garbage; }
115 };

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 };

  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 }

/*------------------------------------------------------------------------*/

// 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);  
     // Internal数据成员clause中包含从cnf文件读入的子句
 4   const int size = (int) clause.size ();
 5   assert (size >= 2);
 6 
 7   if (glue > size) glue = size;
 8 
 9   // Determine whether this clauses should be kept all the time.
10   // 译文：确定这些条款是否应该一直保留
11   bool keep;
12   if (!red) keep = true;
13   else if (glue <= opts.reducetier1glue) keep = true;
14   else keep = false;
15 
16   size_t bytes = Clause::bytes (size);
17   Clause * c = (Clause *) new char[bytes];
18 
19   stats.added.total++;
20 #ifdef LOGGING
21   c->id = stats.added.total;
22 #endif
23 
24   c->conditioned = false;
25   c->covered = false;
26   c->enqueued = false;
27   c->frozen = false;
28   c->garbage = false;
29   c->gate = false;
30   c->hyper = false;
31   c->instantiated = false;
32   c->keep = keep;
33   c->moved = false;
34   c->reason = false;
35   c->redundant = red;//参数red标定该子句是否是学习子句
36   c->transred = false;
37   c->subsume = false;
38   c->vivified = false;
39   c->vivify = false;
40   c->used = 0;
41 
42   c->glue = glue;
43   c->size = size;
44   c->pos = 2;
45 
46   for (int i = 0; i < size; i++) c->literals[i] = clause[i];
47 
48   // Just checking that we did not mess up our sophisticated memory layout.
49   // This might be compiler dependent though. Crucial for correctness.
50   //
51   assert (c->bytes () == bytes);
52 
53   stats.current.total++;
54   stats.added.total++;
55 
56   if (red) {
57     stats.current.redundant++;
58     stats.added.redundant++;
59   } else {
60     stats.irrbytes += bytes;
61     stats.current.irredundant++;
62     stats.added.irredundant++;
63   }
64 
65   clauses.push_back (c);
66   LOG (c, "new pointer %p", c);
67 
68   if (likely_to_be_kept_clause (c)) mark_added (c);
69 
70   return c;
71 }

 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 }