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