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 : : * The bit-vector arithmetic abstraction module.
11 : : */
12 : :
13 : : #include "theory/bv/abstract/abstraction_module.h"
14 : :
15 : : #include <algorithm>
16 : :
17 : : #include "expr/node_manager.h"
18 : : #include "options/bv_options.h"
19 : : #include "smt/env.h"
20 : : #include "theory/bv/theory_bv.h"
21 : : #include "theory/bv/theory_bv_utils.h"
22 : :
23 : : namespace cvc5::internal {
24 : : namespace theory {
25 : : namespace bv {
26 : : namespace abstract {
27 : :
28 : 44 : AbstractionModule::AbstractionModule(Env& env, TheoryBV* bv)
29 : : : EnvObj(env),
30 : 44 : d_bv(bv),
31 : 88 : d_absSize(options().bv.bvAbstractionSize),
32 : 44 : d_valLimiter(options().bv.bvAbstractionValueLimiter),
33 : 44 : d_lemmas(nodeManager()),
34 : 88 : d_stats(statisticsRegistry())
35 : : {
36 : 44 : }
37 : :
38 : 44 : AbstractionModule::Statistics::Statistics(StatisticsRegistry& reg)
39 : : : d_numAbstractions(
40 : 44 : reg.registerInt("theory::bv::abstraction::numAbstractions")),
41 : 44 : d_numChecks(reg.registerInt("theory::bv::abstraction::numChecks")),
42 : : d_numLemmasTier12(
43 : 44 : reg.registerInt("theory::bv::abstraction::numLemmasTier12")),
44 : : d_numLemmasTier3(
45 : 44 : reg.registerInt("theory::bv::abstraction::numLemmasTier3")),
46 : : d_numLemmasTier4(
47 : 44 : reg.registerInt("theory::bv::abstraction::numLemmasTier4"))
48 : : {
49 : 44 : }
50 : :
51 : 17161 : bool AbstractionModule::abstractable(TNode n) const
52 : : {
53 : 17161 : Kind k = n.getKind();
54 [ + + ][ + + ]: 17161 : if (k != Kind::BITVECTOR_MULT && k != Kind::BITVECTOR_UDIV
55 [ + + ]: 16661 : && k != Kind::BITVECTOR_UREM)
56 : : {
57 : 16557 : return false;
58 : : }
59 : : // The lemma schemes are binary; cvc5 allows n-ary BITVECTOR_MULT.
60 [ - + ]: 604 : if (n.getNumChildren() != 2)
61 : : {
62 : 0 : return false;
63 : : }
64 : 604 : return utils::getSize(n) >= d_absSize;
65 : : }
66 : :
67 : 36 : Node AbstractionModule::abstractNode(TNode node)
68 : : {
69 [ - + ][ - + ]: 36 : Assert(abstractable(node));
[ - - ]
70 : 36 : auto it = d_cache.find(node);
71 : : // If the cached node is different from `node`, it must be an abstraction
72 : : // constant. Hence, we don't have to check for d_abs2node.find(it->second).
73 [ + + ][ - + ]: 36 : if (it != d_cache.end() && !it->second.isNull() && it->second != node)
[ - - ][ - + ]
74 : : {
75 : 0 : return it->second;
76 : : }
77 : : // A fresh, opaque constant of the same sort. It is deliberately *not* a
78 : : // purification skolem: the abstraction must stay an unconstrained
79 : : // over-approximation, never silently re-expanded to `op` during rewriting
80 : : // or model construction.
81 : 72 : Node t = NodeManager::mkDummySkolem("bvabs", node.getType());
82 : 36 : d_abs2node.emplace(t, node);
83 : : // Note: We do not insert into d_cache here: the caller writes the mapping
84 : : // through a live iterator, which an insertion could invalidate (rehash).
85 : 36 : ++d_stats.d_numAbstractions;
86 : 36 : return t;
87 : 36 : }
88 : :
89 : 2887055 : Node AbstractionModule::abstract(TNode fact)
90 : : {
91 : 2887055 : NodeManager* nm = nodeManager();
92 : 11548220 : std::vector<TNode> visit{fact};
93 : : do
94 : : {
95 : 2920228 : TNode cur = visit.back();
96 : 2920228 : auto it = d_cache.find(cur);
97 [ + + ]: 2920228 : if (it == d_cache.end())
98 : : {
99 : : // Do not descend into terms of other theories (e.g., array selects).
100 : : // The bit-blaster treats them as opaque leaves (variables), and they are
101 : : // the terms shared with the other theory. Rebuilding below such a term
102 : : // would create a NEW node (e.g., a select over an abstracted index)
103 : : // distinct from the shared one: the other theory would continue to
104 : : // reason about the original while this solver constrains the copy,
105 : : // silently disconnecting the two (unsound under theory combination).
106 : 17072 : theory::TheoryId tid = d_env.theoryOf(cur);
107 [ + + ]: 33113 : if (cur.getNumChildren() > 0 && tid != theory::THEORY_BV
108 [ + + ][ + + ]: 33113 : && tid != theory::THEORY_BOOL)
[ + + ]
109 : : {
110 : 5043 : d_cache.emplace(cur, cur);
111 : 5043 : visit.pop_back();
112 : 5043 : continue;
113 : : }
114 : 12029 : d_cache.emplace(cur, Node::null());
115 : 12029 : visit.insert(visit.end(), cur.begin(), cur.end());
116 : 12029 : continue;
117 : 12029 : }
118 [ + + ]: 2903156 : if (it->second.isNull())
119 : : {
120 : 12029 : bool rebuild = false;
121 : 12029 : std::vector<Node> children;
122 [ + + ]: 12029 : if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
123 : : {
124 : 196 : children.push_back(cur.getOperator());
125 : : }
126 [ + + ]: 33173 : for (const TNode& child : cur)
127 : : {
128 : 21144 : Node abs = d_cache.at(child);
129 [ - + ][ - + ]: 21144 : Assert(!abs.isNull());
[ - - ]
130 [ + + ][ + + ]: 21144 : rebuild = rebuild || abs != child;
131 : 21144 : children.push_back(abs);
132 : 21144 : }
133 [ + + ]: 12029 : Node ret = rebuild ? nm->mkNode(cur.getKind(), children) : Node(cur);
134 [ + + ]: 12029 : if (abstractable(ret))
135 : : {
136 : 36 : ret = abstractNode(ret);
137 : : }
138 : 12029 : it->second = rewrite(ret);
139 : 12029 : }
140 : 2903156 : visit.pop_back();
141 [ + + ][ + + ]: 5840456 : } while (!visit.empty());
142 : 8661165 : return d_cache.at(fact);
143 : 2887055 : }
144 : :
145 : 334 : void AbstractionModule::check(std::vector<Node>& lemmas)
146 : : {
147 : 334 : ++d_stats.d_numChecks;
148 : 334 : NodeManager* nm = nodeManager();
149 : 334 : Node falseNode = nm->mkConst(false);
150 : 334 : std::vector<Node> args(3);
151 : 334 : std::vector<Node> vals(3);
152 [ + + ]: 721 : for (const auto& [t, n] : d_abs2node)
153 : : {
154 [ - + ][ - + ]: 387 : Assert(abstractable(n));
[ - - ]
155 : 387 : Kind kind = n.getKind();
156 : 387 : TNode x = n[0];
157 : 387 : TNode s = n[1];
158 : 387 : Node xval = d_bv->getValue(x);
159 : 387 : Node sval = d_bv->getValue(s);
160 : 387 : Node tval = d_bv->getValue(t);
161 [ + - ][ + - ]: 387 : Assert(xval.isConst() && sval.isConst() && tval.isConst());
[ + - ][ + - ]
[ - + ][ - + ]
[ - - ]
162 : :
163 : : // The abstraction `t = op(x, s)` is consistent with the model iff the
164 : : // actual operator applied to the operand values equals the value of `t`.
165 : : // If so, there is nothing to refine for this node.
166 : 774 : Node value = rewrite(nm->mkNode(kind, xval, sval));
167 [ + + ]: 387 : if (value == tval)
168 : : {
169 : 151 : continue;
170 : : }
171 : :
172 : : // Tier 1/2: add the FIRST Table-2 lemma scheme (in registry order, which
173 : : // follows Bitwuzla's) that is violated under the current model, i.e.,
174 : : // whose instantiation constant-folds to false when x, s, t are substituted
175 : : // by their model values. Only one lemma is added per term per refinement
176 : : // round (as in Bitwuzla), so the SAT solver is not swamped with all
177 : : // violated schemes at once.
178 : : //
179 : : // Note: We do not use the Evaluator here since it only substitutes
180 : : // *variable* keys (it matches `args` entries only for nodes with
181 : : // isVar()) and leaves a compound key unsubstituted (thus would
182 : : // evaluate to a non-constant, and so miss the violation).
183 [ + + ][ - - ]: 944 : args = {x, s, t};
184 [ + + ][ - - ]: 944 : vals = {xval, sval, tval};
185 : 236 : bool violated = false;
186 [ + + ]: 1724 : for (const std::unique_ptr<AbstractionLemma>& lemma : d_lemmas.lemmas(kind))
187 : : {
188 : 3320 : Node inst = lemma->instance(x, s, t);
189 [ + + ]: 1660 : if (inst.isNull())
190 : : {
191 : 315 : inst = lemma->instance(x, s, t, xval, sval);
192 : : }
193 [ + + ]: 1660 : if (inst.isNull())
194 : : {
195 : : // Value lemma not applicable under the current model values (e.g. the
196 : : // POW2 schemes when the value is not a power of two).
197 : 180 : continue;
198 : : }
199 : : Node subst =
200 : 1480 : inst.substitute(args.begin(), args.end(), vals.begin(), vals.end());
201 [ + + ]: 1480 : if (rewrite(subst) == falseNode)
202 : : {
203 : 172 : lemmas.push_back(inst);
204 : 172 : violated = true;
205 : 172 : break;
206 : : }
207 [ + + ][ + + ]: 1832 : }
[ + ]
208 : : // If a Table-2 lemma ruled out this spurious model, move on.
209 [ + + ]: 236 : if (violated)
210 : : {
211 : 172 : ++d_stats.d_numLemmasTier12;
212 : 172 : continue;
213 : : }
214 : :
215 : : // No tier-1/2 lemma violated, fall back to value instantiation if we have
216 : : // not exhausted the instantiation budget for this term yet.
217 : 64 : uint64_t budget = utils::getSize(t) / d_valLimiter;
218 [ + + ]: 64 : if (d_valueInstCount[t] < budget)
219 : : {
220 : : // Tier 3: value instantiation.
221 : 48 : lemmas.push_back(
222 [ + + ][ - - ]: 240 : nm->mkNode(Kind::IMPLIES,
223 [ + + ][ - - ]: 192 : {nm->mkNode(Kind::AND, {x.eqNode(xval), s.eqNode(sval)}),
224 : 96 : t.eqNode(value)}));
225 : 48 : ++d_valueInstCount[t];
226 : 48 : ++d_stats.d_numLemmasTier3;
227 : : }
228 : : else
229 : : {
230 : : // Tier 4: bit-blasting fallback. Assert t = op(x, s), forcing the real
231 : : // circuit to be bit-blasted; `t` is fully constrained from now on.
232 : 16 : lemmas.push_back(t.eqNode(nm->mkNode(kind, x, s)));
233 : 16 : ++d_stats.d_numLemmasTier4;
234 : : }
235 [ + + ][ + + ]: 2002 : }
[ + + ][ + + ]
[ + + ][ + + ]
236 : 334 : }
237 : :
238 : : #ifdef CVC5_ASSERTIONS
239 : 110 : bool AbstractionModule::isModelConsistent()
240 : : {
241 : 110 : NodeManager* nm = nodeManager();
242 [ + + ]: 207 : for (const auto& [t, n] : d_abs2node)
243 : : {
244 [ - + ][ - + ]: 97 : Assert(abstractable(n));
[ - - ]
245 : 194 : Node xval = d_bv->getValue(n[0]);
246 : 194 : Node sval = d_bv->getValue(n[1]);
247 : 97 : Node tval = d_bv->getValue(t);
248 [ + - ][ + - ]: 97 : if (!xval.isConst() || !sval.isConst() || !tval.isConst())
[ - + ][ - + ]
249 : : {
250 : 0 : continue;
251 : : }
252 [ - + ]: 97 : if (rewrite(nm->mkNode(n.getKind(), xval, sval)) != tval)
253 : : {
254 : 0 : return false;
255 : : }
256 [ + - ][ - + ]: 97 : }
[ - - ][ + - ]
[ - ]
257 : 110 : return true;
258 : : }
259 : : #endif
260 : :
261 : 74 : bool AbstractionModule::isAbstracted(TNode node) const
262 : : {
263 : 74 : auto it = d_cache.find(node);
264 : : // Note: The cache also holds null visit markers (while abstract() runs) and
265 : : // rebuilt terms for nodes above an abstracted subterm. Hence, we also
266 : : // have to check if there exists a mapping in d_abs2node.
267 [ + - ][ + - ]: 138 : return it != d_cache.end() && !it->second.isNull() && it->second != node
268 [ + + ][ + - ]: 138 : && d_abs2node.find(it->second) != d_abs2node.end();
269 : : }
270 : :
271 : 32 : TNode AbstractionModule::getAbstraction(TNode node) const
272 : : {
273 [ - + ][ - + ]: 32 : Assert(isAbstracted(node));
[ - - ]
274 : 64 : return d_cache.at(node);
275 : : }
276 : :
277 : : } // namespace abstract
278 : : } // namespace bv
279 : : } // namespace theory
280 : : } // namespace cvc5::internal
|
