GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/minisat/core/Solver.cc Lines: 920 1123 81.9 %
Date: 2021-03-22 Branches: 1459 3346 43.6 %

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/minisat/core/Solver.h"
22
23
#include <math.h>
24
25
#include <iostream>
26
#include <unordered_set>
27
28
#include "base/check.h"
29
#include "base/output.h"
30
#include "options/main_options.h"
31
#include "options/prop_options.h"
32
#include "options/smt_options.h"
33
#include "proof/clause_id.h"
34
#include "proof/cnf_proof.h"
35
#include "proof/proof_manager.h"
36
#include "proof/sat_proof.h"
37
#include "proof/sat_proof_implementation.h"
38
#include "prop/minisat/minisat.h"
39
#include "prop/minisat/mtl/Sort.h"
40
#include "prop/theory_proxy.h"
41
42
using namespace CVC4::prop;
43
44
namespace CVC4 {
45
namespace Minisat {
46
47
namespace {
48
/*
49
 * Returns true if the solver should add all clauses at the current assertion
50
 * level.
51
 *
52
 * FIXME: This is a workaround. Currently, our resolution proofs do not
53
 * handle clauses with a lower-than-assertion-level correctly because the
54
 * resolution proofs get removed when popping the context but the SAT solver
55
 * keeps using them.
56
 */
57
7993826
bool assertionLevelOnly()
58
{
59
15071066
  return (options::produceProofs() || options::unsatCores())
60
10882324
         && options::incrementalSolving();
61
}
62
63
//=================================================================================================
64
// Helper functions for decision tree tracing
65
66
// Writes to Trace macro for decision tree tracing
67
static inline void dtviewDecisionHelper(size_t level,
68
                                        const Node& node,
69
                                        const char* decisiontype)
70
{
71
  Trace("dtview") << std::string(level - (options::incrementalSolving() ? 1 : 0), '*')
72
                  << " " << node << " :" << decisiontype << "-DECISION:" << std::endl;
73
}
74
75
// Writes to Trace macro for propagation tracing
76
static inline void dtviewPropagationHeaderHelper(size_t level)
77
{
78
  Trace("dtview::prop") << std::string(level + 1 - (options::incrementalSolving() ? 1 : 0),
79
                                       '*')
80
                        << " /Propagations/" << std::endl;
81
}
82
83
// Writes to Trace macro for propagation tracing
84
static inline void dtviewBoolPropagationHelper(size_t level,
85
                                               Lit& l,
86
                                               CVC4::prop::TheoryProxy* proxy)
87
{
88
  Trace("dtview::prop") << std::string(
89
      level + 1 - (options::incrementalSolving() ? 1 : 0), ' ')
90
                        << ":BOOL-PROP: "
91
                        << proxy->getNode(MinisatSatSolver::toSatLiteral(l))
92
                        << std::endl;
93
}
94
95
// Writes to Trace macro for conflict tracing
96
static inline void dtviewPropConflictHelper(size_t level,
97
                                            Clause& confl,
98
                                            CVC4::prop::TheoryProxy* proxy)
99
{
100
  Trace("dtview::conflict")
101
      << std::string(level + 1 - (options::incrementalSolving() ? 1 : 0), ' ')
102
      << ":PROP-CONFLICT: (or";
103
  for (int i = 0; i < confl.size(); i++)
104
  {
105
    Trace("dtview::conflict")
106
        << " " << proxy->getNode(MinisatSatSolver::toSatLiteral(confl[i]));
107
  }
108
  Trace("dtview::conflict") << ")" << std::endl;
109
}
110
111
}  // namespace
112
113
//=================================================================================================
114
// Options:
115
116
static const char* _cat = "CORE";
117
118
8892
static DoubleOption  opt_var_decay         (_cat, "var-decay",   "The variable activity decay factor",            0.95,     DoubleRange(0, false, 1, false));
119
8892
static DoubleOption  opt_clause_decay      (_cat, "cla-decay",   "The clause activity decay factor",              0.999,    DoubleRange(0, false, 1, false));
120
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));
121
8892
static DoubleOption  opt_random_seed       (_cat, "rnd-seed",    "Used by the random variable selection",         91648253, DoubleRange(0, false, HUGE_VAL, false));
122
8892
static IntOption     opt_ccmin_mode        (_cat, "ccmin-mode",  "Controls conflict clause minimization (0=none, 1=basic, 2=deep)", 2, IntRange(0, 2));
123
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));
124
8892
static BoolOption    opt_rnd_init_act      (_cat, "rnd-init",    "Randomize the initial activity", false);
125
8892
static BoolOption    opt_luby_restart      (_cat, "luby",        "Use the Luby restart sequence", true);
126
8892
static IntOption     opt_restart_first     (_cat, "rfirst",      "The base restart interval", 25, IntRange(1, INT32_MAX));
127
8892
static DoubleOption  opt_restart_inc       (_cat, "rinc",        "Restart interval increase factor", 3, DoubleRange(1, false, HUGE_VAL, false));
128
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));
129
130
//=================================================================================================
131
// Proof declarations
132
CRef Solver::TCRef_Undef = CRef_Undef;
133
CRef Solver::TCRef_Lazy = CRef_Lazy;
134
135
class ScopedBool
136
{
137
  bool& d_watch;
138
  bool d_oldValue;
139
140
 public:
141
3072500
  ScopedBool(bool& watch, bool newValue) : d_watch(watch), d_oldValue(watch)
142
  {
143
3072500
    watch = newValue;
144
3072500
  }
145
3072500
  ~ScopedBool() { d_watch = d_oldValue; }
146
};
147
148
//=================================================================================================
149
// Constructor/Destructor:
150
151
9027
Solver::Solver(CVC4::prop::TheoryProxy* proxy,
152
               CVC4::context::Context* context,
153
               CVC4::context::UserContext* userContext,
154
               ProofNodeManager* pnm,
155
9027
               bool enableIncremental)
156
    : d_proxy(proxy),
157
      d_context(context),
158
      assertionLevel(0),
159
      d_pfManager(nullptr),
160
      d_enable_incremental(enableIncremental),
161
      minisat_busy(false)
162
      // Parameters (user settable):
163
      //
164
      ,
165
      verbosity(0),
166
      var_decay(opt_var_decay),
167
      clause_decay(opt_clause_decay),
168
      random_var_freq(opt_random_var_freq),
169
      random_seed(opt_random_seed),
170
      luby_restart(opt_luby_restart),
171
      ccmin_mode(opt_ccmin_mode),
172
      phase_saving(opt_phase_saving),
173
      rnd_pol(false),
174
      rnd_init_act(opt_rnd_init_act),
175
      garbage_frac(opt_garbage_frac),
176
      restart_first(opt_restart_first),
177
      restart_inc(opt_restart_inc)
178
179
      // Parameters (the rest):
180
      //
181
      ,
182
      learntsize_factor(1),
183
      learntsize_inc(1.5)
184
185
      // Parameters (experimental):
186
      //
187
      ,
188
      learntsize_adjust_start_confl(100),
189
      learntsize_adjust_inc(1.5)
190
191
      // Statistics: (formerly in 'SolverStats')
192
      //
193
      ,
194
      solves(0),
195
      starts(0),
196
      decisions(0),
197
      rnd_decisions(0),
198
      propagations(0),
199
      conflicts(0),
200
      resources_consumed(0),
201
      dec_vars(0),
202
      clauses_literals(0),
203
      learnts_literals(0),
204
      max_literals(0),
205
      tot_literals(0)
206
207
      ,
208
      ok(true),
209
      cla_inc(1),
210
      var_inc(1),
211
18054
      watches(WatcherDeleted(ca)),
212
      qhead(0),
213
      simpDB_assigns(-1),
214
      simpDB_props(0),
215
18054
      order_heap(VarOrderLt(activity)),
216
      progress_estimate(0),
217
9027
      remove_satisfied(!enableIncremental)
218
219
      // Resource constraints:
220
      //
221
      ,
222
      conflict_budget(-1),
223
      propagation_budget(-1),
224
54162
      asynch_interrupt(false)
225
{
226
9027
  if (pnm)
227
  {
228
1932
    d_pfManager.reset(
229
966
        new SatProofManager(this, proxy->getCnfStream(), userContext, pnm));
230
  }
231
8061
  else if (options::unsatCores())
232
  {
233
1826
    ProofManager::currentPM()->initSatProof(this);
234
  }
235
236
  // Create the constant variables
237
9027
  varTrue = newVar(true, false, false);
238
9027
  varFalse = newVar(false, false, false);
239
240
  // Assert the constants
241
9027
  uncheckedEnqueue(mkLit(varTrue, false));
242
9027
  uncheckedEnqueue(mkLit(varFalse, true));
243
  // FIXME: these should be axioms I believe
244
9027
  if (options::unsatCores() && !isProofEnabled())
245
  {
246
1826
    ProofManager::getSatProof()->registerTrueLit(mkLit(varTrue, false));
247
1826
    ProofManager::getSatProof()->registerFalseLit(mkLit(varFalse, true));
248
  }
249
9027
}
250
251
252
9024
Solver::~Solver()
253
{
254
9024
}
255
256
257
//=================================================================================================
258
// Minor methods:
259
260
261
// Creates a new SAT variable in the solver. If 'decision_var' is cleared, variable will not be
262
// used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result).
263
//
264
808428
Var Solver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool preRegister, bool canErase)
265
{
266
808428
    int v = nVars();
267
268
808428
    watches  .init(mkLit(v, false));
269
808428
    watches  .init(mkLit(v, true ));
270
808428
    assigns  .push(l_Undef);
271
808428
    vardata  .push(VarData(CRef_Undef, -1, -1, assertionLevel, -1));
272
808428
    activity .push(rnd_init_act ? drand(random_seed) * 0.00001 : 0);
273
808428
    seen     .push(0);
274
808428
    polarity .push(sign);
275
808428
    decision .push();
276
808428
    trail    .capacity(v+1);
277
    // push whether it corresponds to a theory atom
278
808428
    theory.push(isTheoryAtom);
279
280
808428
    setDecisionVar(v, dvar);
281
282
808428
    Debug("minisat") << "new var " << v << std::endl;
283
284
    // If the variable is introduced at non-zero level, we need to reintroduce it on backtracks
285
808428
    if (preRegister)
286
    {
287
1038712
      Debug("minisat") << "  To register at level " << decisionLevel()
288
519356
                       << std::endl;
289
519356
      variables_to_register.push(VarIntroInfo(v, decisionLevel()));
290
    }
291
292
808428
    return v;
293
}
294
295
3190
void Solver::resizeVars(int newSize) {
296
3190
  Assert(d_enable_incremental);
297
3190
  Assert(decisionLevel() == 0);
298
3190
  Assert(newSize >= 2) << "always keep true/false";
299
3190
  if (newSize < nVars()) {
300
1893
    int shrinkSize = nVars() - newSize;
301
302
    // Resize watches up to the negated last literal
303
1893
    watches.resizeTo(mkLit(newSize-1, true));
304
305
    // Resize all info arrays
306
1893
    assigns.shrink(shrinkSize);
307
1893
    vardata.shrink(shrinkSize);
308
1893
    activity.shrink(shrinkSize);
309
1893
    seen.shrink(shrinkSize);
310
1893
    polarity.shrink(shrinkSize);
311
1893
    decision.shrink(shrinkSize);
312
1893
    theory.shrink(shrinkSize);
313
  }
314
315
3190
  if (Debug.isOn("minisat::pop")) {
316
    for (int i = 0; i < trail.size(); ++ i) {
317
      Assert(var(trail[i]) < nVars());
318
    }
319
  }
320
3190
}
321
322
52269692
CRef Solver::reason(Var x) {
323
52269692
  Trace("pf::sat") << "Solver::reason(" << x << ")" << std::endl;
324
325
  // If we already have a reason, just return it
326
52269692
  if (vardata[x].d_reason != CRef_Lazy)
327
  {
328
52213637
    if (Trace.isOn("pf::sat"))
329
    {
330
      Trace("pf::sat") << "  Solver::reason: " << vardata[x].d_reason << ", ";
331
      if (vardata[x].d_reason == CRef_Undef)
332
      {
333
        Trace("pf::sat") << "CRef_Undef";
334
      }
335
      else
336
      {
337
        for (unsigned i = 0, size = ca[vardata[x].d_reason].size(); i < size;
338
             ++i)
339
        {
340
          Trace("pf::sat") << ca[vardata[x].d_reason][i] << " ";
341
        }
342
      }
343
      Trace("pf::sat") << "\n";
344
    }
345
52213637
    return vardata[x].d_reason;
346
  }
347
348
  // What's the literal we are trying to explain
349
56055
  Lit l = mkLit(x, value(x) != l_True);
350
351
  // Get the explanation from the theory
352
112110
  SatClause explanation_cl;
353
  // FIXME: at some point return a tag with the theory that spawned you
354
56055
  d_proxy->explainPropagation(MinisatSatSolver::toSatLiteral(l),
355
                              explanation_cl);
356
112110
  vec<Lit> explanation;
357
56055
  MinisatSatSolver::toMinisatClause(explanation_cl, explanation);
358
359
112110
  Trace("pf::sat") << "Solver::reason: explanation_cl = " << explanation_cl
360
56055
                   << std::endl;
361
362
  // Sort the literals by trail index level
363
56055
  lemma_lt lt(*this);
364
56055
  sort(explanation, lt);
365
56055
  Assert(explanation[0] == l);
366
367
  // Compute the assertion level for this clause
368
56055
  int explLevel = 0;
369
56055
  if (assertionLevelOnly())
370
  {
371
814
    explLevel = assertionLevel;
372
    }
373
    else
374
    {
375
      int i, j;
376
55241
      Lit prev = lit_Undef;
377
399843
      for (i = 0, j = 0; i < explanation.size(); ++i)
378
      {
379
        // This clause is valid theory propagation, so its level is the level of
380
        // the top literal
381
344602
        explLevel = std::max(explLevel, intro_level(var(explanation[i])));
382
383
344602
        Assert(value(explanation[i]) != l_Undef);
384
344602
        Assert(i == 0
385
               || trail_index(var(explanation[0]))
386
                      > trail_index(var(explanation[i])));
387
388
        // Always keep the first literal
389
399843
        if (i == 0)
390
        {
391
55241
          prev = explanation[j++] = explanation[i];
392
55241
          continue;
393
        }
394
        // Ignore duplicate literals
395
289361
        if (explanation[i] == prev)
396
        {
397
          continue;
398
        }
399
        // Ignore zero level literals
400
578722
        if (level(var(explanation[i])) == 0
401
289361
            && user_level(var(explanation[i]) == 0))
402
        {
403
          continue;
404
        }
405
        // Keep this literal
406
289361
        prev = explanation[j++] = explanation[i];
407
      }
408
55241
      explanation.shrink(i - j);
409
410
55241
      Trace("pf::sat") << "Solver::reason: explanation = ";
411
399843
      for (int k = 0; k < explanation.size(); ++k)
412
      {
413
344602
        Trace("pf::sat") << explanation[k] << " ";
414
      }
415
55241
      Trace("pf::sat") << std::endl;
416
417
      // We need an explanation clause so we add a fake literal
418
55241
      if (j == 1)
419
      {
420
        // Add not TRUE to the clause
421
        explanation.push(mkLit(varTrue, true));
422
      }
423
    }
424
425
    // Construct the reason
426
56055
    CRef real_reason = ca.alloc(explLevel, explanation, true);
427
    // FIXME: at some point will need more information about where this explanation
428
    // came from (ie. the theory/sharing)
429
112110
    Trace("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (1)"
430
56055
                     << std::endl;
431
56055
    if (options::unsatCores() && !isProofEnabled())
432
    {
433
17044
      ClauseId id = ProofManager::getSatProof()->registerClause(real_reason,
434
17044
                                                                THEORY_LEMMA);
435
      // map id to assertion, which may be required if looking for
436
      // lemmas in unsat core
437
17044
      ProofManager::getCnfProof()->registerConvertedClause(id);
438
      // explainPropagation() pushes the explanation on the assertion stack
439
      // in CnfProof, so we need to pop it here. This is important because
440
      // reason() may be called indirectly while adding a clause, which can
441
      // lead to a wrong assertion being associated with the clause being
442
      // added (see issue #2137).
443
17044
      ProofManager::getCnfProof()->popCurrentAssertion();
444
    }
445
56055
    vardata[x] = VarData(real_reason, level(x), user_level(x), intro_level(x), trail_index(x));
446
56055
    clauses_removable.push(real_reason);
447
56055
    attachClause(real_reason);
448
449
56055
    return real_reason;
450
}
451
452
2175119
bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
453
{
454
2175119
    if (!ok) return false;
455
456
    // Check if clause is satisfied and remove false/duplicate literals:
457
2175119
    sort(ps);
458
    Lit p; int i, j;
459
460
    // Which user-level to assert this clause at
461
2175119
    int clauseLevel = (removable && !assertionLevelOnly()) ? 0 : assertionLevel;
462
463
    // Check the clause for tautologies and similar
464
2175119
    int falseLiteralsCount = 0;
465
9216413
    for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
466
      // Update the level
467
14550692
      clauseLevel = assertionLevelOnly()
468
14348196
                        ? assertionLevel
469
14348196
                        : std::max(clauseLevel, intro_level(var(ps[i])));
470
      // Tautologies are ignored
471
7275346
      if (ps[i] == ~p) {
472
62322
        id = ClauseIdUndef;
473
        // Clause can be ignored
474
62322
        return true;
475
      }
476
      // Clauses with 0-level true literals are also ignored
477
7213024
      if (value(ps[i]) == l_True && level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0) {
478
171730
        id = ClauseIdUndef;
479
171730
        return true;
480
      }
481
      // Ignore repeated literals
482
7041294
      if (ps[i] == p) {
483
3038
        continue;
484
      }
485
      // If a literal is false at 0 level (both sat and user level) we also
486
      // ignore it, unless we are tracking the SAT solver's reasoning
487
7038256
      if (value(ps[i]) == l_False) {
488
7849778
        if (!options::unsatCores() && !isProofEnabled()
489
4590346
            && level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0)
490
        {
491
743123
          continue;
492
        }
493
        else
494
        {
495
          // If we decide to keep it, we count it into the false literals
496
2145449
          falseLiteralsCount++;
497
        }
498
      }
499
      // This literal is a keeper
500
6295133
      ps[j++] = p = ps[i];
501
    }
502
503
    // Fit to size
504
1941067
    ps.shrink(i - j);
505
506
    // If we are in solve_ or propagate
507
1941067
    if (minisat_busy)
508
    {
509
760784
      Trace("pf::sat") << "Add clause adding a new lemma: ";
510
3906360
      for (int k = 0; k < ps.size(); ++k) {
511
3145576
        Trace("pf::sat") << ps[k] << " ";
512
      }
513
760784
      Trace("pf::sat") << std::endl;
514
515
760784
      lemmas.push();
516
760784
      ps.copyTo(lemmas.last());
517
760784
      lemmas_removable.push(removable);
518
760784
      if (options::unsatCores() && !isProofEnabled())
519
      {
520
        // Store the expression being converted to CNF until
521
        // the clause is actually created
522
402998
        lemmas_cnf_assertion.push_back(
523
402998
            ProofManager::getCnfProof()->getCurrentAssertion());
524
201499
        id = ClauseIdUndef;
525
      }
526
    } else {
527
1180283
      Assert(decisionLevel() == 0);
528
529
      // If all false, we're in conflict
530
1180283
      if (ps.size() == falseLiteralsCount) {
531
1537
        if (options::unsatCores() || isProofEnabled())
532
        {
533
          // Take care of false units here; otherwise, we need to
534
          // construct the clause below to give to the proof manager
535
          // as the final conflict.
536
675
          if(falseLiteralsCount == 1) {
537
625
            if (options::unsatCores() && !isProofEnabled())
538
            {
539
              ClauseKind ck =
540
317
                  ProofManager::getCnfProof()->getCurrentAssertionKind()
541
317
                      ? INPUT
542
317
                      : THEORY_LEMMA;
543
317
              id = ProofManager::getSatProof()->storeUnitConflict(ps[0], ck);
544
              // map id to assertion, which may be required if looking for
545
              // lemmas in unsat core
546
317
              if (ck == THEORY_LEMMA)
547
              {
548
                ProofManager::getCnfProof()->registerConvertedClause(id);
549
              }
550
317
              ProofManager::getSatProof()->finalizeProof(
551
                  CVC4::Minisat::CRef_Lazy);
552
            }
553
625
            if (isProofEnabled())
554
            {
555
308
              d_pfManager->finalizeProof(ps[0], true);
556
            }
557
123434
            return ok = false;
558
          }
559
        }
560
        else
561
        {
562
862
          return ok = false;
563
        }
564
      }
565
566
1178796
      CRef cr = CRef_Undef;
567
568
      // If not unit, add the clause
569
1178796
      if (ps.size() > 1) {
570
571
1062833
        lemma_lt lt(*this);
572
1062833
        sort(ps, lt);
573
574
1062833
        cr = ca.alloc(clauseLevel, ps, false);
575
1062833
        clauses_persistent.push(cr);
576
1062833
        attachClause(cr);
577
578
1062833
        if (options::unsatCores() || isProofEnabled())
579
        {
580
306110
          if (options::unsatCores() && !isProofEnabled())
581
          {
582
            ClauseKind ck =
583
206570
                ProofManager::getCnfProof()->getCurrentAssertionKind()
584
206570
                    ? INPUT
585
206570
                    : THEORY_LEMMA;
586
206570
            id = ProofManager::getSatProof()->registerClause(cr, ck);
587
            // map id to assertion, which may be required if looking for
588
            // lemmas in unsat core
589
206570
            if (ck == THEORY_LEMMA)
590
            {
591
16787
              ProofManager::getCnfProof()->registerConvertedClause(id);
592
            }
593
          }
594
306110
          if (ps.size() == falseLiteralsCount)
595
          {
596
50
            if (options::unsatCores() && !isProofEnabled())
597
            {
598
34
              ProofManager::getSatProof()->finalizeProof(cr);
599
            }
600
50
            if (isProofEnabled())
601
            {
602
16
              d_pfManager->finalizeProof(ca[cr], true);
603
            }
604
50
            return ok = false;
605
          }
606
        }
607
      }
608
609
      // Check if it propagates
610
1178746
      if (ps.size() == falseLiteralsCount + 1) {
611
121272
        if(assigns[var(ps[0])] == l_Undef) {
612
119800
          Assert(assigns[var(ps[0])] != l_False);
613
119800
          uncheckedEnqueue(ps[0], cr);
614
239600
          Debug("cores") << "i'm registering a unit clause, maybe input"
615
119800
                         << std::endl;
616
119800
          if (ps.size() == 1)
617
          {
618
115320
            if (options::unsatCores() && !isProofEnabled())
619
            {
620
              ClauseKind ck =
621
43125
                  ProofManager::getCnfProof()->getCurrentAssertionKind()
622
43125
                      ? INPUT
623
43125
                      : THEORY_LEMMA;
624
43125
              id = ProofManager::getSatProof()->registerUnitClause(ps[0], ck);
625
              // map id to assertion, which may be required if looking for
626
              // lemmas in unsat core
627
43125
              if (ck == THEORY_LEMMA)
628
              {
629
1956
                ProofManager::getCnfProof()->registerConvertedClause(id);
630
              }
631
            }
632
            // We need to do this so that the closedness check, if being done,
633
            // goes through when we have unit assumptions whose literal has
634
            // already been registered, as the ProofCnfStream will not register
635
            // them and as they are not the result of propagation will be left
636
            // hanging in assumptions accumulator
637
115320
            if (isProofEnabled())
638
            {
639
20908
              d_pfManager->registerSatLitAssumption(ps[0]);
640
            }
641
          }
642
119800
          CRef confl = propagate(CHECK_WITHOUT_THEORY);
643
119800
          if(! (ok = (confl == CRef_Undef)) ) {
644
40
            if (options::unsatCores() && !isProofEnabled())
645
            {
646
2
              if (ca[confl].size() == 1)
647
              {
648
                id = ProofManager::getSatProof()->storeUnitConflict(
649
                    ca[confl][0], LEARNT);
650
                ProofManager::getSatProof()->finalizeProof(
651
                    CVC4::Minisat::CRef_Lazy);
652
              }
653
              else
654
              {
655
2
                ProofManager::getSatProof()->finalizeProof(confl);
656
              }
657
            }
658
40
            if (isProofEnabled())
659
            {
660
13
              if (ca[confl].size() == 1)
661
              {
662
                d_pfManager->finalizeProof(ca[confl][0]);
663
              }
664
              else
665
              {
666
13
                d_pfManager->finalizeProof(ca[confl]);
667
              }
668
            }
669
          }
670
119800
          return ok;
671
        } else {
672
1472
          if (options::unsatCores() && !isProofEnabled())
673
          {
674
            id = ClauseIdUndef;
675
          }
676
1472
          return ok;
677
        }
678
      }
679
    }
680
681
1818258
    return true;
682
}
683
684
685
2162672
void Solver::attachClause(CRef cr) {
686
2162672
    const Clause& c = ca[cr];
687
2162672
    if (Debug.isOn("minisat"))
688
    {
689
      Debug("minisat") << "Solver::attachClause(" << c << "): ";
690
      for (unsigned i = 0, size = c.size(); i < size; ++i)
691
      {
692
        Debug("minisat") << c[i] << " ";
693
      }
694
      Debug("minisat") << ", level " << c.level() << "\n";
695
    }
696
2162672
    Assert(c.size() > 1);
697
2162672
    watches[~c[0]].push(Watcher(cr, c[1]));
698
2162672
    watches[~c[1]].push(Watcher(cr, c[0]));
699
2162672
    if (c.removable()) learnts_literals += c.size();
700
1651406
    else            clauses_literals += c.size();
701
2162672
}
702
703
704
809228
void Solver::detachClause(CRef cr, bool strict) {
705
809228
    const Clause& c = ca[cr];
706
809228
    Debug("minisat") << "Solver::detachClause(" << c << ")" << std::endl;
707
809228
    if (Debug.isOn("minisat"))
708
    {
709
      Debug("minisat") << "Solver::detachClause(" << c << "), CRef " << cr
710
                       << ", clause ";
711
      for (unsigned i = 0, size = c.size(); i < size; ++i)
712
      {
713
        Debug("minisat") << c[i] << " ";
714
      }
715
716
      Debug("minisat") << "\n";
717
    }
718
809228
    Assert(c.size() > 1);
719
809228
    if (options::unsatCores() && !isProofEnabled())
720
    {
721
79185
      ProofManager::getSatProof()->markDeleted(cr);
722
    }
723
724
809228
    if (strict){
725
89209
        remove(watches[~c[0]], Watcher(cr, c[1]));
726
89209
        remove(watches[~c[1]], Watcher(cr, c[0]));
727
    }else{
728
        // Lazy detaching: (NOTE! Must clean all watcher lists before garbage collecting this clause)
729
720019
        watches.smudge(~c[0]);
730
720019
        watches.smudge(~c[1]);
731
    }
732
733
809228
    if (c.removable()) learnts_literals -= c.size();
734
512691
    else            clauses_literals -= c.size(); }
735
736
737
720019
void Solver::removeClause(CRef cr) {
738
720019
    Clause& c = ca[cr];
739
720019
    if (Debug.isOn("minisat"))
740
    {
741
      Debug("minisat") << "Solver::removeClause(" << c << "), CRef " << cr
742
                       << ", clause ";
743
      for (unsigned i = 0, size = c.size(); i < size; ++i)
744
      {
745
        Debug("minisat") << c[i] << " ";
746
      }
747
      Debug("minisat") << "\n";
748
    }
749
720019
    detachClause(cr);
750
    // Don't leave pointers to free'd memory!
751
720019
    if (locked(c))
752
    {
753
      // a locked clause c is one whose first literal c[0] is true and is
754
      // propagated by c itself, i.e. vardata[var(c[0])].d_reason == c. Because
755
      // of this if we need to justify the propagation of c[0], via
756
      // Solver::reason, if it appears in a resolution chain built lazily we
757
      // will be unable to do so after the step below. Thus we eagerly justify
758
      // this propagation here.
759
12532
      if (isProofEnabled())
760
      {
761
1868
        Trace("pf::sat")
762
934
            << "Solver::removeClause: eagerly compute propagation of " << c[0]
763
934
            << "\n";
764
934
        d_pfManager->startResChain(c);
765
3449
        for (unsigned i = 1, size = c.size(); i < size; ++i)
766
        {
767
2515
          d_pfManager->addResolutionStep(c[i]);
768
        }
769
934
        d_pfManager->endResChain(c[0]);
770
      }
771
12532
      vardata[var(c[0])].d_reason = CRef_Undef;
772
    }
773
720019
    c.mark(1);
774
720019
    ca.free(cr);
775
720019
}
776
777
778
585159
bool Solver::satisfied(const Clause& c) const {
779
9489357
    for (int i = 0; i < c.size(); i++)
780
8973468
        if (value(c[i]) == l_True)
781
69270
            return true;
782
515889
    return false; }
783
784
785
// Revert to the state at given level (keeping all assignment at 'level' but not beyond).
786
//
787
534525
void Solver::cancelUntil(int level) {
788
534525
    Debug("minisat") << "minisat::cancelUntil(" << level << ")" << std::endl;
789
790
534525
    if (decisionLevel() > level){
791
        // Pop the SMT context
792
2907762
        for (int l = trail_lim.size() - level; l > 0; --l) {
793
2492684
          d_context->pop();
794
        }
795
51744968
        for (int c = trail.size()-1; c >= trail_lim[level]; c--){
796
51329890
            Var      x  = var(trail[c]);
797
51329890
            assigns [x] = l_Undef;
798
51329890
            vardata[x].d_trail_index = -1;
799
102659780
            if ((phase_saving > 1 ||
800
                 ((phase_saving == 1) && c > trail_lim.last())
801
102659780
                 ) && ((polarity[x] & 0x2) == 0)) {
802
50680668
              polarity[x] = sign(trail[c]);
803
            }
804
51329890
            insertVarOrder(x);
805
        }
806
415078
        qhead = trail_lim[level];
807
415078
        trail.shrink(trail.size() - trail_lim[level]);
808
415078
        trail_lim.shrink(trail_lim.size() - level);
809
415078
        flipped.shrink(flipped.size() - level);
810
811
        // Register variables that have not been registered yet
812
415078
        int currentLevel = decisionLevel();
813
716802
        for (int i = variables_to_register.size() - 1;
814
716802
             i >= 0 && variables_to_register[i].d_level > currentLevel;
815
             --i)
816
        {
817
301724
          variables_to_register[i].d_level = currentLevel;
818
603448
          d_proxy->variableNotify(
819
301724
              MinisatSatSolver::toSatVariable(variables_to_register[i].d_var));
820
        }
821
    }
822
534525
}
823
824
12399
void Solver::resetTrail() { cancelUntil(0); }
825
826
//=================================================================================================
827
// Major methods:
828
829
830
2556589
Lit Solver::pickBranchLit()
831
{
832
    Lit nextLit;
833
834
    // Theory requests
835
2556585
    nextLit =
836
2556589
        MinisatSatSolver::toMinisatLit(d_proxy->getNextTheoryDecisionRequest());
837
2574019
    while (nextLit != lit_Undef) {
838
54405
      if(value(var(nextLit)) == l_Undef) {
839
91376
        Debug("theoryDecision")
840
45688
            << "getNextTheoryDecisionRequest(): now deciding on " << nextLit
841
45688
            << std::endl;
842
45688
        decisions++;
843
844
        // org-mode tracing -- theory decision
845
45688
        if (Trace.isOn("dtview"))
846
        {
847
          dtviewDecisionHelper(
848
              d_context->getLevel(),
849
              d_proxy->getNode(MinisatSatSolver::toSatLiteral(nextLit)),
850
              "THEORY");
851
        }
852
853
45688
        if (Trace.isOn("dtview::prop"))
854
        {
855
          dtviewPropagationHeaderHelper(d_context->getLevel());
856
        }
857
858
45688
        return nextLit;
859
      } else {
860
17434
        Debug("theoryDecision")
861
8717
            << "getNextTheoryDecisionRequest(): would decide on " << nextLit
862
8717
            << " but it already has an assignment" << std::endl;
863
      }
864
8717
      nextLit = MinisatSatSolver::toMinisatLit(
865
8717
          d_proxy->getNextTheoryDecisionRequest());
866
    }
867
5021794
    Debug("theoryDecision")
868
2510897
        << "getNextTheoryDecisionRequest(): decide on another literal"
869
2510897
        << std::endl;
870
871
    // DE requests
872
2510897
    bool stopSearch = false;
873
2510897
    nextLit = MinisatSatSolver::toMinisatLit(
874
2510897
        d_proxy->getNextDecisionEngineRequest(stopSearch));
875
2510897
    if(stopSearch) {
876
39155
      return lit_Undef;
877
    }
878
2471742
    if(nextLit != lit_Undef) {
879
588455
      Assert(value(var(nextLit)) == l_Undef)
880
          << "literal to decide already has value";
881
588455
      decisions++;
882
588455
      Var next = var(nextLit);
883
588455
      if(polarity[next] & 0x2) {
884
159996
        nextLit = mkLit(next, polarity[next] & 0x1);
885
      }
886
887
      // org-mode tracing -- decision engine decision
888
588455
      if (Trace.isOn("dtview"))
889
      {
890
        dtviewDecisionHelper(
891
            d_context->getLevel(),
892
            d_proxy->getNode(MinisatSatSolver::toSatLiteral(nextLit)),
893
            "DE");
894
      }
895
896
588455
      if (Trace.isOn("dtview::prop"))
897
      {
898
        dtviewPropagationHeaderHelper(d_context->getLevel());
899
      }
900
901
588455
      return nextLit;
902
    }
903
904
1883287
    Var next = var_Undef;
905
906
    // Random decision:
907
1883287
    if (drand(random_seed) < random_var_freq && !order_heap.empty()){
908
        next = order_heap[irand(random_seed,order_heap.size())];
909
        if (value(next) == l_Undef && decision[next])
910
            rnd_decisions++; }
911
912
    // Activity based decision:
913
13597495
    while (next >= nVars() || next == var_Undef || value(next) != l_Undef || !decision[next]) {
914
5881731
        if (order_heap.empty()){
915
24627
            next = var_Undef;
916
24627
            break;
917
        }else {
918
5857104
            next = order_heap.removeMin();
919
        }
920
921
5857104
        if(!decision[next]) continue;
922
        // Check with decision engine about relevancy
923
11688906
        if (d_proxy->isDecisionRelevant(MinisatSatSolver::toSatVariable(next))
924
5844453
            == false)
925
        {
926
          next = var_Undef;
927
        }
928
    }
929
930
1883287
    if(next == var_Undef) {
931
24627
      return lit_Undef;
932
    } else {
933
1858660
      decisions++;
934
      // Check with decision engine if it can tell polarity
935
      lbool dec_pol = MinisatSatSolver::toMinisatlbool(
936
1858660
          d_proxy->getDecisionPolarity(MinisatSatSolver::toSatVariable(next)));
937
      Lit decisionLit;
938
1858660
      if(dec_pol != l_Undef) {
939
        Assert(dec_pol == l_True || dec_pol == l_False);
940
        decisionLit = mkLit(next, (dec_pol == l_True));
941
      }
942
      else
943
      {
944
        // If it can't use internal heuristic to do that
945
1858660
        decisionLit = mkLit(
946
1858660
            next, rnd_pol ? drand(random_seed) < 0.5 : (polarity[next] & 0x1));
947
      }
948
949
      // org-mode tracing -- decision engine decision
950
1858660
      if (Trace.isOn("dtview"))
951
      {
952
        dtviewDecisionHelper(
953
            d_context->getLevel(),
954
            d_proxy->getNode(MinisatSatSolver::toSatLiteral(decisionLit)),
955
            "DE");
956
      }
957
958
1858660
      if (Trace.isOn("dtview::prop"))
959
      {
960
        dtviewPropagationHeaderHelper(d_context->getLevel());
961
      }
962
963
1858660
      return decisionLit;
964
    }
965
}
966
967
968
/*_________________________________________________________________________________________________
969
|
970
|  analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&)  ->  [void]
971
|
972
|  Description:
973
|    Analyze conflict and produce a reason clause.
974
|
975
|    Pre-conditions:
976
|      * 'out_learnt' is assumed to be cleared.
977
|      * Current decision level must be greater than root level.
978
|
979
|    Post-conditions:
980
|      * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'.
981
|      * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the
982
|        rest of literals. There may be others from the same level though.
983
|      * returns the maximal level of the resolved clauses
984
|
985
|________________________________________________________________________________________________@*/
986
260110
int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
987
{
988
520220
  Trace("pf::sat") << "Solver::analyze: starting with " << confl
989
260110
                   << " with decision level " << decisionLevel() << "\n";
990
991
260110
  int pathC = 0;
992
260110
  Lit p = lit_Undef;
993
994
  // Generate conflict clause:
995
  //
996
260110
  out_learnt.push();  // (leave room for the asserting literal)
997
260110
  int index = trail.size() - 1;
998
999
260110
  int max_resolution_level = 0;  // Maximal level of the resolved clauses
1000
1001
260110
  if (options::unsatCores() && !isProofEnabled())
1002
  {
1003
67857
    ProofManager::getSatProof()->startResChain(confl);
1004
    }
1005
260110
    if (isProofEnabled())
1006
    {
1007
13869
      d_pfManager->startResChain(ca[confl]);
1008
    }
1009
6883394
    do{
1010
7143504
      Assert(confl != CRef_Undef);  // (otherwise should be UIP)
1011
1012
      {
1013
        // ! IMPORTANT !
1014
        // It is not safe to use c after this block of code because
1015
        // resolveOutUnit() below may lead to clauses being allocated, which
1016
        // in turn may lead to reallocations that invalidate c.
1017
7143504
        Clause& c = ca[confl];
1018
7143504
        max_resolution_level = std::max(max_resolution_level, c.level());
1019
1020
7143504
        if (c.removable()) claBumpActivity(c);
1021
      }
1022
1023
7143504
        if (Trace.isOn("pf::sat"))
1024
        {
1025
          Trace("pf::sat") << "Solver::analyze: conflict clause ";
1026
          for (unsigned i = 0, size = ca[confl].size(); i < size; ++i)
1027
          {
1028
            Trace("pf::sat") << ca[confl][i] << " ";
1029
          }
1030
          Trace("pf::sat") << "\n";
1031
        }
1032
1033
7143504
        Trace("pf::sat") << CVC4::push;
1034
30504639
        for (int j = (p == lit_Undef) ? 0 : 1, size = ca[confl].size();
1035
30504639
             j < size;
1036
             j++)
1037
        {
1038
23361135
          Lit q = ca[confl][j];
1039
1040
46722270
          Trace("pf::sat") << "Lit " << q
1041
46722270
                           << " seen/level: " << (seen[var(q)] ? 1 : 0) << " / "
1042
23361135
                           << level(var(q)) << "\n";
1043
23361135
          if (!seen[var(q)] && level(var(q)) > 0)
1044
          {
1045
14251469
            varBumpActivity(var(q));
1046
14251469
            seen[var(q)] = 1;
1047
14251469
            if (level(var(q)) >= decisionLevel())
1048
7143504
              pathC++;
1049
            else
1050
7107965
              out_learnt.push(q);
1051
          }
1052
          else
1053
          {
1054
            // We could be resolving a literal propagated by a clause/theory
1055
            // using information from a higher level
1056
9109666
            if (!seen[var(q)] && level(var(q)) == 0)
1057
            {
1058
747009
              max_resolution_level =
1059
1494018
                  std::max(max_resolution_level, user_level(var(q)));
1060
            }
1061
1062
            // FIXME: can we do it lazily if we actually need the proof?
1063
9109666
            if (level(var(q)) == 0)
1064
            {
1065
747009
              if (options::unsatCores() && !isProofEnabled())
1066
              {
1067
365352
                ProofManager::getSatProof()->resolveOutUnit(q);
1068
              }
1069
747009
              if (isProofEnabled())
1070
              {
1071
133942
                d_pfManager->addResolutionStep(q);
1072
              }
1073
            }
1074
          }
1075
        }
1076
7143504
        Trace("pf::sat") << CVC4::pop;
1077
1078
        // Select next clause to look at:
1079
37455069
        while (!seen[var(trail[index--])]);
1080
7143504
        p     = trail[index+1];
1081
7143504
        confl = reason(var(p));
1082
7143504
        seen[var(p)] = 0;
1083
7143504
        pathC--;
1084
1085
7143504
        if (pathC > 0 && confl != CRef_Undef)
1086
        {
1087
6883394
          if (options::unsatCores() && !isProofEnabled())
1088
          {
1089
1822420
            ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p));
1090
          }
1091
6883394
          if (isProofEnabled())
1092
          {
1093
119942
            d_pfManager->addResolutionStep(ca[confl], p);
1094
          }
1095
        }
1096
1097
7143504
    }while (pathC > 0);
1098
260110
    out_learnt[0] = ~p;
1099
260110
    if (Debug.isOn("newproof::sat"))
1100
    {
1101
      Debug("newproof::sat") << "finished with learnt clause ";
1102
      for (unsigned i = 0, size = out_learnt.size(); i < size; ++i)
1103
      {
1104
        prop::SatLiteral satLit = toSatLiteral<Minisat::Solver>(out_learnt[i]);
1105
        Debug("newproof::sat") << satLit << " ";
1106
      }
1107
      Debug("newproof::sat") << "\n";
1108
    }
1109
1110
    // Simplify conflict clause:
1111
    int i, j;
1112
260110
    out_learnt.copyTo(analyze_toclear);
1113
260110
    if (ccmin_mode == 2){
1114
260110
        uint32_t abstract_level = 0;
1115
7368075
        for (i = 1; i < out_learnt.size(); i++)
1116
7107965
            abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involved in conflict)
1117
1118
7368075
        for (i = j = 1; i < out_learnt.size(); i++) {
1119
7107965
            if (reason(var(out_learnt[i])) == CRef_Undef) {
1120
1555802
                out_learnt[j++] = out_learnt[i];
1121
            } else {
1122
              // Check if the literal is redundant
1123
5552163
              if (!litRedundant(out_learnt[i], abstract_level)) {
1124
                // Literal is not redundant
1125
3170907
                out_learnt[j++] = out_learnt[i];
1126
              } else {
1127
2381256
                if (options::unsatCores() && !isProofEnabled())
1128
                {
1129
529680
                  ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]);
1130
                }
1131
2381256
                if (isProofEnabled())
1132
                {
1133
59484
                  Debug("newproof::sat")
1134
29742
                      << "Solver::analyze: redundant lit "
1135
29742
                      << toSatLiteral<Minisat::Solver>(out_learnt[i]) << "\n";
1136
29742
                  d_pfManager->addResolutionStep(out_learnt[i], true);
1137
                }
1138
                // Literal is redundant, to be safe, mark the level as current assertion level
1139
                // TODO: maybe optimize
1140
2381256
                max_resolution_level = std::max(max_resolution_level, user_level(var(out_learnt[i])));
1141
              }
1142
            }
1143
        }
1144
1145
    }else if (ccmin_mode == 1){
1146
        Unreachable();
1147
        for (i = j = 1; i < out_learnt.size(); i++){
1148
            Var x = var(out_learnt[i]);
1149
1150
            if (reason(x) == CRef_Undef)
1151
                out_learnt[j++] = out_learnt[i];
1152
            else{
1153
                Clause& c = ca[reason(var(out_learnt[i]))];
1154
                for (int k = 1; k < c.size(); k++)
1155
                    if (!seen[var(c[k])] && level(var(c[k])) > 0){
1156
                        out_learnt[j++] = out_learnt[i];
1157
                        break; }
1158
            }
1159
        }
1160
    }else
1161
        i = j = out_learnt.size();
1162
1163
260110
    max_literals += out_learnt.size();
1164
260110
    out_learnt.shrink(i - j);
1165
260110
    tot_literals += out_learnt.size();
1166
1167
    // Find correct backtrack level:
1168
    //
1169
260110
    if (out_learnt.size() == 1)
1170
7108
        out_btlevel = 0;
1171
    else{
1172
253002
        int max_i = 1;
1173
        // Find the first literal assigned at the next-highest level:
1174
4726709
        for (int k = 2; k < out_learnt.size(); k++)
1175
4473707
          if (level(var(out_learnt[k])) > level(var(out_learnt[max_i])))
1176
338473
            max_i = k;
1177
        // Swap-in this literal at index 1:
1178
253002
        Lit p2 = out_learnt[max_i];
1179
253002
        out_learnt[max_i] = out_learnt[1];
1180
253002
        out_learnt[1] = p2;
1181
253002
        out_btlevel = level(var(p2));
1182
    }
1183
1184
10028912
    for (int k = 0; k < analyze_toclear.size(); k++)
1185
9768802
      seen[var(analyze_toclear[k])] = 0;  // ('seen[]' is now cleared)
1186
1187
    // Return the maximal resolution level
1188
260110
    return max_resolution_level;
1189
}
1190
1191
1192
// Check if 'p' can be removed. 'abstract_levels' is used to abort early if the algorithm is
1193
// visiting literals at levels that cannot be removed later.
1194
5552163
bool Solver::litRedundant(Lit p, uint32_t abstract_levels)
1195
{
1196
5552163
    analyze_stack.clear(); analyze_stack.push(p);
1197
5552163
    int top = analyze_toclear.size();
1198
31722725
    while (analyze_stack.size() > 0){
1199
16256188
        CRef c_reason = reason(var(analyze_stack.last()));
1200
16256188
        Assert(c_reason != CRef_Undef);
1201
16256188
        Clause& c = ca[c_reason];
1202
16256188
        int c_size = c.size();
1203
16256188
        analyze_stack.pop();
1204
1205
        // Since calling reason might relocate to resize, c is not necesserily the right reference, we must
1206
        // use the allocator each time
1207
43530979
        for (int i = 1; i < c_size; i++){
1208
30445698
          Lit p2 = ca[c_reason][i];
1209
30445698
          if (!seen[var(p2)] && level(var(p2)) > 0)
1210
          {
1211
35271848
            if (reason(var(p2)) != CRef_Undef
1212
17635924
                && (abstractLevel(var(p2)) & abstract_levels) != 0)
1213
            {
1214
14465017
              seen[var(p2)] = 1;
1215
14465017
              analyze_stack.push(p2);
1216
14465017
              analyze_toclear.push(p2);
1217
            }
1218
            else
1219
            {
1220
15235197
              for (int j = top; j < analyze_toclear.size(); j++)
1221
12064290
                seen[var(analyze_toclear[j])] = 0;
1222
3170907
              analyze_toclear.shrink(analyze_toclear.size() - top);
1223
3170907
              return false;
1224
            }
1225
          }
1226
        }
1227
    }
1228
1229
2381256
    return true;
1230
}
1231
1232
1233
/*_________________________________________________________________________________________________
1234
|
1235
|  analyzeFinal : (p : Lit)  ->  [void]
1236
|
1237
|  Description:
1238
|    Specialized analysis procedure to express the final conflict in terms of assumptions.
1239
|    Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and
1240
|    stores the result in 'out_conflict'.
1241
|________________________________________________________________________________________________@*/
1242
void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
1243
{
1244
    out_conflict.clear();
1245
    out_conflict.push(p);
1246
1247
    if (decisionLevel() == 0)
1248
        return;
1249
1250
    seen[var(p)] = 1;
1251
1252
    for (int i = trail.size()-1; i >= trail_lim[0]; i--){
1253
        Var x = var(trail[i]);
1254
        if (seen[x]){
1255
            if (reason(x) == CRef_Undef){
1256
              Assert(level(x) > 0);
1257
              out_conflict.push(~trail[i]);
1258
            }else{
1259
                Clause& c = ca[reason(x)];
1260
                for (int j = 1; j < c.size(); j++)
1261
                    if (level(var(c[j])) > 0)
1262
                        seen[var(c[j])] = 1;
1263
            }
1264
            seen[x] = 0;
1265
        }
1266
    }
1267
1268
    seen[var(p)] = 0;
1269
}
1270
1271
51729531
void Solver::uncheckedEnqueue(Lit p, CRef from)
1272
{
1273
51729531
  if (Debug.isOn("minisat"))
1274
  {
1275
    Debug("minisat") << "unchecked enqueue of " << p << " ("
1276
                     << trail_index(var(p)) << ") trail size is "
1277
                     << trail.size() << " cap is " << trail.capacity()
1278
                     << ", reason is " << from << ", ";
1279
    if (from == CRef_Lazy)
1280
    {
1281
      Debug("minisat") << "CRef_Lazy";
1282
    }
1283
    else if (from == CRef_Undef)
1284
    {
1285
      Debug("minisat") << "CRef_Undef";
1286
    }
1287
    else
1288
    {
1289
      for (unsigned i = 0, size = ca[from].size(); i < size; ++i)
1290
      {
1291
        Debug("minisat") << ca[from][i] << " ";
1292
      }
1293
    }
1294
    Debug("minisat") << "\n";
1295
  }
1296
51729531
  Assert(value(p) == l_Undef);
1297
51729531
  Assert(var(p) < nVars());
1298
51729531
  assigns[var(p)] = lbool(!sign(p));
1299
51729531
  vardata[var(p)] = VarData(
1300
      from, decisionLevel(), assertionLevel, intro_level(var(p)), trail.size());
1301
51729531
  trail.push_(p);
1302
51729531
  if (theory[var(p)])
1303
  {
1304
    // Enqueue to the theory
1305
15884873
    d_proxy->enqueueTheoryLiteral(MinisatSatSolver::toSatLiteral(p));
1306
  }
1307
51729531
}
1308
1309
3060375
CRef Solver::propagate(TheoryCheckType type)
1310
{
1311
3060375
    CRef confl = CRef_Undef;
1312
3060375
    recheck = false;
1313
3060375
    theoryConflict = false;
1314
1315
6120750
    ScopedBool scoped_bool(minisat_busy, true);
1316
1317
    // Add lemmas that we're left behind
1318
3060375
    if (lemmas.size() > 0) {
1319
59
      confl = updateLemmas();
1320
59
      if (confl != CRef_Undef) {
1321
        return confl;
1322
      }
1323
    }
1324
1325
    // If this is the final check, no need for Boolean propagation and
1326
    // theory propagation
1327
3060375
    if (type == CHECK_FINAL) {
1328
      // Do the theory check
1329
73140
      theoryCheck(CVC4::theory::Theory::EFFORT_FULL);
1330
      // Pick up the theory propagated literals (there could be some,
1331
      // if new lemmas are added)
1332
73126
      propagateTheory();
1333
      // If there are lemmas (or conflicts) update them
1334
73126
      if (lemmas.size() > 0) {
1335
49272
        recheck = true;
1336
49272
        confl = updateLemmas();
1337
49272
        return confl;
1338
      } else {
1339
23854
        recheck = d_proxy->theoryNeedCheck();
1340
23854
        return confl;
1341
      }
1342
    }
1343
1344
    // Keep running until we have checked everything, we
1345
    // have no conflict and no new literals have been asserted
1346
944485
    do {
1347
        // Propagate on the clauses
1348
3931720
        confl = propagateBool();
1349
        // If no conflict, do the theory check
1350
3931720
        if (confl == CRef_Undef && type != CHECK_WITHOUT_THEORY) {
1351
            // Do the theory check
1352
3556927
            if (type == CHECK_FINAL_FAKE) {
1353
              theoryCheck(CVC4::theory::Theory::EFFORT_FULL);
1354
            } else {
1355
3556927
              theoryCheck(CVC4::theory::Theory::EFFORT_STANDARD);
1356
            }
1357
            // Pick up the theory propagated literals
1358
3556924
            propagateTheory();
1359
            // If there are lemmas (or conflicts) update them
1360
7113848
            if (lemmas.size() > 0) {
1361
210303
              confl = updateLemmas();
1362
            }
1363
        } else {
1364
          // if dumping decision tree, print the conflict
1365
374793
          if (Trace.isOn("dtview::conflict"))
1366
          {
1367
            if (confl != CRef_Undef)
1368
            {
1369
              dtviewPropConflictHelper(decisionLevel(), ca[confl], d_proxy);
1370
            }
1371
          }
1372
          // Even though in conflict, we still need to discharge the lemmas
1373
374793
          if (lemmas.size() > 0) {
1374
            // Remember the trail size
1375
            int oldLevel = decisionLevel();
1376
            // Update the lemmas
1377
            CRef lemmaConflict = updateLemmas();
1378
            // If we get a conflict, we prefer it since it's earlier in the trail
1379
            if (lemmaConflict != CRef_Undef) {
1380
              // Lemma conflict takes precedence, since it's earlier in the trail
1381
              confl = lemmaConflict;
1382
            } else {
1383
              // Otherwise, the Boolean conflict is canceled in the case we popped the trail
1384
              if (oldLevel > decisionLevel()) {
1385
                confl = CRef_Undef;
1386
              }
1387
            }
1388
          }
1389
        }
1390
3931717
    } while (confl == CRef_Undef && qhead < trail.size());
1391
2987232
    return confl;
1392
}
1393
1394
3630050
void Solver::propagateTheory() {
1395
7260100
  SatClause propagatedLiteralsClause;
1396
  // Doesn't actually call propagate(); that's done in theoryCheck() now that combination
1397
  // is online.  This just incorporates those propagations previously discovered.
1398
3630050
  d_proxy->theoryPropagate(propagatedLiteralsClause);
1399
1400
7260100
  vec<Lit> propagatedLiterals;
1401
3630050
  MinisatSatSolver::toMinisatClause(propagatedLiteralsClause, propagatedLiterals);
1402
1403
3630050
  int oldTrailSize = trail.size();
1404
3630050
  Debug("minisat") << "old trail size is " << oldTrailSize << ", propagating " << propagatedLiterals.size() << " lits..." << std::endl;
1405
11805430
  for (unsigned i = 0, i_end = propagatedLiterals.size(); i < i_end; ++ i) {
1406
8175380
    Debug("minisat") << "Theory propagated: " << propagatedLiterals[i] << std::endl;
1407
    // multiple theories can propagate the same literal
1408
8175380
    Lit p = propagatedLiterals[i];
1409
8175380
    if (value(p) == l_Undef) {
1410
4378719
      uncheckedEnqueue(p, CRef_Lazy);
1411
    } else {
1412
3796661
      if (value(p) == l_False) {
1413
79083
        Debug("minisat") << "Conflict in theory propagation" << std::endl;
1414
158166
        SatClause explanation_cl;
1415
79083
        d_proxy->explainPropagation(MinisatSatSolver::toSatLiteral(p),
1416
                                    explanation_cl);
1417
158166
        vec<Lit> explanation;
1418
79083
        MinisatSatSolver::toMinisatClause(explanation_cl, explanation);
1419
        ClauseId id; // FIXME: mark it as explanation here somehow?
1420
79083
        addClause(explanation, true, id);
1421
        // explainPropagation() pushes the explanation on the assertion
1422
        // stack in CnfProof, so we need to pop it here.
1423
79083
        if (options::unsatCores() && !isProofEnabled())
1424
        {
1425
22806
          ProofManager::getCnfProof()->popCurrentAssertion();
1426
        }
1427
      }
1428
    }
1429
  }
1430
3630050
}
1431
1432
/*_________________________________________________________________________________________________
1433
|
1434
|  theoryCheck: [void]  ->  [Clause*]
1435
|
1436
|  Description:
1437
|    Checks all enqueued theory facts for satisfiability. If a conflict arises, the conflicting
1438
|    clause is returned, otherwise NULL.
1439
|
1440
|    Note: the propagation queue might be NOT empty
1441
|________________________________________________________________________________________________@*/
1442
3630067
void Solver::theoryCheck(CVC4::theory::Theory::Effort effort)
1443
{
1444
3630067
  d_proxy->theoryCheck(effort);
1445
3630050
}
1446
1447
/*_________________________________________________________________________________________________
1448
|
1449
|  propagateBool : [void]  ->  [Clause*]
1450
|
1451
|  Description:
1452
|    Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned,
1453
|    otherwise CRef_Undef.
1454
|
1455
|    Post-conditions:
1456
|      * the propagation queue is empty, even if there was a conflict.
1457
|________________________________________________________________________________________________@*/
1458
3931720
CRef Solver::propagateBool()
1459
{
1460
3931720
    CRef    confl     = CRef_Undef;
1461
3931720
    int     num_props = 0;
1462
3931720
    watches.cleanAll();
1463
1464
97822942
    while (qhead < trail.size()){
1465
46945611
        Lit            p   = trail[qhead++];     // 'p' is enqueued fact to propagate.
1466
46945611
        vec<Watcher>&  ws  = watches[p];
1467
        Watcher        *i, *j, *end;
1468
46945611
        num_props++;
1469
1470
        // if propagation tracing enabled, print boolean propagation
1471
46945611
        if (Trace.isOn("dtview::prop"))
1472
        {
1473
          dtviewBoolPropagationHelper(decisionLevel(), p, d_proxy);
1474
        }
1475
1476
572170915
        for (i = j = (Watcher*)ws, end = i + ws.size();  i != end;){
1477
            // Try to avoid inspecting the clause:
1478
525225304
            Lit blocker = i->blocker;
1479
845594168
            if (value(blocker) == l_True){
1480
980575602
                *j++ = *i++; continue; }
1481
1482
            // Make sure the false literal is data[1]:
1483
204856440
            CRef     cr        = i->cref;
1484
204856440
            Clause&  c         = ca[cr];
1485
204856440
            Lit      false_lit = ~p;
1486
204856440
            if (c[0] == false_lit)
1487
69811552
                c[0] = c[1], c[1] = false_lit;
1488
204856440
            Assert(c[1] == false_lit);
1489
204856440
            i++;
1490
1491
            // If 0th watch is true, then clause is already satisfied.
1492
204856440
            Lit     first = c[0];
1493
204856440
            Watcher w     = Watcher(cr, first);
1494
224325450
            if (first != blocker && value(first) == l_True){
1495
38938020
                *j++ = w; continue; }
1496
1497
            // Look for new watch:
1498
185387430
            Assert(c.size() >= 2);
1499
625629775
            for (int k = 2; k < c.size(); k++)
1500
581245736
                if (value(c[k]) != l_False){
1501
141003391
                    c[1] = c[k]; c[k] = false_lit;
1502
141003391
                    watches[~c[1]].push(w);
1503
141003391
                    goto NextClause; }
1504
1505
            // Did not find watch -- clause is unit under assignment:
1506
44384039
            *j++ = w;
1507
44384039
            if (value(first) == l_False){
1508
202943
                confl = cr;
1509
202943
                qhead = trail.size();
1510
                // Copy the remaining watches:
1511
5406347
                while (i < end)
1512
2601702
                    *j++ = *i++;
1513
            }else
1514
44181096
                uncheckedEnqueue(first, cr);
1515
1516
185387430
        NextClause:;
1517
        }
1518
46945611
        ws.shrink(i - j);
1519
    }
1520
3931720
    propagations += num_props;
1521
3931720
    simpDB_props -= num_props;
1522
1523
3931720
    return confl;
1524
}
1525
1526
1527
/*_________________________________________________________________________________________________
1528
|
1529
|  reduceDB : ()  ->  [void]
1530
|
1531
|  Description:
1532
|    Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked
1533
|    clauses are clauses that are reason to some assignment. Binary clauses are never removed.
1534
|________________________________________________________________________________________________@*/
1535
struct reduceDB_lt {
1536
    ClauseAllocator& ca;
1537
13256
    reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) {}
1538
30609715
    bool operator () (CRef x, CRef y) {
1539
30609715
        return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); }
1540
};
1541
13256
void Solver::reduceDB()
1542
{
1543
    int     i, j;
1544
13256
    double  extra_lim = cla_inc / clauses_removable.size();    // Remove any clause below this activity
1545
1546
13256
    sort(clauses_removable, reduceDB_lt(ca));
1547
    // Don't delete binary or locked clauses. From the rest, delete clauses from the first half
1548
    // and clauses with activity smaller than 'extra_lim':
1549
3225775
    for (i = j = 0; i < clauses_removable.size(); i++){
1550
3212519
        Clause& c = ca[clauses_removable[i]];
1551
3212519
        if (c.size() > 2 && !locked(c) && (i < clauses_removable.size() / 2 || c.activity() < extra_lim))
1552
219161
            removeClause(clauses_removable[i]);
1553
        else
1554
2993358
            clauses_removable[j++] = clauses_removable[i];
1555
    }
1556
13256
    clauses_removable.shrink(i - j);
1557
13256
    checkGarbage();
1558
13256
}
1559
1560
1561
16973
void Solver::removeSatisfied(vec<CRef>& cs)
1562
{
1563
    int i, j;
1564
602132
    for (i = j = 0; i < cs.size(); i++){
1565
585159
        Clause& c = ca[cs[i]];
1566
585159
        if (satisfied(c)) {
1567
69270
          if (options::unsatCores() && !isProofEnabled() && locked(c))
1568
          {
1569
            // store a resolution of the literal c propagated
1570
2260
            ProofManager::getSatProof()->storeUnitResolution(c[0]);
1571
          }
1572
69270
          removeClause(cs[i]);
1573
        }
1574
        else
1575
        {
1576
515889
          cs[j++] = cs[i];
1577
        }
1578
    }
1579
16973
    cs.shrink(i - j);
1580
16973
}
1581
1582
6380
void Solver::removeClausesAboveLevel(vec<CRef>& cs, int level)
1583
{
1584
    int i, j;
1585
601237
    for (i = j = 0; i < cs.size(); i++){
1586
594857
        Clause& c = ca[cs[i]];
1587
594857
        if (c.level() > level) {
1588
177700
          Assert(!locked(c));
1589
177700
          removeClause(cs[i]);
1590
        } else {
1591
417157
            cs[j++] = cs[i];
1592
        }
1593
    }
1594
6380
    cs.shrink(i - j);
1595
6380
}
1596
1597
16973
void Solver::rebuildOrderHeap()
1598
{
1599
33946
    vec<Var> vs;
1600
2207078
    for (Var v = 0; v < nVars(); v++)
1601
2190105
        if (decision[v] && value(v) == l_Undef)
1602
1410419
            vs.push(v);
1603
16973
    order_heap.build(vs);
1604
16973
}
1605
1606
1607
/*_________________________________________________________________________________________________
1608
|
1609
|  simplify : [void]  ->  [bool]
1610
|
1611
|  Description:
1612
|    Simplify the clause database according to the current top-level assigment. Currently, the only
1613
|    thing done here is the removal of satisfied clauses, but more things can be put here.
1614
|________________________________________________________________________________________________@*/
1615
43226
bool Solver::simplify()
1616
{
1617
43226
  Assert(decisionLevel() == 0);
1618
1619
43226
  if (!ok || propagate(CHECK_WITHOUT_THEORY) != CRef_Undef) return ok = false;
1620
1621
42946
  if (nAssigns() == simpDB_assigns || (simpDB_props > 0)) return true;
1622
1623
  // Remove satisfied clauses:
1624
16973
  removeSatisfied(clauses_removable);
1625
16973
  if (remove_satisfied)  // Can be turned off.
1626
    removeSatisfied(clauses_persistent);
1627
16973
  checkGarbage();
1628
16973
  rebuildOrderHeap();
1629
1630
16973
  simpDB_assigns = nAssigns();
1631
16973
  simpDB_props =
1632
16973
      clauses_literals + learnts_literals;  // (shouldn't depend on stats
1633
                                            // really, but it will do for now)
1634
1635
16973
  return true;
1636
}
1637
1638
1639
/*_________________________________________________________________________________________________
1640
|
1641
|  search : (nof_conflicts : int) (params : const SearchParams&)  ->  [lbool]
1642
|
1643
|  Description:
1644
|    Search for a model the specified number of conflicts.
1645
|    NOTE! Use negative value for 'nof_conflicts' indicate infinity.
1646
|
1647
|  Output:
1648
|    'l_True' if a partial assigment that is consistent with respect to the clauseset is found. If
1649
|    all variables are decision variables, this means that the clause set is satisfiable. 'l_False'
1650
|    if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached.
1651
|________________________________________________________________________________________________@*/
1652
12920
lbool Solver::search(int nof_conflicts)
1653
{
1654
12920
  Assert(ok);
1655
  int backtrack_level;
1656
12920
  int conflictC = 0;
1657
25840
  vec<Lit> learnt_clause;
1658
12920
  starts++;
1659
1660
12920
  TheoryCheckType check_type = CHECK_WITH_THEORY;
1661
  for (;;)
1662
  {
1663
    // Propagate and call the theory solvers
1664
2888473
    CRef confl = propagate(check_type);
1665
2888456
    Assert(lemmas.size() == 0);
1666
1667
2888456
    if (confl != CRef_Undef)
1668
    {
1669
264746
      conflicts++;
1670
264746
      conflictC++;
1671
1672
264746
      if (decisionLevel() == 0)
1673
      {
1674
4636
        if (options::unsatCores() && !isProofEnabled())
1675
        {
1676
1415
          ProofManager::getSatProof()->finalizeProof(confl);
1677
        }
1678
4636
        if (isProofEnabled())
1679
        {
1680
736
          if (confl == CRef_Lazy)
1681
          {
1682
44
            d_pfManager->finalizeProof();
1683
          }
1684
          else
1685
          {
1686
692
            d_pfManager->finalizeProof(ca[confl]);
1687
          }
1688
        }
1689
4636
        return l_False;
1690
      }
1691
1692
      // Analyze the conflict
1693
260110
      learnt_clause.clear();
1694
260110
      int max_level = analyze(confl, learnt_clause, backtrack_level);
1695
260110
      cancelUntil(backtrack_level);
1696
1697
      // Assert the conflict clause and the asserting literal
1698
260110
      if (learnt_clause.size() == 1)
1699
      {
1700
7108
        uncheckedEnqueue(learnt_clause[0]);
1701
7108
        if (options::unsatCores() && !isProofEnabled())
1702
        {
1703
2243
          ProofManager::getSatProof()->endResChain(learnt_clause[0]);
1704
        }
1705
7108
        if (isProofEnabled())
1706
        {
1707
1191
          d_pfManager->endResChain(learnt_clause[0]);
1708
        }
1709
      }
1710
      else
1711
      {
1712
253002
        CRef cr = ca.alloc(assertionLevelOnly() ? assertionLevel : max_level,
1713
                           learnt_clause,
1714
253002
                           true);
1715
253002
        clauses_removable.push(cr);
1716
253002
        attachClause(cr);
1717
253002
        claBumpActivity(ca[cr]);
1718
253002
        uncheckedEnqueue(learnt_clause[0], cr);
1719
253002
        if (options::unsatCores() && !isProofEnabled())
1720
        {
1721
65614
          ClauseId id = ProofManager::getSatProof()->registerClause(cr, LEARNT);
1722
65614
          ProofManager::getSatProof()->endResChain(id);
1723
        }
1724
253002
        if (isProofEnabled())
1725
        {
1726
12678
          d_pfManager->endResChain(ca[cr]);
1727
        }
1728
      }
1729
1730
260110
      varDecayActivity();
1731
260110
      claDecayActivity();
1732
1733
260110
      if (--learntsize_adjust_cnt == 0)
1734
      {
1735
500
        learntsize_adjust_confl *= learntsize_adjust_inc;
1736
500
        learntsize_adjust_cnt = (int)learntsize_adjust_confl;
1737
500
        max_learnts *= learntsize_inc;
1738
1739
500
        if (verbosity >= 1)
1740
          printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n",
1741
                 (int)conflicts,
1742
                 (int)dec_vars
1743
                     - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]),
1744
                 nClauses(),
1745
                 (int)clauses_literals,
1746
                 (int)max_learnts,
1747
                 nLearnts(),
1748
                 (double)learnts_literals / nLearnts(),
1749
                 progressEstimate() * 100);
1750
      }
1751
1752
318134
      if (theoryConflict && options::sat_refine_conflicts())
1753
      {
1754
        check_type = CHECK_FINAL_FAKE;
1755
      }
1756
      else
1757
      {
1758
260110
        check_type = CHECK_WITH_THEORY;
1759
      }
1760
    }
1761
    else
1762
    {
1763
      // If this was a final check, we are satisfiable
1764
2623710
      if (check_type == CHECK_FINAL)
1765
      {
1766
64809
        bool decisionEngineDone = d_proxy->isDecisionEngineDone();
1767
        // Unless a lemma has added more stuff to the queues
1768
179118
        if (!decisionEngineDone
1769
64809
            && (!order_heap.empty() || qhead < trail.size()))
1770
        {
1771
49500
          check_type = CHECK_WITH_THEORY;
1772
172140
          continue;
1773
        }
1774
15309
        else if (recheck)
1775
        {
1776
          // There some additional stuff added, so we go for another
1777
          // full-check
1778
9358
          continue;
1779
        }
1780
        else
1781
        {
1782
          // Yes, we're truly satisfiable
1783
5951
          return l_True;
1784
        }
1785
      }
1786
2558901
      else if (check_type == CHECK_FINAL_FAKE)
1787
      {
1788
        check_type = CHECK_WITH_THEORY;
1789
      }
1790
1791
5117802
      if ((nof_conflicts >= 0 && conflictC >= nof_conflicts)
1792
5115490
          || !withinBudget(ResourceManager::Resource::SatConflictStep))
1793
      {
1794
        // Reached bound on number of conflicts:
1795
2312
        progress_estimate = progressEstimate();
1796
2312
        cancelUntil(0);
1797
        // [mdeters] notify theory engine of restarts for deferred
1798
        // theory processing
1799
2312
        d_proxy->notifyRestart();
1800
2312
        return l_Undef;
1801
      }
1802
1803
      // Simplify the set of problem clauses:
1804
2556589
      if (decisionLevel() == 0 && !simplify())
1805
      {
1806
        return l_False;
1807
      }
1808
1809
2556589
      if (clauses_removable.size() - nAssigns() >= max_learnts)
1810
      {
1811
        // Reduce the set of learnt clauses:
1812
13256
        reduceDB();
1813
      }
1814
1815
2556589
      Lit next = lit_Undef;
1816
2556589
      while (decisionLevel() < assumptions.size())
1817
      {
1818
        // Perform user provided assumption:
1819
        Lit p = assumptions[decisionLevel()];
1820
        if (value(p) == l_True)
1821
        {
1822
          // Dummy decision level:
1823
          newDecisionLevel();
1824
        }
1825
        else if (value(p) == l_False)
1826
        {
1827
          analyzeFinal(~p, d_conflict);
1828
          return l_False;
1829
        }
1830
        else
1831
        {
1832
          next = p;
1833
          break;
1834
        }
1835
      }
1836
1837
2556589
      if (next == lit_Undef)
1838
      {
1839
        // New variable decision:
1840
2556589
        next = pickBranchLit();
1841
1842
2620367
        if (next == lit_Undef)
1843
        {
1844
          // We need to do a full theory check to confirm
1845
127564
          Debug("minisat::search")
1846
63782
              << "Doing a full theory check..." << std::endl;
1847
63782
          check_type = CHECK_FINAL;
1848
63782
          continue;
1849
        }
1850
      }
1851
1852
      // Increase decision level and enqueue 'next'
1853
2492803
      newDecisionLevel();
1854
2492803
      uncheckedEnqueue(next);
1855
    }
1856
2875553
  }
1857
}
1858
1859
1860
2312
double Solver::progressEstimate() const
1861
{
1862
2312
    double  progress = 0;
1863
2312
    double  F = 1.0 / nVars();
1864
1865
35373
    for (int i = 0; i <= decisionLevel(); i++){
1866
33061
        int beg = i == 0 ? 0 : trail_lim[i - 1];
1867
33061
        int end = i == decisionLevel() ? trail.size() : trail_lim[i];
1868
33061
        progress += pow(F, i) * (end - beg);
1869
    }
1870
1871
2312
    return progress / nVars();
1872
}
1873
1874
/*
1875
  Finite subsequences of the Luby-sequence:
1876
1877
  0: 1
1878
  1: 1 1 2
1879
  2: 1 1 2 1 1 2 4
1880
  3: 1 1 2 1 1 2 4 1 1 2 1 1 2 4 8
1881
  ...
1882
1883
1884
 */
1885
1886
12920
static double luby(double y, int x){
1887
1888
    // Find the finite subsequence that contains index 'x', and the
1889
    // size of that subsequence:
1890
    int size, seq;
1891
12920
    for (size = 1, seq = 0; size < x+1; seq++, size = 2*size+1);
1892
1893
22818
    while (size-1 != x){
1894
4949
        size = (size-1)>>1;
1895
4949
        seq--;
1896
4949
        x = x % size;
1897
    }
1898
1899
12920
    return pow(y, seq);
1900
}
1901
1902
// NOTE: assumptions passed in member-variable 'assumptions'.
1903
12125
lbool Solver::solve_()
1904
{
1905
12125
    Debug("minisat") << "nvars = " << nVars() << std::endl;
1906
1907
24250
    ScopedBool scoped_bool(minisat_busy, true);
1908
1909
12125
    Assert(decisionLevel() == 0);
1910
1911
12125
    model.clear();
1912
12125
    d_conflict.clear();
1913
12125
    if (!ok){
1914
1517
      minisat_busy = false;
1915
1517
      return l_False;
1916
    }
1917
1918
10608
    solves++;
1919
1920
10608
    max_learnts               = nClauses() * learntsize_factor;
1921
10608
    learntsize_adjust_confl   = learntsize_adjust_start_confl;
1922
10608
    learntsize_adjust_cnt     = (int)learntsize_adjust_confl;
1923
10608
    lbool   status            = l_Undef;
1924
1925
10608
    if (verbosity >= 1){
1926
1
        printf("============================[ Search Statistics ]==============================\n");
1927
1
        printf("| Conflicts |          ORIGINAL         |          LEARNT          | Progress |\n");
1928
1
        printf("|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |\n");
1929
1
        printf("===============================================================================\n");
1930
    }
1931
1932
    // Search:
1933
10608
    int curr_restarts = 0;
1934
36406
    while (status == l_Undef){
1935
12920
        double rest_base = luby_restart ? luby(restart_inc, curr_restarts) : pow(restart_inc, curr_restarts);
1936
12920
        status = search(rest_base * restart_first);
1937
12899
        if (!withinBudget(ResourceManager::Resource::SatConflictStep))
1938
          break;  // FIXME add restart option?
1939
12899
        curr_restarts++;
1940
    }
1941
1942
10587
    if (!withinBudget(ResourceManager::Resource::SatConflictStep))
1943
      status = l_Undef;
1944
1945
10587
    if (verbosity >= 1)
1946
1
        printf("===============================================================================\n");
1947
1948
1949
10587
    if (status == l_True){
1950
        // Extend & copy model:
1951
5951
        model.growTo(nVars());
1952
522449
        for (int i = 0; i < nVars(); i++) {
1953
516498
          model[i] = value(i);
1954
516498
          Debug("minisat") << i << " = " << model[i] << std::endl;
1955
        }
1956
    }
1957
4636
    else if (status == l_False && d_conflict.size() == 0)
1958
4636
      ok = false;
1959
1960
10587
    return status;
1961
}
1962
1963
//=================================================================================================
1964
// Writing CNF to DIMACS:
1965
//
1966
// FIXME: this needs to be rewritten completely.
1967
1968
static Var mapVar(Var x, vec<Var>& map, Var& max)
1969
{
1970
    if (map.size() <= x || map[x] == -1){
1971
        map.growTo(x+1, -1);
1972
        map[x] = max++;
1973
    }
1974
    return map[x];
1975
}
1976
1977
1978
void Solver::toDimacs(FILE* f, Clause& c, vec<Var>& map, Var& max)
1979
{
1980
    if (satisfied(c)) return;
1981
1982
    for (int i = 0; i < c.size(); i++)
1983
        if (value(c[i]) != l_False)
1984
            fprintf(f, "%s%d ", sign(c[i]) ? "-" : "", mapVar(var(c[i]), map, max)+1);
1985
    fprintf(f, "0\n");
1986
}
1987
1988
1989
void Solver::toDimacs(const char *file, const vec<Lit>& assumps)
1990
{
1991
    FILE* f = fopen(file, "wr");
1992
    if (f == NULL)
1993
        fprintf(stderr, "could not open file %s\n", file), exit(1);
1994
    toDimacs(f, assumps);
1995
    fclose(f);
1996
}
1997
1998
1999
void Solver::toDimacs(FILE* f, const vec<Lit>& assumps)
2000
{
2001
    // Handle case when solver is in contradictory state:
2002
    if (!ok){
2003
        fprintf(f, "p cnf 1 2\n1 0\n-1 0\n");
2004
        return; }
2005
2006
    vec<Var> map; Var max = 0;
2007
2008
    // Cannot use removeClauses here because it is not safe
2009
    // to deallocate them at this point. Could be improved.
2010
    int cnt = 0;
2011
    for (int i = 0; i < clauses_persistent.size(); i++)
2012
        if (!satisfied(ca[clauses_persistent[i]]))
2013
            cnt++;
2014
2015
    for (int i = 0; i < clauses_persistent.size(); i++)
2016
        if (!satisfied(ca[clauses_persistent[i]])){
2017
            Clause& c = ca[clauses_persistent[i]];
2018
            for (int j = 0; j < c.size(); j++)
2019
                if (value(c[j]) != l_False)
2020
                    mapVar(var(c[j]), map, max);
2021
        }
2022
2023
    // Assumptions are added as unit clauses:
2024
    cnt += assumptions.size();
2025
2026
    fprintf(f, "p cnf %d %d\n", max, cnt);
2027
2028
    for (int i = 0; i < assumptions.size(); i++){
2029
      Assert(value(assumptions[i]) != l_False);
2030
      fprintf(f,
2031
              "%s%d 0\n",
2032
              sign(assumptions[i]) ? "-" : "",
2033
              mapVar(var(assumptions[i]), map, max) + 1);
2034
    }
2035
2036
    for (int i = 0; i < clauses_persistent.size(); i++)
2037
        toDimacs(f, ca[clauses_persistent[i]], map, max);
2038
2039
    if (verbosity > 0)
2040
        printf("Wrote %d clauses with %d variables.\n", cnt, max);
2041
}
2042
2043
2044
//=================================================================================================
2045
// Garbage Collection methods:
2046
2047
3102
void Solver::relocAll(ClauseAllocator& to)
2048
{
2049
    // All watchers:
2050
    //
2051
    // for (int i = 0; i < watches.size(); i++)
2052
3102
    watches.cleanAll();
2053
741149
    for (int v = 0; v < nVars(); v++)
2054
2214141
        for (int s = 0; s < 2; s++){
2055
1476094
            Lit p = mkLit(v, s);
2056
            // printf(" >>> RELOCING: %s%d\n", sign(p)?"-":"", var(p)+1);
2057
1476094
            vec<Watcher>& ws = watches[p];
2058
3722614
            for (int j = 0; j < ws.size(); j++)
2059
            {
2060
4865294
              ca.reloc(ws[j].cref,
2061
                       to,
2062
2618774
                       (options::unsatCores() && !isProofEnabled())
2063
                           ? ProofManager::getSatProof()
2064
                           : nullptr);
2065
            }
2066
        }
2067
2068
    // All reasons:
2069
    //
2070
227720
    for (int i = 0; i < trail.size(); i++){
2071
224618
        Var v = var(trail[i]);
2072
2073
449236
        if (hasReasonClause(v)
2074
224618
            && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
2075
        {
2076
104555
          ca.reloc(vardata[v].d_reason,
2077
                   to,
2078
58466
                   (options::unsatCores() && !isProofEnabled())
2079
                       ? ProofManager::getSatProof()
2080
                       : nullptr);
2081
        }
2082
    }
2083
    // All learnt:
2084
    //
2085
224841
    for (int i = 0; i < clauses_removable.size(); i++)
2086
    {
2087
508388
      ca.reloc(clauses_removable[i],
2088
               to,
2089
286649
               (options::unsatCores() && !isProofEnabled())
2090
                   ? ProofManager::getSatProof()
2091
                   : nullptr);
2092
    }
2093
    // All original:
2094
    //
2095
904623
    for (int i = 0; i < clauses_persistent.size(); i++)
2096
    {
2097
1924259
      ca.reloc(clauses_persistent[i],
2098
               to,
2099
1022738
               (options::unsatCores() && !isProofEnabled())
2100
                   ? ProofManager::getSatProof()
2101
                   : nullptr);
2102
    }
2103
3102
    if (options::unsatCores() && !isProofEnabled())
2104
    {
2105
822
      ProofManager::getSatProof()->finishUpdateCRef();
2106
    }
2107
3102
}
2108
2109
2110
void Solver::garbageCollect()
2111
{
2112
    // Initialize the next region to a size corresponding to the estimated utilization degree. This
2113
    // is not precise but should avoid some unnecessary reallocations for the new region:
2114
    ClauseAllocator to(ca.size() - ca.wasted());
2115
2116
    relocAll(to);
2117
    if (verbosity >= 2)
2118
        printf("|  Garbage collection:   %12d bytes => %12d bytes             |\n",
2119
               ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
2120
    to.moveTo(ca);
2121
}
2122
2123
3190
void Solver::push()
2124
{
2125
3190
  Assert(d_enable_incremental);
2126
3190
  Assert(decisionLevel() == 0);
2127
2128
3190
  ++assertionLevel;
2129
3190
  Debug("minisat") << "in user push, increasing assertion level to " << assertionLevel << std::endl;
2130
3190
  trail_ok.push(ok);
2131
3190
  assigns_lim.push(assigns.size());
2132
2133
3190
  d_context->push();  // SAT context for CVC4
2134
2135
3190
  Debug("minisat") << "MINISAT PUSH assertionLevel is " << assertionLevel << ", trail.size is " << trail.size() << std::endl;
2136
3190
}
2137
2138
3190
void Solver::pop()
2139
{
2140
3190
  Assert(d_enable_incremental);
2141
2142
3190
  Assert(decisionLevel() == 0);
2143
2144
  // Pop the trail below the user level
2145
3190
  --assertionLevel;
2146
6380
  Debug("minisat") << "in user pop, decreasing assertion level to "
2147
3190
                   << assertionLevel << "\n"
2148
3190
                   << CVC4::push;
2149
  while (true) {
2150
57718
    Debug("minisat") << "== unassigning " << trail.last() << std::endl;
2151
57718
    Var      x  = var(trail.last());
2152
57718
    if (user_level(x) > assertionLevel) {
2153
54528
      assigns[x] = l_Undef;
2154
54528
      vardata[x] = VarData(CRef_Undef, -1, -1, intro_level(x), -1);
2155
54528
      if(phase_saving >= 1 && (polarity[x] & 0x2) == 0)
2156
53127
        polarity[x] = sign(trail.last());
2157
54528
      insertVarOrder(x);
2158
54528
      trail.pop();
2159
    } else {
2160
3190
      break;
2161
    }
2162
54528
  }
2163
2164
  // The head should be at the trail top
2165
3190
  qhead = trail.size();
2166
2167
  // Remove the clauses
2168
3190
  removeClausesAboveLevel(clauses_persistent, assertionLevel);
2169
3190
  removeClausesAboveLevel(clauses_removable, assertionLevel);
2170
3190
  Debug("minisat") << CVC4::pop;
2171
  // Pop the SAT context to notify everyone
2172
3190
  d_context->pop();  // SAT context for CVC4
2173
2174
6380
  Debug("minisat") << "MINISAT POP assertionLevel is " << assertionLevel
2175
3190
                   << ", trail.size is " << trail.size() << "\n";
2176
  // Pop the created variables
2177
3190
  resizeVars(assigns_lim.last());
2178
3190
  assigns_lim.pop();
2179
3190
  variables_to_register.clear();
2180
2181
  // Pop the OK
2182
3190
  ok = trail_ok.last();
2183
3190
  trail_ok.pop();
2184
3190
}
2185
2186
259634
CRef Solver::updateLemmas() {
2187
2188
259634
  Debug("minisat::lemmas") << "Solver::updateLemmas() begin" << std::endl;
2189
2190
  // Avoid adding lemmas indefinitely without resource-out
2191
259634
  d_proxy->spendResource(ResourceManager::Resource::LemmaStep);
2192
2193
259634
  CRef conflict = CRef_Undef;
2194
2195
  // Decision level to backtrack to
2196
259634
  int backtrackLevel = decisionLevel();
2197
2198
  // We use this comparison operator
2199
259634
  lemma_lt lt(*this);
2200
2201
  // Check for propagation and level to backtrack to
2202
259634
  int i = 0;
2203
779042
  while (i < lemmas.size()) {
2204
    // We need this loop as when we backtrack, due to registration more lemmas could be added
2205
1781210
    for (; i < lemmas.size(); ++ i)
2206
    {
2207
      // The current lemma
2208
760753
      vec<Lit>& lemma = lemmas[i];
2209
2210
760753
      Trace("pf::sat") << "Solver::updateLemmas: working on lemma: ";
2211
3906278
      for (int k = 0; k < lemma.size(); ++k) {
2212
3145525
        Trace("pf::sat") << lemma[k] << " ";
2213
      }
2214
760753
      Trace("pf::sat") << std::endl;
2215
2216
      // If it's an empty lemma, we have a conflict at zero level
2217
762303
      if (lemma.size() == 0) {
2218
1550
        Assert(!options::unsatCores() && !isProofEnabled());
2219
1550
        conflict = CRef_Lazy;
2220
1550
        backtrackLevel = 0;
2221
1550
        Debug("minisat::lemmas") << "Solver::updateLemmas(): found empty clause" << std::endl;
2222
1550
        continue;
2223
      }
2224
      // Sort the lemma to be able to attach
2225
759203
      sort(lemma, lt);
2226
      // See if the lemma propagates something
2227
759203
      if (lemma.size() == 1 || value(lemma[1]) == l_False) {
2228
421983
        Debug("minisat::lemmas") << "found unit " << lemma.size() << std::endl;
2229
        // This lemma propagates, see which level we need to backtrack to
2230
421983
        int currentBacktrackLevel = lemma.size() == 1 ? 0 : level(var(lemma[1]));
2231
        // Even if the first literal is true, we should propagate it at this level (unless it's set at a lower level)
2232
421983
        if (value(lemma[0]) != l_True || level(var(lemma[0])) > currentBacktrackLevel) {
2233
411250
          if (currentBacktrackLevel < backtrackLevel) {
2234
154191
            backtrackLevel = currentBacktrackLevel;
2235
          }
2236
        }
2237
      }
2238
    }
2239
2240
    // Pop so that propagation would be current
2241
259704
    Debug("minisat::lemmas") << "Solver::updateLemmas(): backtracking to " << backtrackLevel << " from " << decisionLevel() << std::endl;
2242
259704
    cancelUntil(backtrackLevel);
2243
  }
2244
2245
  // Last index in the trail
2246
259634
  int backtrack_index = trail.size();
2247
2248
259634
  Assert(!options::unsatCores() || isProofEnabled()
2249
         || lemmas.size() == (int)lemmas_cnf_assertion.size());
2250
2251
  // Attach all the clauses and enqueue all the propagations
2252
1020387
  for (int j = 0; j < lemmas.size(); ++j)
2253
  {
2254
    // The current lemma
2255
760753
    vec<Lit>& lemma = lemmas[j];
2256
760753
    bool removable = lemmas_removable[j];
2257
2258
    // Attach it if non-unit
2259
760753
    CRef lemma_ref = CRef_Undef;
2260
760753
    if (lemma.size() > 1) {
2261
      // If the lemmas is removable, we can compute its level by the level
2262
701573
      int clauseLevel = assertionLevel;
2263
701573
      if (removable && !assertionLevelOnly())
2264
      {
2265
199321
        clauseLevel = 0;
2266
1866024
        for (int k = 0; k < lemma.size(); ++k)
2267
        {
2268
1666703
          clauseLevel = std::max(clauseLevel, intro_level(var(lemma[k])));
2269
        }
2270
      }
2271
2272
701573
      lemma_ref = ca.alloc(clauseLevel, lemma, removable);
2273
701573
      if (options::unsatCores() && !isProofEnabled())
2274
      {
2275
387546
        TNode cnf_assertion = lemmas_cnf_assertion[j];
2276
2277
387546
        Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (2)"
2278
193773
                         << std::endl;
2279
193773
        ClauseId id = ProofManager::getSatProof()->registerClause(lemma_ref,
2280
193773
                                                                  THEORY_LEMMA);
2281
193773
        ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
2282
      }
2283
701573
      if (removable) {
2284
202209
        clauses_removable.push(lemma_ref);
2285
      } else {
2286
499364
        clauses_persistent.push(lemma_ref);
2287
      }
2288
701573
      attachClause(lemma_ref);
2289
    }
2290
2291
    // If the lemma is propagating enqueue its literal (or set the conflict)
2292
760753
    if (conflict == CRef_Undef && value(lemma[0]) != l_True) {
2293
701029
      if (lemma.size() == 1 || (value(lemma[1]) == l_False && trail_index(var(lemma[1])) < backtrack_index)) {
2294
338803
        if (options::unsatCores() && !isProofEnabled() && lemma.size() == 1)
2295
        {
2296
15436
          Node cnf_assertion = lemmas_cnf_assertion[j];
2297
2298
15436
          Trace("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (3) "
2299
7718
                           << cnf_assertion << value(lemma[0]) << std::endl;
2300
7718
          ClauseId id = ProofManager::getSatProof()->registerUnitClause(
2301
7718
              lemma[0], THEORY_LEMMA);
2302
7718
          ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
2303
        }
2304
677606
        Trace("pf::sat") << "Solver::updateLemmas: unit theory lemma: "
2305
338803
                         << lemma[0] << std::endl;
2306
338803
        if (value(lemma[0]) == l_False) {
2307
          // We have a conflict
2308
60411
          if (lemma.size() > 1) {
2309
60124
            Debug("minisat::lemmas") << "Solver::updateLemmas(): conflict" << std::endl;
2310
60124
            conflict = lemma_ref;
2311
          } else {
2312
287
            Debug("minisat::lemmas") << "Solver::updateLemmas(): unit conflict or empty clause" << std::endl;
2313
287
            conflict = CRef_Lazy;
2314
287
            if (options::unsatCores() && !isProofEnabled())
2315
            {
2316
74
              ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT);
2317
            }
2318
287
            if (isProofEnabled())
2319
            {
2320
44
              d_pfManager->storeUnitConflict(lemma[0]);
2321
            }
2322
          }
2323
        } else {
2324
278392
          Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl;
2325
278392
          Debug("minisat::lemmas") << "lemma ref is " << lemma_ref << std::endl;
2326
278392
          uncheckedEnqueue(lemma[0], lemma_ref);
2327
        }
2328
      }
2329
    }
2330
  }
2331
2332
259634
  Assert(!options::unsatCores() || isProofEnabled()
2333
         || lemmas.size() == (int)lemmas_cnf_assertion.size());
2334
  // Clear the lemmas
2335
259634
  lemmas.clear();
2336
259634
  lemmas_cnf_assertion.clear();
2337
259634
  lemmas_removable.clear();
2338
2339
259634
  if (conflict != CRef_Undef) {
2340
61855
    theoryConflict = true;
2341
  }
2342
2343
259634
  Debug("minisat::lemmas") << "Solver::updateLemmas() end" << std::endl;
2344
2345
259634
  return conflict;
2346
}
2347
2348
4089597
void ClauseAllocator::reloc(CRef& cr,
2349
                            ClauseAllocator& to,
2350
                            CVC4::TSatProof<Solver>* proof)
2351
{
2352
4089597
  Debug("minisat") << "ClauseAllocator::reloc: cr " << cr << std::endl;
2353
  // FIXME what is this CRef_lazy
2354
4089597
  if (cr == CRef_Lazy) return;
2355
2356
4089597
  CRef old = cr;  // save the old reference
2357
4089597
  Clause& c = operator[](cr);
2358
4089597
  if (c.reloced()) { cr = c.relocation(); return; }
2359
2360
1124195
  cr = to.alloc(c.level(), c, c.removable());
2361
1124195
  c.relocate(cr);
2362
1124195
  if (proof)
2363
  {
2364
186127
    proof->updateCRef(old, cr);
2365
  }
2366
  // Copy extra data-fields:
2367
  // (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?)
2368
1124195
  to[cr].mark(c.mark());
2369
1124195
  if (to[cr].removable())         to[cr].activity() = c.activity();
2370
902456
  else if (to[cr].has_extra()) to[cr].calcAbstraction();
2371
}
2372
2373
2580075
inline bool Solver::withinBudget(ResourceManager::Resource r) const
2374
{
2375
2580075
  Assert(d_proxy);
2376
  // spendResource sets async_interrupt or throws UnsafeInterruptException
2377
  // depending on whether hard-limit is enabled
2378
2580075
  d_proxy->spendResource(r);
2379
2380
2580075
  bool within_budget =
2381
2580075
      !asynch_interrupt
2382
2580075
      && (conflict_budget < 0 || conflicts < (uint64_t)conflict_budget)
2383
7740225
      && (propagation_budget < 0
2384
          || propagations < (uint64_t)propagation_budget);
2385
2580075
  return within_budget;
2386
}
2387
2388
1932
SatProofManager* Solver::getProofManager()
2389
{
2390
1932
  return isProofEnabled() ? d_pfManager.get() : nullptr;
2391
}
2392
2393
2292
std::shared_ptr<ProofNode> Solver::getProof()
2394
{
2395
2292
  return isProofEnabled() ? d_pfManager->getProof() : nullptr;
2396
}
2397
2398
18070120
bool Solver::isProofEnabled() const { return d_pfManager != nullptr; }
2399
2400
} /* CVC4::Minisat namespace */
2401
84700
} /* CVC4 namespace */