1 /********************* */
2 /*! \file theory_bv.cpp
4 ** Original author: Dejan Jovanovic
5 ** Major contributors: Liana Hadarean
6 ** Minor contributors (to current version): Tim King, Kshitij Bansal, Clark Barrett, Andrew Reynolds, Morgan Deters, Martin Brain <>
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 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 ** [[ Add lengthier description here ]]
13 ** \todo document this file
16 #include "theory/bv/theory_bv.h"
18 #include "options/bv_options.h"
19 #include "options/smt_options.h"
20 #include "theory/bv/abstraction.h"
21 #include "theory/bv/bv_eager_solver.h"
22 #include "theory/bv/bv_subtheory_algebraic.h"
23 #include "theory/bv/bv_subtheory_bitblast.h"
24 #include "theory/bv/bv_subtheory_core.h"
25 #include "theory/bv/bv_subtheory_inequality.h"
26 #include "theory/bv/slicer.h"
27 #include "theory/bv/theory_bv_rewrite_rules_normalization.h"
28 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
29 #include "theory/bv/theory_bv_rewriter.h"
30 #include "theory/bv/theory_bv_utils.h"
31 #include "theory/theory_model.h"
32 #include "theory/valuation.h"
35 using namespace CVC4::theory
;
36 using namespace CVC4::theory::bv
;
37 using namespace CVC4::context
;
40 using namespace CVC4::theory::bv::utils
;
42 TheoryBV::TheoryBV(context::Context
* c
, context::UserContext
* u
, OutputChannel
& out
, Valuation valuation
, const LogicInfo
& logicInfo
)
43 : Theory(THEORY_BV
, c
, u
, out
, valuation
, logicInfo
),
45 d_alreadyPropagatedSet(c
),
51 d_lemmasAdded(c
, false),
53 d_invalidateModelCache(c
, true),
54 d_literalsToPropagate(c
),
55 d_literalsToPropagateIndex(c
, 0),
58 d_abstractionModule(new AbstractionModule()),
59 d_isCoreTheory(false),
60 d_calledPreregister(false)
63 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
64 d_eagerSolver
= new EagerBitblastSolver(this);
68 if (options::bitvectorEqualitySolver()) {
69 SubtheorySolver
* core_solver
= new CoreSolver(c
, this);
70 d_subtheories
.push_back(core_solver
);
71 d_subtheoryMap
[SUB_CORE
] = core_solver
;
74 if (options::bitvectorInequalitySolver()) {
75 SubtheorySolver
* ineq_solver
= new InequalitySolver(c
, this);
76 d_subtheories
.push_back(ineq_solver
);
77 d_subtheoryMap
[SUB_INEQUALITY
] = ineq_solver
;
80 if (options::bitvectorAlgebraicSolver()) {
81 SubtheorySolver
* alg_solver
= new AlgebraicSolver(c
, this);
82 d_subtheories
.push_back(alg_solver
);
83 d_subtheoryMap
[SUB_ALGEBRAIC
] = alg_solver
;
86 BitblastSolver
* bb_solver
= new BitblastSolver(c
, this);
87 if (options::bvAbstraction()) {
88 bb_solver
->setAbstraction(d_abstractionModule
);
90 d_subtheories
.push_back(bb_solver
);
91 d_subtheoryMap
[SUB_BITBLAST
] = bb_solver
;
95 TheoryBV::~TheoryBV() {
96 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
97 delete d_subtheories
[i
];
99 delete d_abstractionModule
;
102 void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine
* eq
) {
103 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
106 if (options::bitvectorEqualitySolver()) {
107 dynamic_cast<CoreSolver
*>(d_subtheoryMap
[SUB_CORE
])->setMasterEqualityEngine(eq
);
111 void TheoryBV::spendResource(unsigned ammount
) throw(UnsafeInterruptException
) {
112 getOutputChannel().spendResource(ammount
);
115 TheoryBV::Statistics::Statistics():
116 d_avgConflictSize("theory::bv::AvgBVConflictSize"),
117 d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0),
118 d_solveTimer("theory::bv::solveTimer"),
119 d_numCallsToCheckFullEffort("theory::bv::NumberOfFullCheckCalls", 0),
120 d_numCallsToCheckStandardEffort("theory::bv::NumberOfStandardCheckCalls", 0),
121 d_weightComputationTimer("theory::bv::weightComputationTimer"),
122 d_numMultSlice("theory::bv::NumMultSliceApplied", 0)
124 StatisticsRegistry::registerStat(&d_avgConflictSize
);
125 StatisticsRegistry::registerStat(&d_solveSubstitutions
);
126 StatisticsRegistry::registerStat(&d_solveTimer
);
127 StatisticsRegistry::registerStat(&d_numCallsToCheckFullEffort
);
128 StatisticsRegistry::registerStat(&d_numCallsToCheckStandardEffort
);
129 StatisticsRegistry::registerStat(&d_weightComputationTimer
);
130 StatisticsRegistry::registerStat(&d_numMultSlice
);
133 TheoryBV::Statistics::~Statistics() {
134 StatisticsRegistry::unregisterStat(&d_avgConflictSize
);
135 StatisticsRegistry::unregisterStat(&d_solveSubstitutions
);
136 StatisticsRegistry::unregisterStat(&d_solveTimer
);
137 StatisticsRegistry::unregisterStat(&d_numCallsToCheckFullEffort
);
138 StatisticsRegistry::unregisterStat(&d_numCallsToCheckStandardEffort
);
139 StatisticsRegistry::unregisterStat(&d_weightComputationTimer
);
140 StatisticsRegistry::unregisterStat(&d_numMultSlice
);
143 Node
TheoryBV::getBVDivByZero(Kind k
, unsigned width
) {
144 NodeManager
* nm
= NodeManager::currentNM();
145 if (k
== kind::BITVECTOR_UDIV
) {
146 if (d_BVDivByZero
.find(width
) == d_BVDivByZero
.end()) {
147 // lazily create the function symbols
149 os
<< "BVUDivByZero_" << width
;
150 Node divByZero
= nm
->mkSkolem(os
.str(),
151 nm
->mkFunctionType(nm
->mkBitVectorType(width
), nm
->mkBitVectorType(width
)),
152 "partial bvudiv", NodeManager::SKOLEM_EXACT_NAME
);
153 d_BVDivByZero
[width
] = divByZero
;
155 return d_BVDivByZero
[width
];
157 else if (k
== kind::BITVECTOR_UREM
) {
158 if (d_BVRemByZero
.find(width
) == d_BVRemByZero
.end()) {
160 os
<< "BVURemByZero_" << width
;
161 Node divByZero
= nm
->mkSkolem(os
.str(),
162 nm
->mkFunctionType(nm
->mkBitVectorType(width
), nm
->mkBitVectorType(width
)),
163 "partial bvurem", NodeManager::SKOLEM_EXACT_NAME
);
164 d_BVRemByZero
[width
] = divByZero
;
166 return d_BVRemByZero
[width
];
173 void TheoryBV::collectNumerators(TNode term
, TNodeSet
& seen
) {
174 if (seen
.find(term
) != seen
.end())
176 if (term
.getKind() == kind::BITVECTOR_ACKERMANIZE_UDIV
) {
177 unsigned size
= utils::getSize(term
[0]);
178 if (d_BVDivByZeroAckerman
.find(size
) == d_BVDivByZeroAckerman
.end()) {
179 d_BVDivByZeroAckerman
[size
] = TNodeSet();
181 d_BVDivByZeroAckerman
[size
].insert(term
[0]);
183 } else if (term
.getKind() == kind::BITVECTOR_ACKERMANIZE_UREM
) {
184 unsigned size
= utils::getSize(term
[0]);
185 if (d_BVRemByZeroAckerman
.find(size
) == d_BVRemByZeroAckerman
.end()) {
186 d_BVRemByZeroAckerman
[size
] = TNodeSet();
188 d_BVRemByZeroAckerman
[size
].insert(term
[0]);
191 for (unsigned i
= 0; i
< term
.getNumChildren(); ++i
) {
192 collectNumerators(term
[i
], seen
);
197 void TheoryBV::mkAckermanizationAsssertions(std::vector
<Node
>& assertions
) {
198 Debug("bv-ackermanize") << "TheoryBV::mkAckermanizationAsssertions\n";
200 Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
);
201 AlwaysAssert(!options::incrementalSolving());
203 for (unsigned i
= 0; i
< assertions
.size(); ++i
) {
204 collectNumerators(assertions
[i
], seen
);
207 // process division UF
208 Debug("bv-ackermanize") << "Process division UF...\n";
209 for (WidthToNumerators::const_iterator it
= d_BVDivByZeroAckerman
.begin(); it
!= d_BVDivByZeroAckerman
.end(); ++it
) {
210 const TNodeSet
& numerators
= it
->second
;
211 for (TNodeSet::const_iterator i
= numerators
.begin(); i
!= numerators
.end(); ++i
) {
212 TNodeSet::const_iterator j
= i
;
214 for (; j
!= numerators
.end(); ++j
) {
217 TNode acker1
= utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UDIV
, arg1
);
218 TNode acker2
= utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UDIV
, arg2
);
220 Node arg_eq
= utils::mkNode(kind::EQUAL
, arg1
, arg2
);
221 Node acker_eq
= utils::mkNode(kind::EQUAL
, acker1
, acker2
);
222 Node lemma
= utils::mkNode(kind::IMPLIES
, arg_eq
, acker_eq
);
223 Debug("bv-ackermanize") << " " << lemma
<< "\n";
224 assertions
.push_back(lemma
);
228 // process remainder UF
229 Debug("bv-ackermanize") << "Process remainder UF...\n";
230 for (WidthToNumerators::const_iterator it
= d_BVRemByZeroAckerman
.begin(); it
!= d_BVRemByZeroAckerman
.end(); ++it
) {
231 const TNodeSet
& numerators
= it
->second
;
232 for (TNodeSet::const_iterator i
= numerators
.begin(); i
!= numerators
.end(); ++i
) {
233 TNodeSet::const_iterator j
= i
;
235 for (; j
!= numerators
.end(); ++j
) {
238 TNode acker1
= utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UREM
, arg1
);
239 TNode acker2
= utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UREM
, arg2
);
241 Node arg_eq
= utils::mkNode(kind::EQUAL
, arg1
, arg2
);
242 Node acker_eq
= utils::mkNode(kind::EQUAL
, acker1
, acker2
);
243 Node lemma
= utils::mkNode(kind::IMPLIES
, arg_eq
, acker_eq
);
244 Debug("bv-ackermanize") << " " << lemma
<< "\n";
245 assertions
.push_back(lemma
);
251 Node
TheoryBV::expandDefinition(LogicRequest
&logicRequest
, Node node
) {
252 Debug("bitvector-expandDefinition") << "TheoryBV::expandDefinition(" << node
<< ")" << std::endl
;
254 switch (node
.getKind()) {
255 case kind::BITVECTOR_SDIV
:
256 case kind::BITVECTOR_SREM
:
257 case kind::BITVECTOR_SMOD
:
258 return TheoryBVRewriter::eliminateBVSDiv(node
);
261 case kind::BITVECTOR_UDIV
:
262 case kind::BITVECTOR_UREM
: {
263 NodeManager
* nm
= NodeManager::currentNM();
264 unsigned width
= node
.getType().getBitVectorSize();
266 if (options::bitvectorDivByZeroConst()) {
267 Kind kind
= node
.getKind() == kind::BITVECTOR_UDIV
? kind::BITVECTOR_UDIV_TOTAL
: kind::BITVECTOR_UREM_TOTAL
;
268 return nm
->mkNode(kind
, node
[0], node
[1]);
271 TNode num
= node
[0], den
= node
[1];
272 Node den_eq_0
= nm
->mkNode(kind::EQUAL
, den
, nm
->mkConst(BitVector(width
, Integer(0))));
273 Node divTotalNumDen
= nm
->mkNode(node
.getKind() == kind::BITVECTOR_UDIV
? kind::BITVECTOR_UDIV_TOTAL
:
274 kind::BITVECTOR_UREM_TOTAL
, num
, den
);
276 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
277 // Ackermanize UF if using eager bit-blasting
278 Node ackerman_var
= nm
->mkNode(node
.getKind() == kind::BITVECTOR_UDIV
? kind::BITVECTOR_ACKERMANIZE_UDIV
: kind::BITVECTOR_ACKERMANIZE_UREM
, num
);
279 node
= nm
->mkNode(kind::ITE
, den_eq_0
, ackerman_var
, divTotalNumDen
);
282 Node divByZero
= getBVDivByZero(node
.getKind(), width
);
283 Node divByZeroNum
= nm
->mkNode(kind::APPLY_UF
, divByZero
, num
);
284 node
= nm
->mkNode(kind::ITE
, den_eq_0
, divByZeroNum
, divTotalNumDen
);
285 logicRequest
.widenLogic(THEORY_UF
);
300 void TheoryBV::preRegisterTerm(TNode node
) {
301 d_calledPreregister
= true;
302 Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node
<< ")" << std::endl
;
304 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
305 // the aig bit-blaster option is set heuristically
306 // if bv abstraction is not used
307 if (!d_eagerSolver
->isInitialized()) {
308 d_eagerSolver
->initialize();
311 if (node
.getKind() == kind::BITVECTOR_EAGER_ATOM
) {
312 Node formula
= node
[0];
313 d_eagerSolver
->assertFormula(formula
);
315 // nothing to do for the other terms
319 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
320 d_subtheories
[i
]->preRegister(node
);
324 void TheoryBV::sendConflict() {
326 if (d_conflictNode
.isNull()) {
329 Debug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode
;
330 d_out
->conflict(d_conflictNode
);
331 d_statistics
.d_avgConflictSize
.addEntry(d_conflictNode
.getNumChildren());
332 d_conflictNode
= Node::null();
336 void TheoryBV::checkForLemma(TNode fact
) {
337 if (fact
.getKind() == kind::EQUAL
) {
338 if (fact
[0].getKind() == kind::BITVECTOR_UREM_TOTAL
) {
339 TNode urem
= fact
[0];
340 TNode result
= fact
[1];
341 TNode divisor
= urem
[1];
342 Node result_ult_div
= mkNode(kind::BITVECTOR_ULT
, result
, divisor
);
343 Node divisor_eq_0
= mkNode(kind::EQUAL
,
345 mkConst(BitVector(getSize(divisor
), 0u)));
346 Node split
= utils::mkNode(kind::OR
, divisor_eq_0
, mkNode(kind::NOT
, fact
), result_ult_div
);
349 if (fact
[1].getKind() == kind::BITVECTOR_UREM_TOTAL
) {
350 TNode urem
= fact
[1];
351 TNode result
= fact
[0];
352 TNode divisor
= urem
[1];
353 Node result_ult_div
= mkNode(kind::BITVECTOR_ULT
, result
, divisor
);
354 Node divisor_eq_0
= mkNode(kind::EQUAL
,
356 mkConst(BitVector(getSize(divisor
), 0u)));
357 Node split
= utils::mkNode(kind::OR
, divisor_eq_0
, mkNode(kind::NOT
, fact
), result_ult_div
);
364 void TheoryBV::check(Effort e
)
366 if (done() && !fullEffort(e
)) {
369 TimerStat::CodeTimer
checkTimer(d_checkTime
);
370 Debug("bitvector") << "TheoryBV::check(" << e
<< ")" << std::endl
;
371 TimerStat::CodeTimer
codeTimer(d_statistics
.d_solveTimer
);
372 // we may be getting new assertions so the model cache may not be sound
373 d_invalidateModelCache
.set(true);
374 // if we are using the eager solver
375 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
376 // this can only happen on an empty benchmark
377 if (!d_eagerSolver
->isInitialized()) {
378 d_eagerSolver
->initialize();
380 if (!Theory::fullEffort(e
))
383 std::vector
<TNode
> assertions
;
385 TNode fact
= get().assertion
;
386 Assert (fact
.getKind() == kind::BITVECTOR_EAGER_ATOM
);
387 assertions
.push_back(fact
);
389 Assert (d_eagerSolver
->hasAssertions(assertions
));
391 bool ok
= d_eagerSolver
->checkSat();
393 if (assertions
.size() == 1) {
394 d_out
->conflict(assertions
[0]);
397 Node conflict
= NodeManager::currentNM()->mkNode(kind::AND
, assertions
);
398 d_out
->conflict(conflict
);
405 if (Theory::fullEffort(e
)) {
406 ++(d_statistics
.d_numCallsToCheckFullEffort
);
408 ++(d_statistics
.d_numCallsToCheckStandardEffort
);
410 // if we are already in conflict just return the conflict
417 TNode fact
= get().assertion
;
421 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
422 d_subtheories
[i
]->assertFact(fact
);
427 bool complete
= false;
428 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
429 Assert (!inConflict());
430 ok
= d_subtheories
[i
]->check(e
);
431 complete
= d_subtheories
[i
]->isComplete();
434 // if we are in a conflict no need to check with other theories
435 Assert (inConflict());
440 // if the last subtheory was complete we stop
446 void TheoryBV::collectModelInfo( TheoryModel
* m
, bool fullModel
){
447 Assert(!inConflict());
448 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
449 d_eagerSolver
->collectModelInfo(m
, fullModel
);
451 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
452 if (d_subtheories
[i
]->isComplete()) {
453 d_subtheories
[i
]->collectModelInfo(m
, fullModel
);
459 Node
TheoryBV::getModelValue(TNode var
) {
460 Assert(!inConflict());
461 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
462 if (d_subtheories
[i
]->isComplete()) {
463 return d_subtheories
[i
]->getModelValue(var
);
469 void TheoryBV::propagate(Effort e
) {
470 Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl
;
471 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
479 // go through stored propagations
481 for (; d_literalsToPropagateIndex
< d_literalsToPropagate
.size() && ok
; d_literalsToPropagateIndex
= d_literalsToPropagateIndex
+ 1) {
482 TNode literal
= d_literalsToPropagate
[d_literalsToPropagateIndex
];
483 // temporary fix for incremental bit-blasting
484 if (d_valuation
.isSatLiteral(literal
)) {
485 Debug("bitvector::propagate") << "TheoryBV:: propagating " << literal
<<"\n";
486 ok
= d_out
->propagate(literal
);
491 Debug("bitvector::propagate") << indent() << "TheoryBV::propagate(): conflict from theory engine" << std::endl
;
497 Theory::PPAssertStatus
TheoryBV::ppAssert(TNode in
, SubstitutionMap
& outSubstitutions
) {
498 switch(in
.getKind()) {
501 if (in
[0].isVar() && !in
[1].hasSubterm(in
[0])) {
502 ++(d_statistics
.d_solveSubstitutions
);
503 outSubstitutions
.addSubstitution(in
[0], in
[1]);
504 return PP_ASSERT_STATUS_SOLVED
;
506 if (in
[1].isVar() && !in
[0].hasSubterm(in
[1])) {
507 ++(d_statistics
.d_solveSubstitutions
);
508 outSubstitutions
.addSubstitution(in
[1], in
[0]);
509 return PP_ASSERT_STATUS_SOLVED
;
511 Node node
= Rewriter::rewrite(in
);
512 if ((node
[0].getKind() == kind::BITVECTOR_EXTRACT
&& node
[1].isConst()) ||
513 (node
[1].getKind() == kind::BITVECTOR_EXTRACT
&& node
[0].isConst())) {
514 Node extract
= node
[0].isConst() ? node
[1] : node
[0];
515 if (extract
[0].getKind() == kind::VARIABLE
) {
516 Node c
= node
[0].isConst() ? node
[0] : node
[1];
518 unsigned high
= utils::getExtractHigh(extract
);
519 unsigned low
= utils::getExtractLow(extract
);
520 unsigned var_bitwidth
= utils::getSize(extract
[0]);
521 std::vector
<Node
> children
;
524 Assert (high
!= var_bitwidth
- 1);
525 unsigned skolem_size
= var_bitwidth
- high
- 1;
526 Node skolem
= utils::mkVar(skolem_size
);
527 children
.push_back(skolem
);
528 children
.push_back(c
);
529 } else if (high
== var_bitwidth
- 1) {
530 unsigned skolem_size
= low
;
531 Node skolem
= utils::mkVar(skolem_size
);
532 children
.push_back(c
);
533 children
.push_back(skolem
);
535 unsigned skolem1_size
= low
;
536 unsigned skolem2_size
= var_bitwidth
- high
- 1;
537 Node skolem1
= utils::mkVar(skolem1_size
);
538 Node skolem2
= utils::mkVar(skolem2_size
);
539 children
.push_back(skolem2
);
540 children
.push_back(c
);
541 children
.push_back(skolem1
);
543 Node concat
= utils::mkNode(kind::BITVECTOR_CONCAT
, children
);
544 Assert (utils::getSize(concat
) == utils::getSize(extract
[0]));
545 outSubstitutions
.addSubstitution(extract
[0], concat
);
546 return PP_ASSERT_STATUS_SOLVED
;
551 case kind::BITVECTOR_ULT
:
552 case kind::BITVECTOR_SLT
:
553 case kind::BITVECTOR_ULE
:
554 case kind::BITVECTOR_SLE
:
557 // TODO other predicates
560 return PP_ASSERT_STATUS_UNSOLVED
;
563 Node
TheoryBV::ppRewrite(TNode t
)
565 Debug("bv-pp-rewrite") << "TheoryBV::ppRewrite " << t
<< "\n";
567 if (RewriteRule
<BitwiseEq
>::applies(t
)) {
568 Node result
= RewriteRule
<BitwiseEq
>::run
<false>(t
);
569 res
= Rewriter::rewrite(result
);
570 } else if (d_isCoreTheory
&& t
.getKind() == kind::EQUAL
) {
571 std::vector
<Node
> equalities
;
572 Slicer::splitEqualities(t
, equalities
);
573 res
= utils::mkAnd(equalities
);
574 } else if (RewriteRule
<UltPlusOne
>::applies(t
)) {
575 Node result
= RewriteRule
<UltPlusOne
>::run
<false>(t
);
576 res
= Rewriter::rewrite(result
);
577 } else if( res
.getKind() == kind::EQUAL
&&
578 ((res
[0].getKind() == kind::BITVECTOR_PLUS
&&
579 RewriteRule
<ConcatToMult
>::applies(res
[1])) ||
580 (res
[1].getKind() == kind::BITVECTOR_PLUS
&&
581 RewriteRule
<ConcatToMult
>::applies(res
[0])))) {
582 Node mult
= RewriteRule
<ConcatToMult
>::applies(res
[0])?
583 RewriteRule
<ConcatToMult
>::run
<false>(res
[0]) :
584 RewriteRule
<ConcatToMult
>::run
<true>(res
[1]);
585 Node factor
= mult
[0];
586 Node sum
= RewriteRule
<ConcatToMult
>::applies(res
[0])? res
[1] : res
[0];
587 Node new_eq
=utils::mkNode(kind::EQUAL
, sum
, mult
);
588 Node rewr_eq
= RewriteRule
<SolveEq
>::run
<true>(new_eq
);
589 if (rewr_eq
[0].isVar() || rewr_eq
[1].isVar()){
590 res
= Rewriter::rewrite(rewr_eq
);
597 // if(t.getKind() == kind::EQUAL &&
598 // ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() == kind::BITVECTOR_PLUS) ||
599 // (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() == kind::BITVECTOR_PLUS))) {
600 // // if we have an equality between a multiplication and addition
601 // // try to express multiplication in terms of addition
602 // Node mult = t[0].getKind() == kind::BITVECTOR_MULT? t[0] : t[1];
603 // Node add = t[0].getKind() == kind::BITVECTOR_PLUS? t[0] : t[1];
604 // if (RewriteRule<MultSlice>::applies(mult)) {
605 // Node new_mult = RewriteRule<MultSlice>::run<false>(mult);
606 // Node new_eq = Rewriter::rewrite(utils::mkNode(kind::EQUAL, new_mult, add));
608 // // the simplification can cause the formula to blow up
609 // // only apply if formula reduced
610 // if (d_subtheoryMap.find(SUB_BITBLAST) != d_subtheoryMap.end()) {
611 // BitblastSolver* bv = (BitblastSolver*)d_subtheoryMap[SUB_BITBLAST];
612 // uint64_t old_size = bv->computeAtomWeight(t);
613 // Assert (old_size);
614 // uint64_t new_size = bv->computeAtomWeight(new_eq);
615 // double ratio = ((double)new_size)/old_size;
616 // if (ratio <= 0.4) {
617 // ++(d_statistics.d_numMultSlice);
622 // if (new_eq.getKind() == kind::CONST_BOOLEAN) {
623 // ++(d_statistics.d_numMultSlice);
629 if (options::bvAbstraction() && t
.getType().isBoolean()) {
630 d_abstractionModule
->addInputAtom(res
);
632 Debug("bv-pp-rewrite") << "to " << res
<< "\n";
636 void TheoryBV::presolve() {
637 Debug("bitvector") << "TheoryBV::presolve" << endl
;
640 static int prop_count
= 0;
642 bool TheoryBV::storePropagation(TNode literal
, SubTheory subtheory
)
644 Debug("bitvector::propagate") << indent() << getSatContext()->getLevel() << " " << "TheoryBV::storePropagation(" << literal
<< ", " << subtheory
<< ")" << std::endl
;
647 // If already in conflict, no more propagation
649 Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal
<< ", " << subtheory
<< "): already in conflict" << std::endl
;
653 // If propagated already, just skip
654 PropagatedMap::const_iterator find
= d_propagatedBy
.find(literal
);
655 if (find
!= d_propagatedBy
.end()) {
658 bool polarity
= literal
.getKind() != kind::NOT
;
659 Node negatedLiteral
= polarity
? literal
.notNode() : (Node
) literal
[0];
660 find
= d_propagatedBy
.find(negatedLiteral
);
661 if (find
!= d_propagatedBy
.end() && (*find
).second
!= subtheory
) {
662 // Safe to ignore this one, subtheory should produce a conflict
666 d_propagatedBy
[literal
] = subtheory
;
669 // Propagate differs depending on the subtheory
670 // * bitblaster needs to be left alone until it's done, otherwise it doesn't know how to explain
671 // * equality engine can propagate eagerly
673 if (subtheory
== SUB_CORE
) {
674 d_out
->propagate(literal
);
679 d_literalsToPropagate
.push_back(literal
);
683 }/* TheoryBV::propagate(TNode) */
686 void TheoryBV::explain(TNode literal
, std::vector
<TNode
>& assumptions
) {
687 Assert (wasPropagatedBySubtheory(literal
));
688 SubTheory sub
= getPropagatingSubtheory(literal
);
689 d_subtheoryMap
[sub
]->explain(literal
, assumptions
);
693 Node
TheoryBV::explain(TNode node
) {
694 Debug("bitvector::explain") << "TheoryBV::explain(" << node
<< ")" << std::endl
;
695 std::vector
<TNode
> assumptions
;
697 // Ask for the explanation
698 explain(node
, assumptions
);
699 // this means that it is something true at level 0
700 if (assumptions
.size() == 0) {
701 return utils::mkTrue();
703 // return the explanation
704 Node explanation
= utils::mkAnd(assumptions
);
705 Debug("bitvector::explain") << "TheoryBV::explain(" << node
<< ") => " << explanation
<< std::endl
;
710 void TheoryBV::addSharedTerm(TNode t
) {
711 Debug("bitvector::sharing") << indent() << "TheoryBV::addSharedTerm(" << t
<< ")" << std::endl
;
712 d_sharedTermsSet
.insert(t
);
713 if (options::bitvectorEqualitySolver()) {
714 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
715 d_subtheories
[i
]->addSharedTerm(t
);
721 EqualityStatus
TheoryBV::getEqualityStatus(TNode a
, TNode b
)
723 Assert (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY
);
724 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
725 EqualityStatus status
= d_subtheories
[i
]->getEqualityStatus(a
, b
);
726 if (status
!= EQUALITY_UNKNOWN
) {
730 return EQUALITY_UNKNOWN
; ;
734 void TheoryBV::enableCoreTheorySlicer() {
735 Assert (!d_calledPreregister
);
736 d_isCoreTheory
= true;
737 if (d_subtheoryMap
.find(SUB_CORE
) != d_subtheoryMap
.end()) {
738 CoreSolver
* core
= (CoreSolver
*)d_subtheoryMap
[SUB_CORE
];
739 core
->enableSlicer();
744 void TheoryBV::ppStaticLearn(TNode in
, NodeBuilder
<>& learned
) {
745 if(d_staticLearnCache
.find(in
) != d_staticLearnCache
.end()){
748 d_staticLearnCache
.insert(in
);
750 if (in
.getKind() == kind::EQUAL
) {
751 if((in
[0].getKind() == kind::BITVECTOR_PLUS
&& in
[1].getKind() == kind::BITVECTOR_SHL
) ||
752 (in
[1].getKind() == kind::BITVECTOR_PLUS
&& in
[0].getKind() == kind::BITVECTOR_SHL
)) {
753 TNode p
= in
[0].getKind() == kind::BITVECTOR_PLUS
? in
[0] : in
[1];
754 TNode s
= in
[0].getKind() == kind::BITVECTOR_PLUS
? in
[1] : in
[0];
756 if(p
.getNumChildren() == 2
757 && p
[0].getKind() == kind::BITVECTOR_SHL
758 && p
[1].getKind() == kind::BITVECTOR_SHL
){
759 unsigned size
= utils::getSize(s
);
760 Node one
= utils::mkConst(size
, 1u);
761 if(s
[0] == one
&& p
[0][0] == one
&& p
[1][0] == one
){
762 Node zero
= utils::mkConst(size
, 0u);
765 // (s : 1 << S) = (b : 1 << B) + (c : 1 << C)
766 Node b_eq_0
= b
.eqNode(zero
);
767 Node c_eq_0
= c
.eqNode(zero
);
768 Node b_eq_c
= b
.eqNode(c
);
770 Node dis
= utils::mkNode(kind::OR
, b_eq_0
, c_eq_0
, b_eq_c
);
771 Node imp
= in
.impNode(dis
);
776 }else if(in
.getKind() == kind::AND
){
777 for(size_t i
= 0, N
= in
.getNumChildren(); i
< N
; ++i
){
778 ppStaticLearn(in
[i
], learned
);
783 bool TheoryBV::applyAbstraction(const std::vector
<Node
>& assertions
, std::vector
<Node
>& new_assertions
) {
784 bool changed
= d_abstractionModule
->applyAbstraction(assertions
, new_assertions
);
786 options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
&&
787 options::bitvectorAig()) {
789 AlwaysAssert (!d_eagerSolver
->isInitialized());
790 d_eagerSolver
->turnOffAig();
791 d_eagerSolver
->initialize();
796 void TheoryBV::setConflict(Node conflict
) {
797 if (options::bvAbstraction()) {
798 Node new_conflict
= d_abstractionModule
->simplifyConflict(conflict
);
800 std::vector
<Node
> lemmas
;
801 lemmas
.push_back(new_conflict
);
802 d_abstractionModule
->generalizeConflict(new_conflict
, lemmas
);
803 for (unsigned i
= 0; i
< lemmas
.size(); ++i
) {
804 lemma(utils::mkNode(kind::NOT
, lemmas
[i
]));
808 d_conflictNode
= conflict
;