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 : : * Theory of bit-vectors.
11 : : */
12 : :
13 : : #include "theory/bv/theory_bv.h"
14 : :
15 : : #include "expr/skolem_manager.h"
16 : : #include "options/bv_options.h"
17 : : #include "options/smt_options.h"
18 : : #include "proof/proof_checker.h"
19 : : #include "theory/bv/bv_solver_bitblast.h"
20 : : #include "theory/bv/bv_solver_bitblast_internal.h"
21 : : #include "theory/bv/theory_bv_rewrite_rules_normalization.h"
22 : : #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
23 : : #include "theory/bv/theory_bv_utils.h"
24 : : #include "theory/ee_setup_info.h"
25 : : #include "theory/uf/equality_engine.h"
26 : :
27 : : namespace cvc5::internal {
28 : : namespace theory {
29 : : namespace bv {
30 : :
31 : 51048 : TheoryBV::TheoryBV(Env& env,
32 : : OutputChannel& out,
33 : : Valuation valuation,
34 : 51048 : std::string name)
35 : : : Theory(THEORY_BV, env, out, valuation, name),
36 : 51048 : d_internal(nullptr),
37 : 51048 : d_ppAssert(env, valuation),
38 : 51048 : d_rewriter(nodeManager()),
39 : 51048 : d_state(env, valuation),
40 : 51048 : d_im(env, *this, d_state, "theory::bv::"),
41 : 51048 : d_notify(d_im),
42 : 51048 : d_invalidateModelCache(context(), true),
43 : 51048 : d_stats(statisticsRegistry(), "theory::bv::"),
44 : 153144 : d_checker(nodeManager())
45 : : {
46 [ + + ]: 51048 : switch (options().bv.bvSolver)
47 : : {
48 : 40253 : case options::BVSolver::BITBLAST:
49 : 40253 : d_internal.reset(new BVSolverBitblast(env, &d_state, d_im));
50 : 40253 : break;
51 : :
52 : 10795 : default:
53 [ - + ][ - + ]: 10795 : AlwaysAssert(options().bv.bvSolver == options::BVSolver::BITBLAST_INTERNAL);
[ - - ]
54 : 10795 : d_internal.reset(new BVSolverBitblastInternal(d_env, &d_state, d_im));
55 : : }
56 : 51048 : d_theoryState = &d_state;
57 : 51048 : d_inferManager = &d_im;
58 : 51048 : }
59 : :
60 : 101406 : TheoryBV::~TheoryBV() {}
61 : :
62 : 51048 : TheoryRewriter* TheoryBV::getTheoryRewriter() { return &d_rewriter; }
63 : :
64 : 19795 : ProofRuleChecker* TheoryBV::getProofChecker() { return &d_checker; }
65 : :
66 : 51048 : bool TheoryBV::needsEqualityEngine(EeSetupInfo& esi)
67 : : {
68 : 51048 : bool need_ee = d_internal->needsEqualityEngine(esi);
69 : :
70 : : /* Set up default notify class for equality engine. */
71 [ + + ][ + - ]: 51048 : if (need_ee && esi.d_notify == nullptr)
72 : : {
73 : 51023 : esi.d_notify = &d_notify;
74 : 51023 : esi.d_name = "theory::bv::ee";
75 : : }
76 : :
77 : 51048 : return need_ee;
78 : : }
79 : :
80 : 51048 : void TheoryBV::finishInit()
81 : : {
82 : : // these kinds are semi-evaluated in getModelValue (applications of this
83 : : // kind are treated as variables)
84 : 51048 : getValuation().setSemiEvaluatedKind(Kind::BITVECTOR_ACKERMANNIZE_UDIV);
85 : 51048 : getValuation().setSemiEvaluatedKind(Kind::BITVECTOR_ACKERMANNIZE_UREM);
86 : 51048 : d_internal->finishInit();
87 : :
88 : 51048 : eq::EqualityEngine* ee = getEqualityEngine();
89 [ + + ]: 51048 : if (ee)
90 : : {
91 : 51023 : bool eagerEval = options().bv.bvEagerEval;
92 : : // The kinds we are treating as function application in congruence
93 : 51023 : ee->addFunctionKind(Kind::BITVECTOR_CONCAT, eagerEval);
94 : : // ee->addFunctionKind(Kind::BITVECTOR_AND);
95 : : // ee->addFunctionKind(Kind::BITVECTOR_OR);
96 : : // ee->addFunctionKind(Kind::BITVECTOR_XOR);
97 : : // ee->addFunctionKind(Kind::BITVECTOR_NOT);
98 : : // ee->addFunctionKind(Kind::BITVECTOR_NAND);
99 : : // ee->addFunctionKind(Kind::BITVECTOR_NOR);
100 : : // ee->addFunctionKind(Kind::BITVECTOR_XNOR);
101 : : // ee->addFunctionKind(Kind::BITVECTOR_COMP);
102 : 51023 : ee->addFunctionKind(Kind::BITVECTOR_MULT, eagerEval);
103 : 51023 : ee->addFunctionKind(Kind::BITVECTOR_ADD, eagerEval);
104 : 51023 : ee->addFunctionKind(Kind::BITVECTOR_EXTRACT, eagerEval);
105 : : // ee->addFunctionKind(Kind::BITVECTOR_SUB);
106 : : // ee->addFunctionKind(Kind::BITVECTOR_NEG);
107 : : // ee->addFunctionKind(Kind::BITVECTOR_UDIV);
108 : : // ee->addFunctionKind(Kind::BITVECTOR_UREM);
109 : : // ee->addFunctionKind(Kind::BITVECTOR_SDIV);
110 : : // ee->addFunctionKind(Kind::BITVECTOR_SREM);
111 : : // ee->addFunctionKind(Kind::BITVECTOR_SMOD);
112 : : // ee->addFunctionKind(Kind::BITVECTOR_SHL);
113 : : // ee->addFunctionKind(Kind::BITVECTOR_LSHR);
114 : : // ee->addFunctionKind(Kind::BITVECTOR_ASHR);
115 : : // ee->addFunctionKind(Kind::BITVECTOR_ULT);
116 : : // ee->addFunctionKind(Kind::BITVECTOR_ULE);
117 : : // ee->addFunctionKind(Kind::BITVECTOR_UGT);
118 : : // ee->addFunctionKind(Kind::BITVECTOR_UGE);
119 : : // ee->addFunctionKind(Kind::BITVECTOR_SLT);
120 : : // ee->addFunctionKind(Kind::BITVECTOR_SLE);
121 : : // ee->addFunctionKind(Kind::BITVECTOR_SGT);
122 : : // ee->addFunctionKind(Kind::BITVECTOR_SGE);
123 : : }
124 : 51048 : }
125 : :
126 : 449016 : void TheoryBV::preRegisterTerm(TNode node)
127 : : {
128 : 449016 : d_internal->preRegisterTerm(node);
129 : :
130 : 449016 : eq::EqualityEngine* ee = getEqualityEngine();
131 [ + + ]: 449016 : if (ee)
132 : : {
133 [ + + ]: 445980 : if (node.getKind() == Kind::EQUAL)
134 : : {
135 : 72054 : d_state.addEqualityEngineTriggerPredicate(node);
136 : : }
137 : : else
138 : : {
139 : 373926 : ee->addTerm(node);
140 : : }
141 : : }
142 : 449016 : }
143 : :
144 : 2852342 : bool TheoryBV::preCheck(Effort e) { return d_internal->preCheck(e); }
145 : :
146 : 2852342 : void TheoryBV::postCheck(Effort e)
147 : : {
148 : 2852342 : d_invalidateModelCache = true;
149 : 2852342 : d_internal->postCheck(e);
150 : 2852342 : }
151 : :
152 : 7641666 : bool TheoryBV::preNotifyFact(
153 : : TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
154 : : {
155 : 7641666 : return d_internal->preNotifyFact(atom, pol, fact, isPrereg, isInternal);
156 : : }
157 : :
158 : 7638190 : void TheoryBV::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal)
159 : : {
160 : 7638190 : d_internal->notifyFact(atom, pol, fact, isInternal);
161 : 7638190 : }
162 : :
163 : 30259 : bool TheoryBV::needsCheckLastEffort()
164 : : {
165 : 30259 : return d_internal->needsCheckLastEffort();
166 : : }
167 : :
168 : 18682 : void TheoryBV::computeRelevantTerms(std::set<Node>& termSet)
169 : : {
170 : 18682 : return d_internal->computeRelevantTerms(termSet);
171 : : }
172 : :
173 : 18682 : bool TheoryBV::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
174 : : {
175 : 18682 : return d_internal->collectModelValues(m, termSet);
176 : : }
177 : :
178 : 4389525 : void TheoryBV::propagate(Effort e) { return d_internal->propagate(e); }
179 : :
180 : 6846 : bool TheoryBV::ppAssert(TrustNode tin, TrustSubstitutionMap& outSubstitutions)
181 : : {
182 : 6846 : Kind k = tin.getNode().getKind();
183 [ + + ]: 6846 : if (k == Kind::EQUAL)
184 : : {
185 : 2857 : bool status = Theory::ppAssert(tin, outSubstitutions);
186 [ + + ]: 2857 : if (status)
187 : : {
188 : 1265 : return status;
189 : : }
190 [ + + ]: 1592 : if (d_ppAssert.ppAssert(tin, outSubstitutions))
191 : : {
192 : 107 : return true;
193 : : }
194 : : }
195 : 5474 : return false;
196 : : }
197 : :
198 : 347420 : TrustNode TheoryBV::ppRewrite(TNode t,
199 : : CVC5_UNUSED std::vector<SkolemLemma>& lems)
200 : : {
201 [ + - ]: 347420 : Trace("theory-bv-pp-rewrite") << "ppRewrite " << t << "\n";
202 : 347420 : Node res = t;
203 : : // useful on QF_BV/space/ndist
204 [ + + ]: 347420 : if (RewriteRule<UltAddOne>::applies(t))
205 : : {
206 : 68 : res = RewriteRule<UltAddOne>::run<false>(t);
207 : : }
208 : : // When int-blasting, it is better to handle most overflow operators
209 : : // natively, rather than to eliminate them eagerly.
210 [ + + ]: 347420 : if (options().smt.solveBVAsInt == options::SolveBVAsIntMode::OFF)
211 : : {
212 : 347144 : res = d_rewriter.eliminateOverflows(res);
213 : : }
214 : :
215 [ + - ]: 347420 : Trace("theory-bv-pp-rewrite") << "to " << res << "\n";
216 [ + + ]: 347420 : if (res != t)
217 : : {
218 : 199 : return TrustNode::mkTrustRewrite(t, res, nullptr);
219 : : }
220 : :
221 : 347221 : return d_internal->ppRewrite(t);
222 : 347420 : }
223 : :
224 : 1025104 : TrustNode TheoryBV::ppStaticRewrite(TNode atom)
225 : : {
226 : 1025104 : Kind k = atom.getKind();
227 [ + + ]: 1025104 : if (k == Kind::EQUAL)
228 : : {
229 [ + + ]: 103311 : if (RewriteRule<SolveEq>::applies(atom))
230 : : {
231 : 82105 : Node res = RewriteRule<SolveEq>::run<false>(atom);
232 [ + + ]: 82105 : if (res != atom)
233 : : {
234 : 1060 : return TrustNode::mkTrustRewrite(atom, res);
235 : : }
236 [ + + ]: 82105 : }
237 [ + + ][ + + ]: 102251 : if (options().bv.bitwiseEq && RewriteRule<BitwiseEq>::applies(atom))
[ + + ][ + + ]
[ - - ]
238 : : {
239 : 14 : Node res = RewriteRule<BitwiseEq>::run<false>(atom);
240 [ + - ]: 14 : if (res != atom)
241 : : {
242 : 14 : return TrustNode::mkTrustRewrite(atom, res);
243 : : }
244 [ - + ]: 14 : }
245 : : // Useful for BV/2017-Preiner-scholl-smt08, but not for QF_BV
246 [ - + ]: 102237 : if (options().bv.rwExtendEq)
247 : : {
248 : 0 : Node res;
249 [ - - ]: 0 : if (RewriteRule<SignExtendEqConst>::applies(atom))
250 : : {
251 : 0 : res = RewriteRule<SignExtendEqConst>::run<false>(atom);
252 : : }
253 [ - - ]: 0 : else if (RewriteRule<ZeroExtendEqConst>::applies(atom))
254 : : {
255 : 0 : res = RewriteRule<ZeroExtendEqConst>::run<false>(atom);
256 : : }
257 [ - - ]: 0 : if (res != atom)
258 : : {
259 : 0 : return TrustNode::mkTrustRewrite(atom, res);
260 : : }
261 [ - - ]: 0 : }
262 : : }
263 : 1024030 : return TrustNode::null();
264 : : }
265 : :
266 : 50487 : void TheoryBV::presolve() { d_internal->presolve(); }
267 : :
268 : 37293 : EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
269 : : {
270 : 37293 : EqualityStatus status = d_internal->getEqualityStatus(a, b);
271 : :
272 [ + - ]: 37293 : if (status == EqualityStatus::EQUALITY_UNKNOWN)
273 : : {
274 : 37293 : Node value_a = getValue(a);
275 : 37293 : Node value_b = getValue(b);
276 : :
277 [ + - ][ - + ]: 37293 : if (value_a.isNull() || value_b.isNull())
[ - + ]
278 : : {
279 : 0 : return status;
280 : : }
281 : :
282 [ + + ]: 37293 : if (value_a == value_b)
283 : : {
284 [ + - ]: 3029 : Trace("theory-bv") << EQUALITY_TRUE_IN_MODEL << std::endl;
285 : 3029 : return EQUALITY_TRUE_IN_MODEL;
286 : : }
287 [ + - ]: 34264 : Trace("theory-bv") << EQUALITY_FALSE_IN_MODEL << std::endl;
288 : 34264 : return EQUALITY_FALSE_IN_MODEL;
289 : 37293 : }
290 : 0 : return status;
291 : : }
292 : :
293 : 3879 : TrustNode TheoryBV::explain(TNode node) { return d_internal->explain(node); }
294 : :
295 : 131396 : void TheoryBV::notifySharedTerm(TNode t)
296 : : {
297 : 131396 : d_internal->notifySharedTerm(t);
298 : 131396 : }
299 : :
300 : 344924 : void TheoryBV::ppStaticLearn(TNode in, std::vector<TrustNode>& learned)
301 : : {
302 [ + + ]: 344924 : if (in.getKind() == Kind::EQUAL)
303 : : {
304 : : // Only useful in combination with --bv-intro-pow2 on
305 : : // QF_BV/pspace/power2sum benchmarks.
306 : : //
307 : : // Matches for equality:
308 : : //
309 : : // (= (bvadd (bvshl 1 x) (bvshl 1 y)) (bvshl 1 z))
310 : : //
311 : : // and does case analysis on the sum of two power of twos.
312 [ + + ][ - - ]: 38562 : if ((in[0].getKind() == Kind::BITVECTOR_ADD
313 [ + - ][ + - ]: 38567 : && in[1].getKind() == Kind::BITVECTOR_SHL)
[ - - ]
314 [ + + ][ + + ]: 77414 : || (in[1].getKind() == Kind::BITVECTOR_ADD
[ + + ][ - - ]
315 [ + + ][ + + ]: 38847 : && in[0].getKind() == Kind::BITVECTOR_SHL))
[ + - ][ - - ]
316 : : {
317 [ - + ]: 5 : TNode p = in[0].getKind() == Kind::BITVECTOR_ADD ? in[0] : in[1];
318 [ - + ]: 5 : TNode s = in[0].getKind() == Kind::BITVECTOR_ADD ? in[1] : in[0];
319 : :
320 [ + - ][ + - ]: 10 : if (p.getNumChildren() == 2 && p[0].getKind() == Kind::BITVECTOR_SHL
[ - - ]
321 [ + - ][ + - ]: 10 : && p[1].getKind() == Kind::BITVECTOR_SHL)
[ + - ][ + - ]
[ - - ]
322 : : {
323 : 10 : if (utils::isOne(s[0]) && utils::isOne(p[0][0])
324 : 10 : && utils::isOne(p[1][0]))
325 : : {
326 : 5 : Node zero = utils::mkZero(nodeManager(), utils::getSize(s));
327 : 5 : TNode b = p[0];
328 : 5 : TNode c = p[1];
329 : : // (s : 1 << S) = (b : 1 << B) + (c : 1 << C)
330 : 5 : Node b_eq_0 = b.eqNode(zero);
331 : 5 : Node c_eq_0 = c.eqNode(zero);
332 : 5 : Node b_eq_c = b.eqNode(c);
333 : :
334 : 10 : Node dis = nodeManager()->mkNode(Kind::OR, b_eq_0, c_eq_0, b_eq_c);
335 : 5 : Node imp = in.impNode(dis);
336 : 5 : TrustNode trn = TrustNode::mkTrustLemma(imp, nullptr);
337 : 5 : learned.emplace_back(trn);
338 : 5 : }
339 : : }
340 : 5 : }
341 : : }
342 : :
343 : 344924 : d_internal->ppStaticLearn(in, learned);
344 : 344924 : }
345 : :
346 : 74586 : Node TheoryBV::getValue(TNode node)
347 : : {
348 [ + + ]: 74586 : if (d_invalidateModelCache.get())
349 : : {
350 : 426 : d_modelCache.clear();
351 : : }
352 : 74586 : d_invalidateModelCache.set(false);
353 : :
354 : 74586 : std::vector<TNode> visit;
355 : :
356 : 74586 : TNode cur;
357 : 74586 : visit.push_back(node);
358 : : do
359 : : {
360 : 75387 : cur = visit.back();
361 : 75387 : visit.pop_back();
362 : :
363 : 75387 : auto it = d_modelCache.find(cur);
364 [ + + ][ + + ]: 75387 : if (it != d_modelCache.end() && !it->second.isNull())
[ + + ]
365 : : {
366 : 74829 : continue;
367 : : }
368 : :
369 [ + + ]: 2119 : if (cur.isConst())
370 : : {
371 : 378 : d_modelCache[cur] = cur;
372 : 378 : continue;
373 : : }
374 : :
375 : 1741 : Node value = d_internal->getValue(cur, false);
376 [ + + ]: 1741 : if (value.isConst())
377 : : {
378 : 776 : d_modelCache[cur] = value;
379 : 776 : continue;
380 : : }
381 : :
382 [ + + ]: 965 : if (Theory::isLeafOf(cur, theory::THEORY_BV))
383 : : {
384 : 407 : value = d_internal->getValue(cur, true);
385 : 407 : d_modelCache[cur] = value;
386 : 407 : continue;
387 : : }
388 : :
389 [ + + ]: 558 : if (it == d_modelCache.end())
390 : : {
391 : 279 : visit.push_back(cur);
392 : 279 : d_modelCache.emplace(cur, Node());
393 : 279 : visit.insert(visit.end(), cur.begin(), cur.end());
394 : : }
395 [ + - ]: 279 : else if (it->second.isNull())
396 : : {
397 : 279 : NodeBuilder nb(nodeManager(), cur.getKind());
398 [ + + ]: 279 : if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
399 : : {
400 : 38 : nb << cur.getOperator();
401 : : }
402 : :
403 : 279 : std::unordered_map<Node, Node>::iterator iit;
404 [ + + ]: 801 : for (const TNode& child : cur)
405 : : {
406 : 522 : iit = d_modelCache.find(child);
407 [ - + ][ - + ]: 522 : Assert(iit != d_modelCache.end());
[ - - ]
408 [ - + ][ - + ]: 522 : Assert(iit->second.isConst());
[ - - ]
409 : 522 : nb << iit->second;
410 : 522 : }
411 : 279 : it->second = rewrite(nb.constructNode());
412 : 279 : }
413 [ + + ][ + + ]: 77128 : } while (!visit.empty());
414 : :
415 : 74586 : auto it = d_modelCache.find(node);
416 [ - + ][ - + ]: 74586 : Assert(it != d_modelCache.end());
[ - - ]
417 : 149172 : return it->second;
418 : 74586 : }
419 : :
420 : 51048 : TheoryBV::Statistics::Statistics(StatisticsRegistry& reg,
421 : 51048 : const std::string& name)
422 : 51048 : : d_solveSubstitutions(reg.registerInt(name + "NumSolveSubstitutions"))
423 : : {
424 : 51048 : }
425 : :
426 : : } // namespace bv
427 : : } // namespace theory
428 : : } // namespace cvc5::internal
|
