GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/theory_bv_rewriter.cpp Lines: 297 314 94.6 %
Date: 2021-03-23 Branches: 446 884 50.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_bv_rewriter.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Liana Hadarean, Aina Niemetz, Dejan Jovanovic
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 "options/bv_options.h"
19
#include "theory/bv/theory_bv_rewrite_rules.h"
20
#include "theory/bv/theory_bv_rewrite_rules_constant_evaluation.h"
21
#include "theory/bv/theory_bv_rewrite_rules_core.h"
22
#include "theory/bv/theory_bv_rewrite_rules_normalization.h"
23
#include "theory/bv/theory_bv_rewrite_rules_operator_elimination.h"
24
#include "theory/bv/theory_bv_rewrite_rules_simplification.h"
25
#include "theory/bv/theory_bv_rewriter.h"
26
#include "theory/theory.h"
27
28
using namespace CVC4;
29
using namespace CVC4::theory;
30
using namespace CVC4::theory::bv;
31
32
8997
TheoryBVRewriter::TheoryBVRewriter() { initializeRewrites(); }
33
34
1556179
RewriteResponse TheoryBVRewriter::preRewrite(TNode node) {
35
1556179
  RewriteResponse res = d_rewriteTable[node.getKind()](node, true);
36
1556179
  if (res.d_node != node)
37
  {
38
491090
    Debug("bitvector-rewrite") << "TheoryBV::preRewrite    " << node << std::endl;
39
982180
    Debug("bitvector-rewrite")
40
491090
        << "TheoryBV::preRewrite to " << res.d_node << std::endl;
41
  }
42
1556179
  return res;
43
}
44
45
1853418
RewriteResponse TheoryBVRewriter::postRewrite(TNode node) {
46
1853418
  RewriteResponse res = d_rewriteTable[node.getKind()](node, false);
47
1853418
  if (res.d_node != node)
48
  {
49
410049
    Debug("bitvector-rewrite") << "TheoryBV::postRewrite    " << node << std::endl;
50
820098
    Debug("bitvector-rewrite")
51
410049
        << "TheoryBV::postRewrite to " << res.d_node << std::endl;
52
  }
53
1853418
  return res;
54
}
55
56
555135
RewriteResponse TheoryBVRewriter::RewriteBitOf(TNode node, bool prerewrite)
57
{
58
1110270
  Node resultNode = LinearRewriteStrategy<RewriteRule<BitOfConst>>::apply(node);
59
1110270
  return RewriteResponse(REWRITE_DONE, resultNode);
60
}
61
62
112746
RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool prerewrite) {
63
  // reduce common subexpressions on both sides
64
  Node resultNode = LinearRewriteStrategy
65
    < RewriteRule<EvalUlt>, // if both arguments are constants evaluates
66
      RewriteRule<UltZero>, // a < 0 rewrites to false,
67
      RewriteRule<SignExtendUltConst>,
68
      RewriteRule<ZeroExtendUltConst>
69
225492
       >::apply(node);
70
71
112746
  return RewriteResponse(resultNode == node ? REWRITE_DONE : REWRITE_AGAIN_FULL,
72
338238
                         resultNode);
73
}
74
75
3326
RewriteResponse TheoryBVRewriter::RewriteUltBv(TNode node, bool prerewrite) {
76
  // reduce common subexpressions on both sides
77
  Node resultNode = LinearRewriteStrategy
78
    < RewriteRule<EvalUltBv>
79
6652
       >::apply(node);
80
81
6652
  return RewriteResponse(REWRITE_DONE, resultNode);
82
}
83
84
85
119420
RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node, bool prerewrite){
86
  Node resultNode = LinearRewriteStrategy
87
    < RewriteRule<EvalSlt>,
88
      RewriteRule<MultSltMult>
89
238840
       >::apply(node);
90
91
238840
  return RewriteResponse(REWRITE_DONE, resultNode);
92
93
  // Node resultNode = LinearRewriteStrategy
94
  //   < RewriteRule < SltEliminate >
95
  //     // a <_s b ==> a + 2^{n-1} <_u b + 2^{n-1}
96
  //     >::apply(node);
97
98
  // return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
99
}
100
101
6425
RewriteResponse TheoryBVRewriter::RewriteSltBv(TNode node, bool prerewrite){
102
  Node resultNode = LinearRewriteStrategy
103
    < RewriteRule < EvalSltBv >
104
12850
       >::apply(node);
105
106
12850
  return RewriteResponse(REWRITE_DONE, resultNode);
107
}
108
109
6665
RewriteResponse TheoryBVRewriter::RewriteUle(TNode node, bool prerewrite){
110
  Node resultNode = LinearRewriteStrategy
111
    < RewriteRule<EvalUle>,
112
      RewriteRule<UleMax>,
113
      RewriteRule<ZeroUle>,
114
      RewriteRule<UleZero>,
115
      RewriteRule<UleSelf>,
116
      RewriteRule<UleEliminate>
117
13330
      >::apply(node);
118
13330
  return RewriteResponse(resultNode == node ? REWRITE_DONE : REWRITE_AGAIN, resultNode);
119
}
120
121
6961
RewriteResponse TheoryBVRewriter::RewriteSle(TNode node, bool prerewrite){
122
  Node resultNode = LinearRewriteStrategy
123
    < RewriteRule <EvalSle>,
124
      RewriteRule <SleEliminate>
125
13922
      >::apply(node);
126
13922
  return RewriteResponse(resultNode == node? REWRITE_DONE : REWRITE_AGAIN, resultNode);
127
}
128
129
3618
RewriteResponse TheoryBVRewriter::RewriteUgt(TNode node, bool prerewrite){
130
  Node resultNode =
131
      LinearRewriteStrategy<RewriteRule<UgtUrem>,
132
7236
                            RewriteRule<UgtEliminate>>::apply(node);
133
134
7236
  return RewriteResponse(REWRITE_AGAIN, resultNode);
135
}
136
137
3651
RewriteResponse TheoryBVRewriter::RewriteSgt(TNode node, bool prerewrite){
138
  Node resultNode = LinearRewriteStrategy
139
    < RewriteRule<SgtEliminate>
140
      //RewriteRule<SltEliminate>
141
7302
      >::apply(node);
142
143
7302
  return RewriteResponse(REWRITE_AGAIN, resultNode);
144
}
145
146
3334
RewriteResponse TheoryBVRewriter::RewriteUge(TNode node, bool prerewrite){
147
  Node resultNode = LinearRewriteStrategy
148
    < RewriteRule<UgeEliminate>
149
6668
    >::apply(node);
150
151
6668
  return RewriteResponse(REWRITE_AGAIN, resultNode);
152
}
153
154
3444
RewriteResponse TheoryBVRewriter::RewriteSge(TNode node, bool prerewrite){
155
  Node resultNode = LinearRewriteStrategy
156
    < RewriteRule<SgeEliminate>
157
      //      RewriteRule<SleEliminate>
158
6888
    >::apply(node);
159
160
6888
  return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
161
}
162
163
20954
RewriteResponse TheoryBVRewriter::RewriteITEBv(TNode node, bool prerewrite)
164
{
165
  Node resultNode =
166
      LinearRewriteStrategy<RewriteRule<EvalITEBv>,
167
                            RewriteRule<BvIteConstCond>,
168
41908
                            RewriteRule<BvIteEqualChildren>>::apply(node);
169
  // If the node has been rewritten, we return here because we need to make
170
  // sure that `BvIteEqualChildren` has been applied until we reach a fixpoint
171
  // before applying `BvIteConstChildren`. Otherwise, `BvIteConstChildren`
172
  // potentially performs an unsound rewrite. Returning hands back the control
173
  // to the `Rewriter` which will then call this method again, ensuring that
174
  // the rewrites are applied in the correct order.
175
20954
  if (resultNode != node)
176
  {
177
1738
    return RewriteResponse(REWRITE_AGAIN, resultNode);
178
  }
179
180
19216
  resultNode = LinearRewriteStrategy<RewriteRule<BvIteConstChildren>,
181
38432
                                     RewriteRule<BvIteEqualCond>>::apply(node);
182
19216
  if (resultNode != node)
183
  {
184
210
    return RewriteResponse(REWRITE_AGAIN, resultNode);
185
  }
186
187
19006
  resultNode =
188
      LinearRewriteStrategy<RewriteRule<BvIteMergeThenIf>,
189
                            RewriteRule<BvIteMergeElseIf>,
190
                            RewriteRule<BvIteMergeThenElse>,
191
38012
                            RewriteRule<BvIteMergeElseElse>>::apply(node);
192
19006
  return RewriteResponse(resultNode == node ? REWRITE_DONE : REWRITE_AGAIN_FULL,
193
38012
                         resultNode);
194
}
195
196
122522
RewriteResponse TheoryBVRewriter::RewriteNot(TNode node, bool prerewrite){
197
245044
  Node resultNode = node;
198
199
  // // if(RewriteRule<NotXor>::applies(node)) {
200
  // //   resultNode = RewriteRule<NotXor>::run<false>(node);
201
  // //   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
202
  // // }
203
122522
  resultNode = LinearRewriteStrategy
204
    < RewriteRule<EvalNot>,
205
      RewriteRule<NotIdemp>
206
245044
    >::apply(node);
207
208
245044
  return RewriteResponse(REWRITE_DONE, resultNode);
209
}
210
211
182044
RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node, bool prerewrite) {
212
364088
  Node resultNode = node;
213
214
182044
  if (RewriteRule<ExtractConcat>::applies(node)) {
215
8248
    resultNode = RewriteRule<ExtractConcat>::run<false>(node);
216
8248
    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
217
  }
218
219
173796
  if (RewriteRule<ExtractSignExtend>::applies(node)) {
220
616
    resultNode = RewriteRule<ExtractSignExtend>::run<false>(node);
221
616
    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
222
  }
223
224
173180
  if (RewriteRule<ExtractNot>::applies(node)) {
225
2326
    resultNode = RewriteRule<ExtractNot>::run<false>(node);
226
2326
    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
227
  }
228
229
341708
  if (options::bvExtractArithRewrite()) {
230
    if (RewriteRule<ExtractArith>::applies(node)) {
231
      resultNode = RewriteRule<ExtractArith>::run<false>(node);
232
      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
233
    }
234
  }
235
236
237
170854
  resultNode = LinearRewriteStrategy
238
    < RewriteRule<ExtractConstant>,
239
      RewriteRule<ExtractExtract>,
240
      // We could get another extract over extract
241
      RewriteRule<ExtractWhole>,
242
      // At this point only Extract-Whole could apply
243
      RewriteRule<ExtractMultLeadingBit>
244
341708
      >::apply(node);
245
246
170854
  return RewriteResponse(REWRITE_DONE, resultNode);
247
}
248
249
201229
RewriteResponse TheoryBVRewriter::RewriteConcat(TNode node, bool prerewrite)
250
{
251
  Node resultNode = LinearRewriteStrategy<
252
      RewriteRule<ConcatFlatten>,
253
      // Flatten the top level concatenations
254
      RewriteRule<ConcatExtractMerge>,
255
      // Merge the adjacent extracts on non-constants
256
      RewriteRule<ConcatConstantMerge>,
257
      // Merge the adjacent extracts on constants
258
402458
      ApplyRuleToChildren<kind::BITVECTOR_CONCAT, ExtractWhole>>::apply(node);
259
402458
  return RewriteResponse(REWRITE_DONE, resultNode);
260
}
261
262
153982
RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool prerewrite)
263
{
264
307964
  Node resultNode = node;
265
153982
  resultNode =
266
      LinearRewriteStrategy<RewriteRule<FlattenAssocCommutNoDuplicates>,
267
                            RewriteRule<AndSimplify>,
268
307964
                            RewriteRule<AndOrXorConcatPullUp>>::apply(node);
269
153982
  if (!prerewrite)
270
  {
271
73911
    resultNode =
272
147822
        LinearRewriteStrategy<RewriteRule<BitwiseSlicing>>::apply(resultNode);
273
274
73911
    if (resultNode.getKind() != node.getKind())
275
    {
276
37718
      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
277
    }
278
  }
279
280
116264
  return RewriteResponse(REWRITE_DONE, resultNode);
281
}
282
283
189258
RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool prerewrite)
284
{
285
378516
  Node resultNode = node;
286
189258
  resultNode =
287
      LinearRewriteStrategy<RewriteRule<FlattenAssocCommutNoDuplicates>,
288
                            RewriteRule<OrSimplify>,
289
378516
                            RewriteRule<AndOrXorConcatPullUp>>::apply(node);
290
291
189258
  if (!prerewrite)
292
  {
293
91836
    resultNode =
294
183672
        LinearRewriteStrategy<RewriteRule<BitwiseSlicing>>::apply(resultNode);
295
296
91836
    if (resultNode.getKind() != node.getKind())
297
    {
298
44928
      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
299
    }
300
  }
301
302
144330
  return RewriteResponse(REWRITE_DONE, resultNode);
303
}
304
305
11098
RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool prerewrite)
306
{
307
22196
  Node resultNode = node;
308
11098
  resultNode = LinearRewriteStrategy<
309
      RewriteRule<FlattenAssocCommut>,  // flatten the expression
310
      RewriteRule<XorSimplify>,         // simplify duplicates and constants
311
      RewriteRule<XorZero>,  // checks if the constant part is zero and
312
                             // eliminates it
313
      RewriteRule<AndOrXorConcatPullUp>,
314
22196
      RewriteRule<BitwiseSlicing>>::apply(node);
315
316
11098
  if (!prerewrite)
317
  {
318
5886
    resultNode =
319
        LinearRewriteStrategy<RewriteRule<XorOne>,
320
11772
                              RewriteRule<BitwiseSlicing>>::apply(resultNode);
321
322
5886
    if (resultNode.getKind() != node.getKind())
323
    {
324
1723
      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
325
    }
326
  }
327
328
9375
  return RewriteResponse(REWRITE_DONE, resultNode);
329
}
330
331
932
RewriteResponse TheoryBVRewriter::RewriteXnor(TNode node, bool prerewrite) {
332
  Node resultNode = LinearRewriteStrategy
333
    < RewriteRule<XnorEliminate>
334
1864
    >::apply(node);
335
  // need to rewrite two levels in
336
1864
  return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
337
}
338
339
630
RewriteResponse TheoryBVRewriter::RewriteNand(TNode node, bool prerewrite) {
340
  Node resultNode = LinearRewriteStrategy
341
    < RewriteRule<NandEliminate>
342
1260
      >::apply(node);
343
344
1260
  return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
345
}
346
347
811
RewriteResponse TheoryBVRewriter::RewriteNor(TNode node, bool prerewrite) {
348
  Node resultNode = LinearRewriteStrategy
349
    < RewriteRule<NorEliminate>
350
1622
    >::apply(node);
351
352
1622
  return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
353
}
354
355
166430
RewriteResponse TheoryBVRewriter::RewriteComp(TNode node, bool prerewrite)
356
{
357
  Node resultNode =
358
      LinearRewriteStrategy<RewriteRule<EvalComp>, RewriteRule<BvComp> >::apply(
359
332860
          node);
360
361
332860
  return RewriteResponse(REWRITE_DONE, resultNode);
362
}
363
364
304319
RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool prerewrite) {
365
608638
  Node resultNode = node;
366
304319
  resultNode = LinearRewriteStrategy
367
    < RewriteRule<FlattenAssocCommut>, // flattens and sorts
368
      RewriteRule<MultSimplify>,       // multiplies constant part and checks for 0
369
      RewriteRule<MultPow2>            // replaces multiplication by a power of 2 by a shift
370
608638
    >::apply(resultNode);
371
372
  // only apply if every subterm was already rewritten
373
304319
  if (!prerewrite) {
374
113314
    resultNode = LinearRewriteStrategy
375
      <   RewriteRule<MultDistribConst>
376
        , RewriteRule<MultDistrib>
377
226628
        >::apply(resultNode);
378
  }
379
380
304319
  if(resultNode == node) {
381
176325
    return RewriteResponse(REWRITE_DONE, resultNode);
382
  }
383
127994
  return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
384
}
385
386
164162
RewriteResponse TheoryBVRewriter::RewritePlus(TNode node, bool prerewrite) {
387
328324
  Node resultNode = node;
388
164162
  if (prerewrite) {
389
69806
    resultNode = LinearRewriteStrategy
390
      < RewriteRule<FlattenAssocCommut>
391
139612
        >::apply(node);
392
69806
    return RewriteResponse(REWRITE_DONE, resultNode);
393
  }
394
395
94356
  resultNode =  LinearRewriteStrategy
396
    < RewriteRule<FlattenAssocCommut>,
397
      RewriteRule<PlusCombineLikeTerms>
398
188712
      >::apply(node);
399
400
94356
  if (node != resultNode) {
401
43984
    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
402
  }
403
404
50372
  return RewriteResponse(REWRITE_DONE, resultNode);
405
}
406
407
2418
RewriteResponse TheoryBVRewriter::RewriteSub(TNode node, bool prerewrite){
408
  // return RewriteResponse(REWRITE_DONE, node);
409
  Node resultNode = LinearRewriteStrategy
410
    < RewriteRule<SubEliminate>
411
4836
    >::apply(node);
412
413
4836
  return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
414
}
415
416
35000
RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool prerewrite) {
417
70000
  Node resultNode = node;
418
419
35000
  resultNode = LinearRewriteStrategy
420
    < RewriteRule<EvalNeg>,
421
      RewriteRule<NegIdemp>,
422
      RewriteRule<NegSub>
423
70000
      >::apply(node);
424
425
35000
  if (RewriteRule<NegPlus>::applies(node)) {
426
1238
    resultNode = RewriteRule<NegPlus>::run<false>(node);
427
1238
    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
428
  }
429
430
33762
  if(!prerewrite) {
431
18254
    if (RewriteRule<NegMult>::applies(node)) {
432
      resultNode = RewriteRule<NegMult>::run<false>(node);
433
      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
434
    }
435
  }
436
437
33762
  return RewriteResponse(REWRITE_DONE, resultNode);
438
}
439
440
38870
RewriteResponse TheoryBVRewriter::RewriteUdiv(TNode node, bool prerewrite){
441
77740
  Node resultNode = node;
442
443
38870
  if(RewriteRule<UdivPow2>::applies(node)) {
444
2731
    resultNode = RewriteRule<UdivPow2>::run <false> (node);
445
2731
    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
446
  }
447
448
36139
  resultNode =
449
      LinearRewriteStrategy<RewriteRule<EvalUdiv>, RewriteRule<UdivZero>,
450
72278
                            RewriteRule<UdivOne> >::apply(node);
451
452
36139
  return RewriteResponse(REWRITE_DONE, resultNode);
453
}
454
455
39767
RewriteResponse TheoryBVRewriter::RewriteUrem(TNode node, bool prerewrite)
456
{
457
79534
  Node resultNode = node;
458
459
39767
  if(RewriteRule<UremPow2>::applies(node)) {
460
2483
    resultNode = RewriteRule<UremPow2>::run <false> (node);
461
2483
    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
462
  }
463
464
37284
  resultNode = LinearRewriteStrategy
465
    < RewriteRule<EvalUrem>,
466
      RewriteRule<UremOne>,
467
      RewriteRule<UremSelf>
468
74568
      >::apply(node);
469
37284
  return RewriteResponse(REWRITE_DONE, resultNode);
470
}
471
472
112
RewriteResponse TheoryBVRewriter::RewriteSmod(TNode node, bool prerewrite) {
473
  Node resultNode = LinearRewriteStrategy
474
    < RewriteRule<SmodEliminate>
475
224
      >::apply(node);
476
477
224
  return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
478
}
479
480
155
RewriteResponse TheoryBVRewriter::RewriteSdiv(TNode node, bool prerewrite) {
481
  Node resultNode = LinearRewriteStrategy
482
    < RewriteRule<SdivEliminate>
483
310
      >::apply(node);
484
485
310
  return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
486
}
487
488
77
RewriteResponse TheoryBVRewriter::RewriteSrem(TNode node, bool prerewrite) {
489
  Node resultNode = LinearRewriteStrategy
490
    < RewriteRule<SremEliminate>
491
154
       >::apply(node);
492
154
  return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
493
}
494
495
27232
RewriteResponse TheoryBVRewriter::RewriteShl(TNode node, bool prerewrite) {
496
54464
  Node resultNode = node;
497
27232
  if(RewriteRule<ShlByConst>::applies(node)) {
498
17076
    resultNode = RewriteRule<ShlByConst>::run <false> (node);
499
17076
    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
500
  }
501
502
10156
  resultNode = LinearRewriteStrategy
503
    < RewriteRule<EvalShl>,
504
      RewriteRule<ShiftZero>
505
20312
      >::apply(node);
506
507
10156
  return RewriteResponse(REWRITE_DONE, resultNode);
508
}
509
510
33395
RewriteResponse TheoryBVRewriter::RewriteLshr(TNode node, bool prerewrite) {
511
66790
  Node resultNode = node;
512
33395
  if(RewriteRule<LshrByConst>::applies(node)) {
513
18995
    resultNode = RewriteRule<LshrByConst>::run <false> (node);
514
18995
    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
515
  }
516
517
14400
  resultNode = LinearRewriteStrategy
518
    < RewriteRule<EvalLshr>,
519
      RewriteRule<ShiftZero>
520
28800
      >::apply(node);
521
522
14400
  return RewriteResponse(REWRITE_DONE, resultNode);
523
}
524
525
6829
RewriteResponse TheoryBVRewriter::RewriteAshr(TNode node, bool prerewrite) {
526
13658
  Node resultNode = node;
527
6829
  if(RewriteRule<AshrByConst>::applies(node)) {
528
693
    resultNode = RewriteRule<AshrByConst>::run <false> (node);
529
693
    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
530
  }
531
532
6136
  resultNode = LinearRewriteStrategy
533
    < RewriteRule<EvalAshr>,
534
      RewriteRule<ShiftZero>
535
12272
        >::apply(node);
536
537
6136
  return RewriteResponse(REWRITE_DONE, resultNode);
538
}
539
540
541
797
RewriteResponse TheoryBVRewriter::RewriteRepeat(TNode node, bool prerewrite) {
542
  Node resultNode = LinearRewriteStrategy
543
    < RewriteRule<RepeatEliminate >
544
1594
    >::apply(node);
545
546
1594
  return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
547
}
548
549
10751
RewriteResponse TheoryBVRewriter::RewriteZeroExtend(TNode node, bool prerewrite){
550
  Node resultNode = LinearRewriteStrategy
551
    < RewriteRule<ZeroExtendEliminate >
552
21502
    >::apply(node);
553
554
21502
  return RewriteResponse(REWRITE_AGAIN, resultNode);
555
}
556
557
65760
RewriteResponse TheoryBVRewriter::RewriteSignExtend(TNode node, bool prerewrite) {
558
  Node resultNode = LinearRewriteStrategy
559
    < RewriteRule<MergeSignExtend>
560
    , RewriteRule<EvalSignExtend>
561
131520
    >::apply(node);
562
563
564
65760
  if (resultNode != node) {
565
2144
    return RewriteResponse(REWRITE_AGAIN, resultNode);
566
  }
567
63616
  return RewriteResponse(REWRITE_DONE, resultNode);
568
}
569
570
571
813
RewriteResponse TheoryBVRewriter::RewriteRotateRight(TNode node, bool prerewrite) {
572
  Node resultNode = LinearRewriteStrategy
573
    < RewriteRule<RotateRightEliminate >
574
1626
    >::apply(node);
575
576
1626
  return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
577
}
578
579
678
RewriteResponse TheoryBVRewriter::RewriteRotateLeft(TNode node, bool prerewrite){
580
  Node resultNode = LinearRewriteStrategy
581
    < RewriteRule<RotateLeftEliminate >
582
1356
    >::apply(node);
583
584
1356
  return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
585
}
586
587
RewriteResponse TheoryBVRewriter::RewriteRedor(TNode node, bool prerewrite){
588
  Node resultNode = LinearRewriteStrategy
589
    < RewriteRule<RedorEliminate>
590
    >::apply(node);
591
592
  return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
593
}
594
595
RewriteResponse TheoryBVRewriter::RewriteRedand(TNode node, bool prerewrite){
596
  Node resultNode = LinearRewriteStrategy
597
    < RewriteRule<RedandEliminate>
598
    >::apply(node);
599
600
  return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
601
}
602
603
790
RewriteResponse TheoryBVRewriter::RewriteBVToNat(TNode node, bool prerewrite) {
604
  //do not use lazy rewrite strategy if equality solver is disabled
605
790
  if( node[0].isConst() || !options::bvLazyRewriteExtf() ){
606
    Node resultNode = LinearRewriteStrategy
607
      < RewriteRule<BVToNatEliminate>
608
360
      >::apply(node);
609
180
    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
610
  }else{
611
610
    return RewriteResponse(REWRITE_DONE, node);
612
  }
613
}
614
615
596
RewriteResponse TheoryBVRewriter::RewriteIntToBV(TNode node, bool prerewrite) {
616
  //do not use lazy rewrite strategy if equality solver is disabled
617
596
  if( node[0].isConst() || !options::bvLazyRewriteExtf() ){
618
    Node resultNode = LinearRewriteStrategy
619
      < RewriteRule<IntToBVEliminate>
620
502
      >::apply(node);
621
622
251
    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
623
  }else{
624
345
    return RewriteResponse(REWRITE_DONE, node);
625
  }
626
}
627
628
519949
RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool prerewrite) {
629
519949
  if (prerewrite) {
630
    Node resultNode = LinearRewriteStrategy
631
      < RewriteRule<FailEq>,
632
        RewriteRule<SimplifyEq>,
633
        RewriteRule<ReflexivityEq>
634
436390
        >::apply(node);
635
218195
    return RewriteResponse(REWRITE_DONE, resultNode);
636
  }
637
  else {
638
    Node resultNode = LinearRewriteStrategy
639
      < RewriteRule<FailEq>,
640
        RewriteRule<SimplifyEq>,
641
        RewriteRule<ReflexivityEq>
642
603508
        >::apply(node);
643
644
301754
    if(RewriteRule<SolveEq>::applies(resultNode)) {
645
152926
      resultNode = RewriteRule<SolveEq>::run<false>(resultNode);
646
152926
      if (resultNode != node) {
647
7408
        return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
648
      }
649
    }
650
294346
    return RewriteResponse(REWRITE_DONE, resultNode);
651
  }
652
}
653
654
655
282512
RewriteResponse TheoryBVRewriter::IdentityRewrite(TNode node, bool prerewrite) {
656
282512
  return RewriteResponse(REWRITE_DONE, node);
657
}
658
659
RewriteResponse TheoryBVRewriter::UndefinedRewrite(TNode node, bool prerewrite) {
660
  Debug("bv-rewrite") << "TheoryBV::UndefinedRewrite for" << node;
661
  Unimplemented();
662
}
663
664
665
666
8997
void TheoryBVRewriter::initializeRewrites() {
667
668
2915028
  for(unsigned i = 0; i < kind::LAST_KIND; ++i) {
669
2906031
    d_rewriteTable[i] = IdentityRewrite; //UndefinedRewrite;
670
  }
671
672
8997
  d_rewriteTable [ kind::EQUAL ] = RewriteEqual;
673
8997
  d_rewriteTable[kind::BITVECTOR_BITOF] = RewriteBitOf;
674
8997
  d_rewriteTable [ kind::BITVECTOR_ULT ] = RewriteUlt;
675
8997
  d_rewriteTable [ kind::BITVECTOR_SLT ] = RewriteSlt;
676
8997
  d_rewriteTable [ kind::BITVECTOR_ULE ] = RewriteUle;
677
8997
  d_rewriteTable [ kind::BITVECTOR_SLE ] = RewriteSle;
678
8997
  d_rewriteTable [ kind::BITVECTOR_UGT ] = RewriteUgt;
679
8997
  d_rewriteTable [ kind::BITVECTOR_SGT ] = RewriteSgt;
680
8997
  d_rewriteTable [ kind::BITVECTOR_UGE ] = RewriteUge;
681
8997
  d_rewriteTable [ kind::BITVECTOR_SGE ] = RewriteSge;
682
8997
  d_rewriteTable [ kind::BITVECTOR_NOT ] = RewriteNot;
683
8997
  d_rewriteTable [ kind::BITVECTOR_CONCAT ] = RewriteConcat;
684
8997
  d_rewriteTable [ kind::BITVECTOR_AND ] = RewriteAnd;
685
8997
  d_rewriteTable [ kind::BITVECTOR_OR ] = RewriteOr;
686
8997
  d_rewriteTable [ kind::BITVECTOR_XOR] = RewriteXor;
687
8997
  d_rewriteTable [ kind::BITVECTOR_XNOR ] = RewriteXnor;
688
8997
  d_rewriteTable [ kind::BITVECTOR_NAND ] = RewriteNand;
689
8997
  d_rewriteTable [ kind::BITVECTOR_NOR ] = RewriteNor;
690
8997
  d_rewriteTable [ kind::BITVECTOR_COMP ] = RewriteComp;
691
8997
  d_rewriteTable [ kind::BITVECTOR_MULT ] = RewriteMult;
692
8997
  d_rewriteTable [ kind::BITVECTOR_PLUS ] = RewritePlus;
693
8997
  d_rewriteTable [ kind::BITVECTOR_SUB ] = RewriteSub;
694
8997
  d_rewriteTable [ kind::BITVECTOR_NEG ] = RewriteNeg;
695
8997
  d_rewriteTable [ kind::BITVECTOR_UDIV ] = RewriteUdiv;
696
8997
  d_rewriteTable [ kind::BITVECTOR_UREM ] = RewriteUrem;
697
8997
  d_rewriteTable [ kind::BITVECTOR_SMOD ] = RewriteSmod;
698
8997
  d_rewriteTable [ kind::BITVECTOR_SDIV ] = RewriteSdiv;
699
8997
  d_rewriteTable [ kind::BITVECTOR_SREM ] = RewriteSrem;
700
8997
  d_rewriteTable [ kind::BITVECTOR_SHL ] = RewriteShl;
701
8997
  d_rewriteTable [ kind::BITVECTOR_LSHR ] = RewriteLshr;
702
8997
  d_rewriteTable [ kind::BITVECTOR_ASHR ] = RewriteAshr;
703
8997
  d_rewriteTable [ kind::BITVECTOR_EXTRACT ] = RewriteExtract;
704
8997
  d_rewriteTable [ kind::BITVECTOR_REPEAT ] = RewriteRepeat;
705
8997
  d_rewriteTable [ kind::BITVECTOR_ZERO_EXTEND ] = RewriteZeroExtend;
706
8997
  d_rewriteTable [ kind::BITVECTOR_SIGN_EXTEND ] = RewriteSignExtend;
707
8997
  d_rewriteTable [ kind::BITVECTOR_ROTATE_RIGHT ] = RewriteRotateRight;
708
8997
  d_rewriteTable [ kind::BITVECTOR_ROTATE_LEFT ] = RewriteRotateLeft;
709
8997
  d_rewriteTable [ kind::BITVECTOR_REDOR ] = RewriteRedor;
710
8997
  d_rewriteTable [ kind::BITVECTOR_REDAND ] = RewriteRedand;
711
8997
  d_rewriteTable [ kind::BITVECTOR_ULTBV ] = RewriteUltBv;
712
8997
  d_rewriteTable [ kind::BITVECTOR_SLTBV ] = RewriteSltBv;
713
8997
  d_rewriteTable [ kind::BITVECTOR_ITE ] = RewriteITEBv;
714
715
8997
  d_rewriteTable [ kind::BITVECTOR_TO_NAT ] = RewriteBVToNat;
716
8997
  d_rewriteTable [ kind::INT_TO_BITVECTOR ] = RewriteIntToBV;
717
8997
}
718
719
Node TheoryBVRewriter::eliminateBVSDiv(TNode node) {
720
  Node result = bv::LinearRewriteStrategy <
721
    bv::RewriteRule<bv::SremEliminate>,
722
    bv::RewriteRule<bv::SdivEliminate>,
723
    bv::RewriteRule<bv::SmodEliminate>
724
    >::apply(node);
725
  return result;
726
197539
}