GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/bvminisat/core/Solver.cc Lines: 521 651 80.0 %
Date: 2021-03-22 Branches: 579 1413 41.0 %

Line Exec Source
1
/***************************************************************************************[Solver.cc]
2
Copyright (c) 2003-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/core/Solver.h"
22
23
#include <math.h>
24
25
#include <iostream>
26
#include <vector>
27
28
#include "base/check.h"
29
#include "base/exception.h"
30
#include "base/output.h"
31
#include "options/bv_options.h"
32
#include "options/smt_options.h"
33
#include "prop/bvminisat/mtl/Sort.h"
34
#include "theory/interrupted.h"
35
#include "util/utility.h"
36
37
namespace CVC4 {
38
namespace BVMinisat {
39
40
#define OUTPUT_TAG "bvminisat: [a=" << assumptions.size() << ",l=" << decisionLevel() << "] "
41
42
std::ostream& operator << (std::ostream& out, const BVMinisat::Lit& l) {
43
  out << (sign(l) ? "-" : "") << var(l) + 1;
44
  return out;
45
}
46
47
std::ostream& operator << (std::ostream& out, const BVMinisat::Clause& c) {
48
  for (int i = 0; i < c.size(); i++) {
49
    if (i > 0) {
50
      out << " ";
51
    }
52
    out << c[i];
53
  }
54
  return out;
55
}
56
57
58
//=================================================================================================
59
// Options:
60
61
62
static const char* _cat = "CORE";
63
64
8892
static DoubleOption  opt_var_decay         (_cat, "var-decay",   "The variable activity decay factor",            0.95,     DoubleRange(0, false, 1, false));
65
8892
static DoubleOption  opt_clause_decay      (_cat, "cla-decay",   "The clause activity decay factor",              0.999,    DoubleRange(0, false, 1, false));
66
8892
static DoubleOption  opt_random_var_freq   (_cat, "rnd-freq",    "The frequency with which the decision heuristic tries to choose a random variable", 0, DoubleRange(0, true, 1, true));
67
8892
static DoubleOption  opt_random_seed       (_cat, "rnd-seed",    "Used by the random variable selection",         91648253, DoubleRange(0, false, HUGE_VAL, false));
68
8892
static IntOption     opt_ccmin_mode        (_cat, "ccmin-mode",  "Controls conflict clause minimization (0=none, 1=basic, 2=deep)", 2, IntRange(0, 2));
69
8892
static IntOption     opt_phase_saving      (_cat, "phase-saving", "Controls the level of phase saving (0=none, 1=limited, 2=full)", 2, IntRange(0, 2));
70
8892
static BoolOption    opt_rnd_init_act      (_cat, "rnd-init",    "Randomize the initial activity", false);
71
8892
static BoolOption    opt_luby_restart      (_cat, "luby",        "Use the Luby restart sequence", true);
72
8892
static IntOption     opt_restart_first     (_cat, "rfirst",      "The base restart interval", 25, IntRange(1, INT32_MAX));
73
8892
static DoubleOption  opt_restart_inc       (_cat, "rinc",        "Restart interval increase factor", 3, DoubleRange(1, false, HUGE_VAL, false));
74
8892
static DoubleOption  opt_garbage_frac      (_cat, "gc-frac",     "The fraction of wasted memory allowed before a garbage collection is triggered",  0.20, DoubleRange(0, false, HUGE_VAL, false));
75
76
//=================================================================================================
77
// Proof declarations
78
CRef Solver::TCRef_Undef = CRef_Undef;
79
CRef Solver::TCRef_Lazy = CRef_Undef - 1; // no real lazy ref here
80
81
82
//=================================================================================================
83
// Constructor/Destructor:
84
85
8975
Solver::Solver(CVC4::context::Context* context)
86
    :
87
88
      // Parameters (user settable):
89
      //
90
      d_notify(nullptr),
91
      c(context),
92
      verbosity(0),
93
      var_decay(opt_var_decay),
94
      clause_decay(opt_clause_decay),
95
      random_var_freq(opt_random_var_freq),
96
      random_seed(opt_random_seed),
97
      luby_restart(opt_luby_restart),
98
      ccmin_mode(opt_ccmin_mode),
99
      phase_saving(opt_phase_saving),
100
      rnd_pol(false),
101
      rnd_init_act(opt_rnd_init_act),
102
      garbage_frac(opt_garbage_frac),
103
      restart_first(opt_restart_first),
104
      restart_inc(opt_restart_inc)
105
106
      // Parameters (the rest):
107
      //
108
      ,
109
      learntsize_factor((double)1 / (double)3),
110
      learntsize_inc(1.5)
111
112
      // Parameters (experimental):
113
      //
114
      ,
115
      learntsize_adjust_start_confl(100),
116
      learntsize_adjust_inc(1.5)
117
118
      // Statistics: (formerly in 'SolverStats')
119
      //
120
      ,
121
      solves(0),
122
      starts(0),
123
      decisions(0),
124
      rnd_decisions(0),
125
      propagations(0),
126
      conflicts(0),
127
      dec_vars(0),
128
      clauses_literals(0),
129
      learnts_literals(0),
130
      max_literals(0),
131
      tot_literals(0)
132
133
      ,
134
      need_to_propagate(false),
135
      only_bcp(false),
136
      clause_added(false),
137
      ok(true),
138
      cla_inc(1),
139
      var_inc(1),
140
17950
      watches(WatcherDeleted(ca)),
141
      qhead(0),
142
      simpDB_assigns(-1),
143
      simpDB_props(0),
144
17950
      order_heap(VarOrderLt(activity)),
145
      progress_estimate(0),
146
      remove_satisfied(true)
147
148
      ,
149
      ca()
150
151
      // even though these are temporaries and technically should be set
152
      // before calling, lets initialize them. this will reduces chances of
153
      // non-determinism in portfolio (parallel) solver if variables are
154
      // being (incorrectly) used without initialization.
155
      ,
156
      seen(),
157
      analyze_stack(),
158
      analyze_toclear(),
159
      add_tmp(),
160
      max_learnts(0.0),
161
      learntsize_adjust_confl(0.0),
162
      learntsize_adjust_cnt(0)
163
164
      // Resource constraints:
165
      //
166
      ,
167
      conflict_budget(-1),
168
      propagation_budget(-1),
169
44875
      asynch_interrupt(false)
170
{
171
  // Create the constant variables
172
8975
  varTrue = newVar(true, false);
173
8975
  varFalse = newVar(false, false);
174
175
  // Assert the constants
176
8975
  uncheckedEnqueue(mkLit(varTrue, false));
177
8975
  uncheckedEnqueue(mkLit(varFalse, true));
178
8975
}
179
180
181
8972
Solver::~Solver()
182
{
183
8972
}
184
185
186
//=================================================================================================
187
// Minor methods:
188
189
190
// Creates a new SAT variable in the solver. If 'decision' is cleared, variable will not be
191
// used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result).
192
//
193
1853602
Var Solver::newVar(bool sign, bool dvar)
194
{
195
1853602
    int v = nVars();
196
1853602
    watches  .init(mkLit(v, false));
197
1853602
    watches  .init(mkLit(v, true ));
198
1853602
    assigns  .push(l_Undef);
199
1853602
    vardata  .push(mkVarData(CRef_Undef, 0));
200
1853602
    marker   .push(0);
201
    //activity .push(0);
202
1853602
    activity .push(rnd_init_act ? drand(random_seed) * 0.00001 : 0);
203
1853602
    seen     .push(0);
204
1853602
    polarity .push(sign);
205
1853602
    decision .push();
206
1853602
    trail    .capacity(v+1);
207
1853602
    setDecisionVar(v, dvar);
208
209
1853602
    return v;
210
}
211
212
213
6987705
bool Solver::addClause_(vec<Lit>& ps, ClauseId& id)
214
{
215
6987705
    if (decisionLevel() > 0) {
216
14547
      cancelUntil(0);
217
    }
218
219
6987705
    if (!ok) {
220
4
      id = ClauseIdUndef;
221
4
      return false;
222
    }
223
224
    // Check if clause is satisfied and remove false/duplicate literals:
225
    // TODO proof for duplicate literals removal?
226
6987701
    sort(ps);
227
    Lit p; int i, j;
228
6987701
    int falseLiteralsCount = 0;
229
230
25987339
    for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
231
      // tautologies are ignored
232
19007987
      if (value(ps[i]) == l_True || ps[i] == ~p) {
233
8349
        id = ClauseIdUndef;
234
8349
        return true;
235
      }
236
237
      // Ignore repeated literals
238
18999638
      if (ps[i] == p) {
239
3524
        continue;
240
      }
241
242
18996114
      if (value(ps[i]) == l_False) {
243
3769
        continue;
244
      }
245
18992345
      ps[j++] = p = ps[i];
246
    }
247
248
6979352
    ps.shrink(i - j);
249
250
6979352
    clause_added = true;
251
252
6979352
    if(falseLiteralsCount == 0) {
253
6979352
      if (ps.size() == 0) {
254
4
        return ok = false;
255
      }
256
6979348
      else if (ps.size() == 1){
257
3033
        uncheckedEnqueue(ps[0]);
258
3033
        CRef confl_ref = propagate();
259
3033
        ok = (confl_ref == CRef_Undef);
260
3033
        return ok;
261
      } else {
262
6976315
        CRef cr = ca.alloc(ps, false);
263
6976315
        clauses.push(cr);
264
6976315
        attachClause(cr);
265
      }
266
6976315
      return ok;
267
    }
268
    return ok;
269
}
270
271
7217065
void Solver::attachClause(CRef cr) {
272
7217065
  const Clause& clause = ca[cr];
273
7217065
  Assert(clause.size() > 1);
274
7217065
  watches[~clause[0]].push(Watcher(cr, clause[1]));
275
7217065
  watches[~clause[1]].push(Watcher(cr, clause[0]));
276
7217065
  if (clause.learnt())
277
204631
    learnts_literals += clause.size();
278
  else
279
7012434
    clauses_literals += clause.size();
280
7217065
}
281
282
106604
void Solver::detachClause(CRef cr, bool strict) {
283
106604
  const Clause& clause = ca[cr];
284
285
106604
  Assert(clause.size() > 1);
286
287
106604
  if (strict)
288
  {
289
36119
    remove(watches[~clause[0]], Watcher(cr, clause[1]));
290
36119
    remove(watches[~clause[1]], Watcher(cr, clause[0]));
291
    }else{
292
        // Lazy detaching: (NOTE! Must clean all watcher lists before garbage collecting this clause)
293
70485
        watches.smudge(~clause[0]);
294
70485
        watches.smudge(~clause[1]);
295
    }
296
297
106604
    if (clause.learnt())
298
19339
      learnts_literals -= clause.size();
299
    else
300
87265
      clauses_literals -= clause.size();
301
106604
}
302
303
70485
void Solver::removeClause(CRef cr) {
304
70485
  Clause& clause = ca[cr];
305
70485
  detachClause(cr);
306
  // Don't leave pointers to free'd memory!
307
70485
  if (locked(clause)) vardata[var(clause[0])].reason = CRef_Undef;
308
70485
  clause.mark(1);
309
70485
  ca.free(cr);
310
70485
}
311
312
15925
bool Solver::satisfied(const Clause& clause) const
313
{
314
420830
  for (int i = 0; i < clause.size(); i++)
315
404996
    if (value(clause[i]) == l_True) return true;
316
15834
  return false;
317
}
318
319
// Revert to the state at given level (keeping all assignment at 'level' but not beyond).
320
//
321
838493
void Solver::cancelUntil(int level) {
322
838493
    if (decisionLevel() > level){
323
813929
      Debug("bvminisat::explain") << OUTPUT_TAG << " backtracking to " << level << std::endl;
324
223433365
      for (int clause = trail.size() - 1; clause >= trail_lim[level]; clause--)
325
      {
326
222619436
        Var x = var(trail[clause]);
327
222619436
        assigns[x] = l_Undef;
328
222619436
        if (marker[x] == 2) marker[x] = 1;
329
445238872
        if (phase_saving > 1
330
222619436
            || ((phase_saving == 1) && clause > trail_lim.last()))
331
        {
332
222619436
          polarity[x] = sign(trail[clause]);
333
        }
334
222619436
        insertVarOrder(x);
335
      }
336
813929
        qhead = trail_lim[level];
337
813929
        trail.shrink(trail.size() - trail_lim[level]);
338
813929
        trail_lim.shrink(trail_lim.size() - level);
339
    }
340
838493
}
341
342
343
//=================================================================================================
344
// Major methods:
345
346
347
6744847
Lit Solver::pickBranchLit()
348
{
349
6744847
    Var next = var_Undef;
350
351
    // Random decision:
352
6744847
    if (drand(random_seed) < random_var_freq && !order_heap.empty()){
353
        next = order_heap[irand(random_seed,order_heap.size())];
354
        if (value(next) == l_Undef && decision[next])
355
            rnd_decisions++; }
356
357
    // Activity based decision:
358
62725223
    while (next == var_Undef || value(next) != l_Undef || !decision[next])
359
27994795
        if (order_heap.empty()){
360
4607
            next = var_Undef;
361
4607
            break;
362
        }else
363
27990188
            next = order_heap.removeMin();
364
365
6744847
    return next == var_Undef ? lit_Undef : mkLit(next, rnd_pol ? drand(random_seed) < 0.5 : polarity[next]);
366
}
367
368
/*_________________________________________________________________________________________________
369
|
370
|  analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&)  ->
371
[void]
372
|
373
|  Description:
374
|    Analyze conflict and produce a reason clause.
375
|
376
|    Pre-conditions:
377
|      * 'out_learnt' is assumed to be cleared.
378
|      * Current decision level must be greater than root level.
379
|
380
|    Post-conditions:
381
|      * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'.
382
|      * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision
383
level of the |        rest of literals. There may be others from the same level
384
though.
385
|
386
|________________________________________________________________________________________________@*/
387
204987
void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip)
388
{
389
204987
    int pathC = 0;
390
204987
    Lit p     = lit_Undef;
391
392
    // Generate conflict clause:
393
    //
394
204987
    out_learnt.push();      // (leave room for the asserting literal)
395
204987
    int index   = trail.size() - 1;
396
397
204987
    bool done = false;
398
399
12295658
    do{
400
12500645
      Assert(confl != CRef_Undef);  // (otherwise should be UIP)
401
12500645
      Clause& clause = ca[confl];
402
403
12500645
      if (clause.learnt()) claBumpActivity(clause);
404
405
68430166
      for (int j = (p == lit_Undef) ? 0 : 1; j < clause.size(); j++)
406
      {
407
55929521
        Lit q = clause[j];
408
409
55929521
        if (!seen[var(q)] && level(var(q)) > 0)
410
        {
411
25391681
          varBumpActivity(var(q));
412
25391681
          seen[var(q)] = 1;
413
25391681
          if (level(var(q)) >= decisionLevel())
414
12500645
            pathC++;
415
          else
416
12891036
            out_learnt.push(q);
417
        }
418
      }
419
420
        // Select next clause to look at:
421
58157115
        while (!seen[var(trail[index--])]);
422
12500645
        p     = trail[index+1];
423
12500645
        confl = reason(var(p));
424
12500645
        seen[var(p)] = 0;
425
12500645
        pathC--;
426
427
12500645
        switch (uip) {
428
12500645
        case UIP_FIRST:
429
12500645
          done = pathC == 0;
430
12500645
          break;
431
        case UIP_LAST:
432
          done = confl == CRef_Undef || (pathC == 0 && marker[var(p)] == 2);
433
          break;
434
        default:
435
          Unreachable();
436
          break;
437
        }
438
12500645
    } while (!done);
439
204987
    out_learnt[0] = ~p;
440
441
    // Simplify conflict clause:
442
    //
443
    int i1, j;
444
204987
    out_learnt.copyTo(analyze_toclear);
445
204987
    if (ccmin_mode == 2){
446
        uint32_t abstract_level = 0;
447
        for (i1 = 1; i1 < out_learnt.size(); i1++)
448
          abstract_level |= abstractLevel(
449
              var(out_learnt[i1]));  // (maintain an abstraction of levels
450
                                     // involved in conflict)
451
452
        for (i1 = j = 1; i1 < out_learnt.size(); i1++)
453
        {
454
          if (reason(var(out_learnt[i1])) == CRef_Undef)
455
          {
456
            out_learnt[j++] = out_learnt[i1];
457
          }
458
          else
459
          {
460
            // Check if the literal is redundant
461
            if (!litRedundant(out_learnt[i1], abstract_level))
462
            {
463
              // Literal is not redundant
464
              out_learnt[j++] = out_learnt[i1];
465
            }
466
          }
467
        }
468
204987
    }else if (ccmin_mode == 1){
469
        Unreachable();
470
        for (i1 = j = 1; i1 < out_learnt.size(); i1++)
471
        {
472
          Var x = var(out_learnt[i1]);
473
474
          if (reason(x) == CRef_Undef)
475
            out_learnt[j++] = out_learnt[i1];
476
          else
477
          {
478
            Clause& clause = ca[reason(var(out_learnt[i1]))];
479
            for (int k = 1; k < clause.size(); k++)
480
              if (!seen[var(clause[k])] && level(var(clause[k])) > 0)
481
              {
482
                out_learnt[j++] = out_learnt[i1];
483
                break;
484
              }
485
          }
486
        }
487
    }else
488
204987
      i1 = j = out_learnt.size();
489
490
204987
    max_literals += out_learnt.size();
491
204987
    out_learnt.shrink(i1 - j);
492
204987
    tot_literals += out_learnt.size();
493
494
204987
    for (int i2 = 0; i2 < out_learnt.size(); ++i2)
495
    {
496
204987
      if (marker[var(out_learnt[i2])] == 0)
497
      {
498
204987
        break;
499
      }
500
    }
501
502
    // Find correct backtrack level:
503
    //
504
204987
    if (out_learnt.size() == 1) {
505
356
      out_btlevel = 0;
506
    }
507
    else{
508
204631
        int max_i = 1;
509
        // Find the first literal assigned at the next-highest level:
510
12891036
        for (int i3 = 2; i3 < out_learnt.size(); i3++)
511
12686405
          if (level(var(out_learnt[i3])) > level(var(out_learnt[max_i])))
512
311976
            max_i = i3;
513
        // Swap-in this literal at i1 1:
514
204631
        Lit p2 = out_learnt[max_i];
515
204631
        out_learnt[max_i] = out_learnt[1];
516
204631
        out_learnt[1] = p2;
517
204631
        out_btlevel = level(var(p2));
518
    }
519
520
13301010
    for (int j2 = 0; j2 < analyze_toclear.size(); j2++)
521
13096023
      seen[var(analyze_toclear[j2])] = 0;  // ('seen[]' is now cleared)
522
204987
}
523
524
525
// Check if 'p' can be removed. 'abstract_levels' is used to abort early if the algorithm is
526
// visiting literals at levels that cannot be removed later.
527
bool Solver::litRedundant(Lit p, uint32_t abstract_levels)
528
{
529
    analyze_stack.clear(); analyze_stack.push(p);
530
    int top = analyze_toclear.size();
531
    while (analyze_stack.size() > 0){
532
        CRef c_reason = reason(var(analyze_stack.last()));
533
        Assert(c_reason != CRef_Undef);
534
        Clause& clause = ca[c_reason];
535
        int c_size = clause.size();
536
        analyze_stack.pop();
537
538
        for (int i = 1; i < c_size; i++){
539
          Lit p2 = clause[i];
540
          if (!seen[var(p2)] && level(var(p2)) > 0)
541
          {
542
            if (reason(var(p2)) != CRef_Undef
543
                && (abstractLevel(var(p2)) & abstract_levels) != 0)
544
            {
545
              seen[var(p2)] = 1;
546
              analyze_stack.push(p2);
547
              analyze_toclear.push(p2);
548
            }
549
            else
550
            {
551
              for (int j = top; j < analyze_toclear.size(); j++)
552
                seen[var(analyze_toclear[j])] = 0;
553
              analyze_toclear.shrink(analyze_toclear.size() - top);
554
              return false;
555
            }
556
          }
557
        }
558
    }
559
560
    return true;
561
}
562
563
/**
564
 * Specialized analyzeFinal procedure where we test the consistency
565
 * of the assumptions before backtracking bellow the assumption level.
566
 *
567
 * @param p the original uip (may be unit)
568
 * @param confl_clause the conflict clause
569
 * @param out_conflict the conflict in terms of assumptions we are building
570
 */
571
697
void Solver::analyzeFinal2(Lit p, CRef confl_clause, vec<Lit>& out_conflict) {
572
697
  Assert(confl_clause != CRef_Undef);
573
697
  Assert(decisionLevel() == assumptions.size());
574
697
  Assert(level(var(p)) == assumptions.size());
575
576
697
  out_conflict.clear();
577
578
697
  Clause& cl = ca[confl_clause];
579
8532
  for (int i = 0; i < cl.size(); ++i) {
580
7835
    seen[var(cl[i])] = 1;
581
  }
582
583
697
  int end = trail_lim[0];
584
4228134
  for (int i = trail.size() - 1; i >= end; i--) {
585
4227437
    Var x = var(trail[i]);
586
4227437
    if (seen[x]) {
587
256515
      if (reason(x) == CRef_Undef) {
588
        // we skip p if was a learnt unit
589
16849
        if (x != var(p)) {
590
16827
          if (marker[x] == 2) {
591
16827
            Assert(level(x) > 0);
592
16827
            out_conflict.push(~trail[i]);
593
          }
594
        }
595
      } else {
596
239666
        Clause& clause = ca[reason(x)];
597
598
688373
        for (int j = 1; j < clause.size(); j++)
599
        {
600
448707
          if (level(var(clause[j])) > 0) seen[var(clause[j])] = 1;
601
        }
602
      }
603
256515
      seen[x] = 0;
604
    }
605
4227437
    Assert(seen[x] == 0);
606
  }
607
697
  Assert(out_conflict.size());
608
697
}
609
610
/*_________________________________________________________________________________________________
611
|
612
|  analyzeFinal : (p : Lit)  ->  [void]
613
|
614
|  Description:
615
|    Specialized analysis procedure to express the final conflict in terms of
616
assumptions. |    Calculates the (possibly empty) set of assumptions that led to
617
the assignment of 'p', and |    stores the result in 'out_conflict'.
618
|________________________________________________________________________________________________@*/
619
11415
void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
620
{
621
11415
    out_conflict.clear();
622
11415
    if (marker[var(p)] == 2) {
623
1376
      out_conflict.push(p);
624
    }
625
626
11415
    if (decisionLevel() == 0)
627
    {
628
46
      return;
629
    }
630
631
11369
    seen[var(p)] = 1;
632
11369
    int end = trail_lim[0];
633
634
44502833
    for (int i = trail.size()-1; i >= end; i--){
635
44491464
        Var x = var(trail[i]);
636
44491464
        if (seen[x]) {
637
1102287
            if (reason(x) == CRef_Undef) {
638
109387
              Assert(marker[x] == 2);
639
109387
              Assert(level(x) > 0);
640
109387
              if (~trail[i] != p)
641
              {
642
109387
                out_conflict.push(~trail[i]);
643
              }
644
            } else {
645
992900
              Clause& clause = ca[reason(x)];
646
2438309
              for (int j = 1; j < clause.size(); j++)
647
              {
648
1445409
                if (level(var(clause[j])) > 0)
649
                {
650
1445221
                  seen[var(clause[j])] = 1;
651
                }
652
              }
653
            }
654
1102287
            seen[x] = 0;
655
        }
656
    }
657
658
11369
    seen[var(p)] = 0;
659
11369
    Assert(out_conflict.size());
660
}
661
662
663
222645159
void Solver::uncheckedEnqueue(Lit p, CRef from)
664
{
665
222645159
  Assert(value(p) == l_Undef);
666
222645159
  assigns[var(p)] = lbool(!sign(p));
667
222645159
  vardata[var(p)] = mkVarData(from, decisionLevel());
668
222645159
  trail.push_(p);
669
222645159
  if (decisionLevel() <= assumptions.size() && marker[var(p)] == 1)
670
  {
671
1844162
    if (d_notify)
672
    {
673
3688324
      Debug("bvminisat::explain")
674
1844162
          << OUTPUT_TAG << "propagating " << p << std::endl;
675
1844162
      d_notify->notify(p);
676
    }
677
  }
678
222645159
}
679
680
619545
void Solver::popAssumption() {
681
619545
    assumptions.pop();
682
619545
    conflict.clear();
683
619545
    cancelUntil(assumptions.size());
684
619545
}
685
686
171639
lbool Solver::propagateAssumptions() {
687
171639
  only_bcp = true;
688
171639
  ccmin_mode = 0;
689
171639
  return search(-1);
690
}
691
692
619545
lbool Solver::assertAssumption(Lit p, bool propagate) {
693
  // TODO need to somehow mark the assumption as unit in the current context?
694
  // it's not always unit though, but this would be useful for debugging
695
696
  // Assert(marker[var(p)] == 1);
697
698
619545
  if (decisionLevel() > assumptions.size()) {
699
5
    cancelUntil(assumptions.size());
700
  }
701
702
619545
  conflict.clear();
703
704
  // add to the assumptions
705
619545
  if (c->getLevel() > 0) {
706
619545
    assumptions.push(p);
707
  } else {
708
    ClauseId id;
709
    if (!addClause(p, id)) {
710
      conflict.push(~p);
711
      return l_False;
712
    }
713
  }
714
715
  // run the propagation
716
619545
  if (propagate) {
717
619545
    only_bcp = true;
718
619545
    ccmin_mode = 0;
719
619545
    lbool result = search(-1);
720
619545
    return result;
721
  } else {
722
    return l_True;
723
  }
724
}
725
726
71653
void Solver::addMarkerLiteral(Var var) {
727
  // make sure it wasn't already marked
728
71653
  Assert(marker[var] == 0);
729
71653
  marker[var] = 1;
730
71653
}
731
732
/*_________________________________________________________________________________________________
733
|
734
|  propagate : [void]  ->  [Clause*]
735
|
736
|  Description:
737
|    Propagates all enqueued facts. If a conflict arises, the conflicting clause
738
is returned, |    otherwise CRef_Undef.
739
|
740
|    Post-conditions:
741
|      * the propagation queue is empty, even if there was a conflict.
742
|________________________________________________________________________________________________@*/
743
10641572
CRef Solver::propagate()
744
{
745
10641572
    CRef    confl     = CRef_Undef;
746
10641572
    int     num_props = 0;
747
10641572
    watches.cleanAll();
748
749
447712544
    while (qhead < trail.size()){
750
218535486
        Lit            p   = trail[qhead++];     // 'p' is enqueued fact to propagate.
751
218535486
        vec<Watcher>&  ws  = watches[p];
752
        Watcher        *i, *j, *end;
753
218535486
        num_props++;
754
755
867371146
        for (i = j = (Watcher*)ws, end = i + ws.size();  i != end;){
756
            // Try to avoid inspecting the clause:
757
648835660
            Lit blocker = i->blocker;
758
1036104575
            if (value(blocker) == l_True){
759
1169551358
                *j++ = *i++; continue; }
760
761
            // Make sure the false literal is data[1]:
762
261566745
            CRef     cr        = i->cref;
763
261566745
            Clause& clause = ca[cr];
764
261566745
            Lit      false_lit = ~p;
765
261566745
            if (clause[0] == false_lit)
766
26233982
              clause[0] = clause[1], clause[1] = false_lit;
767
261566745
            Assert(clause[1] == false_lit);
768
261566745
            i++;
769
770
            // If 0th watch is true, then clause is already satisfied.
771
261566745
            Lit first = clause[0];
772
261566745
            Watcher w     = Watcher(cr, first);
773
269311358
            if (first != blocker && value(first) == l_True){
774
15489226
                *j++ = w; continue; }
775
776
            // Look for new watch:
777
713989510
            for (int k = 2; k < clause.size(); k++)
778
500965163
              if (value(clause[k]) != l_False)
779
              {
780
40797785
                clause[1] = clause[k];
781
40797785
                clause[k] = false_lit;
782
40797785
                watches[~clause[1]].push(w);
783
40797785
                goto NextClause;
784
              }
785
786
            // Did not find watch -- clause is unit under assignment:
787
213024347
            *j++ = w;
788
213024347
            if (value(first) == l_False){
789
205690
                confl = cr;
790
205690
                qhead = trail.size();
791
                // Copy the remaining watches:
792
2006614
                while (i < end)
793
900462
                    *j++ = *i++;
794
            }else
795
212818657
                uncheckedEnqueue(first, cr);
796
797
253822132
        NextClause:;
798
        }
799
218535486
        ws.shrink(i - j);
800
    }
801
10641572
    propagations += num_props;
802
10641572
    simpDB_props -= num_props;
803
804
10641572
    return confl;
805
}
806
807
/*_________________________________________________________________________________________________
808
|
809
|  reduceDB : ()  ->  [void]
810
|
811
|  Description:
812
|    Remove half of the learnt clauses, minus the clauses locked by the current
813
assignment. Locked |    clauses are clauses that are reason to some assignment.
814
Binary clauses are never removed.
815
|________________________________________________________________________________________________@*/
816
struct reduceDB_lt
817
{
818
  ClauseAllocator& ca;
819
30
  reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) {}
820
599747
  bool operator()(CRef x, CRef y)
821
  {
822
599747
    return ca[x].size() > 2
823
599747
           && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity());
824
  }
825
};
826
30
void Solver::reduceDB()
827
{
828
    int     i, j;
829
30
    double  extra_lim = cla_inc / learnts.size();    // Remove any clause below this activity
830
831
30
    sort(learnts, reduceDB_lt(ca));
832
    // Don't delete binary or locked clauses. From the rest, delete clauses from the first half
833
    // and clauses with activity smaller than 'extra_lim':
834
38557
    for (i = j = 0; i < learnts.size(); i++){
835
38527
      Clause& clause = ca[learnts[i]];
836
114152
      if (clause.size() > 2 && !locked(clause)
837
75619
          && (i < learnts.size() / 2 || clause.activity() < extra_lim))
838
19248
        removeClause(learnts[i]);
839
      else
840
19279
        learnts[j++] = learnts[i];
841
    }
842
30
    learnts.shrink(i - j);
843
30
    checkGarbage();
844
30
}
845
846
847
1610
void Solver::removeSatisfied(vec<CRef>& cs)
848
{
849
    int i, j;
850
17535
    for (i = j = 0; i < cs.size(); i++){
851
15925
      Clause& clause = ca[cs[i]];
852
15925
      if (satisfied(clause))
853
      {
854
91
        removeClause(cs[i]);
855
      }
856
        else
857
15834
            cs[j++] = cs[i];
858
    }
859
1610
    cs.shrink(i - j);
860
1610
}
861
862
863
1610
void Solver::rebuildOrderHeap()
864
{
865
3220
    vec<Var> vs;
866
1628827
    for (Var v = 0; v < nVars(); v++)
867
1627217
        if (decision[v] && value(v) == l_Undef)
868
1618641
            vs.push(v);
869
1610
    order_heap.build(vs);
870
1610
}
871
872
/*_________________________________________________________________________________________________
873
|
874
|  simplify : [void]  ->  [bool]
875
|
876
|  Description:
877
|    Simplify the clause database according to the current top-level assigment.
878
Currently, the only |    thing done here is the removal of satisfied clauses,
879
but more things can be put here.
880
|________________________________________________________________________________________________@*/
881
28617
bool Solver::simplify()
882
{
883
28617
  Assert(decisionLevel() == 0);
884
885
28617
  if (!ok || propagate() != CRef_Undef) return ok = false;
886
887
28613
  if (nAssigns() == simpDB_assigns || (simpDB_props > 0)) return true;
888
889
1610
  d_notify->spendResource(ResourceManager::Resource::BvSatSimplifyStep);
890
891
  // Remove satisfied clauses:
892
1610
  removeSatisfied(learnts);
893
1610
  if (remove_satisfied)  // Can be turned off.
894
    removeSatisfied(clauses);
895
1610
  checkGarbage();
896
1610
  rebuildOrderHeap();
897
898
1610
  simpDB_assigns = nAssigns();
899
1610
  simpDB_props =
900
1610
      clauses_literals + learnts_literals;  // (shouldn't depend on stats
901
                                            // really, but it will do for now)
902
903
1610
  return true;
904
}
905
906
/*_________________________________________________________________________________________________
907
|
908
|  search : (nof_conflicts : int) (params : const SearchParams&)  ->  [lbool]
909
|
910
|  Description:
911
|    Search for a model the specified number of conflicts.
912
|    NOTE! Use negative value for 'nof_conflicts' indicate infinity.
913
|
914
|  Output:
915
|    'l_True' if a partial assigment that is consistent with respect to the
916
clauseset is found. If |    all variables are decision variables, this means
917
that the clause set is satisfiable. 'l_False' |    if the clause set is
918
unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached.
919
|________________________________________________________________________________________________@*/
920
802924
lbool Solver::search(int nof_conflicts, UIP uip)
921
{
922
802924
  Assert(ok);
923
  int backtrack_level;
924
802924
  int conflictC = 0;
925
1605848
  vec<Lit> learnt_clause;
926
802924
  starts++;
927
928
  for (;;)
929
  {
930
10604494
    d_notify->safePoint(ResourceManager::Resource::BvSatPropagateStep);
931
10604494
    CRef confl = propagate();
932
10604494
    if (confl != CRef_Undef)
933
    {
934
      // CONFLICT
935
204993
      conflicts++;
936
204993
      conflictC++;
937
938
204993
      if (decisionLevel() == 0)
939
      {
940
        // can this happen for bv?
941
6
        return l_False;
942
      }
943
944
204987
      learnt_clause.clear();
945
204987
      analyze(confl, learnt_clause, backtrack_level, uip);
946
947
204987
      Lit p = learnt_clause[0];
948
      // bool assumption = marker[var(p)] == 2;
949
950
204987
      CRef cr = CRef_Undef;
951
204987
      if (learnt_clause.size() > 1)
952
      {
953
204631
        cr = ca.alloc(learnt_clause, true);
954
204631
        learnts.push(cr);
955
204631
        attachClause(cr);
956
204631
        claBumpActivity(ca[cr]);
957
      }
958
959
204987
      if (learnt_clause.size() == 1)
960
      {
961
        // learning a unit clause
962
      }
963
964
      //  if the uip was an assumption we are unsat
965
204987
      if (level(var(p)) <= assumptions.size())
966
      {
967
249616
        for (int i = 0; i < learnt_clause.size(); ++i)
968
        {
969
239577
          Assert(level(var(learnt_clause[i])) <= decisionLevel());
970
239577
          seen[var(learnt_clause[i])] = 1;
971
        }
972
973
10039
        analyzeFinal(p, conflict);
974
20078
        Debug("bvminisat::search")
975
10039
            << OUTPUT_TAG << " conflict on assumptions " << std::endl;
976
10039
        return l_False;
977
      }
978
979
2261719
      if (!CVC4::options::bvEagerExplanations())
980
      {
981
        // check if uip leads to a conflict
982
81885
        if (backtrack_level < assumptions.size())
983
        {
984
1898
          cancelUntil(assumptions.size());
985
1898
          uncheckedEnqueue(p, cr);
986
987
1898
          CRef new_confl = propagate();
988
1898
          if (new_confl != CRef_Undef)
989
          {
990
            // we have a conflict we now need to explain it
991
697
            analyzeFinal2(p, new_confl, conflict);
992
697
            return l_False;
993
          }
994
        }
995
      }
996
997
194251
      cancelUntil(backtrack_level);
998
194251
      uncheckedEnqueue(p, cr);
999
1000
194251
      varDecayActivity();
1001
194251
      claDecayActivity();
1002
1003
194251
      if (--learntsize_adjust_cnt == 0)
1004
      {
1005
384
        learntsize_adjust_confl *= learntsize_adjust_inc;
1006
384
        learntsize_adjust_cnt = (int)learntsize_adjust_confl;
1007
384
        max_learnts *= learntsize_inc;
1008
1009
384
        if (verbosity >= 1)
1010
          printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n",
1011
                 (int)conflicts,
1012
                 (int)dec_vars
1013
                     - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]),
1014
                 nClauses(),
1015
                 (int)clauses_literals,
1016
                 (int)max_learnts,
1017
                 nLearnts(),
1018
                 (double)learnts_literals / nLearnts(),
1019
                 progressEstimate() * 100);
1020
      }
1021
    }
1022
    else
1023
    {
1024
      // NO CONFLICT
1025
      bool isWithinBudget;
1026
      try
1027
      {
1028
10399501
        isWithinBudget =
1029
            withinBudget(ResourceManager::Resource::BvSatConflictsStep);
1030
      }
1031
      catch (const CVC4::theory::Interrupted& e)
1032
      {
1033
        // do some clean-up and rethrow
1034
        cancelUntil(assumptions.size());
1035
        throw e;
1036
      }
1037
1038
27510755
      if ((decisionLevel() > assumptions.size() && nof_conflicts >= 0
1039
6711638
           && conflictC >= nof_conflicts)
1040
20796430
          || !isWithinBudget)
1041
      {
1042
        // Reached bound on number of conflicts:
1043
2572
        Debug("bvminisat::search") << OUTPUT_TAG << " restarting " << std::endl;
1044
2572
        progress_estimate = progressEstimate();
1045
2572
        cancelUntil(assumptions.size());
1046
2572
        return l_Undef;
1047
      }
1048
1049
      // Simplify the set of problem clauses:
1050
10396929
      if (decisionLevel() == 0 && !simplify())
1051
      {
1052
        Debug("bvminisat::search")
1053
            << OUTPUT_TAG << " base level conflict, we're unsat" << std::endl;
1054
        return l_False;
1055
      }
1056
1057
      // We can't erase clauses if there is unprocessed assumptions, there might
1058
      // be some propagationg we need to redu
1059
20793858
      if (decisionLevel() >= assumptions.size()
1060
10396929
          && learnts.size() - nAssigns() >= max_learnts)
1061
      {
1062
        // Reduce the set of learnt clauses:
1063
60
        Debug("bvminisat::search")
1064
30
            << OUTPUT_TAG << " cleaning up database" << std::endl;
1065
30
        reduceDB();
1066
      }
1067
1068
10396929
      Lit next = lit_Undef;
1069
11675565
      while (decisionLevel() < assumptions.size())
1070
      {
1071
        // Perform user provided assumption:
1072
3507773
        Lit p = assumptions[decisionLevel()];
1073
3507773
        if (value(p) == l_True)
1074
        {
1075
          // Dummy decision level:
1076
639318
          newDecisionLevel();
1077
        }
1078
2868455
        else if (value(p) == l_False)
1079
        {
1080
1376
          marker[var(p)] = 2;
1081
1082
1376
          analyzeFinal(~p, conflict);
1083
2752
          Debug("bvminisat::search")
1084
1376
              << OUTPUT_TAG << " assumption false, we're unsat" << std::endl;
1085
1376
          return l_False;
1086
        }
1087
        else
1088
        {
1089
2867079
          marker[var(p)] = 2;
1090
2867079
          next = p;
1091
2867079
          break;
1092
        }
1093
      }
1094
1095
10395553
      if (next == lit_Undef)
1096
      {
1097
7528474
        if (only_bcp)
1098
        {
1099
1567254
          Debug("bvminisat::search")
1100
1567254
              << OUTPUT_TAG << " only bcp, skipping rest of the problem"
1101
783627
              << std::endl;
1102
783627
          return l_True;
1103
        }
1104
1105
        // New variable decision:
1106
6744847
        decisions++;
1107
6744847
        next = pickBranchLit();
1108
1109
6744847
        if (next == lit_Undef)
1110
        {
1111
9214
          Debug("bvminisat::search")
1112
4607
              << OUTPUT_TAG << " satisfiable" << std::endl;
1113
          // Model found:
1114
4607
          return l_True;
1115
        }
1116
      }
1117
1118
      // Increase decision level and enqueue 'next'
1119
9607319
      newDecisionLevel();
1120
9607319
      uncheckedEnqueue(next);
1121
    }
1122
9801570
  }
1123
}
1124
1125
1126
2572
double Solver::progressEstimate() const
1127
{
1128
2572
    double  progress = 0;
1129
2572
    double  F = 1.0 / nVars();
1130
1131
367822
    for (int i = 0; i <= decisionLevel(); i++){
1132
365250
        int beg = i == 0 ? 0 : trail_lim[i - 1];
1133
365250
        int end = i == decisionLevel() ? trail.size() : trail_lim[i];
1134
365250
        progress += pow(F, i) * (end - beg);
1135
    }
1136
1137
2572
    return progress / nVars();
1138
}
1139
1140
/*
1141
  Finite subsequences of the Luby-sequence:
1142
1143
  0: 1
1144
  1: 1 1 2
1145
  2: 1 1 2 1 1 2 4
1146
  3: 1 1 2 1 1 2 4 1 1 2 1 1 2 4 8
1147
  ...
1148
1149
1150
 */
1151
1152
11740
static double luby(double y, int x){
1153
1154
    // Find the finite subsequence that contains index 'x', and the
1155
    // size of that subsequence:
1156
    int size, seq;
1157
11740
    for (size = 1, seq = 0; size < x+1; seq++, size = 2*size+1);
1158
1159
18422
    while (size-1 != x){
1160
3341
        size = (size-1)>>1;
1161
3341
        seq--;
1162
3341
        x = x % size;
1163
    }
1164
1165
11740
    return pow(y, seq);
1166
}
1167
1168
// NOTE: assumptions passed in member-variable 'assumptions'.
1169
9168
lbool Solver::solve_()
1170
{
1171
9168
    Debug("bvminisat") <<"BVMinisat::Solving learned clauses " << learnts.size() <<"\n";
1172
9168
    Debug("bvminisat") <<"BVMinisat::Solving assumptions " << assumptions.size() <<"\n";
1173
1174
9168
    model.clear();
1175
9168
    conflict.clear();
1176
1177
9168
    ccmin_mode = 0;
1178
1179
9168
    if (!ok) return l_False;
1180
1181
9168
    solves++;
1182
1183
9168
    max_learnts               = nClauses() * learntsize_factor;
1184
9168
    learntsize_adjust_confl   = learntsize_adjust_start_confl;
1185
9168
    learntsize_adjust_cnt     = (int)learntsize_adjust_confl;
1186
9168
    lbool   status            = l_Undef;
1187
1188
9168
    if (verbosity >= 1){
1189
        printf("============================[ Search Statistics ]==============================\n");
1190
        printf("| Conflicts |          ORIGINAL         |          LEARNT          | Progress |\n");
1191
        printf("|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |\n");
1192
        printf("===============================================================================\n");
1193
    }
1194
1195
    // Search:
1196
9168
    int curr_restarts = 0;
1197
32648
    while (status == l_Undef){
1198
11740
        double rest_base = luby_restart ? luby(restart_inc, curr_restarts) : pow(restart_inc, curr_restarts);
1199
11740
        status = search(rest_base * restart_first);
1200
11740
        if (!withinBudget(ResourceManager::Resource::BvSatConflictsStep)) break;
1201
11740
        curr_restarts++;
1202
    }
1203
1204
9168
    if (verbosity >= 1)
1205
        printf("===============================================================================\n");
1206
1207
9168
    if (status == l_True){
1208
        // Extend & copy model:
1209
        // model.growTo(nVars());
1210
        // for (int i = 0; i < nVars(); i++) model[i] = value(i);
1211
4561
    }else if (status == l_False && conflict.size() == 0)
1212
6
        ok = false;
1213
1214
9168
    return status;
1215
}
1216
1217
//=================================================================================================
1218
// Bitvector propagations
1219
//
1220
1221
84079
void Solver::explain(Lit p, std::vector<Lit>& explanation) {
1222
84079
  Debug("bvminisat::explain") << OUTPUT_TAG << "starting explain of " << p << std::endl;
1223
1224
  // top level fact, no explanation necessary
1225
84079
  if (level(var(p)) == 0) {
1226
805
    return;
1227
  }
1228
1229
83274
  seen[var(p)] = 1;
1230
1231
  // if we are called at decisionLevel = 0 trail_lim is empty
1232
83274
  int bottom = trail_lim[0];
1233
312348180
  for (int i = trail.size()-1; i >= bottom; i--){
1234
312264906
    Var x = var(trail[i]);
1235
312264906
    if (seen[x]) {
1236
4017892
      if (reason(x) == CRef_Undef) {
1237
374078
        if (marker[x] == 2) {
1238
374078
          Assert(level(x) > 0);
1239
374078
          explanation.push_back(trail[i]);
1240
        } else {
1241
          Assert(level(x) == 0);
1242
         }
1243
      } else {
1244
3643814
        Clause& clause = ca[reason(x)];
1245
9755978
        for (int j = 1; j < clause.size(); j++)
1246
        {
1247
6112164
          if (level(var(clause[j])) > 0)
1248
          {
1249
6112086
            seen[var(clause[j])] = 1;
1250
          }
1251
        }
1252
      }
1253
4017892
      seen[x] = 0;
1254
    }
1255
  }
1256
83274
  seen[var(p)] = 0;
1257
}
1258
1259
//=================================================================================================
1260
// Writing CNF to DIMACS:
1261
//
1262
// FIXME: this needs to be rewritten completely.
1263
1264
static Var mapVar(Var x, vec<Var>& map, Var& max)
1265
{
1266
    if (map.size() <= x || map[x] == -1){
1267
        map.growTo(x+1, -1);
1268
        map[x] = max++;
1269
    }
1270
    return map[x];
1271
}
1272
1273
void Solver::toDimacs(FILE* f, Clause& clause, vec<Var>& map, Var& max)
1274
{
1275
  if (satisfied(clause)) return;
1276
1277
  for (int i = 0; i < clause.size(); i++)
1278
    if (value(clause[i]) != l_False)
1279
      fprintf(f,
1280
              "%s%d ",
1281
              sign(clause[i]) ? "-" : "",
1282
              mapVar(var(clause[i]), map, max) + 1);
1283
  fprintf(f, "0\n");
1284
}
1285
1286
1287
void Solver::toDimacs(const char *file, const vec<Lit>& assumps)
1288
{
1289
    FILE* f = fopen(file, "wr");
1290
    if (f == NULL)
1291
        fprintf(stderr, "could not open file %s\n", file), exit(1);
1292
    toDimacs(f, assumps);
1293
    fclose(f);
1294
}
1295
1296
1297
void Solver::toDimacs(FILE* f, const vec<Lit>& assumps)
1298
{
1299
    // Handle case when solver is in contradictory state:
1300
    if (!ok){
1301
        fprintf(f, "p cnf 1 2\n1 0\n-1 0\n");
1302
        return; }
1303
1304
    vec<Var> map; Var max = 0;
1305
1306
    // Cannot use removeClauses here because it is not safe
1307
    // to deallocate them at this point. Could be improved.
1308
    int cnt = 0;
1309
    for (int i = 0; i < clauses.size(); i++)
1310
        if (!satisfied(ca[clauses[i]]))
1311
            cnt++;
1312
1313
    for (int i = 0; i < clauses.size(); i++)
1314
        if (!satisfied(ca[clauses[i]])){
1315
          Clause& clause = ca[clauses[i]];
1316
          for (int j = 0; j < clause.size(); j++)
1317
            if (value(clause[j]) != l_False) mapVar(var(clause[j]), map, max);
1318
        }
1319
1320
    // Assumptions are added as unit clauses:
1321
    cnt += assumps.size();
1322
1323
    fprintf(f, "p cnf %d %d\n", max, cnt);
1324
1325
    for (int i = 0; i < assumps.size(); i++){
1326
      Assert(value(assumps[i]) != l_False);
1327
      fprintf(f,
1328
              "%s%d 0\n",
1329
              sign(assumps[i]) ? "-" : "",
1330
              mapVar(var(assumps[i]), map, max) + 1);
1331
    }
1332
1333
    for (int i = 0; i < clauses.size(); i++)
1334
        toDimacs(f, ca[clauses[i]], map, max);
1335
1336
    if (verbosity > 0)
1337
        printf("Wrote %d clauses with %d variables.\n", cnt, max);
1338
}
1339
1340
1341
//=================================================================================================
1342
// Garbage Collection methods:
1343
1344
72
void Solver::relocAll(ClauseAllocator& to)
1345
{
1346
    // All watchers:
1347
    //
1348
    // for (int i = 0; i < watches.size(); i++)
1349
72
    watches.cleanAll();
1350
35738
    for (int v = 0; v < nVars(); v++)
1351
106998
        for (int s = 0; s < 2; s++){
1352
71332
            Lit p = mkLit(v, s);
1353
            // printf(" >>> RELOCING: %s%d\n", sign(p)?"-":"", var(p)+1);
1354
71332
            vec<Watcher>& ws = watches[p];
1355
71332
            for (int j = 0; j < ws.size(); j++) ca.reloc(ws[j].cref, to);
1356
        }
1357
1358
    // All reasons:
1359
    //
1360
3091
    for (int i = 0; i < trail.size(); i++){
1361
3019
        Var v = var(trail[i]);
1362
1363
3019
        if (reason(v) != CRef_Undef && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
1364
1067
          ca.reloc(vardata[v].reason, to);
1365
    }
1366
1367
    // All learnt:
1368
    //
1369
72
    for (int i = 0; i < learnts.size(); i++) ca.reloc(learnts[i], to);
1370
1371
    // All original:
1372
    //
1373
72
    for (int i = 0; i < clauses.size(); i++) ca.reloc(clauses[i], to);
1374
72
}
1375
1376
1377
void Solver::garbageCollect()
1378
{
1379
    // Initialize the next region to a size corresponding to the estimated utilization degree. This
1380
    // is not precise but should avoid some unnecessary reallocations for the new region:
1381
    ClauseAllocator to(ca.size() - ca.wasted());
1382
    Debug("bvminisat") << " BVMinisat::Garbage collection \n";
1383
    relocAll(to);
1384
    if (verbosity >= 2)
1385
      printf(
1386
          "|  Garbage collection:   %12d bytes => %12d bytes             |\n",
1387
          ca.size() * ClauseAllocator::Unit_Size,
1388
          to.size() * ClauseAllocator::Unit_Size);
1389
    to.moveTo(ca);
1390
}
1391
1392
687274
void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to)
1393
{
1394
687274
  Clause& c = operator[](cr);
1395
687274
  if (c.reloced()) { cr = c.relocation(); return; }
1396
1397
128279
  cr = to.alloc(c, c.learnt());
1398
128279
  c.relocate(cr);
1399
1400
  // Copy extra data-fields:
1401
  // (This could be cleaned-up. Generalize Clause-constructor to be applicable
1402
  // here instead?)
1403
128279
  to[cr].mark(c.mark());
1404
128279
  if (to[cr].learnt())         to[cr].activity() = c.activity();
1405
110326
  else if (to[cr].has_extra()) to[cr].calcAbstraction();
1406
}
1407
1408
8975
void Solver::setNotify(Notify* toNotify) { d_notify = toNotify; }
1409
10411241
bool Solver::withinBudget(ResourceManager::Resource r) const
1410
{
1411
10411241
  AlwaysAssert(d_notify);
1412
10411241
  d_notify->safePoint(r);
1413
1414
20822482
  return !asynch_interrupt &&
1415
31233723
         (conflict_budget < 0 || conflicts < (uint64_t)conflict_budget) &&
1416
10411241
         (propagation_budget < 0 ||
1417
10411241
          propagations < (uint64_t)propagation_budget);
1418
}
1419
1420
} /* CVC4::BVMinisat namespace */
1421
2093447
} /* CVC4 namespace */