Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Bit-blasting solver that supports multiple SAT backends.
11 : : */
12 : :
13 : : #include "theory/bv/bv_solver_bitblast.h"
14 : :
15 : : #include "options/bv_options.h"
16 : : #include "prop/sat_solver_factory.h"
17 : : #include "theory/bv/theory_bv.h"
18 : : #include "theory/bv/theory_bv_utils.h"
19 : : #include "theory/theory_model.h"
20 : :
21 : : namespace cvc5::internal {
22 : : namespace theory {
23 : : namespace bv {
24 : :
25 : : /**
26 : : * Notifies the BV solver when assertions were reset.
27 : : *
28 : : * This class is notified after every user-context pop and maintains a flag
29 : : * that indicates whether assertions have been reset. If the user-context level
30 : : * reaches level 0 it means that the assertions were reset.
31 : : */
32 : : class NotifyResetAssertions : public context::ContextNotifyObj
33 : : {
34 : : public:
35 : 40231 : NotifyResetAssertions(context::Context* c)
36 : 40231 : : context::ContextNotifyObj(c, false),
37 : 40231 : d_context(c),
38 : 40231 : d_doneResetAssertions(false)
39 : : {
40 : 40231 : }
41 : :
42 : 8 : bool doneResetAssertions() { return d_doneResetAssertions; }
43 : :
44 : 2 : void reset() { d_doneResetAssertions = false; }
45 : :
46 : : protected:
47 : 47611 : void contextNotifyPop() override
48 : : {
49 : : // If the user-context level reaches 0 it means that reset-assertions was
50 : : // called.
51 [ + + ]: 47611 : if (d_context->getLevel() == 0)
52 : : {
53 : 40338 : d_doneResetAssertions = true;
54 : : }
55 : 47611 : }
56 : :
57 : : private:
58 : : /** The user-context. */
59 : : context::Context* d_context;
60 : :
61 : : /** Flag to notify whether reset assertions was called. */
62 : : bool d_doneResetAssertions;
63 : : };
64 : :
65 : : /**
66 : : * Bit-blasting registrar.
67 : : *
68 : : * The CnfStream calls preRegister() if it encounters a theory atom.
69 : : * This registrar bit-blasts given atom and remembers which bit-vector atoms
70 : : * were bit-blasted.
71 : : *
72 : : * This registrar is needed when --bitblast=eager is enabled.
73 : : */
74 : : class BBRegistrar : public prop::Registrar
75 : : {
76 : : public:
77 : 40231 : BBRegistrar(NodeBitblaster* bb) : d_bitblaster(bb) {}
78 : :
79 : 159375 : void notifySatLiteral(Node n) override
80 : : {
81 [ - + ]: 159375 : if (d_registeredAtoms.find(n) != d_registeredAtoms.end())
82 : : {
83 : 0 : return;
84 : : }
85 : : /* We are only interested in bit-vector atoms. */
86 : 159794 : if ((n.getKind() == Kind::EQUAL && n[0].getType().isBitVector())
87 [ + + ]: 158956 : || n.getKind() == Kind::BITVECTOR_ULT
88 [ + - ]: 158859 : || n.getKind() == Kind::BITVECTOR_ULE
89 [ + - ]: 158859 : || n.getKind() == Kind::BITVECTOR_SLT
90 [ + + ][ - + ]: 318750 : || n.getKind() == Kind::BITVECTOR_SLE)
[ + + ]
91 : : {
92 : 516 : d_registeredAtoms.insert(n);
93 : 516 : d_bitblaster->bbAtom(n);
94 : : }
95 : : }
96 : :
97 : 241 : std::unordered_set<TNode>& getRegisteredAtoms() { return d_registeredAtoms; }
98 : :
99 : : private:
100 : : /** The bitblaster used. */
101 : : NodeBitblaster* d_bitblaster;
102 : :
103 : : /** Stores bit-vector atoms encounterd on preRegister(). */
104 : : std::unordered_set<TNode> d_registeredAtoms;
105 : : };
106 : :
107 : 40231 : BVSolverBitblast::BVSolverBitblast(Env& env,
108 : : TheoryState* s,
109 : 40231 : TheoryInferenceManager& inferMgr)
110 : : : BVSolver(env, *s, inferMgr),
111 : 40231 : d_bitblaster(new NodeBitblaster(env, s)),
112 : 40231 : d_bbRegistrar(new BBRegistrar(d_bitblaster.get())),
113 : 40231 : d_nullContext(new context::Context()),
114 : 40231 : d_bbFacts(context()),
115 : 40231 : d_bbInputFacts(context()),
116 : 40231 : d_assumptions(context()),
117 : 40231 : d_assertions(context()),
118 : 40261 : d_epg(env.isTheoryProofProducing()
119 : 30 : ? new EagerProofGenerator(env, userContext(), "")
120 : : : nullptr),
121 : 40231 : d_bvProofChecker(nodeManager()),
122 : 40231 : d_factLiteralCache(context()),
123 : 40231 : d_literalFactCache(context()),
124 : 40231 : d_propagate(options().bv.bitvectorPropagate),
125 : 120693 : d_resetNotify(new NotifyResetAssertions(userContext()))
126 : : {
127 [ + + ]: 40231 : if (env.isTheoryProofProducing())
128 : : {
129 : 15 : d_bvProofChecker.registerTo(env.getProofNodeManager()->getChecker());
130 : : }
131 : :
132 : 40231 : initSatSolver();
133 : 40231 : }
134 : :
135 : 40231 : bool BVSolverBitblast::needsEqualityEngine(CVC5_UNUSED EeSetupInfo& esi)
136 : : {
137 : : // we always need the equality engine if sharing is enabled for processing
138 : : // equality engine and shared terms
139 [ + + ][ + - ]: 40231 : return logicInfo().isSharingEnabled() || options().bv.bvEqEngine;
140 : : }
141 : :
142 : 2380017 : void BVSolverBitblast::postCheck(Theory::Effort level)
143 : : {
144 [ + + ]: 2380017 : if (level != Theory::Effort::EFFORT_FULL)
145 : : {
146 : : /* Do bit-level propagation only if the SAT solver supports it. */
147 [ - + ][ - - ]: 2306440 : if (!d_propagate || !d_satSolver->setPropagateOnly())
[ + - ]
148 : : {
149 : 2306440 : return;
150 : : }
151 : : }
152 : :
153 : : // If we permanently added assertions to the SAT solver and the assertions
154 : : // were reset, we have to reset the SAT solver and the CNF stream.
155 [ + + ][ + + ]: 73577 : if (options().bv.bvAssertInput && d_resetNotify->doneResetAssertions())
[ + + ]
156 : : {
157 : 2 : d_satSolver.reset(nullptr);
158 : 2 : d_cnfStream.reset(nullptr);
159 : 2 : initSatSolver();
160 : 2 : d_resetNotify->reset();
161 : : }
162 : :
163 : 73577 : NodeManager* nm = nodeManager();
164 : :
165 : : /* Process input assertions bit-blast queue. */
166 [ + + ]: 73585 : while (!d_bbInputFacts.empty())
167 : : {
168 : 8 : Node fact = d_bbInputFacts.front();
169 : 8 : d_bbInputFacts.pop();
170 : : /* Bit-blast fact and cache literal. */
171 [ + - ]: 8 : if (d_factLiteralCache.find(fact) == d_factLiteralCache.end())
172 : : {
173 [ - + ]: 8 : if (fact.getKind() == Kind::BITVECTOR_EAGER_ATOM)
174 : : {
175 : 0 : handleEagerAtom(fact, true);
176 : : }
177 : : else
178 : : {
179 : 8 : d_bitblaster->bbAtom(fact);
180 : 8 : Node bb_fact = d_bitblaster->getStoredBBAtom(fact);
181 : 8 : d_cnfStream->convertAndAssert(bb_fact, false, false);
182 : 8 : }
183 : : }
184 : 8 : d_assertions.push_back(fact);
185 : 8 : }
186 : :
187 : : /* Process bit-blast queue and store SAT literals. */
188 [ + + ]: 7817387 : while (!d_bbFacts.empty())
189 : : {
190 : 7743810 : Node fact = d_bbFacts.front();
191 : 7743810 : d_bbFacts.pop();
192 : : /* Bit-blast fact and cache literal. */
193 [ + - ]: 7743810 : if (d_factLiteralCache.find(fact) == d_factLiteralCache.end())
194 : : {
195 : 7743810 : prop::SatLiteral lit;
196 [ + + ]: 7743810 : if (fact.getKind() == Kind::BITVECTOR_EAGER_ATOM)
197 : : {
198 : 241 : handleEagerAtom(fact, false);
199 : 241 : lit = d_cnfStream->getLiteral(fact[0]);
200 : : }
201 : : else
202 : : {
203 : 7743569 : d_bitblaster->bbAtom(fact);
204 : 7743569 : Node bb_fact = d_bitblaster->getStoredBBAtom(fact);
205 : 7743569 : d_cnfStream->ensureLiteral(bb_fact);
206 : 7743569 : lit = d_cnfStream->getLiteral(bb_fact);
207 : 7743569 : }
208 : 7743810 : d_factLiteralCache[fact] = lit;
209 : 7743810 : d_literalFactCache[lit] = fact;
210 : : }
211 : 7743810 : d_assumptions.push_back(d_factLiteralCache[fact]);
212 : 7743810 : }
213 : :
214 : : std::vector<prop::SatLiteral> assumptions(d_assumptions.begin(),
215 : 73577 : d_assumptions.end());
216 : 73577 : prop::SatValue val = d_satSolver->solve(assumptions);
217 : :
218 [ + + ]: 73577 : if (val == prop::SatValue::SAT_VALUE_FALSE)
219 : : {
220 : 19848 : std::vector<prop::SatLiteral> unsat_assumptions;
221 : 19848 : d_satSolver->getUnsatAssumptions(unsat_assumptions);
222 : :
223 : 19848 : Node conflict;
224 : : // Unsat assumptions produce conflict.
225 [ + - ]: 19848 : if (unsat_assumptions.size() > 0)
226 : : {
227 : 19848 : std::vector<Node> conf;
228 [ + + ]: 171622 : for (const prop::SatLiteral& lit : unsat_assumptions)
229 : : {
230 : 151774 : conf.push_back(d_literalFactCache[lit]);
231 [ + - ]: 303548 : Trace("bv-bitblast")
232 : 151774 : << "unsat assumption (" << lit << "): " << conf.back() << std::endl;
233 : : }
234 : 19848 : conflict = nm->mkAnd(conf);
235 : 19848 : }
236 : : else // Input assertions produce conflict.
237 : : {
238 : 0 : std::vector<Node> assertions(d_assertions.begin(), d_assertions.end());
239 : 0 : conflict = nm->mkAnd(assertions);
240 : 0 : }
241 : 19848 : TrustNode tconflict;
242 [ + + ]: 19848 : if (d_epg != nullptr)
243 : : {
244 : 1064 : tconflict = d_epg->mkTrustNodeTrusted(
245 : 532 : conflict, TrustId::BV_BITBLAST_CONFLICT, {}, {}, true);
246 : : }
247 : : else
248 : : {
249 : 19316 : tconflict = TrustNode::mkTrustConflict(conflict, nullptr);
250 : : }
251 : 19848 : d_im.trustedConflict(tconflict, InferenceId::BV_BITBLAST_CONFLICT);
252 : 19848 : }
253 : 73577 : }
254 : :
255 : 4289970 : bool BVSolverBitblast::preNotifyFact(CVC5_UNUSED TNode atom,
256 : : CVC5_UNUSED bool pol,
257 : : TNode fact,
258 : : CVC5_UNUSED bool isPrereg,
259 : : CVC5_UNUSED bool isInternal)
260 : : {
261 : 4289970 : Valuation& val = d_state.getValuation();
262 : :
263 : : /**
264 : : * Check whether `fact` is an input assertion on user-level 0.
265 : : *
266 : : * If this is the case we can assert `fact` to the SAT solver instead of
267 : : * using assumptions.
268 : : */
269 [ + + ][ + + ]: 4289970 : if (options().bv.bvAssertInput && val.isFixed(fact))
[ + + ][ + + ]
[ - - ]
270 : : {
271 [ - + ][ - + ]: 8 : Assert(!val.isDecision(fact));
[ - - ]
272 : 8 : d_bbInputFacts.push_back(fact);
273 : : }
274 : : else
275 : : {
276 : 4289962 : d_bbFacts.push_back(fact);
277 : : }
278 : :
279 : : // Return false to enable equality engine reasoning in Theory, which is
280 : : // available if we are using the equality engine.
281 [ + + ][ - + ]: 4289970 : return !logicInfo().isSharingEnabled() && !options().bv.bvEqEngine;
282 : : }
283 : :
284 : 3748 : TrustNode BVSolverBitblast::explain(TNode n)
285 : : {
286 [ + - ]: 3748 : Trace("bv-bitblast") << "explain called on " << n << std::endl;
287 : 3748 : return d_im.explainLit(n);
288 : : }
289 : :
290 : 14362 : void BVSolverBitblast::computeRelevantTerms(std::set<Node>& termSet)
291 : : {
292 : : /* BITVECTOR_EAGER_ATOM wraps input assertions that may also contain
293 : : * equalities. As a result, these equalities are not handled by the equality
294 : : * engine and terms below these equalities do not appear in `termSet`.
295 : : * We need to make sure that we compute model values for all relevant terms
296 : : * in BitblastMode::EAGER and therefore add all variables from the
297 : : * bit-blaster to `termSet`.
298 : : */
299 [ + + ]: 14362 : if (options().bv.bitblastMode == options::BitblastMode::EAGER)
300 : : {
301 : 9 : d_bitblaster->computeRelevantTerms(termSet);
302 : : }
303 : 14362 : }
304 : :
305 : 14362 : bool BVSolverBitblast::collectModelValues(TheoryModel* m,
306 : : const std::set<Node>& termSet)
307 : : {
308 [ + + ]: 384342 : for (const auto& term : termSet)
309 : : {
310 [ + + ]: 369980 : if (!d_bitblaster->isVariable(term))
311 : : {
312 : 348194 : continue;
313 : : }
314 : :
315 : 21786 : Node value = getValue(term, true);
316 [ - + ][ - + ]: 21786 : Assert(value.isConst());
[ - - ]
317 [ - + ]: 21786 : if (!m->assertEquality(term, value, true))
318 : : {
319 : 0 : return false;
320 : : }
321 [ + - ]: 21786 : }
322 : :
323 : : // In eager bitblast mode we also have to collect the model values for
324 : : // Boolean variables in the CNF stream.
325 [ + + ]: 14362 : if (options().bv.bitblastMode == options::BitblastMode::EAGER)
326 : : {
327 : 9 : NodeManager* nm = nodeManager();
328 : 9 : std::vector<TNode> vars;
329 : 9 : d_cnfStream->getBooleanVariables(vars);
330 [ + + ]: 11 : for (TNode var : vars)
331 : : {
332 [ - + ][ - + ]: 2 : Assert(d_cnfStream->hasLiteral(var));
[ - - ]
333 : 2 : prop::SatLiteral bit = d_cnfStream->getLiteral(var);
334 : 2 : prop::SatValue value = d_satSolver->modelValue(bit);
335 [ - + ][ - + ]: 2 : Assert(value != prop::SAT_VALUE_UNKNOWN);
[ - - ]
336 : 2 : if (!m->assertEquality(
337 [ - + ]: 4 : var, nm->mkConst(value == prop::SAT_VALUE_TRUE), true))
338 : : {
339 : 0 : return false;
340 : : }
341 [ + - ]: 2 : }
342 [ + - ]: 9 : }
343 : :
344 : 14362 : return true;
345 : : }
346 : :
347 : 40233 : void BVSolverBitblast::initSatSolver()
348 : : {
349 : : const auto factory =
350 : 40233 : prop::SatSolverFactory::getFactory(options().bv.bvSatSolver);
351 : 80466 : d_satSolver.reset(factory(d_env,
352 : : statisticsRegistry(),
353 : 40233 : d_env.getResourceManager(),
354 : : "theory::bv::BVSolverBitblast::"));
355 : :
356 : 80466 : d_cnfStream.reset(new prop::CnfStream(d_env,
357 : 40233 : d_satSolver.get(),
358 : 40233 : d_bbRegistrar.get(),
359 : 40233 : d_nullContext.get(),
360 : : prop::FormulaLitPolicy::INTERNAL,
361 : 40233 : "theory::bv::BVSolverBitblast"));
362 : 40233 : }
363 : :
364 : 23415 : Node BVSolverBitblast::getValue(TNode node, bool initialize)
365 : : {
366 [ - + ]: 23415 : if (node.isConst())
367 : : {
368 : 0 : return node;
369 : : }
370 : :
371 : 23415 : NodeManager* nm = node.getNodeManager();
372 [ + + ]: 23415 : if (!d_bitblaster->hasBBTerm(node))
373 : : {
374 [ + + ][ + + ]: 682 : return initialize ? utils::mkConst(nm, utils::getSize(node), 0u) : Node();
[ - - ]
375 : : }
376 : :
377 : 22733 : std::vector<Node> bits;
378 : 22733 : d_bitblaster->getBBTerm(node, bits);
379 : 22733 : Integer value(0), one(1), zero(0), bit;
380 [ + + ]: 448581 : for (size_t i = 0, size = bits.size(), j = size - 1; i < size; ++i, --j)
381 : : {
382 [ + + ]: 426112 : if (d_cnfStream->hasLiteral(bits[j]))
383 : : {
384 : 424644 : prop::SatLiteral lit = d_cnfStream->getLiteral(bits[j]);
385 : 424644 : prop::SatValue val = d_satSolver->modelValue(lit);
386 [ + + ]: 424644 : bit = val == prop::SatValue::SAT_VALUE_TRUE ? one : zero;
387 : : }
388 : : else
389 : : {
390 [ + + ]: 1468 : if (!initialize) return Node();
391 : 1204 : bit = zero;
392 : : }
393 : 425848 : value = value * 2 + bit;
394 : : }
395 : 22469 : return utils::mkConst(nm, bits.size(), value);
396 : 22733 : }
397 : :
398 : 241 : void BVSolverBitblast::handleEagerAtom(TNode fact, bool assertFact)
399 : : {
400 [ - + ][ - + ]: 241 : Assert(fact.getKind() == Kind::BITVECTOR_EAGER_ATOM);
[ - - ]
401 : :
402 [ - + ]: 241 : if (assertFact)
403 : : {
404 : 0 : d_cnfStream->convertAndAssert(fact[0], false, false);
405 : : }
406 : : else
407 : : {
408 : 241 : d_cnfStream->ensureLiteral(fact[0]);
409 : : }
410 : :
411 : : /* convertAndAssert() does not make the connection between the bit-vector
412 : : * atom and it's bit-blasted form (it only calls preRegister() from the
413 : : * registrar). Thus, we add the equalities now. */
414 : 241 : auto& registeredAtoms = d_bbRegistrar->getRegisteredAtoms();
415 [ + + ]: 757 : for (auto atom : registeredAtoms)
416 : : {
417 : 516 : Node bb_atom = d_bitblaster->getStoredBBAtom(atom);
418 : 516 : d_cnfStream->convertAndAssert(atom.eqNode(bb_atom), false, false);
419 : 516 : }
420 : : // Clear cache since we only need to do this once per bit-blasted atom.
421 : 241 : registeredAtoms.clear();
422 : 241 : }
423 : :
424 : : } // namespace bv
425 : : } // namespace theory
426 : : } // namespace cvc5::internal
|
