1 /********************* */
2 /*! \file bv_quick_check.cpp
4 ** Original author: Liana Hadaren
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Wrapper around the SAT solver used for bitblasting.
14 ** Wrapper around the SAT solver used for bitblasting.
17 #include "theory/bv/bv_quick_check.h"
18 #include "theory/bv/theory_bv_utils.h"
20 #include "theory/bv/bitblaster_template.h"
23 using namespace CVC4::theory
;
24 using namespace CVC4::theory::bv
;
25 using namespace CVC4::prop
;
27 BVQuickCheck::BVQuickCheck(const std::string
& name
, theory::bv::TheoryBV
* bv
)
28 : d_ctx(new context::Context())
29 , d_bitblaster(new TLazyBitblaster(d_ctx
, bv
, name
, true))
31 , d_inConflict(d_ctx
, false)
35 bool BVQuickCheck::inConflict() { return d_inConflict
.get(); }
37 uint64_t BVQuickCheck::computeAtomWeight(TNode node
, NodeSet
& seen
) {
38 return d_bitblaster
->computeAtomWeight(node
, seen
);
41 void BVQuickCheck::setConflict() {
42 Assert (!inConflict());
43 std::vector
<TNode
> conflict
;
44 d_bitblaster
->getConflict(conflict
);
45 Node confl
= utils::mkConjunction(conflict
);
50 prop::SatValue
BVQuickCheck::checkSat(std::vector
<Node
>& assumptions
, unsigned long budget
) {
53 for (unsigned i
= 0; i
< assumptions
.size(); ++i
) {
54 TNode a
= assumptions
[i
];
55 Assert (a
.getType().isBoolean());
56 d_bitblaster
->bbAtom(a
);
57 bool ok
= d_bitblaster
->assertToSat(a
, false);
60 return SAT_VALUE_FALSE
;
65 bool ok
= d_bitblaster
->propagate();
68 return SAT_VALUE_FALSE
;
70 return SAT_VALUE_UNKNOWN
; // could check if assignment is full and return SAT_VALUE_TRUE
73 prop::SatValue res
= d_bitblaster
->solveWithBudget(budget
);
74 if (res
== SAT_VALUE_FALSE
) {
78 // could be unknown or could be sat
82 prop::SatValue
BVQuickCheck::checkSat(unsigned long budget
) {
83 prop::SatValue res
= d_bitblaster
->solveWithBudget(budget
);
84 if (res
== SAT_VALUE_FALSE
) {
90 bool BVQuickCheck::addAssertion(TNode assertion
) {
91 Assert (assertion
.getType().isBoolean());
92 d_bitblaster
->bbAtom(assertion
);
93 // assert to sat solver and run bcp to detect easy conflicts
94 bool ok
= d_bitblaster
->assertToSat(assertion
, true);
102 void BVQuickCheck::push() {
106 void BVQuickCheck::pop() {
110 BVQuickCheck::vars_iterator
BVQuickCheck::beginVars() {
111 return d_bitblaster
->beginVars();
113 BVQuickCheck::vars_iterator
BVQuickCheck::endVars() {
114 return d_bitblaster
->endVars();
117 Node
BVQuickCheck::getVarValue(TNode var
) {
118 return d_bitblaster
->getVarValue(var
);
123 * Constructs a new sat solver which requires throwing out the atomBBCache
124 * but keeps all the termBBCache
127 void BVQuickCheck::clearSolver() {
129 d_bitblaster
->clearSolver();
132 void BVQuickCheck::popToZero() {
133 while (d_ctx
->getLevel() > 0) {
138 void BVQuickCheck::collectModelInfo(theory::TheoryModel
* model
, bool fullModel
) {
139 d_bitblaster
->collectModelInfo(model
, fullModel
);
142 BVQuickCheck::~BVQuickCheck() {
146 QuickXPlain::QuickXPlain(const std::string
& name
, BVQuickCheck
* solver
, unsigned long budget
)
157 QuickXPlain::~QuickXPlain() {}
159 unsigned QuickXPlain::selectUnsatCore(unsigned low
, unsigned high
,
160 std::vector
<TNode
>& conflict
) {
162 Assert(!d_solver
->getConflict().isNull() &&
163 d_solver
->inConflict());
164 Node query_confl
= d_solver
->getConflict();
166 // conflict wasn't actually minimized
167 if (query_confl
.getNumChildren() == high
- low
+ 1) {
172 for (unsigned i
= low
; i
<= high
; i
++) {
173 nodes
.insert(conflict
[i
]);
176 unsigned write
= low
;
177 for (unsigned i
= 0; i
< query_confl
.getNumChildren(); ++i
) {
178 TNode current
= query_confl
[i
];
179 // the conflict can have nodes in lower decision levels
180 if (nodes
.find(current
) != nodes
.end()) {
181 conflict
[write
++] = current
;
182 nodes
.erase(nodes
.find(current
));
185 // if all of the nodes in the conflict were on a lower level
190 unsigned new_high
= write
- 1;
192 for (TNodeSet::const_iterator it
= nodes
.begin(); it
!= nodes
.end(); ++it
) {
193 conflict
[write
++] = *it
;
195 Assert (write
-1 == high
);
196 Assert (new_high
<= high
);
201 void QuickXPlain::minimizeConflictInternal(unsigned low
, unsigned high
,
202 std::vector
<TNode
>& conflict
,
203 std::vector
<TNode
>& new_conflict
) {
205 Assert (low
<= high
&& high
< conflict
.size());
208 new_conflict
.push_back(conflict
[low
]);
212 // check if top half is unsat
213 unsigned new_low
= (high
- low
+ 1)/ 2 + low
;
216 for (unsigned i
= new_low
; i
<=high
; ++i
) {
217 bool ok
= d_solver
->addAssertion(conflict
[i
]);
219 unsigned top
= selectUnsatCore(new_low
, i
, conflict
);
221 minimizeConflictInternal(new_low
, top
, conflict
, new_conflict
);
226 SatValue res
= d_solver
->checkSat(d_budget
);
228 if (res
== SAT_VALUE_UNKNOWN
) {
229 ++(d_statistics
.d_numUnknown
);
231 ++(d_statistics
.d_numSolved
);
234 if (res
== SAT_VALUE_FALSE
) {
235 unsigned top
= selectUnsatCore(new_low
, high
, conflict
);
237 minimizeConflictInternal(new_low
, top
, conflict
, new_conflict
);
242 unsigned new_high
= new_low
- 1;
246 for (unsigned i
= low
; i
<= new_high
; ++i
) {
247 bool ok
= d_solver
->addAssertion(conflict
[i
]);
249 unsigned top
= selectUnsatCore(low
, i
, conflict
);
251 minimizeConflictInternal(low
, top
, conflict
, new_conflict
);
256 res
= d_solver
->checkSat(d_budget
);
258 if (res
== SAT_VALUE_UNKNOWN
) {
259 ++(d_statistics
.d_numUnknown
);
261 ++(d_statistics
.d_numSolved
);
264 if (res
== SAT_VALUE_FALSE
) {
265 unsigned top
= selectUnsatCore(low
, new_high
, conflict
);
267 minimizeConflictInternal(low
, top
, conflict
, new_conflict
);
271 // conflict (probably) contains literals in both halves
272 // keep bottom half in context (no pop)
273 minimizeConflictInternal(new_low
, high
, conflict
, new_conflict
);
276 for (unsigned i
= 0; i
< new_conflict
.size(); ++i
) {
277 bool ok
= d_solver
->addAssertion(new_conflict
[i
]);
279 ++(d_statistics
.d_numUnknownWasUnsat
);
284 minimizeConflictInternal(low
, new_high
, conflict
, new_conflict
);
289 bool QuickXPlain::useHeuristic() {
291 // d_statistics.d_finalPeriod.setData(d_period);
292 // // try to minimize conflict periodically
293 // if (d_numConflicts % d_period == 0)
296 // if (d_numCalled == 0) {
300 // if (d_minRatioSum / d_numCalled >= d_thresh &&
301 // d_numCalled <= 20 ) {
305 // if (d_minRatioSum / d_numCalled >= d_hardThresh) {
312 Node
QuickXPlain::minimizeConflict(TNode confl
) {
315 if (!useHeuristic()) {
320 ++(d_statistics
.d_numConflictsMinimized
);
321 TimerStat::CodeTimer
xplainTimer(d_statistics
.d_xplainTime
);
322 Assert (confl
.getNumChildren() > 2);
323 std::vector
<TNode
> conflict
;
324 for (unsigned i
= 0; i
< confl
.getNumChildren(); ++i
) {
325 conflict
.push_back(confl
[i
]);
327 d_solver
->popToZero();
328 std::vector
<TNode
> minimized
;
329 minimizeConflictInternal(0, conflict
.size() - 1, conflict
, minimized
);
331 double minimization_ratio
= ((double) minimized
.size())/confl
.getNumChildren();
332 d_minRatioSum
+= minimization_ratio
;
335 // if (minimization_ratio >= d_hardThresh) {
336 // d_period = d_period * 5;
339 // if (minimization_ratio <= d_thresh && d_period >= 40) {
340 // d_period = d_period *0.5;
343 // if (1.5* d_statistics.d_numUnknown.getData() > d_statistics.d_numSolved.getData()) {
344 // d_period = d_period * 2;
346 d_statistics
.d_avgMinimizationRatio
.addEntry(minimization_ratio
);
347 return utils::mkAnd(minimized
);
350 QuickXPlain::Statistics::Statistics(const std::string
& name
)
351 : d_xplainTime("theory::bv::"+name
+"::QuickXplain::Time")
352 , d_numSolved("theory::bv::"+name
+"::QuickXplain::NumSolved", 0)
353 , d_numUnknown("theory::bv::"+name
+"::QuickXplain::NumUnknown", 0)
354 , d_numUnknownWasUnsat("theory::bv::"+name
+"::QuickXplain::NumUnknownWasUnsat", 0)
355 , d_numConflictsMinimized("theory::bv::"+name
+"::QuickXplain::NumConflictsMinimized", 0)
356 , d_finalPeriod("theory::bv::"+name
+"::QuickXplain::FinalPeriod", 0)
357 , d_avgMinimizationRatio("theory::bv::"+name
+"::QuickXplain::AvgMinRatio")
359 StatisticsRegistry::registerStat(&d_xplainTime
);
360 StatisticsRegistry::registerStat(&d_numSolved
);
361 StatisticsRegistry::registerStat(&d_numUnknown
);
362 StatisticsRegistry::registerStat(&d_numUnknownWasUnsat
);
363 StatisticsRegistry::registerStat(&d_numConflictsMinimized
);
364 StatisticsRegistry::registerStat(&d_finalPeriod
);
365 StatisticsRegistry::registerStat(&d_avgMinimizationRatio
);
368 QuickXPlain::Statistics::~Statistics() {
369 StatisticsRegistry::unregisterStat(&d_xplainTime
);
370 StatisticsRegistry::unregisterStat(&d_numSolved
);
371 StatisticsRegistry::unregisterStat(&d_numUnknown
);
372 StatisticsRegistry::unregisterStat(&d_numUnknownWasUnsat
);
373 StatisticsRegistry::unregisterStat(&d_numConflictsMinimized
);
374 StatisticsRegistry::unregisterStat(&d_finalPeriod
);
375 StatisticsRegistry::unregisterStat(&d_avgMinimizationRatio
);