GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/bv_quick_check.cpp Lines: 1 200 0.5 %
Date: 2021-03-23 Branches: 2 386 0.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bv_quick_check.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Liana Hadarean, Tim King, 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 Wrapper around the SAT solver used for bitblasting.
13
 **
14
 ** Wrapper around the SAT solver used for bitblasting.
15
 **/
16
17
#include "theory/bv/bv_quick_check.h"
18
19
#include "smt/smt_statistics_registry.h"
20
#include "theory/bv/bitblast/lazy_bitblaster.h"
21
#include "theory/bv/bv_solver_lazy.h"
22
#include "theory/bv/theory_bv_utils.h"
23
24
using namespace CVC4::prop;
25
26
namespace CVC4 {
27
namespace theory {
28
namespace bv {
29
30
BVQuickCheck::BVQuickCheck(const std::string& name,
31
                           theory::bv::BVSolverLazy* bv)
32
    : d_ctx(),
33
      d_bitblaster(new TLazyBitblaster(&d_ctx, bv, name, true)),
34
      d_conflict(),
35
      d_inConflict(&d_ctx, false)
36
{}
37
38
39
bool BVQuickCheck::inConflict() { return d_inConflict.get(); }
40
41
uint64_t BVQuickCheck::computeAtomWeight(TNode node, NodeSet& seen) {
42
  return d_bitblaster->computeAtomWeight(node, seen);
43
}
44
45
void BVQuickCheck::setConflict()
46
{
47
  Assert(!inConflict());
48
  std::vector<TNode> conflict;
49
  d_bitblaster->getConflict(conflict);
50
  Node confl = utils::mkAnd(conflict);
51
  d_inConflict = true;
52
  d_conflict = confl;
53
}
54
55
prop::SatValue BVQuickCheck::checkSat(std::vector<Node>& assumptions, unsigned long budget) {
56
  Node conflict;
57
58
  for (unsigned i = 0; i < assumptions.size(); ++i) {
59
    TNode a = assumptions[i];
60
    Assert(a.getType().isBoolean());
61
    d_bitblaster->bbAtom(a);
62
    bool ok = d_bitblaster->assertToSat(a, false);
63
    if (!ok) {
64
      setConflict();
65
      return SAT_VALUE_FALSE;
66
    }
67
  }
68
69
  if (budget == 0) {
70
    bool ok = d_bitblaster->propagate();
71
    if (!ok) {
72
      setConflict();
73
      return SAT_VALUE_FALSE;
74
    }
75
    return SAT_VALUE_UNKNOWN; // could check if assignment is full and return SAT_VALUE_TRUE
76
  }
77
78
  prop::SatValue res = d_bitblaster->solveWithBudget(budget);
79
  if (res == SAT_VALUE_FALSE) {
80
    setConflict();
81
    return res;
82
  }
83
  // could be unknown or could be sat
84
   return res;
85
}
86
87
prop::SatValue BVQuickCheck::checkSat(unsigned long budget) {
88
  prop::SatValue res = d_bitblaster->solveWithBudget(budget);
89
  if (res == SAT_VALUE_FALSE) {
90
    setConflict();
91
  }
92
  return res;
93
}
94
95
bool BVQuickCheck::addAssertion(TNode assertion) {
96
  Assert(assertion.getType().isBoolean());
97
  d_bitblaster->bbAtom(assertion);
98
  // assert to sat solver and run bcp to detect easy conflicts
99
  bool ok = d_bitblaster->assertToSat(assertion, true);
100
  if (!ok) {
101
    setConflict();
102
  }
103
  return ok;
104
}
105
106
107
void BVQuickCheck::push() {
108
  d_ctx.push();
109
}
110
111
void BVQuickCheck::pop() {
112
  d_ctx.pop();
113
}
114
115
BVQuickCheck::vars_iterator BVQuickCheck::beginVars() {
116
  return d_bitblaster->beginVars();
117
}
118
BVQuickCheck::vars_iterator BVQuickCheck::endVars() {
119
  return d_bitblaster->endVars();
120
}
121
122
Node BVQuickCheck::getVarValue(TNode var, bool fullModel) {
123
  return d_bitblaster->getTermModel(var, fullModel);
124
}
125
126
127
/**
128
 * Constructs a new sat solver which requires throwing out the atomBBCache
129
 * but keeps all the termBBCache
130
 *
131
 */
132
void BVQuickCheck::clearSolver() {
133
  popToZero();
134
  d_bitblaster->clearSolver();
135
}
136
137
void BVQuickCheck::popToZero() {
138
  while (d_ctx.getLevel() > 0) {
139
    d_ctx.pop();
140
  }
141
}
142
143
bool BVQuickCheck::collectModelValues(theory::TheoryModel* model,
144
                                      const std::set<Node>& termSet)
145
{
146
  return d_bitblaster->collectModelValues(model, termSet);
147
}
148
149
BVQuickCheck::~BVQuickCheck() {
150
  clearSolver();
151
}
152
153
QuickXPlain::QuickXPlain(const std::string& name, BVQuickCheck* solver, unsigned long budget)
154
  : d_solver(solver)
155
  , d_budget(budget)
156
  , d_numCalled(0)
157
  , d_minRatioSum(0)
158
  , d_numConflicts(0)
159
  // , d_period(20)
160
  // , d_thresh(0.7)
161
  // , d_hardThresh(0.9)
162
  , d_statistics(name)
163
{}
164
QuickXPlain::~QuickXPlain() {}
165
166
unsigned QuickXPlain::selectUnsatCore(unsigned low, unsigned high,
167
                                      std::vector<TNode>& conflict) {
168
  Assert(!d_solver->getConflict().isNull() && d_solver->inConflict());
169
  Node query_confl = d_solver->getConflict();
170
171
  // conflict wasn't actually minimized
172
  if (query_confl.getNumChildren() == high - low + 1) {
173
    return high;
174
  }
175
176
  TNodeSet nodes;
177
  for (unsigned i = low; i <= high; i++) {
178
    nodes.insert(conflict[i]);
179
  }
180
181
  unsigned write = low;
182
  for (unsigned i = 0; i < query_confl.getNumChildren(); ++i) {
183
    TNode current = query_confl[i];
184
    // the conflict can have nodes in lower decision levels
185
    if (nodes.find(current) != nodes.end()) {
186
      conflict[write++] = current;
187
      nodes.erase(nodes.find(current));
188
    }
189
  }
190
  // if all of the nodes in the conflict were on a lower level
191
  if (write == low) {
192
    return low;
193
  }
194
  Assert(write != 0);
195
  unsigned new_high = write - 1;
196
197
  for (TNodeSet::const_iterator it = nodes.begin(); it != nodes.end(); ++it) {
198
    conflict[write++] = *it;
199
  }
200
  Assert(write - 1 == high);
201
  Assert(new_high <= high);
202
203
  return new_high;
204
}
205
206
void QuickXPlain::minimizeConflictInternal(unsigned low, unsigned high,
207
                                           std::vector<TNode>& conflict,
208
                                           std::vector<TNode>& new_conflict) {
209
  Assert(low <= high && high < conflict.size());
210
211
  if (low == high) {
212
    new_conflict.push_back(conflict[low]);
213
    return;
214
  }
215
216
  // check if top half is unsat
217
  unsigned new_low = (high - low + 1)/ 2 + low;
218
  d_solver->push();
219
220
  for (unsigned i = new_low; i <=high; ++i) {
221
    bool ok = d_solver->addAssertion(conflict[i]);
222
    if (!ok) {
223
      unsigned top = selectUnsatCore(new_low, i, conflict);
224
      d_solver->pop();
225
      minimizeConflictInternal(new_low, top, conflict, new_conflict);
226
      return;
227
    }
228
  }
229
230
  SatValue res = d_solver->checkSat(d_budget);
231
232
  if (res == SAT_VALUE_UNKNOWN) {
233
    ++(d_statistics.d_numUnknown);
234
  } else {
235
    ++(d_statistics.d_numSolved);
236
  }
237
238
  if (res == SAT_VALUE_FALSE) {
239
    unsigned top = selectUnsatCore(new_low, high, conflict);
240
    d_solver->pop();
241
    minimizeConflictInternal(new_low, top, conflict, new_conflict);
242
    return;
243
  }
244
245
  d_solver->pop();
246
  unsigned new_high = new_low - 1;
247
  d_solver->push();
248
249
  // check bottom half
250
  for (unsigned i = low; i <= new_high; ++i) {
251
    bool ok = d_solver->addAssertion(conflict[i]);
252
    if (!ok) {
253
      unsigned top = selectUnsatCore(low, i, conflict);
254
      d_solver->pop();
255
      minimizeConflictInternal(low, top, conflict, new_conflict);
256
      return;
257
    }
258
  }
259
260
  res = d_solver->checkSat(d_budget);
261
262
  if (res == SAT_VALUE_UNKNOWN) {
263
    ++(d_statistics.d_numUnknown);
264
  } else {
265
    ++(d_statistics.d_numSolved);
266
  }
267
268
  if (res == SAT_VALUE_FALSE) {
269
    unsigned top = selectUnsatCore(low, new_high, conflict);
270
    d_solver->pop();
271
    minimizeConflictInternal(low, top, conflict, new_conflict);
272
    return;
273
  }
274
275
  // conflict (probably) contains literals in both halves
276
  // keep bottom half in context (no pop)
277
  minimizeConflictInternal(new_low, high, conflict, new_conflict);
278
  d_solver->pop();
279
  d_solver->push();
280
  for (unsigned i = 0; i < new_conflict.size(); ++i) {
281
    bool ok = d_solver->addAssertion(new_conflict[i]);
282
    if (!ok) {
283
      ++(d_statistics.d_numUnknownWasUnsat);
284
      d_solver->pop();
285
      return;
286
    }
287
  }
288
  minimizeConflictInternal(low, new_high, conflict, new_conflict);
289
  d_solver->pop();
290
}
291
292
293
bool QuickXPlain::useHeuristic() {
294
  return true;
295
  // d_statistics.d_finalPeriod.setData(d_period);
296
  // // try to minimize conflict periodically
297
  // if (d_numConflicts % d_period == 0)
298
  //   return true;
299
300
  // if (d_numCalled == 0) {
301
  //   return true;
302
  // }
303
304
  // if (d_minRatioSum / d_numCalled >= d_thresh &&
305
  //     d_numCalled <= 20 ) {
306
  //   return false;
307
  // }
308
309
  // if (d_minRatioSum / d_numCalled >= d_hardThresh) {
310
  //   return false;
311
  // }
312
313
  // return true;
314
}
315
316
Node QuickXPlain::minimizeConflict(TNode confl) {
317
  ++d_numConflicts;
318
319
  if (!useHeuristic()) {
320
    return confl;
321
  }
322
323
  ++d_numCalled;
324
  ++(d_statistics.d_numConflictsMinimized);
325
  TimerStat::CodeTimer xplainTimer(d_statistics.d_xplainTime);
326
  Assert(confl.getNumChildren() > 2);
327
  std::vector<TNode> conflict;
328
  for (unsigned i = 0; i < confl.getNumChildren(); ++i) {
329
    conflict.push_back(confl[i]);
330
  }
331
  d_solver->popToZero();
332
  std::vector<TNode> minimized;
333
  minimizeConflictInternal(0, conflict.size() - 1, conflict, minimized);
334
335
  double minimization_ratio = ((double) minimized.size())/confl.getNumChildren();
336
  d_minRatioSum+= minimization_ratio;
337
338
339
  // if (minimization_ratio >= d_hardThresh) {
340
  //   d_period = d_period * 5;
341
  // }
342
343
  // if (minimization_ratio <= d_thresh && d_period >= 40) {
344
  //   d_period = d_period *0.5;
345
  // }
346
347
  // if (1.5* d_statistics.d_numUnknown.getData() > d_statistics.d_numSolved.getData()) {
348
  //   d_period = d_period * 2;
349
  // }
350
  d_statistics.d_avgMinimizationRatio << minimization_ratio;
351
  return utils::mkAnd(minimized);
352
}
353
354
QuickXPlain::Statistics::Statistics(const std::string& name)
355
  : d_xplainTime(name + "::QuickXplain::Time")
356
  , d_numSolved(name + "::QuickXplain::NumSolved", 0)
357
  , d_numUnknown(name + "::QuickXplain::NumUnknown", 0)
358
  , d_numUnknownWasUnsat(name + "::QuickXplain::NumUnknownWasUnsat", 0)
359
  , d_numConflictsMinimized(name + "::QuickXplain::NumConflictsMinimized", 0)
360
  , d_finalPeriod(name + "::QuickXplain::FinalPeriod", 0)
361
  , d_avgMinimizationRatio(name + "::QuickXplain::AvgMinRatio")
362
{
363
  smtStatisticsRegistry()->registerStat(&d_xplainTime);
364
  smtStatisticsRegistry()->registerStat(&d_numSolved);
365
  smtStatisticsRegistry()->registerStat(&d_numUnknown);
366
  smtStatisticsRegistry()->registerStat(&d_numUnknownWasUnsat);
367
  smtStatisticsRegistry()->registerStat(&d_numConflictsMinimized);
368
  smtStatisticsRegistry()->registerStat(&d_finalPeriod);
369
  smtStatisticsRegistry()->registerStat(&d_avgMinimizationRatio);
370
}
371
372
QuickXPlain::Statistics::~Statistics() {
373
  smtStatisticsRegistry()->unregisterStat(&d_xplainTime);
374
  smtStatisticsRegistry()->unregisterStat(&d_numSolved);
375
  smtStatisticsRegistry()->unregisterStat(&d_numUnknown);
376
  smtStatisticsRegistry()->unregisterStat(&d_numUnknownWasUnsat);
377
  smtStatisticsRegistry()->unregisterStat(&d_numConflictsMinimized);
378
  smtStatisticsRegistry()->unregisterStat(&d_finalPeriod);
379
  smtStatisticsRegistry()->unregisterStat(&d_avgMinimizationRatio);
380
}
381
382
}  // namespace bv
383
}  // namespace theory
384
26685
}  // namespace CVC4