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