GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/bitblast/bitblast_strategies_template.h Lines: 364 455 80.0 %
Date: 2021-03-23 Branches: 699 2412 29.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bitblast_strategies_template.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Liana Hadarean, Aina Niemetz, Tim King
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 Implementation of bitblasting functions for various operators.
13
 **
14
 ** Implementation of bitblasting functions for various operators.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H
20
#define CVC4__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H
21
22
#include <cmath>
23
#include <ostream>
24
25
#include "expr/node.h"
26
#include "theory/bv/bitblast/bitblast_utils.h"
27
#include "theory/bv/theory_bv_utils.h"
28
#include "theory/rewriter.h"
29
30
namespace CVC4 {
31
32
namespace theory {
33
namespace bv {
34
35
/**
36
 * Default Atom Bitblasting strategies:
37
 *
38
 * @param node the atom to be bitblasted
39
 * @param bb the bitblaster
40
 */
41
42
template <class T>
43
T UndefinedAtomBBStrategy(TNode node, TBitblaster<T>* bb) {
44
  Debug("bitvector") << "TheoryBV::Bitblaster Undefined bitblasting strategy for kind: "
45
                     << node.getKind() << "\n";
46
  Unreachable();
47
}
48
49
50
template <class T>
51
47000
T DefaultEqBB(TNode node, TBitblaster<T>* bb) {
52
47000
  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
53
54
47000
  Assert(node.getKind() == kind::EQUAL);
55
94000
  std::vector<T> lhs, rhs;
56
47000
  bb->bbTerm(node[0], lhs);
57
47000
  bb->bbTerm(node[1], rhs);
58
59
47000
  Assert(lhs.size() == rhs.size());
60
61
94000
  std::vector<T> bits_eq;
62
529172
  for (unsigned i = 0; i < lhs.size(); i++) {
63
964344
    T bit_eq = mkIff(lhs[i], rhs[i]);
64
482172
    bits_eq.push_back(bit_eq);
65
  }
66
47000
  T bv_eq = mkAnd(bits_eq);
67
94000
  return bv_eq;
68
}
69
70
template <class T>
71
T AdderUltBB(TNode node, TBitblaster<T>* bb) {
72
  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
73
  Assert(node.getKind() == kind::BITVECTOR_ULT);
74
  std::vector<T> a, b;
75
  bb->bbTerm(node[0], a);
76
  bb->bbTerm(node[1], b);
77
  Assert(a.size() == b.size());
78
79
  // a < b <=> ~ (add(a, ~b, 1).carry_out)
80
  std::vector<T> not_b;
81
  negateBits(b, not_b);
82
  T carry = mkTrue<T>();
83
84
  for (unsigned i = 0 ; i < a.size(); ++i) {
85
    carry = mkOr( mkAnd(a[i], not_b[i]),
86
                  mkAnd( mkXor(a[i], not_b[i]),
87
                         carry));
88
  }
89
  return mkNot(carry);
90
}
91
92
93
template <class T>
94
12043
T DefaultUltBB(TNode node, TBitblaster<T>* bb) {
95
12043
  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
96
12043
  Assert(node.getKind() == kind::BITVECTOR_ULT);
97
24086
  std::vector<T> a, b;
98
12043
  bb->bbTerm(node[0], a);
99
12043
  bb->bbTerm(node[1], b);
100
12043
  Assert(a.size() == b.size());
101
102
  // construct bitwise comparison
103
12043
  T res = uLessThanBB(a, b, false);
104
24086
  return res;
105
}
106
107
template <class T>
108
T DefaultUleBB(TNode node, TBitblaster<T>* bb){
109
  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
110
  Assert(node.getKind() == kind::BITVECTOR_ULE);
111
  std::vector<T> a, b;
112
113
  bb->bbTerm(node[0], a);
114
  bb->bbTerm(node[1], b);
115
  Assert(a.size() == b.size());
116
  // construct bitwise comparison
117
  T res = uLessThanBB(a, b, true);
118
  return res;
119
}
120
121
template <class T>
122
T DefaultUgtBB(TNode node, TBitblaster<T>* bb){
123
  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
124
  // should be rewritten
125
  Unimplemented();
126
}
127
template <class T>
128
T DefaultUgeBB(TNode node, TBitblaster<T>* bb){
129
  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
130
  // should be rewritten
131
  Unimplemented();
132
}
133
134
template <class T>
135
13350
T DefaultSltBB(TNode node, TBitblaster<T>* bb){
136
13350
  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
137
138
26700
  std::vector<T> a, b;
139
13350
  bb->bbTerm(node[0], a);
140
13350
  bb->bbTerm(node[1], b);
141
13350
  Assert(a.size() == b.size());
142
143
13350
  T res = sLessThanBB(a, b, false);
144
26700
  return res;
145
}
146
147
template <class T>
148
T DefaultSleBB(TNode node, TBitblaster<T>* bb){
149
  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
150
151
  std::vector<T> a, b;
152
  bb->bbTerm(node[0], a);
153
  bb->bbTerm(node[1], b);
154
  Assert(a.size() == b.size());
155
156
  T res = sLessThanBB(a, b, true);
157
  return res;
158
}
159
160
template <class T>
161
T DefaultSgtBB(TNode node, TBitblaster<T>* bb){
162
  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
163
  // should be rewritten
164
  Unimplemented();
165
}
166
167
template <class T>
168
T DefaultSgeBB(TNode node, TBitblaster<T>* bb){
169
  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
170
  // should be rewritten
171
  Unimplemented();
172
}
173
174
175
/// Term bitblasting strategies
176
177
/**
178
 * Default Term Bitblasting strategies
179
 *
180
 * @param node the term to be bitblasted
181
 * @param bits [output parameter] bits representing the new term
182
 * @param bb the bitblaster in which the clauses are added
183
 */
184
template <class T>
185
void UndefinedTermBBStrategy(TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
186
  Debug("bitvector") << "theory::bv:: Undefined bitblasting strategy for kind: "
187
                     << node.getKind() << "\n";
188
  Unreachable();
189
}
190
191
template <class T>
192
17847
void DefaultVarBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
193
17847
  Assert(bits.size() == 0);
194
17847
  bb->makeVariable(node, bits);
195
196
17847
  if(Debug.isOn("bitvector-bb")) {
197
    Debug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting  " << node << "\n";
198
    Debug("bitvector-bb") << "                           with bits  " << toString(bits);
199
  }
200
17847
}
201
202
template <class T>
203
12562
void DefaultConstBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
204
12562
  Debug("bitvector-bb") << "theory::bv::DefaultConstBB bitblasting " << node << "\n";
205
12562
  Assert(node.getKind() == kind::CONST_BITVECTOR);
206
12562
  Assert(bits.size() == 0);
207
208
127090
  for (unsigned i = 0; i < utils::getSize(node); ++i) {
209
229056
    Integer bit = node.getConst<BitVector>().extract(i, i).getValue();
210
114528
    if(bit == Integer(0)){
211
78281
      bits.push_back(mkFalse<T>());
212
    } else {
213
36247
      Assert(bit == Integer(1));
214
36247
      bits.push_back(mkTrue<T>());
215
    }
216
  }
217
12562
  if(Debug.isOn("bitvector-bb")) {
218
    Debug("bitvector-bb") << "with  bits: " << toString(bits) << "\n";
219
  }
220
12562
}
221
222
223
template <class T>
224
5226
void DefaultNotBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
225
5226
  Debug("bitvector-bb") << "theory::bv::DefaultNotBB bitblasting " << node << "\n";
226
5226
  Assert(node.getKind() == kind::BITVECTOR_NOT);
227
5226
  Assert(bits.size() == 0);
228
10452
  std::vector<T> bv;
229
5226
  bb->bbTerm(node[0], bv);
230
5226
  negateBits(bv, bits);
231
5226
}
232
233
template <class T>
234
12610
void DefaultConcatBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
235
12610
  Debug("bitvector-bb") << "theory::bv::DefaultConcatBB bitblasting " << node << "\n";
236
12610
  Assert(bits.size() == 0);
237
238
12610
  Assert(node.getKind() == kind::BITVECTOR_CONCAT);
239
44168
  for (int i = node.getNumChildren() -1 ; i >= 0; --i ) {
240
63116
    TNode current = node[i];
241
63116
    std::vector<T> current_bits;
242
31558
    bb->bbTerm(current, current_bits);
243
244
189647
    for(unsigned j = 0; j < utils::getSize(current); ++j) {
245
158089
      bits.push_back(current_bits[j]);
246
    }
247
  }
248
12610
  Assert(bits.size() == utils::getSize(node));
249
12610
  if(Debug.isOn("bitvector-bb")) {
250
    Debug("bitvector-bb") << "with  bits: " << toString(bits) << "\n";
251
  }
252
12610
}
253
254
template <class T>
255
4152
void DefaultAndBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
256
4152
  Debug("bitvector-bb") << "theory::bv::DefaultAndBB bitblasting " << node << "\n";
257
258
4152
  Assert(node.getKind() == kind::BITVECTOR_AND && bits.size() == 0);
259
260
4152
  bb->bbTerm(node[0], bits);
261
8304
  std::vector<T> current;
262
11256
  for(unsigned j = 1; j < node.getNumChildren(); ++j) {
263
7104
    bb->bbTerm(node[j], current);
264
24289
    for (unsigned i = 0; i < utils::getSize(node); ++i) {
265
17185
      bits[i] = mkAnd(bits[i], current[i]);
266
    }
267
7104
    current.clear();
268
  }
269
4152
  Assert(bits.size() == utils::getSize(node));
270
4152
}
271
272
template <class T>
273
5545
void DefaultOrBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
274
5545
  Debug("bitvector-bb") << "theory::bv::DefaultOrBB bitblasting " << node << "\n";
275
276
5545
  Assert(node.getKind() == kind::BITVECTOR_OR && bits.size() == 0);
277
278
5545
  bb->bbTerm(node[0], bits);
279
11090
  std::vector<T> current;
280
45414
  for(unsigned j = 1; j < node.getNumChildren(); ++j) {
281
39869
    bb->bbTerm(node[j], current);
282
84235
    for (unsigned i = 0; i < utils::getSize(node); ++i) {
283
44366
      bits[i] = mkOr(bits[i], current[i]);
284
    }
285
39869
    current.clear();
286
  }
287
5545
  Assert(bits.size() == utils::getSize(node));
288
5545
}
289
290
template <class T>
291
699
void DefaultXorBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
292
699
  Debug("bitvector-bb") << "theory::bv::DefaultXorBB bitblasting " << node << "\n";
293
294
699
  Assert(node.getKind() == kind::BITVECTOR_XOR && bits.size() == 0);
295
296
699
  bb->bbTerm(node[0], bits);
297
1398
  std::vector<T> current;
298
1404
  for(unsigned j = 1; j < node.getNumChildren(); ++j) {
299
705
    bb->bbTerm(node[j], current);
300
3974
    for (unsigned i = 0; i < utils::getSize(node); ++i) {
301
3269
      bits[i] = mkXor(bits[i], current[i]);
302
    }
303
705
    current.clear();
304
  }
305
699
  Assert(bits.size() == utils::getSize(node));
306
699
}
307
308
template <class T>
309
void DefaultXnorBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
310
  Debug("bitvector-bb") << "theory::bv::DefaultXnorBB bitblasting " << node << "\n";
311
312
  Assert(node.getNumChildren() == 2 && node.getKind() == kind::BITVECTOR_XNOR
313
         && bits.size() == 0);
314
  std::vector<T> lhs, rhs;
315
  bb->bbTerm(node[0], lhs);
316
  bb->bbTerm(node[1], rhs);
317
  Assert(lhs.size() == rhs.size());
318
319
  for (unsigned i = 0; i < lhs.size(); ++i) {
320
    bits.push_back(mkIff(lhs[i], rhs[i]));
321
  }
322
}
323
324
325
template <class T>
326
void DefaultNandBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
327
  Debug("bitvector") << "theory::bv:: Unimplemented kind "
328
                     << node.getKind() << "\n";
329
  Unimplemented();
330
}
331
template <class T>
332
void DefaultNorBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
333
  Debug("bitvector") << "theory::bv:: Unimplemented kind "
334
                     << node.getKind() << "\n";
335
  Unimplemented();
336
}
337
template <class T>
338
5970
void DefaultCompBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
339
5970
  Debug("bitvector") << "theory::bv:: DefaultCompBB bitblasting "<< node << "\n";
340
341
5970
  Assert(utils::getSize(node) == 1 && bits.size() == 0
342
         && node.getKind() == kind::BITVECTOR_COMP);
343
11940
  std::vector<T> a, b;
344
5970
  bb->bbTerm(node[0], a);
345
5970
  bb->bbTerm(node[1], b);
346
347
11940
  std::vector<T> bit_eqs;
348
62363
  for (unsigned i = 0; i < a.size(); ++i) {
349
112786
    T eq = mkIff(a[i], b[i]);
350
56393
    bit_eqs.push_back(eq);
351
  }
352
11940
  T a_eq_b = mkAnd(bit_eqs);
353
5970
  bits.push_back(a_eq_b);
354
5970
}
355
356
template <class T>
357
1034
void DefaultMultBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
358
1034
  Debug("bitvector") << "theory::bv:: DefaultMultBB bitblasting "<< node << "\n";
359
1034
  Assert(res.size() == 0 && node.getKind() == kind::BITVECTOR_MULT);
360
361
  // if (node.getNumChildren() == 2) {
362
  //   std::vector<T> a;
363
  //   std::vector<T> b;
364
  //   bb->bbTerm(node[0], a);
365
  //   bb->bbTerm(node[1], b);
366
  //   unsigned bw = utils::getSize(node);
367
  //   unsigned thresh = bw % 2 ? bw/2 : bw/2 - 1;
368
  //   bool no_overflow = true;
369
  //   for (unsigned i = thresh; i < bw; ++i) {
370
  //     if (a[i] != mkFalse<T> || b[i] != mkFalse<T> ) {
371
  //       no_overflow = false;
372
  //     }
373
  //   }
374
  //   if (no_overflow) {
375
  //     shiftAddMultiplier();
376
  //     return;
377
  //   }
378
379
  // }
380
381
2068
  std::vector<T> newres;
382
1034
  bb->bbTerm(node[0], res);
383
2108
  for(unsigned i = 1; i < node.getNumChildren(); ++i) {
384
2148
    std::vector<T> current;
385
1074
    bb->bbTerm(node[i], current);
386
1074
    newres.clear();
387
    // constructs a simple shift and add multiplier building the result
388
    // in res
389
1074
    shiftAddMultiplier(res, current, newres);
390
1074
    res = newres;
391
  }
392
1034
  if(Debug.isOn("bitvector-bb")) {
393
    Debug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
394
  }
395
1034
}
396
397
template <class T>
398
3425
void DefaultPlusBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
399
3425
  Debug("bitvector-bb") << "theory::bv::DefaultPlusBB bitblasting " << node << "\n";
400
3425
  Assert(node.getKind() == kind::BITVECTOR_PLUS && res.size() == 0);
401
402
3425
  bb->bbTerm(node[0], res);
403
404
6850
  std::vector<T> newres;
405
406
7083
  for(unsigned i = 1; i < node.getNumChildren(); ++i) {
407
7316
    std::vector<T> current;
408
3658
    bb->bbTerm(node[i], current);
409
3658
    newres.clear();
410
3658
    rippleCarryAdder(res, current, newres, mkFalse<T>());
411
3658
    res = newres;
412
  }
413
414
3425
  Assert(res.size() == utils::getSize(node));
415
3425
}
416
417
418
template <class T>
419
void DefaultSubBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
420
  Debug("bitvector-bb") << "theory::bv::DefaultSubBB bitblasting " << node << "\n";
421
  Assert(node.getKind() == kind::BITVECTOR_SUB && node.getNumChildren() == 2
422
         && bits.size() == 0);
423
424
  std::vector<T> a, b;
425
  bb->bbTerm(node[0], a);
426
  bb->bbTerm(node[1], b);
427
  Assert(a.size() == b.size() && utils::getSize(node) == a.size());
428
429
  // bvsub a b = adder(a, ~b, 1)
430
  std::vector<T> not_b;
431
  negateBits(b, not_b);
432
  rippleCarryAdder(a, not_b, bits, mkTrue<T>());
433
}
434
435
template <class T>
436
1588
void DefaultNegBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
437
1588
  Debug("bitvector-bb") << "theory::bv::DefaultNegBB bitblasting " << node << "\n";
438
1588
  Assert(node.getKind() == kind::BITVECTOR_NEG);
439
440
3176
  std::vector<T> a;
441
1588
  bb->bbTerm(node[0], a);
442
1588
  Assert(utils::getSize(node) == a.size());
443
444
  // -a = add(~a, 0, 1).
445
3176
  std::vector<T> not_a;
446
1588
  negateBits(a, not_a);
447
3176
  std::vector<T> zero;
448
1588
  makeZero(zero, utils::getSize(node));
449
450
1588
  rippleCarryAdder(not_a, zero, bits, mkTrue<T>());
451
1588
}
452
453
template <class T>
454
4567
void uDivModRec(const std::vector<T>& a, const std::vector<T>& b, std::vector<T>& q, std::vector<T>& r, unsigned rec_width) {
455
4567
  Assert(q.size() == 0 && r.size() == 0);
456
457
4567
  if(rec_width == 0 || isZero(a)) {
458
681
    makeZero(q, a.size());
459
681
    makeZero(r, a.size());
460
681
    return;
461
  }
462
463
7772
  std::vector<T> q1, r1;
464
7772
  std::vector<T> a1 = a;
465
3886
  rshift(a1, 1);
466
467
3886
  uDivModRec(a1, b, q1, r1, rec_width - 1);
468
  // shift the quotient and remainder (i.e. multiply by two) and add 1 to remainder if a is odd
469
3886
  lshift(q1, 1);
470
3886
  lshift(r1, 1);
471
472
473
7772
  T is_odd = mkIff(a[0], mkTrue<T>());
474
7772
  T one_if_odd = mkIte(is_odd, mkTrue<T>(), mkFalse<T>());
475
476
7772
  std::vector<T> zero;
477
3886
  makeZero(zero, b.size());
478
479
7772
  std::vector<T> r1_shift_add;
480
  // account for a being odd
481
3886
  rippleCarryAdder(r1, zero, r1_shift_add, one_if_odd);
482
  // now check if the remainder is greater than b
483
7772
  std::vector<T> not_b;
484
3886
  negateBits(b, not_b);
485
7772
  std::vector<T> r_minus_b;
486
7772
  T co1;
487
  // use adder because we need r_minus_b anyway
488
3886
  co1 = rippleCarryAdder(r1_shift_add, not_b, r_minus_b, mkTrue<T>());
489
  // sign is true if r1 < b
490
7772
  T sign = mkNot(co1);
491
492
3886
  q1[0] = mkIte(sign, q1[0], mkTrue<T>());
493
494
  // would be nice to have a high level ITE instead of bitwise
495
42802
  for(unsigned i = 0; i < a.size(); ++i) {
496
38916
    r1_shift_add[i] = mkIte(sign, r1_shift_add[i], r_minus_b[i]);
497
  }
498
499
  // check if a < b
500
501
7772
  std::vector<T> a_minus_b;
502
7772
  T co2 = rippleCarryAdder(a, not_b, a_minus_b, mkTrue<T>());
503
  // Node a_lt_b = a_minus_b.back();
504
7772
  T a_lt_b = mkNot(co2);
505
506
42802
  for(unsigned i = 0; i < a.size(); ++i) {
507
77832
    T qval = mkIte(a_lt_b, mkFalse<T>(), q1[i]);
508
77832
    T rval = mkIte(a_lt_b, a[i], r1_shift_add[i]);
509
38916
    q.push_back(qval);
510
38916
    r.push_back(rval);
511
  }
512
513
}
514
515
template <class T>
516
394
void DefaultUdivBB(TNode node, std::vector<T>& q, TBitblaster<T>* bb)
517
{
518
394
  Debug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node
519
                        << "\n";
520
394
  Assert(node.getKind() == kind::BITVECTOR_UDIV && q.size() == 0);
521
522
788
  std::vector<T> a, b;
523
394
  bb->bbTerm(node[0], a);
524
394
  bb->bbTerm(node[1], b);
525
526
788
  std::vector<T> r;
527
394
  uDivModRec(a, b, q, r, utils::getSize(node));
528
  // adding a special case for division by 0
529
788
  std::vector<T> iszero;
530
3076
  for (unsigned i = 0; i < b.size(); ++i)
531
  {
532
2682
    iszero.push_back(mkIff(b[i], mkFalse<T>()));
533
  }
534
788
  T b_is_0 = mkAnd(iszero);
535
536
3076
  for (unsigned i = 0; i < q.size(); ++i)
537
  {
538
2682
    q[i] = mkIte(b_is_0, mkTrue<T>(), q[i]);  // a udiv 0 is 11..11
539
2682
    r[i] = mkIte(b_is_0, a[i], r[i]);         // a urem 0 is a
540
  }
541
542
  // cache the remainder in case we need it later
543
788
  Node remainder = Rewriter::rewrite(
544
      NodeManager::currentNM()->mkNode(kind::BITVECTOR_UREM, node[0], node[1]));
545
394
  bb->storeBBTerm(remainder, r);
546
394
}
547
548
template <class T>
549
287
void DefaultUremBB(TNode node, std::vector<T>& rem, TBitblaster<T>* bb)
550
{
551
287
  Debug("bitvector-bb") << "theory::bv::DefaultUremBB bitblasting " << node
552
                        << "\n";
553
287
  Assert(node.getKind() == kind::BITVECTOR_UREM && rem.size() == 0);
554
555
574
  std::vector<T> a, b;
556
287
  bb->bbTerm(node[0], a);
557
287
  bb->bbTerm(node[1], b);
558
559
574
  std::vector<T> q;
560
287
  uDivModRec(a, b, q, rem, utils::getSize(node));
561
  // adding a special case for division by 0
562
574
  std::vector<T> iszero;
563
2251
  for (unsigned i = 0; i < b.size(); ++i)
564
  {
565
1964
    iszero.push_back(mkIff(b[i], mkFalse<T>()));
566
  }
567
574
  T b_is_0 = mkAnd(iszero);
568
569
2251
  for (unsigned i = 0; i < q.size(); ++i)
570
  {
571
1964
    q[i] = mkIte(b_is_0, mkTrue<T>(), q[i]);  // a udiv 0 is 11..11
572
1964
    rem[i] = mkIte(b_is_0, a[i], rem[i]);     // a urem 0 is a
573
  }
574
575
  // cache the quotient in case we need it later
576
574
  Node quotient = Rewriter::rewrite(
577
      NodeManager::currentNM()->mkNode(kind::BITVECTOR_UDIV, node[0], node[1]));
578
287
  bb->storeBBTerm(quotient, q);
579
287
}
580
581
template <class T>
582
void DefaultSdivBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
583
  Debug("bitvector") << "theory::bv:: Unimplemented kind "
584
                     << node.getKind() << "\n";
585
  Unimplemented();
586
}
587
template <class T>
588
void DefaultSremBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
589
  Debug("bitvector") << "theory::bv:: Unimplemented kind "
590
                     << node.getKind() << "\n";
591
  Unimplemented();
592
}
593
template <class T>
594
void DefaultSmodBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
595
  Debug("bitvector") << "theory::bv:: Unimplemented kind "
596
                     << node.getKind() << "\n";
597
  Unimplemented();
598
}
599
600
template <class T>
601
792
void DefaultShlBB(TNode node, std::vector<T>& res, TBitblaster<T>* bb)
602
{
603
792
  Debug("bitvector-bb") << "theory::bv::DefaultShlBB bitblasting " << node
604
                        << "\n";
605
792
  Assert(node.getKind() == kind::BITVECTOR_SHL && res.size() == 0);
606
1584
  std::vector<T> a, b;
607
792
  bb->bbTerm(node[0], a);
608
792
  bb->bbTerm(node[1], b);
609
610
  // check for b < log2(n)
611
792
  unsigned size = utils::getSize(node);
612
792
  unsigned log2_size = std::ceil(log2((double)size));
613
1584
  Node a_size = utils::mkConst(size, size);
614
615
1584
  std::vector<T> a_size_bits;
616
792
  DefaultConstBB(a_size, a_size_bits, bb);
617
1584
  T b_ult_a_size = uLessThanBB(b, a_size_bits, false);
618
619
1584
  std::vector<T> prev_res;
620
792
  res = a;
621
  // we only need to look at the bits bellow log2_a_size
622
2546
  for (unsigned s = 0; s < log2_size; ++s)
623
  {
624
    // barrel shift stage: at each stage you can either shift by 2^s bits
625
    // or leave the previous stage untouched
626
1754
    prev_res = res;
627
1754
    unsigned threshold = pow(2, s);
628
14526
    for (unsigned i = 0; i < a.size(); ++i)
629
    {
630
12772
      if (i < threshold)
631
      {
632
        // if b[s] is true then we must have shifted by at least 2^b bits so
633
        // all bits bellow 2^s will be 0, otherwise just use previous shift
634
        // value
635
4068
        res[i] = mkIte(b[s], mkFalse<T>(), prev_res[i]);
636
      }
637
      else
638
      {
639
        // if b[s]= 0, use previous value, otherwise shift by threshold  bits
640
8704
        Assert(i >= threshold);
641
8704
        res[i] = mkIte(b[s], prev_res[i - threshold], prev_res[i]);
642
      }
643
    }
644
  }
645
792
  prev_res = res;
646
5173
  for (unsigned i = 0; i < b.size(); ++i)
647
  {
648
    // this is fine  because b_ult_a_size has been bit-blasted
649
4381
    res[i] = mkIte(b_ult_a_size, prev_res[i], mkFalse<T>());
650
  }
651
652
792
  if (Debug.isOn("bitvector-bb"))
653
  {
654
    Debug("bitvector-bb") << "with bits: " << toString(res) << "\n";
655
  }
656
792
}
657
658
template <class T>
659
855
void DefaultLshrBB(TNode node, std::vector<T>& res, TBitblaster<T>* bb)
660
{
661
855
  Debug("bitvector-bb") << "theory::bv::DefaultLshrBB bitblasting " << node
662
                        << "\n";
663
855
  Assert(node.getKind() == kind::BITVECTOR_LSHR && res.size() == 0);
664
1710
  std::vector<T> a, b;
665
855
  bb->bbTerm(node[0], a);
666
855
  bb->bbTerm(node[1], b);
667
668
  // check for b < log2(n)
669
855
  unsigned size = utils::getSize(node);
670
855
  unsigned log2_size = std::ceil(log2((double)size));
671
1710
  Node a_size = utils::mkConst(size, size);
672
673
1710
  std::vector<T> a_size_bits;
674
855
  DefaultConstBB(a_size, a_size_bits, bb);
675
1710
  T b_ult_a_size = uLessThanBB(b, a_size_bits, false);
676
677
855
  res = a;
678
1710
  std::vector<T> prev_res;
679
680
2975
  for (unsigned s = 0; s < log2_size; ++s)
681
  {
682
    // barrel shift stage: at each stage you can either shift by 2^s bits
683
    // or leave the previous stage untouched
684
2120
    prev_res = res;
685
2120
    int threshold = pow(2, s);
686
24058
    for (unsigned i = 0; i < a.size(); ++i)
687
    {
688
21938
      if (i + threshold >= a.size())
689
      {
690
        // if b[s] is true then we must have shifted by at least 2^b bits so
691
        // all bits above 2^s will be 0, otherwise just use previous shift value
692
5916
        res[i] = mkIte(b[s], mkFalse<T>(), prev_res[i]);
693
      }
694
      else
695
      {
696
        // if b[s]= 0, use previous value, otherwise shift by threshold  bits
697
16022
        Assert(i + threshold < a.size());
698
16022
        res[i] = mkIte(mkNot(b[s]), prev_res[i], prev_res[i + threshold]);
699
      }
700
    }
701
  }
702
703
855
  prev_res = res;
704
7236
  for (unsigned i = 0; i < b.size(); ++i)
705
  {
706
    // this is fine  because b_ult_a_size has been bit-blasted
707
6381
    res[i] = mkIte(b_ult_a_size, prev_res[i], mkFalse<T>());
708
  }
709
710
855
  if (Debug.isOn("bitvector-bb"))
711
  {
712
    Debug("bitvector-bb") << "with bits: " << toString(res) << "\n";
713
  }
714
855
}
715
716
template <class T>
717
672
void DefaultAshrBB(TNode node, std::vector<T>& res, TBitblaster<T>* bb)
718
{
719
672
  Debug("bitvector-bb") << "theory::bv::DefaultAshrBB bitblasting " << node
720
                        << "\n";
721
672
  Assert(node.getKind() == kind::BITVECTOR_ASHR && res.size() == 0);
722
1344
  std::vector<T> a, b;
723
672
  bb->bbTerm(node[0], a);
724
672
  bb->bbTerm(node[1], b);
725
726
  //   check for b < n
727
672
  unsigned size = utils::getSize(node);
728
672
  unsigned log2_size = std::ceil(log2((double)size));
729
1344
  Node a_size = utils::mkConst(size, size);
730
731
1344
  std::vector<T> a_size_bits;
732
672
  DefaultConstBB(a_size, a_size_bits, bb);
733
1344
  T b_ult_a_size = uLessThanBB(b, a_size_bits, false);
734
735
672
  res = a;
736
1344
  T sign_bit = a.back();
737
1344
  std::vector<T> prev_res;
738
739
2066
  for (unsigned s = 0; s < log2_size; ++s)
740
  {
741
    // barrel shift stage: at each stage you can either shift by 2^s bits
742
    // or leave the previous stage untouched
743
1394
    prev_res = res;
744
1394
    int threshold = pow(2, s);
745
13790
    for (unsigned i = 0; i < a.size(); ++i)
746
    {
747
12396
      if (i + threshold >= a.size())
748
      {
749
        // if b[s] is true then we must have shifted by at least 2^b bits so
750
        // all bits above 2^s will be the sign bit, otherwise just use previous
751
        // shift value
752
3624
        res[i] = mkIte(b[s], sign_bit, prev_res[i]);
753
      }
754
      else
755
      {
756
        // if b[s]= 0, use previous value, otherwise shift by threshold  bits
757
8772
        Assert(i + threshold < a.size());
758
8772
        res[i] = mkIte(mkNot(b[s]), prev_res[i], prev_res[i + threshold]);
759
      }
760
    }
761
  }
762
763
672
  prev_res = res;
764
4576
  for (unsigned i = 0; i < b.size(); ++i)
765
  {
766
    // this is fine  because b_ult_a_size has been bit-blasted
767
3904
    res[i] = mkIte(b_ult_a_size, prev_res[i], sign_bit);
768
  }
769
770
672
  if (Debug.isOn("bitvector-bb"))
771
  {
772
    Debug("bitvector-bb") << "with bits: " << toString(res) << "\n";
773
  }
774
672
}
775
776
template <class T>
777
561
void DefaultUltbvBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
778
561
  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
779
561
  Assert(node.getKind() == kind::BITVECTOR_ULTBV);
780
1122
  std::vector<T> a, b;
781
561
  bb->bbTerm(node[0], a);
782
561
  bb->bbTerm(node[1], b);
783
561
  Assert(a.size() == b.size());
784
785
  // construct bitwise comparison
786
561
  res.push_back(uLessThanBB(a, b, false));
787
561
}
788
789
template <class T>
790
1104
void DefaultSltbvBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
791
1104
  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
792
1104
  Assert(node.getKind() == kind::BITVECTOR_SLTBV);
793
2208
  std::vector<T> a, b;
794
1104
  bb->bbTerm(node[0], a);
795
1104
  bb->bbTerm(node[1], b);
796
1104
  Assert(a.size() == b.size());
797
798
  // construct bitwise comparison
799
1104
  res.push_back(sLessThanBB(a, b, false));
800
1104
}
801
802
template <class T>
803
2881
void DefaultIteBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
804
2881
  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
805
2881
  Assert(node.getKind() == kind::BITVECTOR_ITE);
806
5762
  std::vector<T> cond, thenpart, elsepart;
807
2881
  bb->bbTerm(node[0], cond);
808
2881
  bb->bbTerm(node[1], thenpart);
809
2881
  bb->bbTerm(node[2], elsepart);
810
811
2881
  Assert(cond.size() == 1);
812
2881
  Assert(thenpart.size() == elsepart.size());
813
814
44858
  for (unsigned i = 0; i < thenpart.size(); ++i) {
815
    // (~cond OR thenpart) AND (cond OR elsepart)
816
41977
    res.push_back(mkAnd(mkOr(mkNot(cond[0]),thenpart[i]),mkOr(cond[0],elsepart[i])));
817
  }
818
2881
}
819
820
template <class T>
821
8848
void DefaultExtractBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
822
8848
  Assert(node.getKind() == kind::BITVECTOR_EXTRACT);
823
8848
  Assert(bits.size() == 0);
824
825
17696
  std::vector<T> base_bits;
826
8848
  bb->bbTerm(node[0], base_bits);
827
8848
  unsigned high = utils::getExtractHigh(node);
828
8848
  unsigned low  = utils::getExtractLow(node);
829
830
88432
  for (unsigned i = low; i <= high; ++i) {
831
79584
    bits.push_back(base_bits[i]);
832
  }
833
8848
  Assert(bits.size() == high - low + 1);
834
835
8848
  if(Debug.isOn("bitvector-bb")) {
836
    Debug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n";
837
    Debug("bitvector-bb") << "                               with bits " << toString(bits);
838
  }
839
8848
}
840
841
842
template <class T>
843
void DefaultRepeatBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
844
  Debug("bitvector") << "theory::bv:: Unimplemented kind "
845
                     << node.getKind() << "\n";
846
  // this should be rewritten
847
  Unimplemented();
848
}
849
850
template <class T>
851
void DefaultZeroExtendBB (TNode node, std::vector<T>& res_bits, TBitblaster<T>* bb) {
852
853
  Debug("bitvector-bb") << "theory::bv::DefaultZeroExtendBB bitblasting " << node  << "\n";
854
855
  // this should be rewritten
856
  Unimplemented();
857
858
}
859
860
template <class T>
861
7287
void DefaultSignExtendBB (TNode node, std::vector<T>& res_bits, TBitblaster<T>* bb) {
862
7287
  Debug("bitvector-bb") << "theory::bv::DefaultSignExtendBB bitblasting " << node  << "\n";
863
864
7287
  Assert(node.getKind() == kind::BITVECTOR_SIGN_EXTEND && res_bits.size() == 0);
865
866
14574
  std::vector<T> bits;
867
7287
  bb->bbTerm(node[0], bits);
868
869
14574
  T sign_bit = bits.back();
870
7287
  unsigned amount =
871
14574
      node.getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount;
872
873
26956
  for (unsigned i = 0; i < bits.size(); ++i ) {
874
19669
    res_bits.push_back(bits[i]);
875
  }
876
877
44855
  for (unsigned i = 0 ; i < amount ; ++i ) {
878
37568
    res_bits.push_back(sign_bit);
879
  }
880
881
7287
  Assert(res_bits.size() == amount + bits.size());
882
7287
}
883
884
template <class T>
885
void DefaultRotateRightBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
886
  Debug("bitvector") << "theory::bv:: Unimplemented kind "
887
                     << node.getKind() << "\n";
888
889
  Unimplemented();
890
}
891
892
template <class T>
893
void DefaultRotateLeftBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
894
  Debug("bitvector") << "theory::bv:: Unimplemented kind "
895
                     << node.getKind() << "\n";
896
  Unimplemented();
897
}
898
899
900
}
901
}
902
}
903
904
#endif