GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/minisat/core/Solver.cc Lines: 920 1123 81.9 %
Date: 2021-03-23 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
7994464
bool assertionLevelOnly()
58
{
59
15072297
  return (options::produceProofs() || options::unsatCores())
60
10883097
         && 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
8895
static DoubleOption  opt_var_decay         (_cat, "var-decay",   "The variable activity decay factor",            0.95,     DoubleRange(0, false, 1, false));
119
8895
static DoubleOption  opt_clause_decay      (_cat, "cla-decay",   "The clause activity decay factor",              0.999,    DoubleRange(0, false, 1, false));
120
8895
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
8895
static DoubleOption  opt_random_seed       (_cat, "rnd-seed",    "Used by the random variable selection",         91648253, DoubleRange(0, false, HUGE_VAL, false));
122
8895
static IntOption     opt_ccmin_mode        (_cat, "ccmin-mode",  "Controls conflict clause minimization (0=none, 1=basic, 2=deep)", 2, IntRange(0, 2));
123
8895
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
8895
static BoolOption    opt_rnd_init_act      (_cat, "rnd-init",    "Randomize the initial activity", false);
125
8895
static BoolOption    opt_luby_restart      (_cat, "luby",        "Use the Luby restart sequence", true);
126
8895
static IntOption     opt_restart_first     (_cat, "rfirst",      "The base restart interval", 25, IntRange(1, INT32_MAX));
127
8895
static DoubleOption  opt_restart_inc       (_cat, "rinc",        "Restart interval increase factor", 3, DoubleRange(1, false, HUGE_VAL, false));
128
8895
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
3072651
  ScopedBool(bool& watch, bool newValue) : d_watch(watch), d_oldValue(watch)
142
  {
143
3072651
    watch = newValue;
144
3072651
  }
145
3072651
  ~ScopedBool() { d_watch = d_oldValue; }
146
};
147
148
//=================================================================================================
149
// Constructor/Destructor:
150
151
9029
Solver::Solver(CVC4::prop::TheoryProxy* proxy,
152
               CVC4::context::Context* context,
153
               CVC4::context::UserContext* userContext,
154
               ProofNodeManager* pnm,
155
9029
               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
18058
      watches(WatcherDeleted(ca)),
212
      qhead(0),
213
      simpDB_assigns(-1),
214
      simpDB_props(0),
215
18058
      order_heap(VarOrderLt(activity)),
216
      progress_estimate(0),
217
9029
      remove_satisfied(!enableIncremental)
218
219
      // Resource constraints:
220
      //
221
      ,
222
      conflict_budget(-1),
223
      propagation_budget(-1),
224
54174
      asynch_interrupt(false)
225
{
226
9029
  if (pnm)
227
  {
228
1932
    d_pfManager.reset(
229
966
        new SatProofManager(this, proxy->getCnfStream(), userContext, pnm));
230
  }
231
8063
  else if (options::unsatCores())
232
  {
233
1826
    ProofManager::currentPM()->initSatProof(this);
234
  }
235
236
  // Create the constant variables
237
9029
  varTrue = newVar(true, false, false);
238
9029
  varFalse = newVar(false, false, false);
239
240
  // Assert the constants
241
9029
  uncheckedEnqueue(mkLit(varTrue, false));
242
9029
  uncheckedEnqueue(mkLit(varFalse, true));
243
  // FIXME: these should be axioms I believe
244
9029
  if (options::unsatCores() && !isProofEnabled())
245
  {
246
1826
    ProofManager::getSatProof()->registerTrueLit(mkLit(varTrue, false));
247
1826
    ProofManager::getSatProof()->registerFalseLit(mkLit(varFalse, true));
248
  }
249
9029
}
250
251
252
9026
Solver::~Solver()
253
{
254
9026
}
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
808640
Var Solver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool preRegister, bool canErase)
265
{
266
808640
    int v = nVars();
267
268
808640
    watches  .init(mkLit(v, false));
269
808640
    watches  .init(mkLit(v, true ));
270
808640
    assigns  .push(l_Undef);
271
808640
    vardata  .push(VarData(CRef_Undef, -1, -1, assertionLevel, -1));
272
808640
    activity .push(rnd_init_act ? drand(random_seed) * 0.00001 : 0);
273
808640
    seen     .push(0);
274
808640
    polarity .push(sign);
275
808640
    decision .push();
276
808640
    trail    .capacity(v+1);
277
    // push whether it corresponds to a theory atom
278
808640
    theory.push(isTheoryAtom);
279
280
808640
    setDecisionVar(v, dvar);
281
282
808640
    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
808640
    if (preRegister)
286
    {
287
1039084
      Debug("minisat") << "  To register at level " << decisionLevel()
288
519542
                       << std::endl;
289
519542
      variables_to_register.push(VarIntroInfo(v, decisionLevel()));
290
    }
291
292
808640
    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
52269712
CRef Solver::reason(Var x) {
323
52269712
  Trace("pf::sat") << "Solver::reason(" << x << ")" << std::endl;
324
325
  // If we already have a reason, just return it
326
52269712
  if (vardata[x].d_reason != CRef_Lazy)
327
  {
328
52213657
    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
52213657
    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
2175418
bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
453
{
454
2175418
    if (!ok) return false;
455
456
    // Check if clause is satisfied and remove false/duplicate literals:
457
2175418
    sort(ps);
458
    Lit p; int i, j;
459
460
    // Which user-level to assert this clause at
461
2175418
    int clauseLevel = (removable && !assertionLevelOnly()) ? 0 : assertionLevel;
462
463
    // Check the clause for tautologies and similar
464
2175418
    int falseLiteralsCount = 0;
465
9217259
    for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
466
      // Update the level
467
14551878
      clauseLevel = assertionLevelOnly()
468
14349382
                        ? assertionLevel
469
14349382
                        : std::max(clauseLevel, intro_level(var(ps[i])));
470
      // Tautologies are ignored
471
7275939
      if (ps[i] == ~p) {
472
62324
        id = ClauseIdUndef;
473
        // Clause can be ignored
474
62324
        return true;
475
      }
476
      // Clauses with 0-level true literals are also ignored
477
7213615
      if (value(ps[i]) == l_True && level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0) {
478
171774
        id = ClauseIdUndef;
479
171774
        return true;
480
      }
481
      // Ignore repeated literals
482
7041841
      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
7038803
      if (value(ps[i]) == l_False) {
488
7850116
        if (!options::unsatCores() && !isProofEnabled()
489
4590543
            && level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0)
490
        {
491
743163
          continue;
492
        }
493
        else
494
        {
495
          // If we decide to keep it, we count it into the false literals
496
2145533
          falseLiteralsCount++;
497
        }
498
      }
499
      // This literal is a keeper
500
6295640
      ps[j++] = p = ps[i];
501
    }
502
503
    // Fit to size
504
1941320
    ps.shrink(i - j);
505
506
    // If we are in solve_ or propagate
507
1941320
    if (minisat_busy)
508
    {
509
760953
      Trace("pf::sat") << "Add clause adding a new lemma: ";
510
3906882
      for (int k = 0; k < ps.size(); ++k) {
511
3145929
        Trace("pf::sat") << ps[k] << " ";
512
      }
513
760953
      Trace("pf::sat") << std::endl;
514
515
760953
      lemmas.push();
516
760953
      ps.copyTo(lemmas.last());
517
760953
      lemmas_removable.push(removable);
518
760953
      if (options::unsatCores() && !isProofEnabled())
519
      {
520
        // Store the expression being converted to CNF until
521
        // the clause is actually created
522
403062
        lemmas_cnf_assertion.push_back(
523
403062
            ProofManager::getCnfProof()->getCurrentAssertion());
524
201531
        id = ClauseIdUndef;
525
      }
526
    } else {
527
1180367
      Assert(decisionLevel() == 0);
528
529
      // If all false, we're in conflict
530
1180367
      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
123458
            return ok = false;
558
          }
559
        }
560
        else
561
        {
562
862
          return ok = false;
563
        }
564
      }
565
566
1178880
      CRef cr = CRef_Undef;
567
568
      // If not unit, add the clause
569
1178880
      if (ps.size() > 1) {
570
571
1062893
        lemma_lt lt(*this);
572
1062893
        sort(ps, lt);
573
574
1062893
        cr = ca.alloc(clauseLevel, ps, false);
575
1062893
        clauses_persistent.push(cr);
576
1062893
        attachClause(cr);
577
578
1062893
        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
1178830
      if (ps.size() == falseLiteralsCount + 1) {
611
121296
        if(assigns[var(ps[0])] == l_Undef) {
612
119824
          Assert(assigns[var(ps[0])] != l_False);
613
119824
          uncheckedEnqueue(ps[0], cr);
614
239648
          Debug("cores") << "i'm registering a unit clause, maybe input"
615
119824
                         << std::endl;
616
119824
          if (ps.size() == 1)
617
          {
618
115344
            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
115344
            if (isProofEnabled())
638
            {
639
20908
              d_pfManager->registerSatLitAssumption(ps[0]);
640
            }
641
          }
642
119824
          CRef confl = propagate(CHECK_WITHOUT_THEORY);
643
119824
          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
119824
          return ok;
671
        } else {
672
1472
          if (options::unsatCores() && !isProofEnabled())
673
          {
674
            id = ClauseIdUndef;
675
          }
676
1472
          return ok;
677
        }
678
      }
679
    }
680
681
1818487
    return true;
682
}
683
684
685
2162867
void Solver::attachClause(CRef cr) {
686
2162867
    const Clause& c = ca[cr];
687
2162867
    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
2162867
    Assert(c.size() > 1);
697
2162867
    watches[~c[0]].push(Watcher(cr, c[1]));
698
2162867
    watches[~c[1]].push(Watcher(cr, c[0]));
699
2162867
    if (c.removable()) learnts_literals += c.size();
700
1651578
    else            clauses_literals += c.size();
701
2162867
}
702
703
704
809235
void Solver::detachClause(CRef cr, bool strict) {
705
809235
    const Clause& c = ca[cr];
706
809235
    Debug("minisat") << "Solver::detachClause(" << c << ")" << std::endl;
707
809235
    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
809235
    Assert(c.size() > 1);
719
809235
    if (options::unsatCores() && !isProofEnabled())
720
    {
721
79187
      ProofManager::getSatProof()->markDeleted(cr);
722
    }
723
724
809235
    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
720026
        watches.smudge(~c[0]);
730
720026
        watches.smudge(~c[1]);
731
    }
732
733
809235
    if (c.removable()) learnts_literals -= c.size();
734
512695
    else            clauses_literals -= c.size(); }
735
736
737
720026
void Solver::removeClause(CRef cr) {
738
720026
    Clause& c = ca[cr];
739
720026
    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
720026
    detachClause(cr);
750
    // Don't leave pointers to free'd memory!
751
720026
    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
12535
      if (isProofEnabled())
760
      {
761
1870
        Trace("pf::sat")
762
935
            << "Solver::removeClause: eagerly compute propagation of " << c[0]
763
935
            << "\n";
764
935
        d_pfManager->startResChain(c);
765
3452
        for (unsigned i = 1, size = c.size(); i < size; ++i)
766
        {
767
2517
          d_pfManager->addResolutionStep(c[i]);
768
        }
769
935
        d_pfManager->endResChain(c[0]);
770
      }
771
12535
      vardata[var(c[0])].d_reason = CRef_Undef;
772
    }
773
720026
    c.mark(1);
774
720026
    ca.free(cr);
775
720026
}
776
777
778
585166
bool Solver::satisfied(const Clause& c) const {
779
9489372
    for (int i = 0; i < c.size(); i++)
780
8973479
        if (value(c[i]) == l_True)
781
69273
            return true;
782
515893
    return false; }
783
784
785
// Revert to the state at given level (keeping all assignment at 'level' but not beyond).
786
//
787
534598
void Solver::cancelUntil(int level) {
788
534598
    Debug("minisat") << "minisat::cancelUntil(" << level << ")" << std::endl;
789
790
534598
    if (decisionLevel() > level){
791
        // Pop the SMT context
792
2907847
        for (int l = trail_lim.size() - level; l > 0; --l) {
793
2492737
          d_context->pop();
794
        }
795
51745311
        for (int c = trail.size()-1; c >= trail_lim[level]; c--){
796
51330201
            Var      x  = var(trail[c]);
797
51330201
            assigns [x] = l_Undef;
798
51330201
            vardata[x].d_trail_index = -1;
799
102660402
            if ((phase_saving > 1 ||
800
                 ((phase_saving == 1) && c > trail_lim.last())
801
102660402
                 ) && ((polarity[x] & 0x2) == 0)) {
802
50680895
              polarity[x] = sign(trail[c]);
803
            }
804
51330201
            insertVarOrder(x);
805
        }
806
415110
        qhead = trail_lim[level];
807
415110
        trail.shrink(trail.size() - trail_lim[level]);
808
415110
        trail_lim.shrink(trail_lim.size() - level);
809
415110
        flipped.shrink(flipped.size() - level);
810
811
        // Register variables that have not been registered yet
812
415110
        int currentLevel = decisionLevel();
813
716966
        for (int i = variables_to_register.size() - 1;
814
716966
             i >= 0 && variables_to_register[i].d_level > currentLevel;
815
             --i)
816
        {
817
301856
          variables_to_register[i].d_level = currentLevel;
818
603712
          d_proxy->variableNotify(
819
301856
              MinisatSatSolver::toSatVariable(variables_to_register[i].d_var));
820
        }
821
    }
822
534598
}
823
824
12401
void Solver::resetTrail() { cancelUntil(0); }
825
826
//=================================================================================================
827
// Major methods:
828
829
830
2556668
Lit Solver::pickBranchLit()
831
{
832
    Lit nextLit;
833
834
    // Theory requests
835
2556664
    nextLit =
836
2556668
        MinisatSatSolver::toMinisatLit(d_proxy->getNextTheoryDecisionRequest());
837
2574098
    while (nextLit != lit_Undef) {
838
54419
      if(value(var(nextLit)) == l_Undef) {
839
91404
        Debug("theoryDecision")
840
45702
            << "getNextTheoryDecisionRequest(): now deciding on " << nextLit
841
45702
            << std::endl;
842
45702
        decisions++;
843
844
        // org-mode tracing -- theory decision
845
45702
        if (Trace.isOn("dtview"))
846
        {
847
          dtviewDecisionHelper(
848
              d_context->getLevel(),
849
              d_proxy->getNode(MinisatSatSolver::toSatLiteral(nextLit)),
850
              "THEORY");
851
        }
852
853
45702
        if (Trace.isOn("dtview::prop"))
854
        {
855
          dtviewPropagationHeaderHelper(d_context->getLevel());
856
        }
857
858
45702
        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
5021924
    Debug("theoryDecision")
868
2510962
        << "getNextTheoryDecisionRequest(): decide on another literal"
869
2510962
        << std::endl;
870
871
    // DE requests
872
2510962
    bool stopSearch = false;
873
2510962
    nextLit = MinisatSatSolver::toMinisatLit(
874
2510962
        d_proxy->getNextDecisionEngineRequest(stopSearch));
875
2510962
    if(stopSearch) {
876
39181
      return lit_Undef;
877
    }
878
2471781
    if(nextLit != lit_Undef) {
879
588494
      Assert(value(var(nextLit)) == l_Undef)
880
          << "literal to decide already has value";
881
588494
      decisions++;
882
588494
      Var next = var(nextLit);
883
588494
      if(polarity[next] & 0x2) {
884
160020
        nextLit = mkLit(next, polarity[next] & 0x1);
885
      }
886
887
      // org-mode tracing -- decision engine decision
888
588494
      if (Trace.isOn("dtview"))
889
      {
890
        dtviewDecisionHelper(
891
            d_context->getLevel(),
892
            d_proxy->getNode(MinisatSatSolver::toSatLiteral(nextLit)),
893
            "DE");
894
      }
895
896
588494
      if (Trace.isOn("dtview::prop"))
897
      {
898
        dtviewPropagationHeaderHelper(d_context->getLevel());
899
      }
900
901
588494
      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
260114
int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
987
{
988
520228
  Trace("pf::sat") << "Solver::analyze: starting with " << confl
989
260114
                   << " with decision level " << decisionLevel() << "\n";
990
991
260114
  int pathC = 0;
992
260114
  Lit p = lit_Undef;
993
994
  // Generate conflict clause:
995
  //
996
260114
  out_learnt.push();  // (leave room for the asserting literal)
997
260114
  int index = trail.size() - 1;
998
999
260114
  int max_resolution_level = 0;  // Maximal level of the resolved clauses
1000
1001
260114
  if (options::unsatCores() && !isProofEnabled())
1002
  {
1003
67859
    ProofManager::getSatProof()->startResChain(confl);
1004
    }
1005
260114
    if (isProofEnabled())
1006
    {
1007
13870
      d_pfManager->startResChain(ca[confl]);
1008
    }
1009
6883402
    do{
1010
7143516
      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
7143516
        Clause& c = ca[confl];
1018
7143516
        max_resolution_level = std::max(max_resolution_level, c.level());
1019
1020
7143516
        if (c.removable()) claBumpActivity(c);
1021
      }
1022
1023
7143516
        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
7143516
        Trace("pf::sat") << CVC4::push;
1034
30504680
        for (int j = (p == lit_Undef) ? 0 : 1, size = ca[confl].size();
1035
30504680
             j < size;
1036
             j++)
1037
        {
1038
23361164
          Lit q = ca[confl][j];
1039
1040
46722328
          Trace("pf::sat") << "Lit " << q
1041
46722328
                           << " seen/level: " << (seen[var(q)] ? 1 : 0) << " / "
1042
23361164
                           << level(var(q)) << "\n";
1043
23361164
          if (!seen[var(q)] && level(var(q)) > 0)
1044
          {
1045
14251485
            varBumpActivity(var(q));
1046
14251485
            seen[var(q)] = 1;
1047
14251485
            if (level(var(q)) >= decisionLevel())
1048
7143516
              pathC++;
1049
            else
1050
7107969
              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
9109679
            if (!seen[var(q)] && level(var(q)) == 0)
1057
            {
1058
747018
              max_resolution_level =
1059
1494036
                  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
9109679
            if (level(var(q)) == 0)
1064
            {
1065
747018
              if (options::unsatCores() && !isProofEnabled())
1066
              {
1067
365358
                ProofManager::getSatProof()->resolveOutUnit(q);
1068
              }
1069
747018
              if (isProofEnabled())
1070
              {
1071
133945
                d_pfManager->addResolutionStep(q);
1072
              }
1073
            }
1074
          }
1075
        }
1076
7143516
        Trace("pf::sat") << CVC4::pop;
1077
1078
        // Select next clause to look at:
1079
37455085
        while (!seen[var(trail[index--])]);
1080
7143516
        p     = trail[index+1];
1081
7143516
        confl = reason(var(p));
1082
7143516
        seen[var(p)] = 0;
1083
7143516
        pathC--;
1084
1085
7143516
        if (pathC > 0 && confl != CRef_Undef)
1086
        {
1087
6883402
          if (options::unsatCores() && !isProofEnabled())
1088
          {
1089
1822424
            ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p));
1090
          }
1091
6883402
          if (isProofEnabled())
1092
          {
1093
119944
            d_pfManager->addResolutionStep(ca[confl], p);
1094
          }
1095
        }
1096
1097
7143516
    }while (pathC > 0);
1098
260114
    out_learnt[0] = ~p;
1099
260114
    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
260114
    out_learnt.copyTo(analyze_toclear);
1113
260114
    if (ccmin_mode == 2){
1114
260114
        uint32_t abstract_level = 0;
1115
7368083
        for (i = 1; i < out_learnt.size(); i++)
1116
7107969
            abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involved in conflict)
1117
1118
7368083
        for (i = j = 1; i < out_learnt.size(); i++) {
1119
7107969
            if (reason(var(out_learnt[i])) == CRef_Undef) {
1120
1555806
                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
260114
    max_literals += out_learnt.size();
1164
260114
    out_learnt.shrink(i - j);
1165
260114
    tot_literals += out_learnt.size();
1166
1167
    // Find correct backtrack level:
1168
    //
1169
260114
    if (out_learnt.size() == 1)
1170
7108
        out_btlevel = 0;
1171
    else{
1172
253006
        int max_i = 1;
1173
        // Find the first literal assigned at the next-highest level:
1174
4726713
        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
253006
        Lit p2 = out_learnt[max_i];
1179
253006
        out_learnt[max_i] = out_learnt[1];
1180
253006
        out_learnt[1] = p2;
1181
253006
        out_btlevel = level(var(p2));
1182
    }
1183
1184
10028924
    for (int k = 0; k < analyze_toclear.size(); k++)
1185
9768810
      seen[var(analyze_toclear[k])] = 0;  // ('seen[]' is now cleared)
1186
1187
    // Return the maximal resolution level
1188
260114
    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
51729946
void Solver::uncheckedEnqueue(Lit p, CRef from)
1272
{
1273
51729946
  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
51729946
  Assert(value(p) == l_Undef);
1297
51729946
  Assert(var(p) < nVars());
1298
51729946
  assigns[var(p)] = lbool(!sign(p));
1299
51729946
  vardata[var(p)] = VarData(
1300
      from, decisionLevel(), assertionLevel, intro_level(var(p)), trail.size());
1301
51729946
  trail.push_(p);
1302
51729946
  if (theory[var(p)])
1303
  {
1304
    // Enqueue to the theory
1305
15885240
    d_proxy->enqueueTheoryLiteral(MinisatSatSolver::toSatLiteral(p));
1306
  }
1307
51729946
}
1308
1309
3060524
CRef Solver::propagate(TheoryCheckType type)
1310
{
1311
3060524
    CRef confl = CRef_Undef;
1312
3060524
    recheck = false;
1313
3060524
    theoryConflict = false;
1314
1315
6121048
    ScopedBool scoped_bool(minisat_busy, true);
1316
1317
    // Add lemmas that we're left behind
1318
3060524
    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
3060524
    if (type == CHECK_FINAL) {
1328
      // Do the theory check
1329
73166
      theoryCheck(CVC4::theory::Theory::EFFORT_FULL);
1330
      // Pick up the theory propagated literals (there could be some,
1331
      // if new lemmas are added)
1332
73152
      propagateTheory();
1333
      // If there are lemmas (or conflicts) update them
1334
73152
      if (lemmas.size() > 0) {
1335
49294
        recheck = true;
1336
49294
        confl = updateLemmas();
1337
49294
        return confl;
1338
      } else {
1339
23858
        recheck = d_proxy->theoryNeedCheck();
1340
23858
        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
944530
    do {
1347
        // Propagate on the clauses
1348
3931888
        confl = propagateBool();
1349
        // If no conflict, do the theory check
1350
3931888
        if (confl == CRef_Undef && type != CHECK_WITHOUT_THEORY) {
1351
            // Do the theory check
1352
3557055
            if (type == CHECK_FINAL_FAKE) {
1353
              theoryCheck(CVC4::theory::Theory::EFFORT_FULL);
1354
            } else {
1355
3557055
              theoryCheck(CVC4::theory::Theory::EFFORT_STANDARD);
1356
            }
1357
            // Pick up the theory propagated literals
1358
3557052
            propagateTheory();
1359
            // If there are lemmas (or conflicts) update them
1360
7114104
            if (lemmas.size() > 0) {
1361
210348
              confl = updateLemmas();
1362
            }
1363
        } else {
1364
          // if dumping decision tree, print the conflict
1365
374833
          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
374833
          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
3931885
    } while (confl == CRef_Undef && qhead < trail.size());
1391
2987355
    return confl;
1392
}
1393
1394
3630204
void Solver::propagateTheory() {
1395
7260408
  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
3630204
  d_proxy->theoryPropagate(propagatedLiteralsClause);
1399
1400
7260408
  vec<Lit> propagatedLiterals;
1401
3630204
  MinisatSatSolver::toMinisatClause(propagatedLiteralsClause, propagatedLiterals);
1402
1403
3630204
  int oldTrailSize = trail.size();
1404
3630204
  Debug("minisat") << "old trail size is " << oldTrailSize << ", propagating " << propagatedLiterals.size() << " lits..." << std::endl;
1405
11805775
  for (unsigned i = 0, i_end = propagatedLiterals.size(); i < i_end; ++ i) {
1406
8175571
    Debug("minisat") << "Theory propagated: " << propagatedLiterals[i] << std::endl;
1407
    // multiple theories can propagate the same literal
1408
8175571
    Lit p = propagatedLiterals[i];
1409
8175571
    if (value(p) == l_Undef) {
1410
4378789
      uncheckedEnqueue(p, CRef_Lazy);
1411
    } else {
1412
3796782
      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
3630204
}
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
3630221
void Solver::theoryCheck(CVC4::theory::Theory::Effort effort)
1443
{
1444
3630221
  d_proxy->theoryCheck(effort);
1445
3630204
}
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
3931888
CRef Solver::propagateBool()
1459
{
1460
3931888
    CRef    confl     = CRef_Undef;
1461
3931888
    int     num_props = 0;
1462
3931888
    watches.cleanAll();
1463
1464
97823922
    while (qhead < trail.size()){
1465
46946017
        Lit            p   = trail[qhead++];     // 'p' is enqueued fact to propagate.
1466
46946017
        vec<Watcher>&  ws  = watches[p];
1467
        Watcher        *i, *j, *end;
1468
46946017
        num_props++;
1469
1470
        // if propagation tracing enabled, print boolean propagation
1471
46946017
        if (Trace.isOn("dtview::prop"))
1472
        {
1473
          dtviewBoolPropagationHelper(decisionLevel(), p, d_proxy);
1474
        }
1475
1476
572171674
        for (i = j = (Watcher*)ws, end = i + ws.size();  i != end;){
1477
            // Try to avoid inspecting the clause:
1478
525225657
            Lit blocker = i->blocker;
1479
845594627
            if (value(blocker) == l_True){
1480
980575934
                *j++ = *i++; continue; }
1481
1482
            // Make sure the false literal is data[1]:
1483
204856687
            CRef     cr        = i->cref;
1484
204856687
            Clause&  c         = ca[cr];
1485
204856687
            Lit      false_lit = ~p;
1486
204856687
            if (c[0] == false_lit)
1487
69811672
                c[0] = c[1], c[1] = false_lit;
1488
204856687
            Assert(c[1] == false_lit);
1489
204856687
            i++;
1490
1491
            // If 0th watch is true, then clause is already satisfied.
1492
204856687
            Lit     first = c[0];
1493
204856687
            Watcher w     = Watcher(cr, first);
1494
224325711
            if (first != blocker && value(first) == l_True){
1495
38938048
                *j++ = w; continue; }
1496
1497
            // Look for new watch:
1498
185387663
            Assert(c.size() >= 2);
1499
625630027
            for (int k = 2; k < c.size(); k++)
1500
581245791
                if (value(c[k]) != l_False){
1501
141003427
                    c[1] = c[k]; c[k] = false_lit;
1502
141003427
                    watches[~c[1]].push(w);
1503
141003427
                    goto NextClause; }
1504
1505
            // Did not find watch -- clause is unit under assignment:
1506
44384236
            *j++ = w;
1507
44384236
            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
44181293
                uncheckedEnqueue(first, cr);
1515
1516
185387663
        NextClause:;
1517
        }
1518
46946017
        ws.shrink(i - j);
1519
    }
1520
3931888
    propagations += num_props;
1521
3931888
    simpDB_props -= num_props;
1522
1523
3931888
    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
16985
void Solver::removeSatisfied(vec<CRef>& cs)
1562
{
1563
    int i, j;
1564
602151
    for (i = j = 0; i < cs.size(); i++){
1565
585166
        Clause& c = ca[cs[i]];
1566
585166
        if (satisfied(c)) {
1567
69273
          if (options::unsatCores() && !isProofEnabled() && locked(c))
1568
          {
1569
            // store a resolution of the literal c propagated
1570
2262
            ProofManager::getSatProof()->storeUnitResolution(c[0]);
1571
          }
1572
69273
          removeClause(cs[i]);
1573
        }
1574
        else
1575
        {
1576
515893
          cs[j++] = cs[i];
1577
        }
1578
    }
1579
16985
    cs.shrink(i - j);
1580
16985
}
1581
1582
6380
void Solver::removeClausesAboveLevel(vec<CRef>& cs, int level)
1583
{
1584
    int i, j;
1585
601241
    for (i = j = 0; i < cs.size(); i++){
1586
594861
        Clause& c = ca[cs[i]];
1587
594861
        if (c.level() > level) {
1588
177704
          Assert(!locked(c));
1589
177704
          removeClause(cs[i]);
1590
        } else {
1591
417157
            cs[j++] = cs[i];
1592
        }
1593
    }
1594
6380
    cs.shrink(i - j);
1595
6380
}
1596
1597
16985
void Solver::rebuildOrderHeap()
1598
{
1599
33970
    vec<Var> vs;
1600
2207424
    for (Var v = 0; v < nVars(); v++)
1601
2190439
        if (decision[v] && value(v) == l_Undef)
1602
1410519
            vs.push(v);
1603
16985
    order_heap.build(vs);
1604
16985
}
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
43242
bool Solver::simplify()
1616
{
1617
43242
  Assert(decisionLevel() == 0);
1618
1619
43242
  if (!ok || propagate(CHECK_WITHOUT_THEORY) != CRef_Undef) return ok = false;
1620
1621
42962
  if (nAssigns() == simpDB_assigns || (simpDB_props > 0)) return true;
1622
1623
  // Remove satisfied clauses:
1624
16985
  removeSatisfied(clauses_removable);
1625
16985
  if (remove_satisfied)  // Can be turned off.
1626
    removeSatisfied(clauses_persistent);
1627
16985
  checkGarbage();
1628
16985
  rebuildOrderHeap();
1629
1630
16985
  simpDB_assigns = nAssigns();
1631
16985
  simpDB_props =
1632
16985
      clauses_literals + learnts_literals;  // (shouldn't depend on stats
1633
                                            // really, but it will do for now)
1634
1635
16985
  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
12922
lbool Solver::search(int nof_conflicts)
1653
{
1654
12922
  Assert(ok);
1655
  int backtrack_level;
1656
12922
  int conflictC = 0;
1657
25844
  vec<Lit> learnt_clause;
1658
12922
  starts++;
1659
1660
12922
  TheoryCheckType check_type = CHECK_WITH_THEORY;
1661
  for (;;)
1662
  {
1663
    // Propagate and call the theory solvers
1664
2888582
    CRef confl = propagate(check_type);
1665
2888565
    Assert(lemmas.size() == 0);
1666
1667
2888565
    if (confl != CRef_Undef)
1668
    {
1669
264750
      conflicts++;
1670
264750
      conflictC++;
1671
1672
264750
      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
260114
      learnt_clause.clear();
1694
260114
      int max_level = analyze(confl, learnt_clause, backtrack_level);
1695
260114
      cancelUntil(backtrack_level);
1696
1697
      // Assert the conflict clause and the asserting literal
1698
260114
      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
253006
        CRef cr = ca.alloc(assertionLevelOnly() ? assertionLevel : max_level,
1713
                           learnt_clause,
1714
253006
                           true);
1715
253006
        clauses_removable.push(cr);
1716
253006
        attachClause(cr);
1717
253006
        claBumpActivity(ca[cr]);
1718
253006
        uncheckedEnqueue(learnt_clause[0], cr);
1719
253006
        if (options::unsatCores() && !isProofEnabled())
1720
        {
1721
65616
          ClauseId id = ProofManager::getSatProof()->registerClause(cr, LEARNT);
1722
65616
          ProofManager::getSatProof()->endResChain(id);
1723
        }
1724
253006
        if (isProofEnabled())
1725
        {
1726
12679
          d_pfManager->endResChain(ca[cr]);
1727
        }
1728
      }
1729
1730
260114
      varDecayActivity();
1731
260114
      claDecayActivity();
1732
1733
260114
      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
318142
      if (theoryConflict && options::sat_refine_conflicts())
1753
      {
1754
        check_type = CHECK_FINAL_FAKE;
1755
      }
1756
      else
1757
      {
1758
260114
        check_type = CHECK_WITH_THEORY;
1759
      }
1760
    }
1761
    else
1762
    {
1763
      // If this was a final check, we are satisfiable
1764
2623815
      if (check_type == CHECK_FINAL)
1765
      {
1766
64835
        bool decisionEngineDone = d_proxy->isDecisionEngineDone();
1767
        // Unless a lemma has added more stuff to the queues
1768
179194
        if (!decisionEngineDone
1769
64835
            && (!order_heap.empty() || qhead < trail.size()))
1770
        {
1771
49524
          check_type = CHECK_WITH_THEORY;
1772
172214
          continue;
1773
        }
1774
15311
        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
5953
          return l_True;
1784
        }
1785
      }
1786
2558980
      else if (check_type == CHECK_FINAL_FAKE)
1787
      {
1788
        check_type = CHECK_WITH_THEORY;
1789
      }
1790
1791
5117960
      if ((nof_conflicts >= 0 && conflictC >= nof_conflicts)
1792
5115648
          || !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
2556668
      if (decisionLevel() == 0 && !simplify())
1805
      {
1806
        return l_False;
1807
      }
1808
1809
2556668
      if (clauses_removable.size() - nAssigns() >= max_learnts)
1810
      {
1811
        // Reduce the set of learnt clauses:
1812
13256
        reduceDB();
1813
      }
1814
1815
2556668
      Lit next = lit_Undef;
1816
2556668
      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
2556668
      if (next == lit_Undef)
1838
      {
1839
        // New variable decision:
1840
2556668
        next = pickBranchLit();
1841
1842
2620472
        if (next == lit_Undef)
1843
        {
1844
          // We need to do a full theory check to confirm
1845
127616
          Debug("minisat::search")
1846
63808
              << "Doing a full theory check..." << std::endl;
1847
63808
          check_type = CHECK_FINAL;
1848
63808
          continue;
1849
        }
1850
      }
1851
1852
      // Increase decision level and enqueue 'next'
1853
2492856
      newDecisionLevel();
1854
2492856
      uncheckedEnqueue(next);
1855
    }
1856
2875660
  }
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
12922
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
12922
    for (size = 1, seq = 0; size < x+1; seq++, size = 2*size+1);
1892
1893
22820
    while (size-1 != x){
1894
4949
        size = (size-1)>>1;
1895
4949
        seq--;
1896
4949
        x = x % size;
1897
    }
1898
1899
12922
    return pow(y, seq);
1900
}
1901
1902
// NOTE: assumptions passed in member-variable 'assumptions'.
1903
12127
lbool Solver::solve_()
1904
{
1905
12127
    Debug("minisat") << "nvars = " << nVars() << std::endl;
1906
1907
24254
    ScopedBool scoped_bool(minisat_busy, true);
1908
1909
12127
    Assert(decisionLevel() == 0);
1910
1911
12127
    model.clear();
1912
12127
    d_conflict.clear();
1913
12127
    if (!ok){
1914
1517
      minisat_busy = false;
1915
1517
      return l_False;
1916
    }
1917
1918
10610
    solves++;
1919
1920
10610
    max_learnts               = nClauses() * learntsize_factor;
1921
10610
    learntsize_adjust_confl   = learntsize_adjust_start_confl;
1922
10610
    learntsize_adjust_cnt     = (int)learntsize_adjust_confl;
1923
10610
    lbool   status            = l_Undef;
1924
1925
10610
    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
10610
    int curr_restarts = 0;
1934
36412
    while (status == l_Undef){
1935
12922
        double rest_base = luby_restart ? luby(restart_inc, curr_restarts) : pow(restart_inc, curr_restarts);
1936
12922
        status = search(rest_base * restart_first);
1937
12901
        if (!withinBudget(ResourceManager::Resource::SatConflictStep))
1938
          break;  // FIXME add restart option?
1939
12901
        curr_restarts++;
1940
    }
1941
1942
10589
    if (!withinBudget(ResourceManager::Resource::SatConflictStep))
1943
      status = l_Undef;
1944
1945
10589
    if (verbosity >= 1)
1946
1
        printf("===============================================================================\n");
1947
1948
1949
10589
    if (status == l_True){
1950
        // Extend & copy model:
1951
5953
        model.growTo(nVars());
1952
522601
        for (int i = 0; i < nVars(); i++) {
1953
516648
          model[i] = value(i);
1954
516648
          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
10589
    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
741155
    for (int v = 0; v < nVars(); v++)
2054
2214159
        for (int s = 0; s < 2; s++){
2055
1476106
            Lit p = mkLit(v, s);
2056
            // printf(" >>> RELOCING: %s%d\n", sign(p)?"-":"", var(p)+1);
2057
1476106
            vec<Watcher>& ws = watches[p];
2058
3722634
            for (int j = 0; j < ws.size(); j++)
2059
            {
2060
4865310
              ca.reloc(ws[j].cref,
2061
                       to,
2062
2618782
                       (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
904627
    for (int i = 0; i < clauses_persistent.size(); i++)
2096
    {
2097
1924267
      ca.reloc(clauses_persistent[i],
2098
               to,
2099
1022742
               (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
259701
CRef Solver::updateLemmas() {
2187
2188
259701
  Debug("minisat::lemmas") << "Solver::updateLemmas() begin" << std::endl;
2189
2190
  // Avoid adding lemmas indefinitely without resource-out
2191
259701
  d_proxy->spendResource(ResourceManager::Resource::LemmaStep);
2192
2193
259701
  CRef conflict = CRef_Undef;
2194
2195
  // Decision level to backtrack to
2196
259701
  int backtrackLevel = decisionLevel();
2197
2198
  // We use this comparison operator
2199
259701
  lemma_lt lt(*this);
2200
2201
  // Check for propagation and level to backtrack to
2202
259701
  int i = 0;
2203
779243
  while (i < lemmas.size()) {
2204
    // We need this loop as when we backtrack, due to registration more lemmas could be added
2205
1781615
    for (; i < lemmas.size(); ++ i)
2206
    {
2207
      // The current lemma
2208
760922
      vec<Lit>& lemma = lemmas[i];
2209
2210
760922
      Trace("pf::sat") << "Solver::updateLemmas: working on lemma: ";
2211
3906800
      for (int k = 0; k < lemma.size(); ++k) {
2212
3145878
        Trace("pf::sat") << lemma[k] << " ";
2213
      }
2214
760922
      Trace("pf::sat") << std::endl;
2215
2216
      // If it's an empty lemma, we have a conflict at zero level
2217
762472
      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
759372
      sort(lemma, lt);
2226
      // See if the lemma propagates something
2227
759372
      if (lemma.size() == 1 || value(lemma[1]) == l_False) {
2228
422065
        Debug("minisat::lemmas") << "found unit " << lemma.size() << std::endl;
2229
        // This lemma propagates, see which level we need to backtrack to
2230
422065
        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
422065
        if (value(lemma[0]) != l_True || level(var(lemma[0])) > currentBacktrackLevel) {
2233
411318
          if (currentBacktrackLevel < backtrackLevel) {
2234
154217
            backtrackLevel = currentBacktrackLevel;
2235
          }
2236
        }
2237
      }
2238
    }
2239
2240
    // Pop so that propagation would be current
2241
259771
    Debug("minisat::lemmas") << "Solver::updateLemmas(): backtracking to " << backtrackLevel << " from " << decisionLevel() << std::endl;
2242
259771
    cancelUntil(backtrackLevel);
2243
  }
2244
2245
  // Last index in the trail
2246
259701
  int backtrack_index = trail.size();
2247
2248
259701
  Assert(!options::unsatCores() || isProofEnabled()
2249
         || lemmas.size() == (int)lemmas_cnf_assertion.size());
2250
2251
  // Attach all the clauses and enqueue all the propagations
2252
1020623
  for (int j = 0; j < lemmas.size(); ++j)
2253
  {
2254
    // The current lemma
2255
760922
    vec<Lit>& lemma = lemmas[j];
2256
760922
    bool removable = lemmas_removable[j];
2257
2258
    // Attach it if non-unit
2259
760922
    CRef lemma_ref = CRef_Undef;
2260
760922
    if (lemma.size() > 1) {
2261
      // If the lemmas is removable, we can compute its level by the level
2262
701704
      int clauseLevel = assertionLevel;
2263
701704
      if (removable && !assertionLevelOnly())
2264
      {
2265
199340
        clauseLevel = 0;
2266
1866099
        for (int k = 0; k < lemma.size(); ++k)
2267
        {
2268
1666759
          clauseLevel = std::max(clauseLevel, intro_level(var(lemma[k])));
2269
        }
2270
      }
2271
2272
701704
      lemma_ref = ca.alloc(clauseLevel, lemma, removable);
2273
701704
      if (options::unsatCores() && !isProofEnabled())
2274
      {
2275
387590
        TNode cnf_assertion = lemmas_cnf_assertion[j];
2276
2277
387590
        Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (2)"
2278
193795
                         << std::endl;
2279
193795
        ClauseId id = ProofManager::getSatProof()->registerClause(lemma_ref,
2280
193795
                                                                  THEORY_LEMMA);
2281
193795
        ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
2282
      }
2283
701704
      if (removable) {
2284
202228
        clauses_removable.push(lemma_ref);
2285
      } else {
2286
499476
        clauses_persistent.push(lemma_ref);
2287
      }
2288
701704
      attachClause(lemma_ref);
2289
    }
2290
2291
    // If the lemma is propagating enqueue its literal (or set the conflict)
2292
760922
    if (conflict == CRef_Undef && value(lemma[0]) != l_True) {
2293
701182
      if (lemma.size() == 1 || (value(lemma[1]) == l_False && trail_index(var(lemma[1])) < backtrack_index)) {
2294
338870
        if (options::unsatCores() && !isProofEnabled() && lemma.size() == 1)
2295
        {
2296
15456
          Node cnf_assertion = lemmas_cnf_assertion[j];
2297
2298
15456
          Trace("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (3) "
2299
7728
                           << cnf_assertion << value(lemma[0]) << std::endl;
2300
7728
          ClauseId id = ProofManager::getSatProof()->registerUnitClause(
2301
7728
              lemma[0], THEORY_LEMMA);
2302
7728
          ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
2303
        }
2304
677740
        Trace("pf::sat") << "Solver::updateLemmas: unit theory lemma: "
2305
338870
                         << lemma[0] << std::endl;
2306
338870
        if (value(lemma[0]) == l_False) {
2307
          // We have a conflict
2308
60415
          if (lemma.size() > 1) {
2309
60128
            Debug("minisat::lemmas") << "Solver::updateLemmas(): conflict" << std::endl;
2310
60128
            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
278455
          Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl;
2325
278455
          Debug("minisat::lemmas") << "lemma ref is " << lemma_ref << std::endl;
2326
278455
          uncheckedEnqueue(lemma[0], lemma_ref);
2327
        }
2328
      }
2329
    }
2330
  }
2331
2332
259701
  Assert(!options::unsatCores() || isProofEnabled()
2333
         || lemmas.size() == (int)lemmas_cnf_assertion.size());
2334
  // Clear the lemmas
2335
259701
  lemmas.clear();
2336
259701
  lemmas_cnf_assertion.clear();
2337
259701
  lemmas_removable.clear();
2338
2339
259701
  if (conflict != CRef_Undef) {
2340
61859
    theoryConflict = true;
2341
  }
2342
2343
259701
  Debug("minisat::lemmas") << "Solver::updateLemmas() end" << std::endl;
2344
2345
259701
  return conflict;
2346
}
2347
2348
4089609
void ClauseAllocator::reloc(CRef& cr,
2349
                            ClauseAllocator& to,
2350
                            CVC4::TSatProof<Solver>* proof)
2351
{
2352
4089609
  Debug("minisat") << "ClauseAllocator::reloc: cr " << cr << std::endl;
2353
  // FIXME what is this CRef_lazy
2354
4089609
  if (cr == CRef_Lazy) return;
2355
2356
4089609
  CRef old = cr;  // save the old reference
2357
4089609
  Clause& c = operator[](cr);
2358
4089609
  if (c.reloced()) { cr = c.relocation(); return; }
2359
2360
1124199
  cr = to.alloc(c.level(), c, c.removable());
2361
1124199
  c.relocate(cr);
2362
1124199
  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
1124199
  to[cr].mark(c.mark());
2369
1124199
  if (to[cr].removable())         to[cr].activity() = c.activity();
2370
902460
  else if (to[cr].has_extra()) to[cr].calcAbstraction();
2371
}
2372
2373
2580158
inline bool Solver::withinBudget(ResourceManager::Resource r) const
2374
{
2375
2580158
  Assert(d_proxy);
2376
  // spendResource sets async_interrupt or throws UnsafeInterruptException
2377
  // depending on whether hard-limit is enabled
2378
2580158
  d_proxy->spendResource(r);
2379
2380
2580158
  bool within_budget =
2381
2580158
      !asynch_interrupt
2382
2580158
      && (conflict_budget < 0 || conflicts < (uint64_t)conflict_budget)
2383
7740474
      && (propagation_budget < 0
2384
          || propagations < (uint64_t)propagation_budget);
2385
2580158
  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
18070458
bool Solver::isProofEnabled() const { return d_pfManager != nullptr; }
2399
2400
} /* CVC4::Minisat namespace */
2401
84713
} /* CVC4 namespace */