Initial work towards -Wshadow (#3817)
[cvc5.git] / src / theory / bv / theory_bv.cpp
1 /********************* */
2 /*! \file theory_bv.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Liana Hadarean, Andrew Reynolds, Aina Niemetz
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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 ** [[ Add lengthier description here ]]
13 ** \todo document this file
14 **/
15
16 #include "theory/bv/theory_bv.h"
17
18 #include "expr/node_algorithm.h"
19 #include "options/bv_options.h"
20 #include "options/smt_options.h"
21 #include "proof/proof_manager.h"
22 #include "proof/theory_proof.h"
23 #include "smt/smt_statistics_registry.h"
24 #include "theory/bv/abstraction.h"
25 #include "theory/bv/bv_eager_solver.h"
26 #include "theory/bv/bv_subtheory_algebraic.h"
27 #include "theory/bv/bv_subtheory_bitblast.h"
28 #include "theory/bv/bv_subtheory_core.h"
29 #include "theory/bv/bv_subtheory_inequality.h"
30 #include "theory/bv/slicer.h"
31 #include "theory/bv/theory_bv_rewrite_rules_normalization.h"
32 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
33 #include "theory/bv/theory_bv_rewriter.h"
34 #include "theory/bv/theory_bv_utils.h"
35 #include "theory/ext_theory.h"
36 #include "theory/theory_model.h"
37 #include "theory/valuation.h"
38
39 using namespace CVC4::context;
40 using namespace CVC4::theory::bv::utils;
41 using namespace std;
42
43 namespace CVC4 {
44 namespace theory {
45 namespace bv {
46
47 TheoryBV::TheoryBV(context::Context* c,
48 context::UserContext* u,
49 OutputChannel& out,
50 Valuation valuation,
51 const LogicInfo& logicInfo,
52 std::string name)
53 : Theory(THEORY_BV, c, u, out, valuation, logicInfo, name),
54 d_context(c),
55 d_alreadyPropagatedSet(c),
56 d_sharedTermsSet(c),
57 d_subtheories(),
58 d_subtheoryMap(),
59 d_statistics(),
60 d_staticLearnCache(),
61 d_BVDivByZero(),
62 d_BVRemByZero(),
63 d_lemmasAdded(c, false),
64 d_conflict(c, false),
65 d_invalidateModelCache(c, true),
66 d_literalsToPropagate(c),
67 d_literalsToPropagateIndex(c, 0),
68 d_propagatedBy(c),
69 d_eagerSolver(),
70 d_abstractionModule(new AbstractionModule(getStatsPrefix(THEORY_BV))),
71 d_isCoreTheory(false),
72 d_calledPreregister(false),
73 d_needsLastCallCheck(false),
74 d_extf_range_infer(u),
75 d_extf_collapse_infer(u)
76 {
77 setupExtTheory();
78 getExtTheory()->addFunctionKind(kind::BITVECTOR_TO_NAT);
79 getExtTheory()->addFunctionKind(kind::INT_TO_BITVECTOR);
80 if (options::bitblastMode() == options::BitblastMode::EAGER)
81 {
82 d_eagerSolver.reset(new EagerBitblastSolver(c, this));
83 return;
84 }
85
86 if (options::bitvectorEqualitySolver() && !options::proof())
87 {
88 d_subtheories.emplace_back(new CoreSolver(c, this));
89 d_subtheoryMap[SUB_CORE] = d_subtheories.back().get();
90 }
91
92 if (options::bitvectorInequalitySolver() && !options::proof())
93 {
94 d_subtheories.emplace_back(new InequalitySolver(c, u, this));
95 d_subtheoryMap[SUB_INEQUALITY] = d_subtheories.back().get();
96 }
97
98 if (options::bitvectorAlgebraicSolver() && !options::proof())
99 {
100 d_subtheories.emplace_back(new AlgebraicSolver(c, this));
101 d_subtheoryMap[SUB_ALGEBRAIC] = d_subtheories.back().get();
102 }
103
104 BitblastSolver* bb_solver = new BitblastSolver(c, this);
105 if (options::bvAbstraction())
106 {
107 bb_solver->setAbstraction(d_abstractionModule.get());
108 }
109 d_subtheories.emplace_back(bb_solver);
110 d_subtheoryMap[SUB_BITBLAST] = bb_solver;
111 }
112
113 TheoryBV::~TheoryBV() {}
114
115 void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
116 if (options::bitblastMode() == options::BitblastMode::EAGER)
117 {
118 return;
119 }
120 if (options::bitvectorEqualitySolver()) {
121 dynamic_cast<CoreSolver*>(d_subtheoryMap[SUB_CORE])->setMasterEqualityEngine(eq);
122 }
123 }
124
125 void TheoryBV::spendResource(ResourceManager::Resource r)
126 {
127 getOutputChannel().spendResource(r);
128 }
129
130 TheoryBV::Statistics::Statistics():
131 d_avgConflictSize("theory::bv::AvgBVConflictSize"),
132 d_solveSubstitutions("theory::bv::NumSolveSubstitutions", 0),
133 d_solveTimer("theory::bv::solveTimer"),
134 d_numCallsToCheckFullEffort("theory::bv::NumFullCheckCalls", 0),
135 d_numCallsToCheckStandardEffort("theory::bv::NumStandardCheckCalls", 0),
136 d_weightComputationTimer("theory::bv::weightComputationTimer"),
137 d_numMultSlice("theory::bv::NumMultSliceApplied", 0)
138 {
139 smtStatisticsRegistry()->registerStat(&d_avgConflictSize);
140 smtStatisticsRegistry()->registerStat(&d_solveSubstitutions);
141 smtStatisticsRegistry()->registerStat(&d_solveTimer);
142 smtStatisticsRegistry()->registerStat(&d_numCallsToCheckFullEffort);
143 smtStatisticsRegistry()->registerStat(&d_numCallsToCheckStandardEffort);
144 smtStatisticsRegistry()->registerStat(&d_weightComputationTimer);
145 smtStatisticsRegistry()->registerStat(&d_numMultSlice);
146 }
147
148 TheoryBV::Statistics::~Statistics() {
149 smtStatisticsRegistry()->unregisterStat(&d_avgConflictSize);
150 smtStatisticsRegistry()->unregisterStat(&d_solveSubstitutions);
151 smtStatisticsRegistry()->unregisterStat(&d_solveTimer);
152 smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckFullEffort);
153 smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckStandardEffort);
154 smtStatisticsRegistry()->unregisterStat(&d_weightComputationTimer);
155 smtStatisticsRegistry()->unregisterStat(&d_numMultSlice);
156 }
157
158 Node TheoryBV::getBVDivByZero(Kind k, unsigned width) {
159 NodeManager* nm = NodeManager::currentNM();
160 if (k == kind::BITVECTOR_UDIV) {
161 if (d_BVDivByZero.find(width) == d_BVDivByZero.end()) {
162 // lazily create the function symbols
163 ostringstream os;
164 os << "BVUDivByZero_" << width;
165 Node divByZero = nm->mkSkolem(os.str(),
166 nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)),
167 "partial bvudiv", NodeManager::SKOLEM_EXACT_NAME);
168 d_BVDivByZero[width] = divByZero;
169 }
170 return d_BVDivByZero[width];
171 }
172 else if (k == kind::BITVECTOR_UREM) {
173 if (d_BVRemByZero.find(width) == d_BVRemByZero.end()) {
174 ostringstream os;
175 os << "BVURemByZero_" << width;
176 Node divByZero = nm->mkSkolem(os.str(),
177 nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)),
178 "partial bvurem", NodeManager::SKOLEM_EXACT_NAME);
179 d_BVRemByZero[width] = divByZero;
180 }
181 return d_BVRemByZero[width];
182 }
183
184 Unreachable();
185 }
186
187 void TheoryBV::finishInit()
188 {
189 // these kinds are semi-evaluated in getModelValue (applications of this
190 // kind are treated as variables)
191 TheoryModel* tm = d_valuation.getModel();
192 Assert(tm != nullptr);
193 tm->setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UDIV);
194 tm->setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM);
195 }
196
197 Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) {
198 Debug("bitvector-expandDefinition") << "TheoryBV::expandDefinition(" << node << ")" << std::endl;
199
200 switch (node.getKind()) {
201 case kind::BITVECTOR_SDIV:
202 case kind::BITVECTOR_SREM:
203 case kind::BITVECTOR_SMOD:
204 return TheoryBVRewriter::eliminateBVSDiv(node);
205 break;
206
207 case kind::BITVECTOR_UDIV:
208 case kind::BITVECTOR_UREM: {
209 NodeManager* nm = NodeManager::currentNM();
210 unsigned width = node.getType().getBitVectorSize();
211
212 if (options::bitvectorDivByZeroConst()) {
213 Kind kind = node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL : kind::BITVECTOR_UREM_TOTAL;
214 return nm->mkNode(kind, node[0], node[1]);
215 }
216
217 TNode num = node[0], den = node[1];
218 Node den_eq_0 = nm->mkNode(kind::EQUAL, den, utils::mkZero(width));
219 Node divTotalNumDen = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL :
220 kind::BITVECTOR_UREM_TOTAL, num, den);
221 Node divByZero = getBVDivByZero(node.getKind(), width);
222 Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num);
223 node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen);
224 logicRequest.widenLogic(THEORY_UF);
225 return node;
226 }
227 break;
228
229 default:
230 return node;
231 break;
232 }
233
234 Unreachable();
235 }
236
237
238 void TheoryBV::preRegisterTerm(TNode node) {
239 d_calledPreregister = true;
240 Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
241
242 if (options::bitblastMode() == options::BitblastMode::EAGER)
243 {
244 // the aig bit-blaster option is set heuristically
245 // if bv abstraction is used
246 if (!d_eagerSolver->isInitialized())
247 {
248 d_eagerSolver->initialize();
249 }
250
251 if (node.getKind() == kind::BITVECTOR_EAGER_ATOM)
252 {
253 Node formula = node[0];
254 d_eagerSolver->assertFormula(formula);
255 }
256 return;
257 }
258
259 for (unsigned i = 0; i < d_subtheories.size(); ++i) {
260 d_subtheories[i]->preRegister(node);
261 }
262
263 // AJR : equality solver currently registers all terms to ExtTheory, if we want a lazy reduction without the bv equality solver, need to call this
264 //getExtTheory()->registerTermRec( node );
265 }
266
267 void TheoryBV::sendConflict() {
268 Assert(d_conflict);
269 if (d_conflictNode.isNull()) {
270 return;
271 } else {
272 Debug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode << std::endl;
273 d_out->conflict(d_conflictNode);
274 d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren());
275 d_conflictNode = Node::null();
276 }
277 }
278
279 void TheoryBV::checkForLemma(TNode fact)
280 {
281 if (fact.getKind() == kind::EQUAL)
282 {
283 NodeManager* nm = NodeManager::currentNM();
284 if (fact[0].getKind() == kind::BITVECTOR_UREM_TOTAL)
285 {
286 TNode urem = fact[0];
287 TNode result = fact[1];
288 TNode divisor = urem[1];
289 Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor);
290 Node divisor_eq_0 =
291 nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor)));
292 Node split = nm->mkNode(
293 kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div);
294 lemma(split);
295 }
296 if (fact[1].getKind() == kind::BITVECTOR_UREM_TOTAL)
297 {
298 TNode urem = fact[1];
299 TNode result = fact[0];
300 TNode divisor = urem[1];
301 Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor);
302 Node divisor_eq_0 =
303 nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor)));
304 Node split = nm->mkNode(
305 kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div);
306 lemma(split);
307 }
308 }
309 }
310
311 void TheoryBV::check(Effort e)
312 {
313 if (done() && e<Theory::EFFORT_FULL) {
314 return;
315 }
316
317 //last call : do reductions on extended bitvector functions
318 if (e == Theory::EFFORT_LAST_CALL) {
319 std::vector<Node> nred = getExtTheory()->getActive();
320 doExtfReductions(nred);
321 return;
322 }
323
324 TimerStat::CodeTimer checkTimer(d_checkTime);
325 Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
326 TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer);
327 // we may be getting new assertions so the model cache may not be sound
328 d_invalidateModelCache.set(true);
329 // if we are using the eager solver
330 if (options::bitblastMode() == options::BitblastMode::EAGER)
331 {
332 // this can only happen on an empty benchmark
333 if (!d_eagerSolver->isInitialized()) {
334 d_eagerSolver->initialize();
335 }
336 if (!Theory::fullEffort(e))
337 return;
338
339 std::vector<TNode> assertions;
340 while (!done()) {
341 TNode fact = get().d_assertion;
342 Assert(fact.getKind() == kind::BITVECTOR_EAGER_ATOM);
343 assertions.push_back(fact);
344 d_eagerSolver->assertFormula(fact[0]);
345 }
346
347 bool ok = d_eagerSolver->checkSat();
348 if (!ok) {
349 if (assertions.size() == 1) {
350 d_out->conflict(assertions[0]);
351 return;
352 }
353 Node conflict = utils::mkAnd(assertions);
354 d_out->conflict(conflict);
355 return;
356 }
357 return;
358 }
359
360 if (Theory::fullEffort(e)) {
361 ++(d_statistics.d_numCallsToCheckFullEffort);
362 } else {
363 ++(d_statistics.d_numCallsToCheckStandardEffort);
364 }
365 // if we are already in conflict just return the conflict
366 if (inConflict()) {
367 sendConflict();
368 return;
369 }
370
371 while (!done()) {
372 TNode fact = get().d_assertion;
373
374 checkForLemma(fact);
375
376 for (unsigned i = 0; i < d_subtheories.size(); ++i) {
377 d_subtheories[i]->assertFact(fact);
378 }
379 }
380
381 bool ok = true;
382 bool complete = false;
383 for (unsigned i = 0; i < d_subtheories.size(); ++i) {
384 Assert(!inConflict());
385 ok = d_subtheories[i]->check(e);
386 complete = d_subtheories[i]->isComplete();
387
388 if (!ok) {
389 // if we are in a conflict no need to check with other theories
390 Assert(inConflict());
391 sendConflict();
392 return;
393 }
394 if (complete) {
395 // if the last subtheory was complete we stop
396 break;
397 }
398 }
399
400 //check extended functions
401 if (Theory::fullEffort(e)) {
402 //do inferences (adds external lemmas) TODO: this can be improved to add internal inferences
403 std::vector< Node > nred;
404 if( getExtTheory()->doInferences( 0, nred ) ){
405 return;
406 }
407 d_needsLastCallCheck = false;
408 if( !nred.empty() ){
409 //other inferences involving bv2nat, int2bv
410 if( options::bvAlgExtf() ){
411 if( doExtfInferences( nred ) ){
412 return;
413 }
414 }
415 if( !options::bvLazyReduceExtf() ){
416 if( doExtfReductions( nred ) ){
417 return;
418 }
419 }else{
420 d_needsLastCallCheck = true;
421 }
422 }
423 }
424 }
425
426 bool TheoryBV::doExtfInferences(std::vector<Node>& terms)
427 {
428 NodeManager* nm = NodeManager::currentNM();
429 bool sentLemma = false;
430 eq::EqualityEngine* ee = getEqualityEngine();
431 std::map<Node, Node> op_map;
432 for (unsigned j = 0; j < terms.size(); j++)
433 {
434 TNode n = terms[j];
435 Assert(n.getKind() == kind::BITVECTOR_TO_NAT
436 || n.getKind() == kind::INT_TO_BITVECTOR);
437 if (n.getKind() == kind::BITVECTOR_TO_NAT)
438 {
439 // range lemmas
440 if (d_extf_range_infer.find(n) == d_extf_range_infer.end())
441 {
442 d_extf_range_infer.insert(n);
443 unsigned bvs = n[0].getType().getBitVectorSize();
444 Node min = nm->mkConst(Rational(0));
445 Node max = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs)));
446 Node lem = nm->mkNode(kind::AND,
447 nm->mkNode(kind::GEQ, n, min),
448 nm->mkNode(kind::LT, n, max));
449 Trace("bv-extf-lemma")
450 << "BV extf lemma (range) : " << lem << std::endl;
451 d_out->lemma(lem);
452 sentLemma = true;
453 }
454 }
455 Node r = (ee && ee->hasTerm(n[0])) ? ee->getRepresentative(n[0]) : n[0];
456 op_map[r] = n;
457 }
458 for (unsigned j = 0; j < terms.size(); j++)
459 {
460 TNode n = terms[j];
461 Node r = (ee && ee->hasTerm(n[0])) ? ee->getRepresentative(n) : n;
462 std::map<Node, Node>::iterator it = op_map.find(r);
463 if (it != op_map.end())
464 {
465 Node parent = it->second;
466 // Node cterm = parent[0]==n ? parent : nm->mkNode( parent.getOperator(),
467 // n );
468 Node cterm = parent[0].eqNode(n);
469 Trace("bv-extf-lemma-debug")
470 << "BV extf collapse based on : " << cterm << std::endl;
471 if (d_extf_collapse_infer.find(cterm) == d_extf_collapse_infer.end())
472 {
473 d_extf_collapse_infer.insert(cterm);
474
475 Node t = n[0];
476 if (t.getType() == parent.getType())
477 {
478 if (n.getKind() == kind::INT_TO_BITVECTOR)
479 {
480 Assert(t.getType().isInteger());
481 // congruent modulo 2^( bv width )
482 unsigned bvs = n.getType().getBitVectorSize();
483 Node coeff = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs)));
484 Node k = nm->mkSkolem(
485 "int_bv_cong", t.getType(), "for int2bv/bv2nat congruence");
486 t = nm->mkNode(kind::PLUS, t, nm->mkNode(kind::MULT, coeff, k));
487 }
488 Node lem = parent.eqNode(t);
489
490 if (parent[0] != n)
491 {
492 Assert(ee->areEqual(parent[0], n));
493 lem = nm->mkNode(kind::IMPLIES, parent[0].eqNode(n), lem);
494 }
495 // this handles inferences of the form, e.g.:
496 // ((_ int2bv w) (bv2nat x)) == x (if x is bit-width w)
497 // (bv2nat ((_ int2bv w) x)) == x + k*2^w for some k
498 Trace("bv-extf-lemma")
499 << "BV extf lemma (collapse) : " << lem << std::endl;
500 d_out->lemma(lem);
501 sentLemma = true;
502 }
503 }
504 Trace("bv-extf-lemma-debug")
505 << "BV extf f collapse based on : " << cterm << std::endl;
506 }
507 }
508 return sentLemma;
509 }
510
511 bool TheoryBV::doExtfReductions( std::vector< Node >& terms ) {
512 std::vector< Node > nredr;
513 if( getExtTheory()->doReductions( 0, terms, nredr ) ){
514 return true;
515 }
516 Assert(nredr.empty());
517 return false;
518 }
519
520 bool TheoryBV::needsCheckLastEffort() {
521 return d_needsLastCallCheck;
522 }
523 bool TheoryBV::collectModelInfo(TheoryModel* m)
524 {
525 Assert(!inConflict());
526 if (options::bitblastMode() == options::BitblastMode::EAGER)
527 {
528 if (!d_eagerSolver->collectModelInfo(m, true))
529 {
530 return false;
531 }
532 }
533 for (unsigned i = 0; i < d_subtheories.size(); ++i) {
534 if (d_subtheories[i]->isComplete()) {
535 return d_subtheories[i]->collectModelInfo(m, true);
536 }
537 }
538 return true;
539 }
540
541 Node TheoryBV::getModelValue(TNode var) {
542 Assert(!inConflict());
543 for (unsigned i = 0; i < d_subtheories.size(); ++i) {
544 if (d_subtheories[i]->isComplete()) {
545 return d_subtheories[i]->getModelValue(var);
546 }
547 }
548 Unreachable();
549 }
550
551 void TheoryBV::propagate(Effort e) {
552 Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl;
553 if (options::bitblastMode() == options::BitblastMode::EAGER)
554 {
555 return;
556 }
557
558 if (inConflict()) {
559 return;
560 }
561
562 // go through stored propagations
563 bool ok = true;
564 for (; d_literalsToPropagateIndex < d_literalsToPropagate.size() && ok; d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
565 TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
566 // temporary fix for incremental bit-blasting
567 if (d_valuation.isSatLiteral(literal)) {
568 Debug("bitvector::propagate") << "TheoryBV:: propagating " << literal <<"\n";
569 ok = d_out->propagate(literal);
570 }
571 }
572
573 if (!ok) {
574 Debug("bitvector::propagate") << indent() << "TheoryBV::propagate(): conflict from theory engine" << std::endl;
575 setConflict();
576 }
577 }
578
579
580 eq::EqualityEngine * TheoryBV::getEqualityEngine() {
581 CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
582 if( core ){
583 return core->getEqualityEngine();
584 }else{
585 return NULL;
586 }
587 }
588
589 bool TheoryBV::getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) {
590 eq::EqualityEngine * ee = getEqualityEngine();
591 if( ee ){
592 //get the constant equivalence classes
593 bool retVal = false;
594 for( unsigned i=0; i<vars.size(); i++ ){
595 Node n = vars[i];
596 if( ee->hasTerm( n ) ){
597 Node nr = ee->getRepresentative( n );
598 if( nr.isConst() ){
599 subs.push_back( nr );
600 exp[n].push_back( n.eqNode( nr ) );
601 retVal = true;
602 }else{
603 subs.push_back( n );
604 }
605 }else{
606 subs.push_back( n );
607 }
608 }
609 //return true if the substitution is non-trivial
610 return retVal;
611 }
612 return false;
613 }
614
615 int TheoryBV::getReduction(int effort, Node n, Node& nr)
616 {
617 Trace("bv-ext") << "TheoryBV::checkExt : non-reduced : " << n << std::endl;
618 if (n.getKind() == kind::BITVECTOR_TO_NAT)
619 {
620 nr = utils::eliminateBv2Nat(n);
621 return -1;
622 }
623 else if (n.getKind() == kind::INT_TO_BITVECTOR)
624 {
625 nr = utils::eliminateInt2Bv(n);
626 return -1;
627 }
628 return 0;
629 }
630
631 Theory::PPAssertStatus TheoryBV::ppAssert(TNode in,
632 SubstitutionMap& outSubstitutions)
633 {
634 switch (in.getKind())
635 {
636 case kind::EQUAL:
637 {
638 if (in[0].isVar() && !expr::hasSubterm(in[1], in[0]))
639 {
640 ++(d_statistics.d_solveSubstitutions);
641 outSubstitutions.addSubstitution(in[0], in[1]);
642 return PP_ASSERT_STATUS_SOLVED;
643 }
644 if (in[1].isVar() && !expr::hasSubterm(in[0], in[1]))
645 {
646 ++(d_statistics.d_solveSubstitutions);
647 outSubstitutions.addSubstitution(in[1], in[0]);
648 return PP_ASSERT_STATUS_SOLVED;
649 }
650 Node node = Rewriter::rewrite(in);
651 if ((node[0].getKind() == kind::BITVECTOR_EXTRACT && node[1].isConst())
652 || (node[1].getKind() == kind::BITVECTOR_EXTRACT
653 && node[0].isConst()))
654 {
655 Node extract = node[0].isConst() ? node[1] : node[0];
656 if (extract[0].getKind() == kind::VARIABLE)
657 {
658 Node c = node[0].isConst() ? node[0] : node[1];
659
660 unsigned high = utils::getExtractHigh(extract);
661 unsigned low = utils::getExtractLow(extract);
662 unsigned var_bitwidth = utils::getSize(extract[0]);
663 std::vector<Node> children;
664
665 if (low == 0)
666 {
667 Assert(high != var_bitwidth - 1);
668 unsigned skolem_size = var_bitwidth - high - 1;
669 Node skolem = utils::mkVar(skolem_size);
670 children.push_back(skolem);
671 children.push_back(c);
672 }
673 else if (high == var_bitwidth - 1)
674 {
675 unsigned skolem_size = low;
676 Node skolem = utils::mkVar(skolem_size);
677 children.push_back(c);
678 children.push_back(skolem);
679 }
680 else
681 {
682 unsigned skolem1_size = low;
683 unsigned skolem2_size = var_bitwidth - high - 1;
684 Node skolem1 = utils::mkVar(skolem1_size);
685 Node skolem2 = utils::mkVar(skolem2_size);
686 children.push_back(skolem2);
687 children.push_back(c);
688 children.push_back(skolem1);
689 }
690 Node concat = utils::mkConcat(children);
691 Assert(utils::getSize(concat) == utils::getSize(extract[0]));
692 outSubstitutions.addSubstitution(extract[0], concat);
693 return PP_ASSERT_STATUS_SOLVED;
694 }
695 }
696 }
697 break;
698 case kind::BITVECTOR_ULT:
699 case kind::BITVECTOR_SLT:
700 case kind::BITVECTOR_ULE:
701 case kind::BITVECTOR_SLE:
702
703 default:
704 // TODO other predicates
705 break;
706 }
707 return PP_ASSERT_STATUS_UNSOLVED;
708 }
709
710 Node TheoryBV::ppRewrite(TNode t)
711 {
712 Debug("bv-pp-rewrite") << "TheoryBV::ppRewrite " << t << "\n";
713 Node res = t;
714 if (options::bitwiseEq() && RewriteRule<BitwiseEq>::applies(t)) {
715 Node result = RewriteRule<BitwiseEq>::run<false>(t);
716 res = Rewriter::rewrite(result);
717 } else if (d_isCoreTheory && t.getKind() == kind::EQUAL) {
718 std::vector<Node> equalities;
719 Slicer::splitEqualities(t, equalities);
720 res = utils::mkAnd(equalities);
721 } else if (RewriteRule<UltPlusOne>::applies(t)) {
722 Node result = RewriteRule<UltPlusOne>::run<false>(t);
723 res = Rewriter::rewrite(result);
724 } else if( res.getKind() == kind::EQUAL &&
725 ((res[0].getKind() == kind::BITVECTOR_PLUS &&
726 RewriteRule<ConcatToMult>::applies(res[1])) ||
727 (res[1].getKind() == kind::BITVECTOR_PLUS &&
728 RewriteRule<ConcatToMult>::applies(res[0])))) {
729 Node mult = RewriteRule<ConcatToMult>::applies(res[0])?
730 RewriteRule<ConcatToMult>::run<false>(res[0]) :
731 RewriteRule<ConcatToMult>::run<true>(res[1]);
732 Node factor = mult[0];
733 Node sum = RewriteRule<ConcatToMult>::applies(res[0])? res[1] : res[0];
734 Node new_eq = NodeManager::currentNM()->mkNode(kind::EQUAL, sum, mult);
735 Node rewr_eq = RewriteRule<SolveEq>::run<true>(new_eq);
736 if (rewr_eq[0].isVar() || rewr_eq[1].isVar()){
737 res = Rewriter::rewrite(rewr_eq);
738 } else {
739 res = t;
740 }
741 } else if (RewriteRule<SignExtendEqConst>::applies(t)) {
742 res = RewriteRule<SignExtendEqConst>::run<false>(t);
743 } else if (RewriteRule<ZeroExtendEqConst>::applies(t)) {
744 res = RewriteRule<ZeroExtendEqConst>::run<false>(t);
745 }
746 else if (RewriteRule<NormalizeEqPlusNeg>::applies(t))
747 {
748 res = RewriteRule<NormalizeEqPlusNeg>::run<false>(t);
749 }
750
751 // if(t.getKind() == kind::EQUAL &&
752 // ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() ==
753 // kind::BITVECTOR_PLUS) ||
754 // (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() ==
755 // kind::BITVECTOR_PLUS))) {
756 // // if we have an equality between a multiplication and addition
757 // // try to express multiplication in terms of addition
758 // Node mult = t[0].getKind() == kind::BITVECTOR_MULT? t[0] : t[1];
759 // Node add = t[0].getKind() == kind::BITVECTOR_PLUS? t[0] : t[1];
760 // if (RewriteRule<MultSlice>::applies(mult)) {
761 // Node new_mult = RewriteRule<MultSlice>::run<false>(mult);
762 // Node new_eq =
763 // Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL,
764 // new_mult, add));
765
766 // // the simplification can cause the formula to blow up
767 // // only apply if formula reduced
768 // if (d_subtheoryMap.find(SUB_BITBLAST) != d_subtheoryMap.end()) {
769 // BitblastSolver* bv = (BitblastSolver*)d_subtheoryMap[SUB_BITBLAST];
770 // uint64_t old_size = bv->computeAtomWeight(t);
771 // Assert (old_size);
772 // uint64_t new_size = bv->computeAtomWeight(new_eq);
773 // double ratio = ((double)new_size)/old_size;
774 // if (ratio <= 0.4) {
775 // ++(d_statistics.d_numMultSlice);
776 // return new_eq;
777 // }
778 // }
779
780 // if (new_eq.getKind() == kind::CONST_BOOLEAN) {
781 // ++(d_statistics.d_numMultSlice);
782 // return new_eq;
783 // }
784 // }
785 // }
786
787 if (options::bvAbstraction() && t.getType().isBoolean()) {
788 d_abstractionModule->addInputAtom(res);
789 }
790 Debug("bv-pp-rewrite") << "to " << res << "\n";
791 return res;
792 }
793
794 void TheoryBV::presolve() {
795 Debug("bitvector") << "TheoryBV::presolve" << endl;
796 }
797
798 static int prop_count = 0;
799
800 bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
801 {
802 Debug("bitvector::propagate") << indent() << getSatContext()->getLevel() << " " << "TheoryBV::storePropagation(" << literal << ", " << subtheory << ")" << std::endl;
803 prop_count++;
804
805 // If already in conflict, no more propagation
806 if (d_conflict) {
807 Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << "): already in conflict" << std::endl;
808 return false;
809 }
810
811 // If propagated already, just skip
812 PropagatedMap::const_iterator find = d_propagatedBy.find(literal);
813 if (find != d_propagatedBy.end()) {
814 return true;
815 } else {
816 bool polarity = literal.getKind() != kind::NOT;
817 Node negatedLiteral = polarity ? literal.notNode() : (Node) literal[0];
818 find = d_propagatedBy.find(negatedLiteral);
819 if (find != d_propagatedBy.end() && (*find).second != subtheory) {
820 // Safe to ignore this one, subtheory should produce a conflict
821 return true;
822 }
823
824 d_propagatedBy[literal] = subtheory;
825 }
826
827 // Propagate differs depending on the subtheory
828 // * bitblaster needs to be left alone until it's done, otherwise it doesn't
829 // know how to explain
830 // * equality engine can propagate eagerly
831 // TODO(2348): Determine if ok should be set by propagate. If not, remove ok.
832 constexpr bool ok = true;
833 if (subtheory == SUB_CORE) {
834 d_out->propagate(literal);
835 if (!ok) {
836 setConflict();
837 }
838 } else {
839 d_literalsToPropagate.push_back(literal);
840 }
841 return ok;
842
843 }/* TheoryBV::propagate(TNode) */
844
845
846 void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) {
847 Assert(wasPropagatedBySubtheory(literal));
848 SubTheory sub = getPropagatingSubtheory(literal);
849 d_subtheoryMap[sub]->explain(literal, assumptions);
850 }
851
852
853 Node TheoryBV::explain(TNode node) {
854 Debug("bitvector::explain") << "TheoryBV::explain(" << node << ")" << std::endl;
855 std::vector<TNode> assumptions;
856
857 // Ask for the explanation
858 explain(node, assumptions);
859 // this means that it is something true at level 0
860 if (assumptions.size() == 0) {
861 return utils::mkTrue();
862 }
863 // return the explanation
864 Node explanation = utils::mkAnd(assumptions);
865 Debug("bitvector::explain") << "TheoryBV::explain(" << node << ") => " << explanation << std::endl;
866 Debug("bitvector::explain") << "TheoryBV::explain done. \n";
867 return explanation;
868 }
869
870
871 void TheoryBV::addSharedTerm(TNode t) {
872 Debug("bitvector::sharing") << indent() << "TheoryBV::addSharedTerm(" << t << ")" << std::endl;
873 d_sharedTermsSet.insert(t);
874 if (options::bitvectorEqualitySolver()) {
875 for (unsigned i = 0; i < d_subtheories.size(); ++i) {
876 d_subtheories[i]->addSharedTerm(t);
877 }
878 }
879 }
880
881
882 EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
883 {
884 if (options::bitblastMode() == options::BitblastMode::EAGER)
885 return EQUALITY_UNKNOWN;
886 Assert(options::bitblastMode() == options::BitblastMode::LAZY);
887 for (unsigned i = 0; i < d_subtheories.size(); ++i) {
888 EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b);
889 if (status != EQUALITY_UNKNOWN) {
890 return status;
891 }
892 }
893 return EQUALITY_UNKNOWN; ;
894 }
895
896
897 void TheoryBV::enableCoreTheorySlicer() {
898 Assert(!d_calledPreregister);
899 d_isCoreTheory = true;
900 if (d_subtheoryMap.find(SUB_CORE) != d_subtheoryMap.end()) {
901 CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
902 core->enableSlicer();
903 }
904 }
905
906
907 void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
908 if(d_staticLearnCache.find(in) != d_staticLearnCache.end()){
909 return;
910 }
911 d_staticLearnCache.insert(in);
912
913 if (in.getKind() == kind::EQUAL) {
914 if((in[0].getKind() == kind::BITVECTOR_PLUS && in[1].getKind() == kind::BITVECTOR_SHL) ||
915 (in[1].getKind() == kind::BITVECTOR_PLUS && in[0].getKind() == kind::BITVECTOR_SHL)) {
916 TNode p = in[0].getKind() == kind::BITVECTOR_PLUS ? in[0] : in[1];
917 TNode s = in[0].getKind() == kind::BITVECTOR_PLUS ? in[1] : in[0];
918
919 if(p.getNumChildren() == 2
920 && p[0].getKind() == kind::BITVECTOR_SHL
921 && p[1].getKind() == kind::BITVECTOR_SHL ){
922 unsigned size = utils::getSize(s);
923 Node one = utils::mkConst(size, 1u);
924 if(s[0] == one && p[0][0] == one && p[1][0] == one){
925 Node zero = utils::mkConst(size, 0u);
926 TNode b = p[0];
927 TNode c = p[1];
928 // (s : 1 << S) = (b : 1 << B) + (c : 1 << C)
929 Node b_eq_0 = b.eqNode(zero);
930 Node c_eq_0 = c.eqNode(zero);
931 Node b_eq_c = b.eqNode(c);
932
933 Node dis = NodeManager::currentNM()->mkNode(
934 kind::OR, b_eq_0, c_eq_0, b_eq_c);
935 Node imp = in.impNode(dis);
936 learned << imp;
937 }
938 }
939 }
940 }else if(in.getKind() == kind::AND){
941 for(size_t i = 0, N = in.getNumChildren(); i < N; ++i){
942 ppStaticLearn(in[i], learned);
943 }
944 }
945 }
946
947 bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
948 bool changed = d_abstractionModule->applyAbstraction(assertions, new_assertions);
949 if (changed && options::bitblastMode() == options::BitblastMode::EAGER
950 && options::bitvectorAig())
951 {
952 // disable AIG mode
953 AlwaysAssert(!d_eagerSolver->isInitialized());
954 d_eagerSolver->turnOffAig();
955 d_eagerSolver->initialize();
956 }
957 return changed;
958 }
959
960 void TheoryBV::setProofLog(proof::BitVectorProof* bvp)
961 {
962 if (options::bitblastMode() == options::BitblastMode::EAGER)
963 {
964 d_eagerSolver->setProofLog(bvp);
965 }
966 else
967 {
968 for( unsigned i=0; i< d_subtheories.size(); i++ ){
969 d_subtheories[i]->setProofLog( bvp );
970 }
971 }
972 }
973
974 void TheoryBV::setConflict(Node conflict)
975 {
976 if (options::bvAbstraction())
977 {
978 NodeManager* const nm = NodeManager::currentNM();
979 Node new_conflict = d_abstractionModule->simplifyConflict(conflict);
980
981 std::vector<Node> lemmas;
982 lemmas.push_back(new_conflict);
983 d_abstractionModule->generalizeConflict(new_conflict, lemmas);
984 for (unsigned i = 0; i < lemmas.size(); ++i)
985 {
986 lemma(nm->mkNode(kind::NOT, lemmas[i]));
987 }
988 }
989 d_conflict = true;
990 d_conflictNode = conflict;
991 }
992
993 } /* namespace CVC4::theory::bv */
994 } /* namespace CVC4::theory */
995 } /* namespace CVC4 */