1 /********************* */
2 /*! \file theory_bv.cpp
4 ** Top contributors (to current version):
5 ** Liana Hadarean, Aina Niemetz, Andrew Reynolds
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
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 "smt/smt_statistics_registry.h"
21 #include "theory/bv/abstraction.h"
22 #include "theory/bv/bv_eager_solver.h"
23 #include "theory/bv/bv_subtheory_algebraic.h"
24 #include "theory/bv/bv_subtheory_bitblast.h"
25 #include "theory/bv/bv_subtheory_core.h"
26 #include "theory/bv/bv_subtheory_inequality.h"
27 #include "theory/bv/slicer.h"
28 #include "theory/bv/theory_bv_rewrite_rules_normalization.h"
29 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
30 #include "theory/bv/theory_bv_rewriter.h"
31 #include "theory/bv/theory_bv_utils.h"
32 #include "theory/theory_model.h"
33 #include "proof/theory_proof.h"
34 #include "proof/proof_manager.h"
35 #include "theory/valuation.h"
37 using namespace CVC4::context
;
38 using namespace CVC4::theory::bv::utils
;
45 TheoryBV::TheoryBV(context::Context
* c
, context::UserContext
* u
,
46 OutputChannel
& out
, Valuation valuation
,
47 const LogicInfo
& logicInfo
, std::string name
)
48 : Theory(THEORY_BV
, c
, u
, out
, valuation
, logicInfo
, name
),
50 d_alreadyPropagatedSet(c
),
60 d_lemmasAdded(c
, false),
62 d_invalidateModelCache(c
, true),
63 d_literalsToPropagate(c
),
64 d_literalsToPropagateIndex(c
, 0),
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
)
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(this);
82 if (options::bitvectorEqualitySolver() && !options::proof())
84 SubtheorySolver
* core_solver
= new CoreSolver(c
, this);
85 d_subtheories
.push_back(core_solver
);
86 d_subtheoryMap
[SUB_CORE
] = core_solver
;
89 if (options::bitvectorInequalitySolver() && !options::proof())
91 SubtheorySolver
* ineq_solver
= new InequalitySolver(c
, u
, this);
92 d_subtheories
.push_back(ineq_solver
);
93 d_subtheoryMap
[SUB_INEQUALITY
] = ineq_solver
;
96 if (options::bitvectorAlgebraicSolver() && !options::proof())
98 SubtheorySolver
* alg_solver
= new AlgebraicSolver(c
, this);
99 d_subtheories
.push_back(alg_solver
);
100 d_subtheoryMap
[SUB_ALGEBRAIC
] = alg_solver
;
103 BitblastSolver
* bb_solver
= new BitblastSolver(c
, this);
104 if (options::bvAbstraction()) {
105 bb_solver
->setAbstraction(d_abstractionModule
);
107 d_subtheories
.push_back(bb_solver
);
108 d_subtheoryMap
[SUB_BITBLAST
] = bb_solver
;
111 TheoryBV::~TheoryBV() {
113 delete d_eagerSolver
;
115 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
116 delete d_subtheories
[i
];
118 delete d_abstractionModule
;
121 void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine
* eq
) {
122 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
125 if (options::bitvectorEqualitySolver()) {
126 dynamic_cast<CoreSolver
*>(d_subtheoryMap
[SUB_CORE
])->setMasterEqualityEngine(eq
);
130 void TheoryBV::spendResource(unsigned amount
)
132 getOutputChannel().spendResource(amount
);
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)
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
);
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
);
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
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
;
175 return d_BVDivByZero
[width
];
177 else if (k
== kind::BITVECTOR_UREM
) {
178 if (d_BVRemByZero
.find(width
) == d_BVRemByZero
.end()) {
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
;
186 return d_BVRemByZero
[width
];
193 void TheoryBV::collectFunctionSymbols(TNode term
, TNodeSet
& seen
) {
194 if (seen
.find(term
) != seen
.end())
196 if (term
.getKind() == kind::APPLY_UF
) {
197 TNode func
= term
.getOperator();
198 storeFunction(func
, term
);
199 } else if (term
.getKind() == kind::SELECT
) {
200 TNode func
= term
[0];
201 storeFunction(func
, term
);
202 } else if (term
.getKind() == kind::STORE
) {
203 AlwaysAssert(false, "Cannot use eager bitblasting on QF_ABV formula with stores");
205 for (unsigned i
= 0; i
< term
.getNumChildren(); ++i
) {
206 collectFunctionSymbols(term
[i
], seen
);
211 void TheoryBV::storeFunction(TNode func
, TNode term
) {
212 if (d_funcToArgs
.find(func
) == d_funcToArgs
.end()) {
213 d_funcToArgs
.insert(make_pair(func
, NodeSet()));
215 NodeSet
& set
= d_funcToArgs
[func
];
216 if (set
.find(term
) == set
.end()) {
218 Node skolem
= utils::mkVar(utils::getSize(term
));
219 d_funcToSkolem
.addSubstitution(term
, skolem
);
223 void TheoryBV::mkAckermanizationAssertions(std::vector
<Node
>& assertions
) {
224 Debug("bv-ackermanize") << "TheoryBV::mkAckermanizationAssertions\n";
226 Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
);
227 AlwaysAssert(!options::incrementalSolving());
229 for (unsigned i
= 0; i
< assertions
.size(); ++i
) {
230 collectFunctionSymbols(assertions
[i
], seen
);
233 FunctionToArgs::const_iterator it
= d_funcToArgs
.begin();
234 NodeManager
* nm
= NodeManager::currentNM();
235 for (; it
!= d_funcToArgs
.end(); ++it
) {
236 TNode func
= it
->first
;
237 const NodeSet
& args
= it
->second
;
238 NodeSet::const_iterator it1
= args
.begin();
239 for ( ; it1
!= args
.end(); ++it1
) {
240 for(NodeSet::const_iterator it2
= it1
; it2
!= args
.end(); ++it2
) {
245 if (args1
.getKind() == kind::APPLY_UF
) {
246 AlwaysAssert (args1
.getKind() == kind::APPLY_UF
&&
247 args1
.getOperator() == func
);
248 AlwaysAssert (args2
.getKind() == kind::APPLY_UF
&&
249 args2
.getOperator() == func
);
250 AlwaysAssert (args1
.getNumChildren() == args2
.getNumChildren());
252 std::vector
<Node
> eqs(args1
.getNumChildren());
254 for (unsigned i
= 0; i
< args1
.getNumChildren(); ++i
) {
255 eqs
[i
] = nm
->mkNode(kind::EQUAL
, args1
[i
], args2
[i
]);
257 args_eq
= utils::mkAnd(eqs
);
259 AlwaysAssert (args1
.getKind() == kind::SELECT
&&
261 AlwaysAssert (args2
.getKind() == kind::SELECT
&&
263 AlwaysAssert (args1
.getNumChildren() == 2);
264 AlwaysAssert (args2
.getNumChildren() == 2);
265 args_eq
= nm
->mkNode(kind::EQUAL
, args1
[1], args2
[1]);
267 Node func_eq
= nm
->mkNode(kind::EQUAL
, args1
, args2
);
268 Node lemma
= nm
->mkNode(kind::IMPLIES
, args_eq
, func_eq
);
269 assertions
.push_back(lemma
);
274 // replace applications of UF by skolems (FIXME for model building)
275 for(unsigned i
= 0; i
< assertions
.size(); ++i
) {
276 assertions
[i
] = d_funcToSkolem
.apply(assertions
[i
]);
280 Node
TheoryBV::expandDefinition(LogicRequest
&logicRequest
, Node node
) {
281 Debug("bitvector-expandDefinition") << "TheoryBV::expandDefinition(" << node
<< ")" << std::endl
;
283 switch (node
.getKind()) {
284 case kind::BITVECTOR_SDIV
:
285 case kind::BITVECTOR_SREM
:
286 case kind::BITVECTOR_SMOD
:
287 return TheoryBVRewriter::eliminateBVSDiv(node
);
290 case kind::BITVECTOR_UDIV
:
291 case kind::BITVECTOR_UREM
: {
292 NodeManager
* nm
= NodeManager::currentNM();
293 unsigned width
= node
.getType().getBitVectorSize();
295 if (options::bitvectorDivByZeroConst()) {
296 Kind kind
= node
.getKind() == kind::BITVECTOR_UDIV
? kind::BITVECTOR_UDIV_TOTAL
: kind::BITVECTOR_UREM_TOTAL
;
297 return nm
->mkNode(kind
, node
[0], node
[1]);
300 TNode num
= node
[0], den
= node
[1];
301 Node den_eq_0
= nm
->mkNode(kind::EQUAL
, den
, utils::mkZero(width
));
302 Node divTotalNumDen
= nm
->mkNode(node
.getKind() == kind::BITVECTOR_UDIV
? kind::BITVECTOR_UDIV_TOTAL
:
303 kind::BITVECTOR_UREM_TOTAL
, num
, den
);
305 // if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
306 // // Ackermanize UF if using eager bit-blasting
307 // Node ackerman_var = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_ACKERMANIZE_UDIV : kind::BITVECTOR_ACKERMANIZE_UREM, num);
308 // node = nm->mkNode(kind::ITE, den_eq_0, ackerman_var, divTotalNumDen);
311 Node divByZero
= getBVDivByZero(node
.getKind(), width
);
312 Node divByZeroNum
= nm
->mkNode(kind::APPLY_UF
, divByZero
, num
);
313 node
= nm
->mkNode(kind::ITE
, den_eq_0
, divByZeroNum
, divTotalNumDen
);
314 logicRequest
.widenLogic(THEORY_UF
);
329 void TheoryBV::preRegisterTerm(TNode node
) {
330 d_calledPreregister
= true;
331 Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node
<< ")" << std::endl
;
333 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
334 // the aig bit-blaster option is set heuristically
335 // if bv abstraction is not used
336 if (!d_eagerSolver
->isInitialized()) {
337 d_eagerSolver
->initialize();
340 if (node
.getKind() == kind::BITVECTOR_EAGER_ATOM
) {
341 Node formula
= node
[0];
342 d_eagerSolver
->assertFormula(formula
);
344 // nothing to do for the other terms
348 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
349 d_subtheories
[i
]->preRegister(node
);
352 // AJR : equality solver currently registers all terms to ExtTheory, if we want a lazy reduction without the bv equality solver, need to call this
353 //getExtTheory()->registerTermRec( node );
356 void TheoryBV::sendConflict() {
358 if (d_conflictNode
.isNull()) {
361 Debug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode
<< std::endl
;
362 d_out
->conflict(d_conflictNode
);
363 d_statistics
.d_avgConflictSize
.addEntry(d_conflictNode
.getNumChildren());
364 d_conflictNode
= Node::null();
368 void TheoryBV::checkForLemma(TNode fact
)
370 if (fact
.getKind() == kind::EQUAL
)
372 NodeManager
* nm
= NodeManager::currentNM();
373 if (fact
[0].getKind() == kind::BITVECTOR_UREM_TOTAL
)
375 TNode urem
= fact
[0];
376 TNode result
= fact
[1];
377 TNode divisor
= urem
[1];
378 Node result_ult_div
= nm
->mkNode(kind::BITVECTOR_ULT
, result
, divisor
);
380 nm
->mkNode(kind::EQUAL
, divisor
, mkZero(getSize(divisor
)));
381 Node split
= nm
->mkNode(
382 kind::OR
, divisor_eq_0
, nm
->mkNode(kind::NOT
, fact
), result_ult_div
);
385 if (fact
[1].getKind() == kind::BITVECTOR_UREM_TOTAL
)
387 TNode urem
= fact
[1];
388 TNode result
= fact
[0];
389 TNode divisor
= urem
[1];
390 Node result_ult_div
= nm
->mkNode(kind::BITVECTOR_ULT
, result
, divisor
);
392 nm
->mkNode(kind::EQUAL
, divisor
, mkZero(getSize(divisor
)));
393 Node split
= nm
->mkNode(
394 kind::OR
, divisor_eq_0
, nm
->mkNode(kind::NOT
, fact
), result_ult_div
);
400 void TheoryBV::check(Effort e
)
402 if (done() && e
<Theory::EFFORT_FULL
) {
406 //last call : do reductions on extended bitvector functions
407 if (e
== Theory::EFFORT_LAST_CALL
) {
408 std::vector
<Node
> nred
= getExtTheory()->getActive();
409 doExtfReductions(nred
);
413 TimerStat::CodeTimer
checkTimer(d_checkTime
);
414 Debug("bitvector") << "TheoryBV::check(" << e
<< ")" << std::endl
;
415 TimerStat::CodeTimer
codeTimer(d_statistics
.d_solveTimer
);
416 // we may be getting new assertions so the model cache may not be sound
417 d_invalidateModelCache
.set(true);
418 // if we are using the eager solver
419 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
420 // this can only happen on an empty benchmark
421 if (!d_eagerSolver
->isInitialized()) {
422 d_eagerSolver
->initialize();
424 if (!Theory::fullEffort(e
))
427 std::vector
<TNode
> assertions
;
429 TNode fact
= get().assertion
;
430 Assert (fact
.getKind() == kind::BITVECTOR_EAGER_ATOM
);
431 assertions
.push_back(fact
);
433 Assert (d_eagerSolver
->hasAssertions(assertions
));
435 bool ok
= d_eagerSolver
->checkSat();
437 if (assertions
.size() == 1) {
438 d_out
->conflict(assertions
[0]);
441 Node conflict
= utils::mkAnd(assertions
);
442 d_out
->conflict(conflict
);
449 if (Theory::fullEffort(e
)) {
450 ++(d_statistics
.d_numCallsToCheckFullEffort
);
452 ++(d_statistics
.d_numCallsToCheckStandardEffort
);
454 // if we are already in conflict just return the conflict
461 TNode fact
= get().assertion
;
465 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
466 d_subtheories
[i
]->assertFact(fact
);
471 bool complete
= false;
472 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
473 Assert (!inConflict());
474 ok
= d_subtheories
[i
]->check(e
);
475 complete
= d_subtheories
[i
]->isComplete();
478 // if we are in a conflict no need to check with other theories
479 Assert (inConflict());
484 // if the last subtheory was complete we stop
489 //check extended functions
490 if (Theory::fullEffort(e
)) {
491 //do inferences (adds external lemmas) TODO: this can be improved to add internal inferences
492 std::vector
< Node
> nred
;
493 if( getExtTheory()->doInferences( 0, nred
) ){
496 d_needsLastCallCheck
= false;
498 //other inferences involving bv2nat, int2bv
499 if( options::bvAlgExtf() ){
500 if( doExtfInferences( nred
) ){
504 if( !options::bvLazyReduceExtf() ){
505 if( doExtfReductions( nred
) ){
509 d_needsLastCallCheck
= true;
515 bool TheoryBV::doExtfInferences(std::vector
<Node
>& terms
)
517 NodeManager
* nm
= NodeManager::currentNM();
518 bool sentLemma
= false;
519 eq::EqualityEngine
* ee
= getEqualityEngine();
520 std::map
<Node
, Node
> op_map
;
521 for (unsigned j
= 0; j
< terms
.size(); j
++)
524 Assert(n
.getKind() == kind::BITVECTOR_TO_NAT
525 || n
.getKind() == kind::INT_TO_BITVECTOR
);
526 if (n
.getKind() == kind::BITVECTOR_TO_NAT
)
529 if (d_extf_range_infer
.find(n
) == d_extf_range_infer
.end())
531 d_extf_range_infer
.insert(n
);
532 unsigned bvs
= n
[0].getType().getBitVectorSize();
533 Node min
= nm
->mkConst(Rational(0));
534 Node max
= nm
->mkConst(Rational(Integer(1).multiplyByPow2(bvs
)));
535 Node lem
= nm
->mkNode(kind::AND
,
536 nm
->mkNode(kind::GEQ
, n
, min
),
537 nm
->mkNode(kind::LT
, n
, max
));
538 Trace("bv-extf-lemma")
539 << "BV extf lemma (range) : " << lem
<< std::endl
;
544 Node r
= (ee
&& ee
->hasTerm(n
[0])) ? ee
->getRepresentative(n
[0]) : n
[0];
547 for (unsigned j
= 0; j
< terms
.size(); j
++)
550 Node r
= (ee
&& ee
->hasTerm(n
[0])) ? ee
->getRepresentative(n
) : n
;
551 std::map
<Node
, Node
>::iterator it
= op_map
.find(r
);
552 if (it
!= op_map
.end())
554 Node parent
= it
->second
;
555 // Node cterm = parent[0]==n ? parent : nm->mkNode( parent.getOperator(),
557 Node cterm
= parent
[0].eqNode(n
);
558 Trace("bv-extf-lemma-debug")
559 << "BV extf collapse based on : " << cterm
<< std::endl
;
560 if (d_extf_collapse_infer
.find(cterm
) == d_extf_collapse_infer
.end())
562 d_extf_collapse_infer
.insert(cterm
);
565 if (n
.getKind() == kind::INT_TO_BITVECTOR
)
567 Assert(t
.getType().isInteger());
568 // congruent modulo 2^( bv width )
569 unsigned bvs
= n
.getType().getBitVectorSize();
570 Node coeff
= nm
->mkConst(Rational(Integer(1).multiplyByPow2(bvs
)));
571 Node k
= nm
->mkSkolem(
572 "int_bv_cong", t
.getType(), "for int2bv/bv2nat congruence");
573 t
= nm
->mkNode(kind::PLUS
, t
, nm
->mkNode(kind::MULT
, coeff
, k
));
575 Node lem
= parent
.eqNode(t
);
579 Assert(ee
->areEqual(parent
[0], n
));
580 lem
= nm
->mkNode(kind::IMPLIES
, parent
[0].eqNode(n
), lem
);
582 Trace("bv-extf-lemma")
583 << "BV extf lemma (collapse) : " << lem
<< std::endl
;
592 bool TheoryBV::doExtfReductions( std::vector
< Node
>& terms
) {
593 std::vector
< Node
> nredr
;
594 if( getExtTheory()->doReductions( 0, terms
, nredr
) ){
597 Assert( nredr
.empty() );
601 bool TheoryBV::needsCheckLastEffort() {
602 return d_needsLastCallCheck
;
604 bool TheoryBV::collectModelInfo(TheoryModel
* m
)
606 Assert(!inConflict());
607 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
608 if (!d_eagerSolver
->collectModelInfo(m
, true))
613 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
614 if (d_subtheories
[i
]->isComplete()) {
615 return d_subtheories
[i
]->collectModelInfo(m
, true);
621 Node
TheoryBV::getModelValue(TNode var
) {
622 Assert(!inConflict());
623 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
624 if (d_subtheories
[i
]->isComplete()) {
625 return d_subtheories
[i
]->getModelValue(var
);
631 void TheoryBV::propagate(Effort e
) {
632 Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl
;
633 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
641 // go through stored propagations
643 for (; d_literalsToPropagateIndex
< d_literalsToPropagate
.size() && ok
; d_literalsToPropagateIndex
= d_literalsToPropagateIndex
+ 1) {
644 TNode literal
= d_literalsToPropagate
[d_literalsToPropagateIndex
];
645 // temporary fix for incremental bit-blasting
646 if (d_valuation
.isSatLiteral(literal
)) {
647 Debug("bitvector::propagate") << "TheoryBV:: propagating " << literal
<<"\n";
648 ok
= d_out
->propagate(literal
);
653 Debug("bitvector::propagate") << indent() << "TheoryBV::propagate(): conflict from theory engine" << std::endl
;
659 eq::EqualityEngine
* TheoryBV::getEqualityEngine() {
660 CoreSolver
* core
= (CoreSolver
*)d_subtheoryMap
[SUB_CORE
];
662 return core
->getEqualityEngine();
668 bool TheoryBV::getCurrentSubstitution( int effort
, std::vector
< Node
>& vars
, std::vector
< Node
>& subs
, std::map
< Node
, std::vector
< Node
> >& exp
) {
669 eq::EqualityEngine
* ee
= getEqualityEngine();
671 //get the constant equivalence classes
673 for( unsigned i
=0; i
<vars
.size(); i
++ ){
675 if( ee
->hasTerm( n
) ){
676 Node nr
= ee
->getRepresentative( n
);
678 subs
.push_back( nr
);
679 exp
[n
].push_back( n
.eqNode( nr
) );
688 //return true if the substitution is non-trivial
694 int TheoryBV::getReduction(int effort
, Node n
, Node
& nr
)
696 Trace("bv-ext") << "TheoryBV::checkExt : non-reduced : " << n
<< std::endl
;
697 NodeManager
* const nm
= NodeManager::currentNM();
698 if (n
.getKind() == kind::BITVECTOR_TO_NAT
)
700 // taken from rewrite code
701 const unsigned size
= utils::getSize(n
[0]);
702 const Node z
= nm
->mkConst(Rational(0));
703 const Node bvone
= utils::mkOne(1);
704 NodeBuilder
<> result(kind::PLUS
);
706 for (unsigned bit
= 0; bit
< size
; ++bit
, i
*= 2)
709 nm
->mkNode(kind::EQUAL
,
710 nm
->mkNode(nm
->mkConst(BitVectorExtract(bit
, bit
)), n
[0]),
712 result
<< nm
->mkNode(kind::ITE
, cond
, nm
->mkConst(Rational(i
)), z
);
717 else if (n
.getKind() == kind::INT_TO_BITVECTOR
)
719 // taken from rewrite code
720 const unsigned size
= n
.getOperator().getConst
<IntToBitVector
>().size
;
721 const Node bvzero
= utils::mkZero(1);
722 const Node bvone
= utils::mkOne(1);
725 while (v
.size() < size
)
727 Node cond
= nm
->mkNode(
729 nm
->mkNode(kind::INTS_MODULUS_TOTAL
, n
[0], nm
->mkConst(Rational(i
))),
730 nm
->mkConst(Rational(i
, 2)));
731 cond
= Rewriter::rewrite(cond
);
732 v
.push_back(nm
->mkNode(kind::ITE
, cond
, bvone
, bvzero
));
735 NodeBuilder
<> result(kind::BITVECTOR_CONCAT
);
736 result
.append(v
.rbegin(), v
.rend());
743 Theory::PPAssertStatus
TheoryBV::ppAssert(TNode in
,
744 SubstitutionMap
& outSubstitutions
)
746 switch (in
.getKind())
750 if (in
[0].isVar() && !in
[1].hasSubterm(in
[0]))
752 ++(d_statistics
.d_solveSubstitutions
);
753 outSubstitutions
.addSubstitution(in
[0], in
[1]);
754 return PP_ASSERT_STATUS_SOLVED
;
756 if (in
[1].isVar() && !in
[0].hasSubterm(in
[1]))
758 ++(d_statistics
.d_solveSubstitutions
);
759 outSubstitutions
.addSubstitution(in
[1], in
[0]);
760 return PP_ASSERT_STATUS_SOLVED
;
762 Node node
= Rewriter::rewrite(in
);
763 if ((node
[0].getKind() == kind::BITVECTOR_EXTRACT
&& node
[1].isConst())
764 || (node
[1].getKind() == kind::BITVECTOR_EXTRACT
765 && node
[0].isConst()))
767 Node extract
= node
[0].isConst() ? node
[1] : node
[0];
768 if (extract
[0].getKind() == kind::VARIABLE
)
770 Node c
= node
[0].isConst() ? node
[0] : node
[1];
772 unsigned high
= utils::getExtractHigh(extract
);
773 unsigned low
= utils::getExtractLow(extract
);
774 unsigned var_bitwidth
= utils::getSize(extract
[0]);
775 std::vector
<Node
> children
;
779 Assert(high
!= var_bitwidth
- 1);
780 unsigned skolem_size
= var_bitwidth
- high
- 1;
781 Node skolem
= utils::mkVar(skolem_size
);
782 children
.push_back(skolem
);
783 children
.push_back(c
);
785 else if (high
== var_bitwidth
- 1)
787 unsigned skolem_size
= low
;
788 Node skolem
= utils::mkVar(skolem_size
);
789 children
.push_back(c
);
790 children
.push_back(skolem
);
794 unsigned skolem1_size
= low
;
795 unsigned skolem2_size
= var_bitwidth
- high
- 1;
796 Node skolem1
= utils::mkVar(skolem1_size
);
797 Node skolem2
= utils::mkVar(skolem2_size
);
798 children
.push_back(skolem2
);
799 children
.push_back(c
);
800 children
.push_back(skolem1
);
802 Node concat
= utils::mkConcat(children
);
803 Assert(utils::getSize(concat
) == utils::getSize(extract
[0]));
804 outSubstitutions
.addSubstitution(extract
[0], concat
);
805 return PP_ASSERT_STATUS_SOLVED
;
810 case kind::BITVECTOR_ULT
:
811 case kind::BITVECTOR_SLT
:
812 case kind::BITVECTOR_ULE
:
813 case kind::BITVECTOR_SLE
:
816 // TODO other predicates
819 return PP_ASSERT_STATUS_UNSOLVED
;
822 Node
TheoryBV::ppRewrite(TNode t
)
824 Debug("bv-pp-rewrite") << "TheoryBV::ppRewrite " << t
<< "\n";
826 if (RewriteRule
<BitwiseEq
>::applies(t
)) {
827 Node result
= RewriteRule
<BitwiseEq
>::run
<false>(t
);
828 res
= Rewriter::rewrite(result
);
829 } else if (d_isCoreTheory
&& t
.getKind() == kind::EQUAL
) {
830 std::vector
<Node
> equalities
;
831 Slicer::splitEqualities(t
, equalities
);
832 res
= utils::mkAnd(equalities
);
833 } else if (RewriteRule
<UltPlusOne
>::applies(t
)) {
834 Node result
= RewriteRule
<UltPlusOne
>::run
<false>(t
);
835 res
= Rewriter::rewrite(result
);
836 } else if( res
.getKind() == kind::EQUAL
&&
837 ((res
[0].getKind() == kind::BITVECTOR_PLUS
&&
838 RewriteRule
<ConcatToMult
>::applies(res
[1])) ||
839 (res
[1].getKind() == kind::BITVECTOR_PLUS
&&
840 RewriteRule
<ConcatToMult
>::applies(res
[0])))) {
841 Node mult
= RewriteRule
<ConcatToMult
>::applies(res
[0])?
842 RewriteRule
<ConcatToMult
>::run
<false>(res
[0]) :
843 RewriteRule
<ConcatToMult
>::run
<true>(res
[1]);
844 Node factor
= mult
[0];
845 Node sum
= RewriteRule
<ConcatToMult
>::applies(res
[0])? res
[1] : res
[0];
846 Node new_eq
= NodeManager::currentNM()->mkNode(kind::EQUAL
, sum
, mult
);
847 Node rewr_eq
= RewriteRule
<SolveEq
>::run
<true>(new_eq
);
848 if (rewr_eq
[0].isVar() || rewr_eq
[1].isVar()){
849 res
= Rewriter::rewrite(rewr_eq
);
853 } else if (RewriteRule
<SignExtendEqConst
>::applies(t
)) {
854 res
= RewriteRule
<SignExtendEqConst
>::run
<false>(t
);
855 } else if (RewriteRule
<ZeroExtendEqConst
>::applies(t
)) {
856 res
= RewriteRule
<ZeroExtendEqConst
>::run
<false>(t
);
859 // if(t.getKind() == kind::EQUAL &&
860 // ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() ==
861 // kind::BITVECTOR_PLUS) ||
862 // (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() ==
863 // kind::BITVECTOR_PLUS))) {
864 // // if we have an equality between a multiplication and addition
865 // // try to express multiplication in terms of addition
866 // Node mult = t[0].getKind() == kind::BITVECTOR_MULT? t[0] : t[1];
867 // Node add = t[0].getKind() == kind::BITVECTOR_PLUS? t[0] : t[1];
868 // if (RewriteRule<MultSlice>::applies(mult)) {
869 // Node new_mult = RewriteRule<MultSlice>::run<false>(mult);
871 // Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL,
874 // // the simplification can cause the formula to blow up
875 // // only apply if formula reduced
876 // if (d_subtheoryMap.find(SUB_BITBLAST) != d_subtheoryMap.end()) {
877 // BitblastSolver* bv = (BitblastSolver*)d_subtheoryMap[SUB_BITBLAST];
878 // uint64_t old_size = bv->computeAtomWeight(t);
879 // Assert (old_size);
880 // uint64_t new_size = bv->computeAtomWeight(new_eq);
881 // double ratio = ((double)new_size)/old_size;
882 // if (ratio <= 0.4) {
883 // ++(d_statistics.d_numMultSlice);
888 // if (new_eq.getKind() == kind::CONST_BOOLEAN) {
889 // ++(d_statistics.d_numMultSlice);
895 if (options::bvAbstraction() && t
.getType().isBoolean()) {
896 d_abstractionModule
->addInputAtom(res
);
898 Debug("bv-pp-rewrite") << "to " << res
<< "\n";
902 void TheoryBV::presolve() {
903 Debug("bitvector") << "TheoryBV::presolve" << endl
;
906 static int prop_count
= 0;
908 bool TheoryBV::storePropagation(TNode literal
, SubTheory subtheory
)
910 Debug("bitvector::propagate") << indent() << getSatContext()->getLevel() << " " << "TheoryBV::storePropagation(" << literal
<< ", " << subtheory
<< ")" << std::endl
;
913 // If already in conflict, no more propagation
915 Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal
<< ", " << subtheory
<< "): already in conflict" << std::endl
;
919 // If propagated already, just skip
920 PropagatedMap::const_iterator find
= d_propagatedBy
.find(literal
);
921 if (find
!= d_propagatedBy
.end()) {
924 bool polarity
= literal
.getKind() != kind::NOT
;
925 Node negatedLiteral
= polarity
? literal
.notNode() : (Node
) literal
[0];
926 find
= d_propagatedBy
.find(negatedLiteral
);
927 if (find
!= d_propagatedBy
.end() && (*find
).second
!= subtheory
) {
928 // Safe to ignore this one, subtheory should produce a conflict
932 d_propagatedBy
[literal
] = subtheory
;
935 // Propagate differs depending on the subtheory
936 // * bitblaster needs to be left alone until it's done, otherwise it doesn't know how to explain
937 // * equality engine can propagate eagerly
939 if (subtheory
== SUB_CORE
) {
940 d_out
->propagate(literal
);
945 d_literalsToPropagate
.push_back(literal
);
949 }/* TheoryBV::propagate(TNode) */
952 void TheoryBV::explain(TNode literal
, std::vector
<TNode
>& assumptions
) {
953 Assert (wasPropagatedBySubtheory(literal
));
954 SubTheory sub
= getPropagatingSubtheory(literal
);
955 d_subtheoryMap
[sub
]->explain(literal
, assumptions
);
959 Node
TheoryBV::explain(TNode node
) {
960 Debug("bitvector::explain") << "TheoryBV::explain(" << node
<< ")" << std::endl
;
961 std::vector
<TNode
> assumptions
;
963 // Ask for the explanation
964 explain(node
, assumptions
);
965 // this means that it is something true at level 0
966 if (assumptions
.size() == 0) {
967 return utils::mkTrue();
969 // return the explanation
970 Node explanation
= utils::mkAnd(assumptions
);
971 Debug("bitvector::explain") << "TheoryBV::explain(" << node
<< ") => " << explanation
<< std::endl
;
972 Debug("bitvector::explain") << "TheoryBV::explain done. \n";
977 void TheoryBV::addSharedTerm(TNode t
) {
978 Debug("bitvector::sharing") << indent() << "TheoryBV::addSharedTerm(" << t
<< ")" << std::endl
;
979 d_sharedTermsSet
.insert(t
);
980 if (options::bitvectorEqualitySolver()) {
981 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
982 d_subtheories
[i
]->addSharedTerm(t
);
988 EqualityStatus
TheoryBV::getEqualityStatus(TNode a
, TNode b
)
990 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
)
991 return EQUALITY_UNKNOWN
;
992 Assert (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY
);
993 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
994 EqualityStatus status
= d_subtheories
[i
]->getEqualityStatus(a
, b
);
995 if (status
!= EQUALITY_UNKNOWN
) {
999 return EQUALITY_UNKNOWN
; ;
1003 void TheoryBV::enableCoreTheorySlicer() {
1004 Assert (!d_calledPreregister
);
1005 d_isCoreTheory
= true;
1006 if (d_subtheoryMap
.find(SUB_CORE
) != d_subtheoryMap
.end()) {
1007 CoreSolver
* core
= (CoreSolver
*)d_subtheoryMap
[SUB_CORE
];
1008 core
->enableSlicer();
1013 void TheoryBV::ppStaticLearn(TNode in
, NodeBuilder
<>& learned
) {
1014 if(d_staticLearnCache
.find(in
) != d_staticLearnCache
.end()){
1017 d_staticLearnCache
.insert(in
);
1019 if (in
.getKind() == kind::EQUAL
) {
1020 if((in
[0].getKind() == kind::BITVECTOR_PLUS
&& in
[1].getKind() == kind::BITVECTOR_SHL
) ||
1021 (in
[1].getKind() == kind::BITVECTOR_PLUS
&& in
[0].getKind() == kind::BITVECTOR_SHL
)) {
1022 TNode p
= in
[0].getKind() == kind::BITVECTOR_PLUS
? in
[0] : in
[1];
1023 TNode s
= in
[0].getKind() == kind::BITVECTOR_PLUS
? in
[1] : in
[0];
1025 if(p
.getNumChildren() == 2
1026 && p
[0].getKind() == kind::BITVECTOR_SHL
1027 && p
[1].getKind() == kind::BITVECTOR_SHL
){
1028 unsigned size
= utils::getSize(s
);
1029 Node one
= utils::mkConst(size
, 1u);
1030 if(s
[0] == one
&& p
[0][0] == one
&& p
[1][0] == one
){
1031 Node zero
= utils::mkConst(size
, 0u);
1034 // (s : 1 << S) = (b : 1 << B) + (c : 1 << C)
1035 Node b_eq_0
= b
.eqNode(zero
);
1036 Node c_eq_0
= c
.eqNode(zero
);
1037 Node b_eq_c
= b
.eqNode(c
);
1039 Node dis
= NodeManager::currentNM()->mkNode(
1040 kind::OR
, b_eq_0
, c_eq_0
, b_eq_c
);
1041 Node imp
= in
.impNode(dis
);
1046 }else if(in
.getKind() == kind::AND
){
1047 for(size_t i
= 0, N
= in
.getNumChildren(); i
< N
; ++i
){
1048 ppStaticLearn(in
[i
], learned
);
1053 bool TheoryBV::applyAbstraction(const std::vector
<Node
>& assertions
, std::vector
<Node
>& new_assertions
) {
1054 bool changed
= d_abstractionModule
->applyAbstraction(assertions
, new_assertions
);
1056 options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
&&
1057 options::bitvectorAig()) {
1059 AlwaysAssert (!d_eagerSolver
->isInitialized());
1060 d_eagerSolver
->turnOffAig();
1061 d_eagerSolver
->initialize();
1066 void TheoryBV::setProofLog( BitVectorProof
* bvp
) {
1067 if( options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
){
1068 d_eagerSolver
->setProofLog( bvp
);
1070 for( unsigned i
=0; i
< d_subtheories
.size(); i
++ ){
1071 d_subtheories
[i
]->setProofLog( bvp
);
1076 void TheoryBV::setConflict(Node conflict
)
1078 if (options::bvAbstraction())
1080 NodeManager
* const nm
= NodeManager::currentNM();
1081 Node new_conflict
= d_abstractionModule
->simplifyConflict(conflict
);
1083 std::vector
<Node
> lemmas
;
1084 lemmas
.push_back(new_conflict
);
1085 d_abstractionModule
->generalizeConflict(new_conflict
, lemmas
);
1086 for (unsigned i
= 0; i
< lemmas
.size(); ++i
)
1088 lemma(nm
->mkNode(kind::NOT
, lemmas
[i
]));
1092 d_conflictNode
= conflict
;
1095 } /* namespace CVC4::theory::bv */
1096 } /* namespace CVC4::theory */
1097 } /* namespace CVC4 */