libs/minisat/SimpSolver.cc

   1 #ifndef __STDC_FORMAT_MACROS
   2 #define __STDC_FORMAT_MACROS
   3 #endif
   4 #ifndef __STDC_LIMIT_MACROS
   5 #define __STDC_LIMIT_MACROS
   6 #endif
   7 /***********************************************************************************[SimpSolver.cc]
   8 Copyright (c) 2006,      Niklas Een, Niklas Sorensson
   9 Copyright (c) 2007-2010, Niklas Sorensson
  10
  11 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
  12 associated documentation files (the "Software"), to deal in the Software without restriction,
  13 including without limitation the rights to use, copy, modify, merge, publish, distribute,
  14 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
  15 furnished to do so, subject to the following conditions:
  16
  17 The above copyright notice and this permission notice shall be included in all copies or
  18 substantial portions of the Software.
  19
  20 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
  21 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
  22 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
  23 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
  24 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
  25 **************************************************************************************************/
  26
  27 #include "Sort.h"
  28 #include "SimpSolver.h"
  29 #include "System.h"
  30
  31 using namespace Minisat;
  32
  33 //=================================================================================================
  34 // Options:
  35
  36
  37 static const char* _cat = "SIMP";
  38
  39 static BoolOption   opt_use_asymm        (_cat, "asymm",        "Shrink clauses by asymmetric branching.", false);
  40 static BoolOption   opt_use_rcheck       (_cat, "rcheck",       "Check if a clause is already implied. (costly)", false);
  41 static BoolOption   opt_use_elim         (_cat, "elim",         "Perform variable elimination.", true);
  42 static IntOption    opt_grow             (_cat, "grow",         "Allow a variable elimination step to grow by a number of clauses.", 0);
  43 static IntOption    opt_clause_lim       (_cat, "cl-lim",       "Variables are not eliminated if it produces a resolvent with a length above this limit. -1 means no limit", 20,   IntRange(-1, INT32_MAX));
  44 static IntOption    opt_subsumption_lim  (_cat, "sub-lim",      "Do not check if subsumption against a clause larger than this. -1 means no limit.", 1000, IntRange(-1, INT32_MAX));
  45 static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered during simplification.",  0.5, DoubleRange(0, false, HUGE_VAL, false));
  46
  47
  48 //=================================================================================================
  49 // Constructor/Destructor:
  50
  51
  52 SimpSolver::SimpSolver() :
  53     grow               (opt_grow)
  54   , clause_lim         (opt_clause_lim)
  55   , subsumption_lim    (opt_subsumption_lim)
  56   , simp_garbage_frac  (opt_simp_garbage_frac)
  57   , use_asymm          (opt_use_asymm)
  58   , use_rcheck         (opt_use_rcheck)
  59   , use_elim           (opt_use_elim)
  60   , extend_model       (true)
  61   , merges             (0)
  62   , asymm_lits         (0)
  63   , eliminated_vars    (0)
  64   , elimorder          (1)
  65   , use_simplification (true)
  66   , occurs             (ClauseDeleted(ca))
  67   , elim_heap          (ElimLt(n_occ))
  68   , bwdsub_assigns     (0)
  69   , n_touched          (0)
  70 {
  71     vec<Lit> dummy(1,lit_Undef);
  72     ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
  73     bwdsub_tmpunit        = ca.alloc(dummy);
  74     remove_satisfied      = false;
  75 }
  76
  77
  78 SimpSolver::~SimpSolver()
  79 {
  80 }
  81
  82
  83 Var SimpSolver::newVar(lbool upol, bool dvar) {
  84     Var v = Solver::newVar(upol, dvar);
  85
  86     frozen    .insert(v, (char)false);
  87     eliminated.insert(v, (char)false);
  88
  89     if (use_simplification){
  90         n_occ     .insert( mkLit(v), 0);
  91         n_occ     .insert(~mkLit(v), 0);
  92         occurs    .init  (v);
  93         touched   .insert(v, 0);
  94         elim_heap .insert(v);
  95     }
  96     return v; }
  97
  98
  99 void SimpSolver::releaseVar(Lit l)
 100 {
 101     assert(!isEliminated(var(l)));
 102     if (!use_simplification && var(l) >= max_simp_var)
 103         // Note: Guarantees that no references to this variable is
 104         // left in model extension datastructure. Could be improved!
 105         Solver::releaseVar(l);
 106     else
 107         // Otherwise, don't allow variable to be reused.
 108         Solver::addClause(l);
 109 }
 110
 111
 112 lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
 113 {
 114     vec<Var> extra_frozen;
 115     lbool    result = l_True;
 116
 117     do_simp &= use_simplification;
 118
 119     if (do_simp){
 120         // Assumptions must be temporarily frozen to run variable elimination:
 121         for (int i = 0; i < assumptions.size(); i++){
 122             Var v = var(assumptions[i]);
 123
 124             // If an assumption has been eliminated, remember it.
 125             assert(!isEliminated(v));
 126
 127             if (!frozen[v]){
 128                 // Freeze and store.
 129                 setFrozen(v, true);
 130                 extra_frozen.push(v);
 131             } }
 132
 133         result = lbool(eliminate(turn_off_simp));
 134     }
 135
 136     if (result == l_True)
 137         result = Solver::solve_();
 138     else if (verbosity >= 1)
 139         printf("===============================================================================\n");
 140
 141     if (result == l_True && extend_model)
 142         extendModel();
 143
 144     if (do_simp)
 145         // Unfreeze the assumptions that were frozen:
 146         for (int i = 0; i < extra_frozen.size(); i++)
 147             setFrozen(extra_frozen[i], false);
 148
 149     return result;
 150 }
 151
 152
 153
 154 bool SimpSolver::addClause_(vec<Lit>& ps)
 155 {
 156 #ifndef NDEBUG
 157     for (int i = 0; i < ps.size(); i++)
 158         assert(!isEliminated(var(ps[i])));
 159 #endif
 160
 161     int nclauses = clauses.size();
 162
 163     if (use_rcheck && implied(ps))
 164         return true;
 165
 166     if (!Solver::addClause_(ps))
 167         return false;
 168
 169     if (use_simplification && clauses.size() == nclauses + 1){
 170         CRef          cr = clauses.last();
 171         const Clause& c  = ca[cr];
 172
 173         // NOTE: the clause is added to the queue immediately and then
 174         // again during 'gatherTouchedClauses()'. If nothing happens
 175         // in between, it will only be checked once. Otherwise, it may
 176         // be checked twice unnecessarily. This is an unfortunate
 177         // consequence of how backward subsumption is used to mimic
 178         // forward subsumption.
 179         subsumption_queue.insert(cr);
 180         for (int i = 0; i < c.size(); i++){
 181             occurs[var(c[i])].push(cr);
 182             n_occ[c[i]]++;
 183             touched[var(c[i])] = 1;
 184             n_touched++;
 185             if (elim_heap.inHeap(var(c[i])))
 186                 elim_heap.increase(var(c[i]));
 187         }
 188     }
 189
 190     return true;
 191 }
 192
 193
 194 void SimpSolver::removeClause(CRef cr)
 195 {
 196     const Clause& c = ca[cr];
 197
 198     if (use_simplification)
 199         for (int i = 0; i < c.size(); i++){
 200             n_occ[c[i]]--;
 201             updateElimHeap(var(c[i]));
 202             occurs.smudge(var(c[i]));
 203         }
 204
 205     Solver::removeClause(cr);
 206 }
 207
 208
 209 bool SimpSolver::strengthenClause(CRef cr, Lit l)
 210 {
 211     Clause& c = ca[cr];
 212     assert(decisionLevel() == 0);
 213     assert(use_simplification);
 214
 215     // FIX: this is too inefficient but would be nice to have (properly implemented)
 216     // if (!find(subsumption_queue, &c))
 217     subsumption_queue.insert(cr);
 218
 219     if (c.size() == 2){
 220         removeClause(cr);
 221         c.strengthen(l);
 222     }else{
 223         detachClause(cr, true);
 224         c.strengthen(l);
 225         attachClause(cr);
 226         remove(occurs[var(l)], cr);
 227         n_occ[l]--;
 228         updateElimHeap(var(l));
 229     }
 230
 231     return c.size() == 1 ? enqueue(c[0]) && propagate() == CRef_Undef : true;
 232 }
 233
 234
 235 // Returns FALSE if clause is always satisfied ('out_clause' should not be used).
 236 bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause)
 237 {
 238     merges++;
 239     out_clause.clear();
 240
 241     bool  ps_smallest = _ps.size() < _qs.size();
 242     const Clause& ps  =  ps_smallest ? _qs : _ps;
 243     const Clause& qs  =  ps_smallest ? _ps : _qs;
 244
 245     for (int i = 0; i < qs.size(); i++){
 246         if (var(qs[i]) != v){
 247             for (int j = 0; j < ps.size(); j++)
 248                 if (var(ps[j]) == var(qs[i])){
 249                     if (ps[j] == ~qs[i])
 250                         return false;
 251                     else
 252                         goto next;
 253                 }
 254             out_clause.push(qs[i]);
 255         }
 256         next:;
 257     }
 258
 259     for (int i = 0; i < ps.size(); i++)
 260         if (var(ps[i]) != v)
 261             out_clause.push(ps[i]);
 262
 263     return true;
 264 }
 265
 266
 267 // Returns FALSE if clause is always satisfied.
 268 bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)
 269 {
 270     merges++;
 271
 272     bool  ps_smallest = _ps.size() < _qs.size();
 273     const Clause& ps  =  ps_smallest ? _qs : _ps;
 274     const Clause& qs  =  ps_smallest ? _ps : _qs;
 275     const Lit*  __ps  = (const Lit*)ps;
 276     const Lit*  __qs  = (const Lit*)qs;
 277
 278     size = ps.size()-1;
 279
 280     for (int i = 0; i < qs.size(); i++){
 281         if (var(__qs[i]) != v){
 282             for (int j = 0; j < ps.size(); j++)
 283                 if (var(__ps[j]) == var(__qs[i])){
 284                     if (__ps[j] == ~__qs[i])
 285                         return false;
 286                     else
 287                         goto next;
 288                 }
 289             size++;
 290         }
 291         next:;
 292     }
 293
 294     return true;
 295 }
 296
 297
 298 void SimpSolver::gatherTouchedClauses()
 299 {
 300     if (n_touched == 0) return;
 301
 302     int i,j;
 303     for (i = j = 0; i < subsumption_queue.size(); i++)
 304         if (ca[subsumption_queue[i]].mark() == 0)
 305             ca[subsumption_queue[i]].mark(2);
 306
 307     for (i = 0; i < nVars(); i++)
 308         if (touched[i]){
 309             const vec<CRef>& cs = occurs.lookup(i);
 310             for (j = 0; j < cs.size(); j++)
 311                 if (ca[cs[j]].mark() == 0){
 312                     subsumption_queue.insert(cs[j]);
 313                     ca[cs[j]].mark(2);
 314                 }
 315             touched[i] = 0;
 316         }
 317
 318     for (i = 0; i < subsumption_queue.size(); i++)
 319         if (ca[subsumption_queue[i]].mark() == 2)
 320             ca[subsumption_queue[i]].mark(0);
 321
 322     n_touched = 0;
 323 }
 324
 325
 326 bool SimpSolver::implied(const vec<Lit>& c)
 327 {
 328     assert(decisionLevel() == 0);
 329
 330     trail_lim.push(trail.size());
 331     for (int i = 0; i < c.size(); i++)
 332         if (value(c[i]) == l_True){
 333             cancelUntil(0);
 334             return true;
 335         }else if (value(c[i]) != l_False){
 336             assert(value(c[i]) == l_Undef);
 337             uncheckedEnqueue(~c[i]);
 338         }
 339
 340     bool result = propagate() != CRef_Undef;
 341     cancelUntil(0);
 342     return result;
 343 }
 344
 345
 346 // Backward subsumption + backward subsumption resolution
 347 bool SimpSolver::backwardSubsumptionCheck(bool verbose)
 348 {
 349     int cnt = 0;
 350     int subsumed = 0;
 351     int deleted_literals = 0;
 352     assert(decisionLevel() == 0);
 353
 354     while (subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()){
 355
 356         // Empty subsumption queue and return immediately on user-interrupt:
 357         if (asynch_interrupt){
 358             subsumption_queue.clear();
 359             bwdsub_assigns = trail.size();
 360             break; }
 361
 362         // Check top-level assignments by creating a dummy clause and placing it in the queue:
 363         if (subsumption_queue.size() == 0 && bwdsub_assigns < trail.size()){
 364             Lit l = trail[bwdsub_assigns++];
 365             ca[bwdsub_tmpunit][0] = l;
 366             ca[bwdsub_tmpunit].calcAbstraction();
 367             subsumption_queue.insert(bwdsub_tmpunit); }
 368
 369         CRef    cr = subsumption_queue.peek(); subsumption_queue.pop();
 370         Clause& c  = ca[cr];
 371
 372         if (c.mark()) continue;
 373
 374         if (verbose && verbosity >= 2 && cnt++ % 1000 == 0)
 375             printf("subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue.size(), subsumed, deleted_literals);
 376
 377         assert(c.size() > 1 || value(c[0]) == l_True);    // Unit-clauses should have been propagated before this point.
 378
 379         // Find best variable to scan:
 380         Var best = var(c[0]);
 381         for (int i = 1; i < c.size(); i++)
 382             if (occurs[var(c[i])].size() < occurs[best].size())
 383                 best = var(c[i]);
 384
 385         // Search all candidates:
 386         vec<CRef>& _cs = occurs.lookup(best);
 387         CRef*       cs = (CRef*)_cs;
 388
 389         for (int j = 0; j < _cs.size(); j++)
 390             if (c.mark())
 391                 break;
 392             else if (!ca[cs[j]].mark() &&  cs[j] != cr && (subsumption_lim == -1 || ca[cs[j]].size() < subsumption_lim)){
 393                 Lit l = c.subsumes(ca[cs[j]]);
 394
 395                 if (l == lit_Undef)
 396                     subsumed++, removeClause(cs[j]);
 397                 else if (l != lit_Error){
 398                     deleted_literals++;
 399
 400                     if (!strengthenClause(cs[j], ~l))
 401                         return false;
 402
 403                     // Did current candidate get deleted from cs? Then check candidate at index j again:
 404                     if (var(l) == best)
 405                         j--;
 406                 }
 407             }
 408     }
 409
 410     return true;
 411 }
 412
 413
 414 bool SimpSolver::asymm(Var v, CRef cr)
 415 {
 416     Clause& c = ca[cr];
 417     assert(decisionLevel() == 0);
 418
 419     if (c.mark() || satisfied(c)) return true;
 420
 421     trail_lim.push(trail.size());
 422     Lit l = lit_Undef;
 423     for (int i = 0; i < c.size(); i++)
 424         if (var(c[i]) != v && value(c[i]) != l_False)
 425             uncheckedEnqueue(~c[i]);
 426         else
 427             l = c[i];
 428
 429     if (propagate() != CRef_Undef){
 430         cancelUntil(0);
 431         asymm_lits++;
 432         if (!strengthenClause(cr, l))
 433             return false;
 434     }else
 435         cancelUntil(0);
 436
 437     return true;
 438 }
 439
 440
 441 bool SimpSolver::asymmVar(Var v)
 442 {
 443     assert(use_simplification);
 444
 445     const vec<CRef>& cls = occurs.lookup(v);
 446
 447     if (value(v) != l_Undef || cls.size() == 0)
 448         return true;
 449
 450     for (int i = 0; i < cls.size(); i++)
 451         if (!asymm(v, cls[i]))
 452             return false;
 453
 454     return backwardSubsumptionCheck();
 455 }
 456
 457
 458 static void mkElimClause(vec<uint32_t>& elimclauses, Lit x)
 459 {
 460     elimclauses.push(toInt(x));
 461     elimclauses.push(1);
 462 }
 463
 464
 465 static void mkElimClause(vec<uint32_t>& elimclauses, Var v, Clause& c)
 466 {
 467     int first = elimclauses.size();
 468     int v_pos = -1;
 469
 470     // Copy clause to elimclauses-vector. Remember position where the
 471     // variable 'v' occurs:
 472     for (int i = 0; i < c.size(); i++){
 473         elimclauses.push(toInt(c[i]));
 474         if (var(c[i]) == v)
 475             v_pos = i + first;
 476     }
 477     assert(v_pos != -1);
 478
 479     // Swap the first literal with the 'v' literal, so that the literal
 480     // containing 'v' will occur first in the clause:
 481     uint32_t tmp = elimclauses[v_pos];
 482     elimclauses[v_pos] = elimclauses[first];
 483     elimclauses[first] = tmp;
 484
 485     // Store the length of the clause last:
 486     elimclauses.push(c.size());
 487 }
 488
 489
 490
 491 bool SimpSolver::eliminateVar(Var v)
 492 {
 493     assert(!frozen[v]);
 494     assert(!isEliminated(v));
 495     assert(value(v) == l_Undef);
 496
 497     // Split the occurrences into positive and negative:
 498     //
 499     const vec<CRef>& cls = occurs.lookup(v);
 500     vec<CRef>        pos, neg;
 501     for (int i = 0; i < cls.size(); i++)
 502         (find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]);
 503
 504     // Check wether the increase in number of clauses stays within the allowed ('grow'). Moreover, no
 505     // clause must exceed the limit on the maximal clause size (if it is set):
 506     //
 507     int cnt         = 0;
 508     int clause_size = 0;
 509
 510     for (int i = 0; i < pos.size(); i++)
 511         for (int j = 0; j < neg.size(); j++)
 512             if (merge(ca[pos[i]], ca[neg[j]], v, clause_size) &&
 513                 (++cnt > cls.size() + grow || (clause_lim != -1 && clause_size > clause_lim)))
 514                 return true;
 515
 516     // Delete and store old clauses:
 517     eliminated[v] = true;
 518     setDecisionVar(v, false);
 519     eliminated_vars++;
 520
 521     if (pos.size() > neg.size()){
 522         for (int i = 0; i < neg.size(); i++)
 523             mkElimClause(elimclauses, v, ca[neg[i]]);
 524         mkElimClause(elimclauses, mkLit(v));
 525     }else{
 526         for (int i = 0; i < pos.size(); i++)
 527             mkElimClause(elimclauses, v, ca[pos[i]]);
 528         mkElimClause(elimclauses, ~mkLit(v));
 529     }
 530
 531     for (int i = 0; i < cls.size(); i++)
 532         removeClause(cls[i]);
 533
 534     // Produce clauses in cross product:
 535     vec<Lit>& resolvent = add_tmp;
 536     for (int i = 0; i < pos.size(); i++)
 537         for (int j = 0; j < neg.size(); j++)
 538             if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent))
 539                 return false;
 540
 541     // Free occurs list for this variable:
 542     occurs[v].clear(true);
 543
 544     // Free watchers lists for this variable, if possible:
 545     if (watches[ mkLit(v)].size() == 0) watches[ mkLit(v)].clear(true);
 546     if (watches[~mkLit(v)].size() == 0) watches[~mkLit(v)].clear(true);
 547
 548     return backwardSubsumptionCheck();
 549 }
 550
 551
 552 bool SimpSolver::substitute(Var v, Lit x)
 553 {
 554     assert(!frozen[v]);
 555     assert(!isEliminated(v));
 556     assert(value(v) == l_Undef);
 557
 558     if (!ok) return false;
 559
 560     eliminated[v] = true;
 561     setDecisionVar(v, false);
 562     const vec<CRef>& cls = occurs.lookup(v);
 563
 564     vec<Lit>& subst_clause = add_tmp;
 565     for (int i = 0; i < cls.size(); i++){
 566         Clause& c = ca[cls[i]];
 567
 568         subst_clause.clear();
 569         for (int j = 0; j < c.size(); j++){
 570             Lit p = c[j];
 571             subst_clause.push(var(p) == v ? x ^ sign(p) : p);
 572         }
 573
 574         removeClause(cls[i]);
 575
 576         if (!addClause_(subst_clause))
 577             return ok = false;
 578     }
 579
 580     return true;
 581 }
 582
 583
 584 void SimpSolver::extendModel()
 585 {
 586     int i, j;
 587     Lit x;
 588
 589     for (i = elimclauses.size()-1; i > 0; i -= j){
 590         for (j = elimclauses[i--]; j > 1; j--, i--)
 591             if (modelValue(toLit(elimclauses[i])) != l_False)
 592                 goto next;
 593
 594         x = toLit(elimclauses[i]);
 595         model[var(x)] = lbool(!sign(x));
 596     next:;
 597     }
 598 }
 599
 600
 601 bool SimpSolver::eliminate(bool turn_off_elim)
 602 {
 603     if (!simplify())
 604         return false;
 605     else if (!use_simplification)
 606         return true;
 607
 608     // Main simplification loop:
 609     //
 610     while (n_touched > 0 || bwdsub_assigns < trail.size() || elim_heap.size() > 0){
 611
 612         gatherTouchedClauses();
 613         // printf("  ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns);
 614         if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()) &&
 615             !backwardSubsumptionCheck(true)){
 616             ok = false; goto cleanup; }
 617
 618         // Empty elim_heap and return immediately on user-interrupt:
 619         if (asynch_interrupt){
 620             assert(bwdsub_assigns == trail.size());
 621             assert(subsumption_queue.size() == 0);
 622             assert(n_touched == 0);
 623             elim_heap.clear();
 624             goto cleanup; }
 625
 626         // printf("  ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size());
 627         for (int cnt = 0; !elim_heap.empty(); cnt++){
 628             Var elim = elim_heap.removeMin();
 629
 630             if (asynch_interrupt) break;
 631
 632             if (isEliminated(elim) || value(elim) != l_Undef) continue;
 633
 634             if (verbosity >= 2 && cnt % 100 == 0)
 635                 printf("elimination left: %10d\r", elim_heap.size());
 636
 637             if (use_asymm){
 638                 // Temporarily freeze variable. Otherwise, it would immediately end up on the queue again:
 639                 bool was_frozen = frozen[elim];
 640                 frozen[elim] = true;
 641                 if (!asymmVar(elim)){
 642                     ok = false; goto cleanup; }
 643                 frozen[elim] = was_frozen; }
 644
 645             // At this point, the variable may have been set by assymetric branching, so check it
 646             // again. Also, don't eliminate frozen variables:
 647             if (use_elim && value(elim) == l_Undef && !frozen[elim] && !eliminateVar(elim)){
 648                 ok = false; goto cleanup; }
 649
 650             checkGarbage(simp_garbage_frac);
 651         }
 652
 653         assert(subsumption_queue.size() == 0);
 654     }
 655  cleanup:
 656
 657     // If no more simplification is needed, free all simplification-related data structures:
 658     if (turn_off_elim){
 659         touched  .clear(true);
 660         occurs   .clear(true);
 661         n_occ    .clear(true);
 662         elim_heap.clear(true);
 663         subsumption_queue.clear(true);
 664
 665         use_simplification    = false;
 666         remove_satisfied      = true;
 667         ca.extra_clause_field = false;
 668         max_simp_var          = nVars();
 669
 670         // Force full cleanup (this is safe and desirable since it only happens once):
 671         rebuildOrderHeap();
 672         garbageCollect();
 673     }else{
 674         // Cheaper cleanup:
 675         checkGarbage();
 676     }
 677
 678     if (verbosity >= 1 && elimclauses.size() > 0)
 679         printf("|  Eliminated clauses:     %10.2f Mb                                      |\n",
 680                double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024));
 681
 682     return ok;
 683 }
 684
 685
 686 //=================================================================================================
 687 // Garbage Collection methods:
 688
 689
 690 void SimpSolver::relocAll(ClauseAllocator& to)
 691 {
 692     if (!use_simplification) return;
 693
 694     // All occurs lists:
 695     //
 696     for (int i = 0; i < nVars(); i++){
 697         occurs.clean(i);
 698         vec<CRef>& cs = occurs[i];
 699         for (int j = 0; j < cs.size(); j++)
 700             ca.reloc(cs[j], to);
 701     }
 702
 703     // Subsumption queue:
 704     //
 705     for (int i = subsumption_queue.size(); i > 0; i--){
 706         CRef cr = subsumption_queue.peek(); subsumption_queue.pop();
 707         if (ca[cr].mark()) continue;
 708         ca.reloc(cr, to);
 709         subsumption_queue.insert(cr);
 710     }
 711
 712     // Temporary clause:
 713     //
 714     ca.reloc(bwdsub_tmpunit, to);
 715 }
 716
 717
 718 void SimpSolver::garbageCollect()
 719 {
 720     // Initialize the next region to a size corresponding to the estimated utilization degree. This
 721     // is not precise but should avoid some unnecessary reallocations for the new region:
 722     ClauseAllocator to(ca.size() - ca.wasted());
 723
 724     to.extra_clause_field = ca.extra_clause_field; // NOTE: this is important to keep (or lose) the extra fields.
 725     relocAll(to);
 726     Solver::relocAll(to);
 727     if (verbosity >= 2)
 728         printf("|  Garbage collection:   %12d bytes => %12d bytes             |\n",
 729                ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
 730     to.moveTo(ca);
 731 }