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