1 /********************* */
2 /*! \file bitblast_strategies_template.h
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
12 ** \brief Implementation of bitblasting functions for various operators.
14 ** Implementation of bitblasting functions for various operators.
17 #ifndef __CVC4__BITBLAST__STRATEGIES_TEMPLATE_H
18 #define __CVC4__BITBLAST__STRATEGIES_TEMPLATE_H
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"
32 * Default Atom Bitblasting strategies:
34 * @param node the atom to be bitblasted
35 * @param bb the bitblaster
39 T
UndefinedAtomBBStrategy(TNode node
, TBitblaster
<T
>* bb
) {
40 Debug("bitvector") << "TheoryBV::Bitblaster Undefined bitblasting strategy for kind: "
41 << node
.getKind() << "\n";
47 T
DefaultEqBB(TNode node
, TBitblaster
<T
>* bb
) {
48 Debug("bitvector-bb") << "Bitblasting node " << node
<< "\n";
50 Assert(node
.getKind() == kind::EQUAL
);
51 std::vector
<T
> lhs
, rhs
;
52 bb
->bbTerm(node
[0], lhs
);
53 bb
->bbTerm(node
[1], rhs
);
55 Assert(lhs
.size() == rhs
.size());
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
);
62 T bv_eq
= mkAnd(bits_eq
);
67 T
AdderUltBB(TNode node
, TBitblaster
<T
>* bb
) {
68 Debug("bitvector-bb") << "Bitblasting node " << node
<< "\n";
69 Assert(node
.getKind() == kind::BITVECTOR_ULT
);
71 bb
->bbTerm(node
[0], a
);
72 bb
->bbTerm(node
[1], b
);
73 Assert(a
.size() == b
.size());
75 // a < b <=> ~ (add(a, ~b, 1).carry_out)
78 T carry
= mkTrue
<T
>();
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
]),
90 T
DefaultUltBB(TNode node
, TBitblaster
<T
>* bb
) {
91 Debug("bitvector-bb") << "Bitblasting node " << node
<< "\n";
92 Assert(node
.getKind() == kind::BITVECTOR_ULT
);
94 bb
->bbTerm(node
[0], a
);
95 bb
->bbTerm(node
[1], b
);
96 Assert(a
.size() == b
.size());
98 // construct bitwise comparison
99 T res
= uLessThanBB(a
, b
, false);
104 T
DefaultUleBB(TNode node
, TBitblaster
<T
>* bb
){
105 Debug("bitvector-bb") << "Bitblasting node " << node
<< "\n";
106 Assert(node
.getKind() == kind::BITVECTOR_ULE
);
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);
118 T
DefaultUgtBB(TNode node
, TBitblaster
<T
>* bb
){
119 Debug("bitvector-bb") << "Bitblasting node " << node
<< "\n";
120 // should be rewritten
124 T
DefaultUgeBB(TNode node
, TBitblaster
<T
>* bb
){
125 Debug("bitvector-bb") << "Bitblasting node " << node
<< "\n";
126 // should be rewritten
131 T
DefaultSltBB(TNode node
, TBitblaster
<T
>* bb
){
132 Debug("bitvector-bb") << "Bitblasting node " << node
<< "\n";
135 bb
->bbTerm(node
[0], a
);
136 bb
->bbTerm(node
[1], b
);
137 Assert(a
.size() == b
.size());
139 T res
= sLessThanBB(a
, b
, false);
144 T
DefaultSleBB(TNode node
, TBitblaster
<T
>* bb
){
145 Debug("bitvector-bb") << "Bitblasting node " << node
<< "\n";
148 bb
->bbTerm(node
[0], a
);
149 bb
->bbTerm(node
[1], b
);
150 Assert(a
.size() == b
.size());
152 T res
= sLessThanBB(a
, b
, true);
157 T
DefaultSgtBB(TNode node
, TBitblaster
<T
>* bb
){
158 Debug("bitvector-bb") << "Bitblasting node " << node
<< "\n";
159 // should be rewritten
164 T
DefaultSgeBB(TNode node
, TBitblaster
<T
>* bb
){
165 Debug("bitvector-bb") << "Bitblasting node " << node
<< "\n";
166 // should be rewritten
171 /// Term bitblasting strategies
174 * Default Term Bitblasting strategies
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
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";
188 void DefaultVarBB (TNode node
, std::vector
<T
>& bits
, TBitblaster
<T
>* bb
) {
189 Assert(bits
.size() == 0);
190 bb
->makeVariable(node
, bits
);
192 if(Debug
.isOn("bitvector-bb")) {
193 Debug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting " << node
<< "\n";
194 Debug("bitvector-bb") << " with bits " << toString(bits
);
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);
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
>());
209 Assert (bit
== Integer(1));
210 bits
.push_back(mkTrue
<T
>());
213 if(Debug
.isOn("bitvector-bb")) {
214 Debug("bitvector-bb") << "with bits: " << toString(bits
) << "\n";
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);
225 bb
->bbTerm(node
[0], bv
);
226 negateBits(bv
, bits
);
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);
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
);
240 for(unsigned j
= 0; j
< utils::getSize(current
); ++j
) {
241 bits
.push_back(current_bits
[j
]);
244 Assert (bits
.size() == utils::getSize(node
));
245 if(Debug
.isOn("bitvector-bb")) {
246 Debug("bitvector-bb") << "with bits: " << toString(bits
) << "\n";
251 void DefaultAndBB (TNode node
, std::vector
<T
>& bits
, TBitblaster
<T
>* bb
) {
252 Debug("bitvector-bb") << "theory::bv::DefaultAndBB bitblasting " << node
<< "\n";
254 Assert(node
.getKind() == kind::BITVECTOR_AND
&&
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
]);
266 Assert (bits
.size() == utils::getSize(node
));
270 void DefaultOrBB (TNode node
, std::vector
<T
>& bits
, TBitblaster
<T
>* bb
) {
271 Debug("bitvector-bb") << "theory::bv::DefaultOrBB bitblasting " << node
<< "\n";
273 Assert(node
.getKind() == kind::BITVECTOR_OR
&&
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
]);
285 Assert (bits
.size() == utils::getSize(node
));
289 void DefaultXorBB (TNode node
, std::vector
<T
>& bits
, TBitblaster
<T
>* bb
) {
290 Debug("bitvector-bb") << "theory::bv::DefaultXorBB bitblasting " << node
<< "\n";
292 Assert(node
.getKind() == kind::BITVECTOR_XOR
&&
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
]);
304 Assert (bits
.size() == utils::getSize(node
));
308 void DefaultXnorBB (TNode node
, std::vector
<T
>& bits
, TBitblaster
<T
>* bb
) {
309 Debug("bitvector-bb") << "theory::bv::DefaultXnorBB bitblasting " << node
<< "\n";
311 Assert(node
.getNumChildren() == 2 &&
312 node
.getKind() == kind::BITVECTOR_XNOR
&&
314 std::vector
<T
> lhs
, rhs
;
315 bb
->bbTerm(node
[0], lhs
);
316 bb
->bbTerm(node
[1], rhs
);
317 Assert(lhs
.size() == rhs
.size());
319 for (unsigned i
= 0; i
< lhs
.size(); ++i
) {
320 bits
.push_back(mkIff(lhs
[i
], rhs
[i
]));
326 void DefaultNandBB (TNode node
, std::vector
<T
>& bits
, TBitblaster
<T
>* bb
) {
327 Debug("bitvector") << "theory::bv:: Unimplemented kind "
328 << node
.getKind() << "\n";
332 void DefaultNorBB (TNode node
, std::vector
<T
>& bits
, TBitblaster
<T
>* bb
) {
333 Debug("bitvector") << "theory::bv:: Unimplemented kind "
334 << node
.getKind() << "\n";
338 void DefaultCompBB (TNode node
, std::vector
<T
>& bits
, TBitblaster
<T
>* bb
) {
339 Debug("bitvector") << "theory::bv:: DefaultCompBB bitblasting "<< node
<< "\n";
341 Assert(utils::getSize(node
) == 1 && bits
.size() == 0 && node
.getKind() == kind::BITVECTOR_COMP
);
343 bb
->bbTerm(node
[0], a
);
344 bb
->bbTerm(node
[1], b
);
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
);
351 T a_eq_b
= mkAnd(bit_eqs
);
352 bits
.push_back(a_eq_b
);
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
);
361 // if (node.getNumChildren() == 2) {
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;
374 // if (no_overflow) {
375 // shiftAddMultiplier();
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
);
387 // constructs a simple shift and add multiplier building the result
389 shiftAddMultiplier(res
, current
, newres
);
392 if(Debug
.isOn("bitvector-bb")) {
393 Debug("bitvector-bb") << "with bits: " << toString(res
) << "\n";
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
&&
403 bb
->bbTerm(node
[0], res
);
405 std::vector
<T
> newres
;
407 for(unsigned i
= 1; i
< node
.getNumChildren(); ++i
) {
408 std::vector
<T
> current
;
409 bb
->bbTerm(node
[i
], current
);
411 rippleCarryAdder(res
, current
, newres
, mkFalse
<T
>());
415 Assert(res
.size() == utils::getSize(node
));
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 &&
427 bb
->bbTerm(node
[0], a
);
428 bb
->bbTerm(node
[1], b
);
429 Assert(a
.size() == b
.size() && utils::getSize(node
) == a
.size());
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
>());
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
);
443 bb
->bbTerm(node
[0], a
);
444 Assert(utils::getSize(node
) == a
.size());
446 // -a = add(~a, 0, 1).
447 std::vector
<T
> not_a
;
448 negateBits(a
, not_a
);
450 makeZero(zero
, utils::getSize(node
));
452 rippleCarryAdder(not_a
, zero
, bits
, mkTrue
<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);
459 if(rec_width
== 0 || isZero(a
)) {
460 makeZero(q
, a
.size());
461 makeZero(r
, a
.size());
465 std::vector
<T
> q1
, r1
;
466 std::vector
<T
> a1
= a
;
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
475 T is_odd
= mkIff(a
[0], mkTrue
<T
>());
476 T one_if_odd
= mkIte(is_odd
, mkTrue
<T
>(), mkFalse
<T
>());
479 makeZero(zero
, b
.size());
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
;
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
494 q1
[0] = mkIte(sign
, q1
[0], mkTrue
<T
>());
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
]);
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
);
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
]);
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);
523 bb
->bbTerm(node
[0], a
);
524 bb
->bbTerm(node
[1], b
);
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
>()));
533 T b_is_0
= mkAnd(iszero
);
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
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
);
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);
551 bb
->bbTerm(node
[0], a
);
552 bb
->bbTerm(node
[1], b
);
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
>()));
561 T b_is_0
= mkAnd(iszero
);
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
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
);
575 void DefaultSdivBB (TNode node
, std::vector
<T
>& bits
, TBitblaster
<T
>* bb
) {
576 Debug("bitvector") << "theory::bv:: Unimplemented kind "
577 << node
.getKind() << "\n";
581 void DefaultSremBB (TNode node
, std::vector
<T
>& bits
, TBitblaster
<T
>* bb
) {
582 Debug("bitvector") << "theory::bv:: Unimplemented kind "
583 << node
.getKind() << "\n";
587 void DefaultSmodBB (TNode node
, std::vector
<T
>& bits
, TBitblaster
<T
>* bb
) {
588 Debug("bitvector") << "theory::bv:: Unimplemented kind "
589 << node
.getKind() << "\n";
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
&&
599 bb
->bbTerm(node
[0], a
);
600 bb
->bbTerm(node
[1], b
);
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
;
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
617 unsigned threshold
= pow(2, s
);
618 for(unsigned i
= 0; i
< a
.size(); ++i
) {
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
]);
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
]);
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
>());
636 if(Debug
.isOn("bitvector-bb")) {
637 Debug("bitvector-bb") << "with bits: " << toString(res
) << "\n";
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
&&
647 bb
->bbTerm(node
[0], a
);
648 bb
->bbTerm(node
[1], b
);
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
);
659 std::vector
<T
> prev_res
;
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
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
]);
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
]);
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
>());
685 if(Debug
.isOn("bitvector-bb")) {
686 Debug("bitvector-bb") << "with bits: " << toString(res
) << "\n";
691 void DefaultAshrBB (TNode node
, std::vector
<T
>& res
, TBitblaster
<T
>* bb
) {
693 Debug("bitvector-bb") << "theory::bv::DefaultAshrBB bitblasting " << node
<< "\n";
694 Assert (node
.getKind() == kind::BITVECTOR_ASHR
&&
697 bb
->bbTerm(node
[0], a
);
698 bb
->bbTerm(node
[1], b
);
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
);
710 T sign_bit
= a
.back();
711 std::vector
<T
> prev_res
;
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
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
]);
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
]);
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
);
737 if(Debug
.isOn("bitvector-bb")) {
738 Debug("bitvector-bb") << "with bits: " << toString(res
) << "\n";
743 void DefaultExtractBB (TNode node
, std::vector
<T
>& bits
, TBitblaster
<T
>* bb
) {
744 Assert (node
.getKind() == kind::BITVECTOR_EXTRACT
);
745 Assert(bits
.size() == 0);
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
);
752 for (unsigned i
= low
; i
<= high
; ++i
) {
753 bits
.push_back(base_bits
[i
]);
755 Assert (bits
.size() == high
- low
+ 1);
757 if(Debug
.isOn("bitvector-bb")) {
758 Debug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node
<< "\n";
759 Debug("bitvector-bb") << " with bits " << toString(bits
);
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
773 void DefaultZeroExtendBB (TNode node
, std::vector
<T
>& res_bits
, TBitblaster
<T
>* bb
) {
775 Debug("bitvector-bb") << "theory::bv::DefaultZeroExtendBB bitblasting " << node
<< "\n";
777 // this should be rewritten
783 void DefaultSignExtendBB (TNode node
, std::vector
<T
>& res_bits
, TBitblaster
<T
>* bb
) {
784 Debug("bitvector-bb") << "theory::bv::DefaultSignExtendBB bitblasting " << node
<< "\n";
786 Assert (node
.getKind() == kind::BITVECTOR_SIGN_EXTEND
&&
787 res_bits
.size() == 0);
790 bb
->bbTerm(node
[0], bits
);
792 T sign_bit
= bits
.back();
793 unsigned amount
= node
.getOperator().getConst
<BitVectorSignExtend
>().signExtendAmount
;
795 for (unsigned i
= 0; i
< bits
.size(); ++i
) {
796 res_bits
.push_back(bits
[i
]);
799 for (unsigned i
= 0 ; i
< amount
; ++i
) {
800 res_bits
.push_back(sign_bit
);
803 Assert (res_bits
.size() == amount
+ bits
.size());
807 void DefaultRotateRightBB (TNode node
, std::vector
<T
>& res
, TBitblaster
<T
>* bb
) {
808 Debug("bitvector") << "theory::bv:: Unimplemented kind "
809 << node
.getKind() << "\n";
815 void DefaultRotateLeftBB (TNode node
, std::vector
<T
>& bits
, TBitblaster
<T
>* bb
) {
816 Debug("bitvector") << "theory::bv:: Unimplemented kind "
817 << node
.getKind() << "\n";