GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/theory_bv_rewrite_rules_simplification.h Lines: 669 747 89.6 %
Date: 2021-03-23 Branches: 1968 4290 45.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_bv_rewrite_rules_simplification.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Liana Hadarean, 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 [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#include "cvc4_private.h"
19
20
#pragma once
21
22
#include "options/bv_options.h"
23
#include "theory/bv/theory_bv_rewrite_rules.h"
24
#include "theory/bv/theory_bv_utils.h"
25
#include "theory/rewriter.h"
26
27
namespace CVC4 {
28
namespace theory {
29
namespace bv {
30
31
/* -------------------------------------------------------------------------- */
32
33
/**
34
 * BitOfConst
35
 */
36
template <>
37
555154
inline bool RewriteRule<BitOfConst>::applies(TNode node)
38
{
39
555154
  return node.getKind() == kind::BITVECTOR_BITOF && node[0].isConst();
40
}
41
42
template <>
43
19
inline Node RewriteRule<BitOfConst>::apply(TNode node)
44
{
45
19
  size_t pos = node.getOperator().getConst<BitVectorBitOf>().d_bitIndex;
46
19
  return utils::getBit(node[0], pos) ? utils::mkTrue() : utils::mkFalse();
47
}
48
49
/* -------------------------------------------------------------------------- */
50
51
/**
52
 * BvIteConstCond
53
 *
54
 * BITVECTOR_ITE with constant condition
55
 */
56
template <>
57
21338
inline bool RewriteRule<BvIteConstCond>::applies(TNode node)
58
{
59
21338
  return (node.getKind() == kind::BITVECTOR_ITE && node[0].isConst());
60
}
61
62
template <>
63
384
inline Node RewriteRule<BvIteConstCond>::apply(TNode node)
64
{
65
768
  Debug("bv-rewrite") << "RewriteRule<BvIteConstCond>(" << node << ")"
66
384
                      << std::endl;
67
384
  return utils::isZero(node[0]) ? node[2] : node[1];
68
}
69
70
/* -------------------------------------------------------------------------- */
71
72
/**
73
 * BvIteEqualChildren
74
 *
75
 * BITVECTOR_ITE with term_then = term_else
76
 */
77
template <>
78
21359
inline bool RewriteRule<BvIteEqualChildren>::applies(TNode node)
79
{
80
21359
  return (node.getKind() == kind::BITVECTOR_ITE && node[1] == node[2]);
81
}
82
83
template <>
84
405
inline Node RewriteRule<BvIteEqualChildren>::apply(TNode node)
85
{
86
810
  Debug("bv-rewrite") << "RewriteRule<BvIteEqualChildren>(" << node << ")"
87
405
                      << std::endl;
88
405
  return node[1];
89
}
90
91
/* -------------------------------------------------------------------------- */
92
93
/**
94
 * BvIteConstChildren
95
 *
96
 * BITVECTOR_ITE with constant children of size one
97
 */
98
template <>
99
19419
inline bool RewriteRule<BvIteConstChildren>::applies(TNode node)
100
{
101
19419
  return (node.getKind() == kind::BITVECTOR_ITE
102
38838
          && utils::getSize(node[1]) == 1
103
65900
          && node[1].isConst() && node[2].isConst());
104
}
105
106
template <>
107
203
inline Node RewriteRule<BvIteConstChildren>::apply(TNode node)
108
{
109
406
  Debug("bv-rewrite") << "RewriteRule<BvIteConstChildren>(" << node << ")"
110
203
                      << std::endl;
111
203
  if (utils::isOne(node[1]) && utils::isZero(node[2]))
112
  {
113
179
    return node[0];
114
  }
115
24
  Assert(utils::isZero(node[1]) && utils::isOne(node[2]));
116
24
  return NodeManager::currentNM()->mkNode(kind::BITVECTOR_NOT, node[0]);
117
}
118
119
/* -------------------------------------------------------------------------- */
120
121
/**
122
 * BvIteEqualCond
123
 *
124
 * Nested BITVECTOR_ITE with cond_outer == cond_inner
125
 *
126
 * c0 ? (c0 ? t0 : e0) : e1              ->  c0 ? t0 : e1
127
 * c0 ? t0             : (c0 ? t1 : e1)  ->  c0 ? t0 : e1
128
 * c0 ? (c0 ? t0 : e0) : (c0 ? t1 : e1)  ->  c0 ? t0 : e1
129
 */
130
template <>
131
19223
inline bool RewriteRule<BvIteEqualCond>::applies(TNode node)
132
{
133
  return (
134
19223
      node.getKind() == kind::BITVECTOR_ITE
135
57683
      && ((node[1].getKind() == kind::BITVECTOR_ITE && node[0] == node[1][0])
136
38231
          || (node[2].getKind() == kind::BITVECTOR_ITE
137
46138
              && node[0] == node[2][0])));
138
}
139
140
template <>
141
7
inline Node RewriteRule<BvIteEqualCond>::apply(TNode node)
142
{
143
14
  Debug("bv-rewrite") << "RewriteRule<BvIteEqualCond>(" << node << ")"
144
7
                      << std::endl;
145
28
  Node t0 = node[1].getKind() == kind::BITVECTOR_ITE && node[0] == node[1][0]
146
35
                ? node[1][1]
147
14
                : node[1];
148
25
  Node e1 = node[2].getKind() == kind::BITVECTOR_ITE && node[0] == node[2][0]
149
28
                ? node[2][2]
150
14
                : node[2];
151
14
  return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ITE, node[0], t0, e1);
152
}
153
154
/* -------------------------------------------------------------------------- */
155
156
/**
157
 * BvIteMergeThenIf
158
 *
159
 * Nested BITVECTOR_ITE of the form
160
 *   c0 ? (c1 ? t1 : e1) : t1  ->  c0 AND NOT(c1) ? e1 : t1
161
 */
162
template <>
163
19042
inline bool RewriteRule<BvIteMergeThenIf>::applies(TNode node)
164
{
165
19042
  return (node.getKind() == kind::BITVECTOR_ITE
166
38084
          && node[1].getKind() == kind::BITVECTOR_ITE
167
59223
          && node[1][1] == node[2]);
168
}
169
170
template <>
171
36
inline Node RewriteRule<BvIteMergeThenIf>::apply(TNode node)
172
{
173
72
  Debug("bv-rewrite") << "RewriteRule<BvIteMergeThenIf>(" << node << ")"
174
36
                      << std::endl;
175
36
  NodeManager* nm = NodeManager::currentNM();
176
36
  Assert(node[1].getKind() == kind::BITVECTOR_ITE);
177
  Node cond = nm->mkNode(kind::BITVECTOR_AND,
178
                         node[0],
179
72
                         nm->mkNode(kind::BITVECTOR_NOT, node[1][0]));
180
72
  return nm->mkNode(kind::BITVECTOR_ITE, cond, node[1][2], node[2]);
181
}
182
183
/* -------------------------------------------------------------------------- */
184
185
/**
186
 * BvIteMergeElseIf
187
 *
188
 * Nested BITVECTOR_ITE of the form
189
 *   c0 ? (c1 ? t1 : e1) : e1  ->  c0 AND c1 ? t1 : e1
190
 */
191
template <>
192
19022
inline bool RewriteRule<BvIteMergeElseIf>::applies(TNode node)
193
{
194
19022
  return (node.getKind() == kind::BITVECTOR_ITE
195
38044
          && node[1].getKind() == kind::BITVECTOR_ITE
196
59117
          && node[1][2] == node[2]);
197
}
198
199
template <>
200
16
inline Node RewriteRule<BvIteMergeElseIf>::apply(TNode node)
201
{
202
32
  Debug("bv-rewrite") << "RewriteRule<BvIteMergeElseIf>(" << node << ")"
203
16
                      << std::endl;
204
16
  NodeManager* nm = NodeManager::currentNM();
205
16
  Assert(node[1].getKind() == kind::BITVECTOR_ITE);
206
32
  Node cond = nm->mkNode(kind::BITVECTOR_AND, node[0], node[1][0]);
207
32
  return nm->mkNode(kind::BITVECTOR_ITE, cond, node[1][1], node[2]);
208
}
209
210
/* -------------------------------------------------------------------------- */
211
212
/**
213
 * BvIteMergeThenElse
214
 *
215
 * Nested BITVECTOR_ITE of the form
216
 *   c0 ? t0 : (c1 ? t0 : e1)  ->  NOT(c0) AND NOT(c1) ? e1 : t0
217
 */
218
template <>
219
19063
inline bool RewriteRule<BvIteMergeThenElse>::applies(TNode node)
220
{
221
19063
  return (node.getKind() == kind::BITVECTOR_ITE
222
38126
          && node[2].getKind() == kind::BITVECTOR_ITE
223
64938
          && node[1] == node[2][1]);
224
}
225
226
template <>
227
57
inline Node RewriteRule<BvIteMergeThenElse>::apply(TNode node)
228
{
229
114
  Debug("bv-rewrite") << "RewriteRule<BvIteMergeThenElse>(" << node << ")"
230
57
                      << std::endl;
231
57
  NodeManager* nm = NodeManager::currentNM();
232
57
  Assert(node[2].getKind() == kind::BITVECTOR_ITE);
233
  Node cond = nm->mkNode(kind::BITVECTOR_AND,
234
114
                         nm->mkNode(kind::BITVECTOR_NOT, node[0]),
235
228
                         nm->mkNode(kind::BITVECTOR_NOT, node[2][0]));
236
114
  return nm->mkNode(kind::BITVECTOR_ITE, cond, node[2][2], node[1]);
237
}
238
239
/* -------------------------------------------------------------------------- */
240
241
/**
242
 * BvIteMergeElseElse
243
 *
244
 * Nested BITVECTOR_ITE of the form
245
 *   c0 ? t0 : (c1 ? t1 : t0)  ->  NOT(c0) AND c1 ? t1 : t0
246
 */
247
template <>
248
19025
inline bool RewriteRule<BvIteMergeElseElse>::applies(TNode node)
249
{
250
19025
  return (node.getKind() == kind::BITVECTOR_ITE
251
38050
          && node[2].getKind() == kind::BITVECTOR_ITE
252
64747
          && node[1] == node[2][2]);
253
}
254
255
template <>
256
19
inline Node RewriteRule<BvIteMergeElseElse>::apply(TNode node)
257
{
258
38
  Debug("bv-rewrite") << "RewriteRule<BvIteMergeElseElse>(" << node << ")"
259
19
                      << std::endl;
260
19
  NodeManager* nm = NodeManager::currentNM();
261
19
  Assert(node[2].getKind() == kind::BITVECTOR_ITE);
262
  Node cond = nm->mkNode(kind::BITVECTOR_AND,
263
38
                         nm->mkNode(kind::BITVECTOR_NOT, node[0]),
264
76
                         node[2][0]);
265
38
  return nm->mkNode(kind::BITVECTOR_ITE, cond, node[2][1], node[1]);
266
}
267
268
/* -------------------------------------------------------------------------- */
269
270
/**
271
 * BvComp
272
 *
273
 * BITVECTOR_COMP of children of size 1 with one constant child
274
 */
275
template <>
276
167733
inline bool RewriteRule<BvComp>::applies(TNode node)
277
{
278
167733
  return (node.getKind() == kind::BITVECTOR_COMP
279
204347
          && utils::getSize(node[0]) == 1
280
507815
          && (node[0].isConst() || node[1].isConst()));
281
}
282
283
template <>
284
1303
inline Node RewriteRule<BvComp>::apply(TNode node)
285
{
286
1303
  Debug("bv-rewrite") << "RewriteRule<BvComp>(" << node << ")" << std::endl;
287
1303
  NodeManager* nm = NodeManager::currentNM();
288
1303
  if (node[0].isConst())
289
  {
290
710
    return utils::isZero(node[0]) ? nm->mkNode(kind::BITVECTOR_NOT, node[1])
291
355
                                  : Node(node[1]);
292
  }
293
1896
  return utils::isZero(node[1]) ? nm->mkNode(kind::BITVECTOR_NOT, node[0])
294
948
                                : Node(node[0]);
295
}
296
297
/* -------------------------------------------------------------------------- */
298
299
/**
300
 * ShlByConst
301
 *
302
 * Left Shift by constant amount
303
 */
304
template<> inline
305
44308
bool RewriteRule<ShlByConst>::applies(TNode node) {
306
  // if the shift amount is constant
307
132924
  return (node.getKind() == kind::BITVECTOR_SHL &&
308
132924
          node[1].getKind() == kind::CONST_BITVECTOR);
309
}
310
311
template<> inline
312
17076
Node RewriteRule<ShlByConst>::apply(TNode node) {
313
17076
  Debug("bv-rewrite") << "RewriteRule<ShlByConst>(" << node << ")" << std::endl;
314
34152
  Integer amount = node[1].getConst<BitVector>().toInteger();
315
17076
  if (amount == 0) {
316
3191
    return node[0];
317
  }
318
27770
  Node a = node[0];
319
13885
  uint32_t size = utils::getSize(a);
320
321
322
13885
  if (amount >= Integer(size)) {
323
    // if we are shifting more than the length of the bitvector return 0
324
10239
    return utils::mkZero(size);
325
  }
326
327
  // make sure we do not lose information casting
328
3646
  Assert(amount < Integer(1).multiplyByPow2(32));
329
330
3646
  uint32_t uint32_amount = amount.toUnsignedInt();
331
332
7292
  Node left = utils::mkExtract(a, size - 1 - uint32_amount, 0);
333
7292
  Node right = utils::mkZero(uint32_amount);
334
3646
  return utils::mkConcat(left, right);
335
}
336
337
/* -------------------------------------------------------------------------- */
338
339
/**
340
 * LshrByConst
341
 *
342
 * Right Logical Shift by constant amount
343
 */
344
345
template<> inline
346
52390
bool RewriteRule<LshrByConst>::applies(TNode node) {
347
  // if the shift amount is constant
348
157170
  return (node.getKind() == kind::BITVECTOR_LSHR &&
349
157170
          node[1].getKind() == kind::CONST_BITVECTOR);
350
}
351
352
template<> inline
353
18995
Node RewriteRule<LshrByConst>::apply(TNode node) {
354
18995
  Debug("bv-rewrite") << "RewriteRule<LshrByConst>(" << node << ")" << std::endl;
355
37990
  Integer amount = node[1].getConst<BitVector>().toInteger();
356
18995
  if (amount == 0) {
357
3370
    return node[0];
358
  }
359
360
31250
  Node a = node[0];
361
15625
  uint32_t size = utils::getSize(a);
362
363
364
15625
  if (amount >= Integer(size)) {
365
    // if we are shifting more than the length of the bitvector return 0
366
12490
    return utils::mkZero(size);
367
  }
368
369
  // make sure we do not lose information casting
370
3135
  Assert(amount < Integer(1).multiplyByPow2(32));
371
372
3135
  uint32_t uint32_amount = amount.toUnsignedInt();
373
6270
  Node right = utils::mkExtract(a, size - 1, uint32_amount);
374
6270
  Node left = utils::mkZero(uint32_amount);
375
3135
  return utils::mkConcat(left, right);
376
}
377
378
/* -------------------------------------------------------------------------- */
379
380
/**
381
 * AshrByConst
382
 *
383
 * Right Arithmetic Shift by constant amount
384
 */
385
386
template<> inline
387
7522
bool RewriteRule<AshrByConst>::applies(TNode node) {
388
  // if the shift amount is constant
389
22566
  return (node.getKind() == kind::BITVECTOR_ASHR &&
390
22566
          node[1].getKind() == kind::CONST_BITVECTOR);
391
}
392
393
template<> inline
394
693
Node RewriteRule<AshrByConst>::apply(TNode node) {
395
693
  Debug("bv-rewrite") << "RewriteRule<AshrByConst>(" << node << ")" << std::endl;
396
1386
  Integer amount = node[1].getConst<BitVector>().toInteger();
397
693
  if (amount == 0) {
398
110
    return node[0];
399
  }
400
401
1166
  Node a = node[0];
402
583
  uint32_t size = utils::getSize(a);
403
1166
  Node sign_bit = utils::mkExtract(a, size-1, size-1);
404
405
583
  if (amount >= Integer(size)) {
406
    // if we are shifting more than the length of the bitvector return n repetitions
407
    // of the first bit
408
161
    return utils::mkConcat(sign_bit, size);
409
  }
410
411
  // make sure we do not lose information casting
412
422
  Assert(amount < Integer(1).multiplyByPow2(32));
413
414
422
  uint32_t uint32_amount = amount.toUnsignedInt();
415
422
  if (uint32_amount == 0) {
416
    return a;
417
  }
418
419
844
  Node left = utils::mkConcat(sign_bit, uint32_amount);
420
844
  Node right = utils::mkExtract(a, size - 1, uint32_amount);
421
422
  return utils::mkConcat(left, right);
422
}
423
424
/* -------------------------------------------------------------------------- */
425
426
/**
427
 * BitwiseIdemp
428
 *
429
 * (a bvand a) ==> a
430
 * (a bvor a)  ==> a
431
 */
432
433
template<> inline
434
bool RewriteRule<BitwiseIdemp>::applies(TNode node) {
435
  Unreachable();
436
  return ((node.getKind() == kind::BITVECTOR_AND ||
437
           node.getKind() == kind::BITVECTOR_OR) &&
438
          node.getNumChildren() == 2 &&
439
          node[0] == node[1]);
440
}
441
442
template<> inline
443
Node RewriteRule<BitwiseIdemp>::apply(TNode node) {
444
  Unreachable();
445
  Debug("bv-rewrite") << "RewriteRule<BitwiseIdemp>(" << node << ")" << std::endl;
446
  return node[0];
447
}
448
449
/* -------------------------------------------------------------------------- */
450
451
/**
452
 * AndZero
453
 *
454
 * (a bvand 0) ==> 0
455
 */
456
457
template<> inline
458
bool RewriteRule<AndZero>::applies(TNode node) {
459
  Unreachable();
460
  unsigned size = utils::getSize(node);
461
  return (node.getKind() == kind::BITVECTOR_AND  &&
462
          node.getNumChildren() == 2 &&
463
          (node[0] == utils::mkConst(size, 0) ||
464
           node[1] == utils::mkConst(size, 0)));
465
}
466
467
template<> inline
468
Node RewriteRule<AndZero>::apply(TNode node) {
469
  Unreachable();
470
  Debug("bv-rewrite") << "RewriteRule<AndZero>(" << node << ")" << std::endl;
471
  return utils::mkConst(utils::getSize(node), 0);
472
}
473
474
/* -------------------------------------------------------------------------- */
475
476
/**
477
 * AndOne
478
 *
479
 * (a bvand 1) ==> a
480
 */
481
482
template<> inline
483
bool RewriteRule<AndOne>::applies(TNode node) {
484
  Unreachable();
485
  unsigned size = utils::getSize(node);
486
  Node ones = utils::mkOnes(size);
487
  return (node.getKind() == kind::BITVECTOR_AND  &&
488
          node.getNumChildren() == 2 &&
489
          (node[0] == ones ||
490
           node[1] == ones));
491
}
492
493
template<> inline
494
Node RewriteRule<AndOne>::apply(TNode node) {
495
  Unreachable();
496
  Debug("bv-rewrite") << "RewriteRule<AndOne>(" << node << ")" << std::endl;
497
  unsigned size = utils::getSize(node);
498
499
  if (node[0] == utils::mkOnes(size)) {
500
    return node[1];
501
  } else {
502
    Assert(node[1] == utils::mkOnes(size));
503
    return node[0];
504
  }
505
}
506
507
/* -------------------------------------------------------------------------- */
508
509
/**
510
 * AndOrXorConcatPullUp
511
 *
512
 * Match:       x_m <op> concat(y_my, <const>_n, z_mz)
513
 *              <const>_n in { 0_n, 1_n, ~0_n }
514
 *
515
 * Rewrites to: concat(x[m-1:m-my]  <op> y,
516
 *                     x[m-my-1:mz] <op> <const>_n,
517
 *                     x[mz-1:0]    <op> z)
518
 */
519
520
template <>
521
357307
inline bool RewriteRule<AndOrXorConcatPullUp>::applies(TNode node)
522
{
523
714614
  if (node.getKind() != kind::BITVECTOR_AND
524
259053
      && node.getKind() != kind::BITVECTOR_OR
525
492004
      && node.getKind() != kind::BITVECTOR_XOR)
526
  {
527
124832
    return false;
528
  }
529
530
464950
  TNode n;
531
532
1024921
  for (const TNode& c : node)
533
  {
534
801473
    if (c.getKind() == kind::BITVECTOR_CONCAT)
535
    {
536
41703
      for (const TNode& cc : c)
537
      {
538
38679
        if (cc.isConst())
539
        {
540
6003
          n = cc;
541
6003
          break;
542
        }
543
      }
544
9027
      break;
545
    }
546
  }
547
232475
  if (n.isNull()) return false;
548
6003
  return utils::isZero(n) || utils::isOne(n) || utils::isOnes(n);
549
}
550
551
template <>
552
2969
inline Node RewriteRule<AndOrXorConcatPullUp>::apply(TNode node)
553
{
554
5938
  Debug("bv-rewrite") << "RewriteRule<AndOrXorConcatPullUp>(" << node << ")"
555
2969
                      << std::endl;
556
  uint32_t m, my, mz;
557
  size_t nc;
558
2969
  Kind kind = node.getKind();
559
5938
  TNode concat;
560
5938
  Node x, y, z, c;
561
5938
  NodeBuilder<> xb(kind);
562
5938
  NodeBuilder<> yb(kind::BITVECTOR_CONCAT);
563
5938
  NodeBuilder<> zb(kind::BITVECTOR_CONCAT);
564
5938
  NodeBuilder<> res(kind::BITVECTOR_CONCAT);
565
2969
  NodeManager* nm = NodeManager::currentNM();
566
567
9086
  for (const TNode& child : node)
568
  {
569
6117
    if (concat.isNull() && child.getKind() == kind::BITVECTOR_CONCAT)
570
    {
571
2969
      concat = child;
572
    }
573
    else
574
    {
575
3148
      xb << child;
576
    }
577
  }
578
2969
  x = xb.getNumChildren() > 1 ? xb.constructNode() : xb[0];
579
580
10368
  for (const TNode& child : concat)
581
  {
582
7399
    if (c.isNull())
583
    {
584
6136
      if (utils::isZero(child) || utils::isOne(child) || utils::isOnes(child))
585
      {
586
2969
        c = child;
587
      }
588
      else
589
      {
590
3167
        yb << child;
591
      }
592
    }
593
    else
594
    {
595
1263
      zb << child;
596
    }
597
  }
598
2969
  Assert(!c.isNull());
599
2969
  Assert(yb.getNumChildren() || zb.getNumChildren());
600
601
2969
  if ((nc = yb.getNumChildren()) > 0)
602
  {
603
1820
    y = nc > 1 ? yb.constructNode() : yb[0];
604
  }
605
2969
  if ((nc = zb.getNumChildren()) > 0)
606
  {
607
1157
    z = nc > 1 ? zb.constructNode() : zb[0];
608
  }
609
2969
  m = utils::getSize(x);
610
#ifdef CVC4_ASSERTIONS
611
2969
  uint32_t n = utils::getSize(c);
612
#endif
613
2969
  my = y.isNull() ? 0 : utils::getSize(y);
614
2969
  mz = z.isNull() ? 0 : utils::getSize(z);
615
2969
  Assert(mz == m - my - n);
616
2969
  Assert(my || mz);
617
618
2969
  if (my)
619
  {
620
1820
    res << nm->mkNode(kind, utils::mkExtract(x, m - 1, m - my), y);
621
  }
622
623
2969
  res << nm->mkNode(kind, utils::mkExtract(x, m - my - 1, mz), c);
624
625
2969
  if (mz)
626
  {
627
1157
    res << nm->mkNode(kind, utils::mkExtract(x, mz - 1, 0), z);
628
  }
629
630
5938
  return res;
631
}
632
633
/* -------------------------------------------------------------------------- */
634
635
/**
636
 * OrZero
637
 *
638
 * (a bvor 0) ==> a
639
 */
640
641
template<> inline
642
bool RewriteRule<OrZero>::applies(TNode node) {
643
  Unreachable();
644
  unsigned size = utils::getSize(node);
645
  return (node.getKind() == kind::BITVECTOR_OR  &&
646
          node.getNumChildren() == 2 &&
647
          (node[0] == utils::mkConst(size, 0) ||
648
           node[1] == utils::mkConst(size, 0)));
649
}
650
651
template<> inline
652
Node RewriteRule<OrZero>::apply(TNode node) {
653
  Unreachable();
654
  Debug("bv-rewrite") << "RewriteRule<OrZero>(" << node << ")" << std::endl;
655
656
  unsigned size = utils::getSize(node);
657
  if (node[0] == utils::mkConst(size, 0)) {
658
    return node[1];
659
  } else {
660
    Assert(node[1] == utils::mkConst(size, 0));
661
    return node[0];
662
  }
663
}
664
665
/* -------------------------------------------------------------------------- */
666
667
/**
668
 * OrOne
669
 *
670
 * (a bvor 1) ==> 1
671
 */
672
673
template<> inline
674
bool RewriteRule<OrOne>::applies(TNode node) {
675
  Unreachable();
676
  unsigned size = utils::getSize(node);
677
  Node ones = utils::mkOnes(size);
678
  return (node.getKind() == kind::BITVECTOR_OR  &&
679
          node.getNumChildren() == 2 &&
680
          (node[0] == ones ||
681
           node[1] == ones));
682
}
683
684
template<> inline
685
Node RewriteRule<OrOne>::apply(TNode node) {
686
  Unreachable();
687
  Debug("bv-rewrite") << "RewriteRule<OrOne>(" << node << ")" << std::endl;
688
  return utils::mkOnes(utils::getSize(node));
689
}
690
691
/* -------------------------------------------------------------------------- */
692
693
/**
694
 * XorDuplicate
695
 *
696
 * (a bvxor a) ==> 0
697
 */
698
699
template<> inline
700
bool RewriteRule<XorDuplicate>::applies(TNode node) {
701
  Unreachable();
702
  return (node.getKind() == kind::BITVECTOR_XOR &&
703
          node.getNumChildren() == 2 &&
704
          node[0] == node[1]);
705
}
706
707
template<> inline
708
Node RewriteRule<XorDuplicate>::apply(TNode node) {
709
  Unreachable();
710
  Debug("bv-rewrite") << "RewriteRule<XorDuplicate>(" << node << ")" << std::endl;
711
  return utils::mkZero(utils::getSize(node));
712
}
713
714
/* -------------------------------------------------------------------------- */
715
716
/**
717
 * XorOne
718
 *
719
 * (a bvxor 1) ==> ~a
720
 */
721
722
template<> inline
723
6326
bool RewriteRule<XorOne>::applies(TNode node) {
724
6326
  if (node.getKind() != kind::BITVECTOR_XOR) {
725
1283
    return false;
726
  }
727
10086
  Node ones = utils::mkOnes(utils::getSize(node));
728
13553
  for (unsigned i = 0; i < node.getNumChildren(); ++i) {
729
9390
    if (node[i] == ones) {
730
880
      return true;
731
    }
732
  }
733
4163
  return false;
734
}
735
736
template <>
737
440
inline Node RewriteRule<XorOne>::apply(TNode node)
738
{
739
440
  Debug("bv-rewrite") << "RewriteRule<XorOne>(" << node << ")" << std::endl;
740
440
  NodeManager *nm = NodeManager::currentNM();
741
880
  Node ones = utils::mkOnes(utils::getSize(node));
742
880
  std::vector<Node> children;
743
440
  bool found_ones = false;
744
  // XorSimplify should have been called before
745
1334
  for (unsigned i = 0; i < node.getNumChildren(); ++i)
746
  {
747
894
    if (node[i] == ones)
748
    {
749
      // make sure only ones occurs only once
750
440
      found_ones = !found_ones;
751
    }
752
    else
753
    {
754
454
      children.push_back(node[i]);
755
    }
756
  }
757
758
440
  Node result = utils::mkNaryNode(kind::BITVECTOR_XOR, children);
759
440
  if (found_ones)
760
  {
761
440
    result = nm->mkNode(kind::BITVECTOR_NOT, result);
762
  }
763
880
  return result;
764
}
765
766
/* -------------------------------------------------------------------------- */
767
768
/**
769
 * XorZero
770
 *
771
 * (a bvxor 0) ==> a
772
 */
773
774
template<> inline
775
12020
bool RewriteRule<XorZero>::applies(TNode node) {
776
12020
  if (node.getKind() != kind::BITVECTOR_XOR) {
777
637
    return false;
778
  }
779
22766
  Node zero = utils::mkConst(utils::getSize(node), 0);
780
30804
  for (unsigned i = 0; i < node.getNumChildren(); ++i) {
781
21265
    if (node[i] == zero) {
782
1844
      return true;
783
    }
784
  }
785
9539
  return false;
786
}
787
788
template <>
789
922
inline Node RewriteRule<XorZero>::apply(TNode node)
790
{
791
922
  Debug("bv-rewrite") << "RewriteRule<XorZero>(" << node << ")" << std::endl;
792
1844
  std::vector<Node> children;
793
1844
  Node zero = utils::mkConst(utils::getSize(node), 0);
794
795
  // XorSimplify should have been called before
796
2775
  for (unsigned i = 0; i < node.getNumChildren(); ++i)
797
  {
798
1853
    if (node[i] != zero)
799
    {
800
931
      children.push_back(node[i]);
801
    }
802
  }
803
922
  Node res = utils::mkNaryNode(kind::BITVECTOR_XOR, children);
804
1844
  return res;
805
}
806
807
/* -------------------------------------------------------------------------- */
808
809
/**
810
 * BitwiseNotAnd
811
 *
812
 * (a bvand (~ a)) ==> 0
813
 */
814
815
template<> inline
816
bool RewriteRule<BitwiseNotAnd>::applies(TNode node) {
817
  Unreachable();
818
  return (node.getKind() == kind::BITVECTOR_AND &&
819
          node.getNumChildren() == 2 &&
820
          ((node[0].getKind() == kind::BITVECTOR_NOT && node[0][0] == node[1]) ||
821
           (node[1].getKind() == kind::BITVECTOR_NOT && node[1][0] == node[0])));
822
}
823
824
template<> inline
825
Node RewriteRule<BitwiseNotAnd>::apply(TNode node) {
826
  Unreachable();
827
  Debug("bv-rewrite") << "RewriteRule<BitwiseNegAnd>(" << node << ")" << std::endl;
828
  return utils::mkZero(utils::getSize(node));
829
}
830
831
/* -------------------------------------------------------------------------- */
832
833
/**
834
 * BitwiseNegOr
835
 *
836
 * (a bvor (~ a)) ==> 1
837
 */
838
839
template<> inline
840
bool RewriteRule<BitwiseNotOr>::applies(TNode node) {
841
  Unreachable();
842
  return (node.getKind() == kind::BITVECTOR_OR &&
843
          node.getNumChildren() == 2 &&
844
          ((node[0].getKind() == kind::BITVECTOR_NOT && node[0][0] == node[1]) ||
845
           (node[1].getKind() == kind::BITVECTOR_NOT && node[1][0] == node[0])));
846
}
847
848
template<> inline
849
Node RewriteRule<BitwiseNotOr>::apply(TNode node) {
850
  Unreachable();
851
  Debug("bv-rewrite") << "RewriteRule<BitwiseNotOr>(" << node << ")" << std::endl;
852
  uint32_t size = utils::getSize(node);
853
  return utils::mkOnes(size);
854
}
855
856
/* -------------------------------------------------------------------------- */
857
858
/**
859
 * XorNot
860
 *
861
 * ((~ a) bvxor (~ b)) ==> (a bvxor b)
862
 */
863
864
template<> inline
865
bool RewriteRule<XorNot>::applies(TNode node) {
866
  Unreachable();
867
}
868
869
template <>
870
inline Node RewriteRule<XorNot>::apply(TNode node)
871
{
872
  Unreachable();
873
  Debug("bv-rewrite") << "RewriteRule<XorNot>(" << node << ")" << std::endl;
874
  Node a = node[0][0];
875
  Node b = node[1][0];
876
  return NodeManager::currentNM()->mkNode(kind::BITVECTOR_XOR, a, b);
877
}
878
879
/* -------------------------------------------------------------------------- */
880
881
/**
882
 * NotXor
883
 *
884
 * ~(a bvxor b) ==> (~ a bvxor b)
885
 */
886
887
template<> inline
888
bool RewriteRule<NotXor>::applies(TNode node) {
889
  return (node.getKind() == kind::BITVECTOR_NOT &&
890
          node[0].getKind() == kind::BITVECTOR_XOR);
891
}
892
893
template <>
894
inline Node RewriteRule<NotXor>::apply(TNode node)
895
{
896
  Debug("bv-rewrite") << "RewriteRule<NotXor>(" << node << ")" << std::endl;
897
  std::vector<Node> children;
898
  TNode::iterator child_it = node[0].begin();
899
  children.push_back(
900
      NodeManager::currentNM()->mkNode(kind::BITVECTOR_NOT, *child_it));
901
  for (++child_it; child_it != node[0].end(); ++child_it)
902
  {
903
    children.push_back(*child_it);
904
  }
905
  return utils::mkSortedNode(kind::BITVECTOR_XOR, children);
906
}
907
908
/* -------------------------------------------------------------------------- */
909
910
/**
911
 * NotIdemp
912
 *
913
 * ~ (~ a) ==> a
914
 */
915
916
template<> inline
917
122983
bool RewriteRule<NotIdemp>::applies(TNode node) {
918
307989
  return (node.getKind() == kind::BITVECTOR_NOT &&
919
307989
          node[0].getKind() == kind::BITVECTOR_NOT);
920
}
921
922
template<> inline
923
461
Node RewriteRule<NotIdemp>::apply(TNode node) {
924
461
  Debug("bv-rewrite") << "RewriteRule<NotIdemp>(" << node << ")" << std::endl;
925
461
  return node[0][0];
926
}
927
928
/* -------------------------------------------------------------------------- */
929
930
/**
931
 * LtSelf
932
 *
933
 * a < a ==> false
934
 */
935
936
template<> inline
937
bool RewriteRule<LtSelf>::applies(TNode node) {
938
  return ((node.getKind() == kind::BITVECTOR_ULT ||
939
           node.getKind() == kind::BITVECTOR_SLT) &&
940
          node[0] == node[1]);
941
}
942
943
template<> inline
944
Node RewriteRule<LtSelf>::apply(TNode node) {
945
  Debug("bv-rewrite") << "RewriteRule<LtSelf>(" << node << ")" << std::endl;
946
  return utils::mkFalse();
947
}
948
949
/* -------------------------------------------------------------------------- */
950
951
/**
952
 * LteSelf
953
 *
954
 * a <= a ==> true
955
 */
956
957
template<> inline
958
bool RewriteRule<LteSelf>::applies(TNode node) {
959
  return ((node.getKind() == kind::BITVECTOR_ULE ||
960
           node.getKind() == kind::BITVECTOR_SLE) &&
961
          node[0] == node[1]);
962
}
963
964
template<> inline
965
Node RewriteRule<LteSelf>::apply(TNode node) {
966
  Debug("bv-rewrite") << "RewriteRule<LteSelf>(" << node << ")" << std::endl;
967
  return utils::mkTrue();
968
}
969
970
/* -------------------------------------------------------------------------- */
971
972
/**
973
 * ZeroUlt
974
 *
975
 * 0 < a ==> a != 0
976
 */
977
978
template <>
979
inline bool RewriteRule<ZeroUlt>::applies(TNode node)
980
{
981
  return (node.getKind() == kind::BITVECTOR_ULT
982
          && node[0] == utils::mkZero(utils::getSize(node[0])));
983
}
984
985
template <>
986
inline Node RewriteRule<ZeroUlt>::apply(TNode node)
987
{
988
  Debug("bv-rewrite") << "RewriteRule<ZeroUlt>(" << node << ")" << std::endl;
989
  NodeManager *nm = NodeManager::currentNM();
990
  return nm->mkNode(kind::NOT, nm->mkNode(kind::EQUAL, node[0], node[1]));
991
}
992
993
/* -------------------------------------------------------------------------- */
994
995
/**
996
 * UltZero
997
 *
998
 * a < 0 ==> false
999
 */
1000
1001
template<> inline
1002
113285
bool RewriteRule<UltZero>::applies(TNode node) {
1003
448355
  return (node.getKind() == kind::BITVECTOR_ULT &&
1004
448355
          node[1] == utils::mkZero(utils::getSize(node[0])));
1005
}
1006
1007
template<> inline
1008
539
Node RewriteRule<UltZero>::apply(TNode node) {
1009
539
  Debug("bv-rewrite") << "RewriteRule<UltZero>(" << node << ")" << std::endl;
1010
539
  return utils::mkFalse();
1011
}
1012
1013
1014
/* -------------------------------------------------------------------------- */
1015
1016
/**
1017
 *
1018
 */
1019
template<> inline
1020
bool RewriteRule<UltOne>::applies(TNode node) {
1021
  return (node.getKind() == kind::BITVECTOR_ULT &&
1022
          node[1] == utils::mkOne(utils::getSize(node[0])));
1023
}
1024
1025
template <>
1026
inline Node RewriteRule<UltOne>::apply(TNode node)
1027
{
1028
  Debug("bv-rewrite") << "RewriteRule<UltOne>(" << node << ")" << std::endl;
1029
  return NodeManager::currentNM()->mkNode(
1030
      kind::EQUAL, node[0], utils::mkZero(utils::getSize(node[0])));
1031
}
1032
1033
/* -------------------------------------------------------------------------- */
1034
1035
/**
1036
 *
1037
 */
1038
template<> inline
1039
bool RewriteRule<SltZero>::applies(TNode node) {
1040
  return (node.getKind() == kind::BITVECTOR_SLT &&
1041
          node[1] == utils::mkZero(utils::getSize(node[0])));
1042
}
1043
1044
template <>
1045
inline Node RewriteRule<SltZero>::apply(TNode node)
1046
{
1047
  Debug("bv-rewrite") << "RewriteRule<UltZero>(" << node << ")" << std::endl;
1048
  unsigned size = utils::getSize(node[0]);
1049
  Node most_significant_bit = utils::mkExtract(node[0], size - 1, size - 1);
1050
  return NodeManager::currentNM()->mkNode(
1051
      kind::EQUAL, most_significant_bit, utils::mkOne(1));
1052
}
1053
1054
/* -------------------------------------------------------------------------- */
1055
1056
/**
1057
 * UltSelf
1058
 *
1059
 * a < a ==> false
1060
 */
1061
1062
template<> inline
1063
bool RewriteRule<UltSelf>::applies(TNode node) {
1064
  return (node.getKind() == kind::BITVECTOR_ULT &&
1065
          node[1] == node[0]);
1066
}
1067
1068
template<> inline
1069
Node RewriteRule<UltSelf>::apply(TNode node) {
1070
  Debug("bv-rewrite") << "RewriteRule<UltSelf>(" << node << ")" << std::endl;
1071
  return utils::mkFalse();
1072
}
1073
1074
1075
/* -------------------------------------------------------------------------- */
1076
1077
/**
1078
 * UleZero
1079
 *
1080
 * a <= 0 ==> a = 0
1081
 */
1082
1083
template<> inline
1084
6707
bool RewriteRule<UleZero>::applies(TNode node) {
1085
26660
  return (node.getKind() == kind::BITVECTOR_ULE &&
1086
26660
          node[1] == utils::mkZero(utils::getSize(node[0])));
1087
}
1088
1089
template <>
1090
42
inline Node RewriteRule<UleZero>::apply(TNode node)
1091
{
1092
42
  Debug("bv-rewrite") << "RewriteRule<UleZero>(" << node << ")" << std::endl;
1093
42
  return NodeManager::currentNM()->mkNode(kind::EQUAL, node[0], node[1]);
1094
}
1095
1096
/* -------------------------------------------------------------------------- */
1097
1098
/**
1099
 * UleSelf
1100
 *
1101
 * a <= a ==> true
1102
 */
1103
1104
template<> inline
1105
6714
bool RewriteRule<UleSelf>::applies(TNode node) {
1106
26562
  return (node.getKind() == kind::BITVECTOR_ULE &&
1107
26562
          node[1] == node[0]);
1108
}
1109
1110
template<> inline
1111
49
Node RewriteRule<UleSelf>::apply(TNode node) {
1112
49
  Debug("bv-rewrite") << "RewriteRule<UleSelf>(" << node << ")" << std::endl;
1113
49
  return utils::mkTrue();
1114
}
1115
1116
/* -------------------------------------------------------------------------- */
1117
1118
/**
1119
 * ZeroUle
1120
 *
1121
 * 0 <= a ==> true
1122
 */
1123
1124
template<> inline
1125
6678
bool RewriteRule<ZeroUle>::applies(TNode node) {
1126
26583
  return (node.getKind() == kind::BITVECTOR_ULE &&
1127
26583
          node[0] == utils::mkZero(utils::getSize(node[0])));
1128
}
1129
1130
template<> inline
1131
13
Node RewriteRule<ZeroUle>::apply(TNode node) {
1132
13
  Debug("bv-rewrite") << "RewriteRule<ZeroUle>(" << node << ")" << std::endl;
1133
13
  return utils::mkTrue();
1134
}
1135
1136
/* -------------------------------------------------------------------------- */
1137
1138
/**
1139
 * UleMax
1140
 *
1141
 * a <= 11..1 ==> true
1142
 */
1143
1144
template<> inline
1145
6682
bool RewriteRule<UleMax>::applies(TNode node) {
1146
6682
  if (node.getKind()!= kind::BITVECTOR_ULE) {
1147
26
    return false;
1148
  }
1149
6656
  uint32_t size = utils::getSize(node[0]);
1150
6656
  return (node.getKind() == kind::BITVECTOR_ULE
1151
13312
          && node[1] == utils::mkOnes(size));
1152
}
1153
1154
template<> inline
1155
17
Node RewriteRule<UleMax>::apply(TNode node) {
1156
17
  Debug("bv-rewrite") << "RewriteRule<UleMax>(" << node << ")" << std::endl;
1157
17
  return utils::mkTrue();
1158
}
1159
1160
/* -------------------------------------------------------------------------- */
1161
1162
/**
1163
 * NotUlt
1164
 *
1165
 * ~ ( a < b) ==> b <= a
1166
 */
1167
1168
template<> inline
1169
bool RewriteRule<NotUlt>::applies(TNode node) {
1170
  return (node.getKind() == kind::NOT &&
1171
          node[0].getKind() == kind::BITVECTOR_ULT);
1172
}
1173
1174
template <>
1175
inline Node RewriteRule<NotUlt>::apply(TNode node)
1176
{
1177
  Debug("bv-rewrite") << "RewriteRule<NotUlt>(" << node << ")" << std::endl;
1178
  Node ult = node[0];
1179
  Node a = ult[0];
1180
  Node b = ult[1];
1181
  return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULE, b, a);
1182
}
1183
1184
/* -------------------------------------------------------------------------- */
1185
1186
/**
1187
 * NotUle
1188
 *
1189
 * ~ ( a <= b) ==> b < a
1190
 */
1191
1192
template<> inline
1193
bool RewriteRule<NotUle>::applies(TNode node) {
1194
  return (node.getKind() == kind::NOT &&
1195
          node[0].getKind() == kind::BITVECTOR_ULE);
1196
}
1197
1198
template <>
1199
inline Node RewriteRule<NotUle>::apply(TNode node)
1200
{
1201
  Debug("bv-rewrite") << "RewriteRule<NotUle>(" << node << ")" << std::endl;
1202
  Node ult = node[0];
1203
  Node a = ult[0];
1204
  Node b = ult[1];
1205
  return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, b, a);
1206
}
1207
1208
/* -------------------------------------------------------------------------- */
1209
1210
/**
1211
 * MultPow2
1212
 *
1213
 * (a * 2^k) ==> a[n-k-1:0] 0_k
1214
 */
1215
1216
template <>
1217
313684
inline bool RewriteRule<MultPow2>::applies(TNode node)
1218
{
1219
313684
  if (node.getKind() != kind::BITVECTOR_MULT)
1220
51398
    return false;
1221
1222
958397
  for (const Node& cn : node)
1223
  {
1224
714841
    bool cIsNeg = false;
1225
714841
    if (utils::isPow2Const(cn, cIsNeg))
1226
    {
1227
18730
      return true;
1228
    }
1229
  }
1230
243556
  return false;
1231
}
1232
1233
template <>
1234
9365
inline Node RewriteRule<MultPow2>::apply(TNode node)
1235
{
1236
9365
  Debug("bv-rewrite") << "RewriteRule<MultPow2>(" << node << ")" << std::endl;
1237
9365
  NodeManager *nm = NodeManager::currentNM();
1238
9365
  unsigned size = utils::getSize(node);
1239
18730
  std::vector<Node>  children;
1240
9365
  unsigned exponent = 0;
1241
9365
  bool isNeg = false;
1242
28195
  for (const Node& cn : node)
1243
  {
1244
18830
    bool cIsNeg = false;
1245
18830
    unsigned exp = utils::isPow2Const(cn, cIsNeg);
1246
18830
    if (exp) {
1247
9367
      exponent += exp - 1;
1248
9367
      if (cIsNeg)
1249
      {
1250
1724
        isNeg = !isNeg;
1251
      }
1252
    }
1253
    else {
1254
9463
      children.push_back(cn);
1255
    }
1256
  }
1257
9365
  if (exponent >= size)
1258
  {
1259
    return utils::mkZero(size);
1260
  }
1261
1262
18730
  Node a;
1263
9365
  if (children.empty())
1264
  {
1265
2
    a = utils::mkOne(size);
1266
  }
1267
  else
1268
  {
1269
9363
    a = utils::mkNaryNode(kind::BITVECTOR_MULT, children);
1270
  }
1271
1272
9365
  if (isNeg && size > 1)
1273
  {
1274
1720
    a = nm->mkNode(kind::BITVECTOR_NEG, a);
1275
  }
1276
9365
  if (exponent == 0)
1277
  {
1278
2
    return a;
1279
  }
1280
18726
  Node extract = utils::mkExtract(a, size - exponent - 1, 0);
1281
18726
  Node zeros = utils::mkConst(exponent, 0);
1282
9363
  return utils::mkConcat(extract, zeros);
1283
}
1284
1285
/* -------------------------------------------------------------------------- */
1286
1287
/**
1288
 * ExtractMultLeadingBit
1289
 *
1290
 * If the bit-vectors multiplied have enough leading zeros,
1291
 * we can determine that the top bits of the multiplication
1292
 * are zero and not compute them. Only apply for large bitwidths
1293
 * as this can interfere with other mult normalization rewrites such
1294
 * as flattening.
1295
 */
1296
1297
template<> inline
1298
170854
bool RewriteRule<ExtractMultLeadingBit>::applies(TNode node) {
1299
170854
  if (node.getKind() != kind::BITVECTOR_EXTRACT)
1300
63002
    return false;
1301
107852
  unsigned low = utils::getExtractLow(node);
1302
107852
  node = node[0];
1303
1304
218343
  if (node.getKind() != kind::BITVECTOR_MULT ||
1305
220444
      node.getNumChildren() != 2 ||
1306
112592
      utils::getSize(node) <= 64)
1307
107846
    return false;
1308
1309
30
  if (node[0].getKind() != kind::BITVECTOR_CONCAT ||
1310
30
      node[1].getKind() != kind::BITVECTOR_CONCAT ||
1311
48
      !node[0][0].isConst() ||
1312
18
      !node[1][0].isConst())
1313
    return false;
1314
1315
6
  unsigned n = utils::getSize(node);
1316
  // count number of leading zeroes
1317
12
  const Integer& int1 = node[0][0].getConst<BitVector>().toInteger();
1318
12
  const Integer& int2 = node[1][0].getConst<BitVector>().toInteger();
1319
6
  size_t int1_size = utils::getSize(node[0][0]);
1320
6
  size_t int2_size = utils::getSize(node[1][0]);
1321
6
  unsigned zeroes1 = int1.isZero() ? int1_size : int1_size - int1.length();
1322
6
  unsigned zeroes2 = int2.isZero() ? int2_size : int2_size - int2.length();
1323
1324
  // first k bits are not zero in the result
1325
6
  unsigned k = 2 * n - (zeroes1 + zeroes2);
1326
1327
6
  if (k > low)
1328
6
    return false;
1329
1330
  return true;
1331
}
1332
1333
template<> inline
1334
Node RewriteRule<ExtractMultLeadingBit>::apply(TNode node) {
1335
  Debug("bv-rewrite") << "RewriteRule<MultLeadingBit>(" << node << ")" << std::endl;
1336
1337
  unsigned bitwidth = utils::getSize(node);
1338
1339
  // node = node[0];
1340
  // const Integer& int1 = node[0][0].getConst<BitVector>().toInteger();
1341
  // const Integer& int2 = node[1][0].getConst<BitVector>().toInteger();
1342
  // unsigned zeroes1 = int1.isZero()? utils::getSize(node[0][0]) :
1343
  //                                   int1.length();
1344
1345
  // unsigned zeroes2 = int2.isZero()? utils::getSize(node[1][0]) :
1346
  //                                   int2.length();
1347
  // all bits >= k in the multiplier will have to be 0
1348
  // unsigned n = utils::getSize(node);
1349
  // unsigned k = 2 * n - (zeroes1 + zeroes2);
1350
  // Node extract1 = utils::mkExtract(node[0], k - 1, 0);
1351
  // Node extract2 = utils::mkExtract(node[1], k - 1, 0);
1352
  // Node k_zeroes = utils::mkConst(n - k, 0u);
1353
1354
  // NodeManager *nm = NodeManager::currentNM();
1355
  // Node new_mult = nm->mkNode(kind::BITVECTOR_MULT, extract1, extract2);
1356
  // Node result = utils::mkExtract(nm->mkNode(kind::BITVECTOR_CONCAT, k_zeroes, new_mult), high, low);
1357
1358
  // since the extract is over multiplier bits that have to be 0, return 0
1359
  Node result = utils::mkConst(bitwidth, 0u);
1360
  //  std::cout << "MultLeadingBit " << node <<" => " << result <<"\n";
1361
  return result;
1362
}
1363
1364
/* -------------------------------------------------------------------------- */
1365
1366
/**
1367
 * NegIdemp
1368
 *
1369
 * -(-a) ==> a
1370
 */
1371
1372
template<> inline
1373
35151
bool RewriteRule<NegIdemp>::applies(TNode node) {
1374
88445
  return (node.getKind() == kind::BITVECTOR_NEG &&
1375
88445
          node[0].getKind() == kind::BITVECTOR_NEG);
1376
}
1377
1378
template<> inline
1379
151
Node RewriteRule<NegIdemp>::apply(TNode node) {
1380
151
  Debug("bv-rewrite") << "RewriteRule<NegIdemp>(" << node << ")" << std::endl;
1381
151
  return node[0][0];
1382
}
1383
1384
/* -------------------------------------------------------------------------- */
1385
1386
/**
1387
 * UdivPow2
1388
 *
1389
 * (a udiv 2^k) ==> 0_k a[n-1: k]
1390
 */
1391
1392
template <>
1393
41601
inline bool RewriteRule<UdivPow2>::applies(TNode node)
1394
{
1395
41601
  bool isNeg = false;
1396
83202
  if (node.getKind() == kind::BITVECTOR_UDIV
1397
83202
      && utils::isPow2Const(node[1], isNeg))
1398
  {
1399
6546
    return !isNeg;
1400
  }
1401
35055
  return false;
1402
}
1403
1404
template <>
1405
2731
inline Node RewriteRule<UdivPow2>::apply(TNode node)
1406
{
1407
2731
  Debug("bv-rewrite") << "RewriteRule<UdivPow2>(" << node << ")" << std::endl;
1408
2731
  NodeManager *nm = NodeManager::currentNM();
1409
2731
  unsigned size = utils::getSize(node);
1410
5462
  Node a = node[0];
1411
2731
  bool isNeg = false;
1412
2731
  unsigned power = utils::isPow2Const(node[1], isNeg) - 1;
1413
2731
  Node ret;
1414
2731
  if (power == 0)
1415
  {
1416
1599
    ret = a;
1417
  }
1418
  else
1419
  {
1420
2264
    Node extract = utils::mkExtract(a, size - 1, power);
1421
2264
    Node zeros = utils::mkConst(power, 0);
1422
1423
1132
    ret = nm->mkNode(kind::BITVECTOR_CONCAT, zeros, extract);
1424
  }
1425
2731
  if (isNeg && size > 1)
1426
  {
1427
    ret = nm->mkNode(kind::BITVECTOR_NEG, ret);
1428
  }
1429
5462
  return ret;
1430
}
1431
1432
/* -------------------------------------------------------------------------- */
1433
1434
/**
1435
 * UdivZero
1436
 *
1437
 * (a udiv 0) ==> 111...1
1438
 */
1439
1440
template <>
1441
37967
inline bool RewriteRule<UdivZero>::applies(TNode node) {
1442
37967
  return (node.getKind() == kind::BITVECTOR_UDIV
1443
75934
          && node[1] == utils::mkConst(utils::getSize(node), 0));
1444
}
1445
1446
template <>
1447
190
inline Node RewriteRule<UdivZero>::apply(TNode node) {
1448
190
  Debug("bv-rewrite") << "RewriteRule<UdivZero>(" << node << ")" << std::endl;
1449
190
  return utils::mkOnes(utils::getSize(node));
1450
}
1451
1452
/* -------------------------------------------------------------------------- */
1453
1454
/**
1455
 * UdivOne
1456
 *
1457
 * (a udiv 1) ==> a
1458
 */
1459
1460
template <>
1461
36139
inline bool RewriteRule<UdivOne>::applies(TNode node) {
1462
36139
  return (node.getKind() == kind::BITVECTOR_UDIV
1463
72278
          && node[1] == utils::mkConst(utils::getSize(node), 1));
1464
}
1465
1466
template <>
1467
inline Node RewriteRule<UdivOne>::apply(TNode node) {
1468
  Debug("bv-rewrite") << "RewriteRule<UdivOne>(" << node << ")" << std::endl;
1469
  return node[0];
1470
}
1471
1472
/* -------------------------------------------------------------------------- */
1473
1474
/**
1475
 * UremPow2
1476
 *
1477
 * (a urem 2^k) ==> 0_(n-k) a[k-1:0]
1478
 */
1479
1480
template <>
1481
42250
inline bool RewriteRule<UremPow2>::applies(TNode node)
1482
{
1483
  bool isNeg;
1484
84500
  if (node.getKind() == kind::BITVECTOR_UREM
1485
84500
      && utils::isPow2Const(node[1], isNeg))
1486
  {
1487
6075
    return !isNeg;
1488
  }
1489
36175
  return false;
1490
}
1491
1492
template <>
1493
2483
inline Node RewriteRule<UremPow2>::apply(TNode node)
1494
{
1495
2483
  Debug("bv-rewrite") << "RewriteRule<UremPow2>(" << node << ")" << std::endl;
1496
4966
  TNode a = node[0];
1497
2483
  bool isNeg = false;
1498
2483
  unsigned power = utils::isPow2Const(node[1], isNeg) - 1;
1499
2483
  Node ret;
1500
2483
  if (power == 0)
1501
  {
1502
1407
    ret = utils::mkZero(utils::getSize(node));
1503
  }
1504
  else
1505
  {
1506
2152
    Node extract = utils::mkExtract(a, power - 1, 0);
1507
2152
    Node zeros = utils::mkZero(utils::getSize(node) - power);
1508
1076
    ret = NodeManager::currentNM()->mkNode(
1509
        kind::BITVECTOR_CONCAT, zeros, extract);
1510
  }
1511
4966
  return ret;
1512
}
1513
1514
/* -------------------------------------------------------------------------- */
1515
1516
/**
1517
 * UremOne
1518
 *
1519
 * (a urem 1) ==> 0
1520
 */
1521
1522
template<> inline
1523
37284
bool RewriteRule<UremOne>::applies(TNode node) {
1524
37284
  return (node.getKind() == kind::BITVECTOR_UREM
1525
74568
          && node[1] == utils::mkConst(utils::getSize(node), 1));
1526
}
1527
1528
template<> inline
1529
Node RewriteRule<UremOne>::apply(TNode node) {
1530
  Debug("bv-rewrite") << "RewriteRule<UremOne>(" << node << ")" << std::endl;
1531
  return utils::mkConst(utils::getSize(node), 0);
1532
}
1533
1534
/* -------------------------------------------------------------------------- */
1535
1536
/**
1537
 * UremSelf
1538
 *
1539
 * (a urem a) ==> 0
1540
 */
1541
1542
template<> inline
1543
37356
bool RewriteRule<UremSelf>::applies(TNode node) {
1544
37356
  return (node.getKind() == kind::BITVECTOR_UREM && node[0] == node[1]);
1545
}
1546
1547
template<> inline
1548
72
Node RewriteRule<UremSelf>::apply(TNode node) {
1549
72
  Debug("bv-rewrite") << "RewriteRule<UremSelf>(" << node << ")" << std::endl;
1550
72
  return utils::mkConst(utils::getSize(node), 0);
1551
}
1552
1553
/* -------------------------------------------------------------------------- */
1554
1555
/**
1556
 * ShiftZero
1557
 *
1558
 * (0_k >> a) ==> 0_k
1559
 */
1560
1561
template<> inline
1562
32027
bool RewriteRule<ShiftZero>::applies(TNode node) {
1563
53307
  return ((node.getKind() == kind::BITVECTOR_SHL ||
1564
27434
           node.getKind() == kind::BITVECTOR_LSHR ||
1565
166289
           node.getKind() == kind::BITVECTOR_ASHR) &&
1566
128108
          node[0] == utils::mkConst(utils::getSize(node), 0));
1567
}
1568
1569
template<> inline
1570
1335
Node RewriteRule<ShiftZero>::apply(TNode node) {
1571
1335
  Debug("bv-rewrite") << "RewriteRule<ShiftZero>(" << node << ")" << std::endl;
1572
1335
  return node[0];
1573
}
1574
1575
/* -------------------------------------------------------------------------- */
1576
1577
/**
1578
 * UgtUrem
1579
 *
1580
 * (bvugt (bvurem T x) x)
1581
 *   ==>  (ite (= x 0_k) (bvugt T x) false)
1582
 *   ==>  (and (=> (= x 0_k) (bvugt T x)) (=> (not (= x 0_k)) false))
1583
 *   ==>  (and (=> (= x 0_k) (bvugt T x)) (= x 0_k))
1584
 *   ==>  (and (bvugt T x) (= x 0_k))
1585
 *   ==>  (and (bvugt T 0_k) (= x 0_k))
1586
 */
1587
1588
template <>
1589
3627
inline bool RewriteRule<UgtUrem>::applies(TNode node)
1590
{
1591
3627
  return (node.getKind() == kind::BITVECTOR_UGT
1592
7254
          && node[0].getKind() == kind::BITVECTOR_UREM
1593
10917
          && node[0][1] == node[1]);
1594
}
1595
1596
template <>
1597
9
inline Node RewriteRule<UgtUrem>::apply(TNode node)
1598
{
1599
9
  Debug("bv-rewrite") << "RewriteRule<UgtUrem>(" << node << ")" << std::endl;
1600
18
  const Node& T = node[0][0];
1601
18
  const Node& x = node[1];
1602
18
  Node zero = utils::mkConst(utils::getSize(x), 0);
1603
9
  NodeManager* nm = NodeManager::currentNM();
1604
  return nm->mkNode(kind::AND,
1605
18
                    nm->mkNode(kind::EQUAL, x, zero),
1606
36
                    nm->mkNode(kind::BITVECTOR_UGT, T, zero));
1607
}
1608
1609
/* -------------------------------------------------------------------------- */
1610
1611
/**
1612
 * BBPlusNeg
1613
 *
1614
 * -a1 - a2 - ... - an + ak + ..  ==> - (a1 + a2 + ... + an) + ak
1615
 *
1616
 */
1617
1618
template<> inline
1619
bool RewriteRule<BBPlusNeg>::applies(TNode node) {
1620
  if (node.getKind() != kind::BITVECTOR_PLUS) {
1621
    return false;
1622
  }
1623
1624
  unsigned neg_count = 0;
1625
  for(unsigned i = 0; i < node.getNumChildren(); ++i) {
1626
    if (node[i].getKind()== kind::BITVECTOR_NEG) {
1627
      ++neg_count;
1628
    }
1629
  }
1630
  return neg_count > 1;
1631
}
1632
1633
template <>
1634
inline Node RewriteRule<BBPlusNeg>::apply(TNode node)
1635
{
1636
  Debug("bv-rewrite") << "RewriteRule<BBPlusNeg>(" << node << ")" << std::endl;
1637
  NodeManager *nm = NodeManager::currentNM();
1638
  std::vector<Node> children;
1639
  unsigned neg_count = 0;
1640
  for (unsigned i = 0; i < node.getNumChildren(); ++i)
1641
  {
1642
    if (node[i].getKind() == kind::BITVECTOR_NEG)
1643
    {
1644
      ++neg_count;
1645
      children.push_back(nm->mkNode(kind::BITVECTOR_NOT, node[i][0]));
1646
    }
1647
    else
1648
    {
1649
      children.push_back(node[i]);
1650
    }
1651
  }
1652
  Assert(neg_count != 0);
1653
  children.push_back(utils::mkConst(utils::getSize(node), neg_count));
1654
1655
  return utils::mkNaryNode(kind::BITVECTOR_PLUS, children);
1656
}
1657
1658
/* -------------------------------------------------------------------------- */
1659
1660
template<> inline
1661
66159
bool RewriteRule<MergeSignExtend>::applies(TNode node) {
1662
329997
  if (node.getKind() != kind::BITVECTOR_SIGN_EXTEND ||
1663
330007
      (node[0].getKind() != kind::BITVECTOR_SIGN_EXTEND &&
1664
197689
       node[0].getKind() != kind::BITVECTOR_ZERO_EXTEND))
1665
65361
    return false;
1666
798
  return true;
1667
}
1668
1669
template<> inline
1670
399
Node RewriteRule<MergeSignExtend>::apply(TNode node) {
1671
399
  Debug("bv-rewrite") << "RewriteRule<MergeSignExtend>(" << node << ")" << std::endl;
1672
  unsigned amount1 =
1673
399
      node.getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount;
1674
1675
399
  NodeManager* nm = NodeManager::currentNM();
1676
399
  if (node[0].getKind() == kind::BITVECTOR_ZERO_EXTEND) {
1677
    unsigned amount2 = node[0]
1678
404
                           .getOperator()
1679
202
                           .getConst<BitVectorZeroExtend>()
1680
202
                           .d_zeroExtendAmount;
1681
202
    if (amount2 == 0)
1682
    {
1683
142
      NodeBuilder<> nb(kind::BITVECTOR_SIGN_EXTEND);
1684
142
      Node op = nm->mkConst<BitVectorSignExtend>(BitVectorSignExtend(amount1));
1685
71
      nb << op << node[0][0];
1686
142
      Node res = nb;
1687
71
      return res;
1688
    }
1689
262
    NodeBuilder<> nb(kind::BITVECTOR_ZERO_EXTEND);
1690
    Node op = nm->mkConst<BitVectorZeroExtend>(
1691
262
        BitVectorZeroExtend(amount1 + amount2));
1692
131
    nb << op << node[0][0];
1693
262
    Node res = nb;
1694
131
    return res;
1695
  }
1696
197
  Assert(node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND);
1697
  unsigned amount2 =
1698
197
      node[0].getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount;
1699
197
  return utils::mkSignExtend(node[0][0], amount1 + amount2);
1700
}
1701
1702
/* -------------------------------------------------------------------------- */
1703
1704
/**
1705
 * ZeroExtendEqConst
1706
 *
1707
 * Rewrite zero_extend(x^n, m) = c^n+m to
1708
 *
1709
 *   false         if c[n+m-1:n] != 0
1710
 *   x = c[n-1:0]  otherwise.
1711
 */
1712
template <>
1713
301488
inline bool RewriteRule<ZeroExtendEqConst>::applies(TNode node) {
1714
333730
  return node.getKind() == kind::EQUAL &&
1715
333730
         ((node[0].getKind() == kind::BITVECTOR_ZERO_EXTEND &&
1716
333730
           node[1].isConst()) ||
1717
333730
          (node[1].getKind() == kind::BITVECTOR_ZERO_EXTEND &&
1718
602976
           node[0].isConst()));
1719
}
1720
1721
template <>
1722
inline Node RewriteRule<ZeroExtendEqConst>::apply(TNode node) {
1723
  TNode t, c;
1724
  if (node[0].getKind() == kind::BITVECTOR_ZERO_EXTEND) {
1725
    t = node[0][0];
1726
    c = node[1];
1727
  } else {
1728
    t = node[1][0];
1729
    c = node[0];
1730
  }
1731
  BitVector c_hi =
1732
      c.getConst<BitVector>().extract(utils::getSize(c) - 1, utils::getSize(t));
1733
  BitVector c_lo = c.getConst<BitVector>().extract(utils::getSize(t) - 1, 0);
1734
  BitVector zero = BitVector(c_hi.getSize(), Integer(0));
1735
1736
  if (c_hi == zero) {
1737
    return NodeManager::currentNM()->mkNode(kind::EQUAL, t,
1738
                                            utils::mkConst(c_lo));
1739
  }
1740
  return utils::mkFalse();
1741
}
1742
1743
/* -------------------------------------------------------------------------- */
1744
1745
/**
1746
 * SignExtendEqConst
1747
 *
1748
 * Rewrite sign_extend(x^n, m) = c^n+m to
1749
 *
1750
 *   x = c[n-1:0]   if (c[n-1:n-1] == 0 && c[n+m-1:n] == 0) ||
1751
 *                     (c[n-1:n-1] == 1 && c[n+m-1:n] == ~0)
1752
 *   false          otherwise.
1753
 */
1754
template <>
1755
302178
inline bool RewriteRule<SignExtendEqConst>::applies(TNode node) {
1756
336490
  return node.getKind() == kind::EQUAL &&
1757
339804
         ((node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND &&
1758
338512
           node[1].isConst()) ||
1759
335840
          (node[1].getKind() == kind::BITVECTOR_SIGN_EXTEND &&
1760
605688
           node[0].isConst()));
1761
}
1762
1763
template <>
1764
345
inline Node RewriteRule<SignExtendEqConst>::apply(TNode node) {
1765
690
  TNode t, c;
1766
345
  if (node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND) {
1767
323
    t = node[0][0];
1768
323
    c = node[1];
1769
  } else {
1770
22
    t = node[1][0];
1771
22
    c = node[0];
1772
  }
1773
345
  unsigned pos_msb_t = utils::getSize(t) - 1;
1774
  BitVector c_hi =
1775
690
      c.getConst<BitVector>().extract(utils::getSize(c) - 1, pos_msb_t);
1776
690
  BitVector c_lo = c.getConst<BitVector>().extract(pos_msb_t, 0);
1777
690
  BitVector zero = BitVector(c_hi.getSize(), Integer(0));
1778
1779
345
  if (c_hi == zero || c_hi == ~zero) {
1780
    return NodeManager::currentNM()->mkNode(kind::EQUAL, t,
1781
170
                                            utils::mkConst(c_lo));
1782
  }
1783
175
  return utils::mkFalse();
1784
}
1785
1786
/* -------------------------------------------------------------------------- */
1787
1788
/**
1789
 * ZeroExtendUltConst
1790
 *
1791
 * Rewrite zero_extend(x^n,m) < c^n+m to
1792
 *
1793
 *   x < c[n-1:0]   if c[n+m-1:n] == 0.
1794
 *
1795
 * Rewrite c^n+m < Rewrite zero_extend(x^n,m) to
1796
 *
1797
 *   c[n-1:0] < x   if c[n+m-1:n] == 0.
1798
 */
1799
template <>
1800
112774
inline bool RewriteRule<ZeroExtendUltConst>::applies(TNode node) {
1801
446280
  if (node.getKind() == kind::BITVECTOR_ULT &&
1802
337608
      ((node[0].getKind() == kind::BITVECTOR_ZERO_EXTEND &&
1803
337444
        node[1].isConst()) ||
1804
337154
       (node[1].getKind() == kind::BITVECTOR_ZERO_EXTEND &&
1805
116758
        node[0].isConst()))) {
1806
344
    TNode t, c;
1807
172
    bool is_lhs = node[0].getKind() == kind::BITVECTOR_ZERO_EXTEND;
1808
172
    if (is_lhs) {
1809
82
      t = node[0][0];
1810
82
      c = node[1];
1811
    } else {
1812
90
      t = node[1][0];
1813
90
      c = node[0];
1814
    }
1815
1816
172
    if (utils::getSize(t) == utils::getSize(c))
1817
    {
1818
8
      return false;
1819
    }
1820
1821
328
    BitVector bv_c = c.getConst<BitVector>();
1822
492
    BitVector c_hi = c.getConst<BitVector>().extract(utils::getSize(c) - 1,
1823
656
                                                     utils::getSize(t));
1824
328
    BitVector zero = BitVector(c_hi.getSize(), Integer(0));
1825
1826
164
    return c_hi == zero;
1827
  }
1828
112602
  return false;
1829
}
1830
1831
template <>
1832
28
inline Node RewriteRule<ZeroExtendUltConst>::apply(TNode node) {
1833
56
  TNode t, c;
1834
28
  bool is_lhs = node[0].getKind() == kind::BITVECTOR_ZERO_EXTEND;
1835
28
  if (is_lhs) {
1836
12
    t = node[0][0];
1837
12
    c = node[1];
1838
  } else {
1839
16
    t = node[1][0];
1840
16
    c = node[0];
1841
  }
1842
  Node c_lo =
1843
56
      utils::mkConst(c.getConst<BitVector>().extract(utils::getSize(t) - 1, 0));
1844
1845
28
  if (is_lhs) {
1846
12
    return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, t, c_lo);
1847
  }
1848
16
  return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, c_lo, t);
1849
}
1850
1851
/* -------------------------------------------------------------------------- */
1852
1853
/**
1854
 * SignExtendUltConst
1855
 *
1856
 * Rewrite sign_extend(x^n,m) < c^n+m to
1857
 *
1858
 *   x < c[n-1:0]   if (c <= (1 << (n - 1))) || (c >= (~0 << (n - 1)))
1859
 *   x[n-1:n-1] = 0 if (1 << (n - 1)) < c <= (~0 << (n - 1)).
1860
 *
1861
 * Rewrite c^n+m < sign_extend(x^n,m) to
1862
 *
1863
 *   c[n-1:0] < x   if (c < (1 << (n - 1))) || (c >= ~(1 << (n-1)))
1864
 *   x[n-1:n-1] = 1 if ~(~0 << (n-1)) <= c <= ~(1 << (n-1))
1865
 *
1866
 * where ~(~0 << (n - 1)) == (1 << (n - 1)) - 1
1867
 *
1868
 */
1869
template <>
1870
113233
inline bool RewriteRule<SignExtendUltConst>::applies(TNode node)
1871
{
1872
226466
  if (node.getKind() == kind::BITVECTOR_ULT
1873
340673
      && ((node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND
1874
129264
           && node[1].isConst())
1875
223958
          || (node[1].getKind() == kind::BITVECTOR_SIGN_EXTEND
1876
129123
              && node[0].isConst())))
1877
  {
1878
1948
    TNode x, c;
1879
974
    bool is_lhs = node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND;
1880
974
    if (is_lhs)
1881
    {
1882
374
      x = node[0][0];
1883
374
      c = node[1];
1884
    }
1885
    else
1886
    {
1887
600
      x = node[1][0];
1888
600
      c = node[0];
1889
    }
1890
1948
    BitVector bv_c = c.getConst<BitVector>();
1891
974
    unsigned size_c = utils::getSize(c);
1892
974
    unsigned msb_x_pos = utils::getSize(x) - 1;
1893
    // (1 << (n - 1)))
1894
1948
    BitVector bv_msb_x(size_c);
1895
974
    bv_msb_x.setBit(msb_x_pos, true);
1896
    // (~0 << (n - 1))
1897
    BitVector bv_upper_bits =
1898
1948
        (~BitVector(size_c)).leftShift(BitVector(size_c, msb_x_pos));
1899
1900
    return (is_lhs
1901
374
            && (bv_c <= bv_msb_x || bv_c >= bv_upper_bits
1902
234
                || (bv_msb_x < bv_c && bv_c <= bv_upper_bits)))
1903
2548
           || (!is_lhs
1904
1574
               && (bv_c < bv_msb_x || bv_c >= ~bv_msb_x
1905
1248
                   || (~bv_upper_bits <= bv_c && bv_c <= ~bv_msb_x)));
1906
  }
1907
112259
  return false;
1908
}
1909
1910
template <>
1911
487
inline Node RewriteRule<SignExtendUltConst>::apply(TNode node)
1912
{
1913
974
  TNode x, c;
1914
487
  bool is_lhs = node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND;
1915
487
  if (is_lhs)
1916
  {
1917
187
    x = node[0][0];
1918
187
    c = node[1];
1919
  }
1920
  else
1921
  {
1922
300
    x = node[1][0];
1923
300
    c = node[0];
1924
  }
1925
974
  BitVector bv_c = c.getConst<BitVector>();
1926
1927
487
  unsigned size_c = utils::getSize(c);
1928
487
  unsigned msb_x_pos = utils::getSize(x) - 1;
1929
974
  Node c_lo = utils::mkConst(bv_c.extract(msb_x_pos, 0));
1930
  // (1 << (n - 1)))
1931
974
  BitVector bv_msb_x(size_c);
1932
487
  bv_msb_x.setBit(msb_x_pos, true);
1933
  // (~0 << (n - 1))
1934
  BitVector bv_upper_bits =
1935
974
      (~BitVector(size_c)).leftShift(BitVector(size_c, msb_x_pos));
1936
1937
487
  NodeManager* nm = NodeManager::currentNM();
1938
487
  if (is_lhs)
1939
  {
1940
    // x[n-1:n-1] = 0
1941
187
    if (bv_msb_x < bv_c && bv_c <= bv_upper_bits)
1942
    {
1943
274
      Node msb_x = utils::mkExtract(x, msb_x_pos, msb_x_pos);
1944
137
      return nm->mkNode(kind::EQUAL, msb_x, utils::mkZero(1));
1945
    }
1946
    // x < c[n-1:0]
1947
50
    Assert(bv_c <= bv_msb_x || bv_c >= bv_upper_bits);
1948
50
    return nm->mkNode(kind::BITVECTOR_ULT, x, c_lo);
1949
  }
1950
1951
  // x[n-1:n-1] = 1
1952
300
  if (~bv_upper_bits <= bv_c && bv_c <= ~bv_msb_x)
1953
  {
1954
446
    Node msb_x = utils::mkExtract(x, msb_x_pos, msb_x_pos);
1955
223
    return nm->mkNode(kind::EQUAL, msb_x, utils::mkOne(1));
1956
  }
1957
  // c[n-1:0] < x
1958
77
  Assert(bv_c < bv_msb_x || bv_c >= ~bv_msb_x);
1959
77
  return nm->mkNode(kind::BITVECTOR_ULT, c_lo, x);
1960
}
1961
1962
/* -------------------------------------------------------------------------- */
1963
1964
template<> inline
1965
4
bool RewriteRule<MultSlice>::applies(TNode node) {
1966
4
  if (node.getKind() != kind::BITVECTOR_MULT || node.getNumChildren() != 2) {
1967
2
    return false;
1968
  }
1969
2
  return utils::getSize(node[0]) % 2 == 0;
1970
}
1971
1972
/**
1973
 * Expressses the multiplication in terms of the top and bottom
1974
 * slices of the terms. Note increases circuit size, but could
1975
 * lead to simplifications (use wisely!).
1976
 *
1977
 * @param node
1978
 *
1979
 * @return
1980
 */
1981
template <>
1982
2
inline Node RewriteRule<MultSlice>::apply(TNode node)
1983
{
1984
2
  Debug("bv-rewrite") << "RewriteRule<MultSlice>(" << node << ")" << std::endl;
1985
2
  NodeManager *nm = NodeManager::currentNM();
1986
2
  unsigned bitwidth = utils::getSize(node[0]);
1987
4
  Node zeros = utils::mkConst(bitwidth / 2, 0);
1988
4
  TNode a = node[0];
1989
4
  Node bottom_a = utils::mkExtract(a, bitwidth / 2 - 1, 0);
1990
4
  Node top_a = utils::mkExtract(a, bitwidth - 1, bitwidth / 2);
1991
4
  TNode b = node[1];
1992
4
  Node bottom_b = utils::mkExtract(b, bitwidth / 2 - 1, 0);
1993
4
  Node top_b = utils::mkExtract(b, bitwidth - 1, bitwidth / 2);
1994
1995
  Node term1 = nm->mkNode(kind::BITVECTOR_MULT,
1996
4
                          nm->mkNode(kind::BITVECTOR_CONCAT, zeros, bottom_a),
1997
8
                          nm->mkNode(kind::BITVECTOR_CONCAT, zeros, bottom_b));
1998
1999
  Node term2 = nm->mkNode(kind::BITVECTOR_CONCAT,
2000
4
                          nm->mkNode(kind::BITVECTOR_MULT, top_b, bottom_a),
2001
8
                          zeros);
2002
  Node term3 = nm->mkNode(kind::BITVECTOR_CONCAT,
2003
4
                          nm->mkNode(kind::BITVECTOR_MULT, top_a, bottom_b),
2004
8
                          zeros);
2005
4
  return nm->mkNode(kind::BITVECTOR_PLUS, term1, term2, term3);
2006
}
2007
2008
/* -------------------------------------------------------------------------- */
2009
2010
/**
2011
 * x < y + 1 <=> (not y < x) and y != 1...1
2012
 *
2013
 * @param node
2014
 *
2015
 * @return
2016
 */
2017
template<> inline
2018
301947
bool RewriteRule<UltPlusOne>::applies(TNode node) {
2019
301947
  if (node.getKind() != kind::BITVECTOR_ULT) return false;
2020
27326
  TNode x = node[0];
2021
27326
  TNode y1 = node[1];
2022
13663
  if (y1.getKind() != kind::BITVECTOR_PLUS) return false;
2023
3416
  if (y1[0].getKind() != kind::CONST_BITVECTOR &&
2024
2515
      y1[1].getKind() != kind::CONST_BITVECTOR)
2025
561
    return false;
2026
2027
868
  if (y1[0].getKind() == kind::CONST_BITVECTOR &&
2028
528
      y1[1].getKind() == kind::CONST_BITVECTOR)
2029
    return false;
2030
2031
340
  if (y1.getNumChildren() != 2)
2032
16
    return false;
2033
2034
648
  TNode one = y1[0].getKind() == kind::CONST_BITVECTOR ? y1[0] : y1[1];
2035
324
  if (one != utils::mkConst(utils::getSize(one), 1)) return false;
2036
108
  return true;
2037
}
2038
2039
template <>
2040
54
inline Node RewriteRule<UltPlusOne>::apply(TNode node)
2041
{
2042
54
  Debug("bv-rewrite") << "RewriteRule<UltPlusOne>(" << node << ")" << std::endl;
2043
54
  NodeManager *nm = NodeManager::currentNM();
2044
108
  TNode x = node[0];
2045
108
  TNode y1 = node[1];
2046
108
  TNode y = y1[0].getKind() != kind::CONST_BITVECTOR ? y1[0] : y1[1];
2047
54
  unsigned size = utils::getSize(x);
2048
  Node not_y_eq_1 =
2049
108
      nm->mkNode(kind::NOT, nm->mkNode(kind::EQUAL, y, utils::mkOnes(size)));
2050
  Node not_y_lt_x =
2051
108
      nm->mkNode(kind::NOT, nm->mkNode(kind::BITVECTOR_ULT, y, x));
2052
108
  return nm->mkNode(kind::AND, not_y_eq_1, not_y_lt_x);
2053
}
2054
2055
/* -------------------------------------------------------------------------- */
2056
2057
/**
2058
 * x ^(x-1) = 0 => 1 << sk
2059
 * WARNING: this is an **EQUISATISFIABLE** transformation!
2060
 * Only to be called on top level assertions.
2061
 *
2062
 * @param node
2063
 *
2064
 * @return
2065
 */
2066
template<> inline
2067
14
bool RewriteRule<IsPowerOfTwo>::applies(TNode node) {
2068
14
  if (node.getKind()!= kind::EQUAL) return false;
2069
32
  if (node[0].getKind() != kind::BITVECTOR_AND &&
2070
18
      node[1].getKind() != kind::BITVECTOR_AND)
2071
2
    return false;
2072
48
  if (!utils::isZero(node[0]) &&
2073
36
      !utils::isZero(node[1]))
2074
    return false;
2075
2076
24
  TNode t = !utils::isZero(node[0])? node[0]: node[1];
2077
12
  if (t.getNumChildren() != 2) return false;
2078
24
  TNode a = t[0];
2079
24
  TNode b = t[1];
2080
12
  unsigned size = utils::getSize(t);
2081
12
  if(size < 2) return false;
2082
  Node diff = Rewriter::rewrite(
2083
24
      NodeManager::currentNM()->mkNode(kind::BITVECTOR_SUB, a, b));
2084
12
  return (diff.isConst() && (diff == utils::mkConst(size, 1u) || diff == utils::mkOnes(size)));
2085
}
2086
2087
template <>
2088
6
inline Node RewriteRule<IsPowerOfTwo>::apply(TNode node)
2089
{
2090
12
  Debug("bv-rewrite") << "RewriteRule<IsPowerOfTwo>(" << node << ")"
2091
6
                      << std::endl;
2092
6
  NodeManager *nm = NodeManager::currentNM();
2093
12
  TNode term = utils::isZero(node[0]) ? node[1] : node[0];
2094
12
  TNode a = term[0];
2095
12
  TNode b = term[1];
2096
6
  unsigned size = utils::getSize(term);
2097
12
  Node diff = Rewriter::rewrite(nm->mkNode(kind::BITVECTOR_SUB, a, b));
2098
6
  Assert(diff.isConst());
2099
12
  TNode x = diff == utils::mkConst(size, 1u) ? a : b;
2100
12
  Node one = utils::mkConst(size, 1u);
2101
12
  Node sk = utils::mkVar(size);
2102
12
  Node sh = nm->mkNode(kind::BITVECTOR_SHL, one, sk);
2103
6
  Node x_eq_sh = nm->mkNode(kind::EQUAL, x, sh);
2104
12
  return x_eq_sh;
2105
}
2106
2107
/* -------------------------------------------------------------------------- */
2108
2109
/**
2110
 * Rewrite
2111
 *   sign_extend(x+t,n) * sign_extend(a,m) < sign_extend(x,n) * sign_extend(a,m)
2112
 * to
2113
 *   (and
2114
 *    (not (= t zero))
2115
 *    (not (= a zero))
2116
 *    (= (bvslt (bvadd x t) x) (bvsgt a zero))
2117
 *   )
2118
 *
2119
 * Rewrite
2120
 *   zero_extend(x+t,n) * sign_extend(a,m) < zero_extend(x,n) * sign_extend(a,m)
2121
 * to
2122
 *   (and
2123
 *    (not (= t zero))
2124
 *    (not (= a zero))
2125
 *    (= (bvult (bvadd x t) x) (bvsgt a zero))
2126
 *   )
2127
 * where n and m are sufficiently big to not produce an overflow for
2128
 * the multiplications.
2129
 *
2130
 * These patterns occur in the quantified BV benchmark family 'ranking',
2131
 * where the BV engine struggles due to the high bit widths of the
2132
 * multiplication's operands.
2133
 */
2134
static std::tuple<Node, Node, bool>
2135
37
extract_ext_tuple(TNode node)
2136
{
2137
74
  TNode a = node[0];
2138
74
  TNode b = node[1];
2139
111
  for (unsigned i = 0; i < 2; ++i)
2140
  {
2141
148
    if (a.getKind() == kind::BITVECTOR_CONCAT
2142
29
        && b.getKind() == kind::BITVECTOR_SIGN_EXTEND
2143
74
        && a[0] == utils::mkZero(utils::getSize(a[0]))
2144
74
        && utils::getSize(a[1]) <= utils::getSize(a[0])
2145
148
        && utils::getSize(b[0]) <= utils::getSignExtendAmount(b))
2146
    {
2147
      return std::make_tuple(a[1], b[0], false);
2148
    }
2149
74
    else if (i == 0
2150
37
             && a.getKind() == kind::BITVECTOR_SIGN_EXTEND
2151
             && b.getKind() == kind::BITVECTOR_SIGN_EXTEND
2152
74
             && utils::getSize(a[0]) <= utils::getSignExtendAmount(a)
2153
74
             && utils::getSize(b[0]) <= utils::getSignExtendAmount(b))
2154
    {
2155
      return std::make_tuple(a[0], b[0], true);
2156
    }
2157
74
    std::swap(a, b);
2158
  }
2159
37
  return std::make_tuple(Node::null(), Node::null(), false);
2160
}
2161
2162
/* -------------------------------------------------------------------------- */
2163
2164
template<> inline
2165
119420
bool RewriteRule<MultSltMult>::applies(TNode node)
2166
{
2167
238840
  if (node.getKind() != kind::BITVECTOR_SLT
2168
237454
      || node[0].getKind() != kind::BITVECTOR_MULT
2169
241772
      || node[1].getKind() != kind::BITVECTOR_MULT)
2170
119373
    return false;
2171
2172
47
  if (node[0].getNumChildren() > 2 || node[1].getNumChildren() > 2)
2173
10
    return false;
2174
2175
  bool is_sext_l, is_sext_r;
2176
74
  TNode ml[2], mr[2];
2177
2178
37
  std::tie(ml[0], ml[1], is_sext_l) = extract_ext_tuple(node[0]);
2179
37
  if (ml[0].isNull())
2180
37
    return false;
2181
2182
  std::tie(mr[0], mr[1], is_sext_r) = extract_ext_tuple(node[1]);
2183
  if (mr[0].isNull())
2184
    return false;
2185
2186
  if (is_sext_l != is_sext_r)
2187
    return false;
2188
2189
  TNode addxt, x, a;
2190
  if (ml[0].getKind() == kind::BITVECTOR_PLUS)
2191
  {
2192
    addxt = ml[0];
2193
    a = ml[1];
2194
  }
2195
  else if (ml[1].getKind() == kind::BITVECTOR_PLUS)
2196
  {
2197
    addxt = ml[1];
2198
    a = ml[0];
2199
  }
2200
  else
2201
    return false;
2202
2203
  if (addxt.getNumChildren() > 2)
2204
    return false;
2205
2206
  if (mr[0] == a)
2207
  {
2208
    x = mr[1];
2209
  }
2210
  else if (mr[1] == a)
2211
  {
2212
    x = mr[0];
2213
  }
2214
  else
2215
    return false;
2216
2217
  return (addxt[0] == x || addxt[1] == x);
2218
}
2219
2220
template<> inline
2221
Node RewriteRule<MultSltMult>::apply(TNode node)
2222
{
2223
  bool is_sext;
2224
  TNode ml[2], mr[2];
2225
2226
  std::tie(ml[0], ml[1], is_sext) = extract_ext_tuple(node[0]);
2227
  std::tie(mr[0], mr[1], std::ignore) = extract_ext_tuple(node[1]);
2228
2229
  TNode addxt, x, t, a;
2230
  if (ml[0].getKind() == kind::BITVECTOR_PLUS)
2231
  {
2232
    addxt = ml[0];
2233
    a = ml[1];
2234
  }
2235
  else
2236
  {
2237
    Assert(ml[1].getKind() == kind::BITVECTOR_PLUS);
2238
    addxt = ml[1];
2239
    a = ml[0];
2240
  }
2241
2242
  x = (mr[0] == a) ? mr[1] : mr[0];
2243
  t = (addxt[0] == x) ? addxt[1] : addxt[0];
2244
2245
  NodeManager *nm = NodeManager::currentNM();
2246
  Node zero_t = utils::mkZero(utils::getSize(t));
2247
  Node zero_a = utils::mkZero(utils::getSize(a));
2248
2249
  NodeBuilder<> nb(kind::AND);
2250
  Kind k = is_sext ? kind::BITVECTOR_SLT : kind::BITVECTOR_ULT;
2251
  nb << t.eqNode(zero_t).notNode();
2252
  nb << a.eqNode(zero_a).notNode();
2253
  nb << nm->mkNode(k, addxt, x)
2254
            .eqNode(nm->mkNode(kind::BITVECTOR_SGT, a, zero_a));
2255
  return nb.constructNode();
2256
}
2257
2258
}  // namespace bv
2259
}  // namespace theory
2260
}  // namespace CVC4