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 : : * Inverse rules for bit-vector operators.
11 : : */
12 : :
13 : : #include "theory/quantifiers/bv_inverter.h"
14 : :
15 : : #include <algorithm>
16 : :
17 : : #include "expr/skolem_manager.h"
18 : : #include "options/quantifiers_options.h"
19 : : #include "theory/bv/theory_bv_utils.h"
20 : : #include "theory/quantifiers/bv_inverter_utils.h"
21 : : #include "theory/quantifiers/term_util.h"
22 : : #include "theory/rewriter.h"
23 : : #include "util/bitvector.h"
24 : :
25 : : using namespace cvc5::internal::kind;
26 : :
27 : : namespace cvc5::internal {
28 : : namespace theory {
29 : : namespace quantifiers {
30 : :
31 : 55686 : BvInverter::BvInverter(Rewriter* r) : d_rewriter(r) {}
32 : :
33 : : /*---------------------------------------------------------------------------*/
34 : :
35 : 15305 : Node BvInverter::getSolveVariable(TypeNode tn)
36 : : {
37 : 15305 : std::map<TypeNode, Node>::iterator its = d_solve_var.find(tn);
38 [ + + ]: 15305 : if (its == d_solve_var.end())
39 : : {
40 : 5274 : Node k = NodeManager::mkDummySkolem("slv", tn);
41 : 2637 : d_solve_var[tn] = k;
42 : 2637 : return k;
43 : 2637 : }
44 : 12668 : return its->second;
45 : : }
46 : :
47 : : /*---------------------------------------------------------------------------*/
48 : :
49 : 1967 : Node BvInverter::getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m)
50 : : {
51 : 3934 : TNode solve_var = getSolveVariable(tn);
52 : :
53 : : // condition should be rewritten
54 : 1967 : Node new_cond = cond;
55 [ + + ]: 1967 : if (d_rewriter != nullptr)
56 : : {
57 : 813 : new_cond = d_rewriter->rewrite(cond);
58 [ + - ]: 813 : if (new_cond != cond)
59 : : {
60 [ + - ]: 1626 : Trace("cegqi-bv-skvinv-debug")
61 : 0 : << "Condition " << cond << " was rewritten to " << new_cond
62 : 813 : << std::endl;
63 : : }
64 : : }
65 : : // optimization : if condition is ( x = solve_var ) should just return
66 : : // solve_var and not introduce a Skolem this can happen when we ask for
67 : : // the multiplicative inversion with bv1
68 : 1967 : Node c;
69 [ + + ]: 1967 : if (new_cond.getKind() == Kind::EQUAL)
70 : : {
71 [ + + ]: 21 : for (unsigned i = 0; i < 2; i++)
72 : : {
73 [ - + ]: 14 : if (new_cond[i] == solve_var)
74 : : {
75 : 0 : c = new_cond[1 - i];
76 [ - - ]: 0 : Trace("cegqi-bv-skvinv")
77 : 0 : << "SKVINV : " << c << " is trivially associated with conditon "
78 : 0 : << new_cond << std::endl;
79 : 0 : break;
80 : : }
81 : : }
82 : : }
83 : :
84 [ + - ]: 1967 : if (c.isNull())
85 : : {
86 [ + + ]: 1967 : if (m)
87 : : {
88 : 813 : Node x = m->getBoundVariable(tn);
89 : 1626 : Node ccond = new_cond.substitute(solve_var, x);
90 : 2439 : c = NodeManager::mkNode(
91 : 2439 : Kind::WITNESS, NodeManager::mkNode(Kind::BOUND_VAR_LIST, x), ccond);
92 [ + - ]: 1626 : Trace("cegqi-bv-skvinv")
93 : 813 : << "SKVINV : Make " << c << " for " << new_cond << std::endl;
94 : 813 : }
95 : : else
96 : : {
97 [ + - ]: 2308 : Trace("bv-invert") << "...fail for " << cond << " : no inverter query!"
98 : 1154 : << std::endl;
99 : : }
100 : : }
101 : : // currently shouldn't cache since
102 : : // the return value depends on the
103 : : // state of m (which bound variable is returned).
104 : 3934 : return c;
105 : 1967 : }
106 : :
107 : : /*---------------------------------------------------------------------------*/
108 : :
109 : 194667 : static bool isInvertible(Kind k)
110 : : {
111 [ + + ][ + + ]: 194607 : return k == Kind::NOT || k == Kind::EQUAL || k == Kind::BITVECTOR_ULT
112 [ + - ][ + + ]: 115672 : || k == Kind::BITVECTOR_SLT || k == Kind::BITVECTOR_COMP
113 [ + + ][ + + ]: 114098 : || k == Kind::BITVECTOR_NOT || k == Kind::BITVECTOR_NEG
114 [ + + ][ + + ]: 113510 : || k == Kind::BITVECTOR_CONCAT || k == Kind::BITVECTOR_SIGN_EXTEND
115 [ + + ][ + + ]: 111185 : || k == Kind::BITVECTOR_ADD || k == Kind::BITVECTOR_MULT
116 [ + + ][ + + ]: 106599 : || k == Kind::BITVECTOR_UREM || k == Kind::BITVECTOR_UDIV
117 [ + + ][ + + ]: 105995 : || k == Kind::BITVECTOR_AND || k == Kind::BITVECTOR_OR
118 [ + + ][ + + ]: 104027 : || k == Kind::BITVECTOR_XOR || k == Kind::BITVECTOR_LSHR
119 [ + + ][ + + ]: 389274 : || k == Kind::BITVECTOR_ASHR || k == Kind::BITVECTOR_SHL;
[ + + ]
120 : : }
121 : :
122 : 132346 : Node BvInverter::getPathToPv(Node lit,
123 : : Node pv,
124 : : Node sv,
125 : : std::vector<uint32_t>& path,
126 : : std::unordered_set<TNode>& visited)
127 : : {
128 [ + + ]: 132346 : if (visited.find(lit) == visited.end())
129 : : {
130 : 131630 : visited.insert(lit);
131 [ + + ]: 131630 : if (lit == pv)
132 : : {
133 : 6175 : return sv;
134 : : }
135 : : else
136 : : {
137 : 125455 : unsigned rmod = 0; // TODO : randomize?
138 [ + + ]: 307652 : for (size_t i = 0, num = lit.getNumChildren(); i < num; i++)
139 : : {
140 : 194667 : size_t ii = (i + rmod) % lit.getNumChildren();
141 : : // only recurse if the kind is invertible
142 : : // this allows us to avoid paths that go through skolem functions
143 [ + + ]: 194667 : if (!isInvertible(lit.getKind()))
144 : : {
145 : 102494 : continue;
146 : : }
147 : 184346 : Node litc = getPathToPv(lit[ii], pv, sv, path, visited);
148 [ + + ]: 92173 : if (!litc.isNull())
149 : : {
150 : : // path is outermost term index last
151 : 12470 : path.push_back(ii);
152 : 12470 : std::vector<Node> children;
153 [ + + ]: 12470 : if (lit.getMetaKind() == kind::metakind::PARAMETERIZED)
154 : : {
155 : 56 : children.push_back(lit.getOperator());
156 : : }
157 [ + + ]: 37368 : for (size_t j = 0, num2 = lit.getNumChildren(); j < num2; j++)
158 : : {
159 [ + + ]: 24898 : children.push_back(j == ii ? litc : lit[j]);
160 : : }
161 : 12470 : return lit.getNodeManager()->mkNode(lit.getKind(), children);
162 : 12470 : }
163 [ + + ]: 92173 : }
164 : : }
165 : : }
166 : 113701 : return Node::null();
167 : : }
168 : :
169 : 40173 : Node BvInverter::getPathToPv(Node lit,
170 : : Node pv,
171 : : Node sv,
172 : : Node pvs,
173 : : std::vector<uint32_t>& path,
174 : : bool projectNl)
175 : : {
176 : 40173 : std::unordered_set<TNode> visited;
177 : 80346 : Node slit = getPathToPv(lit, pv, sv, path, visited);
178 : : // if we are able to find a (invertible) path to pv
179 [ + + ][ + + ]: 40173 : if (!slit.isNull() && !pvs.isNull())
[ + + ]
180 : : {
181 : : // substitute pvs for the other occurrences of pv
182 : 4106 : TNode tpv = pv;
183 : 4106 : TNode tpvs = pvs;
184 : 4106 : Node prev_lit = slit;
185 : 4106 : slit = slit.substitute(tpv, tpvs);
186 [ + - ][ + + ]: 4106 : if (!projectNl && slit != prev_lit)
[ + + ]
187 : : {
188 : : // found another occurrence of pv that was not on the solve path,
189 : : // hence lit is non-linear wrt pv and we return null.
190 : 178 : return Node::null();
191 : : }
192 [ + + ][ + + ]: 4462 : }
[ + + ]
193 : 39995 : return slit;
194 : 40173 : }
195 : :
196 : : /*---------------------------------------------------------------------------*/
197 : :
198 : : /* Drop child at given index from expression.
199 : : * E.g., dropChild((x + y + z), 1) -> (x + z) */
200 : 5632 : static Node dropChild(Node n, unsigned index)
201 : : {
202 : 5632 : unsigned nchildren = n.getNumChildren();
203 [ - + ][ - + ]: 5632 : Assert(nchildren > 0);
[ - - ]
204 [ - + ][ - + ]: 5632 : Assert(index < nchildren);
[ - - ]
205 : :
206 [ + + ]: 5632 : if (nchildren < 2) return Node::null();
207 : :
208 : 5382 : Kind k = n.getKind();
209 : 5382 : NodeBuilder nb(n.getNodeManager(), k);
210 [ + + ]: 16338 : for (unsigned i = 0; i < nchildren; ++i)
211 : : {
212 [ + + ]: 10956 : if (i == index) continue;
213 : 5574 : nb << n[i];
214 : : }
215 [ - + ][ - + ]: 5382 : Assert(nb.getNumChildren() > 0);
[ - - ]
216 [ + + ]: 5382 : return nb.getNumChildren() == 1 ? nb[0] : nb.constructNode();
217 : 5382 : }
218 : :
219 : 5991 : Node BvInverter::solveBvLit(Node sv,
220 : : Node lit,
221 : : std::vector<uint32_t>& path,
222 : : BvInverterQuery* m)
223 : : {
224 [ - + ][ - + ]: 5991 : Assert(!path.empty());
[ - - ]
225 : :
226 : 5991 : bool pol = true;
227 : : uint32_t index;
228 : : Kind k, litk;
229 : :
230 [ - + ][ - + ]: 5991 : Assert(!path.empty());
[ - - ]
231 : 5991 : index = path.back();
232 [ - + ][ - + ]: 5991 : Assert(index < lit.getNumChildren());
[ - - ]
233 : 5991 : path.pop_back();
234 : 5991 : litk = k = lit.getKind();
235 : :
236 : 5991 : NodeManager* nm = lit.getNodeManager();
237 : :
238 : : /* Note: option --bool-to-bv is currently disabled when CBQI BV
239 : : * is enabled and the logic is quantified.
240 : : * We currently do not support Boolean operators
241 : : * that are interpreted as bit-vector operators of width 1. */
242 : :
243 : : /* Boolean layer ----------------------------------------------- */
244 : :
245 [ + + ]: 5991 : if (k == Kind::NOT)
246 : : {
247 : 60 : pol = !pol;
248 : 60 : lit = lit[index];
249 [ - + ][ - + ]: 60 : Assert(!path.empty());
[ - - ]
250 : 60 : index = path.back();
251 [ - + ][ - + ]: 60 : Assert(index < lit.getNumChildren());
[ - - ]
252 : 60 : path.pop_back();
253 : 60 : litk = k = lit.getKind();
254 : : }
255 : :
256 [ + + ][ + - ]: 5991 : Assert(k == Kind::EQUAL || k == Kind::BITVECTOR_ULT
[ - + ][ - - ]
[ - + ][ - + ]
[ - - ]
257 : : || k == Kind::BITVECTOR_SLT);
258 : :
259 : 5991 : Node sv_t = lit[index];
260 : 5991 : Node t = lit[1 - index];
261 [ + + ][ + - ]: 5991 : if (litk == Kind::BITVECTOR_ULT && index == 1)
262 : : {
263 : 2 : litk = Kind::BITVECTOR_UGT;
264 : : }
265 [ - + ][ - - ]: 5989 : else if (litk == Kind::BITVECTOR_SLT && index == 1)
266 : : {
267 : 0 : litk = Kind::BITVECTOR_SGT;
268 : : }
269 : :
270 : : /* Bit-vector layer -------------------------------------------- */
271 : :
272 [ + + ]: 8903 : while (!path.empty())
273 : : {
274 : 5632 : unsigned nchildren = sv_t.getNumChildren();
275 [ - + ][ - + ]: 5632 : Assert(nchildren > 0);
[ - - ]
276 : 5632 : index = path.back();
277 [ - + ][ - + ]: 5632 : Assert(index < nchildren);
[ - - ]
278 : 5632 : path.pop_back();
279 : 5632 : k = sv_t.getKind();
280 : :
281 : : /* Note: All n-ary kinds except for CONCAT (i.e., BITVECTOR_AND,
282 : : * BITVECTOR_OR, MULT, ADD) are commutative (no case split
283 : : * based on index). */
284 : 5632 : Node s = dropChild(sv_t, index);
285 [ + + ][ + - ]: 5632 : Assert((nchildren == 1 && s.isNull()) || (nchildren > 1 && !s.isNull()));
[ + + ][ + - ]
[ + - ][ + - ]
[ - + ][ - + ]
[ - - ]
286 : 5632 : TypeNode solve_tn = sv_t[index].getType();
287 : 5632 : Node x = getSolveVariable(solve_tn);
288 : 5632 : Node ic;
289 : :
290 [ + - ]: 5632 : if (litk == Kind::EQUAL
291 [ + + ][ + + ]: 5632 : && (k == Kind::BITVECTOR_NOT || k == Kind::BITVECTOR_NEG))
292 : : {
293 : 194 : t = NodeManager::mkNode(k, t);
294 : : }
295 [ + - ][ + + ]: 5438 : else if (litk == Kind::EQUAL && k == Kind::BITVECTOR_ADD)
296 : : {
297 : 1139 : t = NodeManager::mkNode(Kind::BITVECTOR_SUB, t, s);
298 : : }
299 [ + - ][ + + ]: 4299 : else if (litk == Kind::EQUAL && k == Kind::BITVECTOR_XOR)
300 : : {
301 : 211 : t = NodeManager::mkNode(Kind::BITVECTOR_XOR, t, s);
302 : : }
303 [ + + ][ + + ]: 4088 : else if (litk == Kind::EQUAL && k == Kind::BITVECTOR_MULT && s.isConst()
304 [ + - ][ + + ]: 8176 : && bv::utils::getBit(s, 0))
[ + + ][ + + ]
[ - - ]
305 : : {
306 : 257 : unsigned w = bv::utils::getSize(s);
307 : 257 : Integer s_val = s.getConst<BitVector>().toInteger();
308 : 257 : Integer mod_val = Integer(1).multiplyByPow2(w);
309 [ + - ]: 514 : Trace("bv-invert-debug")
310 : 257 : << "Compute inverse : " << s_val << " " << mod_val << std::endl;
311 : 257 : Integer inv_val = s_val.modInverse(mod_val);
312 [ + - ]: 257 : Trace("bv-invert-debug") << "Inverse : " << inv_val << std::endl;
313 : 257 : Node inv = bv::utils::mkConst(nm, w, inv_val);
314 : 257 : t = NodeManager::mkNode(Kind::BITVECTOR_MULT, inv, t);
315 : 257 : }
316 [ + + ]: 3831 : else if (k == Kind::BITVECTOR_MULT)
317 : : {
318 : 270 : ic = utils::getICBvMult(pol, litk, k, index, x, s, t);
319 : : }
320 [ + + ]: 3561 : else if (k == Kind::BITVECTOR_SHL)
321 : : {
322 : 238 : ic = utils::getICBvShl(pol, litk, k, index, x, s, t);
323 : : }
324 [ + + ]: 3323 : else if (k == Kind::BITVECTOR_UREM)
325 : : {
326 : 201 : ic = utils::getICBvUrem(pol, litk, k, index, x, s, t);
327 : : }
328 [ + + ]: 3122 : else if (k == Kind::BITVECTOR_UDIV)
329 : : {
330 : 193 : ic = utils::getICBvUdiv(pol, litk, k, index, x, s, t);
331 : : }
332 [ + + ][ + + ]: 2929 : else if (k == Kind::BITVECTOR_AND || k == Kind::BITVECTOR_OR)
333 : : {
334 : 554 : ic = utils::getICBvAndOr(pol, litk, k, index, x, s, t);
335 : : }
336 [ + + ]: 2375 : else if (k == Kind::BITVECTOR_LSHR)
337 : : {
338 : 214 : ic = utils::getICBvLshr(pol, litk, k, index, x, s, t);
339 : : }
340 [ + + ]: 2161 : else if (k == Kind::BITVECTOR_ASHR)
341 : : {
342 : 218 : ic = utils::getICBvAshr(pol, litk, k, index, x, s, t);
343 : : }
344 [ + + ]: 1943 : else if (k == Kind::BITVECTOR_CONCAT)
345 : : {
346 [ + - ]: 321 : if (litk == Kind::EQUAL)
347 : : {
348 : : /* Compute inverse for s1 o x, x o s2, s1 o x o s2
349 : : * (while disregarding that invertibility depends on si)
350 : : * rather than an invertibility condition (the proper handling).
351 : : * This improves performance on a considerable number of benchmarks.
352 : : *
353 : : * x = t[upper:lower]
354 : : * where
355 : : * upper = getSize(t) - 1 - sum(getSize(sv_t[i])) for i < index
356 : : * lower = getSize(sv_t[i]) for i > index */
357 : : unsigned upper, lower;
358 : 321 : upper = bv::utils::getSize(t) - 1;
359 : 321 : lower = 0;
360 : 321 : NodeBuilder nb(nm, Kind::BITVECTOR_CONCAT);
361 [ + + ]: 1016 : for (unsigned i = 0; i < nchildren; i++)
362 : : {
363 [ + + ]: 695 : if (i < index)
364 : : {
365 : 105 : upper -= bv::utils::getSize(sv_t[i]);
366 : : }
367 [ + + ]: 590 : else if (i > index)
368 : : {
369 : 269 : lower += bv::utils::getSize(sv_t[i]);
370 : : }
371 : : }
372 : 321 : t = bv::utils::mkExtract(t, upper, lower);
373 : 321 : }
374 : : else
375 : : {
376 : 0 : ic = utils::getICBvConcat(pol, litk, index, x, sv_t, t);
377 : : }
378 : : }
379 [ + + ]: 1622 : else if (k == Kind::BITVECTOR_SIGN_EXTEND)
380 : : {
381 : 56 : ic = utils::getICBvSext(pol, litk, index, x, sv_t, t);
382 : : }
383 [ + - ][ - + ]: 1566 : else if (litk == Kind::BITVECTOR_ULT || litk == Kind::BITVECTOR_UGT)
384 : : {
385 : 0 : ic = utils::getICBvUltUgt(pol, litk, x, t);
386 : : }
387 [ + - ][ - + ]: 1566 : else if (litk == Kind::BITVECTOR_SLT || litk == Kind::BITVECTOR_SGT)
388 : : {
389 : 0 : ic = utils::getICBvSltSgt(pol, litk, x, t);
390 : : }
391 [ - + ]: 1566 : else if (pol == false)
392 : : {
393 : 0 : Assert(litk == Kind::EQUAL);
394 : 0 : ic = NodeManager::mkNode(Kind::DISTINCT, x, t);
395 [ - - ]: 0 : Trace("bv-invert") << "Add SC_" << litk << "(" << x << "): " << ic
396 : 0 : << std::endl;
397 : : }
398 : : else
399 : : {
400 [ + - ]: 3132 : Trace("bv-invert") << "bv-invert : Unknown kind " << k
401 : 1566 : << " for bit-vector term " << sv_t << std::endl;
402 : 1566 : return Node::null();
403 : : }
404 : :
405 [ + + ]: 4066 : if (!ic.isNull())
406 : : {
407 : : /* We generate a witness term (witness x0. ic => x0 <k> s <litk> t) for
408 : : * x <k> s <litk> t. When traversing down, this witness term determines
409 : : * the value for x <k> s = (witness x0. ic => x0 <k> s <litk> t), i.e.,
410 : : * from here on, the propagated literal is a positive equality. */
411 : 1944 : litk = Kind::EQUAL;
412 : 1944 : pol = true;
413 : : /* t = fresh skolem constant */
414 : 1944 : t = getInversionNode(ic, solve_tn, m);
415 [ + + ]: 1944 : if (t.isNull())
416 : : {
417 : 1154 : return t;
418 : : }
419 : : }
420 : :
421 : 2912 : sv_t = sv_t[index];
422 [ + + ][ + + ]: 13792 : }
[ + + ][ + + ]
423 : :
424 : : /* Base case */
425 [ - + ][ - + ]: 3271 : Assert(sv_t == sv);
[ - - ]
426 : 3271 : TypeNode solve_tn = sv.getType();
427 : 3271 : Node x = getSolveVariable(solve_tn);
428 : 3271 : Node ic;
429 [ + - ][ + + ]: 3271 : if (litk == Kind::BITVECTOR_ULT || litk == Kind::BITVECTOR_UGT)
430 : : {
431 : 2 : ic = utils::getICBvUltUgt(pol, litk, x, t);
432 : : }
433 [ + - ][ - + ]: 3269 : else if (litk == Kind::BITVECTOR_SLT || litk == Kind::BITVECTOR_SGT)
434 : : {
435 : 0 : ic = utils::getICBvSltSgt(pol, litk, x, t);
436 : : }
437 [ + + ]: 3269 : else if (pol == false)
438 : : {
439 [ - + ][ - + ]: 21 : Assert(litk == Kind::EQUAL);
[ - - ]
440 : 21 : ic = NodeManager::mkNode(Kind::DISTINCT, x, t);
441 [ + - ]: 42 : Trace("bv-invert") << "Add SC_" << litk << "(" << x << "): " << ic
442 : 21 : << std::endl;
443 : : }
444 : :
445 : 3271 : return ic.isNull() ? t : getInversionNode(ic, solve_tn, m);
446 : 5991 : }
447 : :
448 : : /*---------------------------------------------------------------------------*/
449 : :
450 : : } // namespace quantifiers
451 : : } // namespace theory
452 : : } // namespace cvc5::internal
|
