GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/minisat/simp/SimpSolver.cc Lines: 313 413 75.8 %
Date: 2021-03-23 Branches: 418 1070 39.1 %

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 CVC4;
31
using namespace CVC4::Minisat;
32
33
//=================================================================================================
34
// Options:
35
36
37
static const char* _cat = "SIMP";
38
39
8895
static BoolOption   opt_use_asymm        (_cat, "asymm",        "Shrink clauses by asymmetric branching.", false);
40
8895
static BoolOption   opt_use_rcheck       (_cat, "rcheck",       "Check if a clause is already implied. (costly)", false);
41
8895
static BoolOption   opt_use_elim         (_cat, "elim",         "Perform variable elimination.", true);
42
8895
static IntOption    opt_grow             (_cat, "grow",         "Allow a variable elimination step to grow by a number of clauses.", 0);
43
8895
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
8895
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
8895
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
9029
SimpSolver::SimpSolver(CVC4::prop::TheoryProxy* proxy,
52
                       CVC4::context::Context* context,
53
                       CVC4::context::UserContext* userContext,
54
                       ProofNodeManager* pnm,
55
9029
                       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
9029
      use_rcheck(opt_use_rcheck && !options::unsatCores() && !pnm),
64
54004
      use_elim(options::minisatUseElim() && !enableIncremental),
65
      merges(0),
66
      asymm_lits(0),
67
      eliminated_vars(0),
68
      elimorder(1),
69
11342
      use_simplification(!enableIncremental && !options::unsatCores()
70
10979
                         && !pnm)  // TODO: turn off simplifications if
71
                                   // proofs are on initially
72
      ,
73
18058
      occurs(ClauseDeleted(ca)),
74
18058
      elim_heap(ElimLt(n_occ)),
75
      bwdsub_assigns(0),
76
72232
      n_touched(0)
77
{
78
19822
    if(options::minisatUseElim() &&
79
9029
       options::minisatUseElim.wasSetByUser() &&
80
       enableIncremental) {
81
        WarningOnce() << "Incremental mode incompatible with --minisat-elim" << std::endl;
82
    }
83
84
18058
    vec<Lit> dummy(1,lit_Undef);
85
9029
    ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
86
9029
    bwdsub_tmpunit        = ca.alloc(0, dummy);
87
9029
    remove_satisfied      = false;
88
89
    // add the initialization for all the internal variables
90
27087
    for (int i = frozen.size(); i < vardata.size(); ++ i) {
91
18058
      frozen    .push(1);
92
18058
      eliminated.push(0);
93
18058
      if (use_simplification){
94
3542
          n_occ     .push(0);
95
3542
          n_occ     .push(0);
96
3542
          occurs    .init(i);
97
3542
          touched   .push(0);
98
3542
          elim_heap .insert(i);
99
      }
100
    }
101
9029
}
102
103
104
18052
SimpSolver::~SimpSolver()
105
{
106
18052
}
107
108
109
790582
Var SimpSolver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool preRegister, bool canErase) {
110
790582
    Var v = Solver::newVar(sign, dvar, isTheoryAtom, preRegister, canErase);
111
112
790582
    if (use_simplification){
113
180209
        frozen    .push((char)(!canErase));
114
180209
        eliminated.push((char)false);
115
180209
        n_occ     .push(0);
116
180209
        n_occ     .push(0);
117
180209
        occurs    .init(v);
118
180209
        touched   .push(0);
119
180209
        elim_heap .insert(v);
120
    }
121
790582
    return v; }
122
123
124
125
12419
lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
126
{
127
24838
    if (options::minisatDumpDimacs()) {
128
      toDimacs();
129
      return l_Undef;
130
    }
131
12419
    Assert(decisionLevel() == 0);
132
133
24838
    vec<Var> extra_frozen;
134
12419
    lbool    result = l_True;
135
136
12419
    do_simp &= use_simplification;
137
138
12419
    if (do_simp){
139
        // Assumptions must be temporarily frozen to run variable elimination:
140
1744
        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
1744
        result = lbool(eliminate(turn_off_simp));
153
    }
154
155
12419
    if (result == l_True)
156
12127
        result = Solver::solve_();
157
292
    else if (verbosity >= 1)
158
1
        printf("===============================================================================\n");
159
160
12398
    if (result == l_True)
161
5953
        extendModel();
162
163
12398
    if (do_simp)
164
        // Unfreeze the assumptions that were frozen:
165
1734
        for (int i = 0; i < extra_frozen.size(); i++)
166
            setFrozen(extra_frozen[i], false);
167
168
12398
    return result;
169
}
170
171
172
173
2096335
bool SimpSolver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
174
{
175
#ifdef CVC4_ASSERTIONS
176
2096335
    if (use_simplification) {
177
757425
      for (int i = 0; i < ps.size(); i++) Assert(!isEliminated(var(ps[i])));
178
    }
179
#endif
180
181
2096335
    int nclauses = clauses_persistent.size();
182
183
2096335
    if (use_rcheck && implied(ps))
184
        return true;
185
186
2096335
    if (!Solver::addClause_(ps, removable, id))
187
1577
        return false;
188
189
2094758
    if (use_simplification && clauses_persistent.size() == nclauses + 1){
190
548804
        CRef          cr = clauses_persistent.last();
191
548804
        const Clause& c  = ca[cr];
192
193
        // NOTE: the clause is added to the queue immediately and then
194
        // again during 'gatherTouchedClauses()'. If nothing happens
195
        // in between, it will only be checked once. Otherwise, it may
196
        // be checked twice unnecessarily. This is an unfortunate
197
        // consequence of how backward subsumption is used to mimic
198
        // forward subsumption.
199
548804
        subsumption_queue.insert(cr);
200
2197937
        for (int i = 0; i < c.size(); i++){
201
1649133
            occurs[var(c[i])].push(cr);
202
1649133
            n_occ[toInt(c[i])]++;
203
1649133
            touched[var(c[i])] = 1;
204
1649133
            n_touched++;
205
1649133
            if (elim_heap.inHeap(var(c[i])))
206
1631559
                elim_heap.increase(var(c[i]));
207
        }
208
    }
209
210
2094758
    return true;
211
}
212
213
214
253888
void SimpSolver::removeClause(CRef cr)
215
{
216
253888
    const Clause& c = ca[cr];
217
253888
    Debug("minisat") << "SimpSolver::removeClause(" << c << ")" << std::endl;
218
219
253888
    if (use_simplification)
220
976515
        for (int i = 0; i < c.size(); i++){
221
722627
            n_occ[toInt(c[i])]--;
222
722627
            updateElimHeap(var(c[i]));
223
722627
            occurs.smudge(var(c[i]));
224
        }
225
226
253888
    Solver::removeClause(cr);
227
253888
}
228
229
230
98365
bool SimpSolver::strengthenClause(CRef cr, Lit l)
231
{
232
98365
    Clause& c = ca[cr];
233
98365
    Assert(decisionLevel() == 0);
234
98365
    Assert(use_simplification);
235
236
    // FIX: this is too inefficient but would be nice to have (properly implemented)
237
    // if (!find(subsumption_queue, &c))
238
98365
    subsumption_queue.insert(cr);
239
240
98365
    if (c.size() == 2){
241
9156
        removeClause(cr);
242
9156
        c.strengthen(l);
243
    }else{
244
89209
        detachClause(cr, true);
245
89209
        c.strengthen(l);
246
89209
        attachClause(cr);
247
89209
        remove(occurs[var(l)], cr);
248
89209
        n_occ[toInt(l)]--;
249
89209
        updateElimHeap(var(l));
250
    }
251
252
98365
    return c.size() == 1 ? enqueue(c[0]) && propagate(CHECK_WITHOUT_THEORY) == CRef_Undef : true;
253
}
254
255
256
// Returns FALSE if clause is always satisfied ('out_clause' should not be used).
257
154291
bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause)
258
{
259
154291
    merges++;
260
154291
    out_clause.clear();
261
262
154291
    bool  ps_smallest = _ps.size() < _qs.size();
263
154291
    const Clause& ps  =  ps_smallest ? _qs : _ps;
264
154291
    const Clause& qs  =  ps_smallest ? _ps : _qs;
265
266
337487
    for (int i = 0; i < qs.size(); i++)
267
    {
268
272986
      if (var(qs[i]) != v)
269
      {
270
881978
        for (int j = 0; j < ps.size(); j++)
271
        {
272
795845
          if (var(ps[j]) == var(qs[i]))
273
          {
274
103323
            if (ps[j] == ~qs[i])
275
89790
              return false;
276
            else
277
13533
              goto next;
278
          }
279
        }
280
86133
        out_clause.push(qs[i]);
281
      }
282
266726
    next:;
283
    }
284
285
347971
    for (int i = 0; i < ps.size(); i++)
286
283470
        if (var(ps[i]) != v)
287
218969
            out_clause.push(ps[i]);
288
289
64501
    return true;
290
}
291
292
293
// Returns FALSE if clause is always satisfied.
294
1001877
bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)
295
{
296
1001877
    merges++;
297
298
1001877
    bool  ps_smallest = _ps.size() < _qs.size();
299
1001877
    const Clause& ps  =  ps_smallest ? _qs : _ps;
300
1001877
    const Clause& qs  =  ps_smallest ? _ps : _qs;
301
1001877
    const Lit*  __ps  = (const Lit*)ps;
302
1001877
    const Lit*  __qs  = (const Lit*)qs;
303
304
1001877
    size = ps.size()-1;
305
306
2920398
    for (int i = 0; i < qs.size(); i++)
307
    {
308
2197642
      if (var(__qs[i]) != v)
309
      {
310
8688003
        for (int j = 0; j < ps.size(); j++)
311
        {
312
7646403
          if (var(__ps[j]) == var(__qs[i]))
313
          {
314
355432
            if (__ps[j] == ~__qs[i])
315
279121
              return false;
316
            else
317
76311
              goto next;
318
          }
319
        }
320
1041600
        size++;
321
      }
322
2719131
    next:;
323
    }
324
325
722756
    return true;
326
}
327
328
329
1555
void SimpSolver::gatherTouchedClauses()
330
{
331
1555
    if (n_touched == 0) return;
332
333
    int i,j;
334
485030
    for (i = j = 0; i < subsumption_queue.size(); i++)
335
484235
        if (ca[subsumption_queue[i]].mark() == 0)
336
484235
            ca[subsumption_queue[i]].mark(2);
337
338
301161
    for (i = 0; i < touched.size(); i++)
339
300366
        if (touched[i]){
340
137699
            const vec<CRef>& cs = occurs.lookup(i);
341
1936753
            for (j = 0; j < cs.size(); j++)
342
1799054
                if (ca[cs[j]].mark() == 0){
343
173236
                    subsumption_queue.insert(cs[j]);
344
173236
                    ca[cs[j]].mark(2);
345
                }
346
137699
            touched[i] = 0;
347
        }
348
349
658266
    for (i = 0; i < subsumption_queue.size(); i++)
350
657471
        if (ca[subsumption_queue[i]].mark() == 2)
351
657471
            ca[subsumption_queue[i]].mark(0);
352
353
795
    n_touched = 0;
354
}
355
356
357
bool SimpSolver::implied(const vec<Lit>& c)
358
{
359
  Assert(decisionLevel() == 0);
360
361
  trail_lim.push(trail.size());
362
  for (int i = 0; i < c.size(); i++)
363
  {
364
    if (value(c[i]) == l_True)
365
    {
366
      cancelUntil(0);
367
      return false;
368
    }
369
    else if (value(c[i]) != l_False)
370
    {
371
      Assert(value(c[i]) == l_Undef);
372
      uncheckedEnqueue(~c[i]);
373
    }
374
  }
375
376
  bool result = propagate(CHECK_WITHOUT_THEORY) != CRef_Undef;
377
  cancelUntil(0);
378
  return result;
379
}
380
381
382
// Backward subsumption + backward subsumption resolution
383
20587
bool SimpSolver::backwardSubsumptionCheck(bool verbose)
384
{
385
20587
    int cnt = 0;
386
20587
    int subsumed = 0;
387
20587
    int deleted_literals = 0;
388
20587
    Assert(decisionLevel() == 0);
389
390
1709369
    while (subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()){
391
392
        // Empty subsumption queue and return immediately on user-interrupt:
393
844403
        if (asynch_interrupt){
394
            subsumption_queue.clear();
395
            bwdsub_assigns = trail.size();
396
            break; }
397
398
        // Check top-level assignments by creating a dummy clause and placing it in the queue:
399
844403
        if (subsumption_queue.size() == 0 && bwdsub_assigns < trail.size()){
400
24886
            Lit l = trail[bwdsub_assigns++];
401
24886
            ca[bwdsub_tmpunit][0] = l;
402
24886
            ca[bwdsub_tmpunit].calcAbstraction();
403
24886
            subsumption_queue.insert(bwdsub_tmpunit); }
404
405
844403
        CRef    cr = subsumption_queue.peek(); subsumption_queue.pop();
406
844403
        Clause& c  = ca[cr];
407
408
844403
        if (c.mark()) continue;
409
410
821169
        if (verbose && verbosity >= 2 && cnt++ % 1000 == 0)
411
            printf("subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue.size(), subsumed, deleted_literals);
412
413
821169
        Assert(c.size() > 1
414
               || value(c[0]) == l_True);  // Unit-clauses should have been
415
                                           // propagated before this point.
416
417
        // Find best variable to scan:
418
821169
        Var best = var(c[0]);
419
5482442
        for (int i = 1; i < c.size(); i++)
420
4661273
            if (occurs[var(c[i])].size() < occurs[best].size())
421
813165
                best = var(c[i]);
422
423
        // Search all candidates:
424
821169
        vec<CRef>& _cs = occurs.lookup(best);
425
821169
        CRef*       cs = (CRef*)_cs;
426
427
28989737
        for (int j = 0; j < _cs.size(); j++)
428
28168580
            if (c.mark())
429
                break;
430
28168580
            else if (!ca[cs[j]].mark() &&  cs[j] != cr && (subsumption_lim == -1 || ca[cs[j]].size() < subsumption_lim)){
431
27363516
                Lit l = c.subsumes(ca[cs[j]]);
432
433
27363516
                if (l == lit_Undef)
434
141858
                    subsumed++, removeClause(cs[j]);
435
27221658
                else if (l != lit_Error){
436
98365
                    deleted_literals++;
437
438
98365
                    if (!strengthenClause(cs[j], ~l))
439
12
                        return false;
440
441
                    // Did current candidate get deleted from cs? Then check candidate at index j again:
442
98353
                    if (var(l) == best)
443
83813
                        j--;
444
                }
445
            }
446
    }
447
448
20575
    return true;
449
}
450
451
452
bool SimpSolver::asymm(Var v, CRef cr)
453
{
454
    Clause& c = ca[cr];
455
    Assert(decisionLevel() == 0);
456
457
    if (c.mark() || satisfied(c)) return true;
458
459
    trail_lim.push(trail.size());
460
    Lit l = lit_Undef;
461
    for (int i = 0; i < c.size(); i++)
462
        if (var(c[i]) != v && value(c[i]) != l_False)
463
            uncheckedEnqueue(~c[i]);
464
        else
465
            l = c[i];
466
467
    if (propagate(CHECK_WITHOUT_THEORY) != CRef_Undef){
468
        cancelUntil(0);
469
        asymm_lits++;
470
        if (!strengthenClause(cr, l))
471
            return false;
472
    }else
473
        cancelUntil(0);
474
475
    return true;
476
}
477
478
479
bool SimpSolver::asymmVar(Var v)
480
{
481
  Assert(use_simplification);
482
483
  const vec<CRef>& cls = occurs.lookup(v);
484
485
  if (value(v) != l_Undef || cls.size() == 0) return true;
486
487
  for (int i = 0; i < cls.size(); i++)
488
    if (!asymm(v, cls[i])) return false;
489
490
  return backwardSubsumptionCheck();
491
}
492
493
494
19034
static void mkElimClause(vec<uint32_t>& elimclauses, Lit x)
495
{
496
19034
    elimclauses.push(toInt(x));
497
19034
    elimclauses.push(1);
498
19034
}
499
500
501
37126
static void mkElimClause(vec<uint32_t>& elimclauses, Var v, Clause& c)
502
{
503
37126
    int first = elimclauses.size();
504
37126
    int v_pos = -1;
505
506
    // Copy clause to elimclauses-vector. Remember position where the
507
    // variable 'v' occurs:
508
177769
    for (int i = 0; i < c.size(); i++){
509
140643
        elimclauses.push(toInt(c[i]));
510
140643
        if (var(c[i]) == v)
511
37126
            v_pos = i + first;
512
    }
513
37126
    Assert(v_pos != -1);
514
515
    // Swap the first literal with the 'v' literal, so that the literal
516
    // containing 'v' will occur first in the clause:
517
37126
    uint32_t tmp = elimclauses[v_pos];
518
37126
    elimclauses[v_pos] = elimclauses[first];
519
37126
    elimclauses[first] = tmp;
520
521
    // Store the length of the clause last:
522
37126
    elimclauses.push(c.size());
523
37126
}
524
525
526
527
47450
bool SimpSolver::eliminateVar(Var v)
528
{
529
47450
  Assert(!frozen[v]);
530
47450
  Assert(!isEliminated(v));
531
47450
  Assert(value(v) == l_Undef);
532
533
  // Split the occurrences into positive and negative:
534
  //
535
47450
  const vec<CRef>& cls = occurs.lookup(v);
536
94900
  vec<CRef> pos, neg;
537
827714
  for (int i = 0; i < cls.size(); i++)
538
780264
    (find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]);
539
540
  // Check whether the increase in number of clauses stays within the allowed
541
  // ('grow'). Moreover, no clause must exceed the limit on the maximal clause
542
  // size (if it is set):
543
  //
544
47450
  int cnt = 0;
545
47450
  int clause_size = 0;
546
547
165644
  for (int i = 0; i < pos.size(); i++)
548
1120071
    for (int j = 0; j < neg.size(); j++)
549
2003754
      if (merge(ca[pos[i]], ca[neg[j]], v, clause_size)
550
1030293
          && (++cnt > cls.size() + grow
551
697005
              || (clause_lim != -1 && clause_size > clause_lim)))
552
28416
        return true;
553
554
  // Delete and store old clauses:
555
19034
  eliminated[v] = true;
556
19034
  setDecisionVar(v, false);
557
19034
  eliminated_vars++;
558
559
19034
  if (pos.size() > neg.size())
560
  {
561
16437
    for (int i = 0; i < neg.size(); i++)
562
10556
      mkElimClause(elimclauses, v, ca[neg[i]]);
563
5881
    mkElimClause(elimclauses, mkLit(v));
564
  }
565
  else
566
  {
567
39723
    for (int i = 0; i < pos.size(); i++)
568
26570
      mkElimClause(elimclauses, v, ca[pos[i]]);
569
13153
    mkElimClause(elimclauses, ~mkLit(v));
570
  }
571
572
19034
    for (int i = 0; i < cls.size(); i++) removeClause(cls[i]);
573
574
19034
    ClauseId id = ClauseIdUndef;
575
    // Produce clauses in cross product:
576
19034
    vec<Lit>& resolvent = add_tmp;
577
68983
    for (int i = 0; i < pos.size(); i++)
578
204240
        for (int j = 0; j < neg.size(); j++) {
579
154291
            bool removable = ca[pos[i]].removable() && ca[pos[neg[j]]].removable();
580
218792
            if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) &&
581
64501
                !addClause_(resolvent, removable, id)) {
582
                return false;
583
            }
584
        }
585
586
    // Free occurs list for this variable:
587
19034
    occurs[v].clear(true);
588
589
    // Free watchers lists for this variable, if possible:
590
19034
    if (watches[ mkLit(v)].size() == 0) watches[ mkLit(v)].clear(true);
591
19034
    if (watches[~mkLit(v)].size() == 0) watches[~mkLit(v)].clear(true);
592
593
19034
    return backwardSubsumptionCheck();
594
}
595
596
597
bool SimpSolver::substitute(Var v, Lit x)
598
{
599
  Assert(!frozen[v]);
600
  Assert(!isEliminated(v));
601
  Assert(value(v) == l_Undef);
602
603
  if (!ok) return false;
604
605
  eliminated[v] = true;
606
  setDecisionVar(v, false);
607
  const vec<CRef>& cls = occurs.lookup(v);
608
609
  vec<Lit>& subst_clause = add_tmp;
610
  for (int i = 0; i < cls.size(); i++)
611
  {
612
    Clause& c = ca[cls[i]];
613
614
    subst_clause.clear();
615
    for (int j = 0; j < c.size(); j++)
616
    {
617
      Lit p = c[j];
618
      subst_clause.push(var(p) == v ? x ^ sign(p) : p);
619
    }
620
621
    removeClause(cls[i]);
622
    ClauseId id = ClauseIdUndef;
623
    if (!addClause_(subst_clause, c.removable(), id))
624
    {
625
      return ok = false;
626
    }
627
  }
628
629
    return true;
630
}
631
632
633
5953
void SimpSolver::extendModel()
634
{
635
    int i, j;
636
    Lit x;
637
638
50466
    for (i = elimclauses.size()-1; i > 0; i -= j){
639
72549
        for (j = elimclauses[i--]; j > 1; j--, i--)
640
50418
            if (modelValue(toLit(elimclauses[i])) != l_False)
641
22382
                goto next;
642
643
22131
        x = toLit(elimclauses[i]);
644
22131
        model[var(x)] = lbool(!sign(x));
645
44513
    next:;
646
    }
647
5953
}
648
649
650
1744
bool SimpSolver::eliminate(bool turn_off_elim)
651
{
652
1744
    if (!simplify())
653
280
        return false;
654
1464
    else if (!use_simplification)
655
        return true;
656
657
    // Main simplification loop:
658
    //
659
4550
    while (n_touched > 0 || bwdsub_assigns < trail.size() || elim_heap.size() > 0){
660
661
1555
        gatherTouchedClauses();
662
        // printf("  ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns);
663
3872
        if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size())
664
3108
            && !backwardSubsumptionCheck(true))
665
        {
666
11
          ok = false;
667
11
          goto cleanup;
668
        }
669
670
        // Empty elim_heap and return immediately on user-interrupt:
671
1544
        if (asynch_interrupt){
672
          Assert(bwdsub_assigns == trail.size());
673
          Assert(subsumption_queue.size() == 0);
674
          Assert(n_touched == 0);
675
          elim_heap.clear();
676
          goto cleanup;
677
        }
678
679
        // printf("  ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size());
680
139509
        for (int cnt = 0; !elim_heap.empty(); cnt++){
681
137966
            Var elim = elim_heap.removeMin();
682
683
137966
            if (asynch_interrupt) break;
684
685
137966
            if (isEliminated(elim) || value(elim) != l_Undef) continue;
686
687
113198
            if (verbosity >= 2 && cnt % 100 == 0)
688
                printf("elimination left: %10d\r", elim_heap.size());
689
690
113198
            if (use_asymm){
691
                // Temporarily freeze variable. Otherwise, it would immediately end up on the queue again:
692
                bool was_frozen = frozen[elim];
693
                frozen[elim] = true;
694
                if (!asymmVar(elim)){
695
                    ok = false; goto cleanup; }
696
                frozen[elim] = was_frozen; }
697
698
            // At this point, the variable may have been set by assymetric branching, so check it
699
            // again. Also, don't eliminate frozen variables:
700
113198
            if (use_elim && value(elim) == l_Undef && !frozen[elim] && !eliminateVar(elim)){
701
1
                ok = false; goto cleanup; }
702
703
113197
            checkGarbage(simp_garbage_frac);
704
        }
705
706
1543
        Assert(subsumption_queue.size() == 0);
707
    }
708
1452
 cleanup:
709
710
    // If no more simplification is needed, free all simplification-related data structures:
711
1464
    if (turn_off_elim){
712
        touched  .clear(true);
713
        occurs   .clear(true);
714
        n_occ    .clear(true);
715
        elim_heap.clear(true);
716
        subsumption_queue.clear(true);
717
718
        use_simplification    = false;
719
        remove_satisfied      = true;
720
        ca.extra_clause_field = false;
721
722
        // Force full cleanup (this is safe and desirable since it only happens once):
723
        rebuildOrderHeap();
724
        garbageCollect();
725
    }else{
726
        // Cheaper cleanup:
727
1464
        cleanUpClauses(); // TODO: can we make 'cleanUpClauses()' not be linear in the problem size somehow?
728
1464
        checkGarbage();
729
    }
730
731
1464
    if (verbosity >= 1 && elimclauses.size() > 0)
732
      printf(
733
          "|  Eliminated clauses:     %10.2f Mb                                "
734
          "      |\n",
735
          double(elimclauses.size() * sizeof(uint32_t)) / (1024 * 1024));
736
737
1464
    return ok;
738
}
739
740
741
4566
void SimpSolver::cleanUpClauses()
742
{
743
4566
    occurs.cleanAll();
744
    int i,j;
745
1454827
    for (i = j = 0; i < clauses_persistent.size(); i++)
746
1450261
        if (ca[clauses_persistent[i]].mark() == 0)
747
1196373
            clauses_persistent[j++] = clauses_persistent[i];
748
4566
    clauses_persistent.shrink(i - j);
749
4566
}
750
751
//=================================================================================================
752
// Garbage Collection methods:
753
754
755
3102
void SimpSolver::relocAll(ClauseAllocator& to)
756
{
757
3102
    if (!use_simplification) return;
758
759
    // All occurs lists:
760
    //
761
413922
    for (int i = 0; i < nVars(); i++){
762
412995
        vec<CRef>& cs = occurs[i];
763
1085769
        for (int j = 0; j < cs.size(); j++)
764
672774
            ca.reloc(cs[j], to);
765
    }
766
767
    // Subsumption queue:
768
    //
769
954
    for (int i = 0; i < subsumption_queue.size(); i++)
770
27
        ca.reloc(subsumption_queue[i], to);
771
    // TODO reloc now takes the proof form the core solver
772
    // Temporary clause:
773
    //
774
927
    ca.reloc(bwdsub_tmpunit, to);
775
    // TODO reloc now takes the proof form the core solver
776
}
777
778
779
3102
void SimpSolver::garbageCollect()
780
{
781
    // Initialize the next region to a size corresponding to the estimated utilization degree. This
782
    // is not precise but should avoid some unnecessary reallocations for the new region:
783
6204
    ClauseAllocator to(ca.size() - ca.wasted());
784
785
3102
    cleanUpClauses();
786
3102
    to.extra_clause_field = ca.extra_clause_field; // NOTE: this is important to keep (or lose) the extra fields.
787
3102
    relocAll(to);
788
3102
    Solver::relocAll(to);
789
3102
    if (verbosity >= 2)
790
      printf(
791
          "|  Garbage collection:   %12d bytes => %12d bytes             |\n",
792
          ca.size() * ClauseAllocator::Unit_Size,
793
          to.size() * ClauseAllocator::Unit_Size);
794
3102
    to.moveTo(ca);
795
    // TODO: proof.finalizeUpdateId();
796
87181
}