GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h Lines: 270 356 75.8 %
Date: 2021-03-22 Branches: 441 1284 34.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_bv_rewrite_rules_operator_elimination.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Yoni Zohar, Liana Hadarean, Aina Niemetz
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
26
namespace CVC4 {
27
namespace theory {
28
namespace bv {
29
30
/*
31
 * This rewrite is not meant to be used by the BV rewriter.
32
 * It is specifically designed for the bv-to-int preprocessing pass.
33
 * Based on Hacker's Delight section 2-2 equation a:
34
 * -x = ~x+1
35
 */
36
template <>
37
1660
inline bool RewriteRule<NegEliminate>::applies(TNode node)
38
{
39
1660
  return (node.getKind() == kind::BITVECTOR_NEG);
40
}
41
42
template <>
43
22
inline Node RewriteRule<NegEliminate>::apply(TNode node)
44
{
45
44
  Debug("bv-rewrite") << "RewriteRule<NegEliminate>(" << node << ")"
46
22
                      << std::endl;
47
22
  NodeManager* nm = NodeManager::currentNM();
48
44
  TNode a = node[0];
49
22
  unsigned size = utils::getSize(a);
50
44
  Node one = utils::mkOne(size);
51
44
  Node nota = nm->mkNode(kind::BITVECTOR_NOT, a);
52
  Node bvadd =
53
22
      nm->mkNode(kind::BITVECTOR_PLUS, nota, one);
54
44
  return bvadd;
55
}
56
57
/*
58
 * This rewrite is not meant to be used by the BV rewriter.
59
 * It is specifically designed for the bv-to-int preprocessing pass.
60
 * Based on Hacker's Delight section 2-2 equation h:
61
 * x+y = x|y + x&y
62
 */
63
template <>
64
1658
inline bool RewriteRule<OrEliminate>::applies(TNode node)
65
{
66
1658
  return (node.getKind() == kind::BITVECTOR_OR);
67
}
68
69
template <>
70
20
inline Node RewriteRule<OrEliminate>::apply(TNode node)
71
{
72
40
  Debug("bv-rewrite") << "RewriteRule<OrEliminate>(" << node << ")"
73
20
                      << std::endl;
74
20
  NodeManager* nm = NodeManager::currentNM();
75
40
  TNode a = node[0];
76
40
  TNode b = node[1];
77
40
  Node bvadd = nm->mkNode(kind::BITVECTOR_PLUS, a, b);
78
40
  Node bvand = nm->mkNode(kind::BITVECTOR_AND, a, b);
79
  Node result =
80
20
      nm->mkNode(kind::BITVECTOR_SUB, bvadd, bvand);
81
40
  return result;
82
}
83
84
/*
85
 * This rewrite is not meant to be used by the BV rewriter.
86
 * It is specifically designed for the bv-to-int preprocessing pass.
87
 * Based on Hacker's Delight section 2-2 equation n:
88
 * x xor y = x|y - x&y
89
 */
90
template <>
91
1638
inline bool RewriteRule<XorEliminate>::applies(TNode node)
92
{
93
1638
  return (node.getKind() == kind::BITVECTOR_XOR);
94
}
95
96
template <>
97
inline Node RewriteRule<XorEliminate>::apply(TNode node)
98
{
99
  Debug("bv-rewrite") << "RewriteRule<XorEliminate>(" << node << ")"
100
                      << std::endl;
101
  NodeManager* nm = NodeManager::currentNM();
102
  TNode a = node[0];
103
  TNode b = node[1];
104
  Node bvor = nm->mkNode(kind::BITVECTOR_OR, a, b);
105
  Node bvand = nm->mkNode(kind::BITVECTOR_AND, a, b);
106
  Node result = nm->mkNode(kind::BITVECTOR_SUB, bvor, bvand);
107
  return result;
108
}
109
110
template <>
111
7227
inline bool RewriteRule<UgtEliminate>::applies(TNode node)
112
{
113
7227
  return (node.getKind() == kind::BITVECTOR_UGT);
114
}
115
116
template <>
117
3609
inline Node RewriteRule<UgtEliminate>::apply(TNode node)
118
{
119
7218
  Debug("bv-rewrite") << "RewriteRule<UgtEliminate>(" << node << ")"
120
3609
                      << std::endl;
121
7218
  TNode a = node[0];
122
7218
  TNode b = node[1];
123
3609
  Node result = NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, b, a);
124
7218
  return result;
125
}
126
127
template <>
128
6668
inline bool RewriteRule<UgeEliminate>::applies(TNode node)
129
{
130
6668
  return (node.getKind() == kind::BITVECTOR_UGE);
131
}
132
133
template <>
134
3334
inline Node RewriteRule<UgeEliminate>::apply(TNode node)
135
{
136
6668
  Debug("bv-rewrite") << "RewriteRule<UgeEliminate>(" << node << ")"
137
3334
                      << std::endl;
138
6668
  TNode a = node[0];
139
6668
  TNode b = node[1];
140
3334
  Node result = NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULE, b, a);
141
6668
  return result;
142
}
143
144
template <>
145
8940
inline bool RewriteRule<SgtEliminate>::applies(TNode node)
146
{
147
8940
  return (node.getKind() == kind::BITVECTOR_SGT);
148
}
149
150
template <>
151
3651
inline Node RewriteRule<SgtEliminate>::apply(TNode node)
152
{
153
7302
  Debug("bv-rewrite") << "RewriteRule<SgtEliminate>(" << node << ")"
154
3651
                      << std::endl;
155
7302
  TNode a = node[0];
156
7302
  TNode b = node[1];
157
3651
  Node result = NodeManager::currentNM()->mkNode(kind::BITVECTOR_SLT, b, a);
158
7302
  return result;
159
}
160
161
template <>
162
8526
inline bool RewriteRule<SgeEliminate>::applies(TNode node)
163
{
164
8526
  return (node.getKind() == kind::BITVECTOR_SGE);
165
}
166
167
template <>
168
3444
inline Node RewriteRule<SgeEliminate>::apply(TNode node)
169
{
170
6888
  Debug("bv-rewrite") << "RewriteRule<SgeEliminate>(" << node << ")"
171
3444
                      << std::endl;
172
6888
  TNode a = node[0];
173
6888
  TNode b = node[1];
174
3444
  Node result = NodeManager::currentNM()->mkNode(kind::BITVECTOR_SLE, b, a);
175
6888
  return result;
176
}
177
178
template <>
179
1653
inline bool RewriteRule<SltEliminate>::applies(TNode node)
180
{
181
1653
  return (node.getKind() == kind::BITVECTOR_SLT);
182
}
183
184
template <>
185
15
inline Node RewriteRule<SltEliminate>::apply(TNode node)
186
{
187
30
  Debug("bv-rewrite") << "RewriteRule<SltEliminate>(" << node << ")"
188
15
                      << std::endl;
189
15
  NodeManager *nm = NodeManager::currentNM();
190
15
  unsigned size = utils::getSize(node[0]);
191
30
  Integer val = Integer(1).multiplyByPow2(size - 1);
192
30
  Node pow_two = utils::mkConst(size, val);
193
30
  Node a = nm->mkNode(kind::BITVECTOR_PLUS, node[0], pow_two);
194
30
  Node b = nm->mkNode(kind::BITVECTOR_PLUS, node[1], pow_two);
195
196
30
  return nm->mkNode(kind::BITVECTOR_ULT, a, b);
197
}
198
199
template <>
200
15534
inline bool RewriteRule<SleEliminate>::applies(TNode node)
201
{
202
15534
  return (node.getKind() == kind::BITVECTOR_SLE);
203
}
204
205
template <>
206
6935
inline Node RewriteRule<SleEliminate>::apply(TNode node)
207
{
208
13870
  Debug("bv-rewrite") << "RewriteRule<SleEliminate>(" << node << ")"
209
6935
                      << std::endl;
210
6935
  NodeManager *nm = NodeManager::currentNM();
211
13870
  TNode a = node[0];
212
13870
  TNode b = node[1];
213
13870
  Node b_slt_a = nm->mkNode(kind::BITVECTOR_SLT, b, a);
214
13870
  return nm->mkNode(kind::NOT, b_slt_a);
215
}
216
217
template <>
218
13183
inline bool RewriteRule<UleEliminate>::applies(TNode node)
219
{
220
13183
  return (node.getKind() == kind::BITVECTOR_ULE);
221
}
222
223
template <>
224
6518
inline Node RewriteRule<UleEliminate>::apply(TNode node)
225
{
226
13036
  Debug("bv-rewrite") << "RewriteRule<UleEliminate>(" << node << ")"
227
6518
                      << std::endl;
228
6518
  NodeManager *nm = NodeManager::currentNM();
229
13036
  TNode a = node[0];
230
13036
  TNode b = node[1];
231
13036
  Node b_ult_a = nm->mkNode(kind::BITVECTOR_ULT, b, a);
232
13036
  return nm->mkNode(kind::NOT, b_ult_a);
233
}
234
235
template <>
236
1638
inline bool RewriteRule<CompEliminate>::applies(TNode node)
237
{
238
1638
  return (node.getKind() == kind::BITVECTOR_COMP);
239
}
240
241
template <>
242
inline Node RewriteRule<CompEliminate>::apply(TNode node)
243
{
244
  Debug("bv-rewrite") << "RewriteRule<CompEliminate>(" << node << ")"
245
                      << std::endl;
246
  NodeManager *nm = NodeManager::currentNM();
247
  Node comp = nm->mkNode(kind::EQUAL, node[0], node[1]);
248
  Node one = utils::mkConst(1, 1);
249
  Node zero = utils::mkConst(1, 0);
250
251
  return nm->mkNode(kind::ITE, comp, one, zero);
252
}
253
254
template <>
255
6494
inline bool RewriteRule<SubEliminate>::applies(TNode node)
256
{
257
6494
  return (node.getKind() == kind::BITVECTOR_SUB);
258
}
259
260
template <>
261
2438
inline Node RewriteRule<SubEliminate>::apply(TNode node)
262
{
263
4876
  Debug("bv-rewrite") << "RewriteRule<SubEliminate>(" << node << ")"
264
2438
                      << std::endl;
265
2438
  NodeManager *nm = NodeManager::currentNM();
266
4876
  Node negb = nm->mkNode(kind::BITVECTOR_NEG, node[1]);
267
4876
  Node a = node[0];
268
269
4876
  return nm->mkNode(kind::BITVECTOR_PLUS, a, negb);
270
}
271
272
template <>
273
3232
inline bool RewriteRule<RepeatEliminate>::applies(TNode node)
274
{
275
3232
  return (node.getKind() == kind::BITVECTOR_REPEAT);
276
}
277
278
template <>
279
797
inline Node RewriteRule<RepeatEliminate>::apply(TNode node)
280
{
281
797
  Debug("bv-rewrite") << "RewriteRule<RepeatEliminate>(" << node << ")" << std::endl;
282
1594
  TNode a = node[0];
283
  unsigned amount =
284
797
      node.getOperator().getConst<BitVectorRepeat>().d_repeatAmount;
285
797
  Assert(amount >= 1);
286
797
  if(amount == 1) {
287
484
    return a;
288
  }
289
626
  NodeBuilder<> result(kind::BITVECTOR_CONCAT);
290
1662
  for(unsigned i = 0; i < amount; ++i) {
291
1349
    result << node[0];
292
  }
293
626
  Node resultNode = result;
294
313
  return resultNode;
295
}
296
297
template <>
298
2994
inline bool RewriteRule<RotateLeftEliminate>::applies(TNode node)
299
{
300
2994
  return (node.getKind() == kind::BITVECTOR_ROTATE_LEFT);
301
}
302
303
template <>
304
678
inline Node RewriteRule<RotateLeftEliminate>::apply(TNode node)
305
{
306
678
  Debug("bv-rewrite") << "RewriteRule<RotateLeftEliminate>(" << node << ")" << std::endl;
307
1356
  TNode a = node[0];
308
  unsigned amount =
309
678
      node.getOperator().getConst<BitVectorRotateLeft>().d_rotateLeftAmount;
310
678
  amount = amount % utils::getSize(a);
311
678
  if (amount == 0) {
312
415
    return a;
313
  }
314
315
526
  Node left   = utils::mkExtract(a, utils::getSize(a)-1 - amount, 0);
316
526
  Node right  = utils::mkExtract(a, utils::getSize(a) -1, utils::getSize(a) - amount);
317
526
  Node result = utils::mkConcat(left, right);
318
319
263
  return result;
320
}
321
322
template <>
323
3264
inline bool RewriteRule<RotateRightEliminate>::applies(TNode node)
324
{
325
3264
  return (node.getKind() == kind::BITVECTOR_ROTATE_RIGHT);
326
}
327
328
template <>
329
813
inline Node RewriteRule<RotateRightEliminate>::apply(TNode node)
330
{
331
813
  Debug("bv-rewrite") << "RewriteRule<RotateRightEliminate>(" << node << ")" << std::endl;
332
1626
  TNode a = node[0];
333
  unsigned amount =
334
813
      node.getOperator().getConst<BitVectorRotateRight>().d_rotateRightAmount;
335
813
  amount = amount % utils::getSize(a);
336
813
  if (amount == 0) {
337
366
    return a;
338
  }
339
340
894
  Node left  = utils::mkExtract(a, amount - 1, 0);
341
894
  Node right = utils::mkExtract(a, utils::getSize(a)-1, amount);
342
894
  Node result = utils::mkConcat(left, right);
343
344
447
  return result;
345
}
346
347
template <>
348
360
inline bool RewriteRule<BVToNatEliminate>::applies(TNode node)
349
{
350
360
  return (node.getKind() == kind::BITVECTOR_TO_NAT);
351
}
352
353
template <>
354
180
inline Node RewriteRule<BVToNatEliminate>::apply(TNode node)
355
{
356
180
  Debug("bv-rewrite") << "RewriteRule<BVToNatEliminate>(" << node << ")" << std::endl;
357
358
  //if( node[0].isConst() ){
359
    //TODO? direct computation instead of term construction+rewriting
360
  //}
361
180
  return utils::eliminateBv2Nat(node);
362
}
363
364
template <>
365
502
inline bool RewriteRule<IntToBVEliminate>::applies(TNode node)
366
{
367
502
  return (node.getKind() == kind::INT_TO_BITVECTOR);
368
}
369
370
template <>
371
251
inline Node RewriteRule<IntToBVEliminate>::apply(TNode node)
372
{
373
251
  Debug("bv-rewrite") << "RewriteRule<IntToBVEliminate>(" << node << ")" << std::endl;
374
375
  //if( node[0].isConst() ){
376
    //TODO? direct computation instead of term construction+rewriting
377
  //}
378
251
  return utils::eliminateInt2Bv(node);
379
}
380
381
template <>
382
2898
inline bool RewriteRule<NandEliminate>::applies(TNode node)
383
{
384
4158
  return (node.getKind() == kind::BITVECTOR_NAND &&
385
4158
          node.getNumChildren() == 2);
386
}
387
388
template <>
389
630
inline Node RewriteRule<NandEliminate>::apply(TNode node)
390
{
391
1260
  Debug("bv-rewrite") << "RewriteRule<NandEliminate>(" << node << ")"
392
630
                      << std::endl;
393
630
  NodeManager *nm = NodeManager::currentNM();
394
1260
  TNode a = node[0];
395
1260
  TNode b = node[1];
396
1260
  Node andNode = nm->mkNode(kind::BITVECTOR_AND, a, b);
397
630
  Node result = nm->mkNode(kind::BITVECTOR_NOT, andNode);
398
1260
  return result;
399
}
400
401
template <>
402
3260
inline bool RewriteRule<NorEliminate>::applies(TNode node)
403
{
404
3260
  return (node.getKind() == kind::BITVECTOR_NOR && node.getNumChildren() == 2);
405
}
406
407
template <>
408
811
inline Node RewriteRule<NorEliminate>::apply(TNode node)
409
{
410
1622
  Debug("bv-rewrite") << "RewriteRule<NorEliminate>(" << node << ")"
411
811
                      << std::endl;
412
811
  NodeManager *nm = NodeManager::currentNM();
413
1622
  TNode a = node[0];
414
1622
  TNode b = node[1];
415
1622
  Node orNode = nm->mkNode(kind::BITVECTOR_OR, a, b);
416
811
  Node result = nm->mkNode(kind::BITVECTOR_NOT, orNode);
417
1622
  return result;
418
}
419
420
template <>
421
3502
inline bool RewriteRule<XnorEliminate>::applies(TNode node)
422
{
423
5366
  return (node.getKind() == kind::BITVECTOR_XNOR &&
424
5366
          node.getNumChildren() == 2);
425
}
426
427
template <>
428
932
inline Node RewriteRule<XnorEliminate>::apply(TNode node)
429
{
430
1864
  Debug("bv-rewrite") << "RewriteRule<XnorEliminate>(" << node << ")"
431
932
                      << std::endl;
432
932
  NodeManager *nm = NodeManager::currentNM();
433
1864
  TNode a = node[0];
434
1864
  TNode b = node[1];
435
1864
  Node xorNode = nm->mkNode(kind::BITVECTOR_XOR, a, b);
436
932
  Node result = nm->mkNode(kind::BITVECTOR_NOT, xorNode);
437
1864
  return result;
438
}
439
440
template <>
441
310
inline bool RewriteRule<SdivEliminate>::applies(TNode node)
442
{
443
310
  return (node.getKind() == kind::BITVECTOR_SDIV);
444
}
445
446
template <>
447
155
inline Node RewriteRule<SdivEliminate>::apply(TNode node)
448
{
449
310
  Debug("bv-rewrite") << "RewriteRule<SdivEliminate>(" << node << ")"
450
155
                      << std::endl;
451
452
155
  NodeManager *nm = NodeManager::currentNM();
453
310
  TNode a = node[0];
454
310
  TNode b = node[1];
455
155
  unsigned size = utils::getSize(a);
456
457
310
  Node one = utils::mkConst(1, 1);
458
  Node a_lt_0 =
459
310
      nm->mkNode(kind::EQUAL, utils::mkExtract(a, size - 1, size - 1), one);
460
  Node b_lt_0 =
461
310
      nm->mkNode(kind::EQUAL, utils::mkExtract(b, size - 1, size - 1), one);
462
  Node abs_a =
463
310
      nm->mkNode(kind::ITE, a_lt_0, nm->mkNode(kind::BITVECTOR_NEG, a), a);
464
  Node abs_b =
465
310
      nm->mkNode(kind::ITE, b_lt_0, nm->mkNode(kind::BITVECTOR_NEG, b), b);
466
467
310
  Node a_udiv_b = nm->mkNode(kind::BITVECTOR_UDIV, abs_a, abs_b);
468
310
  Node neg_result = nm->mkNode(kind::BITVECTOR_NEG, a_udiv_b);
469
470
310
  Node condition = nm->mkNode(kind::XOR, a_lt_0, b_lt_0);
471
155
  Node result = nm->mkNode(kind::ITE, condition, neg_result, a_udiv_b);
472
473
310
  return result;
474
}
475
476
/*
477
 * This rewrite is not meant to be used by the BV rewriter
478
 * It is specifically designed for the bv-to-int preprocessing pass.
479
 * Similar to ordinary sdiv elimination.
480
 * The sign-check is done with bvult instead of bit-extraction.
481
 */
482
template <>
483
1638
inline bool RewriteRule<SdivEliminateFewerBitwiseOps>::applies(TNode node)
484
{
485
1638
  return (node.getKind() == kind::BITVECTOR_SDIV);
486
}
487
488
template <>
489
inline Node RewriteRule<SdivEliminateFewerBitwiseOps>::apply(TNode node)
490
{
491
  Debug("bv-rewrite") << "RewriteRule<SdivEliminateFewerBitwiseOps>(" << node
492
                      << ")" << std::endl;
493
494
  NodeManager* nm = NodeManager::currentNM();
495
  TNode a = node[0];
496
  TNode b = node[1];
497
  unsigned size = utils::getSize(a);
498
  Node a_lt_0 = nm->mkNode(kind::BITVECTOR_UGE, a, utils::mkMinSigned(size));
499
  Node b_lt_0 = nm->mkNode(kind::BITVECTOR_UGE, b, utils::mkMinSigned(size));
500
  Node abs_a =
501
      nm->mkNode(kind::ITE, a_lt_0, nm->mkNode(kind::BITVECTOR_NEG, a), a);
502
  Node abs_b =
503
      nm->mkNode(kind::ITE, b_lt_0, nm->mkNode(kind::BITVECTOR_NEG, b), b);
504
505
  Node a_udiv_b = nm->mkNode(kind::BITVECTOR_UDIV, abs_a, abs_b);
506
  Node neg_result = nm->mkNode(kind::BITVECTOR_NEG, a_udiv_b);
507
508
  Node result = nm->mkNode(kind::ITE, a_lt_0.xorNode(b_lt_0), neg_result, a_udiv_b);
509
510
  return result;
511
}
512
513
template <>
514
154
inline bool RewriteRule<SremEliminate>::applies(TNode node)
515
{
516
154
  return (node.getKind() == kind::BITVECTOR_SREM);
517
}
518
519
template <>
520
77
inline Node RewriteRule<SremEliminate>::apply(TNode node)
521
{
522
154
  Debug("bv-rewrite") << "RewriteRule<SremEliminate>(" << node << ")"
523
77
                      << std::endl;
524
77
  NodeManager *nm = NodeManager::currentNM();
525
154
  TNode a = node[0];
526
154
  TNode b = node[1];
527
77
  unsigned size = utils::getSize(a);
528
529
154
  Node one = utils::mkConst(1, 1);
530
  Node a_lt_0 =
531
154
      nm->mkNode(kind::EQUAL, utils::mkExtract(a, size - 1, size - 1), one);
532
  Node b_lt_0 =
533
154
      nm->mkNode(kind::EQUAL, utils::mkExtract(b, size - 1, size - 1), one);
534
  Node abs_a =
535
154
      nm->mkNode(kind::ITE, a_lt_0, nm->mkNode(kind::BITVECTOR_NEG, a), a);
536
  Node abs_b =
537
154
      nm->mkNode(kind::ITE, b_lt_0, nm->mkNode(kind::BITVECTOR_NEG, b), b);
538
539
154
  Node a_urem_b = nm->mkNode(kind::BITVECTOR_UREM, abs_a, abs_b);
540
154
  Node neg_result = nm->mkNode(kind::BITVECTOR_NEG, a_urem_b);
541
542
77
  Node result = nm->mkNode(kind::ITE, a_lt_0, neg_result, a_urem_b);
543
544
154
  return result;
545
}
546
547
/*
548
 * This rewrite is not meant to be used by the BV rewriter
549
 * It is specifically designed for the bv-to-int preprocessing pass.
550
 * Similar to ordinary srem elimination.
551
 * The sign-check is done with bvult instead of bit-extraction.
552
 */
553
template <>
554
1638
inline bool RewriteRule<SremEliminateFewerBitwiseOps>::applies(TNode node)
555
{
556
1638
  return (node.getKind() == kind::BITVECTOR_SREM);
557
}
558
559
template <>
560
inline Node RewriteRule<SremEliminateFewerBitwiseOps>::apply(TNode node)
561
{
562
  Debug("bv-rewrite") << "RewriteRule<SremEliminateFewerBitwiseOps>(" << node
563
                      << ")" << std::endl;
564
  NodeManager* nm = NodeManager::currentNM();
565
  TNode a = node[0];
566
  TNode b = node[1];
567
  unsigned size = utils::getSize(a);
568
  Node a_lt_0 = nm->mkNode(kind::BITVECTOR_UGE, a, utils::mkMinSigned(size));
569
  Node b_lt_0 = nm->mkNode(kind::BITVECTOR_UGE, b, utils::mkMinSigned(size));
570
  Node abs_a =
571
      nm->mkNode(kind::ITE, a_lt_0, nm->mkNode(kind::BITVECTOR_NEG, a), a);
572
  Node abs_b =
573
      nm->mkNode(kind::ITE, b_lt_0, nm->mkNode(kind::BITVECTOR_NEG, b), b);
574
  Node a_urem_b = nm->mkNode(kind::BITVECTOR_UREM, abs_a, abs_b);
575
  Node neg_result = nm->mkNode(kind::BITVECTOR_NEG, a_urem_b);
576
577
  Node result = nm->mkNode(kind::ITE, a_lt_0, neg_result, a_urem_b);
578
579
  return result;
580
}
581
582
template <>
583
224
inline bool RewriteRule<SmodEliminate>::applies(TNode node)
584
{
585
224
  return (node.getKind() == kind::BITVECTOR_SMOD);
586
}
587
588
template <>
589
112
inline Node RewriteRule<SmodEliminate>::apply(TNode node)
590
{
591
224
  Debug("bv-rewrite") << "RewriteRule<SmodEliminate>(" << node << ")"
592
112
                      << std::endl;
593
112
  NodeManager *nm = NodeManager::currentNM();
594
224
  TNode s = node[0];
595
224
  TNode t = node[1];
596
112
  unsigned size = utils::getSize(s);
597
598
  // (bvsmod s t) abbreviates
599
  //     (let ((?msb_s ((_ extract |m-1| |m-1|) s))
600
  //           (?msb_t ((_ extract |m-1| |m-1|) t)))
601
  //       (let ((abs_s (ite (= ?msb_s #b0) s (bvneg s)))
602
  //             (abs_t (ite (= ?msb_t #b0) t (bvneg t))))
603
  //         (let ((u (bvurem abs_s abs_t)))
604
  //           (ite (= u (_ bv0 m))
605
  //                u
606
  //           (ite (and (= ?msb_s #b0) (= ?msb_t #b0))
607
  //                u
608
  //           (ite (and (= ?msb_s #b1) (= ?msb_t #b0))
609
  //                (bvadd (bvneg u) t)
610
  //           (ite (and (= ?msb_s #b0) (= ?msb_t #b1))
611
  //                (bvadd u t)
612
  //                (bvneg u))))))))
613
614
224
  Node msb_s = utils::mkExtract(s, size - 1, size - 1);
615
224
  Node msb_t = utils::mkExtract(t, size - 1, size - 1);
616
617
224
  Node bit1 = utils::mkConst(1, 1);
618
224
  Node bit0 = utils::mkConst(1, 0);
619
620
  Node abs_s =
621
224
      msb_s.eqNode(bit0).iteNode(s, nm->mkNode(kind::BITVECTOR_NEG, s));
622
  Node abs_t =
623
224
      msb_t.eqNode(bit0).iteNode(t, nm->mkNode(kind::BITVECTOR_NEG, t));
624
625
224
  Node u = nm->mkNode(kind::BITVECTOR_UREM, abs_s, abs_t);
626
224
  Node neg_u = nm->mkNode(kind::BITVECTOR_NEG, u);
627
628
224
  Node cond0 = u.eqNode(utils::mkConst(size, 0));
629
224
  Node cond1 = msb_s.eqNode(bit0).andNode(msb_t.eqNode(bit0));
630
224
  Node cond2 = msb_s.eqNode(bit1).andNode(msb_t.eqNode(bit0));
631
224
  Node cond3 = msb_s.eqNode(bit0).andNode(msb_t.eqNode(bit1));
632
633
  Node result = cond0.iteNode(
634
      u,
635
224
      cond1.iteNode(
636
          u,
637
224
          cond2.iteNode(
638
224
              nm->mkNode(kind::BITVECTOR_PLUS, neg_u, t),
639
336
              cond3.iteNode(nm->mkNode(kind::BITVECTOR_PLUS, u, t), neg_u))));
640
641
224
  return result;
642
}
643
644
/*
645
 * This rewrite is not meant to be used by the BV rewriter
646
 * It is specifically designed for the bv-to-int preprocessing pass.
647
 * Similar to ordinary smod elimination.
648
 * The sign-check is done with bvult instead of bit-extraction.
649
 */
650
template <>
651
1638
inline bool RewriteRule<SmodEliminateFewerBitwiseOps>::applies(TNode node)
652
{
653
1638
  return (node.getKind() == kind::BITVECTOR_SMOD);
654
}
655
656
template <>
657
inline Node RewriteRule<SmodEliminateFewerBitwiseOps>::apply(TNode node)
658
{
659
  Debug("bv-rewrite") << "RewriteRule<SmodEliminate>(" << node << ")"
660
                      << std::endl;
661
  NodeManager* nm = NodeManager::currentNM();
662
  TNode s = node[0];
663
  TNode t = node[1];
664
  unsigned size = utils::getSize(s);
665
666
  /*
667
   * (bvsmod s t) abbreviates
668
   *    (let ((?msb_s ((_ extract |m-1| |m-1|) s))
669
   *          (?msb_t ((_ extract |m-1| |m-1|) t)))
670
   *      (let ((abs_s (ite (= ?msb_s #b0) s (bvneg s)))
671
   *            (abs_t (ite (= ?msb_t #b0) t (bvneg t))))
672
   *        (let ((u (bvurem abs_s abs_t)))
673
   *          (ite (= u (_ bv0 m))
674
   *               u
675
   *          (ite (and (= ?msb_s #b0) (= ?msb_t #b0))
676
   *               u
677
   *          (ite (and (= ?msb_s #b1) (= ?msb_t #b0))
678
   *               (bvadd (bvneg u) t)
679
   *          (ite (and (= ?msb_s #b0) (= ?msb_t #b1))
680
   *               (bvadd u t)
681
   *               (bvneg u))))))))
682
   */
683
684
  Node s_lt_0 = nm->mkNode(kind::BITVECTOR_UGE, s, utils::mkMinSigned(size));
685
  Node t_lt_0 = nm->mkNode(kind::BITVECTOR_UGE, t, utils::mkMinSigned(size));
686
  Node abs_s =
687
      nm->mkNode(kind::ITE, s_lt_0, nm->mkNode(kind::BITVECTOR_NEG, s), s);
688
  Node abs_t =
689
      nm->mkNode(kind::ITE, t_lt_0, nm->mkNode(kind::BITVECTOR_NEG, t), t);
690
691
  Node u = nm->mkNode(kind::BITVECTOR_UREM, abs_s, abs_t);
692
  Node neg_u = nm->mkNode(kind::BITVECTOR_NEG, u);
693
694
  Node cond0 = u.eqNode(utils::mkConst(size, 0));
695
  Node cond1 =
696
      nm->mkNode(kind::NOT, s_lt_0).andNode(nm->mkNode(kind::NOT, t_lt_0));
697
  Node cond2 = s_lt_0.andNode(nm->mkNode(kind::NOT, t_lt_0));
698
  Node cond3 = nm->mkNode(kind::NOT, s_lt_0).andNode(t_lt_0);
699
700
  Node result = cond0.iteNode(
701
      u,
702
      cond1.iteNode(
703
          u,
704
          cond2.iteNode(
705
              nm->mkNode(kind::BITVECTOR_PLUS, neg_u, t),
706
              cond3.iteNode(nm->mkNode(kind::BITVECTOR_PLUS, u, t), neg_u))));
707
708
  return result;
709
}
710
711
template <>
712
21502
inline bool RewriteRule<ZeroExtendEliminate>::applies(TNode node)
713
{
714
21502
  return (node.getKind() == kind::BITVECTOR_ZERO_EXTEND);
715
}
716
717
template <>
718
10751
inline Node RewriteRule<ZeroExtendEliminate>::apply(TNode node)
719
{
720
10751
  Debug("bv-rewrite") << "RewriteRule<ZeroExtendEliminate>(" << node << ")" << std::endl;
721
722
21502
  TNode bv = node[0];
723
  unsigned amount =
724
10751
      node.getOperator().getConst<BitVectorZeroExtend>().d_zeroExtendAmount;
725
10751
  if (amount == 0) {
726
438
    return node[0];
727
  }
728
20626
  Node zero = utils::mkConst(amount, 0);
729
20626
  Node result = utils::mkConcat(zero, node[0]);
730
731
10313
  return result;
732
}
733
734
template <>
735
inline bool RewriteRule<SignExtendEliminate>::applies(TNode node)
736
{
737
  return (node.getKind() == kind::BITVECTOR_SIGN_EXTEND);
738
}
739
740
template <>
741
inline Node RewriteRule<SignExtendEliminate>::apply(TNode node)
742
{
743
  Debug("bv-rewrite") << "RewriteRule<SignExtendEliminate>(" << node << ")" << std::endl;
744
745
  unsigned amount =
746
      node.getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount;
747
  if(amount == 0) {
748
    return node[0];
749
  }
750
  unsigned size = utils::getSize(node[0]);
751
  Node sign_bit = utils::mkExtract(node[0], size-1, size-1);
752
  Node extension = utils::mkConcat(sign_bit, amount);
753
754
  return utils::mkConcat(extension, node[0]);
755
}
756
757
template <>
758
inline bool RewriteRule<RedorEliminate>::applies(TNode node)
759
{
760
  return (node.getKind() == kind::BITVECTOR_REDOR);
761
}
762
763
template <>
764
inline Node RewriteRule<RedorEliminate>::apply(TNode node)
765
{
766
  Debug("bv-rewrite") << "RewriteRule<RedorEliminate>(" << node << ")" << std::endl;
767
  TNode a = node[0];
768
  unsigned size = utils::getSize(node[0]);
769
  Node result = NodeManager::currentNM()->mkNode(kind::EQUAL, a, utils::mkConst( size, 0 ) );
770
  return result.negate();
771
}
772
773
template <>
774
inline bool RewriteRule<RedandEliminate>::applies(TNode node)
775
{
776
  return (node.getKind() == kind::BITVECTOR_REDAND);
777
}
778
779
template <>
780
inline Node RewriteRule<RedandEliminate>::apply(TNode node)
781
{
782
  Debug("bv-rewrite") << "RewriteRule<RedandEliminate>(" << node << ")" << std::endl;
783
  TNode a = node[0];
784
  unsigned size = utils::getSize(node[0]);
785
  Node result = NodeManager::currentNM()->mkNode(kind::EQUAL, a, utils::mkOnes( size ) );
786
  return result;
787
}
788
789
}
790
}
791
}