projects / cvc5.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
Updating the copyright headers and scripts.
[cvc5.git] / src / theory / bv / bitblast_strategies_template.h
1 /********************* */
2 /*! \file bitblast_strategies_template.h
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Liana Hadarean, Tim King, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2016 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 #ifndef __CVC4__BITBLAST__STRATEGIES_TEMPLATE_H
18 #define __CVC4__BITBLAST__STRATEGIES_TEMPLATE_H
19
20 #include "cvc4_private.h"
21 #include "expr/node.h"
22 #include "theory/bv/bitblast_utils.h"
23 #include "theory/bv/theory_bv_utils.h"
24 #include <ostream>
25 #include <cmath>
26 namespace CVC4 {
27
28 namespace theory {
29 namespace bv {
30
31 /**
32 * Default Atom Bitblasting strategies:
33 *
34 * @param node the atom to be bitblasted
35 * @param bb the bitblaster
36 */
37
38 template <class T>
39 T UndefinedAtomBBStrategy(TNode node, TBitblaster<T>* bb) {
40 Debug("bitvector") << "TheoryBV::Bitblaster Undefined bitblasting strategy for kind: "
41 << node.getKind() << "\n";
42 Unreachable();
43 }
44
45
46 template <class T>
47 T DefaultEqBB(TNode node, TBitblaster<T>* bb) {
48 Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
49
50 Assert(node.getKind() == kind::EQUAL);
51 std::vector<T> lhs, rhs;
52 bb->bbTerm(node[0], lhs);
53 bb->bbTerm(node[1], rhs);
54
55 Assert(lhs.size() == rhs.size());
56
57 std::vector<T> bits_eq;
58 for (unsigned i = 0; i < lhs.size(); i++) {
59 T bit_eq = mkIff(lhs[i], rhs[i]);
60 bits_eq.push_back(bit_eq);
61 }
62 T bv_eq = mkAnd(bits_eq);
63 return bv_eq;
64 }
65
66 template <class T>
67 T AdderUltBB(TNode node, TBitblaster<T>* bb) {
68 Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
69 Assert(node.getKind() == kind::BITVECTOR_ULT);
70 std::vector<T> a, b;
71 bb->bbTerm(node[0], a);
72 bb->bbTerm(node[1], b);
73 Assert(a.size() == b.size());
74
75 // a < b <=> ~ (add(a, ~b, 1).carry_out)
76 std::vector<T> not_b;
77 negateBits(b, not_b);
78 T carry = mkTrue<T>();
79
80 for (unsigned i = 0 ; i < a.size(); ++i) {
81 carry = mkOr( mkAnd(a[i], not_b[i]),
82 mkAnd( mkXor(a[i], not_b[i]),
83 carry));
84 }
85 return mkNot(carry);
86 }
87
88
89 template <class T>
90 T DefaultUltBB(TNode node, TBitblaster<T>* bb) {
91 Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
92 Assert(node.getKind() == kind::BITVECTOR_ULT);
93 std::vector<T> a, b;
94 bb->bbTerm(node[0], a);
95 bb->bbTerm(node[1], b);
96 Assert(a.size() == b.size());
97
98 // construct bitwise comparison
99 T res = uLessThanBB(a, b, false);
100 return res;
101 }
102
103 template <class T>
104 T DefaultUleBB(TNode node, TBitblaster<T>* bb){
105 Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
106 Assert(node.getKind() == kind::BITVECTOR_ULE);
107 std::vector<T> a, b;
108
109 bb->bbTerm(node[0], a);
110 bb->bbTerm(node[1], b);
111 Assert(a.size() == b.size());
112 // construct bitwise comparison
113 T res = uLessThanBB(a, b, true);
114 return res;
115 }
116
117 template <class T>
118 T DefaultUgtBB(TNode node, TBitblaster<T>* bb){
119 Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
120 // should be rewritten
121 Unimplemented();
122 }
123 template <class T>
124 T DefaultUgeBB(TNode node, TBitblaster<T>* bb){
125 Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
126 // should be rewritten
127 Unimplemented();
128 }
129
130 template <class T>
131 T DefaultSltBB(TNode node, TBitblaster<T>* bb){
132 Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
133
134 std::vector<T> a, b;
135 bb->bbTerm(node[0], a);
136 bb->bbTerm(node[1], b);
137 Assert(a.size() == b.size());
138
139 T res = sLessThanBB(a, b, false);
140 return res;
141 }
142
143 template <class T>
144 T DefaultSleBB(TNode node, TBitblaster<T>* bb){
145 Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
146
147 std::vector<T> a, b;
148 bb->bbTerm(node[0], a);
149 bb->bbTerm(node[1], b);
150 Assert(a.size() == b.size());
151
152 T res = sLessThanBB(a, b, true);
153 return res;
154 }
155
156 template <class T>
157 T DefaultSgtBB(TNode node, TBitblaster<T>* bb){
158 Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
159 // should be rewritten
160 Unimplemented();
161 }
162
163 template <class T>
164 T DefaultSgeBB(TNode node, TBitblaster<T>* bb){
165 Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
166 // should be rewritten
167 Unimplemented();
168 }
169
170
171 /// Term bitblasting strategies
172
173 /**
174 * Default Term Bitblasting strategies
175 *
176 * @param node the term to be bitblasted
177 * @param bits [output parameter] bits representing the new term
178 * @param bb the bitblaster in which the clauses are added
179 */
180 template <class T>
181 void UndefinedTermBBStrategy(TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
182 Debug("bitvector") << "theory::bv:: Undefined bitblasting strategy for kind: "
183 << node.getKind() << "\n";
184 Unreachable();
185 }
186
187 template <class T>
188 void DefaultVarBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
189 Assert(bits.size() == 0);
190 bb->makeVariable(node, bits);
191
192 if(Debug.isOn("bitvector-bb")) {
193 Debug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting " << node << "\n";
194 Debug("bitvector-bb") << " with bits " << toString(bits);
195 }
196 }
197
198 template <class T>
199 void DefaultConstBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
200 Debug("bitvector-bb") << "theory::bv::DefaultConstBB bitblasting " << node << "\n";
201 Assert(node.getKind() == kind::CONST_BITVECTOR);
202 Assert(bits.size() == 0);
203
204 for (unsigned i = 0; i < utils::getSize(node); ++i) {
205 Integer bit = node.getConst<BitVector>().extract(i, i).getValue();
206 if(bit == Integer(0)){
207 bits.push_back(mkFalse<T>());
208 } else {
209 Assert (bit == Integer(1));
210 bits.push_back(mkTrue<T>());
211 }
212 }
213 if(Debug.isOn("bitvector-bb")) {
214 Debug("bitvector-bb") << "with bits: " << toString(bits) << "\n";
215 }
216 }
217
218
219 template <class T>
220 void DefaultNotBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
221 Debug("bitvector-bb") << "theory::bv::DefaultNotBB bitblasting " << node << "\n";
222 Assert(node.getKind() == kind::BITVECTOR_NOT);
223 Assert(bits.size() == 0);
224 std::vector<T> bv;
225 bb->bbTerm(node[0], bv);
226 negateBits(bv, bits);
227 }
228
229 template <class T>
230 void DefaultConcatBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
231 Debug("bitvector-bb") << "theory::bv::DefaultConcatBB bitblasting " << node << "\n";
232 Assert(bits.size() == 0);
233
234 Assert (node.getKind() == kind::BITVECTOR_CONCAT);
235 for (int i = node.getNumChildren() -1 ; i >= 0; --i ) {
236 TNode current = node[i];
237 std::vector<T> current_bits;
238 bb->bbTerm(current, current_bits);
239
240 for(unsigned j = 0; j < utils::getSize(current); ++j) {
241 bits.push_back(current_bits[j]);
242 }
243 }
244 Assert (bits.size() == utils::getSize(node));
245 if(Debug.isOn("bitvector-bb")) {
246 Debug("bitvector-bb") << "with bits: " << toString(bits) << "\n";
247 }
248 }
249
250 template <class T>
251 void DefaultAndBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
252 Debug("bitvector-bb") << "theory::bv::DefaultAndBB bitblasting " << node << "\n";
253
254 Assert(node.getKind() == kind::BITVECTOR_AND &&
255 bits.size() == 0);
256
257 bb->bbTerm(node[0], bits);
258 std::vector<T> current;
259 for(unsigned j = 1; j < node.getNumChildren(); ++j) {
260 bb->bbTerm(node[j], current);
261 for (unsigned i = 0; i < utils::getSize(node); ++i) {
262 bits[i] = mkAnd(bits[i], current[i]);
263 }
264 current.clear();
265 }
266 Assert (bits.size() == utils::getSize(node));
267 }
268
269 template <class T>
270 void DefaultOrBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
271 Debug("bitvector-bb") << "theory::bv::DefaultOrBB bitblasting " << node << "\n";
272
273 Assert(node.getKind() == kind::BITVECTOR_OR &&
274 bits.size() == 0);
275
276 bb->bbTerm(node[0], bits);
277 std::vector<T> current;
278 for(unsigned j = 1; j < node.getNumChildren(); ++j) {
279 bb->bbTerm(node[j], current);
280 for (unsigned i = 0; i < utils::getSize(node); ++i) {
281 bits[i] = mkOr(bits[i], current[i]);
282 }
283 current.clear();
284 }
285 Assert (bits.size() == utils::getSize(node));
286 }
287
288 template <class T>
289 void DefaultXorBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
290 Debug("bitvector-bb") << "theory::bv::DefaultXorBB bitblasting " << node << "\n";
291
292 Assert(node.getKind() == kind::BITVECTOR_XOR &&
293 bits.size() == 0);
294
295 bb->bbTerm(node[0], bits);
296 std::vector<T> current;
297 for(unsigned j = 1; j < node.getNumChildren(); ++j) {
298 bb->bbTerm(node[j], current);
299 for (unsigned i = 0; i < utils::getSize(node); ++i) {
300 bits[i] = mkXor(bits[i], current[i]);
301 }
302 current.clear();
303 }
304 Assert (bits.size() == utils::getSize(node));
305 }
306
307 template <class T>
308 void DefaultXnorBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
309 Debug("bitvector-bb") << "theory::bv::DefaultXnorBB bitblasting " << node << "\n";
310
311 Assert(node.getNumChildren() == 2 &&
312 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 void DefaultCompBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
339 Debug("bitvector") << "theory::bv:: DefaultCompBB bitblasting "<< node << "\n";
340
341 Assert(utils::getSize(node) == 1 && bits.size() == 0 && node.getKind() == kind::BITVECTOR_COMP);
342 std::vector<T> a, b;
343 bb->bbTerm(node[0], a);
344 bb->bbTerm(node[1], b);
345
346 std::vector<T> bit_eqs;
347 for (unsigned i = 0; i < a.size(); ++i) {
348 T eq = mkIff(a[i], b[i]);
349 bit_eqs.push_back(eq);
350 }
351 T a_eq_b = mkAnd(bit_eqs);
352 bits.push_back(a_eq_b);
353 }
354
355 template <class T>
356 void DefaultMultBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
357 Debug("bitvector") << "theory::bv:: DefaultMultBB bitblasting "<< node << "\n";
358 Assert(res.size() == 0 &&
359 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 std::vector<T> newres;
382 bb->bbTerm(node[0], res);
383 for(unsigned i = 1; i < node.getNumChildren(); ++i) {
384 std::vector<T> current;
385 bb->bbTerm(node[i], current);
386 newres.clear();
387 // constructs a simple shift and add multiplier building the result
388 // in res
389 shiftAddMultiplier(res, current, newres);
390 res = newres;
391 }
392 if(Debug.isOn("bitvector-bb")) {
393 Debug("bitvector-bb") << "with bits: " << toString(res) << "\n";
394 }
395 }
396
397 template <class T>
398 void DefaultPlusBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
399 Debug("bitvector-bb") << "theory::bv::DefaultPlusBB bitblasting " << node << "\n";
400 Assert(node.getKind() == kind::BITVECTOR_PLUS &&
401 res.size() == 0);
402
403 bb->bbTerm(node[0], res);
404
405 std::vector<T> newres;
406
407 for(unsigned i = 1; i < node.getNumChildren(); ++i) {
408 std::vector<T> current;
409 bb->bbTerm(node[i], current);
410 newres.clear();
411 rippleCarryAdder(res, current, newres, mkFalse<T>());
412 res = newres;
413 }
414
415 Assert(res.size() == utils::getSize(node));
416 }
417
418
419 template <class T>
420 void DefaultSubBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
421 Debug("bitvector-bb") << "theory::bv::DefaultSubBB bitblasting " << node << "\n";
422 Assert(node.getKind() == kind::BITVECTOR_SUB &&
423 node.getNumChildren() == 2 &&
424 bits.size() == 0);
425
426 std::vector<T> a, b;
427 bb->bbTerm(node[0], a);
428 bb->bbTerm(node[1], b);
429 Assert(a.size() == b.size() && utils::getSize(node) == a.size());
430
431 // bvsub a b = adder(a, ~b, 1)
432 std::vector<T> not_b;
433 negateBits(b, not_b);
434 rippleCarryAdder(a, not_b, bits, mkTrue<T>());
435 }
436
437 template <class T>
438 void DefaultNegBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
439 Debug("bitvector-bb") << "theory::bv::DefaultNegBB bitblasting " << node << "\n";
440 Assert(node.getKind() == kind::BITVECTOR_NEG);
441
442 std::vector<T> a;
443 bb->bbTerm(node[0], a);
444 Assert(utils::getSize(node) == a.size());
445
446 // -a = add(~a, 0, 1).
447 std::vector<T> not_a;
448 negateBits(a, not_a);
449 std::vector<T> zero;
450 makeZero(zero, utils::getSize(node));
451
452 rippleCarryAdder(not_a, zero, bits, mkTrue<T>());
453 }
454
455 template <class T>
456 void uDivModRec(const std::vector<T>& a, const std::vector<T>& b, std::vector<T>& q, std::vector<T>& r, unsigned rec_width) {
457 Assert( q.size() == 0 && r.size() == 0);
458
459 if(rec_width == 0 || isZero(a)) {
460 makeZero(q, a.size());
461 makeZero(r, a.size());
462 return;
463 }
464
465 std::vector<T> q1, r1;
466 std::vector<T> a1 = a;
467 rshift(a1, 1);
468
469 uDivModRec(a1, b, q1, r1, rec_width - 1);
470 // shift the quotient and remainder (i.e. multiply by two) and add 1 to remainder if a is odd
471 lshift(q1, 1);
472 lshift(r1, 1);
473
474
475 T is_odd = mkIff(a[0], mkTrue<T>());
476 T one_if_odd = mkIte(is_odd, mkTrue<T>(), mkFalse<T>());
477
478 std::vector<T> zero;
479 makeZero(zero, b.size());
480
481 std::vector<T> r1_shift_add;
482 // account for a being odd
483 rippleCarryAdder(r1, zero, r1_shift_add, one_if_odd);
484 // now check if the remainder is greater than b
485 std::vector<T> not_b;
486 negateBits(b, not_b);
487 std::vector<T> r_minus_b;
488 T co1;
489 // use adder because we need r_minus_b anyway
490 co1 = rippleCarryAdder(r1_shift_add, not_b, r_minus_b, mkTrue<T>());
491 // sign is true if r1 < b
492 T sign = mkNot(co1);
493
494 q1[0] = mkIte(sign, q1[0], mkTrue<T>());
495
496 // would be nice to have a high level ITE instead of bitwise
497 for(unsigned i = 0; i < a.size(); ++i) {
498 r1_shift_add[i] = mkIte(sign, r1_shift_add[i], r_minus_b[i]);
499 }
500
501 // check if a < b
502
503 std::vector<T> a_minus_b;
504 T co2 = rippleCarryAdder(a, not_b, a_minus_b, mkTrue<T>());
505 // Node a_lt_b = a_minus_b.back();
506 T a_lt_b = mkNot(co2);
507
508 for(unsigned i = 0; i < a.size(); ++i) {
509 T qval = mkIte(a_lt_b, mkFalse<T>(), q1[i]);
510 T rval = mkIte(a_lt_b, a[i], r1_shift_add[i]);
511 q.push_back(qval);
512 r.push_back(rval);
513 }
514
515 }
516
517 template <class T>
518 void DefaultUdivBB (TNode node, std::vector<T>& q, TBitblaster<T>* bb) {
519 Debug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node << "\n";
520 Assert(node.getKind() == kind::BITVECTOR_UDIV_TOTAL && q.size() == 0);
521
522 std::vector<T> a, b;
523 bb->bbTerm(node[0], a);
524 bb->bbTerm(node[1], b);
525
526 std::vector<T> r;
527 uDivModRec(a, b, q, r, utils::getSize(node));
528 // adding a special case for division by 0
529 std::vector<T> iszero;
530 for (unsigned i = 0; i < b.size(); ++i) {
531 iszero.push_back(mkIff(b[i], mkFalse<T>()));
532 }
533 T b_is_0 = mkAnd(iszero);
534
535 for (unsigned i = 0; i < q.size(); ++i) {
536 q[i] = mkIte(b_is_0, mkTrue<T>(), q[i]); // a udiv 0 is 11..11
537 r[i] = mkIte(b_is_0, a[i], r[i]); // a urem 0 is a
538 }
539
540 // cache the remainder in case we need it later
541 Node remainder = utils::mkNode(kind::BITVECTOR_UREM_TOTAL, node[0], node[1]);
542 bb->storeBBTerm(remainder, r);
543 }
544
545 template <class T>
546 void DefaultUremBB (TNode node, std::vector<T>& rem, TBitblaster<T>* bb) {
547 Debug("bitvector-bb") << "theory::bv::DefaultUremBB bitblasting " << node << "\n";
548 Assert(node.getKind() == kind::BITVECTOR_UREM_TOTAL && rem.size() == 0);
549
550 std::vector<T> a, b;
551 bb->bbTerm(node[0], a);
552 bb->bbTerm(node[1], b);
553
554 std::vector<T> q;
555 uDivModRec(a, b, q, rem, utils::getSize(node));
556 // adding a special case for division by 0
557 std::vector<T> iszero;
558 for (unsigned i = 0; i < b.size(); ++i) {
559 iszero.push_back(mkIff(b[i], mkFalse<T>()));
560 }
561 T b_is_0 = mkAnd(iszero);
562
563 for (unsigned i = 0; i < q.size(); ++i) {
564 q[i] = mkIte(b_is_0, mkTrue<T>(), q[i]); // a udiv 0 is 11..11
565 rem[i] = mkIte(b_is_0, a[i], rem[i]); // a urem 0 is a
566 }
567
568 // cache the quotient in case we need it later
569 Node quotient = utils::mkNode(kind::BITVECTOR_UDIV_TOTAL, node[0], node[1]);
570 bb->storeBBTerm(quotient, q);
571 }
572
573
574 template <class T>
575 void DefaultSdivBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
576 Debug("bitvector") << "theory::bv:: Unimplemented kind "
577 << node.getKind() << "\n";
578 Unimplemented();
579 }
580 template <class T>
581 void DefaultSremBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
582 Debug("bitvector") << "theory::bv:: Unimplemented kind "
583 << node.getKind() << "\n";
584 Unimplemented();
585 }
586 template <class T>
587 void DefaultSmodBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
588 Debug("bitvector") << "theory::bv:: Unimplemented kind "
589 << node.getKind() << "\n";
590 Unimplemented();
591 }
592
593 template <class T>
594 void DefaultShlBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
595 Debug("bitvector-bb") << "theory::bv::DefaultShlBB bitblasting " << node << "\n";
596 Assert (node.getKind() == kind::BITVECTOR_SHL &&
597 res.size() == 0);
598 std::vector<T> a, b;
599 bb->bbTerm(node[0], a);
600 bb->bbTerm(node[1], b);
601
602 // check for b < log2(n)
603 unsigned size = utils::getSize(node);
604 unsigned log2_size = std::ceil(log2((double)size));
605 Node a_size = utils::mkConst(BitVector(size, size));
606 Node b_ult_a_size_node = utils::mkNode(kind::BITVECTOR_ULT, node[1], a_size);
607 // ensure that the inequality is bit-blasted
608 bb->bbAtom(b_ult_a_size_node);
609 T b_ult_a_size = bb->getBBAtom(b_ult_a_size_node);
610 std::vector<T> prev_res;
611 res = a;
612 // we only need to look at the bits bellow log2_a_size
613 for(unsigned s = 0; s < log2_size; ++s) {
614 // barrel shift stage: at each stage you can either shift by 2^s bits
615 // or leave the previous stage untouched
616 prev_res = res;
617 unsigned threshold = pow(2, s);
618 for(unsigned i = 0; i < a.size(); ++i) {
619 if (i < threshold) {
620 // if b[s] is true then we must have shifted by at least 2^b bits so
621 // all bits bellow 2^s will be 0, otherwise just use previous shift value
622 res[i] = mkIte(b[s], mkFalse<T>(), prev_res[i]);
623 } else {
624 // if b[s]= 0, use previous value, otherwise shift by threshold bits
625 Assert(i >= threshold);
626 res[i] = mkIte(b[s], prev_res[i-threshold], prev_res[i]);
627 }
628 }
629 }
630 prev_res = res;
631 for (unsigned i = 0; i < b.size(); ++i) {
632 // this is fine because b_ult_a_size has been bit-blasted
633 res[i] = mkIte(b_ult_a_size, prev_res[i], mkFalse<T>());
634 }
635
636 if(Debug.isOn("bitvector-bb")) {
637 Debug("bitvector-bb") << "with bits: " << toString(res) << "\n";
638 }
639 }
640
641 template <class T>
642 void DefaultLshrBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
643 Debug("bitvector-bb") << "theory::bv::DefaultLshrBB bitblasting " << node << "\n";
644 Assert (node.getKind() == kind::BITVECTOR_LSHR &&
645 res.size() == 0);
646 std::vector<T> a, b;
647 bb->bbTerm(node[0], a);
648 bb->bbTerm(node[1], b);
649
650 // check for b < log2(n)
651 unsigned size = utils::getSize(node);
652 unsigned log2_size = std::ceil(log2((double)size));
653 Node a_size = utils::mkConst(BitVector(size, size));
654 Node b_ult_a_size_node = utils::mkNode(kind::BITVECTOR_ULT, node[1], a_size);
655 // ensure that the inequality is bit-blasted
656 bb->bbAtom(b_ult_a_size_node);
657 T b_ult_a_size = bb->getBBAtom(b_ult_a_size_node);
658 res = a;
659 std::vector<T> prev_res;
660
661 for(unsigned s = 0; s < log2_size; ++s) {
662 // barrel shift stage: at each stage you can either shift by 2^s bits
663 // or leave the previous stage untouched
664 prev_res = res;
665 int threshold = pow(2, s);
666 for(unsigned i = 0; i < a.size(); ++i) {
667 if (i + threshold >= a.size()) {
668 // if b[s] is true then we must have shifted by at least 2^b bits so
669 // all bits above 2^s will be 0, otherwise just use previous shift value
670 res[i] = mkIte(b[s], mkFalse<T>(), prev_res[i]);
671 } else {
672 // if b[s]= 0, use previous value, otherwise shift by threshold bits
673 Assert (i+ threshold < a.size());
674 res[i] = mkIte(mkNot(b[s]), prev_res[i], prev_res[i+threshold]);
675 }
676 }
677 }
678
679 prev_res = res;
680 for (unsigned i = 0; i < b.size(); ++i) {
681 // this is fine because b_ult_a_size has been bit-blasted
682 res[i] = mkIte(b_ult_a_size, prev_res[i], mkFalse<T>());
683 }
684
685 if(Debug.isOn("bitvector-bb")) {
686 Debug("bitvector-bb") << "with bits: " << toString(res) << "\n";
687 }
688 }
689
690 template <class T>
691 void DefaultAshrBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
692
693 Debug("bitvector-bb") << "theory::bv::DefaultAshrBB bitblasting " << node << "\n";
694 Assert (node.getKind() == kind::BITVECTOR_ASHR &&
695 res.size() == 0);
696 std::vector<T> a, b;
697 bb->bbTerm(node[0], a);
698 bb->bbTerm(node[1], b);
699
700 // check for b < n
701 unsigned size = utils::getSize(node);
702 unsigned log2_size = std::ceil(log2((double)size));
703 Node a_size = utils::mkConst(BitVector(size, size));
704 Node b_ult_a_size_node = utils::mkNode(kind::BITVECTOR_ULT, node[1], a_size);
705 // ensure that the inequality is bit-blasted
706 bb->bbAtom(b_ult_a_size_node);
707 T b_ult_a_size = bb->getBBAtom(b_ult_a_size_node);
708
709 res = a;
710 T sign_bit = a.back();
711 std::vector<T> prev_res;
712
713 for(unsigned s = 0; s < log2_size; ++s) {
714 // barrel shift stage: at each stage you can either shift by 2^s bits
715 // or leave the previous stage untouched
716 prev_res = res;
717 int threshold = pow(2, s);
718 for(unsigned i = 0; i < a.size(); ++i) {
719 if (i + threshold >= a.size()) {
720 // if b[s] is true then we must have shifted by at least 2^b bits so
721 // all bits above 2^s will be the sign bit, otherwise just use previous shift value
722 res[i] = mkIte(b[s], sign_bit, prev_res[i]);
723 } else {
724 // if b[s]= 0, use previous value, otherwise shift by threshold bits
725 Assert (i+ threshold < a.size());
726 res[i] = mkIte(mkNot(b[s]), prev_res[i], prev_res[i+threshold]);
727 }
728 }
729 }
730
731 prev_res = res;
732 for (unsigned i = 0; i < b.size(); ++i) {
733 // this is fine because b_ult_a_size has been bit-blasted
734 res[i] = mkIte(b_ult_a_size, prev_res[i], sign_bit);
735 }
736
737 if(Debug.isOn("bitvector-bb")) {
738 Debug("bitvector-bb") << "with bits: " << toString(res) << "\n";
739 }
740 }
741
742 template <class T>
743 void DefaultExtractBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
744 Assert (node.getKind() == kind::BITVECTOR_EXTRACT);
745 Assert(bits.size() == 0);
746
747 std::vector<T> base_bits;
748 bb->bbTerm(node[0], base_bits);
749 unsigned high = utils::getExtractHigh(node);
750 unsigned low = utils::getExtractLow(node);
751
752 for (unsigned i = low; i <= high; ++i) {
753 bits.push_back(base_bits[i]);
754 }
755 Assert (bits.size() == high - low + 1);
756
757 if(Debug.isOn("bitvector-bb")) {
758 Debug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n";
759 Debug("bitvector-bb") << " with bits " << toString(bits);
760 }
761 }
762
763
764 template <class T>
765 void DefaultRepeatBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
766 Debug("bitvector") << "theory::bv:: Unimplemented kind "
767 << node.getKind() << "\n";
768 // this should be rewritten
769 Unimplemented();
770 }
771
772 template <class T>
773 void DefaultZeroExtendBB (TNode node, std::vector<T>& res_bits, TBitblaster<T>* bb) {
774
775 Debug("bitvector-bb") << "theory::bv::DefaultZeroExtendBB bitblasting " << node << "\n";
776
777 // this should be rewritten
778 Unimplemented();
779
780 }
781
782 template <class T>
783 void DefaultSignExtendBB (TNode node, std::vector<T>& res_bits, TBitblaster<T>* bb) {
784 Debug("bitvector-bb") << "theory::bv::DefaultSignExtendBB bitblasting " << node << "\n";
785
786 Assert (node.getKind() == kind::BITVECTOR_SIGN_EXTEND &&
787 res_bits.size() == 0);
788
789 std::vector<T> bits;
790 bb->bbTerm(node[0], bits);
791
792 T sign_bit = bits.back();
793 unsigned amount = node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
794
795 for (unsigned i = 0; i < bits.size(); ++i ) {
796 res_bits.push_back(bits[i]);
797 }
798
799 for (unsigned i = 0 ; i < amount ; ++i ) {
800 res_bits.push_back(sign_bit);
801 }
802
803 Assert (res_bits.size() == amount + bits.size());
804 }
805
806 template <class T>
807 void DefaultRotateRightBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
808 Debug("bitvector") << "theory::bv:: Unimplemented kind "
809 << node.getKind() << "\n";
810
811 Unimplemented();
812 }
813
814 template <class T>
815 void DefaultRotateLeftBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
816 Debug("bitvector") << "theory::bv:: Unimplemented kind "
817 << node.getKind() << "\n";
818 Unimplemented();
819 }
820
821
822 }
823 }
824 }
825
826 #endif