1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Mathias Preiner, Liana Hadarean, Andrew Reynolds |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Layered bit-vector solver. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/bv/bv_solver_layered.h" |
17 |
|
|
18 |
|
#include "expr/node_algorithm.h" |
19 |
|
#include "options/bv_options.h" |
20 |
|
#include "options/smt_options.h" |
21 |
|
#include "smt/smt_statistics_registry.h" |
22 |
|
#include "theory/bv/abstraction.h" |
23 |
|
#include "theory/bv/bv_eager_solver.h" |
24 |
|
#include "theory/bv/bv_subtheory_algebraic.h" |
25 |
|
#include "theory/bv/bv_subtheory_bitblast.h" |
26 |
|
#include "theory/bv/bv_subtheory_core.h" |
27 |
|
#include "theory/bv/bv_subtheory_inequality.h" |
28 |
|
#include "theory/bv/theory_bv_rewrite_rules_normalization.h" |
29 |
|
#include "theory/bv/theory_bv_rewrite_rules_simplification.h" |
30 |
|
#include "theory/bv/theory_bv_rewriter.h" |
31 |
|
#include "theory/bv/theory_bv_utils.h" |
32 |
|
#include "theory/theory_model.h" |
33 |
|
|
34 |
|
using namespace cvc5::theory::bv::utils; |
35 |
|
|
36 |
|
namespace cvc5 { |
37 |
|
namespace theory { |
38 |
|
namespace bv { |
39 |
|
|
40 |
2 |
BVSolverLayered::BVSolverLayered(TheoryBV& bv, |
41 |
|
context::Context* c, |
42 |
|
context::UserContext* u, |
43 |
|
ProofNodeManager* pnm, |
44 |
2 |
std::string name) |
45 |
|
: BVSolver(bv.d_state, bv.d_im), |
46 |
|
d_bv(bv), |
47 |
|
d_context(c), |
48 |
|
d_alreadyPropagatedSet(c), |
49 |
|
d_sharedTermsSet(c), |
50 |
|
d_subtheories(), |
51 |
|
d_subtheoryMap(), |
52 |
|
d_statistics(), |
53 |
|
d_staticLearnCache(), |
54 |
|
d_lemmasAdded(c, false), |
55 |
|
d_conflict(c, false), |
56 |
|
d_invalidateModelCache(c, true), |
57 |
|
d_literalsToPropagate(c), |
58 |
|
d_literalsToPropagateIndex(c, 0), |
59 |
|
d_propagatedBy(c), |
60 |
|
d_eagerSolver(), |
61 |
6 |
d_abstractionModule(new AbstractionModule(getStatsPrefix(THEORY_BV))), |
62 |
8 |
d_calledPreregister(false) |
63 |
|
{ |
64 |
2 |
if (options::bitblastMode() == options::BitblastMode::EAGER) |
65 |
|
{ |
66 |
2 |
d_eagerSolver.reset(new EagerBitblastSolver(c, this)); |
67 |
2 |
return; |
68 |
|
} |
69 |
|
|
70 |
|
if (options::bitvectorEqualitySolver()) |
71 |
|
{ |
72 |
|
d_subtheories.emplace_back(new CoreSolver(c, this)); |
73 |
|
d_subtheoryMap[SUB_CORE] = d_subtheories.back().get(); |
74 |
|
} |
75 |
|
|
76 |
|
if (options::bitvectorInequalitySolver()) |
77 |
|
{ |
78 |
|
d_subtheories.emplace_back(new InequalitySolver(c, u, this)); |
79 |
|
d_subtheoryMap[SUB_INEQUALITY] = d_subtheories.back().get(); |
80 |
|
} |
81 |
|
|
82 |
|
if (options::bitvectorAlgebraicSolver()) |
83 |
|
{ |
84 |
|
d_subtheories.emplace_back(new AlgebraicSolver(c, this)); |
85 |
|
d_subtheoryMap[SUB_ALGEBRAIC] = d_subtheories.back().get(); |
86 |
|
} |
87 |
|
|
88 |
|
BitblastSolver* bb_solver = new BitblastSolver(c, this); |
89 |
|
if (options::bvAbstraction()) |
90 |
|
{ |
91 |
|
bb_solver->setAbstraction(d_abstractionModule.get()); |
92 |
|
} |
93 |
|
d_subtheories.emplace_back(bb_solver); |
94 |
|
d_subtheoryMap[SUB_BITBLAST] = bb_solver; |
95 |
|
} |
96 |
|
|
97 |
4 |
BVSolverLayered::~BVSolverLayered() {} |
98 |
|
|
99 |
2 |
bool BVSolverLayered::needsEqualityEngine(EeSetupInfo& esi) |
100 |
|
{ |
101 |
2 |
CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE]; |
102 |
2 |
if (core) |
103 |
|
{ |
104 |
|
return core->needsEqualityEngine(esi); |
105 |
|
} |
106 |
|
// otherwise we don't use an equality engine |
107 |
2 |
return false; |
108 |
|
} |
109 |
|
|
110 |
2 |
void BVSolverLayered::finishInit() |
111 |
|
{ |
112 |
2 |
CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE]; |
113 |
2 |
if (core) |
114 |
|
{ |
115 |
|
// must finish initialization in the core solver |
116 |
|
core->finishInit(); |
117 |
|
} |
118 |
2 |
} |
119 |
|
|
120 |
12 |
void BVSolverLayered::spendResource(Resource r) { d_im.spendResource(r); } |
121 |
|
|
122 |
2 |
BVSolverLayered::Statistics::Statistics() |
123 |
2 |
: d_avgConflictSize(smtStatisticsRegistry().registerAverage( |
124 |
4 |
"theory::bv::lazy::AvgBVConflictSize")), |
125 |
2 |
d_solveTimer(smtStatisticsRegistry().registerTimer( |
126 |
4 |
"theory::bv::lazy::solveTimer")), |
127 |
2 |
d_numCallsToCheckFullEffort(smtStatisticsRegistry().registerInt( |
128 |
4 |
"theory::bv::lazy::NumFullCheckCalls")), |
129 |
2 |
d_numCallsToCheckStandardEffort(smtStatisticsRegistry().registerInt( |
130 |
4 |
"theory::bv::lazy::NumStandardCheckCalls")), |
131 |
2 |
d_weightComputationTimer(smtStatisticsRegistry().registerTimer( |
132 |
4 |
"theory::bv::lazy::weightComputationTimer")), |
133 |
2 |
d_numMultSlice(smtStatisticsRegistry().registerInt( |
134 |
12 |
"theory::bv::lazy::NumMultSliceApplied")) |
135 |
|
{ |
136 |
2 |
} |
137 |
|
|
138 |
|
void BVSolverLayered::preRegisterTerm(TNode node) |
139 |
|
{ |
140 |
|
d_calledPreregister = true; |
141 |
|
Debug("bitvector-preregister") |
142 |
|
<< "BVSolverLayered::preRegister(" << node << ")" << std::endl; |
143 |
|
|
144 |
|
if (options::bitblastMode() == options::BitblastMode::EAGER) |
145 |
|
{ |
146 |
|
// the aig bit-blaster option is set heuristically |
147 |
|
// if bv abstraction is used |
148 |
|
if (!d_eagerSolver->isInitialized()) |
149 |
|
{ |
150 |
|
d_eagerSolver->initialize(); |
151 |
|
} |
152 |
|
|
153 |
|
if (node.getKind() == kind::BITVECTOR_EAGER_ATOM) |
154 |
|
{ |
155 |
|
Node formula = node[0]; |
156 |
|
d_eagerSolver->assertFormula(formula); |
157 |
|
} |
158 |
|
return; |
159 |
|
} |
160 |
|
|
161 |
|
for (unsigned i = 0; i < d_subtheories.size(); ++i) |
162 |
|
{ |
163 |
|
d_subtheories[i]->preRegister(node); |
164 |
|
} |
165 |
|
|
166 |
|
// AJR : equality solver currently registers all terms to ExtTheory, if we |
167 |
|
// want a lazy reduction without the bv equality solver, need to call this |
168 |
|
// d_bv.d_extTheory->registerTermRec( node ); |
169 |
|
} |
170 |
|
|
171 |
|
void BVSolverLayered::sendConflict() |
172 |
|
{ |
173 |
|
Assert(d_conflict); |
174 |
|
if (d_conflictNode.isNull()) |
175 |
|
{ |
176 |
|
return; |
177 |
|
} |
178 |
|
else |
179 |
|
{ |
180 |
|
Debug("bitvector") << indent() << "BVSolverLayered::check(): conflict " |
181 |
|
<< d_conflictNode << std::endl; |
182 |
|
d_im.conflict(d_conflictNode, InferenceId::BV_LAYERED_CONFLICT); |
183 |
|
d_statistics.d_avgConflictSize << d_conflictNode.getNumChildren(); |
184 |
|
d_conflictNode = Node::null(); |
185 |
|
} |
186 |
|
} |
187 |
|
|
188 |
|
void BVSolverLayered::checkForLemma(TNode fact) |
189 |
|
{ |
190 |
|
if (fact.getKind() == kind::EQUAL) |
191 |
|
{ |
192 |
|
NodeManager* nm = NodeManager::currentNM(); |
193 |
|
if (fact[0].getKind() == kind::BITVECTOR_UREM) |
194 |
|
{ |
195 |
|
TNode urem = fact[0]; |
196 |
|
TNode result = fact[1]; |
197 |
|
TNode divisor = urem[1]; |
198 |
|
Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor); |
199 |
|
Node divisor_eq_0 = |
200 |
|
nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor))); |
201 |
|
Node split = nm->mkNode( |
202 |
|
kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div); |
203 |
|
lemma(split); |
204 |
|
} |
205 |
|
if (fact[1].getKind() == kind::BITVECTOR_UREM) |
206 |
|
{ |
207 |
|
TNode urem = fact[1]; |
208 |
|
TNode result = fact[0]; |
209 |
|
TNode divisor = urem[1]; |
210 |
|
Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor); |
211 |
|
Node divisor_eq_0 = |
212 |
|
nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor))); |
213 |
|
Node split = nm->mkNode( |
214 |
|
kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div); |
215 |
|
lemma(split); |
216 |
|
} |
217 |
|
} |
218 |
|
} |
219 |
|
|
220 |
|
bool BVSolverLayered::preCheck(Theory::Effort e) |
221 |
|
{ |
222 |
|
check(e); |
223 |
|
return true; |
224 |
|
} |
225 |
|
|
226 |
|
void BVSolverLayered::check(Theory::Effort e) |
227 |
|
{ |
228 |
|
if (done() && e < Theory::EFFORT_FULL) |
229 |
|
{ |
230 |
|
return; |
231 |
|
} |
232 |
|
|
233 |
|
Debug("bitvector") << "BVSolverLayered::check(" << e << ")" << std::endl; |
234 |
|
TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer); |
235 |
|
// we may be getting new assertions so the model cache may not be sound |
236 |
|
d_invalidateModelCache.set(true); |
237 |
|
// if we are using the eager solver |
238 |
|
if (options::bitblastMode() == options::BitblastMode::EAGER) |
239 |
|
{ |
240 |
|
// this can only happen on an empty benchmark |
241 |
|
if (!d_eagerSolver->isInitialized()) |
242 |
|
{ |
243 |
|
d_eagerSolver->initialize(); |
244 |
|
} |
245 |
|
if (!Theory::fullEffort(e)) return; |
246 |
|
|
247 |
|
std::vector<TNode> assertions; |
248 |
|
while (!done()) |
249 |
|
{ |
250 |
|
TNode fact = get().d_assertion; |
251 |
|
Assert(fact.getKind() == kind::BITVECTOR_EAGER_ATOM); |
252 |
|
assertions.push_back(fact); |
253 |
|
d_eagerSolver->assertFormula(fact[0]); |
254 |
|
} |
255 |
|
|
256 |
|
bool ok = d_eagerSolver->checkSat(); |
257 |
|
if (!ok) |
258 |
|
{ |
259 |
|
if (assertions.size() == 1) |
260 |
|
{ |
261 |
|
d_im.conflict(assertions[0], InferenceId::BV_LAYERED_CONFLICT); |
262 |
|
return; |
263 |
|
} |
264 |
|
Node conflict = utils::mkAnd(assertions); |
265 |
|
d_im.conflict(conflict, InferenceId::BV_LAYERED_CONFLICT); |
266 |
|
return; |
267 |
|
} |
268 |
|
return; |
269 |
|
} |
270 |
|
|
271 |
|
if (Theory::fullEffort(e)) |
272 |
|
{ |
273 |
|
++(d_statistics.d_numCallsToCheckFullEffort); |
274 |
|
} |
275 |
|
else |
276 |
|
{ |
277 |
|
++(d_statistics.d_numCallsToCheckStandardEffort); |
278 |
|
} |
279 |
|
// if we are already in conflict just return the conflict |
280 |
|
if (inConflict()) |
281 |
|
{ |
282 |
|
sendConflict(); |
283 |
|
return; |
284 |
|
} |
285 |
|
|
286 |
|
while (!done()) |
287 |
|
{ |
288 |
|
TNode fact = get().d_assertion; |
289 |
|
|
290 |
|
checkForLemma(fact); |
291 |
|
|
292 |
|
for (unsigned i = 0; i < d_subtheories.size(); ++i) |
293 |
|
{ |
294 |
|
d_subtheories[i]->assertFact(fact); |
295 |
|
} |
296 |
|
} |
297 |
|
|
298 |
|
bool ok = true; |
299 |
|
bool complete = false; |
300 |
|
for (unsigned i = 0; i < d_subtheories.size(); ++i) |
301 |
|
{ |
302 |
|
Assert(!inConflict()); |
303 |
|
ok = d_subtheories[i]->check(e); |
304 |
|
complete = d_subtheories[i]->isComplete(); |
305 |
|
|
306 |
|
if (!ok) |
307 |
|
{ |
308 |
|
// if we are in a conflict no need to check with other theories |
309 |
|
Assert(inConflict()); |
310 |
|
sendConflict(); |
311 |
|
return; |
312 |
|
} |
313 |
|
if (complete) |
314 |
|
{ |
315 |
|
// if the last subtheory was complete we stop |
316 |
|
break; |
317 |
|
} |
318 |
|
} |
319 |
|
} |
320 |
|
|
321 |
|
bool BVSolverLayered::collectModelValues(TheoryModel* m, |
322 |
|
const std::set<Node>& termSet) |
323 |
|
{ |
324 |
|
Assert(!inConflict()); |
325 |
|
if (options::bitblastMode() == options::BitblastMode::EAGER) |
326 |
|
{ |
327 |
|
if (!d_eagerSolver->collectModelInfo(m, true)) |
328 |
|
{ |
329 |
|
return false; |
330 |
|
} |
331 |
|
} |
332 |
|
for (unsigned i = 0; i < d_subtheories.size(); ++i) |
333 |
|
{ |
334 |
|
if (d_subtheories[i]->isComplete()) |
335 |
|
{ |
336 |
|
return d_subtheories[i]->collectModelValues(m, termSet); |
337 |
|
} |
338 |
|
} |
339 |
|
return true; |
340 |
|
} |
341 |
|
|
342 |
|
Node BVSolverLayered::getModelValue(TNode var) |
343 |
|
{ |
344 |
|
Assert(!inConflict()); |
345 |
|
for (unsigned i = 0; i < d_subtheories.size(); ++i) |
346 |
|
{ |
347 |
|
if (d_subtheories[i]->isComplete()) |
348 |
|
{ |
349 |
|
return d_subtheories[i]->getModelValue(var); |
350 |
|
} |
351 |
|
} |
352 |
|
Unreachable(); |
353 |
|
} |
354 |
|
|
355 |
|
void BVSolverLayered::propagate(Theory::Effort e) |
356 |
|
{ |
357 |
|
Debug("bitvector") << indent() << "BVSolverLayered::propagate()" << std::endl; |
358 |
|
if (options::bitblastMode() == options::BitblastMode::EAGER) |
359 |
|
{ |
360 |
|
return; |
361 |
|
} |
362 |
|
|
363 |
|
if (inConflict()) |
364 |
|
{ |
365 |
|
return; |
366 |
|
} |
367 |
|
|
368 |
|
// go through stored propagations |
369 |
|
bool ok = true; |
370 |
|
for (; d_literalsToPropagateIndex < d_literalsToPropagate.size() && ok; |
371 |
|
d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) |
372 |
|
{ |
373 |
|
TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex]; |
374 |
|
// temporary fix for incremental bit-blasting |
375 |
|
if (d_state.isSatLiteral(literal)) |
376 |
|
{ |
377 |
|
Debug("bitvector::propagate") |
378 |
|
<< "BVSolverLayered:: propagating " << literal << "\n"; |
379 |
|
ok = d_im.propagateLit(literal); |
380 |
|
} |
381 |
|
} |
382 |
|
|
383 |
|
if (!ok) |
384 |
|
{ |
385 |
|
Debug("bitvector::propagate") |
386 |
|
<< indent() |
387 |
|
<< "BVSolverLayered::propagate(): conflict from theory engine" |
388 |
|
<< std::endl; |
389 |
|
setConflict(); |
390 |
|
} |
391 |
|
} |
392 |
|
|
393 |
|
TrustNode BVSolverLayered::ppRewrite(TNode t) |
394 |
|
{ |
395 |
|
Debug("bv-pp-rewrite") << "BVSolverLayered::ppRewrite " << t << "\n"; |
396 |
|
Node res = t; |
397 |
|
if (options::bitwiseEq() && RewriteRule<BitwiseEq>::applies(t)) |
398 |
|
{ |
399 |
|
Node result = RewriteRule<BitwiseEq>::run<false>(t); |
400 |
|
res = Rewriter::rewrite(result); |
401 |
|
} |
402 |
|
else if (RewriteRule<UltAddOne>::applies(t)) |
403 |
|
{ |
404 |
|
Node result = RewriteRule<UltAddOne>::run<false>(t); |
405 |
|
res = Rewriter::rewrite(result); |
406 |
|
} |
407 |
|
else if (res.getKind() == kind::EQUAL |
408 |
|
&& ((res[0].getKind() == kind::BITVECTOR_ADD |
409 |
|
&& RewriteRule<ConcatToMult>::applies(res[1])) |
410 |
|
|| (res[1].getKind() == kind::BITVECTOR_ADD |
411 |
|
&& RewriteRule<ConcatToMult>::applies(res[0])))) |
412 |
|
{ |
413 |
|
Node mult = RewriteRule<ConcatToMult>::applies(res[0]) |
414 |
|
? RewriteRule<ConcatToMult>::run<false>(res[0]) |
415 |
|
: RewriteRule<ConcatToMult>::run<true>(res[1]); |
416 |
|
Node factor = mult[0]; |
417 |
|
Node sum = RewriteRule<ConcatToMult>::applies(res[0]) ? res[1] : res[0]; |
418 |
|
Node new_eq = NodeManager::currentNM()->mkNode(kind::EQUAL, sum, mult); |
419 |
|
Node rewr_eq = RewriteRule<SolveEq>::run<true>(new_eq); |
420 |
|
if (rewr_eq[0].isVar() || rewr_eq[1].isVar()) |
421 |
|
{ |
422 |
|
res = Rewriter::rewrite(rewr_eq); |
423 |
|
} |
424 |
|
else |
425 |
|
{ |
426 |
|
res = t; |
427 |
|
} |
428 |
|
} |
429 |
|
else if (RewriteRule<SignExtendEqConst>::applies(t)) |
430 |
|
{ |
431 |
|
res = RewriteRule<SignExtendEqConst>::run<false>(t); |
432 |
|
} |
433 |
|
else if (RewriteRule<ZeroExtendEqConst>::applies(t)) |
434 |
|
{ |
435 |
|
res = RewriteRule<ZeroExtendEqConst>::run<false>(t); |
436 |
|
} |
437 |
|
else if (RewriteRule<NormalizeEqAddNeg>::applies(t)) |
438 |
|
{ |
439 |
|
res = RewriteRule<NormalizeEqAddNeg>::run<false>(t); |
440 |
|
} |
441 |
|
|
442 |
|
// if(t.getKind() == kind::EQUAL && |
443 |
|
// ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() == |
444 |
|
// kind::BITVECTOR_ADD) || |
445 |
|
// (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() == |
446 |
|
// kind::BITVECTOR_ADD))) { |
447 |
|
// // if we have an equality between a multiplication and addition |
448 |
|
// // try to express multiplication in terms of addition |
449 |
|
// Node mult = t[0].getKind() == kind::BITVECTOR_MULT? t[0] : t[1]; |
450 |
|
// Node add = t[0].getKind() == kind::BITVECTOR_ADD? t[0] : t[1]; |
451 |
|
// if (RewriteRule<MultSlice>::applies(mult)) { |
452 |
|
// Node new_mult = RewriteRule<MultSlice>::run<false>(mult); |
453 |
|
// Node new_eq = |
454 |
|
// Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL, |
455 |
|
// new_mult, add)); |
456 |
|
|
457 |
|
// // the simplification can cause the formula to blow up |
458 |
|
// // only apply if formula reduced |
459 |
|
// if (d_subtheoryMap.find(SUB_BITBLAST) != d_subtheoryMap.end()) { |
460 |
|
// BitblastSolver* bv = (BitblastSolver*)d_subtheoryMap[SUB_BITBLAST]; |
461 |
|
// uint64_t old_size = bv->computeAtomWeight(t); |
462 |
|
// Assert (old_size); |
463 |
|
// uint64_t new_size = bv->computeAtomWeight(new_eq); |
464 |
|
// double ratio = ((double)new_size)/old_size; |
465 |
|
// if (ratio <= 0.4) { |
466 |
|
// ++(d_statistics.d_numMultSlice); |
467 |
|
// return new_eq; |
468 |
|
// } |
469 |
|
// } |
470 |
|
|
471 |
|
// if (new_eq.getKind() == kind::CONST_BOOLEAN) { |
472 |
|
// ++(d_statistics.d_numMultSlice); |
473 |
|
// return new_eq; |
474 |
|
// } |
475 |
|
// } |
476 |
|
// } |
477 |
|
|
478 |
|
if (options::bvAbstraction() && t.getType().isBoolean()) |
479 |
|
{ |
480 |
|
d_abstractionModule->addInputAtom(res); |
481 |
|
} |
482 |
|
Debug("bv-pp-rewrite") << "to " << res << "\n"; |
483 |
|
if (res != t) |
484 |
|
{ |
485 |
|
return TrustNode::mkTrustRewrite(t, res, nullptr); |
486 |
|
} |
487 |
|
return TrustNode::null(); |
488 |
|
} |
489 |
|
|
490 |
|
void BVSolverLayered::presolve() |
491 |
|
{ |
492 |
|
Debug("bitvector") << "BVSolverLayered::presolve" << std::endl; |
493 |
|
} |
494 |
|
|
495 |
|
static int prop_count = 0; |
496 |
|
|
497 |
|
bool BVSolverLayered::storePropagation(TNode literal, SubTheory subtheory) |
498 |
|
{ |
499 |
|
Debug("bitvector::propagate") |
500 |
|
<< indent() << d_context->getLevel() << " " |
501 |
|
<< "BVSolverLayered::storePropagation(" << literal << ", " << subtheory |
502 |
|
<< ")" << std::endl; |
503 |
|
prop_count++; |
504 |
|
|
505 |
|
// If already in conflict, no more propagation |
506 |
|
if (d_conflict) |
507 |
|
{ |
508 |
|
Debug("bitvector::propagate") |
509 |
|
<< indent() << "BVSolverLayered::storePropagation(" << literal << ", " |
510 |
|
<< subtheory << "): already in conflict" << std::endl; |
511 |
|
return false; |
512 |
|
} |
513 |
|
|
514 |
|
// If propagated already, just skip |
515 |
|
PropagatedMap::const_iterator find = d_propagatedBy.find(literal); |
516 |
|
if (find != d_propagatedBy.end()) |
517 |
|
{ |
518 |
|
return true; |
519 |
|
} |
520 |
|
else |
521 |
|
{ |
522 |
|
bool polarity = literal.getKind() != kind::NOT; |
523 |
|
Node negatedLiteral = polarity ? literal.notNode() : (Node)literal[0]; |
524 |
|
find = d_propagatedBy.find(negatedLiteral); |
525 |
|
if (find != d_propagatedBy.end() && (*find).second != subtheory) |
526 |
|
{ |
527 |
|
// Safe to ignore this one, subtheory should produce a conflict |
528 |
|
return true; |
529 |
|
} |
530 |
|
|
531 |
|
d_propagatedBy[literal] = subtheory; |
532 |
|
} |
533 |
|
|
534 |
|
// Propagate differs depending on the subtheory |
535 |
|
// * bitblaster needs to be left alone until it's done, otherwise it doesn't |
536 |
|
// know how to explain |
537 |
|
// * equality engine can propagate eagerly |
538 |
|
// TODO(2348): Determine if ok should be set by propagate. If not, remove ok. |
539 |
|
constexpr bool ok = true; |
540 |
|
if (subtheory == SUB_CORE) |
541 |
|
{ |
542 |
|
d_im.propagateLit(literal); |
543 |
|
if (!ok) |
544 |
|
{ |
545 |
|
setConflict(); |
546 |
|
} |
547 |
|
} |
548 |
|
else |
549 |
|
{ |
550 |
|
d_literalsToPropagate.push_back(literal); |
551 |
|
} |
552 |
|
return ok; |
553 |
|
|
554 |
|
} /* BVSolverLayered::propagate(TNode) */ |
555 |
|
|
556 |
|
void BVSolverLayered::explain(TNode literal, std::vector<TNode>& assumptions) |
557 |
|
{ |
558 |
|
Assert(wasPropagatedBySubtheory(literal)); |
559 |
|
SubTheory sub = getPropagatingSubtheory(literal); |
560 |
|
d_subtheoryMap[sub]->explain(literal, assumptions); |
561 |
|
} |
562 |
|
|
563 |
|
TrustNode BVSolverLayered::explain(TNode node) |
564 |
|
{ |
565 |
|
Debug("bitvector::explain") |
566 |
|
<< "BVSolverLayered::explain(" << node << ")" << std::endl; |
567 |
|
std::vector<TNode> assumptions; |
568 |
|
|
569 |
|
// Ask for the explanation |
570 |
|
explain(node, assumptions); |
571 |
|
// this means that it is something true at level 0 |
572 |
|
Node explanation; |
573 |
|
if (assumptions.size() == 0) |
574 |
|
{ |
575 |
|
explanation = utils::mkTrue(); |
576 |
|
} |
577 |
|
else |
578 |
|
{ |
579 |
|
// return the explanation |
580 |
|
explanation = utils::mkAnd(assumptions); |
581 |
|
} |
582 |
|
Debug("bitvector::explain") << "BVSolverLayered::explain(" << node << ") => " |
583 |
|
<< explanation << std::endl; |
584 |
|
Debug("bitvector::explain") << "BVSolverLayered::explain done. \n"; |
585 |
|
return TrustNode::mkTrustPropExp(node, explanation, nullptr); |
586 |
|
} |
587 |
|
|
588 |
|
void BVSolverLayered::notifySharedTerm(TNode t) |
589 |
|
{ |
590 |
|
Debug("bitvector::sharing") |
591 |
|
<< indent() << "BVSolverLayered::notifySharedTerm(" << t << ")" |
592 |
|
<< std::endl; |
593 |
|
d_sharedTermsSet.insert(t); |
594 |
|
} |
595 |
|
|
596 |
|
EqualityStatus BVSolverLayered::getEqualityStatus(TNode a, TNode b) |
597 |
|
{ |
598 |
|
if (options::bitblastMode() == options::BitblastMode::EAGER) |
599 |
|
return EQUALITY_UNKNOWN; |
600 |
|
Assert(options::bitblastMode() == options::BitblastMode::LAZY); |
601 |
|
for (unsigned i = 0; i < d_subtheories.size(); ++i) |
602 |
|
{ |
603 |
|
EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b); |
604 |
|
if (status != EQUALITY_UNKNOWN) |
605 |
|
{ |
606 |
|
return status; |
607 |
|
} |
608 |
|
} |
609 |
|
return EQUALITY_UNKNOWN; |
610 |
|
; |
611 |
|
} |
612 |
|
|
613 |
|
void BVSolverLayered::ppStaticLearn(TNode in, NodeBuilder& learned) |
614 |
|
{ |
615 |
|
if (d_staticLearnCache.find(in) != d_staticLearnCache.end()) |
616 |
|
{ |
617 |
|
return; |
618 |
|
} |
619 |
|
d_staticLearnCache.insert(in); |
620 |
|
|
621 |
|
if (in.getKind() == kind::EQUAL) |
622 |
|
{ |
623 |
|
if ((in[0].getKind() == kind::BITVECTOR_ADD |
624 |
|
&& in[1].getKind() == kind::BITVECTOR_SHL) |
625 |
|
|| (in[1].getKind() == kind::BITVECTOR_ADD |
626 |
|
&& in[0].getKind() == kind::BITVECTOR_SHL)) |
627 |
|
{ |
628 |
|
TNode p = in[0].getKind() == kind::BITVECTOR_ADD ? in[0] : in[1]; |
629 |
|
TNode s = in[0].getKind() == kind::BITVECTOR_ADD ? in[1] : in[0]; |
630 |
|
|
631 |
|
if (p.getNumChildren() == 2 && p[0].getKind() == kind::BITVECTOR_SHL |
632 |
|
&& p[1].getKind() == kind::BITVECTOR_SHL) |
633 |
|
{ |
634 |
|
unsigned size = utils::getSize(s); |
635 |
|
Node one = utils::mkConst(size, 1u); |
636 |
|
if (s[0] == one && p[0][0] == one && p[1][0] == one) |
637 |
|
{ |
638 |
|
Node zero = utils::mkConst(size, 0u); |
639 |
|
TNode b = p[0]; |
640 |
|
TNode c = p[1]; |
641 |
|
// (s : 1 << S) = (b : 1 << B) + (c : 1 << C) |
642 |
|
Node b_eq_0 = b.eqNode(zero); |
643 |
|
Node c_eq_0 = c.eqNode(zero); |
644 |
|
Node b_eq_c = b.eqNode(c); |
645 |
|
|
646 |
|
Node dis = NodeManager::currentNM()->mkNode( |
647 |
|
kind::OR, b_eq_0, c_eq_0, b_eq_c); |
648 |
|
Node imp = in.impNode(dis); |
649 |
|
learned << imp; |
650 |
|
} |
651 |
|
} |
652 |
|
} |
653 |
|
} |
654 |
|
else if (in.getKind() == kind::AND) |
655 |
|
{ |
656 |
|
for (size_t i = 0, N = in.getNumChildren(); i < N; ++i) |
657 |
|
{ |
658 |
|
ppStaticLearn(in[i], learned); |
659 |
|
} |
660 |
|
} |
661 |
|
} |
662 |
|
|
663 |
|
bool BVSolverLayered::applyAbstraction(const std::vector<Node>& assertions, |
664 |
|
std::vector<Node>& new_assertions) |
665 |
|
{ |
666 |
|
bool changed = |
667 |
|
d_abstractionModule->applyAbstraction(assertions, new_assertions); |
668 |
|
if (changed && options::bitblastMode() == options::BitblastMode::EAGER |
669 |
|
&& options::bitvectorAig()) |
670 |
|
{ |
671 |
|
// disable AIG mode |
672 |
|
AlwaysAssert(!d_eagerSolver->isInitialized()); |
673 |
|
d_eagerSolver->turnOffAig(); |
674 |
|
d_eagerSolver->initialize(); |
675 |
|
} |
676 |
|
return changed; |
677 |
|
} |
678 |
|
|
679 |
|
void BVSolverLayered::setConflict(Node conflict) |
680 |
|
{ |
681 |
|
if (options::bvAbstraction()) |
682 |
|
{ |
683 |
|
NodeManager* const nm = NodeManager::currentNM(); |
684 |
|
Node new_conflict = d_abstractionModule->simplifyConflict(conflict); |
685 |
|
|
686 |
|
std::vector<Node> lemmas; |
687 |
|
lemmas.push_back(new_conflict); |
688 |
|
d_abstractionModule->generalizeConflict(new_conflict, lemmas); |
689 |
|
for (unsigned i = 0; i < lemmas.size(); ++i) |
690 |
|
{ |
691 |
|
lemma(nm->mkNode(kind::NOT, lemmas[i])); |
692 |
|
} |
693 |
|
} |
694 |
|
d_conflict = true; |
695 |
|
d_conflictNode = conflict; |
696 |
|
} |
697 |
|
|
698 |
|
} // namespace bv |
699 |
|
} // namespace theory |
700 |
29322 |
} // namespace cvc5 |