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