Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Aina Niemetz, Mathias Preiner, Daniel Larraz
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 : : * Inverse rules for bit-vector operators.
14 : : */
15 : :
16 : : #include "theory/quantifiers/bv_inverter_utils.h"
17 : : #include "theory/bv/theory_bv_utils.h"
18 : :
19 : : using namespace cvc5::internal::kind;
20 : :
21 : : namespace cvc5::internal {
22 : : namespace theory {
23 : : namespace quantifiers {
24 : : namespace utils {
25 : :
26 : 37 : Node getICBvUltUgt(bool pol, Kind k, Node x, Node t)
27 : : {
28 [ + + ][ - + ]: 37 : Assert(k == Kind::BITVECTOR_ULT || k == Kind::BITVECTOR_UGT);
[ - + ][ - - ]
29 : :
30 : 37 : unsigned w = bv::utils::getSize(t);
31 : 37 : Node ic;
32 : :
33 [ + + ]: 37 : if (k == Kind::BITVECTOR_ULT)
34 : : {
35 [ + + ]: 21 : if (pol == true)
36 : : {
37 : : /* x < t
38 : : * with invertibility condition:
39 : : * (distinct t z)
40 : : * where
41 : : * z = 0 with getSize(z) = w */
42 : 42 : Node scl = NodeManager::mkNode(Kind::DISTINCT, t, bv::utils::mkZero(w));
43 : 28 : Node scr = NodeManager::mkNode(k, x, t);
44 : 14 : ic = NodeManager::mkNode(Kind::IMPLIES, scl, scr);
45 : : }
46 : : else
47 : : {
48 : : /* x >= t
49 : : * with invertibility condition:
50 : : * true (no invertibility condition) */
51 : 7 : ic = NodeManager::mkNode(Kind::NOT, NodeManager::mkNode(k, x, t));
52 : : }
53 : : }
54 : : else
55 : : {
56 [ - + ][ - + ]: 16 : Assert(k == Kind::BITVECTOR_UGT);
[ - - ]
57 [ + + ]: 16 : if (pol == true)
58 : : {
59 : : /* x > t
60 : : * with invertibility condition:
61 : : * (distinct t ones)
62 : : * where
63 : : * ones = ~0 with getSize(ones) = w */
64 : 27 : Node scl = NodeManager::mkNode(Kind::DISTINCT, t, bv::utils::mkOnes(w));
65 : 18 : Node scr = NodeManager::mkNode(k, x, t);
66 : 9 : ic = NodeManager::mkNode(Kind::IMPLIES, scl, scr);
67 : : }
68 : : else
69 : : {
70 : : /* x <= t
71 : : * with invertibility condition:
72 : : * true (no invertibility condition) */
73 : 7 : ic = NodeManager::mkNode(Kind::NOT, NodeManager::mkNode(k, x, t));
74 : : }
75 : : }
76 [ + - ]: 37 : Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << ic << std::endl;
77 : 37 : return ic;
78 : : }
79 : :
80 : 28 : Node getICBvSltSgt(bool pol, Kind k, Node x, Node t)
81 : : {
82 [ + + ][ - + ]: 28 : Assert(k == Kind::BITVECTOR_SLT || k == Kind::BITVECTOR_SGT);
[ - + ][ - - ]
83 : :
84 : 28 : unsigned w = bv::utils::getSize(t);
85 : 28 : Node ic;
86 : :
87 [ + + ]: 28 : if (k == Kind::BITVECTOR_SLT)
88 : : {
89 [ + + ]: 14 : if (pol == true)
90 : : {
91 : : /* x < t
92 : : * with invertibility condition:
93 : : * (distinct t min)
94 : : * where
95 : : * min is the minimum signed value with getSize(min) = w */
96 : 14 : Node min = bv::utils::mkMinSigned(w);
97 : 21 : Node scl = NodeManager::mkNode(Kind::DISTINCT, min, t);
98 : 14 : Node scr = NodeManager::mkNode(k, x, t);
99 : 7 : ic = NodeManager::mkNode(Kind::IMPLIES, scl, scr);
100 : : }
101 : : else
102 : : {
103 : : /* x >= t
104 : : * with invertibility condition:
105 : : * true (no invertibility condition) */
106 : 7 : ic = NodeManager::mkNode(Kind::NOT, NodeManager::mkNode(k, x, t));
107 : : }
108 : : }
109 : : else
110 : : {
111 [ - + ][ - + ]: 14 : Assert(k == Kind::BITVECTOR_SGT);
[ - - ]
112 [ + + ]: 14 : if (pol == true)
113 : : {
114 : : /* x > t
115 : : * with invertibility condition:
116 : : * (distinct t max)
117 : : * where
118 : : * max is the signed maximum value with getSize(max) = w */
119 : 14 : Node max = bv::utils::mkMaxSigned(w);
120 : 21 : Node scl = NodeManager::mkNode(Kind::DISTINCT, t, max);
121 : 14 : Node scr = NodeManager::mkNode(k, x, t);
122 : 7 : ic = NodeManager::mkNode(Kind::IMPLIES, scl, scr);
123 : : }
124 : : else
125 : : {
126 : : /* x <= t
127 : : * with invertibility condition:
128 : : * true (no invertibility condition) */
129 : 7 : ic = NodeManager::mkNode(Kind::NOT, NodeManager::mkNode(k, x, t));
130 : : }
131 : : }
132 [ + - ]: 28 : Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << ic << std::endl;
133 : 28 : return ic;
134 : : }
135 : :
136 : 218 : Node getICBvMult(
137 : : bool pol, Kind litk, Kind k, unsigned idx, Node x, Node s, Node t)
138 : : {
139 [ - + ][ - + ]: 218 : Assert(k == Kind::BITVECTOR_MULT);
[ - - ]
140 [ + + ][ + + ]: 218 : Assert(litk == Kind::EQUAL || litk == Kind::BITVECTOR_ULT
[ + + ][ + + ]
[ - + ][ - + ]
[ - - ]
141 : : || litk == Kind::BITVECTOR_SLT || litk == Kind::BITVECTOR_UGT
142 : : || litk == Kind::BITVECTOR_SGT);
143 : :
144 : 218 : NodeManager* nm = NodeManager::currentNM();
145 : 436 : Node scl;
146 : 218 : unsigned w = bv::utils::getSize(s);
147 [ - + ][ - + ]: 218 : Assert(w == bv::utils::getSize(t));
[ - - ]
148 : :
149 [ + + ]: 218 : if (litk == Kind::EQUAL)
150 : : {
151 : 404 : Node z = bv::utils::mkZero(w);
152 : :
153 [ + + ]: 202 : if (pol)
154 : : {
155 : : /* x * s = t
156 : : * with invertibility condition (synthesized):
157 : : * (= (bvand (bvor (bvneg s) s) t) t)
158 : : *
159 : : * is equivalent to:
160 : : * ctz(t) >= ctz(s)
161 : : * ->
162 : : * (or
163 : : * (= t z)
164 : : * (and
165 : : * (bvuge (bvand t (bvneg t)) (bvand s (bvneg s)))
166 : : * (distinct s z)))
167 : : * where
168 : : * z = 0 with getSize(z) = w */
169 : : Node o =
170 : 392 : nm->mkNode(Kind::BITVECTOR_OR, nm->mkNode(Kind::BITVECTOR_NEG, s), s);
171 : 196 : scl = nm->mkNode(Kind::EQUAL, nm->mkNode(Kind::BITVECTOR_AND, o, t), t);
172 : : }
173 : : else
174 : : {
175 : : /* x * s != t
176 : : * with invertibility condition:
177 : : * (or (distinct t z) (distinct s z))
178 : : * where
179 : : * z = 0 with getSize(z) = w */
180 : 6 : scl = nm->mkNode(Kind::OR, t.eqNode(z).notNode(), s.eqNode(z).notNode());
181 : : }
182 : : }
183 [ + + ]: 16 : else if (litk == Kind::BITVECTOR_ULT)
184 : : {
185 [ + + ]: 4 : if (pol)
186 : : {
187 : : /* x * s < t
188 : : * with invertibility condition (synthesized):
189 : : * (distinct t z)
190 : : * where
191 : : * z = 0 with getSize(z) = w */
192 : 2 : Node z = bv::utils::mkZero(w);
193 : 2 : scl = nm->mkNode(Kind::DISTINCT, t, z);
194 : : }
195 : : else
196 : : {
197 : : /* x * s >= t
198 : : * with invertibility condition (synthesized):
199 : : * (bvuge (bvor (bvneg s) s) t) */
200 : : Node o =
201 : 4 : nm->mkNode(Kind::BITVECTOR_OR, nm->mkNode(Kind::BITVECTOR_NEG, s), s);
202 : 2 : scl = nm->mkNode(Kind::BITVECTOR_UGE, o, t);
203 : : }
204 : : }
205 [ + + ]: 12 : else if (litk == Kind::BITVECTOR_UGT)
206 : : {
207 [ + + ]: 4 : if (pol)
208 : : {
209 : : /* x * s > t
210 : : * with invertibility condition (synthesized):
211 : : * (bvult t (bvor (bvneg s) s)) */
212 : : Node o =
213 : 4 : nm->mkNode(Kind::BITVECTOR_OR, nm->mkNode(Kind::BITVECTOR_NEG, s), s);
214 : 2 : scl = nm->mkNode(Kind::BITVECTOR_ULT, t, o);
215 : : }
216 : : else
217 : : {
218 : : /* x * s <= t
219 : : * true (no invertibility condition) */
220 : 2 : scl = nm->mkConst<bool>(true);
221 : : }
222 : : }
223 [ + + ]: 8 : else if (litk == Kind::BITVECTOR_SLT)
224 : : {
225 [ + + ]: 4 : if (pol)
226 : : {
227 : : /* x * s < t
228 : : * with invertibility condition (synthesized):
229 : : * (bvslt (bvand (bvnot (bvneg t)) (bvor (bvneg s) s)) t) */
230 : : Node a1 =
231 : 6 : nm->mkNode(Kind::BITVECTOR_NOT, nm->mkNode(Kind::BITVECTOR_NEG, t));
232 : : Node a2 =
233 : 4 : nm->mkNode(Kind::BITVECTOR_OR, nm->mkNode(Kind::BITVECTOR_NEG, s), s);
234 : 8 : scl = nm->mkNode(
235 : 6 : Kind::BITVECTOR_SLT, nm->mkNode(Kind::BITVECTOR_AND, a1, a2), t);
236 : : }
237 : : else
238 : : {
239 : : /* x * s >= t
240 : : * with invertibility condition (synthesized):
241 : : * (bvsge (bvand (bvor (bvneg s) s) max) t)
242 : : * where
243 : : * max is the signed maximum value with getSize(max) = w */
244 : 4 : Node max = bv::utils::mkMaxSigned(w);
245 : : Node o =
246 : 6 : nm->mkNode(Kind::BITVECTOR_OR, nm->mkNode(Kind::BITVECTOR_NEG, s), s);
247 : 4 : Node a = nm->mkNode(Kind::BITVECTOR_AND, o, max);
248 : 2 : scl = nm->mkNode(Kind::BITVECTOR_SGE, a, t);
249 : : }
250 : : }
251 : : else
252 : : {
253 [ - + ][ - + ]: 4 : Assert(litk == Kind::BITVECTOR_SGT);
[ - - ]
254 [ + + ]: 4 : if (pol)
255 : : {
256 : : /* x * s > t
257 : : * with invertibility condition (synthesized):
258 : : * (bvslt t (bvsub t (bvor (bvor s t) (bvneg s)))) */
259 : : Node o = nm->mkNode(Kind::BITVECTOR_OR,
260 : 4 : nm->mkNode(Kind::BITVECTOR_OR, s, t),
261 : 10 : nm->mkNode(Kind::BITVECTOR_NEG, s));
262 : 4 : Node sub = nm->mkNode(Kind::BITVECTOR_SUB, t, o);
263 : 2 : scl = nm->mkNode(Kind::BITVECTOR_SLT, t, sub);
264 : : }
265 : : else
266 : : {
267 : : /* x * s <= t
268 : : * with invertibility condition (synthesized):
269 : : * (not (and (= s z) (bvslt t s)))
270 : : * where
271 : : * z = 0 with getSize(z) = w */
272 : 2 : Node z = bv::utils::mkZero(w);
273 : 6 : scl = nm->mkNode(
274 : 8 : Kind::AND, s.eqNode(z), nm->mkNode(Kind::BITVECTOR_SLT, t, s));
275 : 2 : scl = scl.notNode();
276 : : }
277 : : }
278 : :
279 : : Node scr =
280 : 1090 : nm->mkNode(litk, idx == 0 ? nm->mkNode(k, x, s) : nm->mkNode(k, s, x), t);
281 [ + + ]: 436 : Node ic = nm->mkNode(Kind::IMPLIES, scl, pol ? scr : scr.notNode());
282 [ + - ]: 218 : Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << ic << std::endl;
283 : 436 : return ic;
284 : : }
285 : :
286 : 115 : Node getICBvUrem(
287 : : bool pol, Kind litk, Kind k, unsigned idx, Node x, Node s, Node t)
288 : : {
289 [ - + ][ - + ]: 115 : Assert(k == Kind::BITVECTOR_UREM);
[ - - ]
290 [ + + ][ + + ]: 115 : Assert(litk == Kind::EQUAL || litk == Kind::BITVECTOR_ULT
[ + + ][ + + ]
[ - + ][ - + ]
[ - - ]
291 : : || litk == Kind::BITVECTOR_SLT || litk == Kind::BITVECTOR_UGT
292 : : || litk == Kind::BITVECTOR_SGT);
293 : :
294 : 115 : NodeManager* nm = NodeManager::currentNM();
295 : 230 : Node scl;
296 : 115 : unsigned w = bv::utils::getSize(s);
297 [ - + ][ - + ]: 115 : Assert(w == bv::utils::getSize(t));
[ - - ]
298 : :
299 [ + + ]: 115 : if (litk == Kind::EQUAL)
300 : : {
301 [ + + ]: 99 : if (idx == 0)
302 : : {
303 [ + + ]: 43 : if (pol)
304 : : {
305 : : /* x % s = t
306 : : * with invertibility condition (synthesized):
307 : : * (bvuge (bvnot (bvneg s)) t) */
308 : 42 : Node neg = nm->mkNode(Kind::BITVECTOR_NEG, s);
309 : 168 : scl = nm->mkNode(
310 : 126 : Kind::BITVECTOR_UGE, nm->mkNode(Kind::BITVECTOR_NOT, neg), t);
311 : : }
312 : : else
313 : : {
314 : : /* x % s != t
315 : : * with invertibility condition:
316 : : * (or (distinct s (_ bv1 w)) (distinct t z))
317 : : * where
318 : : * z = 0 with getSize(z) = w */
319 : 1 : Node z = bv::utils::mkZero(w);
320 : 3 : scl = nm->mkNode(Kind::OR,
321 : 2 : s.eqNode(bv::utils::mkOne(w)).notNode(),
322 : 3 : t.eqNode(z).notNode());
323 : : }
324 : : }
325 : : else
326 : : {
327 [ + + ]: 56 : if (pol)
328 : : {
329 : : /* s % x = t
330 : : * with invertibility condition (synthesized):
331 : : * (bvuge (bvand (bvsub (bvadd t t) s) s) t)
332 : : *
333 : : * is equivalent to:
334 : : * (or (= s t)
335 : : * (and (bvugt s t)
336 : : * (bvugt (bvsub s t) t)
337 : : * (or (= t z) (distinct (bvsub s (_ bv1 w)) t))))
338 : : * where
339 : : * z = 0 with getSize(z) = w */
340 : 159 : Node add = nm->mkNode(Kind::BITVECTOR_ADD, t, t);
341 : 159 : Node sub = nm->mkNode(Kind::BITVECTOR_SUB, add, s);
342 : 106 : Node a = nm->mkNode(Kind::BITVECTOR_AND, sub, s);
343 : 53 : scl = nm->mkNode(Kind::BITVECTOR_UGE, a, t);
344 : : }
345 : : else
346 : : {
347 : : /* s % x != t
348 : : * with invertibility condition:
349 : : * (or (distinct s z) (distinct t z))
350 : : * where
351 : : * z = 0 with getSize(z) = w */
352 : 3 : Node z = bv::utils::mkZero(w);
353 : : scl =
354 : 3 : nm->mkNode(Kind::OR, s.eqNode(z).notNode(), t.eqNode(z).notNode());
355 : : }
356 : : }
357 : : }
358 [ + + ]: 16 : else if (litk == Kind::BITVECTOR_ULT)
359 : : {
360 [ + + ]: 4 : if (idx == 0)
361 : : {
362 [ + + ]: 2 : if (pol)
363 : : {
364 : : /* x % s < t
365 : : * with invertibility condition:
366 : : * (distinct t z)
367 : : * where
368 : : * z = 0 with getSize(z) = w */
369 : 1 : Node z = bv::utils::mkZero(w);
370 : 1 : scl = t.eqNode(z).notNode();
371 : : }
372 : : else
373 : : {
374 : : /* x % s >= t
375 : : * with invertibility condition (synthesized):
376 : : * (bvuge (bvnot (bvneg s)) t) */
377 : 1 : Node neg = nm->mkNode(Kind::BITVECTOR_NEG, s);
378 : 4 : scl = nm->mkNode(
379 : 3 : Kind::BITVECTOR_UGE, nm->mkNode(Kind::BITVECTOR_NOT, neg), t);
380 : : }
381 : : }
382 : : else
383 : : {
384 [ + + ]: 2 : if (pol)
385 : : {
386 : : /* s % x < t
387 : : * with invertibility condition:
388 : : * (distinct t z)
389 : : * where
390 : : * z = 0 with getSize(z) = w */
391 : 1 : Node z = bv::utils::mkZero(w);
392 : 1 : scl = t.eqNode(z).notNode();
393 : : }
394 : : else
395 : : {
396 : : /* s % x >= t
397 : : * with invertibility condition (combination of = and >):
398 : : * (or
399 : : * (bvuge (bvand (bvsub (bvadd t t) s) s) t) ; eq, synthesized
400 : : * (bvult t s)) ; ugt, synthesized */
401 : 3 : Node add = nm->mkNode(Kind::BITVECTOR_ADD, t, t);
402 : 3 : Node sub = nm->mkNode(Kind::BITVECTOR_SUB, add, s);
403 : 3 : Node a = nm->mkNode(Kind::BITVECTOR_AND, sub, s);
404 : 3 : Node sceq = nm->mkNode(Kind::BITVECTOR_UGE, a, t);
405 : 2 : Node scugt = nm->mkNode(Kind::BITVECTOR_ULT, t, s);
406 : 1 : scl = nm->mkNode(Kind::OR, sceq, scugt);
407 : : }
408 : : }
409 : : }
410 [ + + ]: 12 : else if (litk == Kind::BITVECTOR_UGT)
411 : : {
412 [ + + ]: 4 : if (idx == 0)
413 : : {
414 [ + + ]: 2 : if (pol)
415 : : {
416 : : /* x % s > t
417 : : * with invertibility condition (synthesized):
418 : : * (bvult t (bvnot (bvneg s))) */
419 : : Node nt =
420 : 2 : nm->mkNode(Kind::BITVECTOR_NOT, nm->mkNode(Kind::BITVECTOR_NEG, s));
421 : 1 : scl = nm->mkNode(Kind::BITVECTOR_ULT, t, nt);
422 : : }
423 : : else
424 : : {
425 : : /* x % s <= t
426 : : * true (no invertibility condition) */
427 : 1 : scl = nm->mkConst<bool>(true);
428 : : }
429 : : }
430 : : else
431 : : {
432 [ + + ]: 2 : if (pol)
433 : : {
434 : : /* s % x > t
435 : : * with invertibility condition (synthesized):
436 : : * (bvult t s) */
437 : 1 : scl = nm->mkNode(Kind::BITVECTOR_ULT, t, s);
438 : : }
439 : : else
440 : : {
441 : : /* s % x <= t
442 : : * true (no invertibility condition) */
443 : 1 : scl = nm->mkConst<bool>(true);
444 : : }
445 : : }
446 : : }
447 [ + + ]: 8 : else if (litk == Kind::BITVECTOR_SLT)
448 : : {
449 [ + + ]: 4 : if (idx == 0)
450 : : {
451 [ + + ]: 2 : if (pol)
452 : : {
453 : : /* x % s < t
454 : : * with invertibility condition (synthesized):
455 : : * (bvslt (bvnot t) (bvor (bvneg s) (bvneg t))) */
456 : 2 : Node o1 = nm->mkNode(Kind::BITVECTOR_NEG, s);
457 : 2 : Node o2 = nm->mkNode(Kind::BITVECTOR_NEG, t);
458 : 2 : Node o = nm->mkNode(Kind::BITVECTOR_OR, o1, o2);
459 : 4 : scl = nm->mkNode(
460 : 3 : Kind::BITVECTOR_SLT, nm->mkNode(Kind::BITVECTOR_NOT, t), o);
461 : : }
462 : : else
463 : : {
464 : : /* x % s >= t
465 : : * with invertibility condition (synthesized):
466 : : * (or (bvslt t s) (bvsge z s))
467 : : * where
468 : : * z = 0 with getSize(z) = w */
469 : 2 : Node z = bv::utils::mkZero(w);
470 : 3 : Node s1 = nm->mkNode(Kind::BITVECTOR_SLT, t, s);
471 : 2 : Node s2 = nm->mkNode(Kind::BITVECTOR_SGE, z, s);
472 : 1 : scl = nm->mkNode(Kind::OR, s1, s2);
473 : : }
474 : : }
475 : : else
476 : : {
477 : 4 : Node z = bv::utils::mkZero(w);
478 : :
479 [ + + ]: 2 : if (pol)
480 : : {
481 : : /* s % x < t
482 : : * with invertibility condition (synthesized):
483 : : * (or (bvslt s t) (bvslt z t))
484 : : * where
485 : : * z = 0 with getSize(z) = w */
486 : 3 : Node slt1 = nm->mkNode(Kind::BITVECTOR_SLT, s, t);
487 : 2 : Node slt2 = nm->mkNode(Kind::BITVECTOR_SLT, z, t);
488 : 1 : scl = nm->mkNode(Kind::OR, slt1, slt2);
489 : : }
490 : : else
491 : : {
492 : : /* s % x >= t
493 : : * with invertibility condition:
494 : : * (and
495 : : * (=> (bvsge s z) (bvsge s t))
496 : : * (=> (and (bvslt s z) (bvsge t z)) (bvugt (bvsub s t) t)))
497 : : * where
498 : : * z = 0 with getSize(z) = w */
499 : : Node i1 = nm->mkNode(Kind::IMPLIES,
500 : 2 : nm->mkNode(Kind::BITVECTOR_SGE, s, z),
501 : 5 : nm->mkNode(Kind::BITVECTOR_SGE, s, t));
502 : : Node i2 = nm->mkNode(
503 : : Kind::IMPLIES,
504 : 4 : nm->mkNode(Kind::AND,
505 : 2 : nm->mkNode(Kind::BITVECTOR_SLT, s, z),
506 : 2 : nm->mkNode(Kind::BITVECTOR_SGE, t, z)),
507 : 3 : nm->mkNode(
508 : 6 : Kind::BITVECTOR_UGT, nm->mkNode(Kind::BITVECTOR_SUB, s, t), t));
509 : 1 : scl = nm->mkNode(Kind::AND, i1, i2);
510 : : }
511 : : }
512 : : }
513 : : else
514 : : {
515 [ - + ][ - + ]: 4 : Assert(litk == Kind::BITVECTOR_SGT);
[ - - ]
516 [ + + ]: 4 : if (idx == 0)
517 : : {
518 : 4 : Node z = bv::utils::mkZero(w);
519 : :
520 [ + + ]: 2 : if (pol)
521 : : {
522 : : /* x % s > t
523 : : * with invertibility condition:
524 : : *
525 : : * (and
526 : : * (and
527 : : * (=> (bvsgt s z) (bvslt t (bvnot (bvneg s))))
528 : : * (=> (bvsle s z) (distinct t max)))
529 : : * (or (distinct t z) (distinct s (_ bv1 w))))
530 : : * where
531 : : * z = 0 with getSize(z) = w
532 : : * and max is the maximum signed value with getSize(max) = w */
533 : 2 : Node max = bv::utils::mkMaxSigned(w);
534 : : Node nt =
535 : 3 : nm->mkNode(Kind::BITVECTOR_NOT, nm->mkNode(Kind::BITVECTOR_NEG, s));
536 : : Node i1 = nm->mkNode(Kind::IMPLIES,
537 : 2 : nm->mkNode(Kind::BITVECTOR_SGT, s, z),
538 : 5 : nm->mkNode(Kind::BITVECTOR_SLT, t, nt));
539 : : Node i2 = nm->mkNode(Kind::IMPLIES,
540 : 2 : nm->mkNode(Kind::BITVECTOR_SLE, s, z),
541 : 5 : t.eqNode(max).notNode());
542 : 3 : Node a1 = nm->mkNode(Kind::AND, i1, i2);
543 : : Node a2 = nm->mkNode(Kind::OR,
544 : 2 : t.eqNode(z).notNode(),
545 : 4 : s.eqNode(bv::utils::mkOne(w)).notNode());
546 : 1 : scl = nm->mkNode(Kind::AND, a1, a2);
547 : : }
548 : : else
549 : : {
550 : : /* x % s <= t
551 : : * with invertibility condition (synthesized):
552 : : * (bvslt ones (bvand (bvneg s) t))
553 : : * where
554 : : * z = 0 with getSize(z) = w
555 : : * and ones = ~0 with getSize(ones) = w */
556 : : Node a = nm->mkNode(
557 : 2 : Kind::BITVECTOR_AND, nm->mkNode(Kind::BITVECTOR_NEG, s), t);
558 : 1 : scl = nm->mkNode(Kind::BITVECTOR_SLT, bv::utils::mkOnes(w), a);
559 : : }
560 : : }
561 : : else
562 : : {
563 [ + + ]: 2 : if (pol)
564 : : {
565 : : /* s % x > t
566 : : * with invertibility condition:
567 : : * (and
568 : : * (=> (bvsge s z) (bvsgt s t))
569 : : * (=> (bvslt s z)
570 : : * (bvsgt (bvlshr (bvsub s (_ bv1 w)) (_ bv1 w)) t)))
571 : : * where
572 : : * z = 0 with getSize(z) = w */
573 : 2 : Node z = bv::utils::mkZero(w);
574 : : Node i1 = nm->mkNode(Kind::IMPLIES,
575 : 2 : nm->mkNode(Kind::BITVECTOR_SGE, s, z),
576 : 5 : nm->mkNode(Kind::BITVECTOR_SGT, s, t));
577 : : Node shr = nm->mkNode(
578 : 3 : Kind::BITVECTOR_LSHR, bv::utils::mkDec(s), bv::utils::mkOne(w));
579 : : Node i2 = nm->mkNode(Kind::IMPLIES,
580 : 2 : nm->mkNode(Kind::BITVECTOR_SLT, s, z),
581 : 4 : nm->mkNode(Kind::BITVECTOR_SGT, shr, t));
582 : 1 : scl = nm->mkNode(Kind::AND, i1, i2);
583 : : }
584 : : else
585 : : {
586 : : /* s % x <= t
587 : : * with invertibility condition (synthesized):
588 : : * (or (bvult t min) (bvsge t s))
589 : : * where
590 : : * min is the minimum signed value with getSize(min) = w */
591 : 2 : Node min = bv::utils::mkMinSigned(w);
592 : 3 : Node o1 = nm->mkNode(Kind::BITVECTOR_ULT, t, min);
593 : 2 : Node o2 = nm->mkNode(Kind::BITVECTOR_SGE, t, s);
594 : 1 : scl = nm->mkNode(Kind::OR, o1, o2);
595 : : }
596 : : }
597 : : }
598 : :
599 : : Node scr =
600 : 575 : nm->mkNode(litk, idx == 0 ? nm->mkNode(k, x, s) : nm->mkNode(k, s, x), t);
601 [ + + ]: 230 : Node ic = nm->mkNode(Kind::IMPLIES, scl, pol ? scr : scr.notNode());
602 [ + - ]: 115 : Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << ic << std::endl;
603 : 230 : return ic;
604 : : }
605 : :
606 : 109 : Node getICBvUdiv(
607 : : bool pol, Kind litk, Kind k, unsigned idx, Node x, Node s, Node t)
608 : : {
609 [ - + ][ - + ]: 109 : Assert(k == Kind::BITVECTOR_UDIV);
[ - - ]
610 [ + + ][ + + ]: 109 : Assert(litk == Kind::EQUAL || litk == Kind::BITVECTOR_ULT
[ + + ][ + + ]
[ - + ][ - + ]
[ - - ]
611 : : || litk == Kind::BITVECTOR_SLT || litk == Kind::BITVECTOR_UGT
612 : : || litk == Kind::BITVECTOR_SGT);
613 : :
614 : 109 : NodeManager* nm = NodeManager::currentNM();
615 : 109 : unsigned w = bv::utils::getSize(s);
616 [ - + ][ - + ]: 109 : Assert(w == bv::utils::getSize(t));
[ - - ]
617 : 218 : Node scl;
618 : 218 : Node z = bv::utils::mkZero(w);
619 : :
620 [ + + ]: 109 : if (litk == Kind::EQUAL)
621 : : {
622 [ + + ]: 93 : if (idx == 0)
623 : : {
624 [ + + ]: 39 : if (pol)
625 : : {
626 : : /* x udiv s = t
627 : : * with invertibility condition (synthesized):
628 : : * (= (bvudiv (bvmul s t) s) t)
629 : : *
630 : : * is equivalent to:
631 : : * (or
632 : : * (and (= t (bvnot z))
633 : : * (or (= s z) (= s (_ bv1 w))))
634 : : * (and (distinct t (bvnot z))
635 : : * (distinct s z)
636 : : * (not (umulo s t))))
637 : : *
638 : : * where
639 : : * umulo(s, t) is true if s * t produces and overflow
640 : : * and z = 0 with getSize(z) = w */
641 : 90 : Node mul = nm->mkNode(Kind::BITVECTOR_MULT, s, t);
642 : 60 : Node div = nm->mkNode(Kind::BITVECTOR_UDIV, mul, s);
643 : 30 : scl = nm->mkNode(Kind::EQUAL, div, t);
644 : : }
645 : : else
646 : : {
647 : : /* x udiv s != t
648 : : * with invertibility condition:
649 : : * (or (distinct s z) (distinct t ones))
650 : : * where
651 : : * z = 0 with getSize(z) = w
652 : : * and ones = ~0 with getSize(ones) = w */
653 : 9 : Node ones = bv::utils::mkOnes(w);
654 : 27 : scl = nm->mkNode(
655 : 36 : Kind::OR, s.eqNode(z).notNode(), t.eqNode(ones).notNode());
656 : : }
657 : : }
658 : : else
659 : : {
660 [ + + ]: 54 : if (pol)
661 : : {
662 : : /* s udiv x = t
663 : : * with invertibility condition (synthesized):
664 : : * (= (bvudiv s (bvudiv s t)) t)
665 : : *
666 : : * is equivalent to:
667 : : * (or
668 : : * (= s t)
669 : : * (= t (bvnot z))
670 : : * (and
671 : : * (bvuge s t)
672 : : * (or
673 : : * (= (bvurem s t) z)
674 : : * (bvule (bvadd (bvudiv s (bvadd t (_ bv1 w))) (_ bv1 w))
675 : : * (bvudiv s t)))
676 : : * (=> (= s (bvnot (_ bv0 8))) (distinct t (_ bv0 8)))))
677 : : *
678 : : * where
679 : : * z = 0 with getSize(z) = w */
680 : 90 : Node div = nm->mkNode(Kind::BITVECTOR_UDIV, s, t);
681 : 180 : scl = nm->mkNode(
682 : 135 : Kind::EQUAL, nm->mkNode(Kind::BITVECTOR_UDIV, s, div), t);
683 : : }
684 : : else
685 : : {
686 : : /* s udiv x != t
687 : : * with invertibility condition (w > 1):
688 : : * true (no invertibility condition)
689 : : *
690 : : * with invertibility condition (w == 1):
691 : : * (= (bvand s t) z)
692 : : *
693 : : * where
694 : : * z = 0 with getSize(z) = w */
695 [ + - ]: 9 : if (w > 1)
696 : : {
697 : 9 : scl = nm->mkConst<bool>(true);
698 : : }
699 : : else
700 : : {
701 : 0 : scl = nm->mkNode(Kind::BITVECTOR_AND, s, t).eqNode(z);
702 : : }
703 : : }
704 : : }
705 : : }
706 [ + + ]: 16 : else if (litk == Kind::BITVECTOR_ULT)
707 : : {
708 [ + + ]: 4 : if (idx == 0)
709 : : {
710 [ + + ]: 2 : if (pol)
711 : : {
712 : : /* x udiv s < t
713 : : * with invertibility condition (synthesized):
714 : : * (and (bvult z s) (bvult z t))
715 : : * where
716 : : * z = 0 with getSize(z) = w */
717 : 3 : Node u1 = nm->mkNode(Kind::BITVECTOR_ULT, z, s);
718 : 2 : Node u2 = nm->mkNode(Kind::BITVECTOR_ULT, z, t);
719 : 1 : scl = nm->mkNode(Kind::AND, u1, u2);
720 : : }
721 : : else
722 : : {
723 : : /* x udiv s >= t
724 : : * with invertibility condition (synthesized):
725 : : * (= (bvand (bvudiv (bvmul s t) t) s) s) */
726 : 3 : Node mul = nm->mkNode(Kind::BITVECTOR_MULT, s, t);
727 : 2 : Node div = nm->mkNode(Kind::BITVECTOR_UDIV, mul, t);
728 : : scl =
729 : 1 : nm->mkNode(Kind::EQUAL, nm->mkNode(Kind::BITVECTOR_AND, div, s), s);
730 : : }
731 : : }
732 : : else
733 : : {
734 [ + + ]: 2 : if (pol)
735 : : {
736 : : /* s udiv x < t
737 : : * with invertibility condition (synthesized):
738 : : * (and (bvult z (bvnot (bvand (bvneg t) s))) (bvult z t))
739 : : * where
740 : : * z = 0 with getSize(z) = w */
741 : : Node a = nm->mkNode(
742 : 3 : Kind::BITVECTOR_AND, nm->mkNode(Kind::BITVECTOR_NEG, t), s);
743 : : Node u1 = nm->mkNode(
744 : 3 : Kind::BITVECTOR_ULT, z, nm->mkNode(Kind::BITVECTOR_NOT, a));
745 : 2 : Node u2 = nm->mkNode(Kind::BITVECTOR_ULT, z, t);
746 : 1 : scl = nm->mkNode(Kind::AND, u1, u2);
747 : : }
748 : : else
749 : : {
750 : : /* s udiv x >= t
751 : : * true (no invertibility condition) */
752 : 1 : scl = nm->mkConst<bool>(true);
753 : : }
754 : : }
755 : : }
756 [ + + ]: 12 : else if (litk == Kind::BITVECTOR_UGT)
757 : : {
758 [ + + ]: 4 : if (idx == 0)
759 : : {
760 [ + + ]: 2 : if (pol)
761 : : {
762 : : /* x udiv s > t
763 : : * with invertibility condition:
764 : : * (bvugt (bvudiv ones s) t)
765 : : * where
766 : : * ones = ~0 with getSize(ones) = w */
767 : 2 : Node ones = bv::utils::mkOnes(w);
768 : 2 : Node div = nm->mkNode(Kind::BITVECTOR_UDIV, ones, s);
769 : 1 : scl = nm->mkNode(Kind::BITVECTOR_UGT, div, t);
770 : : }
771 : : else
772 : : {
773 : : /* x udiv s <= t
774 : : * with invertibility condition (synthesized):
775 : : * (bvuge (bvor s t) (bvnot (bvneg s))) */
776 : 3 : Node u1 = nm->mkNode(Kind::BITVECTOR_OR, s, t);
777 : : Node u2 =
778 : 2 : nm->mkNode(Kind::BITVECTOR_NOT, nm->mkNode(Kind::BITVECTOR_NEG, s));
779 : 1 : scl = nm->mkNode(Kind::BITVECTOR_UGE, u1, u2);
780 : : }
781 : : }
782 : : else
783 : : {
784 [ + + ]: 2 : if (pol)
785 : : {
786 : : /* s udiv x > t
787 : : * with invertibility condition (synthesized):
788 : : * (bvult t ones)
789 : : * where
790 : : * ones = ~0 with getSize(ones) = w */
791 : 1 : Node ones = bv::utils::mkOnes(w);
792 : 1 : scl = nm->mkNode(Kind::BITVECTOR_ULT, t, ones);
793 : : }
794 : : else
795 : : {
796 : : /* s udiv x <= t
797 : : * with invertibility condition (synthesized):
798 : : * (bvult z (bvor (bvnot s) t))
799 : : * where
800 : : * z = 0 with getSize(z) = w */
801 : 2 : scl = nm->mkNode(
802 : : Kind::BITVECTOR_ULT,
803 : : z,
804 : 4 : nm->mkNode(
805 : 3 : Kind::BITVECTOR_OR, nm->mkNode(Kind::BITVECTOR_NOT, s), t));
806 : : }
807 : : }
808 : : }
809 [ + + ]: 8 : else if (litk == Kind::BITVECTOR_SLT)
810 : : {
811 [ + + ]: 4 : if (idx == 0)
812 : : {
813 [ + + ]: 2 : if (pol)
814 : : {
815 : : /* x udiv s < t
816 : : * with invertibility condition:
817 : : * (=> (bvsle t z) (bvslt (bvudiv min s) t))
818 : : * where
819 : : * z = 0 with getSize(z) = w
820 : : * and min is the minimum signed value with getSize(min) = w */
821 : 2 : Node min = bv::utils::mkMinSigned(w);
822 : 3 : Node sle = nm->mkNode(Kind::BITVECTOR_SLE, t, z);
823 : 3 : Node div = nm->mkNode(Kind::BITVECTOR_UDIV, min, s);
824 : 2 : Node slt = nm->mkNode(Kind::BITVECTOR_SLT, div, t);
825 : 1 : scl = nm->mkNode(Kind::IMPLIES, sle, slt);
826 : : }
827 : : else
828 : : {
829 : : /* x udiv s >= t
830 : : * with invertibility condition:
831 : : * (or
832 : : * (bvsge (bvudiv ones s) t)
833 : : * (bvsge (bvudiv max s) t))
834 : : * where
835 : : * ones = ~0 with getSize(ones) = w
836 : : * and max is the maximum signed value with getSize(max) = w */
837 : 2 : Node max = bv::utils::mkMaxSigned(w);
838 : 2 : Node ones = bv::utils::mkOnes(w);
839 : 3 : Node udiv1 = nm->mkNode(Kind::BITVECTOR_UDIV, ones, s);
840 : 3 : Node udiv2 = nm->mkNode(Kind::BITVECTOR_UDIV, max, s);
841 : 3 : Node sge1 = nm->mkNode(Kind::BITVECTOR_SGE, udiv1, t);
842 : 2 : Node sge2 = nm->mkNode(Kind::BITVECTOR_SGE, udiv2, t);
843 : 1 : scl = nm->mkNode(Kind::OR, sge1, sge2);
844 : : }
845 : : }
846 : : else
847 : : {
848 [ + + ]: 2 : if (pol)
849 : : {
850 : : /* s udiv x < t
851 : : * with invertibility condition (synthesized):
852 : : * (or (bvslt s t) (bvsge t z))
853 : : * where
854 : : * z = 0 with getSize(z) = w */
855 : 3 : Node slt = nm->mkNode(Kind::BITVECTOR_SLT, s, t);
856 : 2 : Node sge = nm->mkNode(Kind::BITVECTOR_SGE, t, z);
857 : 1 : scl = nm->mkNode(Kind::OR, slt, sge);
858 : : }
859 : : else
860 : : {
861 : : /* s udiv x >= t
862 : : * with invertibility condition (w > 1):
863 : : * (and
864 : : * (=> (bvsge s z) (bvsge s t))
865 : : * (=> (bvslt s z) (bvsge (bvlshr s (_ bv1 w)) t)))
866 : : *
867 : : * with invertibility condition (w == 1):
868 : : * (bvsge s t)
869 : : *
870 : : * where
871 : : * z = 0 with getSize(z) = w */
872 : :
873 [ + - ]: 1 : if (w > 1)
874 : : {
875 : : Node div =
876 : 3 : nm->mkNode(Kind::BITVECTOR_LSHR, s, bv::utils::mkConst(w, 1));
877 : : Node i1 = nm->mkNode(Kind::IMPLIES,
878 : 2 : nm->mkNode(Kind::BITVECTOR_SGE, s, z),
879 : 5 : nm->mkNode(Kind::BITVECTOR_SGE, s, t));
880 : : Node i2 = nm->mkNode(Kind::IMPLIES,
881 : 2 : nm->mkNode(Kind::BITVECTOR_SLT, s, z),
882 : 4 : nm->mkNode(Kind::BITVECTOR_SGE, div, t));
883 : 1 : scl = nm->mkNode(Kind::AND, i1, i2);
884 : : }
885 : : else
886 : : {
887 : 0 : scl = nm->mkNode(Kind::BITVECTOR_SGE, s, t);
888 : : }
889 : : }
890 : : }
891 : : }
892 : : else
893 : : {
894 [ - + ][ - + ]: 4 : Assert(litk == Kind::BITVECTOR_SGT);
[ - - ]
895 [ + + ]: 4 : if (idx == 0)
896 : : {
897 [ + + ]: 2 : if (pol)
898 : : {
899 : : /* x udiv s > t
900 : : * with invertibility condition:
901 : : * (or
902 : : * (bvsgt (bvudiv ones s) t)
903 : : * (bvsgt (bvudiv max s) t))
904 : : * where
905 : : * ones = ~0 with getSize(ones) = w
906 : : * and max is the maximum signed value with getSize(max) = w */
907 : 2 : Node max = bv::utils::mkMaxSigned(w);
908 : 2 : Node ones = bv::utils::mkOnes(w);
909 : 3 : Node div1 = nm->mkNode(Kind::BITVECTOR_UDIV, ones, s);
910 : 3 : Node sgt1 = nm->mkNode(Kind::BITVECTOR_SGT, div1, t);
911 : 3 : Node div2 = nm->mkNode(Kind::BITVECTOR_UDIV, max, s);
912 : 2 : Node sgt2 = nm->mkNode(Kind::BITVECTOR_SGT, div2, t);
913 : 1 : scl = nm->mkNode(Kind::OR, sgt1, sgt2);
914 : : }
915 : : else
916 : : {
917 : : /* x udiv s <= t
918 : : * with invertibility condition (combination of = and <):
919 : : * (or
920 : : * (= (bvudiv (bvmul s t) s) t) ; eq, synthesized
921 : : * (=> (bvsle t z) (bvslt (bvudiv min s) t))) ; slt
922 : : * where
923 : : * z = 0 with getSize(z) = w
924 : : * and min is the minimum signed value with getSize(min) = w */
925 : 3 : Node mul = nm->mkNode(Kind::BITVECTOR_MULT, s, t);
926 : 3 : Node div1 = nm->mkNode(Kind::BITVECTOR_UDIV, mul, s);
927 : 3 : Node o1 = nm->mkNode(Kind::EQUAL, div1, t);
928 : 2 : Node min = bv::utils::mkMinSigned(w);
929 : 3 : Node sle = nm->mkNode(Kind::BITVECTOR_SLE, t, z);
930 : 3 : Node div2 = nm->mkNode(Kind::BITVECTOR_UDIV, min, s);
931 : 3 : Node slt = nm->mkNode(Kind::BITVECTOR_SLT, div2, t);
932 : 2 : Node o2 = nm->mkNode(Kind::IMPLIES, sle, slt);
933 : 1 : scl = nm->mkNode(Kind::OR, o1, o2);
934 : : }
935 : : }
936 : : else
937 : : {
938 [ + + ]: 2 : if (pol)
939 : : {
940 : : /* s udiv x > t
941 : : * with invertibility condition (w > 1):
942 : : * (and
943 : : * (=> (bvsge s z) (bvsgt s t))
944 : : * (=> (bvslt s z) (bvsgt (bvlshr s (_ bv1 w)) t)))
945 : : *
946 : : * with invertibility condition (w == 1):
947 : : * (bvsgt s t)
948 : : *
949 : : * where
950 : : * z = 0 with getSize(z) = w */
951 [ + - ]: 1 : if (w > 1)
952 : : {
953 : : Node div =
954 : 3 : nm->mkNode(Kind::BITVECTOR_LSHR, s, bv::utils::mkConst(w, 1));
955 : : Node i1 = nm->mkNode(Kind::IMPLIES,
956 : 2 : nm->mkNode(Kind::BITVECTOR_SGE, s, z),
957 : 5 : nm->mkNode(Kind::BITVECTOR_SGT, s, t));
958 : : Node i2 = nm->mkNode(Kind::IMPLIES,
959 : 2 : nm->mkNode(Kind::BITVECTOR_SLT, s, z),
960 : 4 : nm->mkNode(Kind::BITVECTOR_SGT, div, t));
961 : 1 : scl = nm->mkNode(Kind::AND, i1, i2);
962 : : }
963 : : else
964 : : {
965 : 0 : scl = nm->mkNode(Kind::BITVECTOR_SGT, s, t);
966 : : }
967 : : }
968 : : else
969 : : {
970 : : /* s udiv x <= t
971 : : * with invertibility condition (synthesized):
972 : : * (not (and (bvslt t (bvnot #x0)) (bvslt t s)))
973 : : * <->
974 : : * (or (bvsge t ones) (bvsge t s))
975 : : * where
976 : : * ones = ~0 with getSize(ones) = w */
977 : 2 : Node ones = bv::utils::mkOnes(w);
978 : 3 : Node sge1 = nm->mkNode(Kind::BITVECTOR_SGE, t, ones);
979 : 2 : Node sge2 = nm->mkNode(Kind::BITVECTOR_SGE, t, s);
980 : 1 : scl = nm->mkNode(Kind::OR, sge1, sge2);
981 : : }
982 : : }
983 : : }
984 : :
985 : : Node scr =
986 : 545 : nm->mkNode(litk, idx == 0 ? nm->mkNode(k, x, s) : nm->mkNode(k, s, x), t);
987 [ + + ]: 218 : Node ic = nm->mkNode(Kind::IMPLIES, scl, pol ? scr : scr.notNode());
988 [ + - ]: 109 : Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << ic << std::endl;
989 : 218 : return ic;
990 : : }
991 : :
992 : 495 : Node getICBvAndOr(
993 : : bool pol, Kind litk, Kind k, unsigned idx, Node x, Node s, Node t)
994 : : {
995 [ + + ][ - + ]: 495 : Assert(k == Kind::BITVECTOR_AND || k == Kind::BITVECTOR_OR);
[ - + ][ - - ]
996 [ + + ][ + + ]: 495 : Assert(litk == Kind::EQUAL || litk == Kind::BITVECTOR_ULT
[ + + ][ + + ]
[ - + ][ - + ]
[ - - ]
997 : : || litk == Kind::BITVECTOR_SLT || litk == Kind::BITVECTOR_UGT
998 : : || litk == Kind::BITVECTOR_SGT);
999 : :
1000 : 495 : NodeManager* nm = NodeManager::currentNM();
1001 : 495 : unsigned w = bv::utils::getSize(s);
1002 [ - + ][ - + ]: 495 : Assert(w == bv::utils::getSize(t));
[ - - ]
1003 : 990 : Node scl;
1004 : :
1005 [ + + ]: 495 : if (litk == Kind::EQUAL)
1006 : : {
1007 [ + + ]: 463 : if (pol)
1008 : : {
1009 : : /* x & s = t
1010 : : * x | s = t
1011 : : * with invertibility condition:
1012 : : * (= (bvand t s) t)
1013 : : * (= (bvor t s) t) */
1014 : 455 : scl = nm->mkNode(Kind::EQUAL, t, nm->mkNode(k, t, s));
1015 : : }
1016 : : else
1017 : : {
1018 [ + + ]: 8 : if (k == Kind::BITVECTOR_AND)
1019 : : {
1020 : : /* x & s = t
1021 : : * with invertibility condition:
1022 : : * (or (distinct s z) (distinct t z))
1023 : : * where
1024 : : * z = 0 with getSize(z) = w */
1025 : 4 : Node z = bv::utils::mkZero(w);
1026 : : scl =
1027 : 4 : nm->mkNode(Kind::OR, s.eqNode(z).notNode(), t.eqNode(z).notNode());
1028 : : }
1029 : : else
1030 : : {
1031 : : /* x | s = t
1032 : : * with invertibility condition:
1033 : : * (or (distinct s ones) (distinct t ones))
1034 : : * where
1035 : : * ones = ~0 with getSize(ones) = w */
1036 : 4 : Node n = bv::utils::mkOnes(w);
1037 : : scl =
1038 : 4 : nm->mkNode(Kind::OR, s.eqNode(n).notNode(), t.eqNode(n).notNode());
1039 : : }
1040 : : }
1041 : : }
1042 [ + + ]: 32 : else if (litk == Kind::BITVECTOR_ULT)
1043 : : {
1044 [ + + ]: 8 : if (pol)
1045 : : {
1046 [ + + ]: 4 : if (k == Kind::BITVECTOR_AND)
1047 : : {
1048 : : /* x & s < t
1049 : : * with invertibility condition (synthesized):
1050 : : * (distinct t z)
1051 : : * where
1052 : : * z = 0 with getSize(z) = 0 */
1053 : 2 : Node z = bv::utils::mkZero(w);
1054 : 2 : scl = t.eqNode(z).notNode();
1055 : : }
1056 : : else
1057 : : {
1058 : : /* x | s < t
1059 : : * with invertibility condition (synthesized):
1060 : : * (bvult s t) */
1061 : 2 : scl = nm->mkNode(Kind::BITVECTOR_ULT, s, t);
1062 : : }
1063 : : }
1064 : : else
1065 : : {
1066 [ + + ]: 4 : if (k == Kind::BITVECTOR_AND)
1067 : : {
1068 : : /* x & s >= t
1069 : : * with invertibility condition (synthesized):
1070 : : * (bvuge s t) */
1071 : 2 : scl = nm->mkNode(Kind::BITVECTOR_UGE, s, t);
1072 : : }
1073 : : else
1074 : : {
1075 : : /* x | s >= t
1076 : : * with invertibility condition (synthesized):
1077 : : * true (no invertibility condition) */
1078 : 2 : scl = nm->mkConst<bool>(true);
1079 : : }
1080 : : }
1081 : : }
1082 [ + + ]: 24 : else if (litk == Kind::BITVECTOR_UGT)
1083 : : {
1084 [ + + ]: 8 : if (pol)
1085 : : {
1086 [ + + ]: 4 : if (k == Kind::BITVECTOR_AND)
1087 : : {
1088 : : /* x & s > t
1089 : : * with invertibility condition (synthesized):
1090 : : * (bvult t s) */
1091 : 2 : scl = nm->mkNode(Kind::BITVECTOR_ULT, t, s);
1092 : : }
1093 : : else
1094 : : {
1095 : : /* x | s > t
1096 : : * with invertibility condition (synthesized):
1097 : : * (bvult t ones)
1098 : : * where
1099 : : * ones = ~0 with getSize(ones) = w */
1100 : 2 : scl = nm->mkNode(Kind::BITVECTOR_ULT, t, bv::utils::mkOnes(w));
1101 : : }
1102 : : }
1103 : : else
1104 : : {
1105 [ + + ]: 4 : if (k == Kind::BITVECTOR_AND)
1106 : : {
1107 : : /* x & s <= t
1108 : : * with invertibility condition (synthesized):
1109 : : * true (no invertibility condition) */
1110 : 2 : scl = nm->mkConst<bool>(true);
1111 : : }
1112 : : else
1113 : : {
1114 : : /* x | s <= t
1115 : : * with invertibility condition (synthesized):
1116 : : * (bvuge t s) */
1117 : 2 : scl = nm->mkNode(Kind::BITVECTOR_UGE, t, s);
1118 : : }
1119 : : }
1120 : : }
1121 [ + + ]: 16 : else if (litk == Kind::BITVECTOR_SLT)
1122 : : {
1123 [ + + ]: 8 : if (pol)
1124 : : {
1125 [ + + ]: 4 : if (k == Kind::BITVECTOR_AND)
1126 : : {
1127 : : /* x & s < t
1128 : : * with invertibility condition (synthesized):
1129 : : * (bvslt (bvand (bvnot (bvneg t)) s) t) */
1130 : : Node nnt =
1131 : 4 : nm->mkNode(Kind::BITVECTOR_NOT, nm->mkNode(Kind::BITVECTOR_NEG, t));
1132 : 8 : scl = nm->mkNode(
1133 : 6 : Kind::BITVECTOR_SLT, nm->mkNode(Kind::BITVECTOR_AND, nnt, s), t);
1134 : : }
1135 : : else
1136 : : {
1137 : : /* x | s < t
1138 : : * with invertibility condition (synthesized):
1139 : : * (bvslt (bvor (bvnot (bvsub s t)) s) t) */
1140 : : Node st = nm->mkNode(Kind::BITVECTOR_NOT,
1141 : 4 : nm->mkNode(Kind::BITVECTOR_SUB, s, t));
1142 : 8 : scl = nm->mkNode(
1143 : 6 : Kind::BITVECTOR_SLT, nm->mkNode(Kind::BITVECTOR_OR, st, s), t);
1144 : : }
1145 : : }
1146 : : else
1147 : : {
1148 [ + + ]: 4 : if (k == Kind::BITVECTOR_AND)
1149 : : {
1150 : : /* x & s >= t
1151 : : * with invertibility condition (case = combined with synthesized
1152 : : * bvsgt): (or
1153 : : * (= (bvand s t) t)
1154 : : * (bvslt t (bvand (bvsub t s) s))) */
1155 : : Node sc_sgt = nm->mkNode(
1156 : : Kind::BITVECTOR_SLT,
1157 : : t,
1158 : 6 : nm->mkNode(
1159 : 10 : Kind::BITVECTOR_AND, nm->mkNode(Kind::BITVECTOR_SUB, t, s), s));
1160 : 4 : Node sc_eq = nm->mkNode(Kind::BITVECTOR_AND, s, t).eqNode(t);
1161 : 2 : scl = sc_eq.orNode(sc_sgt);
1162 : : }
1163 : : else
1164 : : {
1165 : : /* x | s >= t
1166 : : * with invertibility condition (synthesized):
1167 : : * (bvsge s (bvand s t)) */
1168 : 4 : scl = nm->mkNode(
1169 : 6 : Kind::BITVECTOR_SGE, s, nm->mkNode(Kind::BITVECTOR_AND, s, t));
1170 : : }
1171 : : }
1172 : : }
1173 : : else
1174 : : {
1175 [ - + ][ - + ]: 8 : Assert(litk == Kind::BITVECTOR_SGT);
[ - - ]
1176 [ + + ]: 8 : if (pol)
1177 : : {
1178 : : /* x & s > t
1179 : : * x | s > t
1180 : : * with invertibility condition (synthesized):
1181 : : * (bvslt t (bvand s max))
1182 : : * (bvslt t (bvor s max))
1183 : : * where
1184 : : * max is the signed maximum value with getSize(max) = w */
1185 : 4 : Node max = bv::utils::mkMaxSigned(w);
1186 : 4 : scl = nm->mkNode(Kind::BITVECTOR_SLT, t, nm->mkNode(k, s, max));
1187 : : }
1188 : : else
1189 : : {
1190 [ + + ]: 4 : if (k == Kind::BITVECTOR_AND)
1191 : : {
1192 : : /* x & s <= t
1193 : : * with invertibility condition (synthesized):
1194 : : * (bvuge s (bvand t min))
1195 : : * where
1196 : : * min is the signed minimum value with getSize(min) = w */
1197 : 2 : Node min = bv::utils::mkMinSigned(w);
1198 : 4 : scl = nm->mkNode(
1199 : 6 : Kind::BITVECTOR_UGE, s, nm->mkNode(Kind::BITVECTOR_AND, t, min));
1200 : : }
1201 : : else
1202 : : {
1203 : : /* x | s <= t
1204 : : * with invertibility condition (synthesized):
1205 : : * (bvsge t (bvor s min))
1206 : : * where
1207 : : * min is the signed minimum value with getSize(min) = w */
1208 : 2 : Node min = bv::utils::mkMinSigned(w);
1209 : 4 : scl = nm->mkNode(
1210 : 6 : Kind::BITVECTOR_SGE, t, nm->mkNode(Kind::BITVECTOR_OR, s, min));
1211 : : }
1212 : : }
1213 : : }
1214 : 1485 : Node scr = nm->mkNode(litk, nm->mkNode(k, x, s), t);
1215 [ + + ]: 990 : Node ic = nm->mkNode(Kind::IMPLIES, scl, pol ? scr : scr.notNode());
1216 [ + - ]: 495 : Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << ic << std::endl;
1217 : 990 : return ic;
1218 : : }
1219 : :
1220 : : namespace {
1221 : 213 : Node defaultShiftIC(Kind litk, Kind shk, Node s, Node t)
1222 : : {
1223 : : unsigned w;
1224 : 213 : NodeManager* nm = s.getNodeManager();
1225 : 426 : NodeBuilder nb(nm, Kind::OR);
1226 : :
1227 : 213 : w = bv::utils::getSize(s);
1228 [ - + ][ - + ]: 213 : Assert(w == bv::utils::getSize(t));
[ - - ]
1229 : :
1230 : 213 : nb << nm->mkNode(litk, s, t);
1231 [ + + ]: 3121 : for (unsigned i = 1; i <= w; i++)
1232 : : {
1233 : 2908 : Node sw = bv::utils::mkConst(w, i);
1234 : 2908 : nb << nm->mkNode(litk, nm->mkNode(shk, s, sw), t);
1235 : : }
1236 [ - + ]: 213 : if (nb.getNumChildren() == 1) return nb[0];
1237 : 213 : return nb.constructNode();
1238 : : }
1239 : : } // namespace
1240 : :
1241 : 130 : Node getICBvLshr(
1242 : : bool pol, Kind litk, Kind k, unsigned idx, Node x, Node s, Node t)
1243 : : {
1244 [ - + ][ - + ]: 130 : Assert(k == Kind::BITVECTOR_LSHR);
[ - - ]
1245 [ + + ][ + + ]: 130 : Assert(litk == Kind::EQUAL || litk == Kind::BITVECTOR_ULT
[ + + ][ + + ]
[ - + ][ - + ]
[ - - ]
1246 : : || litk == Kind::BITVECTOR_SLT || litk == Kind::BITVECTOR_UGT
1247 : : || litk == Kind::BITVECTOR_SGT);
1248 : :
1249 : 130 : NodeManager* nm = NodeManager::currentNM();
1250 : 260 : Node scl;
1251 : 130 : unsigned w = bv::utils::getSize(s);
1252 [ - + ][ - + ]: 130 : Assert(w == bv::utils::getSize(t));
[ - - ]
1253 : 260 : Node z = bv::utils::mkZero(w);
1254 : :
1255 [ + + ]: 130 : if (litk == Kind::EQUAL)
1256 : : {
1257 [ + + ]: 114 : if (idx == 0)
1258 : : {
1259 : 54 : Node ww = bv::utils::mkConst(w, w);
1260 : :
1261 [ + + ]: 27 : if (pol)
1262 : : {
1263 : : /* x >> s = t
1264 : : * with invertibility condition (synthesized):
1265 : : * (= (bvlshr (bvshl t s) s) t) */
1266 : 72 : Node shl = nm->mkNode(Kind::BITVECTOR_SHL, t, s);
1267 : 48 : Node lshr = nm->mkNode(Kind::BITVECTOR_LSHR, shl, s);
1268 : 24 : scl = lshr.eqNode(t);
1269 : : }
1270 : : else
1271 : : {
1272 : : /* x >> s != t
1273 : : * with invertibility condition:
1274 : : * (or (distinct t z) (bvult s w))
1275 : : * where
1276 : : * z = 0 with getSize(z) = w
1277 : : * and w = getSize(s) = getSize(t) */
1278 : 9 : scl = nm->mkNode(Kind::OR,
1279 : 6 : t.eqNode(z).notNode(),
1280 : 9 : nm->mkNode(Kind::BITVECTOR_ULT, s, ww));
1281 : : }
1282 : : }
1283 : : else
1284 : : {
1285 [ + + ]: 87 : if (pol)
1286 : : {
1287 : : /* s >> x = t
1288 : : * with invertibility condition:
1289 : : * (or (= (bvlshr s i) t) ...)
1290 : : * for i in 0..w */
1291 : 84 : scl = defaultShiftIC(Kind::EQUAL, Kind::BITVECTOR_LSHR, s, t);
1292 : : }
1293 : : else
1294 : : {
1295 : : /* s >> x != t
1296 : : * with invertibility condition:
1297 : : * (or (distinct s z) (distinct t z))
1298 : : * where
1299 : : * z = 0 with getSize(z) = w */
1300 : : scl =
1301 : 3 : nm->mkNode(Kind::OR, s.eqNode(z).notNode(), t.eqNode(z).notNode());
1302 : : }
1303 : : }
1304 : : }
1305 [ + + ]: 16 : else if (litk == Kind::BITVECTOR_ULT)
1306 : : {
1307 [ + + ]: 4 : if (idx == 0)
1308 : : {
1309 [ + + ]: 2 : if (pol)
1310 : : {
1311 : : /* x >> s < t
1312 : : * with invertibility condition (synthesized):
1313 : : * (distinct t z)
1314 : : * where
1315 : : * z = 0 with getSize(z) = w */
1316 : 1 : scl = t.eqNode(z).notNode();
1317 : : }
1318 : : else
1319 : : {
1320 : : /* x >> s >= t
1321 : : * with invertibility condition (synthesized):
1322 : : * (= (bvlshr (bvshl t s) s) t) */
1323 : 2 : Node ts = nm->mkNode(Kind::BITVECTOR_SHL, t, s);
1324 : 1 : scl = nm->mkNode(Kind::BITVECTOR_LSHR, ts, s).eqNode(t);
1325 : : }
1326 : : }
1327 : : else
1328 : : {
1329 [ + + ]: 2 : if (pol)
1330 : : {
1331 : : /* s >> x < t
1332 : : * with invertibility condition (synthesized):
1333 : : * (distinct t z)
1334 : : * where
1335 : : * z = 0 with getSize(z) = w */
1336 : 1 : scl = t.eqNode(z).notNode();
1337 : : }
1338 : : else
1339 : : {
1340 : : /* s >> x >= t
1341 : : * with invertibility condition (synthesized):
1342 : : * (bvuge s t) */
1343 : 1 : scl = nm->mkNode(Kind::BITVECTOR_UGE, s, t);
1344 : : }
1345 : : }
1346 : : }
1347 [ + + ]: 12 : else if (litk == Kind::BITVECTOR_UGT)
1348 : : {
1349 [ + + ]: 4 : if (idx == 0)
1350 : : {
1351 [ + + ]: 2 : if (pol)
1352 : : {
1353 : : /* x >> s > t
1354 : : * with invertibility condition (synthesized):
1355 : : * (bvult t (bvlshr (bvnot s) s)) */
1356 : : Node lshr = nm->mkNode(
1357 : 2 : Kind::BITVECTOR_LSHR, nm->mkNode(Kind::BITVECTOR_NOT, s), s);
1358 : 1 : scl = nm->mkNode(Kind::BITVECTOR_ULT, t, lshr);
1359 : : }
1360 : : else
1361 : : {
1362 : : /* x >> s <= t
1363 : : * with invertibility condition:
1364 : : * true (no invertibility condition) */
1365 : 1 : scl = nm->mkConst<bool>(true);
1366 : : }
1367 : : }
1368 : : else
1369 : : {
1370 [ + + ]: 2 : if (pol)
1371 : : {
1372 : : /* s >> x > t
1373 : : * with invertibility condition (synthesized):
1374 : : * (bvult t s) */
1375 : 1 : scl = nm->mkNode(Kind::BITVECTOR_ULT, t, s);
1376 : : }
1377 : : else
1378 : : {
1379 : : /* s >> x <= t
1380 : : * with invertibility condition:
1381 : : * true (no invertibility condition) */
1382 : 1 : scl = nm->mkConst<bool>(true);
1383 : : }
1384 : : }
1385 : : }
1386 [ + + ]: 8 : else if (litk == Kind::BITVECTOR_SLT)
1387 : : {
1388 [ + + ]: 4 : if (idx == 0)
1389 : : {
1390 [ + + ]: 2 : if (pol)
1391 : : {
1392 : : /* x >> s < t
1393 : : * with invertibility condition (synthesized):
1394 : : * (bvslt (bvlshr (bvnot (bvneg t)) s) t) */
1395 : : Node nnt =
1396 : 3 : nm->mkNode(Kind::BITVECTOR_NOT, nm->mkNode(Kind::BITVECTOR_NEG, t));
1397 : 2 : Node lshr = nm->mkNode(Kind::BITVECTOR_LSHR, nnt, s);
1398 : 1 : scl = nm->mkNode(Kind::BITVECTOR_SLT, lshr, t);
1399 : : }
1400 : : else
1401 : : {
1402 : : /* x >> s >= t
1403 : : * with invertibility condition:
1404 : : * (=> (not (= s z)) (bvsge (bvlshr ones s) t))
1405 : : * where
1406 : : * z = 0 with getSize(z) = w
1407 : : * and ones = ~0 with getSize(ones) = w */
1408 : 2 : Node ones = bv::utils::mkOnes(w);
1409 : 3 : Node lshr = nm->mkNode(Kind::BITVECTOR_LSHR, ones, s);
1410 : 1 : Node nz = s.eqNode(z).notNode();
1411 : 1 : scl = nz.impNode(nm->mkNode(Kind::BITVECTOR_SGE, lshr, t));
1412 : : }
1413 : : }
1414 : : else
1415 : : {
1416 [ + + ]: 2 : if (pol)
1417 : : {
1418 : : /* s >> x < t
1419 : : * with invertibility condition (synthesized):
1420 : : * (or (bvslt s t) (bvslt z t))
1421 : : * where
1422 : : * z = 0 with getSize(z) = w */
1423 : 3 : Node st = nm->mkNode(Kind::BITVECTOR_SLT, s, t);
1424 : 2 : Node zt = nm->mkNode(Kind::BITVECTOR_SLT, z, t);
1425 : 1 : scl = st.orNode(zt);
1426 : : }
1427 : : else
1428 : : {
1429 : : /* s >> x >= t
1430 : : * with invertibility condition:
1431 : : * (and
1432 : : * (=> (bvslt s z) (bvsge (bvlshr s (_ bv1 w)) t))
1433 : : * (=> (bvsge s z) (bvsge s t)))
1434 : : * where
1435 : : * z = 0 with getSize(z) = w */
1436 : 2 : Node one = bv::utils::mkConst(w, 1);
1437 : 3 : Node sz = nm->mkNode(Kind::BITVECTOR_SLT, s, z);
1438 : 3 : Node lshr = nm->mkNode(Kind::BITVECTOR_LSHR, s, one);
1439 : 3 : Node sge1 = nm->mkNode(Kind::BITVECTOR_SGE, lshr, t);
1440 : 2 : Node sge2 = nm->mkNode(Kind::BITVECTOR_SGE, s, t);
1441 : 1 : scl = sz.impNode(sge1).andNode(sz.notNode().impNode(sge2));
1442 : : }
1443 : : }
1444 : : }
1445 : : else
1446 : : {
1447 [ - + ][ - + ]: 4 : Assert(litk == Kind::BITVECTOR_SGT);
[ - - ]
1448 [ + + ]: 4 : if (idx == 0)
1449 : : {
1450 [ + + ]: 2 : if (pol)
1451 : : {
1452 : : /* x >> s > t
1453 : : * with invertibility condition (synthesized):
1454 : : * (bvslt t (bvlshr (bvshl max s) s))
1455 : : * where
1456 : : * max is the signed maximum value with getSize(max) = w */
1457 : 2 : Node max = bv::utils::mkMaxSigned(w);
1458 : 3 : Node shl = nm->mkNode(Kind::BITVECTOR_SHL, max, s);
1459 : 2 : Node lshr = nm->mkNode(Kind::BITVECTOR_LSHR, shl, s);
1460 : 1 : scl = nm->mkNode(Kind::BITVECTOR_SLT, t, lshr);
1461 : : }
1462 : : else
1463 : : {
1464 : : /* x >> s <= t
1465 : : * with invertibility condition (synthesized):
1466 : : * (bvsge t (bvlshr t s)) */
1467 : 2 : scl = nm->mkNode(
1468 : 3 : Kind::BITVECTOR_SGE, t, nm->mkNode(Kind::BITVECTOR_LSHR, t, s));
1469 : : }
1470 : : }
1471 : : else
1472 : : {
1473 [ + + ]: 2 : if (pol)
1474 : : {
1475 : : /* s >> x > t
1476 : : * with invertibility condition:
1477 : : * (and
1478 : : * (=> (bvslt s z) (bvsgt (bvlshr s one) t))
1479 : : * (=> (bvsge s z) (bvsgt s t)))
1480 : : * where
1481 : : * z = 0 and getSize(z) = w */
1482 : 2 : Node one = bv::utils::mkOne(w);
1483 : 3 : Node sz = nm->mkNode(Kind::BITVECTOR_SLT, s, z);
1484 : 3 : Node lshr = nm->mkNode(Kind::BITVECTOR_LSHR, s, one);
1485 : 3 : Node sgt1 = nm->mkNode(Kind::BITVECTOR_SGT, lshr, t);
1486 : 2 : Node sgt2 = nm->mkNode(Kind::BITVECTOR_SGT, s, t);
1487 : 1 : scl = sz.impNode(sgt1).andNode(sz.notNode().impNode(sgt2));
1488 : : }
1489 : : else
1490 : : {
1491 : : /* s >> x <= t
1492 : : * with invertibility condition (synthesized):
1493 : : * (or (bvult t min) (bvsge t s))
1494 : : * where
1495 : : * min is the minimum signed value with getSize(min) = w */
1496 : 2 : Node min = bv::utils::mkMinSigned(w);
1497 : 3 : Node ult = nm->mkNode(Kind::BITVECTOR_ULT, t, min);
1498 : 2 : Node sge = nm->mkNode(Kind::BITVECTOR_SGE, t, s);
1499 : 1 : scl = ult.orNode(sge);
1500 : : }
1501 : : }
1502 : : }
1503 : : Node scr =
1504 : 650 : nm->mkNode(litk, idx == 0 ? nm->mkNode(k, x, s) : nm->mkNode(k, s, x), t);
1505 [ + + ]: 260 : Node ic = nm->mkNode(Kind::IMPLIES, scl, pol ? scr : scr.notNode());
1506 [ + - ]: 130 : Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << ic << std::endl;
1507 : 260 : return ic;
1508 : : }
1509 : :
1510 : 135 : Node getICBvAshr(
1511 : : bool pol, Kind litk, Kind k, unsigned idx, Node x, Node s, Node t)
1512 : : {
1513 [ - + ][ - + ]: 135 : Assert(k == Kind::BITVECTOR_ASHR);
[ - - ]
1514 [ + + ][ + + ]: 135 : Assert(litk == Kind::EQUAL || litk == Kind::BITVECTOR_ULT
[ + + ][ + + ]
[ - + ][ - + ]
[ - - ]
1515 : : || litk == Kind::BITVECTOR_SLT || litk == Kind::BITVECTOR_UGT
1516 : : || litk == Kind::BITVECTOR_SGT);
1517 : :
1518 : 135 : NodeManager* nm = NodeManager::currentNM();
1519 : 270 : Node scl;
1520 : 135 : unsigned w = bv::utils::getSize(s);
1521 [ - + ][ - + ]: 135 : Assert(w == bv::utils::getSize(t));
[ - - ]
1522 : 270 : Node z = bv::utils::mkZero(w);
1523 : 270 : Node n = bv::utils::mkOnes(w);
1524 : :
1525 [ + + ]: 135 : if (litk == Kind::EQUAL)
1526 : : {
1527 [ + + ]: 119 : if (idx == 0)
1528 : : {
1529 [ + + ]: 37 : if (pol)
1530 : : {
1531 : : /* x >> s = t
1532 : : * with invertibility condition:
1533 : : * (and
1534 : : * (=> (bvult s w) (= (bvashr (bvshl t s) s) t))
1535 : : * (=> (bvuge s w) (or (= t ones) (= t z)))
1536 : : * )
1537 : : * where
1538 : : * z = 0 with getSize(z) = w
1539 : : * and ones = ~0 with getSize(ones) = w
1540 : : * and w = getSize(t) = getSize(s) */
1541 : 56 : Node ww = bv::utils::mkConst(w, w);
1542 : 84 : Node shl = nm->mkNode(Kind::BITVECTOR_SHL, t, s);
1543 : 84 : Node ashr = nm->mkNode(Kind::BITVECTOR_ASHR, shl, s);
1544 : 84 : Node ult = nm->mkNode(Kind::BITVECTOR_ULT, s, ww);
1545 : 56 : Node imp1 = ult.impNode(ashr.eqNode(t));
1546 : 56 : Node to = t.eqNode(n);
1547 : 56 : Node tz = t.eqNode(z);
1548 : 56 : Node imp2 = ult.notNode().impNode(to.orNode(tz));
1549 : 28 : scl = imp1.andNode(imp2);
1550 : : }
1551 : : else
1552 : : {
1553 : : /* x >> s != t
1554 : : * true (no invertibility condition) */
1555 : 9 : scl = nm->mkConst<bool>(true);
1556 : : }
1557 : : }
1558 : : else
1559 : : {
1560 [ + + ]: 82 : if (pol)
1561 : : {
1562 : : /* s >> x = t
1563 : : * with invertibility condition:
1564 : : * (or (= (bvashr s i) t) ...)
1565 : : * for i in 0..w */
1566 : 79 : scl = defaultShiftIC(Kind::EQUAL, Kind::BITVECTOR_ASHR, s, t);
1567 : : }
1568 : : else
1569 : : {
1570 : : /* s >> x != t
1571 : : * with invertibility condition:
1572 : : * (and
1573 : : * (or (not (= t z)) (not (= s z)))
1574 : : * (or (not (= t ones)) (not (= s ones))))
1575 : : * where
1576 : : * z = 0 with getSize(z) = w
1577 : : * and ones = ~0 with getSize(ones) = w */
1578 : 9 : scl = nm->mkNode(
1579 : : Kind::AND,
1580 : 6 : nm->mkNode(Kind::OR, t.eqNode(z).notNode(), s.eqNode(z).notNode()),
1581 : 9 : nm->mkNode(Kind::OR, t.eqNode(n).notNode(), s.eqNode(n).notNode()));
1582 : : }
1583 : : }
1584 : : }
1585 [ + + ]: 16 : else if (litk == Kind::BITVECTOR_ULT)
1586 : : {
1587 [ + + ]: 4 : if (idx == 0)
1588 : : {
1589 [ + + ]: 2 : if (pol)
1590 : : {
1591 : : /* x >> s < t
1592 : : * with invertibility condition (synthesized):
1593 : : * (distinct t z)
1594 : : * where
1595 : : * z = 0 with getSize(z) = w */
1596 : 1 : scl = t.eqNode(z).notNode();
1597 : : }
1598 : : else
1599 : : {
1600 : : /* x >> s >= t
1601 : : * with invertibility condition (synthesized):
1602 : : * true (no invertibility condition) */
1603 : 1 : scl = nm->mkConst<bool>(true);
1604 : : }
1605 : : }
1606 : : else
1607 : : {
1608 [ + + ]: 2 : if (pol)
1609 : : {
1610 : : /* s >> x < t
1611 : : * with invertibility condition (synthesized):
1612 : : * (and (not (and (bvuge s t) (bvslt s z))) (not (= t z)))
1613 : : * where
1614 : : * z = 0 with getSize(z) = w */
1615 : 3 : Node st = nm->mkNode(Kind::BITVECTOR_UGE, s, t);
1616 : 3 : Node sz = nm->mkNode(Kind::BITVECTOR_SLT, s, z);
1617 : 1 : Node tz = t.eqNode(z).notNode();
1618 : 1 : scl = st.andNode(sz).notNode().andNode(tz);
1619 : : }
1620 : : else
1621 : : {
1622 : : /* s >> x >= t
1623 : : * with invertibility condition (synthesized):
1624 : : * (not (and (bvult s (bvnot s)) (bvult s t))) */
1625 : : Node ss = nm->mkNode(
1626 : 3 : Kind::BITVECTOR_ULT, s, nm->mkNode(Kind::BITVECTOR_NOT, s));
1627 : 2 : Node st = nm->mkNode(Kind::BITVECTOR_ULT, s, t);
1628 : 1 : scl = ss.andNode(st).notNode();
1629 : : }
1630 : : }
1631 : : }
1632 [ + + ]: 12 : else if (litk == Kind::BITVECTOR_UGT)
1633 : : {
1634 [ + + ]: 4 : if (idx == 0)
1635 : : {
1636 [ + + ]: 2 : if (pol)
1637 : : {
1638 : : /* x >> s > t
1639 : : * with invertibility condition (synthesized):
1640 : : * (bvult t ones)
1641 : : * where
1642 : : * ones = ~0 with getSize(ones) = w */
1643 : 1 : scl = nm->mkNode(Kind::BITVECTOR_ULT, t, bv::utils::mkOnes(w));
1644 : : }
1645 : : else
1646 : : {
1647 : : /* x >> s <= t
1648 : : * with invertibility condition (synthesized):
1649 : : * true (no invertibility condition) */
1650 : 1 : scl = nm->mkConst<bool>(true);
1651 : : }
1652 : : }
1653 : : else
1654 : : {
1655 [ + + ]: 2 : if (pol)
1656 : : {
1657 : : /* s >> x > t
1658 : : * with invertibility condition (synthesized):
1659 : : * (or (bvslt s (bvlshr s (bvnot t))) (bvult t s)) */
1660 : : Node lshr = nm->mkNode(
1661 : 3 : Kind::BITVECTOR_LSHR, s, nm->mkNode(Kind::BITVECTOR_NOT, t));
1662 : 3 : Node ts = nm->mkNode(Kind::BITVECTOR_ULT, t, s);
1663 : 2 : Node slt = nm->mkNode(Kind::BITVECTOR_SLT, s, lshr);
1664 : 1 : scl = slt.orNode(ts);
1665 : : }
1666 : : else
1667 : : {
1668 : : /* s >> x <= t
1669 : : * with invertibility condition (synthesized):
1670 : : * (or (bvult s min) (bvuge t s))
1671 : : * where
1672 : : * min is the minimum signed value with getSize(min) = w */
1673 : 2 : Node min = bv::utils::mkMinSigned(w);
1674 : 3 : Node ult = nm->mkNode(Kind::BITVECTOR_ULT, s, min);
1675 : 2 : Node uge = nm->mkNode(Kind::BITVECTOR_UGE, t, s);
1676 : 1 : scl = ult.orNode(uge);
1677 : : }
1678 : : }
1679 : : }
1680 [ + + ]: 8 : else if (litk == Kind::BITVECTOR_SLT)
1681 : : {
1682 [ + + ]: 4 : if (idx == 0)
1683 : : {
1684 [ + + ]: 2 : if (pol)
1685 : : {
1686 : : /* x >> s < t
1687 : : * with invertibility condition:
1688 : : * (bvslt (bvashr min s) t)
1689 : : * where
1690 : : * min is the minimum signed value with getSize(min) = w */
1691 : 1 : Node min = bv::utils::mkMinSigned(w);
1692 : 4 : scl = nm->mkNode(
1693 : 3 : Kind::BITVECTOR_SLT, nm->mkNode(Kind::BITVECTOR_ASHR, min, s), t);
1694 : : }
1695 : : else
1696 : : {
1697 : : /* x >> s >= t
1698 : : * with invertibility condition:
1699 : : * (bvsge (bvlshr max s) t)
1700 : : * where
1701 : : * max is the signed maximum value with getSize(max) = w */
1702 : 1 : Node max = bv::utils::mkMaxSigned(w);
1703 : 4 : scl = nm->mkNode(
1704 : 3 : Kind::BITVECTOR_SGE, nm->mkNode(Kind::BITVECTOR_LSHR, max, s), t);
1705 : : }
1706 : : }
1707 : : else
1708 : : {
1709 [ + + ]: 2 : if (pol)
1710 : : {
1711 : : /* s >> x < t
1712 : : * with invertibility condition (synthesized):
1713 : : * (or (bvslt s t) (bvslt z t))
1714 : : * where
1715 : : * z = 0 and getSize(z) = w */
1716 : 3 : Node st = nm->mkNode(Kind::BITVECTOR_SLT, s, t);
1717 : 2 : Node zt = nm->mkNode(Kind::BITVECTOR_SLT, z, t);
1718 : 1 : scl = st.orNode(zt);
1719 : : }
1720 : : else
1721 : : {
1722 : : /* s >> x >= t
1723 : : * with invertibility condition (synthesized):
1724 : : * (not (and (bvult t (bvnot t)) (bvslt s t))) */
1725 : : Node tt = nm->mkNode(
1726 : 3 : Kind::BITVECTOR_ULT, t, nm->mkNode(Kind::BITVECTOR_NOT, t));
1727 : 2 : Node st = nm->mkNode(Kind::BITVECTOR_SLT, s, t);
1728 : 1 : scl = tt.andNode(st).notNode();
1729 : : }
1730 : : }
1731 : : }
1732 : : else
1733 : : {
1734 [ - + ][ - + ]: 4 : Assert(litk == Kind::BITVECTOR_SGT);
[ - - ]
1735 : 8 : Node max = bv::utils::mkMaxSigned(w);
1736 [ + + ]: 4 : if (idx == 0)
1737 : : {
1738 : 6 : Node lshr = nm->mkNode(Kind::BITVECTOR_LSHR, max, s);
1739 [ + + ]: 2 : if (pol)
1740 : : {
1741 : : /* x >> s > t
1742 : : * with invertibility condition (synthesized):
1743 : : * (bvslt t (bvlshr max s)))
1744 : : * where
1745 : : * max is the signed maximum value with getSize(max) = w */
1746 : 1 : scl = nm->mkNode(Kind::BITVECTOR_SLT, t, lshr);
1747 : : }
1748 : : else
1749 : : {
1750 : : /* x >> s <= t
1751 : : * with invertibility condition (synthesized):
1752 : : * (bvsge t (bvnot (bvlshr max s)))
1753 : : * where
1754 : : * max is the signed maximum value with getSize(max) = w */
1755 : 2 : scl = nm->mkNode(
1756 : 3 : Kind::BITVECTOR_SGE, t, nm->mkNode(Kind::BITVECTOR_NOT, lshr));
1757 : : }
1758 : : }
1759 : : else
1760 : : {
1761 [ + + ]: 2 : if (pol)
1762 : : {
1763 : : /* s >> x > t
1764 : : * with invertibility condition (synthesized):
1765 : : * (and (bvslt t (bvand s max)) (bvslt t (bvor s max)))
1766 : : * where
1767 : : * max is the signed maximum value with getSize(max) = w */
1768 : 3 : Node sam = nm->mkNode(Kind::BITVECTOR_AND, s, max);
1769 : 3 : Node som = nm->mkNode(Kind::BITVECTOR_OR, s, max);
1770 : 3 : Node slta = nm->mkNode(Kind::BITVECTOR_SLT, t, sam);
1771 : 2 : Node slto = nm->mkNode(Kind::BITVECTOR_SLT, t, som);
1772 : 1 : scl = slta.andNode(slto);
1773 : : }
1774 : : else
1775 : : {
1776 : : /* s >> x <= t
1777 : : * with invertibility condition (synthesized):
1778 : : * (or (bvsge t z) (bvsge t s))
1779 : : * where
1780 : : * z = 0 and getSize(z) = w */
1781 : 3 : Node tz = nm->mkNode(Kind::BITVECTOR_SGE, t, z);
1782 : 2 : Node ts = nm->mkNode(Kind::BITVECTOR_SGE, t, s);
1783 : 1 : scl = tz.orNode(ts);
1784 : : }
1785 : : }
1786 : : }
1787 : : Node scr =
1788 : 675 : nm->mkNode(litk, idx == 0 ? nm->mkNode(k, x, s) : nm->mkNode(k, s, x), t);
1789 [ + + ]: 270 : Node ic = nm->mkNode(Kind::IMPLIES, scl, pol ? scr : scr.notNode());
1790 [ + - ]: 135 : Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << ic << std::endl;
1791 : 270 : return ic;
1792 : : }
1793 : :
1794 : 160 : Node getICBvShl(
1795 : : bool pol, Kind litk, Kind k, unsigned idx, Node x, Node s, Node t)
1796 : : {
1797 [ - + ][ - + ]: 160 : Assert(k == Kind::BITVECTOR_SHL);
[ - - ]
1798 [ + + ][ + + ]: 160 : Assert(litk == Kind::EQUAL || litk == Kind::BITVECTOR_ULT
[ + + ][ + + ]
[ - + ][ - + ]
[ - - ]
1799 : : || litk == Kind::BITVECTOR_SLT || litk == Kind::BITVECTOR_UGT
1800 : : || litk == Kind::BITVECTOR_SGT);
1801 : :
1802 : 160 : NodeManager* nm = NodeManager::currentNM();
1803 : 320 : Node scl;
1804 : 160 : unsigned w = bv::utils::getSize(s);
1805 [ - + ][ - + ]: 160 : Assert(w == bv::utils::getSize(t));
[ - - ]
1806 : 320 : Node z = bv::utils::mkZero(w);
1807 : :
1808 [ + + ]: 160 : if (litk == Kind::EQUAL)
1809 : : {
1810 [ + + ]: 144 : if (idx == 0)
1811 : : {
1812 : 194 : Node ww = bv::utils::mkConst(w, w);
1813 : :
1814 [ + + ]: 97 : if (pol)
1815 : : {
1816 : : /* x << s = t
1817 : : * with invertibility condition (synthesized):
1818 : : * (= (bvshl (bvlshr t s) s) t) */
1819 : 282 : Node lshr = nm->mkNode(Kind::BITVECTOR_LSHR, t, s);
1820 : 188 : Node shl = nm->mkNode(Kind::BITVECTOR_SHL, lshr, s);
1821 : 94 : scl = shl.eqNode(t);
1822 : : }
1823 : : else
1824 : : {
1825 : : /* x << s != t
1826 : : * with invertibility condition:
1827 : : * (or (distinct t z) (bvult s w))
1828 : : * with
1829 : : * w = getSize(s) = getSize(t)
1830 : : * and z = 0 with getSize(z) = w */
1831 : 9 : scl = nm->mkNode(Kind::OR,
1832 : 6 : t.eqNode(z).notNode(),
1833 : 9 : nm->mkNode(Kind::BITVECTOR_ULT, s, ww));
1834 : : }
1835 : : }
1836 : : else
1837 : : {
1838 [ + + ]: 47 : if (pol)
1839 : : {
1840 : : /* s << x = t
1841 : : * with invertibility condition:
1842 : : * (or (= (bvshl s i) t) ...)
1843 : : * for i in 0..w */
1844 : 46 : scl = defaultShiftIC(Kind::EQUAL, Kind::BITVECTOR_SHL, s, t);
1845 : : }
1846 : : else
1847 : : {
1848 : : /* s << x != t
1849 : : * with invertibility condition:
1850 : : * (or (distinct s z) (distinct t z))
1851 : : * where
1852 : : * z = 0 with getSize(z) = w */
1853 : : scl =
1854 : 1 : nm->mkNode(Kind::OR, s.eqNode(z).notNode(), t.eqNode(z).notNode());
1855 : : }
1856 : : }
1857 : : }
1858 [ + + ]: 16 : else if (litk == Kind::BITVECTOR_ULT)
1859 : : {
1860 [ + + ]: 4 : if (idx == 0)
1861 : : {
1862 [ + + ]: 2 : if (pol)
1863 : : {
1864 : : /* x << s < t
1865 : : * with invertibility condition (synthesized):
1866 : : * (not (= t z)) */
1867 : 1 : scl = t.eqNode(z).notNode();
1868 : : }
1869 : : else
1870 : : {
1871 : : /* x << s >= t
1872 : : * with invertibility condition (synthesized):
1873 : : * (bvuge (bvshl ones s) t) */
1874 : 2 : Node shl = nm->mkNode(Kind::BITVECTOR_SHL, bv::utils::mkOnes(w), s);
1875 : 1 : scl = nm->mkNode(Kind::BITVECTOR_UGE, shl, t);
1876 : : }
1877 : : }
1878 : : else
1879 : : {
1880 [ + + ]: 2 : if (pol)
1881 : : {
1882 : : /* s << x < t
1883 : : * with invertibility condition (synthesized):
1884 : : * (not (= t z)) */
1885 : 1 : scl = t.eqNode(z).notNode();
1886 : : }
1887 : : else
1888 : : {
1889 : : /* s << x >= t
1890 : : * with invertibility condition:
1891 : : * (or (bvuge (bvshl s i) t) ...)
1892 : : * for i in 0..w */
1893 : 1 : scl = defaultShiftIC(Kind::BITVECTOR_UGE, Kind::BITVECTOR_SHL, s, t);
1894 : : }
1895 : : }
1896 : : }
1897 [ + + ]: 12 : else if (litk == Kind::BITVECTOR_UGT)
1898 : : {
1899 [ + + ]: 4 : if (idx == 0)
1900 : : {
1901 [ + + ]: 2 : if (pol)
1902 : : {
1903 : : /* x << s > t
1904 : : * with invertibility condition (synthesized):
1905 : : * (bvult t (bvshl ones s))
1906 : : * where
1907 : : * ones = ~0 with getSize(ones) = w */
1908 : 2 : Node shl = nm->mkNode(Kind::BITVECTOR_SHL, bv::utils::mkOnes(w), s);
1909 : 1 : scl = nm->mkNode(Kind::BITVECTOR_ULT, t, shl);
1910 : : }
1911 : : else
1912 : : {
1913 : : /* x << s <= t
1914 : : * with invertibility condition:
1915 : : * true (no invertibility condition) */
1916 : 1 : scl = nm->mkConst<bool>(true);
1917 : : }
1918 : : }
1919 : : else
1920 : : {
1921 [ + + ]: 2 : if (pol)
1922 : : {
1923 : : /* s << x > t
1924 : : * with invertibility condition:
1925 : : * (or (bvugt (bvshl s i) t) ...)
1926 : : * for i in 0..w */
1927 : 1 : scl = defaultShiftIC(Kind::BITVECTOR_UGT, Kind::BITVECTOR_SHL, s, t);
1928 : : }
1929 : : else
1930 : : {
1931 : : /* s << x <= t
1932 : : * with invertibility condition:
1933 : : * true (no invertibility condition) */
1934 : 1 : scl = nm->mkConst<bool>(true);
1935 : : }
1936 : : }
1937 : : }
1938 [ + + ]: 8 : else if (litk == Kind::BITVECTOR_SLT)
1939 : : {
1940 [ + + ]: 4 : if (idx == 0)
1941 : : {
1942 [ + + ]: 2 : if (pol)
1943 : : {
1944 : : /* x << s < t
1945 : : * with invertibility condition (synthesized):
1946 : : * (bvslt (bvshl (bvlshr min s) s) t)
1947 : : * where
1948 : : * min is the signed minimum value with getSize(min) = w */
1949 : 2 : Node min = bv::utils::mkMinSigned(w);
1950 : 3 : Node lshr = nm->mkNode(Kind::BITVECTOR_LSHR, min, s);
1951 : 2 : Node shl = nm->mkNode(Kind::BITVECTOR_SHL, lshr, s);
1952 : 1 : scl = nm->mkNode(Kind::BITVECTOR_SLT, shl, t);
1953 : : }
1954 : : else
1955 : : {
1956 : : /* x << s >= t
1957 : : * with invertibility condition (synthesized):
1958 : : * (bvsge (bvand (bvshl max s) max) t)
1959 : : * where
1960 : : * max is the signed maximum value with getSize(max) = w */
1961 : 2 : Node max = bv::utils::mkMaxSigned(w);
1962 : 2 : Node shl = nm->mkNode(Kind::BITVECTOR_SHL, max, s);
1963 : 4 : scl = nm->mkNode(
1964 : 3 : Kind::BITVECTOR_SGE, nm->mkNode(Kind::BITVECTOR_AND, shl, max), t);
1965 : : }
1966 : : }
1967 : : else
1968 : : {
1969 [ + + ]: 2 : if (pol)
1970 : : {
1971 : : /* s << x < t
1972 : : * with invertibility condition (synthesized):
1973 : : * (bvult (bvshl min s) (bvadd t min))
1974 : : * where
1975 : : * min is the signed minimum value with getSize(min) = w */
1976 : 2 : Node min = bv::utils::mkMinSigned(w);
1977 : 3 : Node shl = nm->mkNode(Kind::BITVECTOR_SHL, min, s);
1978 : 2 : Node add = nm->mkNode(Kind::BITVECTOR_ADD, t, min);
1979 : 1 : scl = nm->mkNode(Kind::BITVECTOR_ULT, shl, add);
1980 : : }
1981 : : else
1982 : : {
1983 : : /* s << x >= t
1984 : : * with invertibility condition:
1985 : : * (or (bvsge (bvshl s i) t) ...)
1986 : : * for i in 0..w */
1987 : 1 : scl = defaultShiftIC(Kind::BITVECTOR_SGE, Kind::BITVECTOR_SHL, s, t);
1988 : : }
1989 : : }
1990 : : }
1991 : : else
1992 : : {
1993 [ - + ][ - + ]: 4 : Assert(litk == Kind::BITVECTOR_SGT);
[ - - ]
1994 [ + + ]: 4 : if (idx == 0)
1995 : : {
1996 [ + + ]: 2 : if (pol)
1997 : : {
1998 : : /* x << s > t
1999 : : * with invertibility condition (synthesized):
2000 : : * (bvslt t (bvand (bvshl max s) max))
2001 : : * where
2002 : : * max is the signed maximum value with getSize(max) = w */
2003 : 2 : Node max = bv::utils::mkMaxSigned(w);
2004 : 2 : Node shl = nm->mkNode(Kind::BITVECTOR_SHL, max, s);
2005 : 2 : scl = nm->mkNode(
2006 : 3 : Kind::BITVECTOR_SLT, t, nm->mkNode(Kind::BITVECTOR_AND, shl, max));
2007 : : }
2008 : : else
2009 : : {
2010 : : /* x << s <= t
2011 : : * with invertibility condition (synthesized):
2012 : : * (bvult (bvlshr t (bvlshr t s)) min)
2013 : : * where
2014 : : * min is the signed minimum value with getSize(min) = w */
2015 : 2 : Node min = bv::utils::mkMinSigned(w);
2016 : 2 : Node ts = nm->mkNode(Kind::BITVECTOR_LSHR, t, s);
2017 : 4 : scl = nm->mkNode(
2018 : 3 : Kind::BITVECTOR_ULT, nm->mkNode(Kind::BITVECTOR_LSHR, t, ts), min);
2019 : : }
2020 : : }
2021 : : else
2022 : : {
2023 [ + + ]: 2 : if (pol)
2024 : : {
2025 : : /* s << x > t
2026 : : * with invertibility condition:
2027 : : * (or (bvsgt (bvshl s i) t) ...)
2028 : : * for i in 0..w */
2029 : 1 : scl = defaultShiftIC(Kind::BITVECTOR_SGT, Kind::BITVECTOR_SHL, s, t);
2030 : : }
2031 : : else
2032 : : {
2033 : : /* s << x <= t
2034 : : * with invertibility condition (synthesized):
2035 : : * (bvult (bvlshr t s) min)
2036 : : * where
2037 : : * min is the signed minimum value with getSize(min) = w */
2038 : 1 : Node min = bv::utils::mkMinSigned(w);
2039 : 4 : scl = nm->mkNode(
2040 : 3 : Kind::BITVECTOR_ULT, nm->mkNode(Kind::BITVECTOR_LSHR, t, s), min);
2041 : : }
2042 : : }
2043 : : }
2044 : : Node scr =
2045 : 800 : nm->mkNode(litk, idx == 0 ? nm->mkNode(k, x, s) : nm->mkNode(k, s, x), t);
2046 [ + + ]: 320 : Node ic = nm->mkNode(Kind::IMPLIES, scl, pol ? scr : scr.notNode());
2047 [ + - ]: 160 : Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << ic << std::endl;
2048 : 320 : return ic;
2049 : : }
2050 : :
2051 : 30 : Node getICBvConcat(bool pol, Kind litk, unsigned idx, Node x, Node sv_t, Node t)
2052 : : {
2053 [ + + ][ + + ]: 30 : Assert(litk == Kind::EQUAL || litk == Kind::BITVECTOR_ULT
[ + + ][ + + ]
[ - + ][ - + ]
[ - - ]
2054 : : || litk == Kind::BITVECTOR_SLT || litk == Kind::BITVECTOR_UGT
2055 : : || litk == Kind::BITVECTOR_SGT);
2056 : :
2057 : 30 : Kind k = sv_t.getKind();
2058 [ - + ][ - + ]: 30 : Assert(k == Kind::BITVECTOR_CONCAT);
[ - - ]
2059 : 30 : NodeManager* nm = NodeManager::currentNM();
2060 : 30 : unsigned nchildren = sv_t.getNumChildren();
2061 : 30 : unsigned w1 = 0, w2 = 0;
2062 : 30 : unsigned w = bv::utils::getSize(t), wx = bv::utils::getSize(x);
2063 : 60 : NodeBuilder nbs1(nm, Kind::BITVECTOR_CONCAT),
2064 : 60 : nbs2(nm, Kind::BITVECTOR_CONCAT);
2065 : 60 : Node s1, s2;
2066 : 60 : Node t1, t2, tx;
2067 : 60 : Node scl, scr;
2068 : :
2069 [ + + ]: 30 : if (idx != 0)
2070 : : {
2071 [ + - ]: 20 : if (idx == 1)
2072 : : {
2073 : 20 : s1 = sv_t[0];
2074 : : }
2075 : : else
2076 : : {
2077 [ - - ]: 0 : for (unsigned i = 0; i < idx; ++i)
2078 : : {
2079 : 0 : nbs1 << sv_t[i];
2080 : : }
2081 : 0 : s1 = nbs1.constructNode();
2082 : : }
2083 : 20 : w1 = bv::utils::getSize(s1);
2084 : 20 : t1 = bv::utils::mkExtract(t, w - 1, w - w1);
2085 : : }
2086 : :
2087 : 30 : tx = bv::utils::mkExtract(t, w - w1 - 1, w - w1 - wx);
2088 : :
2089 [ + + ]: 30 : if (idx != nchildren - 1)
2090 : : {
2091 [ + - ]: 20 : if (idx == nchildren - 2)
2092 : : {
2093 : 20 : s2 = sv_t[nchildren - 1];
2094 : : }
2095 : : else
2096 : : {
2097 [ - - ]: 0 : for (unsigned i = idx + 1; i < nchildren; ++i)
2098 : : {
2099 : 0 : nbs2 << sv_t[i];
2100 : : }
2101 : 0 : s2 = nbs2.constructNode();
2102 : : }
2103 : 20 : w2 = bv::utils::getSize(s2);
2104 [ - + ][ - + ]: 20 : Assert(w2 == w - w1 - wx);
[ - - ]
2105 : 20 : t2 = bv::utils::mkExtract(t, w2 - 1, 0);
2106 : : }
2107 : :
2108 [ + + ][ - + ]: 30 : Assert(!s1.isNull() || t1.isNull());
[ - + ][ - - ]
2109 [ + + ][ - + ]: 30 : Assert(!s2.isNull() || t2.isNull());
[ - + ][ - - ]
2110 [ + + ][ - + ]: 30 : Assert(!s1.isNull() || !s2.isNull());
[ - + ][ - - ]
2111 : 30 : Assert(s1.isNull() || w1 == bv::utils::getSize(t1));
2112 : 30 : Assert(s2.isNull() || w2 == bv::utils::getSize(t2));
2113 : :
2114 [ + + ]: 30 : if (litk == Kind::EQUAL)
2115 : : {
2116 [ + + ]: 6 : if (s1.isNull())
2117 : : {
2118 [ + + ]: 2 : if (pol)
2119 : : {
2120 : : /* x o s2 = t (interpret t as tx o t2)
2121 : : * with invertibility condition:
2122 : : * (= s2 t2) */
2123 : 1 : scl = s2.eqNode(t2);
2124 : : }
2125 : : else
2126 : : {
2127 : : /* x o s2 != t
2128 : : * true (no invertibility condition) */
2129 : 1 : scl = nm->mkConst<bool>(true);
2130 : : }
2131 : : }
2132 [ + + ]: 4 : else if (s2.isNull())
2133 : : {
2134 [ + + ]: 2 : if (pol)
2135 : : {
2136 : : /* s1 o x = t (interpret t as t1 o tx)
2137 : : * with invertibility condition:
2138 : : * (= s1 t1) */
2139 : 1 : scl = s1.eqNode(t1);
2140 : : }
2141 : : else
2142 : : {
2143 : : /* s1 o x != t
2144 : : * true (no invertibility condition) */
2145 : 1 : scl = nm->mkConst<bool>(true);
2146 : : }
2147 : : }
2148 : : else
2149 : : {
2150 [ + + ]: 2 : if (pol)
2151 : : {
2152 : : /* s1 o x o s2 = t (interpret t as t1 o tx o t2)
2153 : : * with invertibility condition:
2154 : : * (and (= s1 t1) (= s2 t2)) */
2155 : 1 : scl = nm->mkNode(Kind::AND, s1.eqNode(t1), s2.eqNode(t2));
2156 : : }
2157 : : else
2158 : : {
2159 : : /* s1 o x o s2 != t
2160 : : * true (no invertibility condition) */
2161 : 1 : scl = nm->mkConst<bool>(true);
2162 : : }
2163 : : }
2164 : : }
2165 [ + + ]: 24 : else if (litk == Kind::BITVECTOR_ULT)
2166 : : {
2167 [ + + ]: 6 : if (s1.isNull())
2168 : : {
2169 [ + + ]: 2 : if (pol)
2170 : : {
2171 : : /* x o s2 < t (interpret t as tx o t2)
2172 : : * with invertibility condition:
2173 : : * (=> (= tx z) (bvult s2 t2))
2174 : : * where
2175 : : * z = 0 with getSize(z) = wx */
2176 : 2 : Node z = bv::utils::mkZero(wx);
2177 : 2 : Node ult = nm->mkNode(Kind::BITVECTOR_ULT, s2, t2);
2178 : 1 : scl = nm->mkNode(Kind::IMPLIES, tx.eqNode(z), ult);
2179 : : }
2180 : : else
2181 : : {
2182 : : /* x o s2 >= t (interpret t as tx o t2)
2183 : : * (=> (= tx ones) (bvuge s2 t2))
2184 : : * where
2185 : : * ones = ~0 with getSize(ones) = wx */
2186 : 2 : Node n = bv::utils::mkOnes(wx);
2187 : 2 : Node uge = nm->mkNode(Kind::BITVECTOR_UGE, s2, t2);
2188 : 1 : scl = nm->mkNode(Kind::IMPLIES, tx.eqNode(n), uge);
2189 : : }
2190 : : }
2191 [ + + ]: 4 : else if (s2.isNull())
2192 : : {
2193 [ + + ]: 2 : if (pol)
2194 : : {
2195 : : /* s1 o x < t (interpret t as t1 o tx)
2196 : : * with invertibility condition:
2197 : : * (and (bvule s1 t1) (=> (= s1 t1) (distinct tx z)))
2198 : : * where
2199 : : * z = 0 with getSize(z) = wx */
2200 : 2 : Node z = bv::utils::mkZero(wx);
2201 : 3 : Node ule = nm->mkNode(Kind::BITVECTOR_ULE, s1, t1);
2202 : : Node imp =
2203 : 2 : nm->mkNode(Kind::IMPLIES, s1.eqNode(t1), tx.eqNode(z).notNode());
2204 : 1 : scl = nm->mkNode(Kind::AND, ule, imp);
2205 : : }
2206 : : else
2207 : : {
2208 : : /* s1 o x >= t (interpret t as t1 o tx)
2209 : : * with invertibility condition:
2210 : : * (bvuge s1 t1) */
2211 : 1 : scl = nm->mkNode(Kind::BITVECTOR_UGE, s1, t1);
2212 : : }
2213 : : }
2214 : : else
2215 : : {
2216 [ + + ]: 2 : if (pol)
2217 : : {
2218 : : /* s1 o x o s2 < t (interpret t as t1 o tx o t2)
2219 : : * with invertibility condition:
2220 : : * (and
2221 : : * (bvule s1 t1)
2222 : : * (=> (and (= s1 t1) (= tx z)) (bvult s2 t2)))
2223 : : * where
2224 : : * z = 0 with getSize(z) = wx */
2225 : 2 : Node z = bv::utils::mkZero(wx);
2226 : 3 : Node ule = nm->mkNode(Kind::BITVECTOR_ULE, s1, t1);
2227 : 3 : Node a = nm->mkNode(Kind::AND, s1.eqNode(t1), tx.eqNode(z));
2228 : : Node imp = nm->mkNode(
2229 : 2 : Kind::IMPLIES, a, nm->mkNode(Kind::BITVECTOR_ULT, s2, t2));
2230 : 1 : scl = nm->mkNode(Kind::AND, ule, imp);
2231 : : }
2232 : : else
2233 : : {
2234 : : /* s1 o x o s2 >= t (interpret t as t1 o tx o t2)
2235 : : * with invertibility condition:
2236 : : * (and
2237 : : * (bvuge s1 t1)
2238 : : * (=> (and (= s1 t1) (= tx ones)) (bvuge s2 t2)))
2239 : : * where
2240 : : * ones = ~0 with getSize(ones) = wx */
2241 : 2 : Node n = bv::utils::mkOnes(wx);
2242 : 3 : Node uge = nm->mkNode(Kind::BITVECTOR_UGE, s1, t1);
2243 : 3 : Node a = nm->mkNode(Kind::AND, s1.eqNode(t1), tx.eqNode(n));
2244 : : Node imp = nm->mkNode(
2245 : 2 : Kind::IMPLIES, a, nm->mkNode(Kind::BITVECTOR_UGE, s2, t2));
2246 : 1 : scl = nm->mkNode(Kind::AND, uge, imp);
2247 : : }
2248 : : }
2249 : : }
2250 [ + + ]: 18 : else if (litk == Kind::BITVECTOR_UGT)
2251 : : {
2252 [ + + ]: 6 : if (s1.isNull())
2253 : : {
2254 [ + + ]: 2 : if (pol)
2255 : : {
2256 : : /* x o s2 > t (interpret t as tx o t2)
2257 : : * with invertibility condition:
2258 : : * (=> (= tx ones) (bvugt s2 t2))
2259 : : * where
2260 : : * ones = ~0 with getSize(ones) = wx */
2261 : 2 : Node n = bv::utils::mkOnes(wx);
2262 : 2 : Node ugt = nm->mkNode(Kind::BITVECTOR_UGT, s2, t2);
2263 : 1 : scl = nm->mkNode(Kind::IMPLIES, tx.eqNode(n), ugt);
2264 : : }
2265 : : else
2266 : : {
2267 : : /* x o s2 <= t (interpret t as tx o t2)
2268 : : * with invertibility condition:
2269 : : * (=> (= tx z) (bvule s2 t2))
2270 : : * where
2271 : : * z = 0 with getSize(z) = wx */
2272 : 2 : Node z = bv::utils::mkZero(wx);
2273 : 2 : Node ule = nm->mkNode(Kind::BITVECTOR_ULE, s2, t2);
2274 : 1 : scl = nm->mkNode(Kind::IMPLIES, tx.eqNode(z), ule);
2275 : : }
2276 : : }
2277 [ + + ]: 4 : else if (s2.isNull())
2278 : : {
2279 [ + + ]: 2 : if (pol)
2280 : : {
2281 : : /* s1 o x > t (interpret t as t1 o tx)
2282 : : * with invertibility condition:
2283 : : * (and (bvuge s1 t1) (=> (= s1 t1) (distinct tx ones)))
2284 : : * where
2285 : : * ones = ~0 with getSize(ones) = wx */
2286 : 2 : Node n = bv::utils::mkOnes(wx);
2287 : 3 : Node uge = nm->mkNode(Kind::BITVECTOR_UGE, s1, t1);
2288 : : Node imp =
2289 : 2 : nm->mkNode(Kind::IMPLIES, s1.eqNode(t1), tx.eqNode(n).notNode());
2290 : 1 : scl = nm->mkNode(Kind::AND, uge, imp);
2291 : : }
2292 : : else
2293 : : {
2294 : : /* s1 o x <= t (interpret t as t1 o tx)
2295 : : * with invertibility condition:
2296 : : * (bvule s1 t1) */
2297 : 1 : scl = nm->mkNode(Kind::BITVECTOR_ULE, s1, t1);
2298 : : }
2299 : : }
2300 : : else
2301 : : {
2302 [ + + ]: 2 : if (pol)
2303 : : {
2304 : : /* s1 o x o s2 > t (interpret t as t1 o tx o t2)
2305 : : * with invertibility condition:
2306 : : * (and
2307 : : * (bvuge s1 t1)
2308 : : * (=> (and (= s1 t1) (= tx ones)) (bvugt s2 t2)))
2309 : : * where
2310 : : * ones = ~0 with getSize(ones) = wx */
2311 : 2 : Node n = bv::utils::mkOnes(wx);
2312 : 3 : Node uge = nm->mkNode(Kind::BITVECTOR_UGE, s1, t1);
2313 : 3 : Node a = nm->mkNode(Kind::AND, s1.eqNode(t1), tx.eqNode(n));
2314 : : Node imp = nm->mkNode(
2315 : 2 : Kind::IMPLIES, a, nm->mkNode(Kind::BITVECTOR_UGT, s2, t2));
2316 : 1 : scl = nm->mkNode(Kind::AND, uge, imp);
2317 : : }
2318 : : else
2319 : : {
2320 : : /* s1 o x o s2 <= t (interpret t as t1 o tx o t2)
2321 : : * with invertibility condition:
2322 : : * (and
2323 : : * (bvule s1 t1)
2324 : : * (=> (and (= s1 t1) (= tx z)) (bvule s2 t2)))
2325 : : * where
2326 : : * z = 0 with getSize(z) = wx */
2327 : 2 : Node z = bv::utils::mkZero(wx);
2328 : 3 : Node ule = nm->mkNode(Kind::BITVECTOR_ULE, s1, t1);
2329 : 3 : Node a = nm->mkNode(Kind::AND, s1.eqNode(t1), tx.eqNode(z));
2330 : : Node imp = nm->mkNode(
2331 : 2 : Kind::IMPLIES, a, nm->mkNode(Kind::BITVECTOR_ULE, s2, t2));
2332 : 1 : scl = nm->mkNode(Kind::AND, ule, imp);
2333 : : }
2334 : : }
2335 : : }
2336 [ + + ]: 12 : else if (litk == Kind::BITVECTOR_SLT)
2337 : : {
2338 [ + + ]: 6 : if (s1.isNull())
2339 : : {
2340 [ + + ]: 2 : if (pol)
2341 : : {
2342 : : /* x o s2 < t (interpret t as tx o t2)
2343 : : * with invertibility condition:
2344 : : * (=> (= tx min) (bvult s2 t2))
2345 : : * where
2346 : : * min is the signed minimum value with getSize(min) = wx */
2347 : 2 : Node min = bv::utils::mkMinSigned(wx);
2348 : 2 : Node ult = nm->mkNode(Kind::BITVECTOR_ULT, s2, t2);
2349 : 1 : scl = nm->mkNode(Kind::IMPLIES, tx.eqNode(min), ult);
2350 : : }
2351 : : else
2352 : : {
2353 : : /* x o s2 >= t (interpret t as tx o t2)
2354 : : * (=> (= tx max) (bvuge s2 t2))
2355 : : * where
2356 : : * max is the signed maximum value with getSize(max) = wx */
2357 : 2 : Node max = bv::utils::mkMaxSigned(wx);
2358 : 2 : Node uge = nm->mkNode(Kind::BITVECTOR_UGE, s2, t2);
2359 : 1 : scl = nm->mkNode(Kind::IMPLIES, tx.eqNode(max), uge);
2360 : : }
2361 : : }
2362 [ + + ]: 4 : else if (s2.isNull())
2363 : : {
2364 [ + + ]: 2 : if (pol)
2365 : : {
2366 : : /* s1 o x < t (interpret t as t1 o tx)
2367 : : * with invertibility condition:
2368 : : * (and (bvsle s1 t1) (=> (= s1 t1) (distinct tx z)))
2369 : : * where
2370 : : * z = 0 with getSize(z) = wx */
2371 : 2 : Node z = bv::utils::mkZero(wx);
2372 : 3 : Node sle = nm->mkNode(Kind::BITVECTOR_SLE, s1, t1);
2373 : : Node imp =
2374 : 2 : nm->mkNode(Kind::IMPLIES, s1.eqNode(t1), tx.eqNode(z).notNode());
2375 : 1 : scl = nm->mkNode(Kind::AND, sle, imp);
2376 : : }
2377 : : else
2378 : : {
2379 : : /* s1 o x >= t (interpret t as t1 o tx)
2380 : : * with invertibility condition:
2381 : : * (bvsge s1 t1) */
2382 : 1 : scl = nm->mkNode(Kind::BITVECTOR_SGE, s1, t1);
2383 : : }
2384 : : }
2385 : : else
2386 : : {
2387 [ + + ]: 2 : if (pol)
2388 : : {
2389 : : /* s1 o x o s2 < t (interpret t as t1 o tx o t2)
2390 : : * with invertibility condition:
2391 : : * (and
2392 : : * (bvsle s1 t1)
2393 : : * (=> (and (= s1 t1) (= tx z)) (bvult s2 t2)))
2394 : : * where
2395 : : * z = 0 with getSize(z) = wx */
2396 : 2 : Node z = bv::utils::mkZero(wx);
2397 : 3 : Node sle = nm->mkNode(Kind::BITVECTOR_SLE, s1, t1);
2398 : 3 : Node a = nm->mkNode(Kind::AND, s1.eqNode(t1), tx.eqNode(z));
2399 : : Node imp = nm->mkNode(
2400 : 2 : Kind::IMPLIES, a, nm->mkNode(Kind::BITVECTOR_ULT, s2, t2));
2401 : 1 : scl = nm->mkNode(Kind::AND, sle, imp);
2402 : : }
2403 : : else
2404 : : {
2405 : : /* s1 o x o s2 >= t (interpret t as t1 o tx o t2)
2406 : : * with invertibility condition:
2407 : : * (and
2408 : : * (bvsge s1 t1)
2409 : : * (=> (and (= s1 t1) (= tx ones)) (bvuge s2 t2)))
2410 : : * where
2411 : : * ones = ~0 with getSize(ones) = wx */
2412 : 2 : Node n = bv::utils::mkOnes(wx);
2413 : 3 : Node sge = nm->mkNode(Kind::BITVECTOR_SGE, s1, t1);
2414 : 3 : Node a = nm->mkNode(Kind::AND, s1.eqNode(t1), tx.eqNode(n));
2415 : : Node imp = nm->mkNode(
2416 : 2 : Kind::IMPLIES, a, nm->mkNode(Kind::BITVECTOR_UGE, s2, t2));
2417 : 1 : scl = nm->mkNode(Kind::AND, sge, imp);
2418 : : }
2419 : : }
2420 : : }
2421 : : else
2422 : : {
2423 [ - + ][ - + ]: 6 : Assert(litk == Kind::BITVECTOR_SGT);
[ - - ]
2424 [ + + ]: 6 : if (s1.isNull())
2425 : : {
2426 [ + + ]: 2 : if (pol)
2427 : : {
2428 : : /* x o s2 > t (interpret t as tx o t2)
2429 : : * with invertibility condition:
2430 : : * (=> (= tx max) (bvugt s2 t2))
2431 : : * where
2432 : : * max is the signed maximum value with getSize(max) = wx */
2433 : 2 : Node max = bv::utils::mkMaxSigned(wx);
2434 : 2 : Node ugt = nm->mkNode(Kind::BITVECTOR_UGT, s2, t2);
2435 : 1 : scl = nm->mkNode(Kind::IMPLIES, tx.eqNode(max), ugt);
2436 : : }
2437 : : else
2438 : : {
2439 : : /* x o s2 <= t (interpret t as tx o t2)
2440 : : * with invertibility condition:
2441 : : * (=> (= tx min) (bvule s2 t2))
2442 : : * where
2443 : : * min is the signed minimum value with getSize(min) = wx */
2444 : 2 : Node min = bv::utils::mkMinSigned(wx);
2445 : 2 : Node ule = nm->mkNode(Kind::BITVECTOR_ULE, s2, t2);
2446 : 1 : scl = nm->mkNode(Kind::IMPLIES, tx.eqNode(min), ule);
2447 : : }
2448 : : }
2449 [ + + ]: 4 : else if (s2.isNull())
2450 : : {
2451 [ + + ]: 2 : if (pol)
2452 : : {
2453 : : /* s1 o x > t (interpret t as t1 o tx)
2454 : : * with invertibility condition:
2455 : : * (and (bvsge s1 t1) (=> (= s1 t1) (distinct tx ones)))
2456 : : * where
2457 : : * ones = ~0 with getSize(ones) = wx */
2458 : 2 : Node n = bv::utils::mkOnes(wx);
2459 : 3 : Node sge = nm->mkNode(Kind::BITVECTOR_SGE, s1, t1);
2460 : : Node imp =
2461 : 2 : nm->mkNode(Kind::IMPLIES, s1.eqNode(t1), tx.eqNode(n).notNode());
2462 : 1 : scl = nm->mkNode(Kind::AND, sge, imp);
2463 : : }
2464 : : else
2465 : : {
2466 : : /* s1 o x <= t (interpret t as t1 o tx)
2467 : : * with invertibility condition:
2468 : : * (bvsle s1 t1) */
2469 : 1 : scl = nm->mkNode(Kind::BITVECTOR_SLE, s1, t1);
2470 : : }
2471 : : }
2472 : : else
2473 : : {
2474 [ + + ]: 2 : if (pol)
2475 : : {
2476 : : /* s1 o x o s2 > t (interpret t as t1 o tx o t2)
2477 : : * with invertibility condition:
2478 : : * (and
2479 : : * (bvsge s1 t1)
2480 : : * (=> (and (= s1 t1) (= tx ones)) (bvugt s2 t2)))
2481 : : * where
2482 : : * ones = ~0 with getSize(ones) = wx */
2483 : 2 : Node n = bv::utils::mkOnes(wx);
2484 : 3 : Node sge = nm->mkNode(Kind::BITVECTOR_SGE, s1, t1);
2485 : 3 : Node a = nm->mkNode(Kind::AND, s1.eqNode(t1), tx.eqNode(n));
2486 : : Node imp = nm->mkNode(
2487 : 2 : Kind::IMPLIES, a, nm->mkNode(Kind::BITVECTOR_UGT, s2, t2));
2488 : 1 : scl = nm->mkNode(Kind::AND, sge, imp);
2489 : : }
2490 : : else
2491 : : {
2492 : : /* s1 o x o s2 <= t (interpret t as t1 o tx o t2)
2493 : : * with invertibility condition:
2494 : : * (and
2495 : : * (bvsle s1 t1)
2496 : : * (=> (and (= s1 t1) (= tx z)) (bvule s2 t2)))
2497 : : * where
2498 : : * z = 0 with getSize(z) = wx */
2499 : 2 : Node z = bv::utils::mkZero(wx);
2500 : 3 : Node sle = nm->mkNode(Kind::BITVECTOR_SLE, s1, t1);
2501 : 3 : Node a = nm->mkNode(Kind::AND, s1.eqNode(t1), tx.eqNode(z));
2502 : : Node imp = nm->mkNode(
2503 : 2 : Kind::IMPLIES, a, nm->mkNode(Kind::BITVECTOR_ULE, s2, t2));
2504 : 1 : scl = nm->mkNode(Kind::AND, sle, imp);
2505 : : }
2506 : : }
2507 : : }
2508 : 30 : scr = s1.isNull() ? x : bv::utils::mkConcat(s1, x);
2509 [ + + ]: 30 : if (!s2.isNull()) scr = bv::utils::mkConcat(scr, s2);
2510 : 30 : scr = nm->mkNode(litk, scr, t);
2511 [ + + ]: 60 : Node ic = nm->mkNode(Kind::IMPLIES, scl, pol ? scr : scr.notNode());
2512 [ + - ]: 30 : Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << ic << std::endl;
2513 : 60 : return ic;
2514 : : }
2515 : :
2516 : 39 : Node getICBvSext(bool pol, Kind litk, unsigned idx, Node x, Node sv_t, Node t)
2517 : : {
2518 [ + + ][ + + ]: 39 : Assert(litk == Kind::EQUAL || litk == Kind::BITVECTOR_ULT
[ + + ][ + + ]
[ - + ][ - + ]
[ - - ]
2519 : : || litk == Kind::BITVECTOR_SLT || litk == Kind::BITVECTOR_UGT
2520 : : || litk == Kind::BITVECTOR_SGT);
2521 : :
2522 : 39 : NodeManager* nm = NodeManager::currentNM();
2523 : 78 : Node scl;
2524 [ - + ][ - + ]: 39 : Assert(idx == 0);
[ - - ]
2525 : : (void)idx;
2526 : 39 : unsigned ws = bv::utils::getSignExtendAmount(sv_t);
2527 : 39 : unsigned w = bv::utils::getSize(t);
2528 : :
2529 [ + + ]: 39 : if (litk == Kind::EQUAL)
2530 : : {
2531 [ + + ]: 31 : if (pol)
2532 : : {
2533 : : /* x sext ws = t
2534 : : * with invertibility condition:
2535 : : * (or (= ((_ extract u l) t) z)
2536 : : * (= ((_ extract u l) t) ones))
2537 : : * where
2538 : : * u = w - 1
2539 : : * l = w - 1 - ws
2540 : : * z = 0 with getSize(z) = ws + 1
2541 : : * ones = ~0 with getSize(ones) = ws + 1 */
2542 : 60 : Node ext = bv::utils::mkExtract(t, w - 1, w - 1 - ws);
2543 : 60 : Node z = bv::utils::mkZero(ws + 1);
2544 : 30 : Node n = bv::utils::mkOnes(ws + 1);
2545 : 30 : scl = nm->mkNode(Kind::OR, ext.eqNode(z), ext.eqNode(n));
2546 : : }
2547 : : else
2548 : : {
2549 : : /* x sext ws != t
2550 : : * true (no invertibility condition) */
2551 : 1 : scl = nm->mkConst<bool>(true);
2552 : : }
2553 : : }
2554 [ + + ]: 8 : else if (litk == Kind::BITVECTOR_ULT)
2555 : : {
2556 [ + + ]: 2 : if (pol)
2557 : : {
2558 : : /* x sext ws < t
2559 : : * with invertibility condition:
2560 : : * (distinct t z)
2561 : : * where
2562 : : * z = 0 with getSize(z) = w */
2563 : 1 : Node z = bv::utils::mkZero(w);
2564 : 1 : scl = t.eqNode(z).notNode();
2565 : : }
2566 : : else
2567 : : {
2568 : : /* x sext ws >= t
2569 : : * true (no invertibility condition) */
2570 : 1 : scl = nm->mkConst<bool>(true);
2571 : : }
2572 : : }
2573 [ + + ]: 6 : else if (litk == Kind::BITVECTOR_UGT)
2574 : : {
2575 [ + + ]: 2 : if (pol)
2576 : : {
2577 : : /* x sext ws > t
2578 : : * with invertibility condition:
2579 : : * (distinct t ones)
2580 : : * where
2581 : : * ones = ~0 with getSize(ones) = w */
2582 : 1 : Node n = bv::utils::mkOnes(w);
2583 : 1 : scl = t.eqNode(n).notNode();
2584 : : }
2585 : : else
2586 : : {
2587 : : /* x sext ws <= t
2588 : : * true (no invertibility condition) */
2589 : 1 : scl = nm->mkConst<bool>(true);
2590 : : }
2591 : : }
2592 [ + + ]: 4 : else if (litk == Kind::BITVECTOR_SLT)
2593 : : {
2594 [ + + ]: 2 : if (pol)
2595 : : {
2596 : : /* x sext ws < t
2597 : : * with invertibility condition:
2598 : : * (bvslt ((_ sign_extend ws) min) t)
2599 : : * where
2600 : : * min is the signed minimum value with getSize(min) = w - ws */
2601 : 2 : Node min = bv::utils::mkMinSigned(w - ws);
2602 : 1 : Node ext = bv::utils::mkSignExtend(min, ws);
2603 : 1 : scl = nm->mkNode(Kind::BITVECTOR_SLT, ext, t);
2604 : : }
2605 : : else
2606 : : {
2607 : : /* x sext ws >= t
2608 : : * with invertibility condition (combination of sgt and eq):
2609 : : *
2610 : : * (or
2611 : : * (or (= ((_ extract u l) t) z) ; eq
2612 : : * (= ((_ extract u l) t) ones))
2613 : : * (bvslt t ((_ zero_extend ws) max))) ; sgt
2614 : : * where
2615 : : * u = w - 1
2616 : : * l = w - 1 - ws
2617 : : * z = 0 with getSize(z) = ws + 1
2618 : : * ones = ~0 with getSize(ones) = ws + 1
2619 : : * max is the signed maximum value with getSize(max) = w - ws */
2620 : 2 : Node ext1 = bv::utils::mkExtract(t, w - 1, w - 1 - ws);
2621 : 2 : Node z = bv::utils::mkZero(ws + 1);
2622 : 2 : Node n = bv::utils::mkOnes(ws + 1);
2623 : 3 : Node o1 = nm->mkNode(Kind::OR, ext1.eqNode(z), ext1.eqNode(n));
2624 : 2 : Node max = bv::utils::mkMaxSigned(w - ws);
2625 : 3 : Node ext2 = bv::utils::mkConcat(bv::utils::mkZero(ws), max);
2626 : 2 : Node o2 = nm->mkNode(Kind::BITVECTOR_SLT, t, ext2);
2627 : 1 : scl = nm->mkNode(Kind::OR, o1, o2);
2628 : : }
2629 : : }
2630 : : else
2631 : : {
2632 [ - + ][ - + ]: 2 : Assert(litk == Kind::BITVECTOR_SGT);
[ - - ]
2633 [ + + ]: 2 : if (pol)
2634 : : {
2635 : : /* x sext ws > t
2636 : : * with invertibility condition:
2637 : : * (bvslt t ((_ zero_extend ws) max))
2638 : : * where
2639 : : * max is the signed maximum value with getSize(max) = w - ws */
2640 : 2 : Node max = bv::utils::mkMaxSigned(w - ws);
2641 : 2 : Node ext = bv::utils::mkConcat(bv::utils::mkZero(ws), max);
2642 : 1 : scl = nm->mkNode(Kind::BITVECTOR_SLT, t, ext);
2643 : : }
2644 : : else
2645 : : {
2646 : : /* x sext ws <= t
2647 : : * with invertibility condition:
2648 : : * (bvsge t (bvnot ((_ zero_extend ws) max)))
2649 : : * where
2650 : : * max is the signed maximum value with getSize(max) = w - ws */
2651 : 2 : Node max = bv::utils::mkMaxSigned(w - ws);
2652 : 2 : Node ext = bv::utils::mkConcat(bv::utils::mkZero(ws), max);
2653 : 2 : scl = nm->mkNode(
2654 : 3 : Kind::BITVECTOR_SGE, t, nm->mkNode(Kind::BITVECTOR_NOT, ext));
2655 : : }
2656 : : }
2657 : 117 : Node scr = nm->mkNode(litk, bv::utils::mkSignExtend(x, ws), t);
2658 [ + + ]: 78 : Node ic = nm->mkNode(Kind::IMPLIES, scl, pol ? scr : scr.notNode());
2659 [ + - ]: 78 : Trace("bv-invert") << "Add SC_" << Kind::BITVECTOR_SIGN_EXTEND << "(" << x
2660 : 39 : << "): " << ic << std::endl;
2661 : 78 : return ic;
2662 : : }
2663 : :
2664 : : } // namespace utils
2665 : : } // namespace quantifiers
2666 : : } // namespace theory
2667 : : } // namespace cvc5::internal
|
