GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/minisat/simp/SimpSolver.cc Lines: 313 413 75.8 %
Date: 2021-05-22 Branches: 418 1072 39.0 %

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