1 /********************* */
2 /*! \file theory_bv.cpp
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-2020 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
12 ** [[ Add lengthier description here ]]
13 ** \todo document this file
16 #include "theory/bv/theory_bv.h"
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/theory_bv_rewrite_rules_normalization.h"
31 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
32 #include "theory/bv/theory_bv_rewriter.h"
33 #include "theory/bv/theory_bv_utils.h"
34 #include "theory/ext_theory.h"
35 #include "theory/theory_model.h"
36 #include "theory/valuation.h"
38 using namespace CVC4::context
;
39 using namespace CVC4::theory::bv::utils
;
46 TheoryBV::TheoryBV(context::Context
* c
,
47 context::UserContext
* u
,
50 const LogicInfo
& logicInfo
,
51 ProofNodeManager
* pnm
,
53 : Theory(THEORY_BV
, c
, u
, out
, valuation
, logicInfo
, pnm
, name
),
55 d_alreadyPropagatedSet(c
),
63 d_lemmasAdded(c
, false),
65 d_invalidateModelCache(c
, true),
66 d_literalsToPropagate(c
),
67 d_literalsToPropagateIndex(c
, 0),
68 d_extTheory(new ExtTheory(this)),
71 d_abstractionModule(new AbstractionModule(getStatsPrefix(THEORY_BV
))),
72 d_calledPreregister(false),
73 d_needsLastCallCheck(false),
74 d_extf_range_infer(u
),
75 d_extf_collapse_infer(u
),
76 d_state(c
, u
, valuation
)
78 d_extTheory
->addFunctionKind(kind::BITVECTOR_TO_NAT
);
79 d_extTheory
->addFunctionKind(kind::INT_TO_BITVECTOR
);
80 if (options::bitblastMode() == options::BitblastMode::EAGER
)
82 d_eagerSolver
.reset(new EagerBitblastSolver(c
, this));
86 if (options::bitvectorEqualitySolver() && !options::proof())
88 d_subtheories
.emplace_back(new CoreSolver(c
, this, d_extTheory
.get()));
89 d_subtheoryMap
[SUB_CORE
] = d_subtheories
.back().get();
92 if (options::bitvectorInequalitySolver() && !options::proof())
94 d_subtheories
.emplace_back(new InequalitySolver(c
, u
, this));
95 d_subtheoryMap
[SUB_INEQUALITY
] = d_subtheories
.back().get();
98 if (options::bitvectorAlgebraicSolver() && !options::proof())
100 d_subtheories
.emplace_back(new AlgebraicSolver(c
, this));
101 d_subtheoryMap
[SUB_ALGEBRAIC
] = d_subtheories
.back().get();
104 BitblastSolver
* bb_solver
= new BitblastSolver(c
, this);
105 if (options::bvAbstraction())
107 bb_solver
->setAbstraction(d_abstractionModule
.get());
109 d_subtheories
.emplace_back(bb_solver
);
110 d_subtheoryMap
[SUB_BITBLAST
] = bb_solver
;
112 // indicate we are using the default theory state object
113 d_theoryState
= &d_state
;
116 TheoryBV::~TheoryBV() {}
118 TheoryRewriter
* TheoryBV::getTheoryRewriter() { return &d_rewriter
; }
120 bool TheoryBV::needsEqualityEngine(EeSetupInfo
& esi
)
122 CoreSolver
* core
= (CoreSolver
*)d_subtheoryMap
[SUB_CORE
];
125 return core
->needsEqualityEngine(esi
);
127 // otherwise we don't use an equality engine
131 void TheoryBV::finishInit()
133 // these kinds are semi-evaluated in getModelValue (applications of this
134 // kind are treated as variables)
135 d_valuation
.setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UDIV
);
136 d_valuation
.setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM
);
138 CoreSolver
* core
= (CoreSolver
*)d_subtheoryMap
[SUB_CORE
];
141 // must finish initialization in the core solver
146 void TheoryBV::spendResource(ResourceManager::Resource r
)
148 getOutputChannel().spendResource(r
);
151 TheoryBV::Statistics::Statistics():
152 d_avgConflictSize("theory::bv::AvgBVConflictSize"),
153 d_solveSubstitutions("theory::bv::NumSolveSubstitutions", 0),
154 d_solveTimer("theory::bv::solveTimer"),
155 d_numCallsToCheckFullEffort("theory::bv::NumFullCheckCalls", 0),
156 d_numCallsToCheckStandardEffort("theory::bv::NumStandardCheckCalls", 0),
157 d_weightComputationTimer("theory::bv::weightComputationTimer"),
158 d_numMultSlice("theory::bv::NumMultSliceApplied", 0)
160 smtStatisticsRegistry()->registerStat(&d_avgConflictSize
);
161 smtStatisticsRegistry()->registerStat(&d_solveSubstitutions
);
162 smtStatisticsRegistry()->registerStat(&d_solveTimer
);
163 smtStatisticsRegistry()->registerStat(&d_numCallsToCheckFullEffort
);
164 smtStatisticsRegistry()->registerStat(&d_numCallsToCheckStandardEffort
);
165 smtStatisticsRegistry()->registerStat(&d_weightComputationTimer
);
166 smtStatisticsRegistry()->registerStat(&d_numMultSlice
);
169 TheoryBV::Statistics::~Statistics() {
170 smtStatisticsRegistry()->unregisterStat(&d_avgConflictSize
);
171 smtStatisticsRegistry()->unregisterStat(&d_solveSubstitutions
);
172 smtStatisticsRegistry()->unregisterStat(&d_solveTimer
);
173 smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckFullEffort
);
174 smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckStandardEffort
);
175 smtStatisticsRegistry()->unregisterStat(&d_weightComputationTimer
);
176 smtStatisticsRegistry()->unregisterStat(&d_numMultSlice
);
179 Node
TheoryBV::getBVDivByZero(Kind k
, unsigned width
) {
180 NodeManager
* nm
= NodeManager::currentNM();
181 if (k
== kind::BITVECTOR_UDIV
) {
182 if (d_BVDivByZero
.find(width
) == d_BVDivByZero
.end()) {
183 // lazily create the function symbols
185 os
<< "BVUDivByZero_" << width
;
186 Node divByZero
= nm
->mkSkolem(os
.str(),
187 nm
->mkFunctionType(nm
->mkBitVectorType(width
), nm
->mkBitVectorType(width
)),
188 "partial bvudiv", NodeManager::SKOLEM_EXACT_NAME
);
189 d_BVDivByZero
[width
] = divByZero
;
191 return d_BVDivByZero
[width
];
193 else if (k
== kind::BITVECTOR_UREM
) {
194 if (d_BVRemByZero
.find(width
) == d_BVRemByZero
.end()) {
196 os
<< "BVURemByZero_" << width
;
197 Node divByZero
= nm
->mkSkolem(os
.str(),
198 nm
->mkFunctionType(nm
->mkBitVectorType(width
), nm
->mkBitVectorType(width
)),
199 "partial bvurem", NodeManager::SKOLEM_EXACT_NAME
);
200 d_BVRemByZero
[width
] = divByZero
;
202 return d_BVRemByZero
[width
];
208 TrustNode
TheoryBV::expandDefinition(Node node
)
210 Debug("bitvector-expandDefinition") << "TheoryBV::expandDefinition(" << node
<< ")" << std::endl
;
213 switch (node
.getKind()) {
214 case kind::BITVECTOR_SDIV
:
215 case kind::BITVECTOR_SREM
:
216 case kind::BITVECTOR_SMOD
:
217 ret
= TheoryBVRewriter::eliminateBVSDiv(node
);
220 case kind::BITVECTOR_UDIV
:
221 case kind::BITVECTOR_UREM
: {
222 NodeManager
* nm
= NodeManager::currentNM();
223 unsigned width
= node
.getType().getBitVectorSize();
225 if (options::bitvectorDivByZeroConst()) {
226 Kind kind
= node
.getKind() == kind::BITVECTOR_UDIV
? kind::BITVECTOR_UDIV_TOTAL
: kind::BITVECTOR_UREM_TOTAL
;
227 ret
= nm
->mkNode(kind
, node
[0], node
[1]);
231 TNode num
= node
[0], den
= node
[1];
232 Node den_eq_0
= nm
->mkNode(kind::EQUAL
, den
, utils::mkZero(width
));
233 Node divTotalNumDen
= nm
->mkNode(node
.getKind() == kind::BITVECTOR_UDIV
? kind::BITVECTOR_UDIV_TOTAL
:
234 kind::BITVECTOR_UREM_TOTAL
, num
, den
);
235 Node divByZero
= getBVDivByZero(node
.getKind(), width
);
236 Node divByZeroNum
= nm
->mkNode(kind::APPLY_UF
, divByZero
, num
);
237 ret
= nm
->mkNode(kind::ITE
, den_eq_0
, divByZeroNum
, divTotalNumDen
);
244 if (!ret
.isNull() && node
!= ret
)
246 return TrustNode::mkTrustRewrite(node
, ret
, nullptr);
248 return TrustNode::null();
251 void TheoryBV::preRegisterTerm(TNode node
) {
252 d_calledPreregister
= true;
253 Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node
<< ")" << std::endl
;
255 if (options::bitblastMode() == options::BitblastMode::EAGER
)
257 // the aig bit-blaster option is set heuristically
258 // if bv abstraction is used
259 if (!d_eagerSolver
->isInitialized())
261 d_eagerSolver
->initialize();
264 if (node
.getKind() == kind::BITVECTOR_EAGER_ATOM
)
266 Node formula
= node
[0];
267 d_eagerSolver
->assertFormula(formula
);
272 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
273 d_subtheories
[i
]->preRegister(node
);
276 // AJR : equality solver currently registers all terms to ExtTheory, if we
277 // want a lazy reduction without the bv equality solver, need to call this
278 // d_extTheory->registerTermRec( node );
281 void TheoryBV::sendConflict() {
283 if (d_conflictNode
.isNull()) {
286 Debug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode
<< std::endl
;
287 d_out
->conflict(d_conflictNode
);
288 d_statistics
.d_avgConflictSize
.addEntry(d_conflictNode
.getNumChildren());
289 d_conflictNode
= Node::null();
293 void TheoryBV::checkForLemma(TNode fact
)
295 if (fact
.getKind() == kind::EQUAL
)
297 NodeManager
* nm
= NodeManager::currentNM();
298 if (fact
[0].getKind() == kind::BITVECTOR_UREM_TOTAL
)
300 TNode urem
= fact
[0];
301 TNode result
= fact
[1];
302 TNode divisor
= urem
[1];
303 Node result_ult_div
= nm
->mkNode(kind::BITVECTOR_ULT
, result
, divisor
);
305 nm
->mkNode(kind::EQUAL
, divisor
, mkZero(getSize(divisor
)));
306 Node split
= nm
->mkNode(
307 kind::OR
, divisor_eq_0
, nm
->mkNode(kind::NOT
, fact
), result_ult_div
);
310 if (fact
[1].getKind() == kind::BITVECTOR_UREM_TOTAL
)
312 TNode urem
= fact
[1];
313 TNode result
= fact
[0];
314 TNode divisor
= urem
[1];
315 Node result_ult_div
= nm
->mkNode(kind::BITVECTOR_ULT
, result
, divisor
);
317 nm
->mkNode(kind::EQUAL
, divisor
, mkZero(getSize(divisor
)));
318 Node split
= nm
->mkNode(
319 kind::OR
, divisor_eq_0
, nm
->mkNode(kind::NOT
, fact
), result_ult_div
);
325 void TheoryBV::check(Effort e
)
327 if (done() && e
<Theory::EFFORT_FULL
) {
331 //last call : do reductions on extended bitvector functions
332 if (e
== Theory::EFFORT_LAST_CALL
) {
333 std::vector
<Node
> nred
= d_extTheory
->getActive();
334 doExtfReductions(nred
);
338 TimerStat::CodeTimer
checkTimer(d_checkTime
);
339 Debug("bitvector") << "TheoryBV::check(" << e
<< ")" << std::endl
;
340 TimerStat::CodeTimer
codeTimer(d_statistics
.d_solveTimer
);
341 // we may be getting new assertions so the model cache may not be sound
342 d_invalidateModelCache
.set(true);
343 // if we are using the eager solver
344 if (options::bitblastMode() == options::BitblastMode::EAGER
)
346 // this can only happen on an empty benchmark
347 if (!d_eagerSolver
->isInitialized()) {
348 d_eagerSolver
->initialize();
350 if (!Theory::fullEffort(e
))
353 std::vector
<TNode
> assertions
;
355 TNode fact
= get().d_assertion
;
356 Assert(fact
.getKind() == kind::BITVECTOR_EAGER_ATOM
);
357 assertions
.push_back(fact
);
358 d_eagerSolver
->assertFormula(fact
[0]);
361 bool ok
= d_eagerSolver
->checkSat();
363 if (assertions
.size() == 1) {
364 d_out
->conflict(assertions
[0]);
367 Node conflict
= utils::mkAnd(assertions
);
368 d_out
->conflict(conflict
);
374 if (Theory::fullEffort(e
)) {
375 ++(d_statistics
.d_numCallsToCheckFullEffort
);
377 ++(d_statistics
.d_numCallsToCheckStandardEffort
);
379 // if we are already in conflict just return the conflict
386 TNode fact
= get().d_assertion
;
390 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
391 d_subtheories
[i
]->assertFact(fact
);
396 bool complete
= false;
397 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
398 Assert(!inConflict());
399 ok
= d_subtheories
[i
]->check(e
);
400 complete
= d_subtheories
[i
]->isComplete();
403 // if we are in a conflict no need to check with other theories
404 Assert(inConflict());
409 // if the last subtheory was complete we stop
414 //check extended functions
415 if (Theory::fullEffort(e
)) {
416 //do inferences (adds external lemmas) TODO: this can be improved to add internal inferences
417 std::vector
< Node
> nred
;
418 if (d_extTheory
->doInferences(0, nred
))
422 d_needsLastCallCheck
= false;
424 //other inferences involving bv2nat, int2bv
425 if( options::bvAlgExtf() ){
426 if( doExtfInferences( nred
) ){
430 if( !options::bvLazyReduceExtf() ){
431 if( doExtfReductions( nred
) ){
435 d_needsLastCallCheck
= true;
441 bool TheoryBV::doExtfInferences(std::vector
<Node
>& terms
)
443 NodeManager
* nm
= NodeManager::currentNM();
444 bool sentLemma
= false;
445 eq::EqualityEngine
* ee
= getEqualityEngine();
446 std::map
<Node
, Node
> op_map
;
447 for (unsigned j
= 0; j
< terms
.size(); j
++)
450 Assert(n
.getKind() == kind::BITVECTOR_TO_NAT
451 || n
.getKind() == kind::INT_TO_BITVECTOR
);
452 if (n
.getKind() == kind::BITVECTOR_TO_NAT
)
455 if (d_extf_range_infer
.find(n
) == d_extf_range_infer
.end())
457 d_extf_range_infer
.insert(n
);
458 unsigned bvs
= n
[0].getType().getBitVectorSize();
459 Node min
= nm
->mkConst(Rational(0));
460 Node max
= nm
->mkConst(Rational(Integer(1).multiplyByPow2(bvs
)));
461 Node lem
= nm
->mkNode(kind::AND
,
462 nm
->mkNode(kind::GEQ
, n
, min
),
463 nm
->mkNode(kind::LT
, n
, max
));
464 Trace("bv-extf-lemma")
465 << "BV extf lemma (range) : " << lem
<< std::endl
;
470 Node r
= (ee
&& ee
->hasTerm(n
[0])) ? ee
->getRepresentative(n
[0]) : n
[0];
473 for (unsigned j
= 0; j
< terms
.size(); j
++)
476 Node r
= (ee
&& ee
->hasTerm(n
[0])) ? ee
->getRepresentative(n
) : n
;
477 std::map
<Node
, Node
>::iterator it
= op_map
.find(r
);
478 if (it
!= op_map
.end())
480 Node parent
= it
->second
;
481 // Node cterm = parent[0]==n ? parent : nm->mkNode( parent.getOperator(),
483 Node cterm
= parent
[0].eqNode(n
);
484 Trace("bv-extf-lemma-debug")
485 << "BV extf collapse based on : " << cterm
<< std::endl
;
486 if (d_extf_collapse_infer
.find(cterm
) == d_extf_collapse_infer
.end())
488 d_extf_collapse_infer
.insert(cterm
);
491 if (t
.getType() == parent
.getType())
493 if (n
.getKind() == kind::INT_TO_BITVECTOR
)
495 Assert(t
.getType().isInteger());
496 // congruent modulo 2^( bv width )
497 unsigned bvs
= n
.getType().getBitVectorSize();
498 Node coeff
= nm
->mkConst(Rational(Integer(1).multiplyByPow2(bvs
)));
499 Node k
= nm
->mkSkolem(
500 "int_bv_cong", t
.getType(), "for int2bv/bv2nat congruence");
501 t
= nm
->mkNode(kind::PLUS
, t
, nm
->mkNode(kind::MULT
, coeff
, k
));
503 Node lem
= parent
.eqNode(t
);
507 Assert(ee
->areEqual(parent
[0], n
));
508 lem
= nm
->mkNode(kind::IMPLIES
, parent
[0].eqNode(n
), lem
);
510 // this handles inferences of the form, e.g.:
511 // ((_ int2bv w) (bv2nat x)) == x (if x is bit-width w)
512 // (bv2nat ((_ int2bv w) x)) == x + k*2^w for some k
513 Trace("bv-extf-lemma")
514 << "BV extf lemma (collapse) : " << lem
<< std::endl
;
519 Trace("bv-extf-lemma-debug")
520 << "BV extf f collapse based on : " << cterm
<< std::endl
;
526 bool TheoryBV::doExtfReductions( std::vector
< Node
>& terms
) {
527 std::vector
< Node
> nredr
;
528 if (d_extTheory
->doReductions(0, terms
, nredr
))
532 Assert(nredr
.empty());
536 bool TheoryBV::needsCheckLastEffort() {
537 return d_needsLastCallCheck
;
539 bool TheoryBV::collectModelInfo(TheoryModel
* m
)
541 Assert(!inConflict());
542 if (options::bitblastMode() == options::BitblastMode::EAGER
)
544 if (!d_eagerSolver
->collectModelInfo(m
, true))
549 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
550 if (d_subtheories
[i
]->isComplete()) {
551 return d_subtheories
[i
]->collectModelInfo(m
, true);
557 Node
TheoryBV::getModelValue(TNode var
) {
558 Assert(!inConflict());
559 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
560 if (d_subtheories
[i
]->isComplete()) {
561 return d_subtheories
[i
]->getModelValue(var
);
567 void TheoryBV::propagate(Effort e
) {
568 Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl
;
569 if (options::bitblastMode() == options::BitblastMode::EAGER
)
578 // go through stored propagations
580 for (; d_literalsToPropagateIndex
< d_literalsToPropagate
.size() && ok
; d_literalsToPropagateIndex
= d_literalsToPropagateIndex
+ 1) {
581 TNode literal
= d_literalsToPropagate
[d_literalsToPropagateIndex
];
582 // temporary fix for incremental bit-blasting
583 if (d_valuation
.isSatLiteral(literal
)) {
584 Debug("bitvector::propagate") << "TheoryBV:: propagating " << literal
<<"\n";
585 ok
= d_out
->propagate(literal
);
590 Debug("bitvector::propagate") << indent() << "TheoryBV::propagate(): conflict from theory engine" << std::endl
;
595 bool TheoryBV::getCurrentSubstitution( int effort
, std::vector
< Node
>& vars
, std::vector
< Node
>& subs
, std::map
< Node
, std::vector
< Node
> >& exp
) {
596 eq::EqualityEngine
* ee
= getEqualityEngine();
598 //get the constant equivalence classes
600 for( unsigned i
=0; i
<vars
.size(); i
++ ){
602 if( ee
->hasTerm( n
) ){
603 Node nr
= ee
->getRepresentative( n
);
605 subs
.push_back( nr
);
606 exp
[n
].push_back( n
.eqNode( nr
) );
615 //return true if the substitution is non-trivial
621 int TheoryBV::getReduction(int effort
, Node n
, Node
& nr
)
623 Trace("bv-ext") << "TheoryBV::checkExt : non-reduced : " << n
<< std::endl
;
624 if (n
.getKind() == kind::BITVECTOR_TO_NAT
)
626 nr
= utils::eliminateBv2Nat(n
);
629 else if (n
.getKind() == kind::INT_TO_BITVECTOR
)
631 nr
= utils::eliminateInt2Bv(n
);
637 Theory::PPAssertStatus
TheoryBV::ppAssert(TNode in
,
638 SubstitutionMap
& outSubstitutions
)
640 switch (in
.getKind())
644 if (in
[0].isVar() && isLegalElimination(in
[0], in
[1]))
646 ++(d_statistics
.d_solveSubstitutions
);
647 outSubstitutions
.addSubstitution(in
[0], in
[1]);
648 return PP_ASSERT_STATUS_SOLVED
;
650 if (in
[1].isVar() && isLegalElimination(in
[1], in
[0]))
652 ++(d_statistics
.d_solveSubstitutions
);
653 outSubstitutions
.addSubstitution(in
[1], in
[0]);
654 return PP_ASSERT_STATUS_SOLVED
;
656 Node node
= Rewriter::rewrite(in
);
657 if ((node
[0].getKind() == kind::BITVECTOR_EXTRACT
&& node
[1].isConst())
658 || (node
[1].getKind() == kind::BITVECTOR_EXTRACT
659 && node
[0].isConst()))
661 Node extract
= node
[0].isConst() ? node
[1] : node
[0];
662 if (extract
[0].isVar())
664 Node c
= node
[0].isConst() ? node
[0] : node
[1];
666 unsigned high
= utils::getExtractHigh(extract
);
667 unsigned low
= utils::getExtractLow(extract
);
668 unsigned var_bitwidth
= utils::getSize(extract
[0]);
669 std::vector
<Node
> children
;
673 Assert(high
!= var_bitwidth
- 1);
674 unsigned skolem_size
= var_bitwidth
- high
- 1;
675 Node skolem
= utils::mkVar(skolem_size
);
676 children
.push_back(skolem
);
677 children
.push_back(c
);
679 else if (high
== var_bitwidth
- 1)
681 unsigned skolem_size
= low
;
682 Node skolem
= utils::mkVar(skolem_size
);
683 children
.push_back(c
);
684 children
.push_back(skolem
);
688 unsigned skolem1_size
= low
;
689 unsigned skolem2_size
= var_bitwidth
- high
- 1;
690 Node skolem1
= utils::mkVar(skolem1_size
);
691 Node skolem2
= utils::mkVar(skolem2_size
);
692 children
.push_back(skolem2
);
693 children
.push_back(c
);
694 children
.push_back(skolem1
);
696 Node concat
= utils::mkConcat(children
);
697 Assert(utils::getSize(concat
) == utils::getSize(extract
[0]));
698 if (isLegalElimination(extract
[0], concat
))
700 outSubstitutions
.addSubstitution(extract
[0], concat
);
701 return PP_ASSERT_STATUS_SOLVED
;
707 case kind::BITVECTOR_ULT
:
708 case kind::BITVECTOR_SLT
:
709 case kind::BITVECTOR_ULE
:
710 case kind::BITVECTOR_SLE
:
713 // TODO other predicates
716 return PP_ASSERT_STATUS_UNSOLVED
;
719 TrustNode
TheoryBV::ppRewrite(TNode t
)
721 Debug("bv-pp-rewrite") << "TheoryBV::ppRewrite " << t
<< "\n";
723 if (options::bitwiseEq() && RewriteRule
<BitwiseEq
>::applies(t
)) {
724 Node result
= RewriteRule
<BitwiseEq
>::run
<false>(t
);
725 res
= Rewriter::rewrite(result
);
726 } else if (RewriteRule
<UltPlusOne
>::applies(t
)) {
727 Node result
= RewriteRule
<UltPlusOne
>::run
<false>(t
);
728 res
= Rewriter::rewrite(result
);
729 } else if( res
.getKind() == kind::EQUAL
&&
730 ((res
[0].getKind() == kind::BITVECTOR_PLUS
&&
731 RewriteRule
<ConcatToMult
>::applies(res
[1])) ||
732 (res
[1].getKind() == kind::BITVECTOR_PLUS
&&
733 RewriteRule
<ConcatToMult
>::applies(res
[0])))) {
734 Node mult
= RewriteRule
<ConcatToMult
>::applies(res
[0])?
735 RewriteRule
<ConcatToMult
>::run
<false>(res
[0]) :
736 RewriteRule
<ConcatToMult
>::run
<true>(res
[1]);
737 Node factor
= mult
[0];
738 Node sum
= RewriteRule
<ConcatToMult
>::applies(res
[0])? res
[1] : res
[0];
739 Node new_eq
= NodeManager::currentNM()->mkNode(kind::EQUAL
, sum
, mult
);
740 Node rewr_eq
= RewriteRule
<SolveEq
>::run
<true>(new_eq
);
741 if (rewr_eq
[0].isVar() || rewr_eq
[1].isVar()){
742 res
= Rewriter::rewrite(rewr_eq
);
746 } else if (RewriteRule
<SignExtendEqConst
>::applies(t
)) {
747 res
= RewriteRule
<SignExtendEqConst
>::run
<false>(t
);
748 } else if (RewriteRule
<ZeroExtendEqConst
>::applies(t
)) {
749 res
= RewriteRule
<ZeroExtendEqConst
>::run
<false>(t
);
751 else if (RewriteRule
<NormalizeEqPlusNeg
>::applies(t
))
753 res
= RewriteRule
<NormalizeEqPlusNeg
>::run
<false>(t
);
756 // if(t.getKind() == kind::EQUAL &&
757 // ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() ==
758 // kind::BITVECTOR_PLUS) ||
759 // (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() ==
760 // kind::BITVECTOR_PLUS))) {
761 // // if we have an equality between a multiplication and addition
762 // // try to express multiplication in terms of addition
763 // Node mult = t[0].getKind() == kind::BITVECTOR_MULT? t[0] : t[1];
764 // Node add = t[0].getKind() == kind::BITVECTOR_PLUS? t[0] : t[1];
765 // if (RewriteRule<MultSlice>::applies(mult)) {
766 // Node new_mult = RewriteRule<MultSlice>::run<false>(mult);
768 // Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL,
771 // // the simplification can cause the formula to blow up
772 // // only apply if formula reduced
773 // if (d_subtheoryMap.find(SUB_BITBLAST) != d_subtheoryMap.end()) {
774 // BitblastSolver* bv = (BitblastSolver*)d_subtheoryMap[SUB_BITBLAST];
775 // uint64_t old_size = bv->computeAtomWeight(t);
776 // Assert (old_size);
777 // uint64_t new_size = bv->computeAtomWeight(new_eq);
778 // double ratio = ((double)new_size)/old_size;
779 // if (ratio <= 0.4) {
780 // ++(d_statistics.d_numMultSlice);
785 // if (new_eq.getKind() == kind::CONST_BOOLEAN) {
786 // ++(d_statistics.d_numMultSlice);
792 if (options::bvAbstraction() && t
.getType().isBoolean()) {
793 d_abstractionModule
->addInputAtom(res
);
795 Debug("bv-pp-rewrite") << "to " << res
<< "\n";
798 return TrustNode::mkTrustRewrite(t
, res
, nullptr);
800 return TrustNode::null();
803 void TheoryBV::presolve() {
804 Debug("bitvector") << "TheoryBV::presolve" << endl
;
807 static int prop_count
= 0;
809 bool TheoryBV::storePropagation(TNode literal
, SubTheory subtheory
)
811 Debug("bitvector::propagate") << indent() << getSatContext()->getLevel() << " " << "TheoryBV::storePropagation(" << literal
<< ", " << subtheory
<< ")" << std::endl
;
814 // If already in conflict, no more propagation
816 Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal
<< ", " << subtheory
<< "): already in conflict" << std::endl
;
820 // If propagated already, just skip
821 PropagatedMap::const_iterator find
= d_propagatedBy
.find(literal
);
822 if (find
!= d_propagatedBy
.end()) {
825 bool polarity
= literal
.getKind() != kind::NOT
;
826 Node negatedLiteral
= polarity
? literal
.notNode() : (Node
) literal
[0];
827 find
= d_propagatedBy
.find(negatedLiteral
);
828 if (find
!= d_propagatedBy
.end() && (*find
).second
!= subtheory
) {
829 // Safe to ignore this one, subtheory should produce a conflict
833 d_propagatedBy
[literal
] = subtheory
;
836 // Propagate differs depending on the subtheory
837 // * bitblaster needs to be left alone until it's done, otherwise it doesn't
838 // know how to explain
839 // * equality engine can propagate eagerly
840 // TODO(2348): Determine if ok should be set by propagate. If not, remove ok.
841 constexpr bool ok
= true;
842 if (subtheory
== SUB_CORE
) {
843 d_out
->propagate(literal
);
848 d_literalsToPropagate
.push_back(literal
);
852 }/* TheoryBV::propagate(TNode) */
855 void TheoryBV::explain(TNode literal
, std::vector
<TNode
>& assumptions
) {
856 Assert(wasPropagatedBySubtheory(literal
));
857 SubTheory sub
= getPropagatingSubtheory(literal
);
858 d_subtheoryMap
[sub
]->explain(literal
, assumptions
);
861 TrustNode
TheoryBV::explain(TNode node
)
863 Debug("bitvector::explain") << "TheoryBV::explain(" << node
<< ")" << std::endl
;
864 std::vector
<TNode
> assumptions
;
866 // Ask for the explanation
867 explain(node
, assumptions
);
868 // this means that it is something true at level 0
870 if (assumptions
.size() == 0) {
871 explanation
= utils::mkTrue();
875 // return the explanation
876 explanation
= utils::mkAnd(assumptions
);
878 Debug("bitvector::explain") << "TheoryBV::explain(" << node
<< ") => " << explanation
<< std::endl
;
879 Debug("bitvector::explain") << "TheoryBV::explain done. \n";
880 return TrustNode::mkTrustPropExp(node
, explanation
, nullptr);
884 void TheoryBV::addSharedTerm(TNode t
) {
885 Debug("bitvector::sharing") << indent() << "TheoryBV::addSharedTerm(" << t
<< ")" << std::endl
;
886 d_sharedTermsSet
.insert(t
);
887 if (options::bitvectorEqualitySolver()) {
888 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
889 d_subtheories
[i
]->addSharedTerm(t
);
895 EqualityStatus
TheoryBV::getEqualityStatus(TNode a
, TNode b
)
897 if (options::bitblastMode() == options::BitblastMode::EAGER
)
898 return EQUALITY_UNKNOWN
;
899 Assert(options::bitblastMode() == options::BitblastMode::LAZY
);
900 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
901 EqualityStatus status
= d_subtheories
[i
]->getEqualityStatus(a
, b
);
902 if (status
!= EQUALITY_UNKNOWN
) {
906 return EQUALITY_UNKNOWN
; ;
909 void TheoryBV::ppStaticLearn(TNode in
, NodeBuilder
<>& learned
) {
910 if(d_staticLearnCache
.find(in
) != d_staticLearnCache
.end()){
913 d_staticLearnCache
.insert(in
);
915 if (in
.getKind() == kind::EQUAL
) {
916 if((in
[0].getKind() == kind::BITVECTOR_PLUS
&& in
[1].getKind() == kind::BITVECTOR_SHL
) ||
917 (in
[1].getKind() == kind::BITVECTOR_PLUS
&& in
[0].getKind() == kind::BITVECTOR_SHL
)) {
918 TNode p
= in
[0].getKind() == kind::BITVECTOR_PLUS
? in
[0] : in
[1];
919 TNode s
= in
[0].getKind() == kind::BITVECTOR_PLUS
? in
[1] : in
[0];
921 if(p
.getNumChildren() == 2
922 && p
[0].getKind() == kind::BITVECTOR_SHL
923 && p
[1].getKind() == kind::BITVECTOR_SHL
){
924 unsigned size
= utils::getSize(s
);
925 Node one
= utils::mkConst(size
, 1u);
926 if(s
[0] == one
&& p
[0][0] == one
&& p
[1][0] == one
){
927 Node zero
= utils::mkConst(size
, 0u);
930 // (s : 1 << S) = (b : 1 << B) + (c : 1 << C)
931 Node b_eq_0
= b
.eqNode(zero
);
932 Node c_eq_0
= c
.eqNode(zero
);
933 Node b_eq_c
= b
.eqNode(c
);
935 Node dis
= NodeManager::currentNM()->mkNode(
936 kind::OR
, b_eq_0
, c_eq_0
, b_eq_c
);
937 Node imp
= in
.impNode(dis
);
942 }else if(in
.getKind() == kind::AND
){
943 for(size_t i
= 0, N
= in
.getNumChildren(); i
< N
; ++i
){
944 ppStaticLearn(in
[i
], learned
);
949 bool TheoryBV::applyAbstraction(const std::vector
<Node
>& assertions
, std::vector
<Node
>& new_assertions
) {
950 bool changed
= d_abstractionModule
->applyAbstraction(assertions
, new_assertions
);
951 if (changed
&& options::bitblastMode() == options::BitblastMode::EAGER
952 && options::bitvectorAig())
955 AlwaysAssert(!d_eagerSolver
->isInitialized());
956 d_eagerSolver
->turnOffAig();
957 d_eagerSolver
->initialize();
962 void TheoryBV::setProofLog(proof::BitVectorProof
* bvp
)
964 if (options::bitblastMode() == options::BitblastMode::EAGER
)
966 d_eagerSolver
->setProofLog(bvp
);
970 for( unsigned i
=0; i
< d_subtheories
.size(); i
++ ){
971 d_subtheories
[i
]->setProofLog( bvp
);
976 void TheoryBV::setConflict(Node conflict
)
978 if (options::bvAbstraction())
980 NodeManager
* const nm
= NodeManager::currentNM();
981 Node new_conflict
= d_abstractionModule
->simplifyConflict(conflict
);
983 std::vector
<Node
> lemmas
;
984 lemmas
.push_back(new_conflict
);
985 d_abstractionModule
->generalizeConflict(new_conflict
, lemmas
);
986 for (unsigned i
= 0; i
< lemmas
.size(); ++i
)
988 lemma(nm
->mkNode(kind::NOT
, lemmas
[i
]));
992 d_conflictNode
= conflict
;
995 } /* namespace CVC4::theory::bv */
996 } /* namespace CVC4::theory */
997 } /* namespace CVC4 */