GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/bitblast/lazy_bitblaster.cpp Lines: 222 317 70.0 %
Date: 2021-03-23 Branches: 364 1141 31.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file lazy_bitblaster.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Liana Hadarean, Aina Niemetz, Mathias Preiner
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Bitblaster for the lazy bv solver.
13
 **
14
 ** Bitblaster for the lazy bv solver.
15
 **/
16
17
#include "theory/bv/bitblast/lazy_bitblaster.h"
18
19
#include "cvc4_private.h"
20
#include "options/bv_options.h"
21
#include "prop/cnf_stream.h"
22
#include "prop/sat_solver.h"
23
#include "prop/sat_solver_factory.h"
24
#include "smt/smt_engine.h"
25
#include "smt/smt_statistics_registry.h"
26
#include "theory/bv/abstraction.h"
27
#include "theory/bv/bv_solver_lazy.h"
28
#include "theory/bv/theory_bv.h"
29
#include "theory/bv/theory_bv_utils.h"
30
#include "theory/rewriter.h"
31
#include "theory/theory_model.h"
32
33
namespace CVC4 {
34
namespace theory {
35
namespace bv {
36
37
namespace {
38
39
/* Determine the number of uncached nodes that a given node consists of.  */
40
uint64_t numNodes(TNode node, utils::NodeSet& seen)
41
{
42
  std::vector<TNode> stack;
43
  uint64_t res = 0;
44
45
  stack.push_back(node);
46
  while (!stack.empty())
47
  {
48
    Node n = stack.back();
49
    stack.pop_back();
50
51
    if (seen.find(n) != seen.end()) continue;
52
53
    res += 1;
54
    seen.insert(n);
55
    stack.insert(stack.end(), n.begin(), n.end());
56
  }
57
  return res;
58
}
59
}
60
61
8956
TLazyBitblaster::TLazyBitblaster(context::Context* c,
62
                                 bv::BVSolverLazy* bv,
63
                                 const std::string name,
64
8956
                                 bool emptyNotify)
65
    : TBitblaster<Node>(),
66
      d_bv(bv),
67
      d_ctx(c),
68
8956
      d_nullRegistrar(new prop::NullRegistrar()),
69
8956
      d_assertedAtoms(new (true) context::CDList<prop::SatLiteral>(c)),
70
8956
      d_explanations(new (true) ExplanationMap(c)),
71
      d_variables(),
72
      d_bbAtoms(),
73
      d_abstraction(NULL),
74
      d_emptyNotify(emptyNotify),
75
      d_fullModelAssertionLevel(c, 0),
76
      d_name(name),
77
35824
      d_statistics(name)
78
{
79
8956
  d_satSolver.reset(
80
      prop::SatSolverFactory::createMinisat(c, smtStatisticsRegistry(), name));
81
82
8956
  ResourceManager* rm = smt::currentResourceManager();
83
26868
  d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
84
8956
                                        d_nullRegistrar.get(),
85
8956
                                        d_nullContext.get(),
86
                                        nullptr,
87
                                        rm,
88
                                        prop::FormulaLitPolicy::INTERNAL,
89
8956
                                        "LazyBitblaster"));
90
91
26868
  d_satSolverNotify.reset(
92
8956
      d_emptyNotify
93
          ? (prop::BVSatSolverNotify*)new MinisatEmptyNotify()
94
          : (prop::BVSatSolverNotify*)new MinisatNotify(
95
8956
                d_cnfStream.get(), bv, this));
96
97
8956
  d_satSolver->setNotify(d_satSolverNotify.get());
98
8956
}
99
100
2
void TLazyBitblaster::setAbstraction(AbstractionModule* abs) {
101
2
  d_abstraction = abs;
102
2
}
103
104
26859
TLazyBitblaster::~TLazyBitblaster()
105
{
106
8953
  d_assertedAtoms->deleteSelf();
107
8953
  d_explanations->deleteSelf();
108
17906
}
109
110
111
/**
112
 * Bitblasts the atom, assigns it a marker literal, adding it to the SAT solver
113
 * NOTE: duplicate clauses are not detected because of marker literal
114
 * @param node the atom to be bitblasted
115
 *
116
 */
117
700225
void TLazyBitblaster::bbAtom(TNode node)
118
{
119
700225
  NodeManager* nm = NodeManager::currentNM();
120
700225
  node = node.getKind() == kind::NOT ? node[0] : node;
121
122
700225
  if (hasBBAtom(node))
123
  {
124
1257144
    return;
125
  }
126
127
  // make sure it is marked as an atom
128
71653
  addAtom(node);
129
130
71653
  Debug("bitvector-bitblast") << "Bitblasting node " << node << "\n";
131
71653
  ++d_statistics.d_numAtoms;
132
133
  /// if we are using bit-vector abstraction bit-blast the original
134
  /// interpretation
135
143318
  if (options::bvAbstraction() && d_abstraction != NULL
136
143318
      && d_abstraction->isAbstraction(node))
137
  {
138
    // node must be of the form P(args) = bv1
139
    Node expansion = Rewriter::rewrite(d_abstraction->getInterpretation(node));
140
141
    Node atom_bb;
142
    if (expansion.getKind() == kind::CONST_BOOLEAN)
143
    {
144
      atom_bb = expansion;
145
    }
146
    else
147
    {
148
      Assert(expansion.getKind() == kind::AND);
149
      std::vector<Node> atoms;
150
      for (unsigned i = 0; i < expansion.getNumChildren(); ++i)
151
      {
152
        Node normalized_i = Rewriter::rewrite(expansion[i]);
153
        Node atom_i =
154
            normalized_i.getKind() != kind::CONST_BOOLEAN
155
                ? Rewriter::rewrite(d_atomBBStrategies[normalized_i.getKind()](
156
                      normalized_i, this))
157
                : normalized_i;
158
        atoms.push_back(atom_i);
159
      }
160
      atom_bb = utils::mkAnd(atoms);
161
    }
162
    Assert(!atom_bb.isNull());
163
    Node atom_definition = nm->mkNode(kind::EQUAL, node, atom_bb);
164
    storeBBAtom(node, atom_bb);
165
    d_cnfStream->convertAndAssert(atom_definition, false, false);
166
    return;
167
  }
168
169
  // the bitblasted definition of the atom
170
143306
  Node normalized = Rewriter::rewrite(node);
171
  Node atom_bb =
172
71653
      normalized.getKind() != kind::CONST_BOOLEAN
173
71610
          ? d_atomBBStrategies[normalized.getKind()](normalized, this)
174
214916
          : normalized;
175
176
71653
  atom_bb = Rewriter::rewrite(atom_bb);
177
178
  // asserting that the atom is true iff the definition holds
179
143306
  Node atom_definition = nm->mkNode(kind::EQUAL, node, atom_bb);
180
71653
  storeBBAtom(node, atom_bb);
181
71653
  d_cnfStream->convertAndAssert(atom_definition, false, false);
182
}
183
184
71653
void TLazyBitblaster::storeBBAtom(TNode atom, Node atom_bb) {
185
71653
  d_bbAtoms.insert(atom);
186
71653
}
187
188
91908
void TLazyBitblaster::storeBBTerm(TNode node, const Bits& bits) {
189
91908
  d_termCache.insert(std::make_pair(node, bits));
190
91908
}
191
192
193
1399830
bool TLazyBitblaster::hasBBAtom(TNode atom) const {
194
1399830
  return d_bbAtoms.find(atom) != d_bbAtoms.end();
195
}
196
197
198
17514
void TLazyBitblaster::makeVariable(TNode var, Bits& bits) {
199
17514
  Assert(bits.size() == 0);
200
198751
  for (unsigned i = 0; i < utils::getSize(var); ++i) {
201
181237
    bits.push_back(utils::mkBitOf(var, i));
202
  }
203
17514
  d_variables.insert(var);
204
17514
}
205
206
uint64_t TLazyBitblaster::computeAtomWeight(TNode node, NodeSet& seen)
207
{
208
  node = node.getKind() == kind::NOT ? node[0] : node;
209
  if (!utils::isBitblastAtom(node)) { return 0; }
210
  Node atom_bb =
211
      Rewriter::rewrite(d_atomBBStrategies[node.getKind()](node, this));
212
  uint64_t size = numNodes(atom_bb, seen);
213
  return size;
214
}
215
216
// cnf conversion ensures the atom represents itself
217
Node TLazyBitblaster::getBBAtom(TNode node) const {
218
  return node;
219
}
220
221
294174
void TLazyBitblaster::bbTerm(TNode node, Bits& bits) {
222
223
294174
  if (hasBBTerm(node)) {
224
202947
    getBBTerm(node, bits);
225
202947
    return;
226
  }
227
91227
  Assert(node.getType().isBitVector());
228
229
91227
  d_bv->spendResource(ResourceManager::Resource::BitblastStep);
230
91227
  Debug("bitvector-bitblast") << "Bitblasting term " << node <<"\n";
231
91227
  ++d_statistics.d_numTerms;
232
233
91227
  d_termBBStrategies[node.getKind()] (node, bits,this);
234
235
91227
  Assert(bits.size() == utils::getSize(node));
236
237
91227
  storeBBTerm(node, bits);
238
}
239
/// Public methods
240
241
71653
void TLazyBitblaster::addAtom(TNode atom) {
242
71653
  d_cnfStream->ensureLiteral(atom);
243
71653
  prop::SatLiteral lit = d_cnfStream->getLiteral(atom);
244
71653
  d_satSolver->addMarkerLiteral(lit);
245
71653
}
246
247
15034
void TLazyBitblaster::explain(TNode atom, std::vector<TNode>& explanation) {
248
15034
  prop::SatLiteral lit = d_cnfStream->getLiteral(atom);
249
250
15034
  ++(d_statistics.d_numExplainedPropagations);
251
15034
  if (options::bvEagerExplanations()) {
252
7556
    Assert(d_explanations->find(lit) != d_explanations->end());
253
7556
    const std::vector<prop::SatLiteral>& literal_explanation = (*d_explanations)[lit].get();
254
29727
    for (unsigned i = 0; i < literal_explanation.size(); ++i) {
255
22171
      explanation.push_back(d_cnfStream->getNode(literal_explanation[i]));
256
    }
257
15112
    return;
258
  }
259
260
14956
  std::vector<prop::SatLiteral> literal_explanation;
261
7478
  d_satSolver->explain(lit, literal_explanation);
262
38528
  for (unsigned i = 0; i < literal_explanation.size(); ++i) {
263
31050
    explanation.push_back(d_cnfStream->getNode(literal_explanation[i]));
264
  }
265
}
266
267
268
/*
269
 * Asserts the clauses corresponding to the atom to the Sat Solver
270
 * by turning on the marker literal (i.e. setting it to false)
271
 * @param node the atom to be asserted
272
 *
273
 */
274
275
171639
bool TLazyBitblaster::propagate() {
276
171639
  return d_satSolver->propagate() == prop::SAT_VALUE_TRUE;
277
}
278
279
619545
bool TLazyBitblaster::assertToSat(TNode lit, bool propagate) {
280
  // strip the not
281
1239090
  TNode atom;
282
619545
  if (lit.getKind() == kind::NOT) {
283
251348
    atom = lit[0];
284
  } else {
285
368197
    atom = lit;
286
  }
287
619545
  Assert(utils::isBitblastAtom(atom));
288
289
619545
  Assert(hasBBAtom(atom));
290
291
619545
  prop::SatLiteral markerLit = d_cnfStream->getLiteral(atom);
292
293
619545
  if(lit.getKind() == kind::NOT) {
294
251348
    markerLit = ~markerLit;
295
  }
296
297
1239090
  Debug("bitvector-bb")
298
619545
      << "BVSolverLazy::TLazyBitblaster::assertToSat asserting node: " << atom
299
619545
      << "\n";
300
1239090
  Debug("bitvector-bb")
301
619545
      << "BVSolverLazy::TLazyBitblaster::assertToSat with literal:   "
302
619545
      << markerLit << "\n";
303
304
619545
  prop::SatValue ret = d_satSolver->assertAssumption(markerLit, propagate);
305
306
619545
  d_assertedAtoms->push_back(markerLit);
307
308
1239090
  return ret == prop::SAT_VALUE_TRUE || ret == prop::SAT_VALUE_UNKNOWN;
309
}
310
311
/**
312
 * Calls the solve method for the Sat Solver.
313
 * passing it the marker literals to be asserted
314
 *
315
 * @return true for sat, and false for unsat
316
 */
317
318
9151
bool TLazyBitblaster::solve() {
319
9151
  if (Trace.isOn("bitvector")) {
320
    Trace("bitvector") << "TLazyBitblaster::solve() asserted atoms ";
321
    context::CDList<prop::SatLiteral>::const_iterator it = d_assertedAtoms->begin();
322
    for (; it != d_assertedAtoms->end(); ++it) {
323
      Trace("bitvector") << "     " << d_cnfStream->getNode(*it) << "\n";
324
    }
325
  }
326
9151
  Debug("bitvector") << "TLazyBitblaster::solve() asserted atoms " << d_assertedAtoms->size() <<"\n";
327
9151
  d_fullModelAssertionLevel.set(d_bv->numAssertions());
328
9151
  return prop::SAT_VALUE_TRUE == d_satSolver->solve();
329
}
330
331
prop::SatValue TLazyBitblaster::solveWithBudget(unsigned long budget) {
332
  if (Trace.isOn("bitvector")) {
333
    Trace("bitvector") << "TLazyBitblaster::solveWithBudget() asserted atoms ";
334
    context::CDList<prop::SatLiteral>::const_iterator it = d_assertedAtoms->begin();
335
    for (; it != d_assertedAtoms->end(); ++it) {
336
      Trace("bitvector") << "     " << d_cnfStream->getNode(*it) << "\n";
337
    }
338
  }
339
  Debug("bitvector") << "TLazyBitblaster::solveWithBudget() asserted atoms " << d_assertedAtoms->size() <<"\n";
340
  return d_satSolver->solve(budget);
341
}
342
343
12112
void TLazyBitblaster::getConflict(std::vector<TNode>& conflict)
344
{
345
12112
  NodeManager* nm = NodeManager::currentNM();
346
24224
  prop::SatClause conflictClause;
347
12112
  d_satSolver->getUnsatCore(conflictClause);
348
349
139702
  for (unsigned i = 0; i < conflictClause.size(); i++)
350
  {
351
127590
    prop::SatLiteral lit = conflictClause[i];
352
255180
    TNode atom = d_cnfStream->getNode(lit);
353
255180
    Node not_atom;
354
127590
    if (atom.getKind() == kind::NOT)
355
    {
356
100829
      not_atom = atom[0];
357
    }
358
    else
359
    {
360
26761
      not_atom = nm->mkNode(kind::NOT, atom);
361
    }
362
127590
    conflict.push_back(not_atom);
363
  }
364
12112
}
365
366
8956
TLazyBitblaster::Statistics::Statistics(const std::string& prefix) :
367
17912
  d_numTermClauses(prefix + "::NumTermSatClauses", 0),
368
17912
  d_numAtomClauses(prefix + "::NumAtomSatClauses", 0),
369
17912
  d_numTerms(prefix + "::NumBitblastedTerms", 0),
370
17912
  d_numAtoms(prefix + "::NumBitblastedAtoms", 0),
371
17912
  d_numExplainedPropagations(prefix + "::NumExplainedPropagations", 0),
372
17912
  d_numBitblastingPropagations(prefix + "::NumBitblastingPropagations", 0),
373
116428
  d_bitblastTimer(prefix + "::BitblastTimer")
374
{
375
8956
  smtStatisticsRegistry()->registerStat(&d_numTermClauses);
376
8956
  smtStatisticsRegistry()->registerStat(&d_numAtomClauses);
377
8956
  smtStatisticsRegistry()->registerStat(&d_numTerms);
378
8956
  smtStatisticsRegistry()->registerStat(&d_numAtoms);
379
8956
  smtStatisticsRegistry()->registerStat(&d_numExplainedPropagations);
380
8956
  smtStatisticsRegistry()->registerStat(&d_numBitblastingPropagations);
381
8956
  smtStatisticsRegistry()->registerStat(&d_bitblastTimer);
382
8956
}
383
384
385
17906
TLazyBitblaster::Statistics::~Statistics() {
386
8953
  smtStatisticsRegistry()->unregisterStat(&d_numTermClauses);
387
8953
  smtStatisticsRegistry()->unregisterStat(&d_numAtomClauses);
388
8953
  smtStatisticsRegistry()->unregisterStat(&d_numTerms);
389
8953
  smtStatisticsRegistry()->unregisterStat(&d_numAtoms);
390
8953
  smtStatisticsRegistry()->unregisterStat(&d_numExplainedPropagations);
391
8953
  smtStatisticsRegistry()->unregisterStat(&d_numBitblastingPropagations);
392
8953
  smtStatisticsRegistry()->unregisterStat(&d_bitblastTimer);
393
8953
}
394
395
1844162
bool TLazyBitblaster::MinisatNotify::notify(prop::SatLiteral lit) {
396
1844162
  if(options::bvEagerExplanations()) {
397
    // compute explanation
398
1026074
    if (d_lazyBB->d_explanations->find(lit) == d_lazyBB->d_explanations->end()) {
399
153202
      std::vector<prop::SatLiteral> literal_explanation;
400
76601
      d_lazyBB->d_satSolver->explain(lit, literal_explanation);
401
76601
      d_lazyBB->d_explanations->insert(lit, literal_explanation);
402
    } else {
403
      // we propagated it at a lower level
404
949473
      return true;
405
    }
406
  }
407
894689
  ++(d_lazyBB->d_statistics.d_numBitblastingPropagations);
408
1789378
  TNode atom = d_cnf->getNode(lit);
409
894689
  return d_bv->storePropagation(atom, SUB_BITBLAST);
410
}
411
412
void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) {
413
  if (clause.size() > 1) {
414
    NodeBuilder<> lemmab(kind::OR);
415
    for (unsigned i = 0; i < clause.size(); ++ i) {
416
      lemmab << d_cnf->getNode(clause[i]);
417
    }
418
    Node lemma = lemmab;
419
    d_bv->d_im.lemma(lemma, InferenceId::BV_LAZY_LEMMA);
420
  } else {
421
    d_bv->d_im.lemma(d_cnf->getNode(clause[0]), InferenceId::BV_LAZY_LEMMA);
422
  }
423
}
424
425
1591
void TLazyBitblaster::MinisatNotify::spendResource(ResourceManager::Resource r)
426
{
427
1591
  d_bv->spendResource(r);
428
1591
}
429
430
21012409
void TLazyBitblaster::MinisatNotify::safePoint(ResourceManager::Resource r)
431
{
432
21012409
  d_bv->d_im.safePoint(r);
433
21012409
}
434
435
31866
EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b)
436
{
437
31866
  int numAssertions = d_bv->numAssertions();
438
  bool has_full_model =
439
31866
      numAssertions != 0 && d_fullModelAssertionLevel.get() == numAssertions;
440
441
63732
  Debug("bv-equality-status")
442
31866
      << "TLazyBitblaster::getEqualityStatus " << a << " = " << b << "\n";
443
63732
  Debug("bv-equality-status")
444
31866
      << "BVSatSolver has full model? " << has_full_model << "\n";
445
446
  // First check if it trivially rewrites to false/true
447
  Node a_eq_b =
448
63732
      Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL, a, b));
449
450
31866
  if (a_eq_b == utils::mkFalse()) return theory::EQUALITY_FALSE;
451
29148
  if (a_eq_b == utils::mkTrue()) return theory::EQUALITY_TRUE;
452
453
29148
  if (!has_full_model)
454
  {
455
114
    return theory::EQUALITY_UNKNOWN;
456
  }
457
458
  // Check if cache is valid (invalidated in check and pops)
459
29034
  if (d_bv->d_invalidateModelCache.get())
460
  {
461
100
    invalidateModelCache();
462
  }
463
29034
  d_bv->d_invalidateModelCache.set(false);
464
465
58068
  Node a_value = getTermModel(a, true);
466
58068
  Node b_value = getTermModel(b, true);
467
468
29034
  Assert(a_value.isConst() && b_value.isConst());
469
470
29034
  if (a_value == b_value)
471
  {
472
4001
    Debug("bv-equality-status") << "theory::EQUALITY_TRUE_IN_MODEL\n";
473
4001
    return theory::EQUALITY_TRUE_IN_MODEL;
474
  }
475
25033
  Debug("bv-equality-status") << "theory::EQUALITY_FALSE_IN_MODEL\n";
476
25033
  return theory::EQUALITY_FALSE_IN_MODEL;
477
}
478
479
6316
bool TLazyBitblaster::isSharedTerm(TNode node) {
480
6316
  return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
481
}
482
483
bool TLazyBitblaster::hasValue(TNode a) {
484
  Assert(hasBBTerm(a));
485
  Bits bits;
486
  getBBTerm(a, bits);
487
  for (int i = bits.size() -1; i >= 0; --i) {
488
    prop::SatValue bit_value;
489
    if (d_cnfStream->hasLiteral(bits[i])) {
490
      prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
491
      bit_value = d_satSolver->value(bit);
492
      if (bit_value ==  prop::SAT_VALUE_UNKNOWN)
493
        return false;
494
    } else {
495
      return false;
496
    }
497
  }
498
  return true;
499
}
500
/**
501
 * Returns the value a is currently assigned to in the SAT solver
502
 * or null if the value is completely unassigned.
503
 *
504
 * @param a
505
 * @param fullModel whether to create a "full model," i.e., add
506
 * constants to equivalence classes that don't already have them
507
 *
508
 * @return
509
 */
510
22100
Node TLazyBitblaster::getModelFromSatSolver(TNode a, bool fullModel) {
511
22100
  if (!hasBBTerm(a)) {
512
404
    return fullModel? utils::mkConst(utils::getSize(a), 0u) : Node();
513
  }
514
515
43392
  Bits bits;
516
21696
  getBBTerm(a, bits);
517
43392
  Integer value(0);
518
284504
  for (int i = bits.size() -1; i >= 0; --i) {
519
    prop::SatValue bit_value;
520
262864
    if (d_cnfStream->hasLiteral(bits[i])) {
521
259525
      prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
522
259525
      bit_value = d_satSolver->value(bit);
523
259525
      Assert(bit_value != prop::SAT_VALUE_UNKNOWN);
524
    } else {
525
3395
      if (!fullModel) return Node();
526
      // unconstrained bits default to false
527
3283
      bit_value = prop::SAT_VALUE_FALSE;
528
    }
529
525616
    Integer bit_int = bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0);
530
262808
    value = value * 2 + bit_int;
531
  }
532
21640
  return utils::mkConst(bits.size(), value);
533
}
534
535
3047
bool TLazyBitblaster::collectModelValues(TheoryModel* m,
536
                                         const std::set<Node>& termSet)
537
{
538
403367
  for (std::set<Node>::const_iterator it = termSet.begin(); it != termSet.end(); ++it) {
539
421677
    TNode var = *it;
540
    // not actually a leaf of the bit-vector theory
541
400320
    if (d_variables.find(var) == d_variables.end())
542
378963
      continue;
543
544
21357
    Assert(Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var));
545
    // only shared terms could not have been bit-blasted
546
21357
    Assert(hasBBTerm(var) || isSharedTerm(var));
547
548
42714
    Node const_value = getModelFromSatSolver(var, true);
549
21357
    Assert(const_value.isNull() || const_value.isConst());
550
21357
    if(const_value != Node()) {
551
42714
      Debug("bitvector-model")
552
21357
          << "TLazyBitblaster::collectModelValues (assert (= " << var << " "
553
21357
          << const_value << "))\n";
554
21357
      if (!m->assertEquality(var, const_value, true))
555
      {
556
        return false;
557
      }
558
    }
559
  }
560
3047
  return true;
561
}
562
563
void TLazyBitblaster::clearSolver() {
564
  Assert(d_ctx->getLevel() == 0);
565
  d_assertedAtoms->deleteSelf();
566
  d_assertedAtoms = new(true) context::CDList<prop::SatLiteral>(d_ctx);
567
  d_explanations->deleteSelf();
568
  d_explanations = new(true) ExplanationMap(d_ctx);
569
  d_bbAtoms.clear();
570
  d_variables.clear();
571
  d_termCache.clear();
572
573
  invalidateModelCache();
574
  // recreate sat solver
575
  d_satSolver.reset(
576
      prop::SatSolverFactory::createMinisat(d_ctx, smtStatisticsRegistry()));
577
  ResourceManager* rm = smt::currentResourceManager();
578
  d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
579
                                        d_nullRegistrar.get(),
580
                                        d_nullContext.get(),
581
                                        nullptr,
582
                                        rm));
583
  d_satSolverNotify.reset(
584
      d_emptyNotify
585
          ? (prop::BVSatSolverNotify*)new MinisatEmptyNotify()
586
          : (prop::BVSatSolverNotify*)new MinisatNotify(
587
                d_cnfStream.get(), d_bv, this));
588
  d_satSolver->setNotify(d_satSolverNotify.get());
589
}
590
591
}  // namespace bv
592
}  // namespace theory
593
26685
}  // namespace CVC4