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