projects / cvc5.git / blob
? search:


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