GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/bvminisat/simp/SimpSolver.cc Lines: 299 403 74.2 %
Date: 2021-03-23 Branches: 366 974 37.6 %

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/bvminisat/simp/SimpSolver.h"
22
23
#include "base/check.h"
24
#include "options/bv_options.h"
25
#include "options/smt_options.h"
26
#include "proof/clause_id.h"
27
#include "prop/bvminisat/mtl/Sort.h"
28
#include "prop/bvminisat/utils/System.h"
29
30
namespace CVC4 {
31
namespace BVMinisat {
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
8977
SimpSolver::SimpSolver(CVC4::context::Context* context)
52
    : Solver(context),
53
      grow(opt_grow),
54
      clause_lim(opt_clause_lim),
55
      subsumption_lim(opt_subsumption_lim),
56
      simp_garbage_frac(opt_simp_garbage_frac),
57
      use_asymm(opt_use_asymm),
58
      use_rcheck(opt_use_rcheck),
59
      use_elim(opt_use_elim
60
1620660
               && CVC4::options::bitblastMode()
61
8977
                      == CVC4::options::BitblastMode::EAGER
62
8998
               && !CVC4::options::produceModels()),
63
      merges(0),
64
      asymm_lits(0),
65
      eliminated_vars(0),
66
      elimorder(1),
67
      use_simplification(true),
68
17954
      occurs(ClauseDeleted(ca)),
69
17954
      elim_heap(ElimLt(n_occ)),
70
      bwdsub_assigns(0),
71
53862
      n_touched(0)
72
{
73
74
17954
    vec<Lit> dummy(1,lit_Undef);
75
8977
    ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
76
8977
    bwdsub_tmpunit        = ca.alloc(dummy);
77
8977
    remove_satisfied      = false;
78
79
    // add the initialization for all the internal variables
80
26931
    for (int i = frozen.size(); i < vardata.size(); ++ i) {
81
17954
      frozen    .push(1);
82
17954
      eliminated.push(0);
83
17954
      if (use_simplification){
84
17954
          n_occ     .push(0);
85
17954
          n_occ     .push(0);
86
17954
          occurs    .init(i);
87
17954
          touched   .push(0);
88
17954
          elim_heap .insert(i);
89
      }
90
    }
91
92
8977
}
93
94
95
17948
SimpSolver::~SimpSolver()
96
{
97
  //  CVC4::StatisticsRegistry::unregisterStat(&total_eliminate_time);
98
17948
}
99
100
101
1835652
Var SimpSolver::newVar(bool sign, bool dvar, bool freeze) {
102
1835652
    Var v = Solver::newVar(sign, dvar);
103
104
1835652
    frozen    .push((char)false);
105
1835652
    eliminated.push((char)false);
106
107
1835652
    if (use_simplification){
108
1835652
        n_occ     .push(0);
109
1835652
        n_occ     .push(0);
110
1835652
        occurs    .init(v);
111
1835652
        touched   .push(0);
112
1835652
        elim_heap .insert(v);
113
1835652
        if (freeze) {
114
248745
          setFrozen(v, true);
115
        }
116
    }
117
1835652
    return v;
118
}
119
120
121
122
9172
lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
123
{
124
9172
    only_bcp = false;
125
126
18344
    vec<Var> extra_frozen;
127
9172
    lbool    result = l_True;
128
129
9172
    do_simp &= use_simplification;
130
131
9172
    if (do_simp) {
132
        // Assumptions must be temporarily frozen to run variable elimination:
133
756198
        for (int i = 0; i < assumptions.size(); i++){
134
747026
            Var v = var(assumptions[i]);
135
136
            // If an assumption has been eliminated, remember it.
137
747026
            Assert(!isEliminated(v));
138
139
747026
            if (!frozen[v]){
140
                // Freeze and store.
141
                setFrozen(v, true);
142
                extra_frozen.push(v);
143
            } }
144
145
9172
        if (do_simp && clause_added) {
146
5675
          cancelUntil(0);
147
5675
          result = lbool(eliminate(turn_off_simp));
148
5675
          clause_added = false;
149
        }
150
    }
151
152
9172
    if (result == l_True)
153
9168
        result = Solver::solve_();
154
4
    else if (verbosity >= 1)
155
        printf("===============================================================================\n");
156
157
9172
    if (do_simp)
158
        // Unfreeze the assumptions that were frozen:
159
9172
        for (int i = 0; i < extra_frozen.size(); i++)
160
            setFrozen(extra_frozen[i], false);
161
162
18344
    return result;
163
}
164
165
166
167
6987705
bool SimpSolver::addClause_(vec<Lit>& ps, ClauseId& id)
168
{
169
#ifdef CVC4_ASSERTIONS
170
6987705
  for (int i = 0; i < ps.size(); i++) Assert(!isEliminated(var(ps[i])));
171
#endif
172
173
6987705
    int nclauses = clauses.size();
174
175
6987705
    if (use_rcheck && implied(ps))
176
        return true;
177
178
6987705
    if (!Solver::addClause_(ps, id))
179
8
        return false;
180
181
6987697
    if (use_simplification && clauses.size() == nclauses + 1){
182
6976315
        CRef          cr = clauses.last();
183
6976315
        const Clause& clause = ca[cr];
184
185
        // NOTE: the clause is added to the queue immediately and then
186
        // again during 'gatherTouchedClauses()'. If nothing happens
187
        // in between, it will only be checked once. Otherwise, it may
188
        // be checked twice unnecessarily. This is an unfortunate
189
        // consequence of how backward subsumption is used to mimic
190
        // forward subsumption.
191
6976315
        subsumption_queue.insert(cr);
192
25959571
        for (int i = 0; i < clause.size(); i++)
193
        {
194
18983256
          occurs[var(clause[i])].push(cr);
195
18983256
          n_occ[toInt(clause[i])]++;
196
18983256
          touched[var(clause[i])] = 1;
197
18983256
          n_touched++;
198
18983256
          if (elim_heap.inHeap(var(clause[i])))
199
17712056
            elim_heap.increase(var(clause[i]));
200
        }
201
    }
202
203
6987697
    return true;
204
}
205
206
207
51146
void SimpSolver::removeClause(CRef cr)
208
{
209
51146
  const Clause& clause = ca[cr];
210
211
51146
  if (use_simplification)
212
  {
213
208175
    for (int i = 0; i < clause.size(); i++)
214
    {
215
157029
      n_occ[toInt(clause[i])]--;
216
157029
      updateElimHeap(var(clause[i]));
217
157029
      occurs.smudge(var(clause[i]));
218
    }
219
  }
220
51146
  Solver::removeClause(cr);
221
51146
}
222
223
224
39653
bool SimpSolver::strengthenClause(CRef cr, Lit l)
225
{
226
39653
  Clause& clause = ca[cr];
227
39653
  Assert(decisionLevel() == 0);
228
39653
  Assert(use_simplification);
229
230
  // FIX: this is too inefficient but would be nice to have (properly
231
  // implemented) if (!find(subsumption_queue, &clause))
232
39653
  subsumption_queue.insert(cr);
233
234
39653
  if (clause.size() == 2)
235
  {
236
3534
    removeClause(cr);
237
3534
    clause.strengthen(l);
238
  }
239
  else
240
  {
241
36119
    detachClause(cr, true);
242
36119
    clause.strengthen(l);
243
36119
    attachClause(cr);
244
36119
    remove(occurs[var(l)], cr);
245
36119
    n_occ[toInt(l)]--;
246
36119
    updateElimHeap(var(l));
247
  }
248
249
39653
  return clause.size() == 1 ? enqueue(clause[0]) && propagate() == CRef_Undef
250
39653
                            : true;
251
}
252
253
254
// Returns FALSE if clause is always satisfied ('out_clause' should not be used).
255
28024
bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause)
256
{
257
28024
    merges++;
258
28024
    out_clause.clear();
259
260
28024
    bool  ps_smallest = _ps.size() < _qs.size();
261
28024
    const Clause& ps  =  ps_smallest ? _qs : _ps;
262
28024
    const Clause& qs  =  ps_smallest ? _ps : _qs;
263
264
58878
    for (int i = 0; i < qs.size(); i++)
265
    {
266
47639
      if (var(qs[i]) != v)
267
      {
268
139412
        for (int j = 0; j < ps.size(); j++)
269
        {
270
125394
          if (var(ps[j]) == var(qs[i]))
271
          {
272
20449
            if (ps[j] == ~qs[i])
273
16785
              return false;
274
            else
275
3664
              goto next;
276
          }
277
        }
278
14018
        out_clause.push(qs[i]);
279
      }
280
44026
    next:;
281
    }
282
283
57525
    for (int i = 0; i < ps.size(); i++)
284
46286
        if (var(ps[i]) != v)
285
35047
            out_clause.push(ps[i]);
286
287
11239
    return true;
288
}
289
290
291
// Returns FALSE if clause is always satisfied.
292
57355
bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)
293
{
294
57355
    merges++;
295
296
57355
    bool  ps_smallest = _ps.size() < _qs.size();
297
57355
    const Clause& ps  =  ps_smallest ? _qs : _ps;
298
57355
    const Clause& qs  =  ps_smallest ? _ps : _qs;
299
57355
    const Lit*  __ps  = (const Lit*)ps;
300
57355
    const Lit*  __qs  = (const Lit*)qs;
301
302
57355
    size = ps.size()-1;
303
304
148315
    for (int i = 0; i < qs.size(); i++)
305
    {
306
116421
      if (var(__qs[i]) != v)
307
      {
308
395728
        for (int j = 0; j < ps.size(); j++)
309
        {
310
347764
          if (var(__ps[j]) == var(__qs[i]))
311
          {
312
33100
            if (__ps[j] == ~__qs[i])
313
25461
              return false;
314
            else
315
7639
              goto next;
316
          }
317
        }
318
47964
        size++;
319
      }
320
126317
    next:;
321
    }
322
323
31894
    return true;
324
}
325
326
327
5682
void SimpSolver::gatherTouchedClauses()
328
{
329
5682
    if (n_touched == 0) return;
330
331
    int i,j;
332
5916093
    for (i = j = 0; i < subsumption_queue.size(); i++)
333
5910411
        if (ca[subsumption_queue[i]].mark() == 0)
334
5910411
            ca[subsumption_queue[i]].mark(2);
335
336
16115668
    for (i = 0; i < touched.size(); i++)
337
16109986
        if (touched[i]){
338
1706890
            const vec<CRef>& cs = occurs.lookup(i);
339
27938604
            for (j = 0; j < cs.size(); j++)
340
26231714
                if (ca[cs[j]].mark() == 0){
341
7607020
                    subsumption_queue.insert(cs[j]);
342
7607020
                    ca[cs[j]].mark(2);
343
                }
344
1706890
            touched[i] = 0;
345
        }
346
347
13523113
    for (i = 0; i < subsumption_queue.size(); i++)
348
13517431
        if (ca[subsumption_queue[i]].mark() == 2)
349
13517431
            ca[subsumption_queue[i]].mark(0);
350
351
5682
    n_touched = 0;
352
}
353
354
bool SimpSolver::implied(const vec<Lit>& clause)
355
{
356
  Assert(decisionLevel() == 0);
357
358
  trail_lim.push(trail.size());
359
  for (int i = 0; i < clause.size(); i++)
360
  {
361
    if (value(clause[i]) == l_True)
362
    {
363
      cancelUntil(0);
364
      return false;
365
    }
366
    else if (value(clause[i]) != l_False)
367
    {
368
      Assert(value(clause[i]) == l_Undef);
369
      uncheckedEnqueue(~clause[i]);
370
    }
371
  }
372
373
  bool result = propagate() != CRef_Undef;
374
  cancelUntil(0);
375
  return result;
376
}
377
378
379
// Backward subsumption + backward subsumption resolution
380
8205
bool SimpSolver::backwardSubsumptionCheck(bool verbose)
381
{
382
8205
    int cnt = 0;
383
8205
    int subsumed = 0;
384
8205
    int deleted_literals = 0;
385
8205
    Assert(decisionLevel() == 0);
386
387
27157919
    while (subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()){
388
389
        // Empty subsumption queue and return immediately on user-interrupt:
390
13574857
        if (asynch_interrupt){
391
            subsumption_queue.clear();
392
            bwdsub_assigns = trail.size();
393
            break; }
394
395
        // Check top-level assignments by creating a dummy clause and placing it in the queue:
396
13574857
        if (subsumption_queue.size() == 0 && bwdsub_assigns < trail.size()){
397
6534
            Lit l = trail[bwdsub_assigns++];
398
6534
            ca[bwdsub_tmpunit][0] = l;
399
6534
            ca[bwdsub_tmpunit].calcAbstraction();
400
6534
            subsumption_queue.insert(bwdsub_tmpunit); }
401
402
13574857
        CRef    cr = subsumption_queue.peek(); subsumption_queue.pop();
403
13574857
        Clause& clause = ca[cr];
404
405
13574857
        if (clause.mark()) continue;
406
407
13551862
        if (verbose && verbosity >= 2 && cnt++ % 1000 == 0)
408
            printf("subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue.size(), subsumed, deleted_literals);
409
410
13551862
        Assert(clause.size() > 1
411
               || value(clause[0]) == l_True);  // Unit-clauses should have been
412
                                                // propagated before this point.
413
414
        // Find best variable to scan:
415
13551862
        Var best = var(clause[0]);
416
39298933
        for (int i = 1; i < clause.size(); i++)
417
25747071
          if (occurs[var(clause[i])].size() < occurs[best].size())
418
12046681
            best = var(clause[i]);
419
420
        // Search all candidates:
421
13551862
        vec<CRef>& _cs = occurs.lookup(best);
422
13551862
        CRef*       cs = (CRef*)_cs;
423
424
150126298
        for (int j = 0; j < _cs.size(); j++)
425
136574436
          if (clause.mark())
426
            break;
427
409722120
          else if (!ca[cs[j]].mark() && cs[j] != cr
428
382630276
                   && (subsumption_lim == -1
429
123027920
                       || ca[cs[j]].size() < subsumption_lim))
430
          {
431
123027920
            Lit l = clause.subsumes(ca[cs[j]]);
432
433
123027920
            if (l == lit_Undef)
434
31332
              subsumed++, removeClause(cs[j]);
435
122996588
            else if (l != lit_Error)
436
            {
437
39653
              deleted_literals++;
438
439
39653
              if (!strengthenClause(cs[j], ~l)) return false;
440
441
              // Did current candidate get deleted from cs? Then check candidate
442
              // at index j again:
443
39653
              if (var(l) == best) j--;
444
            }
445
          }
446
    }
447
448
8205
    return true;
449
}
450
451
452
bool SimpSolver::asymm(Var v, CRef cr)
453
{
454
  Clause& clause = ca[cr];
455
  Assert(decisionLevel() == 0);
456
457
  if (clause.mark() || satisfied(clause)) return true;
458
459
  trail_lim.push(trail.size());
460
  Lit l = lit_Undef;
461
  for (int i = 0; i < clause.size(); i++)
462
    if (var(clause[i]) != v && value(clause[i]) != l_False)
463
      uncheckedEnqueue(~clause[i]);
464
    else
465
      l = clause[i];
466
467
  if (propagate() != CRef_Undef)
468
  {
469
    cancelUntil(0);
470
    asymm_lits++;
471
    if (!strengthenClause(cr, l)) return false;
472
  }
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
2523
static void mkElimClause(vec<uint32_t>& elimclauses, Lit x)
496
{
497
2523
    elimclauses.push(toInt(x));
498
2523
    elimclauses.push(1);
499
2523
}
500
501
6218
static void mkElimClause(vec<uint32_t>& elimclauses, Var v, Clause& clause)
502
{
503
6218
    int first = elimclauses.size();
504
6218
    int v_pos = -1;
505
506
    // Copy clause to elimclauses-vector. Remember position where the
507
    // variable 'v' occurs:
508
29054
    for (int i = 0; i < clause.size(); i++)
509
    {
510
22836
      elimclauses.push(toInt(clause[i]));
511
22836
      if (var(clause[i]) == v) v_pos = i + first;
512
    }
513
6218
    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
6218
    uint32_t tmp = elimclauses[v_pos];
518
6218
    elimclauses[v_pos] = elimclauses[first];
519
6218
    elimclauses[first] = tmp;
520
521
    // Store the length of the clause last:
522
6218
    elimclauses.push(clause.size());
523
6218
}
524
525
526
527
4029
bool SimpSolver::eliminateVar(Var v)
528
{
529
4029
  Assert(!frozen[v]);
530
4029
  Assert(!isEliminated(v));
531
4029
  Assert(value(v) == l_Undef);
532
533
  // Split the occurrences into positive and negative:
534
  //
535
4029
  const vec<CRef>& cls = occurs.lookup(v);
536
8058
  vec<CRef> pos, neg;
537
39458
  for (int i = 0; i < cls.size(); i++)
538
35429
    (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
4029
  int cnt = 0;
545
4029
  int clause_size = 0;
546
547
14000
  for (int i = 0; i < pos.size(); i++)
548
67326
    for (int j = 0; j < neg.size(); j++)
549
114710
      if (merge(ca[pos[i]], ca[neg[j]], v, clause_size)
550
58861
          && (++cnt > cls.size() + grow
551
30388
              || (clause_lim != -1 && clause_size > clause_lim)))
552
1506
        return true;
553
554
  // Delete and store old clauses:
555
2523
  eliminated[v] = true;
556
2523
  setDecisionVar(v, false);
557
2523
  eliminated_vars++;
558
559
2523
  if (pos.size() > neg.size())
560
  {
561
726
    for (int i = 0; i < neg.size(); i++)
562
493
      mkElimClause(elimclauses, v, ca[neg[i]]);
563
233
    mkElimClause(elimclauses, mkLit(v));
564
  }
565
  else
566
  {
567
8015
    for (int i = 0; i < pos.size(); i++)
568
5725
      mkElimClause(elimclauses, v, ca[pos[i]]);
569
2290
    mkElimClause(elimclauses, ~mkLit(v));
570
  }
571
572
2523
    for (int i = 0; i < cls.size(); i++) removeClause(cls[i]);
573
574
    // Produce clauses in cross product:
575
2523
    vec<Lit>& resolvent = add_tmp;
576
8982
    for (int i = 0; i < pos.size(); i++)
577
34483
      for (int j = 0; j < neg.size(); j++) {
578
28024
        ClauseId id = -1;
579
39263
        if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) &&
580
11239
            !addClause_(resolvent, id))
581
          return false;
582
      }
583
584
    // Free occurs list for this variable:
585
2523
    occurs[v].clear(true);
586
587
    // Free watchers lists for this variable, if possible:
588
2523
    if (watches[ mkLit(v)].size() == 0) watches[ mkLit(v)].clear(true);
589
2523
    if (watches[~mkLit(v)].size() == 0) watches[~mkLit(v)].clear(true);
590
591
2523
    return backwardSubsumptionCheck();
592
}
593
594
595
bool SimpSolver::substitute(Var v, Lit x)
596
{
597
  Assert(!frozen[v]);
598
  Assert(!isEliminated(v));
599
  Assert(value(v) == l_Undef);
600
601
  if (!ok) return false;
602
603
  eliminated[v] = true;
604
  setDecisionVar(v, false);
605
  const vec<CRef>& cls = occurs.lookup(v);
606
607
  vec<Lit>& subst_clause = add_tmp;
608
  for (int i = 0; i < cls.size(); i++)
609
  {
610
    Clause& clause = ca[cls[i]];
611
612
    subst_clause.clear();
613
    for (int j = 0; j < clause.size(); j++)
614
    {
615
      Lit p = clause[j];
616
      subst_clause.push(var(p) == v ? x ^ sign(p) : p);
617
    }
618
619
    removeClause(cls[i]);
620
    ClauseId id;
621
    if (!addClause_(subst_clause, id)) return ok = false;
622
  }
623
624
    return true;
625
}
626
627
628
void SimpSolver::extendModel()
629
{
630
    int i, j;
631
    Lit x;
632
633
    for (i = elimclauses.size()-1; i > 0; i -= j){
634
        for (j = elimclauses[i--]; j > 1; j--, i--)
635
            if (modelValue(toLit(elimclauses[i])) != l_False)
636
                goto next;
637
638
        x = toLit(elimclauses[i]);
639
        model[var(x)] = lbool(!sign(x));
640
    next:;
641
    }
642
}
643
644
645
5675
bool SimpSolver::eliminate(bool turn_off_elim)
646
{
647
648
  //  CVC4::TimerStat::CodeTimer codeTimer(total_eliminate_time);
649
650
5675
    if (!simplify())
651
4
        return false;
652
5671
    else if (!use_simplification)
653
        return true;
654
655
    // Main simplification loop:
656
    //
657
17035
    while (n_touched > 0 || bwdsub_assigns < trail.size() || elim_heap.size() > 0){
658
659
5682
        gatherTouchedClauses();
660
        // printf("  ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns);
661
11364
        if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size())
662
11364
            && !backwardSubsumptionCheck(true))
663
        {
664
          ok = false;
665
          goto cleanup;
666
        }
667
668
        // Empty elim_heap and return immediately on user-interrupt:
669
5682
        if (asynch_interrupt){
670
          Assert(bwdsub_assigns == trail.size());
671
          Assert(subsumption_queue.size() == 0);
672
          Assert(n_touched == 0);
673
          elim_heap.clear();
674
          goto cleanup;
675
        }
676
677
        // printf("  ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size());
678
1561661
        for (int cnt = 0; !elim_heap.empty(); cnt++){
679
1555979
            Var elim = elim_heap.removeMin();
680
681
1555979
            if (asynch_interrupt) break;
682
683
1555979
            if (isEliminated(elim) || value(elim) != l_Undef) continue;
684
685
1549475
            if (verbosity >= 2 && cnt % 100 == 0)
686
                printf("elimination left: %10d\r", elim_heap.size());
687
688
1549475
            if (use_asymm){
689
                // Temporarily freeze variable. Otherwise, it would immediately end up on the queue again:
690
                bool was_frozen = frozen[elim];
691
                frozen[elim] = true;
692
                if (!asymmVar(elim)){
693
                    ok = false; goto cleanup; }
694
                frozen[elim] = was_frozen; }
695
696
            // At this point, the variable may have been set by assymetric branching, so check it
697
            // again. Also, don't eliminate frozen variables:
698
1549475
            if (use_elim && value(elim) == l_Undef && !frozen[elim] && !eliminateVar(elim)){
699
                ok = false; goto cleanup; }
700
701
1549475
            checkGarbage(simp_garbage_frac);
702
        }
703
704
5682
        Assert(subsumption_queue.size() == 0);
705
    }
706
5671
 cleanup:
707
708
    // If no more simplification is needed, free all simplification-related data structures:
709
5671
    if (turn_off_elim){
710
        touched  .clear(true);
711
        occurs   .clear(true);
712
        n_occ    .clear(true);
713
        elim_heap.clear(true);
714
        subsumption_queue.clear(true);
715
716
        use_simplification    = false;
717
        remove_satisfied      = true;
718
        ca.extra_clause_field = false;
719
720
        // Force full cleanup (this is safe and desirable since it only happens once):
721
        rebuildOrderHeap();
722
        garbageCollect();
723
    }else{
724
        // Cheaper cleanup:
725
5671
        cleanUpClauses(); // TODO: can we make 'cleanUpClauses()' not be linear in the problem size somehow?
726
5671
        checkGarbage();
727
    }
728
729
5671
    if (verbosity >= 1 && elimclauses.size() > 0)
730
      printf(
731
          "|  Eliminated clauses:     %10.2f Mb                                "
732
          "      |\n",
733
          double(elimclauses.size() * sizeof(uint32_t)) / (1024 * 1024));
734
735
5671
    return ok;
736
737
738
739
}
740
741
742
5743
void SimpSolver::cleanUpClauses()
743
{
744
5743
    occurs.cleanAll();
745
    int i,j;
746
78209116
    for (i = j = 0; i < clauses.size(); i++)
747
78203373
        if (ca[clauses[i]].mark() == 0)
748
78152227
            clauses[j++] = clauses[i];
749
5743
    clauses.shrink(i - j);
750
5743
}
751
752
753
//=================================================================================================
754
// Garbage Collection methods:
755
756
757
72
void SimpSolver::relocAll(ClauseAllocator& to)
758
{
759
72
    if (!use_simplification) return;
760
761
    // All occurs lists:
762
    //
763
35738
    for (int i = 0; i < nVars(); i++){
764
35666
        vec<CRef>& cs = occurs[i];
765
336700
        for (int j = 0; j < cs.size(); j++)
766
301034
            ca.reloc(cs[j], to);
767
    }
768
769
    // Subsumption queue:
770
    //
771
552
    for (int i = 0; i < subsumption_queue.size(); i++)
772
480
        ca.reloc(subsumption_queue[i], to);
773
774
    // Temporary clause:
775
    //
776
72
    ca.reloc(bwdsub_tmpunit, to);
777
}
778
779
780
72
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
144
    ClauseAllocator to(ca.size() - ca.wasted());
785
786
72
    cleanUpClauses();
787
72
    to.extra_clause_field = ca.extra_clause_field; // NOTE: this is important to keep (or lose) the extra fields.
788
72
    relocAll(to);
789
72
    Solver::relocAll(to);
790
72
    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
72
    to.moveTo(ca);
796
72
}
797
798
} /* CVC4::BVMinisat namespace */
799
1638368
} /* CVC4 namespace */