1 /********************* */
2 /*! \file theory_bv.cpp
4 ** Top contributors (to current version):
5 ** Liana Hadarean, Tim King, Dejan Jovanovic
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2016 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
),
54 d_statistics(getFullInstanceName()),
60 d_lemmasAdded(c
, false),
62 d_invalidateModelCache(c
, true),
63 d_literalsToPropagate(c
),
64 d_literalsToPropagateIndex(c
, 0),
67 d_abstractionModule(new AbstractionModule(getFullInstanceName())),
68 d_isCoreTheory(false),
69 d_calledPreregister(false)
71 d_extt
= new ExtTheory( this );
72 d_extt
->addFunctionKind( kind::BITVECTOR_TO_NAT
);
73 d_extt
->addFunctionKind( kind::INT_TO_BITVECTOR
);
75 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
76 d_eagerSolver
= new EagerBitblastSolver(this);
80 if (options::bitvectorEqualitySolver()) {
81 SubtheorySolver
* core_solver
= new CoreSolver(c
, this);
82 d_subtheories
.push_back(core_solver
);
83 d_subtheoryMap
[SUB_CORE
] = core_solver
;
86 if (options::bitvectorInequalitySolver()) {
87 SubtheorySolver
* ineq_solver
= new InequalitySolver(c
, this);
88 d_subtheories
.push_back(ineq_solver
);
89 d_subtheoryMap
[SUB_INEQUALITY
] = ineq_solver
;
92 if (options::bitvectorAlgebraicSolver()) {
93 SubtheorySolver
* alg_solver
= new AlgebraicSolver(c
, this);
94 d_subtheories
.push_back(alg_solver
);
95 d_subtheoryMap
[SUB_ALGEBRAIC
] = alg_solver
;
98 BitblastSolver
* bb_solver
= new BitblastSolver(c
, this);
99 if (options::bvAbstraction()) {
100 bb_solver
->setAbstraction(d_abstractionModule
);
102 d_subtheories
.push_back(bb_solver
);
103 d_subtheoryMap
[SUB_BITBLAST
] = bb_solver
;
106 TheoryBV::~TheoryBV() {
108 delete d_eagerSolver
;
110 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
111 delete d_subtheories
[i
];
113 delete d_abstractionModule
;
117 void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine
* eq
) {
118 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
121 if (options::bitvectorEqualitySolver()) {
122 dynamic_cast<CoreSolver
*>(d_subtheoryMap
[SUB_CORE
])->setMasterEqualityEngine(eq
);
126 void TheoryBV::spendResource(unsigned ammount
) throw(UnsafeInterruptException
) {
127 getOutputChannel().spendResource(ammount
);
130 TheoryBV::Statistics::Statistics(const std::string
&name
):
131 d_avgConflictSize(name
+ "theory::bv::AvgBVConflictSize"),
132 d_solveSubstitutions(name
+ "theory::bv::NumberOfSolveSubstitutions", 0),
133 d_solveTimer(name
+ "theory::bv::solveTimer"),
134 d_numCallsToCheckFullEffort(name
+ "theory::bv::NumberOfFullCheckCalls", 0),
135 d_numCallsToCheckStandardEffort(name
+ "theory::bv::NumberOfStandardCheckCalls", 0),
136 d_weightComputationTimer(name
+ "theory::bv::weightComputationTimer"),
137 d_numMultSlice(name
+ "theory::bv::NumMultSliceApplied", 0)
139 smtStatisticsRegistry()->registerStat(&d_avgConflictSize
);
140 smtStatisticsRegistry()->registerStat(&d_solveSubstitutions
);
141 smtStatisticsRegistry()->registerStat(&d_solveTimer
);
142 smtStatisticsRegistry()->registerStat(&d_numCallsToCheckFullEffort
);
143 smtStatisticsRegistry()->registerStat(&d_numCallsToCheckStandardEffort
);
144 smtStatisticsRegistry()->registerStat(&d_weightComputationTimer
);
145 smtStatisticsRegistry()->registerStat(&d_numMultSlice
);
148 TheoryBV::Statistics::~Statistics() {
149 smtStatisticsRegistry()->unregisterStat(&d_avgConflictSize
);
150 smtStatisticsRegistry()->unregisterStat(&d_solveSubstitutions
);
151 smtStatisticsRegistry()->unregisterStat(&d_solveTimer
);
152 smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckFullEffort
);
153 smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckStandardEffort
);
154 smtStatisticsRegistry()->unregisterStat(&d_weightComputationTimer
);
155 smtStatisticsRegistry()->unregisterStat(&d_numMultSlice
);
158 Node
TheoryBV::getBVDivByZero(Kind k
, unsigned width
) {
159 NodeManager
* nm
= NodeManager::currentNM();
160 if (k
== kind::BITVECTOR_UDIV
) {
161 if (d_BVDivByZero
.find(width
) == d_BVDivByZero
.end()) {
162 // lazily create the function symbols
164 os
<< "BVUDivByZero_" << width
;
165 Node divByZero
= nm
->mkSkolem(os
.str(),
166 nm
->mkFunctionType(nm
->mkBitVectorType(width
), nm
->mkBitVectorType(width
)),
167 "partial bvudiv", NodeManager::SKOLEM_EXACT_NAME
);
168 d_BVDivByZero
[width
] = divByZero
;
170 return d_BVDivByZero
[width
];
172 else if (k
== kind::BITVECTOR_UREM
) {
173 if (d_BVRemByZero
.find(width
) == d_BVRemByZero
.end()) {
175 os
<< "BVURemByZero_" << width
;
176 Node divByZero
= nm
->mkSkolem(os
.str(),
177 nm
->mkFunctionType(nm
->mkBitVectorType(width
), nm
->mkBitVectorType(width
)),
178 "partial bvurem", NodeManager::SKOLEM_EXACT_NAME
);
179 d_BVRemByZero
[width
] = divByZero
;
181 return d_BVRemByZero
[width
];
188 void TheoryBV::collectFunctionSymbols(TNode term
, TNodeSet
& seen
) {
189 if (seen
.find(term
) != seen
.end())
191 if (term
.getKind() == kind::APPLY_UF
) {
192 TNode func
= term
.getOperator();
193 storeFunction(func
, term
);
195 for (unsigned i
= 0; i
< term
.getNumChildren(); ++i
) {
196 collectFunctionSymbols(term
[i
], seen
);
201 void TheoryBV::storeFunction(TNode func
, TNode term
) {
202 if (d_funcToArgs
.find(func
) == d_funcToArgs
.end()) {
203 d_funcToArgs
.insert(make_pair(func
, NodeSet()));
205 NodeSet
& set
= d_funcToArgs
[func
];
206 if (set
.find(term
) == set
.end()) {
208 Node skolem
= utils::mkVar(utils::getSize(term
));
209 d_funcToSkolem
.addSubstitution(term
, skolem
);
213 void TheoryBV::mkAckermanizationAsssertions(std::vector
<Node
>& assertions
) {
214 Debug("bv-ackermanize") << "TheoryBV::mkAckermanizationAsssertions\n";
216 Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
);
217 AlwaysAssert(!options::incrementalSolving());
219 for (unsigned i
= 0; i
< assertions
.size(); ++i
) {
220 collectFunctionSymbols(assertions
[i
], seen
);
223 FunctionToArgs::const_iterator it
= d_funcToArgs
.begin();
224 NodeManager
* nm
= NodeManager::currentNM();
225 for (; it
!= d_funcToArgs
.end(); ++it
) {
226 TNode func
= it
->first
;
227 const NodeSet
& args
= it
->second
;
228 NodeSet::const_iterator it1
= args
.begin();
229 for ( ; it1
!= args
.end(); ++it1
) {
230 for(NodeSet::const_iterator it2
= it1
; it2
!= args
.end(); ++it2
) {
234 AlwaysAssert (args1
.getKind() == kind::APPLY_UF
&&
235 args1
.getOperator() == func
);
236 AlwaysAssert (args2
.getKind() == kind::APPLY_UF
&&
237 args2
.getOperator() == func
);
238 AlwaysAssert (args1
.getNumChildren() == args2
.getNumChildren());
240 std::vector
<Node
> eqs(args1
.getNumChildren());
242 for (unsigned i
= 0; i
< args1
.getNumChildren(); ++i
) {
243 eqs
[i
] = nm
->mkNode(kind::EQUAL
, args1
[i
], args2
[i
]);
246 Node args_eq
= eqs
.size() == 1 ? eqs
[0] : nm
->mkNode(kind::AND
, eqs
);
247 Node func_eq
= nm
->mkNode(kind::EQUAL
, args1
, args2
);
248 Node lemma
= nm
->mkNode(kind::IMPLIES
, args_eq
, func_eq
);
249 assertions
.push_back(lemma
);
254 // replace applications of UF by skolems (FIXME for model building)
255 for(unsigned i
= 0; i
< assertions
.size(); ++i
) {
256 assertions
[i
] = d_funcToSkolem
.apply(assertions
[i
]);
260 Node
TheoryBV::expandDefinition(LogicRequest
&logicRequest
, Node node
) {
261 Debug("bitvector-expandDefinition") << "TheoryBV::expandDefinition(" << node
<< ")" << std::endl
;
263 switch (node
.getKind()) {
264 case kind::BITVECTOR_SDIV
:
265 case kind::BITVECTOR_SREM
:
266 case kind::BITVECTOR_SMOD
:
267 return TheoryBVRewriter::eliminateBVSDiv(node
);
270 case kind::BITVECTOR_UDIV
:
271 case kind::BITVECTOR_UREM
: {
272 NodeManager
* nm
= NodeManager::currentNM();
273 unsigned width
= node
.getType().getBitVectorSize();
275 if (options::bitvectorDivByZeroConst()) {
276 Kind kind
= node
.getKind() == kind::BITVECTOR_UDIV
? kind::BITVECTOR_UDIV_TOTAL
: kind::BITVECTOR_UREM_TOTAL
;
277 return nm
->mkNode(kind
, node
[0], node
[1]);
280 TNode num
= node
[0], den
= node
[1];
281 Node den_eq_0
= nm
->mkNode(kind::EQUAL
, den
, nm
->mkConst(BitVector(width
, Integer(0))));
282 Node divTotalNumDen
= nm
->mkNode(node
.getKind() == kind::BITVECTOR_UDIV
? kind::BITVECTOR_UDIV_TOTAL
:
283 kind::BITVECTOR_UREM_TOTAL
, num
, den
);
285 // if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
286 // // Ackermanize UF if using eager bit-blasting
287 // Node ackerman_var = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_ACKERMANIZE_UDIV : kind::BITVECTOR_ACKERMANIZE_UREM, num);
288 // node = nm->mkNode(kind::ITE, den_eq_0, ackerman_var, divTotalNumDen);
291 Node divByZero
= getBVDivByZero(node
.getKind(), width
);
292 Node divByZeroNum
= nm
->mkNode(kind::APPLY_UF
, divByZero
, num
);
293 node
= nm
->mkNode(kind::ITE
, den_eq_0
, divByZeroNum
, divTotalNumDen
);
294 logicRequest
.widenLogic(THEORY_UF
);
309 void TheoryBV::preRegisterTerm(TNode node
) {
310 d_calledPreregister
= true;
311 Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node
<< ")" << std::endl
;
313 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
314 // the aig bit-blaster option is set heuristically
315 // if bv abstraction is not used
316 if (!d_eagerSolver
->isInitialized()) {
317 d_eagerSolver
->initialize();
320 if (node
.getKind() == kind::BITVECTOR_EAGER_ATOM
) {
321 Node formula
= node
[0];
322 d_eagerSolver
->assertFormula(formula
);
324 // nothing to do for the other terms
328 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
329 d_subtheories
[i
]->preRegister(node
);
332 // AJR : equality solver currently registers all terms, if we want a lazy reduction without the bv equality solver, need to call this
333 //getExtTheory()->registerTermRec( node );
336 void TheoryBV::sendConflict() {
338 if (d_conflictNode
.isNull()) {
341 Debug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode
<< std::endl
;
342 d_out
->conflict(d_conflictNode
);
343 d_statistics
.d_avgConflictSize
.addEntry(d_conflictNode
.getNumChildren());
344 d_conflictNode
= Node::null();
348 void TheoryBV::checkForLemma(TNode fact
) {
349 if (fact
.getKind() == kind::EQUAL
) {
350 if (fact
[0].getKind() == kind::BITVECTOR_UREM_TOTAL
) {
351 TNode urem
= fact
[0];
352 TNode result
= fact
[1];
353 TNode divisor
= urem
[1];
354 Node result_ult_div
= mkNode(kind::BITVECTOR_ULT
, result
, divisor
);
355 Node divisor_eq_0
= mkNode(kind::EQUAL
,
357 mkConst(BitVector(getSize(divisor
), 0u)));
358 Node split
= utils::mkNode(kind::OR
, divisor_eq_0
, mkNode(kind::NOT
, fact
), result_ult_div
);
361 if (fact
[1].getKind() == kind::BITVECTOR_UREM_TOTAL
) {
362 TNode urem
= fact
[1];
363 TNode result
= fact
[0];
364 TNode divisor
= urem
[1];
365 Node result_ult_div
= mkNode(kind::BITVECTOR_ULT
, result
, divisor
);
366 Node divisor_eq_0
= mkNode(kind::EQUAL
,
368 mkConst(BitVector(getSize(divisor
), 0u)));
369 Node split
= utils::mkNode(kind::OR
, divisor_eq_0
, mkNode(kind::NOT
, fact
), result_ult_div
);
375 void TheoryBV::check(Effort e
)
377 if (done() && !fullEffort(e
)) {
380 TimerStat::CodeTimer
checkTimer(d_checkTime
);
381 Debug("bitvector") << "TheoryBV::check(" << e
<< ")" << std::endl
;
382 TimerStat::CodeTimer
codeTimer(d_statistics
.d_solveTimer
);
383 // we may be getting new assertions so the model cache may not be sound
384 d_invalidateModelCache
.set(true);
385 // if we are using the eager solver
386 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
387 // this can only happen on an empty benchmark
388 if (!d_eagerSolver
->isInitialized()) {
389 d_eagerSolver
->initialize();
391 if (!Theory::fullEffort(e
))
394 std::vector
<TNode
> assertions
;
396 TNode fact
= get().assertion
;
397 Assert (fact
.getKind() == kind::BITVECTOR_EAGER_ATOM
);
398 assertions
.push_back(fact
);
400 Assert (d_eagerSolver
->hasAssertions(assertions
));
402 bool ok
= d_eagerSolver
->checkSat();
404 if (assertions
.size() == 1) {
405 d_out
->conflict(assertions
[0]);
408 Node conflict
= NodeManager::currentNM()->mkNode(kind::AND
, assertions
);
409 d_out
->conflict(conflict
);
416 if (Theory::fullEffort(e
)) {
417 ++(d_statistics
.d_numCallsToCheckFullEffort
);
419 ++(d_statistics
.d_numCallsToCheckStandardEffort
);
421 // if we are already in conflict just return the conflict
428 TNode fact
= get().assertion
;
432 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
433 d_subtheories
[i
]->assertFact(fact
);
438 bool complete
= false;
439 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
440 Assert (!inConflict());
441 ok
= d_subtheories
[i
]->check(e
);
442 complete
= d_subtheories
[i
]->isComplete();
445 // if we are in a conflict no need to check with other theories
446 Assert (inConflict());
451 // if the last subtheory was complete we stop
456 //check extended functions
457 if (Theory::fullEffort(e
)) {
458 //do inferences (adds external lemmas) TODO: this can be improved to add internal inferences
459 std::vector
< Node
> nred
;
460 if( getExtTheory()->doInferences( 0, nred
) ){
463 std::vector
< Node
> nredr
;
464 if( getExtTheory()->doReductions( 0, nred
, nredr
) ){
467 Assert( nredr
.empty() );
471 void TheoryBV::collectModelInfo( TheoryModel
* m
, bool fullModel
){
472 Assert(!inConflict());
473 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
474 d_eagerSolver
->collectModelInfo(m
, fullModel
);
476 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
477 if (d_subtheories
[i
]->isComplete()) {
478 d_subtheories
[i
]->collectModelInfo(m
, fullModel
);
484 Node
TheoryBV::getModelValue(TNode var
) {
485 Assert(!inConflict());
486 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
487 if (d_subtheories
[i
]->isComplete()) {
488 return d_subtheories
[i
]->getModelValue(var
);
494 void TheoryBV::propagate(Effort e
) {
495 Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl
;
496 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
504 // go through stored propagations
506 for (; d_literalsToPropagateIndex
< d_literalsToPropagate
.size() && ok
; d_literalsToPropagateIndex
= d_literalsToPropagateIndex
+ 1) {
507 TNode literal
= d_literalsToPropagate
[d_literalsToPropagateIndex
];
508 // temporary fix for incremental bit-blasting
509 if (d_valuation
.isSatLiteral(literal
)) {
510 Debug("bitvector::propagate") << "TheoryBV:: propagating " << literal
<<"\n";
511 ok
= d_out
->propagate(literal
);
516 Debug("bitvector::propagate") << indent() << "TheoryBV::propagate(): conflict from theory engine" << std::endl
;
522 eq::EqualityEngine
* TheoryBV::getEqualityEngine() {
526 bool TheoryBV::getCurrentSubstitution( int effort
, std::vector
< Node
>& vars
, std::vector
< Node
>& subs
, std::map
< Node
, std::vector
< Node
> >& exp
) {
527 CoreSolver
* core
= (CoreSolver
*)d_subtheoryMap
[SUB_CORE
];
529 //get the constant equivalence classes
531 for( unsigned i
=0; i
<vars
.size(); i
++ ){
533 if( core
->getEqualityEngine()->hasTerm( n
) ){
534 Node nr
= core
->getEqualityEngine()->getRepresentative( n
);
536 subs
.push_back( nr
);
537 exp
[n
].push_back( n
.eqNode( nr
) );
546 //return true if the substitution is non-trivial
552 int TheoryBV::getReduction( int effort
, Node n
, Node
& nr
) {
553 Trace("bv-ext") << "TheoryBV::checkExt : non-reduced : " << n
<< std::endl
;
554 if( n
.getKind()==kind::BITVECTOR_TO_NAT
){
555 //taken from rewrite code
556 const unsigned size
= utils::getSize(n
[0]);
557 NodeManager
* const nm
= NodeManager::currentNM();
558 const Node z
= nm
->mkConst(Rational(0));
559 const Node bvone
= nm
->mkConst(BitVector(1u, 1u));
560 NodeBuilder
<> result(kind::PLUS
);
562 for(unsigned bit
= 0; bit
< size
; ++bit
, i
*= 2) {
563 Node cond
= nm
->mkNode(kind::EQUAL
, nm
->mkNode(nm
->mkConst(BitVectorExtract(bit
, bit
)), n
[0]), bvone
);
564 result
<< nm
->mkNode(kind::ITE
, cond
, nm
->mkConst(Rational(i
)), z
);
568 }else if( n
.getKind()==kind::INT_TO_BITVECTOR
){
569 //taken from rewrite code
570 const unsigned size
= n
.getOperator().getConst
<IntToBitVector
>().size
;
571 NodeManager
* const nm
= NodeManager::currentNM();
572 const Node bvzero
= nm
->mkConst(BitVector(1u, 0u));
573 const Node bvone
= nm
->mkConst(BitVector(1u, 1u));
576 while(v
.size() < size
) {
577 Node cond
= nm
->mkNode(kind::GEQ
, nm
->mkNode(kind::INTS_MODULUS_TOTAL
, n
[0], nm
->mkConst(Rational(i
))), nm
->mkConst(Rational(i
, 2)));
578 cond
= Rewriter::rewrite( cond
);
579 v
.push_back(nm
->mkNode(kind::ITE
, cond
, bvone
, bvzero
));
582 NodeBuilder
<> result(kind::BITVECTOR_CONCAT
);
583 result
.append(v
.rbegin(), v
.rend());
590 Theory::PPAssertStatus
TheoryBV::ppAssert(TNode in
, SubstitutionMap
& outSubstitutions
) {
591 switch(in
.getKind()) {
594 if (in
[0].isVar() && !in
[1].hasSubterm(in
[0])) {
595 ++(d_statistics
.d_solveSubstitutions
);
596 outSubstitutions
.addSubstitution(in
[0], in
[1]);
597 return PP_ASSERT_STATUS_SOLVED
;
599 if (in
[1].isVar() && !in
[0].hasSubterm(in
[1])) {
600 ++(d_statistics
.d_solveSubstitutions
);
601 outSubstitutions
.addSubstitution(in
[1], in
[0]);
602 return PP_ASSERT_STATUS_SOLVED
;
604 Node node
= Rewriter::rewrite(in
);
605 if ((node
[0].getKind() == kind::BITVECTOR_EXTRACT
&& node
[1].isConst()) ||
606 (node
[1].getKind() == kind::BITVECTOR_EXTRACT
&& node
[0].isConst())) {
607 Node extract
= node
[0].isConst() ? node
[1] : node
[0];
608 if (extract
[0].getKind() == kind::VARIABLE
) {
609 Node c
= node
[0].isConst() ? node
[0] : node
[1];
611 unsigned high
= utils::getExtractHigh(extract
);
612 unsigned low
= utils::getExtractLow(extract
);
613 unsigned var_bitwidth
= utils::getSize(extract
[0]);
614 std::vector
<Node
> children
;
617 Assert (high
!= var_bitwidth
- 1);
618 unsigned skolem_size
= var_bitwidth
- high
- 1;
619 Node skolem
= utils::mkVar(skolem_size
);
620 children
.push_back(skolem
);
621 children
.push_back(c
);
622 } else if (high
== var_bitwidth
- 1) {
623 unsigned skolem_size
= low
;
624 Node skolem
= utils::mkVar(skolem_size
);
625 children
.push_back(c
);
626 children
.push_back(skolem
);
628 unsigned skolem1_size
= low
;
629 unsigned skolem2_size
= var_bitwidth
- high
- 1;
630 Node skolem1
= utils::mkVar(skolem1_size
);
631 Node skolem2
= utils::mkVar(skolem2_size
);
632 children
.push_back(skolem2
);
633 children
.push_back(c
);
634 children
.push_back(skolem1
);
636 Node concat
= utils::mkNode(kind::BITVECTOR_CONCAT
, children
);
637 Assert (utils::getSize(concat
) == utils::getSize(extract
[0]));
638 outSubstitutions
.addSubstitution(extract
[0], concat
);
639 return PP_ASSERT_STATUS_SOLVED
;
644 case kind::BITVECTOR_ULT
:
645 case kind::BITVECTOR_SLT
:
646 case kind::BITVECTOR_ULE
:
647 case kind::BITVECTOR_SLE
:
650 // TODO other predicates
653 return PP_ASSERT_STATUS_UNSOLVED
;
656 Node
TheoryBV::ppRewrite(TNode t
)
658 Debug("bv-pp-rewrite") << "TheoryBV::ppRewrite " << t
<< "\n";
660 if (RewriteRule
<BitwiseEq
>::applies(t
)) {
661 Node result
= RewriteRule
<BitwiseEq
>::run
<false>(t
);
662 res
= Rewriter::rewrite(result
);
663 } else if (d_isCoreTheory
&& t
.getKind() == kind::EQUAL
) {
664 std::vector
<Node
> equalities
;
665 Slicer::splitEqualities(t
, equalities
);
666 res
= utils::mkAnd(equalities
);
667 } else if (RewriteRule
<UltPlusOne
>::applies(t
)) {
668 Node result
= RewriteRule
<UltPlusOne
>::run
<false>(t
);
669 res
= Rewriter::rewrite(result
);
670 } else if( res
.getKind() == kind::EQUAL
&&
671 ((res
[0].getKind() == kind::BITVECTOR_PLUS
&&
672 RewriteRule
<ConcatToMult
>::applies(res
[1])) ||
673 (res
[1].getKind() == kind::BITVECTOR_PLUS
&&
674 RewriteRule
<ConcatToMult
>::applies(res
[0])))) {
675 Node mult
= RewriteRule
<ConcatToMult
>::applies(res
[0])?
676 RewriteRule
<ConcatToMult
>::run
<false>(res
[0]) :
677 RewriteRule
<ConcatToMult
>::run
<true>(res
[1]);
678 Node factor
= mult
[0];
679 Node sum
= RewriteRule
<ConcatToMult
>::applies(res
[0])? res
[1] : res
[0];
680 Node new_eq
=utils::mkNode(kind::EQUAL
, sum
, mult
);
681 Node rewr_eq
= RewriteRule
<SolveEq
>::run
<true>(new_eq
);
682 if (rewr_eq
[0].isVar() || rewr_eq
[1].isVar()){
683 res
= Rewriter::rewrite(rewr_eq
);
690 // if(t.getKind() == kind::EQUAL &&
691 // ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() == kind::BITVECTOR_PLUS) ||
692 // (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() == kind::BITVECTOR_PLUS))) {
693 // // if we have an equality between a multiplication and addition
694 // // try to express multiplication in terms of addition
695 // Node mult = t[0].getKind() == kind::BITVECTOR_MULT? t[0] : t[1];
696 // Node add = t[0].getKind() == kind::BITVECTOR_PLUS? t[0] : t[1];
697 // if (RewriteRule<MultSlice>::applies(mult)) {
698 // Node new_mult = RewriteRule<MultSlice>::run<false>(mult);
699 // Node new_eq = Rewriter::rewrite(utils::mkNode(kind::EQUAL, new_mult, add));
701 // // the simplification can cause the formula to blow up
702 // // only apply if formula reduced
703 // if (d_subtheoryMap.find(SUB_BITBLAST) != d_subtheoryMap.end()) {
704 // BitblastSolver* bv = (BitblastSolver*)d_subtheoryMap[SUB_BITBLAST];
705 // uint64_t old_size = bv->computeAtomWeight(t);
706 // Assert (old_size);
707 // uint64_t new_size = bv->computeAtomWeight(new_eq);
708 // double ratio = ((double)new_size)/old_size;
709 // if (ratio <= 0.4) {
710 // ++(d_statistics.d_numMultSlice);
715 // if (new_eq.getKind() == kind::CONST_BOOLEAN) {
716 // ++(d_statistics.d_numMultSlice);
722 if (options::bvAbstraction() && t
.getType().isBoolean()) {
723 d_abstractionModule
->addInputAtom(res
);
725 Debug("bv-pp-rewrite") << "to " << res
<< "\n";
729 void TheoryBV::presolve() {
730 Debug("bitvector") << "TheoryBV::presolve" << endl
;
733 static int prop_count
= 0;
735 bool TheoryBV::storePropagation(TNode literal
, SubTheory subtheory
)
737 Debug("bitvector::propagate") << indent() << getSatContext()->getLevel() << " " << "TheoryBV::storePropagation(" << literal
<< ", " << subtheory
<< ")" << std::endl
;
740 // If already in conflict, no more propagation
742 Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal
<< ", " << subtheory
<< "): already in conflict" << std::endl
;
746 // If propagated already, just skip
747 PropagatedMap::const_iterator find
= d_propagatedBy
.find(literal
);
748 if (find
!= d_propagatedBy
.end()) {
751 bool polarity
= literal
.getKind() != kind::NOT
;
752 Node negatedLiteral
= polarity
? literal
.notNode() : (Node
) literal
[0];
753 find
= d_propagatedBy
.find(negatedLiteral
);
754 if (find
!= d_propagatedBy
.end() && (*find
).second
!= subtheory
) {
755 // Safe to ignore this one, subtheory should produce a conflict
759 d_propagatedBy
[literal
] = subtheory
;
762 // Propagate differs depending on the subtheory
763 // * bitblaster needs to be left alone until it's done, otherwise it doesn't know how to explain
764 // * equality engine can propagate eagerly
766 if (subtheory
== SUB_CORE
) {
767 d_out
->propagate(literal
);
772 d_literalsToPropagate
.push_back(literal
);
776 }/* TheoryBV::propagate(TNode) */
779 void TheoryBV::explain(TNode literal
, std::vector
<TNode
>& assumptions
) {
780 Assert (wasPropagatedBySubtheory(literal
));
781 SubTheory sub
= getPropagatingSubtheory(literal
);
782 d_subtheoryMap
[sub
]->explain(literal
, assumptions
);
786 Node
TheoryBV::explain(TNode node
) {
787 Debug("bitvector::explain") << "TheoryBV::explain(" << node
<< ")" << std::endl
;
788 std::vector
<TNode
> assumptions
;
790 // Ask for the explanation
791 explain(node
, assumptions
);
792 // this means that it is something true at level 0
793 if (assumptions
.size() == 0) {
794 return utils::mkTrue();
796 // return the explanation
797 Node explanation
= utils::mkAnd(assumptions
);
798 Debug("bitvector::explain") << "TheoryBV::explain(" << node
<< ") => " << explanation
<< std::endl
;
799 Debug("bitvector::explain") << "TheoryBV::explain done. \n";
804 void TheoryBV::addSharedTerm(TNode t
) {
805 Debug("bitvector::sharing") << indent() << "TheoryBV::addSharedTerm(" << t
<< ")" << std::endl
;
806 d_sharedTermsSet
.insert(t
);
807 if (options::bitvectorEqualitySolver()) {
808 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
809 d_subtheories
[i
]->addSharedTerm(t
);
815 EqualityStatus
TheoryBV::getEqualityStatus(TNode a
, TNode b
)
817 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
)
818 return EQUALITY_UNKNOWN
;
819 Assert (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY
);
820 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
) {
821 EqualityStatus status
= d_subtheories
[i
]->getEqualityStatus(a
, b
);
822 if (status
!= EQUALITY_UNKNOWN
) {
826 return EQUALITY_UNKNOWN
; ;
830 void TheoryBV::enableCoreTheorySlicer() {
831 Assert (!d_calledPreregister
);
832 d_isCoreTheory
= true;
833 if (d_subtheoryMap
.find(SUB_CORE
) != d_subtheoryMap
.end()) {
834 CoreSolver
* core
= (CoreSolver
*)d_subtheoryMap
[SUB_CORE
];
835 core
->enableSlicer();
840 void TheoryBV::ppStaticLearn(TNode in
, NodeBuilder
<>& learned
) {
841 if(d_staticLearnCache
.find(in
) != d_staticLearnCache
.end()){
844 d_staticLearnCache
.insert(in
);
846 if (in
.getKind() == kind::EQUAL
) {
847 if((in
[0].getKind() == kind::BITVECTOR_PLUS
&& in
[1].getKind() == kind::BITVECTOR_SHL
) ||
848 (in
[1].getKind() == kind::BITVECTOR_PLUS
&& in
[0].getKind() == kind::BITVECTOR_SHL
)) {
849 TNode p
= in
[0].getKind() == kind::BITVECTOR_PLUS
? in
[0] : in
[1];
850 TNode s
= in
[0].getKind() == kind::BITVECTOR_PLUS
? in
[1] : in
[0];
852 if(p
.getNumChildren() == 2
853 && p
[0].getKind() == kind::BITVECTOR_SHL
854 && p
[1].getKind() == kind::BITVECTOR_SHL
){
855 unsigned size
= utils::getSize(s
);
856 Node one
= utils::mkConst(size
, 1u);
857 if(s
[0] == one
&& p
[0][0] == one
&& p
[1][0] == one
){
858 Node zero
= utils::mkConst(size
, 0u);
861 // (s : 1 << S) = (b : 1 << B) + (c : 1 << C)
862 Node b_eq_0
= b
.eqNode(zero
);
863 Node c_eq_0
= c
.eqNode(zero
);
864 Node b_eq_c
= b
.eqNode(c
);
866 Node dis
= utils::mkNode(kind::OR
, b_eq_0
, c_eq_0
, b_eq_c
);
867 Node imp
= in
.impNode(dis
);
872 }else if(in
.getKind() == kind::AND
){
873 for(size_t i
= 0, N
= in
.getNumChildren(); i
< N
; ++i
){
874 ppStaticLearn(in
[i
], learned
);
879 bool TheoryBV::applyAbstraction(const std::vector
<Node
>& assertions
, std::vector
<Node
>& new_assertions
) {
880 bool changed
= d_abstractionModule
->applyAbstraction(assertions
, new_assertions
);
882 options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
&&
883 options::bitvectorAig()) {
885 AlwaysAssert (!d_eagerSolver
->isInitialized());
886 d_eagerSolver
->turnOffAig();
887 d_eagerSolver
->initialize();
892 void TheoryBV::setProofLog( BitVectorProof
* bvp
) {
893 if( options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
){
894 d_eagerSolver
->setProofLog( bvp
);
896 for( unsigned i
=0; i
< d_subtheories
.size(); i
++ ){
897 d_subtheories
[i
]->setProofLog( bvp
);
902 void TheoryBV::setConflict(Node conflict
) {
903 if (options::bvAbstraction()) {
904 Node new_conflict
= d_abstractionModule
->simplifyConflict(conflict
);
906 std::vector
<Node
> lemmas
;
907 lemmas
.push_back(new_conflict
);
908 d_abstractionModule
->generalizeConflict(new_conflict
, lemmas
);
909 for (unsigned i
= 0; i
< lemmas
.size(); ++i
) {
910 lemma(utils::mkNode(kind::NOT
, lemmas
[i
]));
914 d_conflictNode
= conflict
;
917 } /* namespace CVC4::theory::bv */
918 } /* namespace CVC4::theory */
919 } /* namespace CVC4 */