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