libs/minisat/SimpSolver.cc

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