Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Mathias Preiner, Andrew Reynolds, Aina Niemetz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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 : : * ****************************************************************************
12 : : *
13 : : * Bit-blasting solver that supports multiple SAT backends.
14 : : */
15 : :
16 : : #include "theory/bv/bv_solver_bitblast.h"
17 : :
18 : : #include "options/bv_options.h"
19 : : #include "prop/sat_solver_factory.h"
20 : : #include "theory/bv/theory_bv.h"
21 : : #include "theory/bv/theory_bv_utils.h"
22 : : #include "theory/theory_model.h"
23 : :
24 : : namespace cvc5::internal {
25 : : namespace theory {
26 : : namespace bv {
27 : :
28 : : /**
29 : : * Notifies the BV solver when assertions were reset.
30 : : *
31 : : * This class is notified after every user-context pop and maintains a flag
32 : : * that indicates whether assertions have been reset. If the user-context level
33 : : * reaches level 0 it means that the assertions were reset.
34 : : */
35 : : class NotifyResetAssertions : public context::ContextNotifyObj
36 : : {
37 : : public:
38 : 40092 : NotifyResetAssertions(context::Context* c)
39 : 40092 : : context::ContextNotifyObj(c, false),
40 : : d_context(c),
41 : 40092 : d_doneResetAssertions(false)
42 : : {
43 : 40092 : }
44 : :
45 : 8 : bool doneResetAssertions() { return d_doneResetAssertions; }
46 : :
47 : 2 : void reset() { d_doneResetAssertions = false; }
48 : :
49 : : protected:
50 : 47469 : void contextNotifyPop() override
51 : : {
52 : : // If the user-context level reaches 0 it means that reset-assertions was
53 : : // called.
54 [ + + ]: 47469 : if (d_context->getLevel() == 0)
55 : : {
56 : 40223 : d_doneResetAssertions = true;
57 : : }
58 : 47469 : }
59 : :
60 : : private:
61 : : /** The user-context. */
62 : : context::Context* d_context;
63 : :
64 : : /** Flag to notify whether reset assertions was called. */
65 : : bool d_doneResetAssertions;
66 : : };
67 : :
68 : : /**
69 : : * Bit-blasting registrar.
70 : : *
71 : : * The CnfStream calls preRegister() if it encounters a theory atom.
72 : : * This registrar bit-blasts given atom and remembers which bit-vector atoms
73 : : * were bit-blasted.
74 : : *
75 : : * This registrar is needed when --bitblast=eager is enabled.
76 : : */
77 : : class BBRegistrar : public prop::Registrar
78 : : {
79 : : public:
80 : 40092 : BBRegistrar(NodeBitblaster* bb) : d_bitblaster(bb) {}
81 : :
82 : 158739 : void notifySatLiteral(Node n) override
83 : : {
84 [ - + ]: 158739 : if (d_registeredAtoms.find(n) != d_registeredAtoms.end())
85 : : {
86 : 0 : return;
87 : : }
88 : : /* We are only interested in bit-vector atoms. */
89 : 159158 : if ((n.getKind() == Kind::EQUAL && n[0].getType().isBitVector())
90 [ + + ]: 158320 : || n.getKind() == Kind::BITVECTOR_ULT
91 [ + - ]: 158223 : || n.getKind() == Kind::BITVECTOR_ULE
92 [ + - ]: 158223 : || n.getKind() == Kind::BITVECTOR_SLT
93 [ + + ][ - + ]: 317478 : || n.getKind() == Kind::BITVECTOR_SLE)
[ + + ]
94 : : {
95 : 516 : d_registeredAtoms.insert(n);
96 : 516 : d_bitblaster->bbAtom(n);
97 : : }
98 : : }
99 : :
100 : 241 : std::unordered_set<TNode>& getRegisteredAtoms() { return d_registeredAtoms; }
101 : :
102 : : private:
103 : : /** The bitblaster used. */
104 : : NodeBitblaster* d_bitblaster;
105 : :
106 : : /** Stores bit-vector atoms encounterd on preRegister(). */
107 : : std::unordered_set<TNode> d_registeredAtoms;
108 : : };
109 : :
110 : 40092 : BVSolverBitblast::BVSolverBitblast(Env& env,
111 : : TheoryState* s,
112 : 40092 : TheoryInferenceManager& inferMgr)
113 : : : BVSolver(env, *s, inferMgr),
114 : 40092 : d_bitblaster(new NodeBitblaster(env, s)),
115 : 40092 : d_bbRegistrar(new BBRegistrar(d_bitblaster.get())),
116 : 40092 : d_nullContext(new context::Context()),
117 : : d_bbFacts(context()),
118 : : d_bbInputFacts(context()),
119 : : d_assumptions(context()),
120 : : d_assertions(context()),
121 : 80184 : d_epg(env.isTheoryProofProducing()
122 : 42 : ? new EagerProofGenerator(env, userContext(), "")
123 : : : nullptr),
124 : : d_bvProofChecker(nodeManager()),
125 : : d_factLiteralCache(context()),
126 : : d_literalFactCache(context()),
127 : 40092 : d_propagate(options().bv.bitvectorPropagate),
128 : 200502 : d_resetNotify(new NotifyResetAssertions(userContext()))
129 : : {
130 [ + + ]: 40092 : if (env.isTheoryProofProducing())
131 : : {
132 : 21 : d_bvProofChecker.registerTo(env.getProofNodeManager()->getChecker());
133 : : }
134 : :
135 : 40092 : initSatSolver();
136 : 40092 : }
137 : :
138 : 40092 : bool BVSolverBitblast::needsEqualityEngine(EeSetupInfo& esi)
139 : : {
140 : : // we always need the equality engine if sharing is enabled for processing
141 : : // equality engine and shared terms
142 [ + + ][ + - ]: 40092 : return logicInfo().isSharingEnabled() || options().bv.bvEqEngine;
143 : : }
144 : :
145 : 2327190 : void BVSolverBitblast::postCheck(Theory::Effort level)
146 : : {
147 [ + + ]: 2327190 : if (level != Theory::Effort::EFFORT_FULL)
148 : : {
149 : : /* Do bit-level propagation only if the SAT solver supports it. */
150 [ - + ][ - - ]: 2258310 : if (!d_propagate || !d_satSolver->setPropagateOnly())
[ + - ]
151 : : {
152 : 2258310 : return;
153 : : }
154 : : }
155 : :
156 : : // If we permanently added assertions to the SAT solver and the assertions
157 : : // were reset, we have to reset the SAT solver and the CNF stream.
158 [ + + ][ + + ]: 68881 : if (options().bv.bvAssertInput && d_resetNotify->doneResetAssertions())
[ + + ]
159 : : {
160 : 2 : d_satSolver.reset(nullptr);
161 : 2 : d_cnfStream.reset(nullptr);
162 : 2 : initSatSolver();
163 : 2 : d_resetNotify->reset();
164 : : }
165 : :
166 : 68881 : NodeManager* nm = nodeManager();
167 : :
168 : : /* Process input assertions bit-blast queue. */
169 [ + + ]: 68889 : while (!d_bbInputFacts.empty())
170 : : {
171 : 16 : Node fact = d_bbInputFacts.front();
172 : 8 : d_bbInputFacts.pop();
173 : : /* Bit-blast fact and cache literal. */
174 [ + - ]: 8 : if (d_factLiteralCache.find(fact) == d_factLiteralCache.end())
175 : : {
176 [ - + ]: 8 : if (fact.getKind() == Kind::BITVECTOR_EAGER_ATOM)
177 : : {
178 : 0 : handleEagerAtom(fact, true);
179 : : }
180 : : else
181 : : {
182 : 8 : d_bitblaster->bbAtom(fact);
183 : 8 : Node bb_fact = d_bitblaster->getStoredBBAtom(fact);
184 : 8 : d_cnfStream->convertAndAssert(bb_fact, false, false);
185 : : }
186 : : }
187 : 8 : d_assertions.push_back(fact);
188 : : }
189 : :
190 : : /* Process bit-blast queue and store SAT literals. */
191 [ + + ]: 7676070 : while (!d_bbFacts.empty())
192 : : {
193 : 7607190 : Node fact = d_bbFacts.front();
194 : 7607190 : d_bbFacts.pop();
195 : : /* Bit-blast fact and cache literal. */
196 [ + - ]: 7607190 : if (d_factLiteralCache.find(fact) == d_factLiteralCache.end())
197 : : {
198 : 7607190 : prop::SatLiteral lit;
199 [ + + ]: 7607190 : if (fact.getKind() == Kind::BITVECTOR_EAGER_ATOM)
200 : : {
201 : 241 : handleEagerAtom(fact, false);
202 : 241 : lit = d_cnfStream->getLiteral(fact[0]);
203 : : }
204 : : else
205 : : {
206 : 7606950 : d_bitblaster->bbAtom(fact);
207 : 7606950 : Node bb_fact = d_bitblaster->getStoredBBAtom(fact);
208 : 7606950 : d_cnfStream->ensureLiteral(bb_fact);
209 : 7606950 : lit = d_cnfStream->getLiteral(bb_fact);
210 : : }
211 : 7607190 : d_factLiteralCache[fact] = lit;
212 : 7607190 : d_literalFactCache[lit] = fact;
213 : : }
214 : 7607190 : d_assumptions.push_back(d_factLiteralCache[fact]);
215 : : }
216 : :
217 : : std::vector<prop::SatLiteral> assumptions(d_assumptions.begin(),
218 : 137762 : d_assumptions.end());
219 : 68881 : prop::SatValue val = d_satSolver->solve(assumptions);
220 : :
221 [ + + ]: 68881 : if (val == prop::SatValue::SAT_VALUE_FALSE)
222 : : {
223 : 40160 : std::vector<prop::SatLiteral> unsat_assumptions;
224 : 20080 : d_satSolver->getUnsatAssumptions(unsat_assumptions);
225 : :
226 : 40160 : Node conflict;
227 : : // Unsat assumptions produce conflict.
228 [ + - ]: 20080 : if (unsat_assumptions.size() > 0)
229 : : {
230 : 20080 : std::vector<Node> conf;
231 [ + + ]: 173691 : for (const prop::SatLiteral& lit : unsat_assumptions)
232 : : {
233 : 153611 : conf.push_back(d_literalFactCache[lit]);
234 [ + - ]: 307222 : Trace("bv-bitblast")
235 : 153611 : << "unsat assumption (" << lit << "): " << conf.back() << std::endl;
236 : : }
237 : 20080 : conflict = nm->mkAnd(conf);
238 : : }
239 : : else // Input assertions produce conflict.
240 : : {
241 : 0 : std::vector<Node> assertions(d_assertions.begin(), d_assertions.end());
242 : 0 : conflict = nm->mkAnd(assertions);
243 : : }
244 : 20080 : TrustNode tconflict;
245 [ + + ]: 20080 : if (d_epg != nullptr)
246 : : {
247 : 1534 : tconflict = d_epg->mkTrustNodeTrusted(
248 : 767 : conflict, TrustId::BV_BITBLAST_CONFLICT, {}, {}, true);
249 : : }
250 : : else
251 : : {
252 : 19313 : tconflict = TrustNode::mkTrustConflict(conflict, nullptr);
253 : : }
254 : 20080 : d_im.trustedConflict(tconflict, InferenceId::BV_BITBLAST_CONFLICT);
255 : : }
256 : : }
257 : :
258 : 4079890 : bool BVSolverBitblast::preNotifyFact(
259 : : TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
260 : : {
261 : 4079890 : 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 [ + + ][ + + ]: 4079890 : 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 : 4079880 : 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 [ + + ][ - + ]: 4079890 : return !logicInfo().isSharingEnabled() && !options().bv.bvEqEngine;
282 : : }
283 : :
284 : 1652 : TrustNode BVSolverBitblast::explain(TNode n)
285 : : {
286 [ + - ]: 1652 : Trace("bv-bitblast") << "explain called on " << n << std::endl;
287 : 1652 : return d_im.explainLit(n);
288 : : }
289 : :
290 : 14902 : 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 [ + + ]: 14902 : if (options().bv.bitblastMode == options::BitblastMode::EAGER)
300 : : {
301 : 9 : d_bitblaster->computeRelevantTerms(termSet);
302 : : }
303 : 14902 : }
304 : :
305 : 14902 : bool BVSolverBitblast::collectModelValues(TheoryModel* m,
306 : : const std::set<Node>& termSet)
307 : : {
308 [ + + ]: 341944 : for (const auto& term : termSet)
309 : : {
310 [ + + ]: 327042 : if (!d_bitblaster->isVariable(term))
311 : : {
312 : 305977 : continue;
313 : : }
314 : :
315 : 21065 : Node value = getValue(term, true);
316 [ - + ][ - + ]: 21065 : Assert(value.isConst());
[ - - ]
317 [ - + ]: 21065 : if (!m->assertEquality(term, value, true))
318 : : {
319 : 0 : return false;
320 : : }
321 : : }
322 : :
323 : : // In eager bitblast mode we also have to collect the model values for
324 : : // Boolean variables in the CNF stream.
325 [ + + ]: 14902 : 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 : : }
342 : : }
343 : :
344 : 14902 : return true;
345 : : }
346 : :
347 : 40094 : void BVSolverBitblast::initSatSolver()
348 : : {
349 [ + + ]: 40094 : switch (options().bv.bvSatSolver)
350 : : {
351 : 10 : case options::BvSatSolverMode::CRYPTOMINISAT:
352 : 20 : d_satSolver.reset(prop::SatSolverFactory::createCryptoMinisat(
353 : : statisticsRegistry(),
354 : 10 : d_env.getResourceManager(),
355 : : "theory::bv::BVSolverBitblast::"));
356 : 10 : break;
357 : 40084 : default:
358 : 80168 : d_satSolver.reset(prop::SatSolverFactory::createCadical(
359 : : d_env,
360 : : statisticsRegistry(),
361 : 40084 : d_env.getResourceManager(),
362 : : "theory::bv::BVSolverBitblast::"));
363 : : }
364 : 80188 : d_cnfStream.reset(new prop::CnfStream(d_env,
365 : 40094 : d_satSolver.get(),
366 : 40094 : d_bbRegistrar.get(),
367 : 40094 : d_nullContext.get(),
368 : : prop::FormulaLitPolicy::INTERNAL,
369 : 40094 : "theory::bv::BVSolverBitblast"));
370 : 40094 : }
371 : :
372 : 22542 : Node BVSolverBitblast::getValue(TNode node, bool initialize)
373 : : {
374 [ - + ]: 22542 : if (node.isConst())
375 : : {
376 : 0 : return node;
377 : : }
378 : :
379 : 22542 : NodeManager* nm = node.getNodeManager();
380 [ + + ]: 22542 : if (!d_bitblaster->hasBBTerm(node))
381 : : {
382 [ + + ][ + + ]: 648 : return initialize ? utils::mkConst(nm, utils::getSize(node), 0u) : Node();
[ - - ]
383 : : }
384 : :
385 : 43788 : std::vector<Node> bits;
386 : 21894 : d_bitblaster->getBBTerm(node, bits);
387 : 43788 : Integer value(0), one(1), zero(0), bit;
388 [ + + ]: 576668 : for (size_t i = 0, size = bits.size(), j = size - 1; i < size; ++i, --j)
389 : : {
390 [ + + ]: 555022 : if (d_cnfStream->hasLiteral(bits[j]))
391 : : {
392 : 553028 : prop::SatLiteral lit = d_cnfStream->getLiteral(bits[j]);
393 : 553028 : prop::SatValue val = d_satSolver->modelValue(lit);
394 [ + + ]: 553028 : bit = val == prop::SatValue::SAT_VALUE_TRUE ? one : zero;
395 : : }
396 : : else
397 : : {
398 [ + + ]: 1994 : if (!initialize) return Node();
399 : 1746 : bit = zero;
400 : : }
401 : 554774 : value = value * 2 + bit;
402 : : }
403 : 21646 : return utils::mkConst(nm, bits.size(), value);
404 : : }
405 : :
406 : 241 : void BVSolverBitblast::handleEagerAtom(TNode fact, bool assertFact)
407 : : {
408 [ - + ][ - + ]: 241 : Assert(fact.getKind() == Kind::BITVECTOR_EAGER_ATOM);
[ - - ]
409 : :
410 [ - + ]: 241 : if (assertFact)
411 : : {
412 : 0 : d_cnfStream->convertAndAssert(fact[0], false, false);
413 : : }
414 : : else
415 : : {
416 : 241 : d_cnfStream->ensureLiteral(fact[0]);
417 : : }
418 : :
419 : : /* convertAndAssert() does not make the connection between the bit-vector
420 : : * atom and it's bit-blasted form (it only calls preRegister() from the
421 : : * registrar). Thus, we add the equalities now. */
422 : 241 : auto& registeredAtoms = d_bbRegistrar->getRegisteredAtoms();
423 [ + + ]: 757 : for (auto atom : registeredAtoms)
424 : : {
425 : 516 : Node bb_atom = d_bitblaster->getStoredBBAtom(atom);
426 : 516 : d_cnfStream->convertAndAssert(atom.eqNode(bb_atom), false, false);
427 : : }
428 : : // Clear cache since we only need to do this once per bit-blasted atom.
429 : 241 : registeredAtoms.clear();
430 : 241 : }
431 : :
432 : : } // namespace bv
433 : : } // namespace theory
434 : : } // namespace cvc5::internal
|
