GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h Lines: 131 149 87.9 %
Date: 2021-03-23 Branches: 322 726 44.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_bv_rewrite_rules_constant_evaluation.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Liana Hadarean, Clark Barrett, 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 "theory/bv/theory_bv_rewrite_rules.h"
23
#include "theory/bv/theory_bv_utils.h"
24
25
namespace CVC4 {
26
namespace theory {
27
namespace bv {
28
29
template<> inline
30
bool RewriteRule<EvalAnd>::applies(TNode node) {
31
  Unreachable();
32
  return (node.getKind() == kind::BITVECTOR_AND &&
33
          node.getNumChildren() == 2 &&
34
          utils::isBvConstTerm(node));
35
}
36
37
template<> inline
38
Node RewriteRule<EvalAnd>::apply(TNode node) {
39
  Unreachable();
40
  Debug("bv-rewrite") << "RewriteRule<EvalAnd>(" << node << ")" << std::endl;
41
  BitVector a = node[0].getConst<BitVector>();
42
  BitVector b = node[1].getConst<BitVector>();
43
  BitVector res = a & b;
44
45
  return utils::mkConst(res);
46
}
47
48
template<> inline
49
bool RewriteRule<EvalOr>::applies(TNode node) {
50
  Unreachable();
51
  return (node.getKind() == kind::BITVECTOR_OR &&
52
          node.getNumChildren() == 2 &&
53
          utils::isBvConstTerm(node));
54
}
55
56
template<> inline
57
Node RewriteRule<EvalOr>::apply(TNode node) {
58
  Unreachable();
59
  Debug("bv-rewrite") << "RewriteRule<EvalOr>(" << node << ")" << std::endl;
60
  BitVector a = node[0].getConst<BitVector>();
61
  BitVector b = node[1].getConst<BitVector>();
62
  BitVector res = a | b;
63
64
  return utils::mkConst(res);
65
}
66
67
template<> inline
68
bool RewriteRule<EvalXor>::applies(TNode node) {
69
  Unreachable();
70
  return (node.getKind() == kind::BITVECTOR_XOR &&
71
          node.getNumChildren() == 2 &&
72
          utils::isBvConstTerm(node));
73
}
74
75
template<> inline
76
Node RewriteRule<EvalXor>::apply(TNode node) {
77
  Unreachable();
78
  Debug("bv-rewrite") << "RewriteRule<EvalXor>(" << node << ")" << std::endl;
79
  BitVector a = node[0].getConst<BitVector>();
80
  BitVector b = node[1].getConst<BitVector>();
81
  BitVector res = a ^ b;
82
83
  return utils::mkConst(res);
84
}
85
86
// template<> inline
87
// bool RewriteRule<EvalXnor>::applies(TNode node) {
88
//   return (node.getKind() == kind::BITVECTOR_XNOR &&
89
//           utils::isBvConstTerm(node));
90
// }
91
92
// template<> inline
93
// Node RewriteRule<EvalXnor>::apply(TNode node) {
94
//   Debug("bv-rewrite") << "RewriteRule<EvalXnor>(" << node << ")" << std::endl;
95
//   BitVector a = node[0].getConst<BitVector>();
96
//   BitVector b = node[1].getConst<BitVector>();
97
//   BitVector res = ~ (a ^ b);
98
99
//   return utils::mkConst(res);
100
// }
101
template<> inline
102
153002
bool RewriteRule<EvalNot>::applies(TNode node) {
103
459006
  return (node.getKind() == kind::BITVECTOR_NOT &&
104
459006
          utils::isBvConstTerm(node));
105
}
106
107
template<> inline
108
30480
Node RewriteRule<EvalNot>::apply(TNode node) {
109
30480
  Debug("bv-rewrite") << "RewriteRule<EvalNot>(" << node << ")" << std::endl;
110
60960
  BitVector a = node[0].getConst<BitVector>();
111
60960
  BitVector res = ~ a;
112
60960
  return utils::mkConst(res);
113
}
114
115
// template<> inline
116
// bool RewriteRule<EvalComp>::applies(TNode node) {
117
//   return (node.getKind() == kind::BITVECTOR_COMP &&
118
//           utils::isBvConstTerm(node));
119
// }
120
121
// template<> inline
122
// Node RewriteRule<EvalComp>::apply(TNode node) {
123
//   Debug("bv-rewrite") << "RewriteRule<EvalComp>(" << node << ")" << std::endl;
124
//   BitVector a = node[0].getConst<BitVector>();
125
//   BitVector b = node[1].getConst<BitVector>();
126
//   BitVector res;
127
//   if (a == b) {
128
//     res = BitVector(1, Integer(1));
129
//   } else {
130
//     res = BitVector(1, Integer(0));
131
//   }
132
133
//   return utils::mkConst(res);
134
// }
135
136
template<> inline
137
bool RewriteRule<EvalMult>::applies(TNode node) {
138
  return (node.getKind() == kind::BITVECTOR_MULT &&
139
          utils::isBvConstTerm(node));
140
}
141
142
template<> inline
143
Node RewriteRule<EvalMult>::apply(TNode node) {
144
  Debug("bv-rewrite") << "RewriteRule<EvalMult>(" << node << ")" << std::endl;
145
  TNode::iterator child_it = node.begin();
146
  BitVector res = (*child_it).getConst<BitVector>();
147
  for(++child_it; child_it != node.end(); ++child_it) {
148
    res = res * (*child_it).getConst<BitVector>();
149
  }
150
  return utils::mkConst(res);
151
}
152
153
template<> inline
154
bool RewriteRule<EvalPlus>::applies(TNode node) {
155
  return (node.getKind() == kind::BITVECTOR_PLUS &&
156
          utils::isBvConstTerm(node));
157
}
158
159
template<> inline
160
Node RewriteRule<EvalPlus>::apply(TNode node) {
161
  Debug("bv-rewrite") << "RewriteRule<EvalPlus>(" << node << ")" << std::endl;
162
  TNode::iterator child_it = node.begin();
163
  BitVector res = (*child_it).getConst<BitVector>();
164
  for(++child_it; child_it != node.end(); ++child_it) {
165
    res = res + (*child_it).getConst<BitVector>();
166
  }
167
  return utils::mkConst(res);
168
}
169
170
// template<> inline
171
// bool RewriteRule<EvalSub>::applies(TNode node) {
172
//   return (node.getKind() == kind::BITVECTOR_SUB &&
173
//           utils::isBvConstTerm(node));
174
// }
175
176
// template<> inline
177
// Node RewriteRule<EvalSub>::apply(TNode node) {
178
//   Debug("bv-rewrite") << "RewriteRule<EvalSub>(" << node << ")" << std::endl;
179
//   BitVector a = node[0].getConst<BitVector>();
180
//   BitVector b = node[1].getConst<BitVector>();
181
//   BitVector res = a - b;
182
183
//   return utils::mkConst(res);
184
// }
185
template<> inline
186
43504
bool RewriteRule<EvalNeg>::applies(TNode node) {
187
130512
  return (node.getKind() == kind::BITVECTOR_NEG &&
188
130512
          utils::isBvConstTerm(node));
189
}
190
191
template<> inline
192
8504
Node RewriteRule<EvalNeg>::apply(TNode node) {
193
8504
  Debug("bv-rewrite") << "RewriteRule<EvalNeg>(" << node << ")" << std::endl;
194
17008
  BitVector a = node[0].getConst<BitVector>();
195
17008
  BitVector res = - a;
196
197
17008
  return utils::mkConst(res);
198
}
199
template<> inline
200
47326
bool RewriteRule<EvalUdiv>::applies(TNode node) {
201
47326
  return utils::isBvConstTerm(node) && node.getKind() == kind::BITVECTOR_UDIV;
202
}
203
204
template<> inline
205
11187
Node RewriteRule<EvalUdiv>::apply(TNode node) {
206
11187
  Debug("bv-rewrite") << "RewriteRule<EvalUdiv>(" << node << ")" << std::endl;
207
22374
  BitVector a = node[0].getConst<BitVector>();
208
22374
  BitVector b = node[1].getConst<BitVector>();
209
22374
  BitVector res = a.unsignedDivTotal(b);
210
211
22374
  return utils::mkConst(res);
212
}
213
template<> inline
214
49294
bool RewriteRule<EvalUrem>::applies(TNode node) {
215
49294
  return utils::isBvConstTerm(node) && node.getKind() == kind::BITVECTOR_UREM;
216
}
217
218
template<> inline
219
12010
Node RewriteRule<EvalUrem>::apply(TNode node) {
220
12010
  Debug("bv-rewrite") << "RewriteRule<EvalUrem>(" << node << ")" << std::endl;
221
24020
  BitVector a = node[0].getConst<BitVector>();
222
24020
  BitVector b = node[1].getConst<BitVector>();
223
24020
  BitVector res = a.unsignedRemTotal(b);
224
24020
  return utils::mkConst(res);
225
}
226
227
template<> inline
228
10156
bool RewriteRule<EvalShl>::applies(TNode node) {
229
30468
  return (node.getKind() == kind::BITVECTOR_SHL &&
230
30468
          utils::isBvConstTerm(node));
231
}
232
233
template<> inline
234
Node RewriteRule<EvalShl>::apply(TNode node) {
235
  Debug("bv-rewrite") << "RewriteRule<EvalShl>(" << node << ")" << std::endl;
236
  BitVector a = node[0].getConst<BitVector>();
237
  BitVector b = node[1].getConst<BitVector>();
238
239
  BitVector res = a.leftShift(b);
240
  return utils::mkConst(res);
241
}
242
243
template<> inline
244
14400
bool RewriteRule<EvalLshr>::applies(TNode node) {
245
43200
  return (node.getKind() == kind::BITVECTOR_LSHR &&
246
43200
          utils::isBvConstTerm(node));
247
}
248
249
template<> inline
250
Node RewriteRule<EvalLshr>::apply(TNode node) {
251
  Debug("bv-rewrite") << "RewriteRule<EvalLshr>(" << node << ")" << std::endl;
252
  BitVector a = node[0].getConst<BitVector>();
253
  BitVector b = node[1].getConst<BitVector>();
254
255
  BitVector res = a.logicalRightShift(b);
256
  return utils::mkConst(res);
257
}
258
259
template<> inline
260
6136
bool RewriteRule<EvalAshr>::applies(TNode node) {
261
18408
  return (node.getKind() == kind::BITVECTOR_ASHR &&
262
18408
          utils::isBvConstTerm(node));
263
}
264
265
template<> inline
266
Node RewriteRule<EvalAshr>::apply(TNode node) {
267
  Debug("bv-rewrite") << "RewriteRule<EvalAshr>(" << node << ")" << std::endl;
268
  BitVector a = node[0].getConst<BitVector>();
269
  BitVector b = node[1].getConst<BitVector>();
270
271
  BitVector res = a.arithRightShift(b);
272
  return utils::mkConst(res);
273
}
274
275
template<> inline
276
114341
bool RewriteRule<EvalUlt>::applies(TNode node) {
277
343023
  return (node.getKind() == kind::BITVECTOR_ULT &&
278
343023
          utils::isBvConstTerm(node));
279
}
280
281
template<> inline
282
1595
Node RewriteRule<EvalUlt>::apply(TNode node) {
283
1595
  Debug("bv-rewrite") << "RewriteRule<EvalUlt>(" << node << ")" << std::endl;
284
3190
  BitVector a = node[0].getConst<BitVector>();
285
3190
  BitVector b = node[1].getConst<BitVector>();
286
287
1595
  if (a.unsignedLessThan(b)) {
288
717
    return utils::mkTrue();
289
  }
290
878
  return utils::mkFalse();
291
}
292
293
template<> inline
294
3393
bool RewriteRule<EvalUltBv>::applies(TNode node) {
295
10179
  return (node.getKind() == kind::BITVECTOR_ULTBV &&
296
10179
          utils::isBvConstTerm(node));
297
}
298
299
template<> inline
300
67
Node RewriteRule<EvalUltBv>::apply(TNode node) {
301
67
  Debug("bv-rewrite") << "RewriteRule<EvalUltBv>(" << node << ")" << std::endl;
302
134
  BitVector a = node[0].getConst<BitVector>();
303
134
  BitVector b = node[1].getConst<BitVector>();
304
305
67
  if (a.unsignedLessThan(b)) {
306
7
    return utils::mkConst(1,1);
307
  }
308
60
  return utils::mkConst(1, 0);
309
}
310
311
template<> inline
312
120806
bool RewriteRule<EvalSlt>::applies(TNode node) {
313
362418
  return (node.getKind() == kind::BITVECTOR_SLT &&
314
362418
          utils::isBvConstTerm(node));
315
}
316
317
template<> inline
318
1386
Node RewriteRule<EvalSlt>::apply(TNode node) {
319
1386
  Debug("bv-rewrite") << "RewriteRule<EvalSlt>(" << node << ")" << std::endl;
320
2772
  BitVector a = node[0].getConst<BitVector>();
321
2772
  BitVector b = node[1].getConst<BitVector>();
322
323
1386
  if (a.signedLessThan(b)) {
324
606
    return utils::mkTrue();
325
  }
326
780
  return utils::mkFalse();
327
328
}
329
330
template<> inline
331
6763
bool RewriteRule<EvalSltBv>::applies(TNode node) {
332
20289
  return (node.getKind() == kind::BITVECTOR_SLTBV &&
333
20289
          utils::isBvConstTerm(node));
334
}
335
336
template<> inline
337
338
Node RewriteRule<EvalSltBv>::apply(TNode node) {
338
338
  Debug("bv-rewrite") << "RewriteRule<EvalSltBv>(" << node << ")" << std::endl;
339
676
  BitVector a = node[0].getConst<BitVector>();
340
676
  BitVector b = node[1].getConst<BitVector>();
341
342
338
  if (a.signedLessThan(b)) {
343
181
    return utils::mkConst(1, 1);
344
  }
345
157
  return utils::mkConst(1, 0);
346
347
}
348
349
template<> inline
350
21903
bool RewriteRule<EvalITEBv>::applies(TNode node) {
351
21903
  Debug("bv-rewrite") << "RewriteRule<EvalITEBv>::applies(" << node << ")" << std::endl;
352
65709
  return (node.getKind() == kind::BITVECTOR_ITE &&
353
65709
          utils::isBvConstTerm(node));
354
}
355
356
template<> inline
357
949
Node RewriteRule<EvalITEBv>::apply(TNode node) {
358
949
  Debug("bv-rewrite") << "RewriteRule<EvalITEBv>(" << node << ")" << std::endl;
359
1898
  BitVector cond = node[0].getConst<BitVector>();
360
361
949
  if (node[0] == utils::mkConst(1, 1)) {
362
379
    return node[1];
363
  } else {
364
570
    Assert(node[0] == utils::mkConst(1, 0));
365
570
    return node[2];
366
  }
367
}
368
369
template<> inline
370
6691
bool RewriteRule<EvalUle>::applies(TNode node) {
371
20073
  return (node.getKind() == kind::BITVECTOR_ULE &&
372
20073
          utils::isBvConstTerm(node));
373
}
374
375
template<> inline
376
26
Node RewriteRule<EvalUle>::apply(TNode node) {
377
26
  Debug("bv-rewrite") << "RewriteRule<EvalUle>(" << node << ")" << std::endl;
378
52
  BitVector a = node[0].getConst<BitVector>();
379
52
  BitVector b = node[1].getConst<BitVector>();
380
381
26
  if (a.unsignedLessThanEq(b)) {
382
20
    return utils::mkTrue();
383
  }
384
6
  return utils::mkFalse();
385
}
386
387
template<> inline
388
6987
bool RewriteRule<EvalSle>::applies(TNode node) {
389
20961
  return (node.getKind() == kind::BITVECTOR_SLE &&
390
20961
          utils::isBvConstTerm(node));
391
}
392
393
template<> inline
394
26
Node RewriteRule<EvalSle>::apply(TNode node) {
395
26
  Debug("bv-rewrite") << "RewriteRule<EvalSle>(" << node << ")" << std::endl;
396
52
  BitVector a = node[0].getConst<BitVector>();
397
52
  BitVector b = node[1].getConst<BitVector>();
398
399
26
  if (a.signedLessThanEq(b)) {
400
24
    return utils::mkTrue();
401
  }
402
2
  return utils::mkFalse();
403
}
404
405
template<> inline
406
bool RewriteRule<EvalExtract>::applies(TNode node) {
407
  return (node.getKind() == kind::BITVECTOR_EXTRACT &&
408
          utils::isBvConstTerm(node));
409
}
410
411
template<> inline
412
Node RewriteRule<EvalExtract>::apply(TNode node) {
413
  Debug("bv-rewrite") << "RewriteRule<EvalExtract>(" << node << ")" << std::endl;
414
  BitVector a = node[0].getConst<BitVector>();
415
  unsigned lo = utils::getExtractLow(node);
416
  unsigned hi = utils::getExtractHigh(node);
417
418
  BitVector res = a.extract(hi, lo);
419
  return utils::mkConst(res);
420
}
421
422
423
template<> inline
424
bool RewriteRule<EvalConcat>::applies(TNode node) {
425
  return (node.getKind() == kind::BITVECTOR_CONCAT &&
426
          utils::isBvConstTerm(node));
427
}
428
429
template<> inline
430
Node RewriteRule<EvalConcat>::apply(TNode node) {
431
  Debug("bv-rewrite") << "RewriteRule<EvalConcat>(" << node << ")" << std::endl;
432
  unsigned num = node.getNumChildren();
433
  BitVector res = node[0].getConst<BitVector>();
434
  for(unsigned i = 1; i < num; ++i ) {
435
    BitVector a = node[i].getConst<BitVector>();
436
    res = res.concat(a);
437
  }
438
  return utils::mkConst(res);
439
}
440
441
template<> inline
442
67513
bool RewriteRule<EvalSignExtend>::applies(TNode node) {
443
202277
  return (node.getKind() == kind::BITVECTOR_SIGN_EXTEND &&
444
202277
          utils::isBvConstTerm(node));
445
}
446
447
template<> inline
448
1753
Node RewriteRule<EvalSignExtend>::apply(TNode node) {
449
1753
  Debug("bv-rewrite") << "RewriteRule<EvalSignExtend>(" << node << ")" << std::endl;
450
3506
  BitVector a = node[0].getConst<BitVector>();
451
  unsigned amount =
452
1753
      node.getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount;
453
3506
  BitVector res = a.signExtend(amount);
454
455
3506
  return utils::mkConst(res);
456
}
457
458
template<> inline
459
bool RewriteRule<EvalEquals>::applies(TNode node) {
460
  return (node.getKind() == kind::EQUAL &&
461
          utils::isBvConstTerm(node));
462
}
463
464
template<> inline
465
Node RewriteRule<EvalEquals>::apply(TNode node) {
466
  Debug("bv-rewrite") << "RewriteRule<EvalEquals>(" << node << ")" << std::endl;
467
  BitVector a = node[0].getConst<BitVector>();
468
  BitVector b = node[1].getConst<BitVector>();
469
  if (a == b) {
470
    return utils::mkTrue();
471
  }
472
  return utils::mkFalse();
473
474
}
475
476
template<> inline
477
297549
bool RewriteRule<EvalComp>::applies(TNode node) {
478
892647
  return (node.getKind() == kind::BITVECTOR_COMP &&
479
892647
          utils::isBvConstTerm(node));
480
}
481
482
template<> inline
483
131119
Node RewriteRule<EvalComp>::apply(TNode node) {
484
131119
  Debug("bv-rewrite") << "RewriteRule<EvalComp>(" << node << ")" << std::endl;
485
262238
  BitVector a = node[0].getConst<BitVector>();
486
262238
  BitVector b = node[1].getConst<BitVector>();
487
131119
  if (a == b) {
488
282
    return utils::mkConst(1, 1);
489
  }
490
130837
  return utils::mkConst(1, 0);
491
}
492
493
}
494
}
495
}