GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/theory_bv_rewrite_rules_normalization.h Lines: 671 727 92.3 %
Date: 2021-03-23 Branches: 1392 2919 47.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_bv_rewrite_rules_normalization.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Liana Hadarean, Aina Niemetz, Clark Barrett
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 <unordered_map>
23
#include <unordered_set>
24
25
#include "expr/node_algorithm.h"
26
#include "theory/bv/theory_bv_rewrite_rules.h"
27
#include "theory/bv/theory_bv_utils.h"
28
#include "theory/rewriter.h"
29
30
namespace CVC4 {
31
namespace theory {
32
namespace bv {
33
34
/**
35
 * ExtractBitwise
36
 *   (x bvop y) [i:j] ==> x[i:j] bvop y[i:j]
37
 *  where bvop is bvand,bvor, bvxor
38
 */
39
template<> inline
40
bool RewriteRule<ExtractBitwise>::applies(TNode node) {
41
  return (node.getKind() == kind::BITVECTOR_EXTRACT &&
42
          (node[0].getKind() == kind::BITVECTOR_AND ||
43
           node[0].getKind() == kind::BITVECTOR_OR ||
44
           node[0].getKind() == kind::BITVECTOR_XOR ));
45
}
46
47
template<> inline
48
Node RewriteRule<ExtractBitwise>::apply(TNode node) {
49
  Debug("bv-rewrite") << "RewriteRule<ExtractBitwise>(" << node << ")" << std::endl;
50
  unsigned high = utils::getExtractHigh(node);
51
  unsigned low = utils::getExtractLow(node);
52
  std::vector<Node> children;
53
  for (unsigned i = 0; i < node[0].getNumChildren(); ++i) {
54
    children.push_back(utils::mkExtract(node[0][i], high, low));
55
  }
56
  Kind kind = node[0].getKind();
57
  return utils::mkSortedNode(kind, children);
58
}
59
60
/**
61
 * ExtractNot
62
 *
63
 *  (~ a) [i:j] ==> ~ (a[i:j])
64
 */
65
template<> inline
66
175506
bool RewriteRule<ExtractNot>::applies(TNode node) {
67
526518
  return (node.getKind() == kind::BITVECTOR_EXTRACT &&
68
526518
          node[0].getKind() == kind::BITVECTOR_NOT);
69
}
70
71
template <>
72
2326
inline Node RewriteRule<ExtractNot>::apply(TNode node)
73
{
74
2326
  Debug("bv-rewrite") << "RewriteRule<ExtractNot>(" << node << ")" << std::endl;
75
2326
  unsigned low = utils::getExtractLow(node);
76
2326
  unsigned high = utils::getExtractHigh(node);
77
4652
  Node a = utils::mkExtract(node[0][0], high, low);
78
4652
  return NodeManager::currentNM()->mkNode(kind::BITVECTOR_NOT, a);
79
}
80
81
/**
82
 * ExtractSignExtend
83
 *
84
 * (sign_extend k x) [i:j] => pushes extract in
85
 *
86
 * @return
87
 */
88
89
template<> inline
90
174412
bool RewriteRule<ExtractSignExtend>::applies(TNode node) {
91
697648
  if (node.getKind() == kind::BITVECTOR_EXTRACT &&
92
523236
      node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND) {
93
1232
    return true;
94
  }
95
173180
  return false;
96
}
97
98
template <>
99
616
inline Node RewriteRule<ExtractSignExtend>::apply(TNode node)
100
{
101
1232
  Debug("bv-rewrite") << "RewriteRule<ExtractSignExtend>(" << node << ")"
102
616
                      << std::endl;
103
1232
  TNode extendee = node[0][0];
104
616
  unsigned extendee_size = utils::getSize(extendee);
105
106
616
  unsigned high = utils::getExtractHigh(node);
107
616
  unsigned low = utils::getExtractLow(node);
108
109
616
  Node resultNode;
110
  // extract falls on extendee
111
616
  if (high < extendee_size)
112
  {
113
225
    resultNode = utils::mkExtract(extendee, high, low);
114
  }
115
391
  else if (low < extendee_size && high >= extendee_size)
116
  {
117
    // if extract overlaps sign extend and extendee
118
144
    Node low_extract = utils::mkExtract(extendee, extendee_size - 1, low);
119
72
    unsigned new_amount = high - extendee_size + 1;
120
144
    resultNode = utils::mkSignExtend(low_extract, new_amount);
121
  }
122
  else
123
  {
124
    // extract only over sign extend
125
319
    Assert(low >= extendee_size);
126
319
    unsigned top = utils::getSize(extendee) - 1;
127
638
    Node most_significant_bit = utils::mkExtract(extendee, top, top);
128
638
    std::vector<Node> bits;
129
868
    for (unsigned i = 0; i < high - low + 1; ++i)
130
    {
131
549
      bits.push_back(most_significant_bit);
132
    }
133
319
    resultNode = utils::mkConcat(bits);
134
  }
135
1232
  Debug("bv-rewrite") << "                           =>" << resultNode
136
616
                      << std::endl;
137
1232
  return resultNode;
138
}
139
140
/**
141
 * ExtractArith
142
 *
143
 * (a bvop b) [k:0] ==> (a[k:0] bvop b[k:0])
144
 */
145
146
template<> inline
147
bool RewriteRule<ExtractArith>::applies(TNode node) {
148
  return (node.getKind() == kind::BITVECTOR_EXTRACT &&
149
          utils::getExtractLow(node) == 0 &&
150
          (node[0].getKind() == kind::BITVECTOR_PLUS ||
151
           node[0].getKind() == kind::BITVECTOR_MULT));
152
}
153
154
template <>
155
inline Node RewriteRule<ExtractArith>::apply(TNode node)
156
{
157
  Debug("bv-rewrite") << "RewriteRule<ExtractArith>(" << node << ")"
158
                      << std::endl;
159
  unsigned low = utils::getExtractLow(node);
160
  Assert(low == 0);
161
  unsigned high = utils::getExtractHigh(node);
162
  std::vector<Node> children;
163
  for (unsigned i = 0; i < node[0].getNumChildren(); ++i)
164
  {
165
    children.push_back(utils::mkExtract(node[0][i], high, low));
166
  }
167
  Kind kind = node[0].getKind();
168
  return utils::mkNaryNode(kind, children);
169
}
170
171
/**
172
 * ExtractArith2
173
 *
174
 * (a bvop b) [i:j] ==> (a[i:0] bvop b[i:0]) [i:j]
175
 */
176
177
// careful not to apply in a loop
178
template<> inline
179
bool RewriteRule<ExtractArith2>::applies(TNode node) {
180
  return (node.getKind() == kind::BITVECTOR_EXTRACT &&
181
          (node[0].getKind() == kind::BITVECTOR_PLUS ||
182
           node[0].getKind() == kind::BITVECTOR_MULT));
183
}
184
185
template <>
186
inline Node RewriteRule<ExtractArith2>::apply(TNode node)
187
{
188
  Debug("bv-rewrite") << "RewriteRule<ExtractArith2>(" << node << ")"
189
                      << std::endl;
190
  unsigned low = utils::getExtractLow(node);
191
  unsigned high = utils::getExtractHigh(node);
192
  std::vector<Node> children;
193
  for (unsigned i = 0; i < node[0].getNumChildren(); ++i)
194
  {
195
    children.push_back(utils::mkExtract(node[0][i], high, 0));
196
  }
197
  Kind kind = node[0].getKind();
198
  Node op_children = utils::mkNaryNode(kind, children);
199
200
  return utils::mkExtract(op_children, high, low);
201
}
202
203
template<> inline
204
506979
bool RewriteRule<FlattenAssocCommut>::applies(TNode node) {
205
506979
  Kind kind = node.getKind();
206
506979
  if (kind != kind::BITVECTOR_PLUS &&
207
11169
      kind != kind::BITVECTOR_MULT &&
208
11169
      kind != kind::BITVECTOR_OR &&
209
      kind != kind::BITVECTOR_XOR &&
210
      kind != kind::BITVECTOR_AND)
211
    return false;
212
506979
  TNode::iterator child_it = node.begin();
213
3336553
  for(; child_it != node.end(); ++child_it) {
214
1469227
    if ((*child_it).getKind() == kind) {
215
54440
      return true;
216
    }
217
  }
218
452539
  return false;
219
}
220
221
template <>
222
27224
inline Node RewriteRule<FlattenAssocCommut>::apply(TNode node)
223
{
224
54448
  Debug("bv-rewrite") << "RewriteRule<FlattenAssocCommut>(" << node << ")"
225
27224
                      << std::endl;
226
54448
  std::vector<Node> processingStack;
227
27224
  processingStack.push_back(node);
228
54448
  std::vector<Node> children;
229
27224
  Kind kind = node.getKind();
230
231
463472
  while (!processingStack.empty())
232
  {
233
436248
    TNode current = processingStack.back();
234
218124
    processingStack.pop_back();
235
236
    // flatten expression
237
218124
    if (current.getKind() == kind)
238
    {
239
254304
      for (unsigned i = 0; i < current.getNumChildren(); ++i)
240
      {
241
190900
        processingStack.push_back(current[i]);
242
      }
243
    }
244
    else
245
    {
246
154720
      children.push_back(current);
247
    }
248
  }
249
54448
  if (node.getKind() == kind::BITVECTOR_PLUS
250
27224
      || node.getKind() == kind::BITVECTOR_MULT)
251
  {
252
27153
    return utils::mkNaryNode(kind, children);
253
  }
254
  else
255
  {
256
71
    return utils::mkSortedNode(kind, children);
257
  }
258
}
259
260
678138
static inline void addToCoefMap(std::map<Node, BitVector>& map,
261
                                TNode term, const BitVector& coef) {
262
678138
  if (map.find(term) != map.end()) {
263
547
    map[term] = map[term] + coef;
264
  } else {
265
677591
    map[term] = coef;
266
  }
267
678138
}
268
269
270
866202
static inline void updateCoefMap(TNode current, unsigned size,
271
                                 std::map<Node, BitVector>& factorToCoefficient,
272
                                 BitVector& constSum) {
273
866202
  switch (current.getKind()) {
274
297351
    case kind::BITVECTOR_MULT: {
275
      // look for c * term, where c is a constant
276
594702
      BitVector coeff;
277
594702
      Node term;
278
297351
      if (current.getNumChildren() == 2) {
279
        // Mult should be normalized with only one constant at end
280
62604
        Assert(!current[0].isConst());
281
62604
        if (current[1].isConst()) {
282
44770
          coeff = current[1].getConst<BitVector>();
283
44770
          term = current[0];
284
        }
285
      }
286
234747
      else if (current[current.getNumChildren()-1].isConst()) {
287
446584
        NodeBuilder<> nb(kind::BITVECTOR_MULT);
288
223292
        TNode::iterator child_it = current.begin();
289
1492164
        for(; (child_it+1) != current.end(); ++child_it) {
290
634436
          Assert(!(*child_it).isConst());
291
634436
          nb << (*child_it);
292
        }
293
223292
        term = nb;
294
223292
        coeff = (*child_it).getConst<BitVector>();
295
      }
296
297351
      if (term.isNull()) {
297
29289
        coeff = BitVector(size, (unsigned)1);
298
29289
        term = current;
299
      }
300
297351
      if(term.getKind() == kind::BITVECTOR_SUB) {
301
        TNode a = term[0];
302
        TNode b = term[1];
303
        addToCoefMap(factorToCoefficient, a, coeff);
304
        addToCoefMap(factorToCoefficient, b, -coeff);
305
      }
306
297351
      else if(term.getKind() == kind::BITVECTOR_NEG) {
307
        addToCoefMap(factorToCoefficient, term[0], -BitVector(size, coeff));
308
      }
309
      else {
310
297351
        addToCoefMap(factorToCoefficient, term, coeff);
311
      }
312
297351
      break;
313
    }
314
    case kind::BITVECTOR_SUB:
315
      // turn into a + (-1)*b
316
      Assert(current.getNumChildren() == 2);
317
      addToCoefMap(factorToCoefficient, current[0], BitVector(size, (unsigned)1));
318
      addToCoefMap(factorToCoefficient, current[1], -BitVector(size, (unsigned)1));
319
      break;
320
73112
    case kind::BITVECTOR_NEG:
321
73112
      addToCoefMap(factorToCoefficient, current[0], -BitVector(size, (unsigned)1));
322
73112
      break;
323
188064
    case kind::CONST_BITVECTOR: {
324
376128
      BitVector constValue = current.getConst<BitVector>();
325
188064
      constSum = constSum + constValue;
326
188064
      break;
327
    }
328
307675
    default:
329
      // store as 1 * current
330
307675
      addToCoefMap(factorToCoefficient, current, BitVector(size, (unsigned)1));
331
307675
      break;
332
  }
333
866202
}
334
335
674190
static inline void addToChildren(TNode term,
336
                                 unsigned size,
337
                                 BitVector coeff,
338
                                 std::vector<Node> &children)
339
{
340
674190
  NodeManager *nm = NodeManager::currentNM();
341
674190
  if (coeff == BitVector(size, (unsigned)0))
342
  {
343
88
    return;
344
  }
345
674102
  else if (coeff == BitVector(size, (unsigned)1))
346
  {
347
333991
    children.push_back(term);
348
  }
349
340111
  else if (coeff == -BitVector(size, (unsigned)1))
350
  {
351
    // avoid introducing an extra multiplication
352
71673
    children.push_back(nm->mkNode(kind::BITVECTOR_NEG, term));
353
  }
354
268438
  else if (term.getKind() == kind::BITVECTOR_MULT)
355
  {
356
446576
    NodeBuilder<> nb(kind::BITVECTOR_MULT);
357
223288
    TNode::iterator child_it = term.begin();
358
1492124
    for (; child_it != term.end(); ++child_it)
359
    {
360
634418
      nb << *child_it;
361
    }
362
223288
    nb << utils::mkConst(coeff);
363
223288
    children.push_back(Node(nb));
364
  }
365
  else
366
  {
367
90300
    Node coeffNode = utils::mkConst(coeff);
368
90300
    Node product = nm->mkNode(kind::BITVECTOR_MULT, term, coeffNode);
369
45150
    children.push_back(product);
370
  }
371
}
372
373
template<> inline
374
188712
bool RewriteRule<PlusCombineLikeTerms>::applies(TNode node) {
375
188712
  return (node.getKind() == kind::BITVECTOR_PLUS);
376
}
377
378
template <>
379
94356
inline Node RewriteRule<PlusCombineLikeTerms>::apply(TNode node)
380
{
381
188712
  Debug("bv-rewrite") << "RewriteRule<PlusCombineLikeTerms>(" << node << ")"
382
94356
                      << std::endl;
383
94356
  unsigned size = utils::getSize(node);
384
188712
  BitVector constSum(size, (unsigned)0);
385
188712
  std::map<Node, BitVector> factorToCoefficient;
386
387
  // combine like-terms
388
565013
  for (size_t i = 0, n = node.getNumChildren(); i < n; ++i)
389
  {
390
941314
    TNode current = node[i];
391
470657
    updateCoefMap(current, size, factorToCoefficient, constSum);
392
  }
393
394
188712
  std::vector<Node> children;
395
396
  // construct result
397
94356
  std::map<Node, BitVector>::const_iterator it = factorToCoefficient.begin();
398
399
824048
  for (; it != factorToCoefficient.end(); ++it)
400
  {
401
364846
    addToChildren(it->first, size, it->second, children);
402
  }
403
404
94356
  if (constSum != BitVector(size, (unsigned)0))
405
  {
406
61163
    children.push_back(utils::mkConst(constSum));
407
  }
408
409
94356
  size_t csize = children.size();
410
94356
  if (csize == node.getNumChildren())
411
  {
412
    // If we couldn't combine any terms, we don't perform the rewrite. This is
413
    // important because we are otherwise reordering terms in the addition
414
    // based on the node ids of the terms that are multiplied with the
415
    // coefficients. Due to garbage collection we may see different id orders
416
    // for those nodes even when we perform one rewrite directly after the
417
    // other, so the rewrite wouldn't be idempotent.
418
51944
    return node;
419
  }
420
421
  return csize == 0
422
    ? utils::mkZero(size)
423
42412
    : utils::mkNaryNode(kind::BITVECTOR_PLUS, children);
424
}
425
426
template<> inline
427
608638
bool RewriteRule<MultSimplify>::applies(TNode node) {
428
608638
  return node.getKind() == kind::BITVECTOR_MULT;
429
}
430
431
template <>
432
304319
inline Node RewriteRule<MultSimplify>::apply(TNode node)
433
{
434
608638
  Debug("bv-rewrite") << "RewriteRule<MultSimplify>(" << node << ")"
435
304319
                      << std::endl;
436
304319
  NodeManager *nm = NodeManager::currentNM();
437
304319
  unsigned size = utils::getSize(node);
438
608638
  BitVector constant(size, Integer(1));
439
440
304319
  bool isNeg = false;
441
608638
  std::vector<Node> children;
442
1088770
  for (const TNode &current : node)
443
  {
444
1582728
    Node c = current;
445
798277
    if (c.getKind() == kind::BITVECTOR_NEG)
446
    {
447
1379
      isNeg = !isNeg;
448
1379
      c = c[0];
449
    }
450
451
798277
    if (c.getKind() == kind::CONST_BITVECTOR)
452
    {
453
613902
      BitVector value = c.getConst<BitVector>();
454
313864
      constant = constant * value;
455
313864
      if (constant == BitVector(size, (unsigned)0))
456
      {
457
13826
        return utils::mkConst(size, 0);
458
      }
459
    }
460
    else
461
    {
462
484413
      children.push_back(c);
463
    }
464
  }
465
580986
  BitVector oValue = BitVector(size, static_cast<unsigned>(1));
466
580986
  BitVector noValue = BitVector::mkOnes(size);
467
468
290493
  if (children.empty())
469
  {
470
35594
    return utils::mkConst(isNeg ? -constant : constant);
471
  }
472
473
254899
  std::sort(children.begin(), children.end());
474
475
254899
  if (constant == noValue)
476
  {
477
1927
    isNeg = !isNeg;
478
  }
479
252972
  else if (constant != oValue)
480
  {
481
214001
    if (isNeg)
482
    {
483
1180
      isNeg = !isNeg;
484
1180
      constant = -constant;
485
    }
486
214001
    children.push_back(utils::mkConst(constant));
487
  }
488
489
509798
  Node ret = utils::mkNaryNode(kind::BITVECTOR_MULT, children);
490
491
  // if negative, negate entire node
492
254899
  if (isNeg && size > 1)
493
  {
494
989
    ret = nm->mkNode(kind::BITVECTOR_NEG, ret);
495
  }
496
254899
  return ret;
497
}
498
499
template<> inline
500
114396
bool RewriteRule<MultDistribConst>::applies(TNode node) {
501
190141
  if (node.getKind() != kind::BITVECTOR_MULT ||
502
75745
      node.getNumChildren() != 2) {
503
82845
    return false;
504
  }
505
31551
  Assert(!node[0].isConst());
506
31551
  if (!node[1].isConst()) {
507
16725
    return false;
508
  }
509
29652
  TNode factor = node[0];
510
27488
  return (factor.getKind() == kind::BITVECTOR_PLUS ||
511
27488
          factor.getKind() == kind::BITVECTOR_SUB ||
512
27488
          factor.getKind() == kind::BITVECTOR_NEG);
513
}
514
515
template <>
516
1082
inline Node RewriteRule<MultDistribConst>::apply(TNode node)
517
{
518
2164
  Debug("bv-rewrite") << "RewriteRule<MultDistribConst>(" << node << ")"
519
1082
                      << std::endl;
520
521
1082
  NodeManager *nm = NodeManager::currentNM();
522
2164
  TNode constant = node[1];
523
2164
  TNode factor = node[0];
524
1082
  Assert(constant.getKind() == kind::CONST_BITVECTOR);
525
526
1082
  if (factor.getKind() == kind::BITVECTOR_NEG)
527
  {
528
    // push negation on the constant part
529
    BitVector const_bv = constant.getConst<BitVector>();
530
    return nm->mkNode(
531
        kind::BITVECTOR_MULT, factor[0], utils::mkConst(-const_bv));
532
  }
533
534
2164
  std::vector<Node> children;
535
11332
  for (unsigned i = 0; i < factor.getNumChildren(); ++i)
536
  {
537
10250
    children.push_back(nm->mkNode(kind::BITVECTOR_MULT, factor[i], constant));
538
  }
539
540
1082
  return utils::mkNaryNode(factor.getKind(), children);
541
}
542
543
template<> inline
544
113701
bool RewriteRule<MultDistrib>::applies(TNode node) {
545
187669
  if (node.getKind() != kind::BITVECTOR_MULT ||
546
73968
      node.getNumChildren() != 2) {
547
83927
    return false;
548
  }
549
118972
  if (node[0].getKind() == kind::BITVECTOR_PLUS ||
550
89198
      node[0].getKind() == kind::BITVECTOR_SUB) {
551
224
    return node[1].getKind() != kind::BITVECTOR_PLUS &&
552
160
           node[1].getKind() != kind::BITVECTOR_SUB;
553
  }
554
117392
  return node[1].getKind() == kind::BITVECTOR_PLUS ||
555
87682
         node[1].getKind() == kind::BITVECTOR_SUB;
556
}
557
558
template <>
559
387
inline Node RewriteRule<MultDistrib>::apply(TNode node)
560
{
561
774
  Debug("bv-rewrite") << "RewriteRule<MultDistrib>(" << node << ")"
562
387
                      << std::endl;
563
564
387
  NodeManager *nm = NodeManager::currentNM();
565
1161
  bool is_rhs_factor = node[0].getKind() == kind::BITVECTOR_PLUS
566
1161
                       || node[0].getKind() == kind::BITVECTOR_SUB;
567
774
  TNode factor = !is_rhs_factor ? node[0] : node[1];
568
774
  TNode sum = is_rhs_factor ? node[0] : node[1];
569
387
  Assert(factor.getKind() != kind::BITVECTOR_PLUS
570
         && factor.getKind() != kind::BITVECTOR_SUB
571
         && (sum.getKind() == kind::BITVECTOR_PLUS
572
             || sum.getKind() == kind::BITVECTOR_SUB));
573
574
774
  std::vector<Node> children;
575
20997
  for (unsigned i = 0; i < sum.getNumChildren(); ++i)
576
  {
577
20610
    children.push_back(nm->mkNode(kind::BITVECTOR_MULT, sum[i], factor));
578
  }
579
580
774
  return utils::mkNaryNode(sum.getKind(), children);
581
}
582
583
template<> inline
584
1172
bool RewriteRule<ConcatToMult>::applies(TNode node) {
585
1172
  if (node.getKind() != kind::BITVECTOR_CONCAT) return false;
586
367
  if (node.getNumChildren() != 2) return false;
587
241
  if (node[0].getKind()!= kind::BITVECTOR_EXTRACT) return false;
588
36
  if (!node[1].isConst()) return false;
589
48
  TNode extract = node[0];
590
48
  TNode c = node[1];
591
24
  unsigned amount = utils::getSize(c);
592
593
24
  if (utils::getSize(node) != utils::getSize(extract[0])) return false;
594
24
  if (c != utils::mkZero(amount)) return false;
595
596
24
  unsigned low = utils::getExtractLow(extract);
597
24
  if (low != 0) return false;
598
24
  unsigned high = utils::getExtractHigh(extract);
599
24
  if (high + amount + 1 != utils::getSize(node)) return false;
600
24
  return true;
601
}
602
603
template <>
604
6
inline Node RewriteRule<ConcatToMult>::apply(TNode node)
605
{
606
12
  Debug("bv-rewrite") << "RewriteRule<ConcatToMult>(" << node << ")"
607
6
                      << std::endl;
608
6
  unsigned size = utils::getSize(node);
609
12
  Node factor = node[0][0];
610
6
  Assert(utils::getSize(factor) == utils::getSize(node));
611
12
  BitVector amount = BitVector(size, utils::getSize(node[1]));
612
12
  Node coef = utils::mkConst(BitVector(size, 1u).leftShift(amount));
613
12
  return NodeManager::currentNM()->mkNode(kind::BITVECTOR_MULT, factor, coef);
614
}
615
616
template <>
617
454686
inline bool RewriteRule<SolveEq>::applies(TNode node)
618
{
619
909372
  if (node.getKind() != kind::EQUAL
620
838768
      || (node[0].isVar() && !expr::hasSubterm(node[1], node[0]))
621
1241918
      || (node[1].isVar() && !expr::hasSubterm(node[0], node[1])))
622
  {
623
148828
    return false;
624
  }
625
305858
  return true;
626
}
627
628
// Doesn't do full solving (yet), instead, if a term appears both on lhs and
629
// rhs, it subtracts from both sides so that one side's coeff is zero
630
template <>
631
152932
inline Node RewriteRule<SolveEq>::apply(TNode node)
632
{
633
152932
  Debug("bv-rewrite") << "RewriteRule<SolveEq>(" << node << ")" << std::endl;
634
635
305864
  TNode left = node[0];
636
305864
  TNode right = node[1];
637
638
152932
  unsigned size = utils::getSize(left);
639
305864
  BitVector zero(size, (unsigned)0);
640
305864
  BitVector leftConst(size, (unsigned)0);
641
305864
  BitVector rightConst(size, (unsigned)0);
642
305864
  std::map<Node, BitVector> leftMap, rightMap;
643
644
  // Collect terms and coefficients plus constant for left
645
152932
  if (left.getKind() == kind::BITVECTOR_PLUS)
646
  {
647
83176
    for (unsigned i = 0; i < left.getNumChildren(); ++i)
648
    {
649
70606
      updateCoefMap(left[i], size, leftMap, leftConst);
650
    }
651
  }
652
140362
  else if (left.getKind() == kind::BITVECTOR_NOT && left[0] == right)
653
  {
654
25
    return utils::mkFalse();
655
  }
656
  else
657
  {
658
140337
    updateCoefMap(left, size, leftMap, leftConst);
659
  }
660
661
  // Collect terms and coefficients plus constant for right
662
152907
  if (right.getKind() == kind::BITVECTOR_PLUS)
663
  {
664
49439
    for (unsigned i = 0; i < right.getNumChildren(); ++i)
665
    {
666
40567
      updateCoefMap(right[i], size, rightMap, rightConst);
667
    }
668
  }
669
144035
  else if (right.getKind() == kind::BITVECTOR_NOT && right[0] == left)
670
  {
671
    return utils::mkFalse();
672
  }
673
  else
674
  {
675
144035
    updateCoefMap(right, size, rightMap, rightConst);
676
  }
677
678
305814
  std::vector<Node> childrenLeft, childrenRight;
679
680
152907
  std::map<Node, BitVector>::const_iterator iLeft = leftMap.begin(),
681
152907
                                            iLeftEnd = leftMap.end();
682
152907
  std::map<Node, BitVector>::const_iterator iRight = rightMap.begin(),
683
152907
                                            iRightEnd = rightMap.end();
684
685
305814
  BitVector coeffLeft;
686
305814
  TNode termLeft;
687
152907
  if (iLeft != iLeftEnd)
688
  {
689
149119
    coeffLeft = iLeft->second;
690
149119
    termLeft = iLeft->first;
691
  }
692
693
305814
  BitVector coeffRight;
694
305814
  TNode termRight;
695
152907
  if (iRight != iRightEnd)
696
  {
697
91099
    coeffRight = iRight->second;
698
91099
    termRight = iRight->first;
699
  }
700
701
  // Changed tracks whether there have been any changes to the coefficients or
702
  // constants of the left- or right-hand side. We perform a rewrite only if
703
  // that is the case. This is important because we are otherwise reordering
704
  // terms in the addition based on the node ids of the terms that are
705
  // multiplied with the coefficients. Due to garbage collection we may see
706
  // different id orders for those nodes even when we perform one rewrite
707
  // directly after the other, so the rewrite wouldn't be idempotent.
708
152907
  bool changed = false;
709
  bool incLeft, incRight;
710
711
774905
  while (iLeft != iLeftEnd || iRight != iRightEnd)
712
  {
713
310999
    incLeft = incRight = false;
714
310999
    if (iLeft != iLeftEnd && (iRight == iRightEnd || termLeft < termRight))
715
    {
716
195356
      addToChildren(termLeft, size, coeffLeft, childrenLeft);
717
195356
      incLeft = true;
718
    }
719
115643
    else if (iLeft == iLeftEnd || termRight < termLeft)
720
    {
721
113897
      Assert(iRight != iRightEnd);
722
113897
      addToChildren(termRight, size, coeffRight, childrenRight);
723
113897
      incRight = true;
724
    }
725
    else
726
    {
727
1746
      if (coeffLeft > coeffRight)
728
      {
729
85
        addToChildren(termLeft, size, coeffLeft - coeffRight, childrenLeft);
730
      }
731
1661
      else if (coeffRight > coeffLeft)
732
      {
733
6
        addToChildren(termRight, size, coeffRight - coeffLeft, childrenRight);
734
      }
735
1746
      incLeft = incRight = true;
736
1746
      changed = true;
737
    }
738
310999
    if (incLeft)
739
    {
740
197102
      ++iLeft;
741
197102
      if (iLeft != iLeftEnd)
742
      {
743
47983
        Assert(termLeft < iLeft->first);
744
47983
        coeffLeft = iLeft->second;
745
47983
        termLeft = iLeft->first;
746
      }
747
    }
748
310999
    if (incRight)
749
    {
750
115643
      ++iRight;
751
115643
      if (iRight != iRightEnd)
752
      {
753
24544
        Assert(termRight < iRight->first);
754
24544
        coeffRight = iRight->second;
755
24544
        termRight = iRight->first;
756
      }
757
    }
758
  }
759
760
  // construct result
761
762
  // If both constants are nonzero, combine on right, otherwise leave them where
763
  // they are
764
152907
  if (rightConst != zero)
765
  {
766
49852
    changed |= (leftConst != zero);
767
49852
    rightConst = rightConst - leftConst;
768
49852
    leftConst = zero;
769
49852
    if (rightConst != zero)
770
    {
771
48766
      childrenRight.push_back(utils::mkConst(rightConst));
772
    }
773
  }
774
103055
  else if (leftConst != zero)
775
  {
776
9198
    childrenLeft.push_back(utils::mkConst(leftConst));
777
  }
778
779
305814
  Node newLeft, newRight;
780
781
152907
  if (childrenRight.size() == 0 && leftConst != zero)
782
  {
783
487
    Assert(childrenLeft.back().isConst()
784
           && childrenLeft.back().getConst<BitVector>() == leftConst);
785
487
    if (childrenLeft.size() == 1)
786
    {
787
      // c = 0 ==> false
788
232
      return utils::mkFalse();
789
    }
790
    // special case - if right is empty and left has a constant, move the
791
    // constant
792
255
    childrenRight.push_back(utils::mkConst(-leftConst));
793
255
    childrenLeft.pop_back();
794
255
    changed = true;
795
  }
796
797
152675
  if (childrenLeft.size() == 0)
798
  {
799
2380
    if (rightConst != zero)
800
    {
801
1868
      Assert(childrenRight.back().isConst()
802
             && childrenRight.back().getConst<BitVector>() == rightConst);
803
1868
      if (childrenRight.size() == 1)
804
      {
805
        // 0 = c ==> false
806
1376
        return utils::mkFalse();
807
      }
808
      // special case - if left is empty and right has a constant, move the
809
      // constant
810
492
      newLeft = utils::mkConst(-rightConst);
811
492
      childrenRight.pop_back();
812
492
      changed = true;
813
    }
814
    else
815
    {
816
512
      newLeft = utils::mkConst(size, (unsigned)0);
817
    }
818
  }
819
  else
820
  {
821
150295
    newLeft = utils::mkNaryNode(kind::BITVECTOR_PLUS, childrenLeft);
822
  }
823
824
151299
  if (childrenRight.size() == 0)
825
  {
826
19112
    newRight = utils::mkConst(size, (unsigned)0);
827
  }
828
  else
829
  {
830
132187
    newRight = utils::mkNaryNode(kind::BITVECTOR_PLUS, childrenRight);
831
  }
832
833
151299
  if (!changed)
834
  {
835
148159
    return node;
836
  }
837
838
3140
  if (newLeft == newRight)
839
  {
840
4
    Assert(newLeft == utils::mkConst(size, (unsigned)0));
841
4
    return utils::mkTrue();
842
  }
843
844
3136
  if (newLeft < newRight)
845
  {
846
933
    Assert((newRight == left && newLeft == right)
847
           || Rewriter::rewrite(newRight) != left
848
           || Rewriter::rewrite(newLeft) != right);
849
933
    return newRight.eqNode(newLeft);
850
  }
851
852
2203
  Assert((newLeft == left && newRight == right)
853
         || Rewriter::rewrite(newLeft) != left
854
         || Rewriter::rewrite(newRight) != right);
855
2203
  return newLeft.eqNode(newRight);
856
}
857
858
template<> inline
859
302727
bool RewriteRule<BitwiseEq>::applies(TNode node) {
860
640066
  if (node.getKind() != kind::EQUAL ||
861
337339
      utils::getSize(node[0]) != 1) {
862
298868
    return false;
863
  }
864
7718
  TNode term;
865
7718
  BitVector c;
866
3859
  if (node[0].getKind() == kind::CONST_BITVECTOR) {
867
144
    c = node[0].getConst<BitVector>();
868
144
    term = node[1];
869
  }
870
3715
  else if (node[1].getKind() == kind::CONST_BITVECTOR) {
871
2274
    c = node[1].getConst<BitVector>();
872
2274
    term = node[0];
873
  }
874
  else {
875
1441
    return false;
876
  }
877
2418
  switch (term.getKind()) {
878
834
    case kind::BITVECTOR_AND:
879
    case kind::BITVECTOR_OR:
880
      //operator BITVECTOR_XOR 2: "bitwise xor"
881
    case kind::BITVECTOR_NOT:
882
    case kind::BITVECTOR_NAND:
883
    case kind::BITVECTOR_NOR:
884
      //operator BITVECTOR_XNOR 2 "bitwise xnor"
885
    case kind::BITVECTOR_COMP:
886
    case kind::BITVECTOR_NEG:
887
834
      return true;
888
      break;
889
1584
    default:
890
1584
      break;
891
  }
892
1584
  return false;
893
}
894
895
896
119
static inline Node mkNodeKind(Kind k, TNode node, TNode c) {
897
119
  unsigned i = 0;
898
119
  unsigned nc = node.getNumChildren();
899
238
  NodeBuilder<> nb(k);
900
1247
  for(; i < nc; ++i) {
901
564
    nb << node[i].eqNode(c);
902
  }
903
238
  return nb;
904
}
905
906
907
template<> inline
908
417
Node RewriteRule<BitwiseEq>::apply(TNode node) {
909
417
  Debug("bv-rewrite") << "RewriteRule<BitwiseEq>(" << node << ")" << std::endl;
910
911
834
  TNode term;
912
834
  BitVector c;
913
914
417
  if (node[0].getKind() == kind::CONST_BITVECTOR) {
915
4
    c = node[0].getConst<BitVector>();
916
4
    term = node[1];
917
  }
918
413
  else if (node[1].getKind() == kind::CONST_BITVECTOR) {
919
413
    c = node[1].getConst<BitVector>();
920
413
    term = node[0];
921
  }
922
923
417
  bool eqOne = (c == BitVector(1,(unsigned)1));
924
925
417
  switch (term.getKind()) {
926
49
    case kind::BITVECTOR_AND:
927
49
      if (eqOne) {
928
19
        return mkNodeKind(kind::AND, term, utils::mkConst(1, (unsigned)1));
929
      }
930
      else {
931
30
        return mkNodeKind(kind::OR, term, utils::mkConst(1, (unsigned)0));
932
      }
933
      break;
934
    case kind::BITVECTOR_NAND:
935
      if (eqOne) {
936
        return mkNodeKind(kind::OR, term, utils::mkConst(1, (unsigned)0));
937
      }
938
      else {
939
        return mkNodeKind(kind::AND, term, utils::mkConst(1, (unsigned)1));
940
      }
941
      break;
942
70
    case kind::BITVECTOR_OR:
943
70
      if (eqOne) {
944
62
        return mkNodeKind(kind::OR, term, utils::mkConst(1, (unsigned)1));
945
      }
946
      else {
947
8
        return mkNodeKind(kind::AND, term, utils::mkConst(1, (unsigned)0));
948
      }
949
      break;
950
    case kind::BITVECTOR_NOR:
951
      if (eqOne) {
952
        return mkNodeKind(kind::AND, term, utils::mkConst(1, (unsigned)0));
953
      }
954
      else {
955
        return mkNodeKind(kind::OR, term, utils::mkConst(1, (unsigned)1));
956
      }
957
      break;
958
138
    case kind::BITVECTOR_NOT:
959
138
      return term[0].eqNode(utils::mkConst(~c));
960
144
    case kind::BITVECTOR_COMP:
961
144
      Assert(term.getNumChildren() == 2);
962
144
      if (eqOne) {
963
132
        return term[0].eqNode(term[1]);
964
      }
965
      else {
966
12
        return term[0].eqNode(term[1]).notNode();
967
      }
968
16
    case kind::BITVECTOR_NEG:
969
16
      return term[0].eqNode(utils::mkConst(c));
970
    default:
971
      break;
972
  }
973
  Unreachable();
974
}
975
976
977
/**
978
 * -(c * expr) ==> (-c * expr)
979
 * where c is a constant
980
 */
981
template<> inline
982
18254
bool RewriteRule<NegMult>::applies(TNode node) {
983
73016
  if(node.getKind()!= kind::BITVECTOR_NEG ||
984
54762
     node[0].getKind() != kind::BITVECTOR_MULT) {
985
17286
    return false;
986
  }
987
968
  return node[node.getNumChildren()-1].isConst();
988
}
989
990
template<> inline
991
Node RewriteRule<NegMult>::apply(TNode node) {
992
  Debug("bv-rewrite") << "RewriteRule<NegMult>(" << node << ")" << std::endl;
993
  TNode mult = node[0];
994
  NodeBuilder<> nb(kind::BITVECTOR_MULT);
995
  BitVector bv(utils::getSize(node), (unsigned)1);
996
  TNode::iterator child_it = mult.begin();
997
  for(; (child_it+1) != mult.end(); ++child_it) {
998
    nb << (*child_it);
999
  }
1000
  Assert((*child_it).isConst());
1001
  bv = (*child_it).getConst<BitVector>();
1002
  nb << utils::mkConst(-bv);
1003
  return Node(nb);
1004
}
1005
1006
template<> inline
1007
35185
bool RewriteRule<NegSub>::applies(TNode node) {
1008
88245
  return (node.getKind() == kind::BITVECTOR_NEG &&
1009
88245
          node[0].getKind() == kind::BITVECTOR_SUB);
1010
}
1011
1012
template <>
1013
185
inline Node RewriteRule<NegSub>::apply(TNode node)
1014
{
1015
185
  Debug("bv-rewrite") << "RewriteRule<NegSub>(" << node << ")" << std::endl;
1016
  return NodeManager::currentNM()->mkNode(
1017
185
      kind::BITVECTOR_SUB, node[0][1], node[0][0]);
1018
}
1019
1020
template<> inline
1021
36238
bool RewriteRule<NegPlus>::applies(TNode node) {
1022
108714
  return (node.getKind() == kind::BITVECTOR_NEG &&
1023
108714
          node[0].getKind() == kind::BITVECTOR_PLUS);
1024
}
1025
1026
template <>
1027
1238
inline Node RewriteRule<NegPlus>::apply(TNode node)
1028
{
1029
1238
  Debug("bv-rewrite") << "RewriteRule<NegPlus>(" << node << ")" << std::endl;
1030
1238
  NodeManager *nm = NodeManager::currentNM();
1031
2476
  std::vector<Node> children;
1032
3728
  for (unsigned i = 0; i < node[0].getNumChildren(); ++i)
1033
  {
1034
2490
    children.push_back(nm->mkNode(kind::BITVECTOR_NEG, node[0][i]));
1035
  }
1036
2476
  return utils::mkNaryNode(kind::BITVECTOR_PLUS, children);
1037
}
1038
1039
struct Count {
1040
  unsigned pos;
1041
  unsigned neg;
1042
754999
  Count() : pos(0), neg(0) {}
1043
754999
  Count(unsigned p, unsigned n):
1044
    pos(p),
1045
754999
    neg(n)
1046
754999
  {}
1047
};
1048
1049
755917
inline static void insert(std::unordered_map<TNode, Count, TNodeHashFunction>& map, TNode node, bool neg) {
1050
755917
  if(map.find(node) == map.end()) {
1051
754999
    Count c = neg? Count(0,1) : Count(1, 0);
1052
754999
    map[node] = c;
1053
  } else {
1054
918
    if (neg) {
1055
357
      ++(map[node].neg);
1056
    } else {
1057
561
      ++(map[node].pos);
1058
    }
1059
  }
1060
755917
}
1061
1062
template<> inline
1063
307964
bool RewriteRule<AndSimplify>::applies(TNode node) {
1064
307964
  return (node.getKind() == kind::BITVECTOR_AND);
1065
}
1066
1067
template <>
1068
153982
inline Node RewriteRule<AndSimplify>::apply(TNode node)
1069
{
1070
307964
  Debug("bv-rewrite") << "RewriteRule<AndSimplify>(" << node << ")"
1071
153982
                      << std::endl;
1072
1073
153982
  NodeManager *nm = NodeManager::currentNM();
1074
  // this will remove duplicates
1075
307964
  std::unordered_map<TNode, Count, TNodeHashFunction> subterms;
1076
153982
  unsigned size = utils::getSize(node);
1077
307964
  BitVector constant = BitVector::mkOnes(size);
1078
488353
  for (unsigned i = 0; i < node.getNumChildren(); ++i)
1079
  {
1080
668742
    TNode current = node[i];
1081
    // simplify constants
1082
334371
    if (current.getKind() == kind::CONST_BITVECTOR)
1083
    {
1084
259808
      BitVector bv = current.getConst<BitVector>();
1085
129904
      constant = constant & bv;
1086
    }
1087
    else
1088
    {
1089
204467
      if (current.getKind() == kind::BITVECTOR_NOT)
1090
      {
1091
65873
        insert(subterms, current[0], true);
1092
      }
1093
      else
1094
      {
1095
138594
        insert(subterms, current, false);
1096
      }
1097
    }
1098
  }
1099
1100
307964
  std::vector<Node> children;
1101
1102
153982
  if (constant == BitVector(size, (unsigned)0))
1103
  {
1104
38898
    return utils::mkZero(size);
1105
  }
1106
1107
115084
  if (constant != BitVector::mkOnes(size))
1108
  {
1109
44708
    children.push_back(utils::mkConst(constant));
1110
  }
1111
1112
  std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it =
1113
115084
      subterms.begin();
1114
1115
493520
  for (; it != subterms.end(); ++it)
1116
  {
1117
189343
    if (it->second.pos > 0 && it->second.neg > 0)
1118
    {
1119
      // if we have a and ~a
1120
125
      return utils::mkZero(size);
1121
    }
1122
    else
1123
    {
1124
      // idempotence
1125
189218
      if (it->second.neg > 0)
1126
      {
1127
        // if it only occured negated
1128
59253
        children.push_back(nm->mkNode(kind::BITVECTOR_NOT, it->first));
1129
      }
1130
      else
1131
      {
1132
        // if it only occured positive
1133
129965
        children.push_back(it->first);
1134
      }
1135
    }
1136
  }
1137
114959
  if (children.size() == 0)
1138
  {
1139
207
    return utils::mkOnes(size);
1140
  }
1141
1142
114752
  return utils::mkSortedNode(kind::BITVECTOR_AND, children);
1143
}
1144
1145
template<> inline
1146
363928
bool RewriteRule<FlattenAssocCommutNoDuplicates>::applies(TNode node) {
1147
363928
  Kind kind = node.getKind();
1148
363928
  if (kind != kind::BITVECTOR_OR &&
1149
      kind != kind::BITVECTOR_AND)
1150
    return false;
1151
363928
  TNode::iterator child_it = node.begin();
1152
2266518
  for(; child_it != node.end(); ++child_it) {
1153
992671
    if ((*child_it).getKind() == kind) {
1154
41376
      return true;
1155
    }
1156
  }
1157
322552
  return false;
1158
}
1159
1160
template<> inline
1161
20688
Node RewriteRule<FlattenAssocCommutNoDuplicates>::apply(TNode node) {
1162
20688
  Debug("bv-rewrite") << "RewriteRule<FlattenAssocCommut>(" << node << ")" << std::endl;
1163
41376
  std::vector<Node> processingStack;
1164
20688
  processingStack.push_back(node);
1165
41376
  std::unordered_set<TNode, TNodeHashFunction> processed;
1166
41376
  std::vector<Node> children;
1167
20688
  Kind kind = node.getKind();
1168
1169
398276
  while (! processingStack.empty()) {
1170
376106
    TNode current = processingStack.back();
1171
188794
    processingStack.pop_back();
1172
188794
    if (processed.count(current))
1173
1482
      continue;
1174
1175
187312
    processed.insert(current);
1176
1177
    // flatten expression
1178
187312
    if (current.getKind() == kind) {
1179
213431
      for (unsigned i = 0; i < current.getNumChildren(); ++i) {
1180
168106
        processingStack.push_back(current[i]);
1181
      }
1182
    } else {
1183
141987
      children.push_back(current);
1184
    }
1185
  }
1186
41376
  return utils::mkSortedNode(kind, children);
1187
}
1188
1189
1190
template<> inline
1191
378504
bool RewriteRule<OrSimplify>::applies(TNode node) {
1192
378504
  return (node.getKind() == kind::BITVECTOR_OR);
1193
}
1194
1195
template <>
1196
189246
inline Node RewriteRule<OrSimplify>::apply(TNode node)
1197
{
1198
189246
  Debug("bv-rewrite") << "RewriteRule<OrSimplify>(" << node << ")" << std::endl;
1199
1200
189246
  NodeManager *nm = NodeManager::currentNM();
1201
  // this will remove duplicates
1202
378492
  std::unordered_map<TNode, Count, TNodeHashFunction> subterms;
1203
189246
  unsigned size = utils::getSize(node);
1204
378492
  BitVector constant(size, (unsigned)0);
1205
1206
927325
  for (unsigned i = 0; i < node.getNumChildren(); ++i)
1207
  {
1208
1476158
    TNode current = node[i];
1209
    // simplify constants
1210
738079
    if (current.getKind() == kind::CONST_BITVECTOR)
1211
    {
1212
412054
      BitVector bv = current.getConst<BitVector>();
1213
206027
      constant = constant | bv;
1214
    }
1215
    else
1216
    {
1217
532052
      if (current.getKind() == kind::BITVECTOR_NOT)
1218
      {
1219
32377
        insert(subterms, current[0], true);
1220
      }
1221
      else
1222
      {
1223
499675
        insert(subterms, current, false);
1224
      }
1225
    }
1226
  }
1227
1228
378492
  std::vector<Node> children;
1229
1230
189246
  if (constant == BitVector::mkOnes(size))
1231
  {
1232
10402
    return utils::mkOnes(size);
1233
  }
1234
1235
178844
  if (constant != BitVector(size, (unsigned)0))
1236
  {
1237
89413
    children.push_back(utils::mkConst(constant));
1238
  }
1239
1240
  std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it =
1241
178844
      subterms.begin();
1242
1243
1233834
  for (; it != subterms.end(); ++it)
1244
  {
1245
527700
    if (it->second.pos > 0 && it->second.neg > 0)
1246
    {
1247
      // if we have a or ~a
1248
205
      return utils::mkOnes(size);
1249
    }
1250
    else
1251
    {
1252
      // idempotence
1253
527495
      if (it->second.neg > 0)
1254
      {
1255
        // if it only occured negated
1256
31918
        children.push_back(nm->mkNode(kind::BITVECTOR_NOT, it->first));
1257
      }
1258
      else
1259
      {
1260
        // if it only occured positive
1261
495577
        children.push_back(it->first);
1262
      }
1263
    }
1264
  }
1265
1266
178639
  if (children.size() == 0)
1267
  {
1268
1382
    return utils::mkZero(size);
1269
  }
1270
177257
  return utils::mkSortedNode(kind::BITVECTOR_OR, children);
1271
}
1272
1273
template<> inline
1274
22196
bool RewriteRule<XorSimplify>::applies(TNode node) {
1275
22196
  return (node.getKind() == kind::BITVECTOR_XOR);
1276
}
1277
1278
template <>
1279
11098
inline Node RewriteRule<XorSimplify>::apply(TNode node)
1280
{
1281
22196
  Debug("bv-rewrite") << "RewriteRule<XorSimplify>(" << node << ")"
1282
11098
                      << std::endl;
1283
1284
11098
  NodeManager *nm = NodeManager::currentNM();
1285
22196
  std::unordered_map<TNode, Count, TNodeHashFunction> subterms;
1286
11098
  unsigned size = utils::getSize(node);
1287
22196
  BitVector constant;
1288
11098
  bool const_set = false;
1289
1290
33489
  for (unsigned i = 0; i < node.getNumChildren(); ++i)
1291
  {
1292
44782
    TNode current = node[i];
1293
    // simplify constants
1294
22391
    if (current.getKind() == kind::CONST_BITVECTOR)
1295
    {
1296
5986
      BitVector bv = current.getConst<BitVector>();
1297
2993
      if (const_set)
1298
      {
1299
582
        constant = constant ^ bv;
1300
      }
1301
      else
1302
      {
1303
2411
        const_set = true;
1304
2411
        constant = bv;
1305
      }
1306
    }
1307
    else
1308
    {
1309
      // collect number of occurances of each term and its negation
1310
19398
      if (current.getKind() == kind::BITVECTOR_NOT)
1311
      {
1312
1058
        insert(subterms, current[0], true);
1313
      }
1314
      else
1315
      {
1316
18340
        insert(subterms, current, false);
1317
      }
1318
    }
1319
  }
1320
1321
22196
  std::vector<Node> children;
1322
1323
  std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it =
1324
11098
      subterms.begin();
1325
11098
  unsigned true_count = 0;
1326
11098
  bool seen_false = false;
1327
49734
  for (; it != subterms.end(); ++it)
1328
  {
1329
19318
    unsigned pos = it->second.pos;  // number of positive occurances
1330
19318
    unsigned neg = it->second.neg;  // number of negated occurances
1331
1332
    // remove duplicates using the following rules
1333
    // a xor a ==> false
1334
    // false xor false ==> false
1335
19318
    seen_false = seen_false ? seen_false : (pos > 1 || neg > 1);
1336
    // check what did not reduce
1337
19318
    if (pos % 2 && neg % 2)
1338
    {
1339
      // we have a xor ~a ==> true
1340
5
      ++true_count;
1341
    }
1342
19313
    else if (pos % 2)
1343
    {
1344
      // we had a positive occurence left
1345
18185
      children.push_back(it->first);
1346
    }
1347
1128
    else if (neg % 2)
1348
    {
1349
      // we had a negative occurence left
1350
1053
      children.push_back(nm->mkNode(kind::BITVECTOR_NOT, it->first));
1351
    }
1352
    // otherwise both reduced to false
1353
  }
1354
1355
22196
  std::vector<BitVector> xorConst;
1356
22196
  BitVector true_bv = BitVector::mkOnes(size);
1357
22196
  BitVector false_bv(size, (unsigned)0);
1358
1359
11098
  if (true_count)
1360
  {
1361
    // true xor ... xor true ==> true (odd)
1362
    //                       ==> false (even)
1363
5
    xorConst.push_back(true_count % 2 ? true_bv : false_bv);
1364
  }
1365
11098
  if (seen_false)
1366
  {
1367
75
    xorConst.push_back(false_bv);
1368
  }
1369
11098
  if (const_set)
1370
  {
1371
2411
    xorConst.push_back(constant);
1372
  }
1373
1374
11098
  if (xorConst.size() > 0)
1375
  {
1376
4974
    BitVector result = xorConst[0];
1377
2491
    for (unsigned i = 1; i < xorConst.size(); ++i)
1378
    {
1379
4
      result = result ^ xorConst[i];
1380
    }
1381
2487
    children.push_back(utils::mkConst(result));
1382
  }
1383
1384
11098
  Assert(children.size());
1385
1386
22196
  return utils::mkSortedNode(kind::BITVECTOR_XOR, children);
1387
}
1388
1389
/**
1390
 * BitwiseSlicing
1391
 *
1392
 * (a bvand c) ==> (concat (bvand a[i0:j0] c0) ... (bvand a[in:jn] cn))
1393
 *  where c0,..., cn are maximally continuous substrings of 0 or 1 in the constant c
1394
 *
1395
 * Note: this rule assumes AndSimplify has already been called on the node
1396
 */
1397
template<> inline
1398
184284
bool RewriteRule<BitwiseSlicing>::applies(TNode node) {
1399
514989
  if ((node.getKind() != kind::BITVECTOR_AND &&
1400
245054
      node.getKind() != kind::BITVECTOR_OR &&
1401
666089
      node.getKind() != kind::BITVECTOR_XOR) ||
1402
383172
      utils::getSize(node) == 1)
1403
128630
    return false;
1404
  // find the first constant and return true if it's not only 1..1 or only 0..0
1405
  // (there could be more than one constant)
1406
172176
  for (unsigned i = 0; i < node.getNumChildren(); ++i) {
1407
119738
    if (node[i].getKind() == kind::CONST_BITVECTOR) {
1408
6432
      BitVector constant = node[i].getConst<BitVector>();
1409
      // we do not apply the rule if the constant is all 0s or all 1s
1410
3216
      if (constant == BitVector(utils::getSize(node), 0u)) return false;
1411
1412
6152
      for (unsigned j = 0, csize = constant.getSize(); j < csize; ++j)
1413
      {
1414
6042
        if (!constant.isBitSet(j)) return true;
1415
      }
1416
110
      return false;
1417
    }
1418
  }
1419
52438
  return false;
1420
}
1421
1422
template <>
1423
1553
inline Node RewriteRule<BitwiseSlicing>::apply(TNode node)
1424
{
1425
3106
  Debug("bv-rewrite") << "RewriteRule<BitwiseSlicing>(" << node << ")"
1426
1553
                      << std::endl;
1427
1553
  NodeManager *nm = NodeManager::currentNM();
1428
  // get the constant
1429
1553
  bool found_constant = false;
1430
3106
  TNode constant;
1431
3106
  std::vector<Node> other_children;
1432
4743
  for (unsigned i = 0; i < node.getNumChildren(); ++i)
1433
  {
1434
3190
    if (node[i].getKind() == kind::CONST_BITVECTOR && !found_constant)
1435
    {
1436
1553
      constant = node[i];
1437
1553
      found_constant = true;
1438
    }
1439
    else
1440
    {
1441
1637
      other_children.push_back(node[i]);
1442
    }
1443
  }
1444
1553
  Assert(found_constant && other_children.size() == node.getNumChildren() - 1);
1445
1446
3106
  Node other = utils::mkNaryNode(node.getKind(), other_children);
1447
1448
3106
  BitVector bv_constant = constant.getConst<BitVector>();
1449
3106
  std::vector<Node> concat_children;
1450
1553
  int start = bv_constant.getSize() - 1;
1451
1553
  int end = start;
1452
34983
  for (int i = end - 1; i >= 0; --i)
1453
  {
1454
33430
    if (bv_constant.isBitSet(i + 1) != bv_constant.isBitSet(i))
1455
    {
1456
5398
      Node other_extract = utils::mkExtract(other, end, start);
1457
5398
      Node const_extract = utils::mkExtract(constant, end, start);
1458
      Node bitwise_op =
1459
5398
          nm->mkNode(node.getKind(), const_extract, other_extract);
1460
2699
      concat_children.push_back(bitwise_op);
1461
2699
      start = end = i;
1462
    }
1463
    else
1464
    {
1465
30731
      start--;
1466
    }
1467
33430
    if (i == 0)
1468
    {
1469
3106
      Node other_extract = utils::mkExtract(other, end, 0);
1470
3106
      Node const_extract = utils::mkExtract(constant, end, 0);
1471
      Node bitwise_op =
1472
3106
          nm->mkNode(node.getKind(), const_extract, other_extract);
1473
1553
      concat_children.push_back(bitwise_op);
1474
    }
1475
  }
1476
1553
  Node result = utils::mkConcat(concat_children);
1477
1553
  Debug("bv-rewrite") << "    =>" << result << std::endl;
1478
3106
  return result;
1479
}
1480
1481
template <>
1482
302630
inline bool RewriteRule<NormalizeEqPlusNeg>::applies(TNode node)
1483
{
1484
302630
  return node.getKind() == kind::EQUAL
1485
910174
         && (node[0].getKind() == kind::BITVECTOR_PLUS
1486
621173
             || node[1].getKind() == kind::BITVECTOR_PLUS);
1487
}
1488
1489
template <>
1490
1142
inline Node RewriteRule<NormalizeEqPlusNeg>::apply(TNode node)
1491
{
1492
2284
  Debug("bv-rewrite") << "RewriteRule<NormalizeEqPlusNeg>(" << node << ")"
1493
1142
                      << std::endl;
1494
1495
2284
  NodeBuilder<> nb_lhs(kind::BITVECTOR_PLUS);
1496
2284
  NodeBuilder<> nb_rhs(kind::BITVECTOR_PLUS);
1497
1142
  NodeManager *nm = NodeManager::currentNM();
1498
1499
1142
  if (node[0].getKind() == kind::BITVECTOR_PLUS)
1500
  {
1501
13342
    for (const TNode &n : node[0])
1502
    {
1503
12667
      if (n.getKind() == kind::BITVECTOR_NEG)
1504
211
        nb_rhs << n[0];
1505
      else
1506
12456
        nb_lhs << n;
1507
    }
1508
  }
1509
  else
1510
  {
1511
467
    nb_lhs << node[0];
1512
  }
1513
1514
1142
  if (node[1].getKind() == kind::BITVECTOR_PLUS)
1515
  {
1516
1494
    for (const TNode &n : node[1])
1517
    {
1518
1021
      if (n.getKind() == kind::BITVECTOR_NEG)
1519
140
        nb_lhs << n[0];
1520
      else
1521
881
        nb_rhs << n;
1522
    }
1523
  }
1524
  else
1525
  {
1526
669
    nb_rhs << node[1];
1527
  }
1528
1529
2284
  Node zero = utils::mkZero(utils::getSize(node[0]));
1530
1531
2284
  Node lhs, rhs;
1532
1142
  if (nb_lhs.getNumChildren() == 0)
1533
  {
1534
11
    lhs = zero;
1535
  }
1536
1131
  else if (nb_lhs.getNumChildren() == 1)
1537
  {
1538
482
    lhs = nb_lhs[0];
1539
  }
1540
  else
1541
  {
1542
649
    lhs = nb_lhs.constructNode();
1543
  }
1544
1142
  if (nb_rhs.getNumChildren() == 0)
1545
  {
1546
    rhs = zero;
1547
  }
1548
1142
  else if (nb_rhs.getNumChildren() == 1)
1549
  {
1550
625
    rhs = nb_rhs[0];
1551
  }
1552
  else
1553
  {
1554
517
    rhs = nb_rhs.constructNode();
1555
  }
1556
2284
  return nm->mkNode(node.getKind(), lhs, rhs);
1557
}
1558
1559
// template<> inline
1560
// bool RewriteRule<>::applies(TNode node) {
1561
//   return (node.getKind() == kind::BITVECTOR_CONCAT);
1562
// }
1563
1564
// template<> inline
1565
// Node RewriteRule<>::apply(TNode node) {
1566
//   Debug("bv-rewrite") << "RewriteRule<>(" << node << ")" << std::endl;
1567
//   return resultNode;
1568
// }
1569
1570
1571
1572
}
1573
}
1574
}