GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/bv_inverter_utils.cpp Lines: 811 820 98.9 %
Date: 2021-03-22 Branches: 2608 5352 48.7 %

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