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