1 /******************************************************************************
2 * Top contributors (to current version):
3 * Mathias Preiner, Liana Hadarean, Andrew Reynolds
5 * This file is part of the cvc5 project.
7 * Copyright (c) 2009-2021 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.
11 * ****************************************************************************
13 * Layered bit-vector solver.
16 #include "theory/bv/bv_solver_layered.h"
18 #include "expr/node_algorithm.h"
19 #include "options/bv_options.h"
20 #include "options/smt_options.h"
21 #include "smt/smt_statistics_registry.h"
22 #include "theory/bv/abstraction.h"
23 #include "theory/bv/bv_eager_solver.h"
24 #include "theory/bv/bv_subtheory_algebraic.h"
25 #include "theory/bv/bv_subtheory_bitblast.h"
26 #include "theory/bv/bv_subtheory_core.h"
27 #include "theory/bv/bv_subtheory_inequality.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"
34 using namespace cvc5::theory::bv::utils
;
40 BVSolverLayered::BVSolverLayered(TheoryBV
& bv
,
43 context::UserContext
* u
,
44 ProofNodeManager
* pnm
,
46 : BVSolver(env
, bv
.d_state
, bv
.d_im
),
49 d_alreadyPropagatedSet(c
),
55 d_lemmasAdded(c
, false),
57 d_invalidateModelCache(c
, true),
58 d_literalsToPropagate(c
),
59 d_literalsToPropagateIndex(c
, 0),
62 d_abstractionModule(new AbstractionModule(getStatsPrefix(THEORY_BV
))),
63 d_calledPreregister(false)
65 if (options().bv
.bitblastMode
== options::BitblastMode::EAGER
)
67 d_eagerSolver
.reset(new EagerBitblastSolver(c
, this));
71 if (options().bv
.bitvectorEqualitySolver
)
73 d_subtheories
.emplace_back(new CoreSolver(c
, this));
74 d_subtheoryMap
[SUB_CORE
] = d_subtheories
.back().get();
77 if (options().bv
.bitvectorInequalitySolver
)
79 d_subtheories
.emplace_back(new InequalitySolver(c
, u
, this));
80 d_subtheoryMap
[SUB_INEQUALITY
] = d_subtheories
.back().get();
83 if (options().bv
.bitvectorAlgebraicSolver
)
85 d_subtheories
.emplace_back(new AlgebraicSolver(c
, this));
86 d_subtheoryMap
[SUB_ALGEBRAIC
] = d_subtheories
.back().get();
89 BitblastSolver
* bb_solver
= new BitblastSolver(c
, this);
90 if (options().bv
.bvAbstraction
)
92 bb_solver
->setAbstraction(d_abstractionModule
.get());
94 d_subtheories
.emplace_back(bb_solver
);
95 d_subtheoryMap
[SUB_BITBLAST
] = bb_solver
;
98 BVSolverLayered::~BVSolverLayered() {}
100 bool BVSolverLayered::needsEqualityEngine(EeSetupInfo
& esi
)
102 CoreSolver
* core
= (CoreSolver
*)d_subtheoryMap
[SUB_CORE
];
105 return core
->needsEqualityEngine(esi
);
107 // otherwise we don't use an equality engine
111 void BVSolverLayered::finishInit()
113 CoreSolver
* core
= (CoreSolver
*)d_subtheoryMap
[SUB_CORE
];
116 // must finish initialization in the core solver
121 void BVSolverLayered::spendResource(Resource r
) { d_im
.spendResource(r
); }
123 BVSolverLayered::Statistics::Statistics()
124 : d_avgConflictSize(smtStatisticsRegistry().registerAverage(
125 "theory::bv::lazy::AvgBVConflictSize")),
126 d_solveTimer(smtStatisticsRegistry().registerTimer(
127 "theory::bv::lazy::solveTimer")),
128 d_numCallsToCheckFullEffort(smtStatisticsRegistry().registerInt(
129 "theory::bv::lazy::NumFullCheckCalls")),
130 d_numCallsToCheckStandardEffort(smtStatisticsRegistry().registerInt(
131 "theory::bv::lazy::NumStandardCheckCalls")),
132 d_weightComputationTimer(smtStatisticsRegistry().registerTimer(
133 "theory::bv::lazy::weightComputationTimer")),
134 d_numMultSlice(smtStatisticsRegistry().registerInt(
135 "theory::bv::lazy::NumMultSliceApplied"))
139 void BVSolverLayered::preRegisterTerm(TNode node
)
141 d_calledPreregister
= true;
142 Debug("bitvector-preregister")
143 << "BVSolverLayered::preRegister(" << node
<< ")" << std::endl
;
145 if (options().bv
.bitblastMode
== options::BitblastMode::EAGER
)
147 // the aig bit-blaster option is set heuristically
148 // if bv abstraction is used
149 if (!d_eagerSolver
->isInitialized())
151 d_eagerSolver
->initialize();
154 if (node
.getKind() == kind::BITVECTOR_EAGER_ATOM
)
156 Node formula
= node
[0];
157 d_eagerSolver
->assertFormula(formula
);
162 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
)
164 d_subtheories
[i
]->preRegister(node
);
167 // AJR : equality solver currently registers all terms to ExtTheory, if we
168 // want a lazy reduction without the bv equality solver, need to call this
169 // d_bv.d_extTheory->registerTermRec( node );
172 void BVSolverLayered::sendConflict()
175 if (d_conflictNode
.isNull())
181 Debug("bitvector") << indent() << "BVSolverLayered::check(): conflict "
182 << d_conflictNode
<< std::endl
;
183 d_im
.conflict(d_conflictNode
, InferenceId::BV_LAYERED_CONFLICT
);
184 d_statistics
.d_avgConflictSize
<< d_conflictNode
.getNumChildren();
185 d_conflictNode
= Node::null();
189 void BVSolverLayered::checkForLemma(TNode fact
)
191 if (fact
.getKind() == kind::EQUAL
)
193 NodeManager
* nm
= NodeManager::currentNM();
194 if (fact
[0].getKind() == kind::BITVECTOR_UREM
)
196 TNode urem
= fact
[0];
197 TNode result
= fact
[1];
198 TNode divisor
= urem
[1];
199 Node result_ult_div
= nm
->mkNode(kind::BITVECTOR_ULT
, result
, divisor
);
201 nm
->mkNode(kind::EQUAL
, divisor
, mkZero(getSize(divisor
)));
202 Node split
= nm
->mkNode(
203 kind::OR
, divisor_eq_0
, nm
->mkNode(kind::NOT
, fact
), result_ult_div
);
206 if (fact
[1].getKind() == kind::BITVECTOR_UREM
)
208 TNode urem
= fact
[1];
209 TNode result
= fact
[0];
210 TNode divisor
= urem
[1];
211 Node result_ult_div
= nm
->mkNode(kind::BITVECTOR_ULT
, result
, divisor
);
213 nm
->mkNode(kind::EQUAL
, divisor
, mkZero(getSize(divisor
)));
214 Node split
= nm
->mkNode(
215 kind::OR
, divisor_eq_0
, nm
->mkNode(kind::NOT
, fact
), result_ult_div
);
221 bool BVSolverLayered::preCheck(Theory::Effort e
)
227 void BVSolverLayered::check(Theory::Effort e
)
229 if (done() && e
< Theory::EFFORT_FULL
)
234 Debug("bitvector") << "BVSolverLayered::check(" << e
<< ")" << std::endl
;
235 TimerStat::CodeTimer
codeTimer(d_statistics
.d_solveTimer
);
236 // we may be getting new assertions so the model cache may not be sound
237 d_invalidateModelCache
.set(true);
238 // if we are using the eager solver
239 if (options().bv
.bitblastMode
== options::BitblastMode::EAGER
)
241 // this can only happen on an empty benchmark
242 if (!d_eagerSolver
->isInitialized())
244 d_eagerSolver
->initialize();
246 if (!Theory::fullEffort(e
)) return;
248 std::vector
<TNode
> assertions
;
251 TNode fact
= get().d_assertion
;
252 Assert(fact
.getKind() == kind::BITVECTOR_EAGER_ATOM
);
253 assertions
.push_back(fact
);
254 d_eagerSolver
->assertFormula(fact
[0]);
257 bool ok
= d_eagerSolver
->checkSat();
260 if (assertions
.size() == 1)
262 d_im
.conflict(assertions
[0], InferenceId::BV_LAYERED_CONFLICT
);
265 Node conflict
= utils::mkAnd(assertions
);
266 d_im
.conflict(conflict
, InferenceId::BV_LAYERED_CONFLICT
);
272 if (Theory::fullEffort(e
))
274 ++(d_statistics
.d_numCallsToCheckFullEffort
);
278 ++(d_statistics
.d_numCallsToCheckStandardEffort
);
280 // if we are already in conflict just return the conflict
289 TNode fact
= get().d_assertion
;
293 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
)
295 d_subtheories
[i
]->assertFact(fact
);
300 bool complete
= false;
301 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
)
303 Assert(!inConflict());
304 ok
= d_subtheories
[i
]->check(e
);
305 complete
= d_subtheories
[i
]->isComplete();
309 // if we are in a conflict no need to check with other theories
310 Assert(inConflict());
316 // if the last subtheory was complete we stop
322 bool BVSolverLayered::collectModelValues(TheoryModel
* m
,
323 const std::set
<Node
>& termSet
)
325 Assert(!inConflict());
326 if (options().bv
.bitblastMode
== options::BitblastMode::EAGER
)
328 if (!d_eagerSolver
->collectModelInfo(m
, true))
333 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
)
335 if (d_subtheories
[i
]->isComplete())
337 return d_subtheories
[i
]->collectModelValues(m
, termSet
);
343 Node
BVSolverLayered::getModelValue(TNode var
)
345 Assert(!inConflict());
346 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
)
348 if (d_subtheories
[i
]->isComplete())
350 return d_subtheories
[i
]->getModelValue(var
);
356 void BVSolverLayered::propagate(Theory::Effort e
)
358 Debug("bitvector") << indent() << "BVSolverLayered::propagate()" << std::endl
;
359 if (options().bv
.bitblastMode
== options::BitblastMode::EAGER
)
369 // go through stored propagations
371 for (; d_literalsToPropagateIndex
< d_literalsToPropagate
.size() && ok
;
372 d_literalsToPropagateIndex
= d_literalsToPropagateIndex
+ 1)
374 TNode literal
= d_literalsToPropagate
[d_literalsToPropagateIndex
];
375 // temporary fix for incremental bit-blasting
376 if (d_state
.isSatLiteral(literal
))
378 Debug("bitvector::propagate")
379 << "BVSolverLayered:: propagating " << literal
<< "\n";
380 ok
= d_im
.propagateLit(literal
);
386 Debug("bitvector::propagate")
388 << "BVSolverLayered::propagate(): conflict from theory engine"
394 TrustNode
BVSolverLayered::ppRewrite(TNode t
)
396 Debug("bv-pp-rewrite") << "BVSolverLayered::ppRewrite " << t
<< "\n";
398 if (options().bv
.bitwiseEq
&& RewriteRule
<BitwiseEq
>::applies(t
))
400 Node result
= RewriteRule
<BitwiseEq
>::run
<false>(t
);
401 res
= rewrite(result
);
403 else if (RewriteRule
<UltAddOne
>::applies(t
))
405 Node result
= RewriteRule
<UltAddOne
>::run
<false>(t
);
406 res
= rewrite(result
);
408 else if (res
.getKind() == kind::EQUAL
409 && ((res
[0].getKind() == kind::BITVECTOR_ADD
410 && RewriteRule
<ConcatToMult
>::applies(res
[1]))
411 || (res
[1].getKind() == kind::BITVECTOR_ADD
412 && RewriteRule
<ConcatToMult
>::applies(res
[0]))))
414 Node mult
= RewriteRule
<ConcatToMult
>::applies(res
[0])
415 ? RewriteRule
<ConcatToMult
>::run
<false>(res
[0])
416 : RewriteRule
<ConcatToMult
>::run
<true>(res
[1]);
417 Node factor
= mult
[0];
418 Node sum
= RewriteRule
<ConcatToMult
>::applies(res
[0]) ? res
[1] : res
[0];
419 Node new_eq
= NodeManager::currentNM()->mkNode(kind::EQUAL
, sum
, mult
);
420 Node rewr_eq
= RewriteRule
<SolveEq
>::run
<true>(new_eq
);
421 if (rewr_eq
[0].isVar() || rewr_eq
[1].isVar())
423 res
= rewrite(rewr_eq
);
430 else if (RewriteRule
<SignExtendEqConst
>::applies(t
))
432 res
= RewriteRule
<SignExtendEqConst
>::run
<false>(t
);
434 else if (RewriteRule
<ZeroExtendEqConst
>::applies(t
))
436 res
= RewriteRule
<ZeroExtendEqConst
>::run
<false>(t
);
438 else if (RewriteRule
<NormalizeEqAddNeg
>::applies(t
))
440 res
= RewriteRule
<NormalizeEqAddNeg
>::run
<false>(t
);
443 // if(t.getKind() == kind::EQUAL &&
444 // ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() ==
445 // kind::BITVECTOR_ADD) ||
446 // (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() ==
447 // kind::BITVECTOR_ADD))) {
448 // // if we have an equality between a multiplication and addition
449 // // try to express multiplication in terms of addition
450 // Node mult = t[0].getKind() == kind::BITVECTOR_MULT? t[0] : t[1];
451 // Node add = t[0].getKind() == kind::BITVECTOR_ADD? t[0] : t[1];
452 // if (RewriteRule<MultSlice>::applies(mult)) {
453 // Node new_mult = RewriteRule<MultSlice>::run<false>(mult);
455 // rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL,
458 // // the simplification can cause the formula to blow up
459 // // only apply if formula reduced
460 // if (d_subtheoryMap.find(SUB_BITBLAST) != d_subtheoryMap.end()) {
461 // BitblastSolver* bv = (BitblastSolver*)d_subtheoryMap[SUB_BITBLAST];
462 // uint64_t old_size = bv->computeAtomWeight(t);
463 // Assert (old_size);
464 // uint64_t new_size = bv->computeAtomWeight(new_eq);
465 // double ratio = ((double)new_size)/old_size;
466 // if (ratio <= 0.4) {
467 // ++(d_statistics.d_numMultSlice);
472 // if (new_eq.getKind() == kind::CONST_BOOLEAN) {
473 // ++(d_statistics.d_numMultSlice);
479 if (options().bv
.bvAbstraction
&& t
.getType().isBoolean())
481 d_abstractionModule
->addInputAtom(res
);
483 Debug("bv-pp-rewrite") << "to " << res
<< "\n";
486 return TrustNode::mkTrustRewrite(t
, res
, nullptr);
488 return TrustNode::null();
491 void BVSolverLayered::presolve()
493 Debug("bitvector") << "BVSolverLayered::presolve" << std::endl
;
496 static int prop_count
= 0;
498 bool BVSolverLayered::storePropagation(TNode literal
, SubTheory subtheory
)
500 Debug("bitvector::propagate")
501 << indent() << d_context
->getLevel() << " "
502 << "BVSolverLayered::storePropagation(" << literal
<< ", " << subtheory
506 // If already in conflict, no more propagation
509 Debug("bitvector::propagate")
510 << indent() << "BVSolverLayered::storePropagation(" << literal
<< ", "
511 << subtheory
<< "): already in conflict" << std::endl
;
515 // If propagated already, just skip
516 PropagatedMap::const_iterator find
= d_propagatedBy
.find(literal
);
517 if (find
!= d_propagatedBy
.end())
523 bool polarity
= literal
.getKind() != kind::NOT
;
524 Node negatedLiteral
= polarity
? literal
.notNode() : (Node
)literal
[0];
525 find
= d_propagatedBy
.find(negatedLiteral
);
526 if (find
!= d_propagatedBy
.end() && (*find
).second
!= subtheory
)
528 // Safe to ignore this one, subtheory should produce a conflict
532 d_propagatedBy
[literal
] = subtheory
;
535 // Propagate differs depending on the subtheory
536 // * bitblaster needs to be left alone until it's done, otherwise it doesn't
537 // know how to explain
538 // * equality engine can propagate eagerly
539 // TODO(2348): Determine if ok should be set by propagate. If not, remove ok.
540 constexpr bool ok
= true;
541 if (subtheory
== SUB_CORE
)
543 d_im
.propagateLit(literal
);
551 d_literalsToPropagate
.push_back(literal
);
555 } /* BVSolverLayered::propagate(TNode) */
557 void BVSolverLayered::explain(TNode literal
, std::vector
<TNode
>& assumptions
)
559 Assert(wasPropagatedBySubtheory(literal
));
560 SubTheory sub
= getPropagatingSubtheory(literal
);
561 d_subtheoryMap
[sub
]->explain(literal
, assumptions
);
564 TrustNode
BVSolverLayered::explain(TNode node
)
566 Debug("bitvector::explain")
567 << "BVSolverLayered::explain(" << node
<< ")" << std::endl
;
568 std::vector
<TNode
> assumptions
;
570 // Ask for the explanation
571 explain(node
, assumptions
);
572 // this means that it is something true at level 0
574 if (assumptions
.size() == 0)
576 explanation
= utils::mkTrue();
580 // return the explanation
581 explanation
= utils::mkAnd(assumptions
);
583 Debug("bitvector::explain") << "BVSolverLayered::explain(" << node
<< ") => "
584 << explanation
<< std::endl
;
585 Debug("bitvector::explain") << "BVSolverLayered::explain done. \n";
586 return TrustNode::mkTrustPropExp(node
, explanation
, nullptr);
589 void BVSolverLayered::notifySharedTerm(TNode t
)
591 Debug("bitvector::sharing")
592 << indent() << "BVSolverLayered::notifySharedTerm(" << t
<< ")"
594 d_sharedTermsSet
.insert(t
);
597 EqualityStatus
BVSolverLayered::getEqualityStatus(TNode a
, TNode b
)
599 if (options().bv
.bitblastMode
== options::BitblastMode::EAGER
)
600 return EQUALITY_UNKNOWN
;
601 Assert(options().bv
.bitblastMode
== options::BitblastMode::LAZY
);
602 for (unsigned i
= 0; i
< d_subtheories
.size(); ++i
)
604 EqualityStatus status
= d_subtheories
[i
]->getEqualityStatus(a
, b
);
605 if (status
!= EQUALITY_UNKNOWN
)
610 return EQUALITY_UNKNOWN
;
614 void BVSolverLayered::ppStaticLearn(TNode in
, NodeBuilder
& learned
)
616 if (d_staticLearnCache
.find(in
) != d_staticLearnCache
.end())
620 d_staticLearnCache
.insert(in
);
622 if (in
.getKind() == kind::EQUAL
)
624 if ((in
[0].getKind() == kind::BITVECTOR_ADD
625 && in
[1].getKind() == kind::BITVECTOR_SHL
)
626 || (in
[1].getKind() == kind::BITVECTOR_ADD
627 && in
[0].getKind() == kind::BITVECTOR_SHL
))
629 TNode p
= in
[0].getKind() == kind::BITVECTOR_ADD
? in
[0] : in
[1];
630 TNode s
= in
[0].getKind() == kind::BITVECTOR_ADD
? in
[1] : in
[0];
632 if (p
.getNumChildren() == 2 && p
[0].getKind() == kind::BITVECTOR_SHL
633 && p
[1].getKind() == kind::BITVECTOR_SHL
)
635 unsigned size
= utils::getSize(s
);
636 Node one
= utils::mkConst(size
, 1u);
637 if (s
[0] == one
&& p
[0][0] == one
&& p
[1][0] == one
)
639 Node zero
= utils::mkConst(size
, 0u);
642 // (s : 1 << S) = (b : 1 << B) + (c : 1 << C)
643 Node b_eq_0
= b
.eqNode(zero
);
644 Node c_eq_0
= c
.eqNode(zero
);
645 Node b_eq_c
= b
.eqNode(c
);
647 Node dis
= NodeManager::currentNM()->mkNode(
648 kind::OR
, b_eq_0
, c_eq_0
, b_eq_c
);
649 Node imp
= in
.impNode(dis
);
655 else if (in
.getKind() == kind::AND
)
657 for (size_t i
= 0, N
= in
.getNumChildren(); i
< N
; ++i
)
659 ppStaticLearn(in
[i
], learned
);
664 bool BVSolverLayered::applyAbstraction(const std::vector
<Node
>& assertions
,
665 std::vector
<Node
>& new_assertions
)
668 d_abstractionModule
->applyAbstraction(assertions
, new_assertions
);
669 if (changed
&& options().bv
.bitblastMode
== options::BitblastMode::EAGER
670 && options().bv
.bitvectorAig
)
673 AlwaysAssert(!d_eagerSolver
->isInitialized());
674 d_eagerSolver
->turnOffAig();
675 d_eagerSolver
->initialize();
680 void BVSolverLayered::setConflict(Node conflict
)
682 if (options().bv
.bvAbstraction
)
684 NodeManager
* const nm
= NodeManager::currentNM();
685 Node new_conflict
= d_abstractionModule
->simplifyConflict(conflict
);
687 std::vector
<Node
> lemmas
;
688 lemmas
.push_back(new_conflict
);
689 d_abstractionModule
->generalizeConflict(new_conflict
, lemmas
);
690 for (unsigned i
= 0; i
< lemmas
.size(); ++i
)
692 lemma(nm
->mkNode(kind::NOT
, lemmas
[i
]));
696 d_conflictNode
= conflict
;
700 } // namespace theory