CBMC: /home/runner/work/cbmc/cbmc/src/solvers/flattening/bv_utils.cpp Source File

CBMC
Loading...
Searching...
No Matches
bv_utils.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "bv_utils.h"
10
11#include <util/arith_tools.h>
12
13#include <list>
14#include <utility>
15
16 bvt bv_utilst::build_constant(const mp_integer &n, std::size_t width)
17{
18 std::string n_str=integer2binary(n, width);
19 CHECK_RETURN(n_str.size() == width);
20 bvt result;
21 result.resize(width);
22 for(std::size_t i=0; i<width; i++)
23 result[i]=const_literal(n_str[width-i-1]=='1');
24 return result;
25}
26
28{
30 const std::size_t width = bv.size();
31 std::string s(width, '0');
32 for(std::size_t i = 0; i < width; i++)
33 s[width - i - 1] = bv[i].is_true() ? '1' : '0';
34 return binary2integer(s, false);
35}
36
38{
39 PRECONDITION(!bv.empty());
40 bvt tmp;
41 tmp=bv;
42 tmp.erase(tmp.begin(), tmp.begin()+1);
43 return prop.land(is_zero(tmp), bv[0]);
44}
45
46 void bv_utilst::set_equal(const bvt &a, const bvt &b)
47{
48 PRECONDITION(a.size() == b.size());
49 for(std::size_t i=0; i<a.size(); i++)
50 prop.set_equal(a[i], b[i]);
51}
52
53 bvt bv_utilst::extract(const bvt &a, std::size_t first, std::size_t last)
54{
55 // preconditions
56 PRECONDITION(first < a.size());
57 PRECONDITION(last < a.size());
58 PRECONDITION(first <= last);
59
60 bvt result=a;
61 result.resize(last+1);
62 if(first!=0)
63 result.erase(result.begin(), result.begin()+first);
64
65 POSTCONDITION(result.size() == last - first + 1);
66 return result;
67}
68
69 bvt bv_utilst::extract_msb(const bvt &a, std::size_t n)
70{
71 // preconditions
72 PRECONDITION(n <= a.size());
73
74 bvt result=a;
75 result.erase(result.begin(), result.begin()+(result.size()-n));
76
77 POSTCONDITION(result.size() == n);
78 return result;
79}
80
81 bvt bv_utilst::extract_lsb(const bvt &a, std::size_t n)
82{
83 // preconditions
84 PRECONDITION(n <= a.size());
85
86 bvt result=a;
87 result.resize(n);
88 return result;
89}
90
92{
93 bvt result;
94
95 result.resize(a.size()+b.size());
96
97 for(std::size_t i=0; i<a.size(); i++)
98 result[i]=a[i];
99
100 for(std::size_t i=0; i<b.size(); i++)
101 result[i+a.size()]=b[i];
102
103 return result;
104}
105
108{
109 PRECONDITION(a.size() == b.size());
110
111 bvt result;
112
113 result.resize(a.size());
114 for(std::size_t i=0; i<result.size(); i++)
115 result[i]=prop.lselect(s, a[i], b[i]);
116
117 return result;
118}
119
121 const bvt &bv,
122 std::size_t new_size,
123 representationt rep)
124{
125 std::size_t old_size=bv.size();
127
128 bvt result=bv;
129 result.resize(new_size);
130
132 (rep==representationt::SIGNED && !bv.empty())?bv[old_size-1]:
133 const_literal(false);
134
135 for(std::size_t i=old_size; i<new_size; i++)
136 result[i]=extend_with;
137
138 return result;
139}
140
141
147// The optimal encoding is the default as it gives a reduction in space
148// and small performance gains
149 #define OPTIMAL_FULL_ADDER
150
152 const literalt a,
153 const literalt b,
154 const literalt carry_in,
155 literalt &carry_out)
156{
157 #ifdef OPTIMAL_FULL_ADDER
159 {
160 literalt x;
161 literalt y;
162 int constantProp = -1;
163
164 if(a.is_constant())
165 {
166 x = b;
167 y = carry_in;
168 constantProp = (a.is_true()) ? 1 : 0;
169 }
170 else if(b.is_constant())
171 {
172 x = a;
173 y = carry_in;
174 constantProp = (b.is_true()) ? 1 : 0;
175 }
176 else if(carry_in.is_constant())
177 {
178 x = a;
179 y = b;
180 constantProp = (carry_in.is_true()) ? 1 : 0;
181 }
182
184
185 // Rely on prop.l* to do further constant propagation
186 if(constantProp == 1)
187 {
188 // At least one input bit is 1
189 carry_out = prop.lor(x, y);
190 sum = prop.lequal(x, y);
191 }
192 else if(constantProp == 0)
193 {
194 // At least one input bit is 0
195 carry_out = prop.land(x, y);
196 sum = prop.lxor(x, y);
197 }
198 else
199 {
202
203 // Any two inputs 1 will set the carry_out to 1
204 prop.lcnf(!a, !b, carry_out);
207
208 // Any two inputs 0 will set the carry_out to 0
209 prop.lcnf(a, b, !carry_out);
212
213 // If both carry out and sum are 1 then all inputs are 1
214 prop.lcnf(a, !sum, !carry_out);
215 prop.lcnf(b, !sum, !carry_out);
217
218 // If both carry out and sum are 0 then all inputs are 0
219 prop.lcnf(!a, sum, carry_out);
220 prop.lcnf(!b, sum, carry_out);
222
223 // If all of the inputs are 1 or all are 0 it sets the sum
224 prop.lcnf(!a, !b, !carry_in, sum);
225 prop.lcnf(a, b, carry_in, !sum);
226 }
227
228 return sum;
229 }
230 else // NOLINT(readability/braces)
231 #endif // OPTIMAL_FULL_ADDER
232 {
233 // trivial encoding
235 return prop.lxor(prop.lxor(a, b), carry_in);
236 }
237}
238
239// Daniel's carry optimisation
240 #define COMPACT_CARRY
241
243{
244 #ifdef COMPACT_CARRY
246 {
247 // propagation possible?
248 const auto const_count =
249 a.is_constant() + b.is_constant() + c.is_constant();
250
251 // propagation is possible if two or three inputs are constant
252 if(const_count>=2)
253 return prop.lor(prop.lor(
254 prop.land(a, b),
255 prop.land(a, c)),
256 prop.land(b, c));
257
258 // it's also possible if two of a,b,c are the same
259 if(a==b)
260 return a;
261 else if(a==c)
262 return a;
263 else if(b==c)
264 return b;
265
266 // the below yields fewer clauses and variables,
267 // but doesn't propagate anything at all
268
269 bvt clause;
270
272
273 /*
274 carry_correct: LEMMA
275 ( a OR b OR NOT x) AND
276 ( a OR NOT b OR c OR NOT x) AND
277 ( a OR NOT b OR NOT c OR x) AND
278 (NOT a OR b OR c OR NOT x) AND
279 (NOT a OR b OR NOT c OR x) AND
280 (NOT a OR NOT b OR x)
281 IFF
282 (x=((a AND b) OR (a AND c) OR (b AND c)));
283 */
284
285 prop.lcnf(a, b, !x);
286 prop.lcnf(a, !b, c, !x);
287 prop.lcnf(a, !b, !c, x);
288 prop.lcnf(!a, b, c, !x);
289 prop.lcnf(!a, b, !c, x);
290 prop.lcnf(!a, !b, x);
291
292 return x;
293 }
294 else
295 #endif // COMPACT_CARRY
296 {
297 // trivial encoding
298 bvt tmp;
299
300 tmp.push_back(prop.land(a, b));
301 tmp.push_back(prop.land(a, c));
302 tmp.push_back(prop.land(b, c));
303
304 return prop.lor(tmp);
305 }
306}
307
308std::pair<bvt, literalt>
309 bv_utilst::adder(const bvt &op0, const bvt &op1, literalt carry_in)
310{
311 PRECONDITION(op0.size() == op1.size());
312
313 std::pair<bvt, literalt> result{bvt{}, carry_in};
314 result.first.reserve(op0.size());
315 literalt &carry_out = result.second;
316
317 for(std::size_t i = 0; i < op0.size(); i++)
318 {
319 result.first.push_back(full_adder(op0[i], op1[i], carry_out, carry_out));
320 }
321
322 return result;
323}
324
326 const bvt &op0,
327 const bvt &op1,
329{
330 PRECONDITION(op0.size() == op1.size());
331
333
334 for(std::size_t i=0; i<op0.size(); i++)
335 carry_out=carry(op0[i], op1[i], carry_out);
336
337 return carry_out;
338}
339
341 const bvt &op0,
342 const bvt &op1,
343 bool subtract,
344 representationt rep)
345{
346 return adder_no_overflow(op0, op1, subtract, rep);
347}
348
349 bvt bv_utilst::add_sub(const bvt &op0, const bvt &op1, bool subtract)
350{
351 PRECONDITION(op0.size() == op1.size());
352
354
355 bvt tmp_op1=subtract?inverted(op1):op1;
356
357 // we ignore the carry-out
358 return adder(op0, tmp_op1, carry_in).first;
359}
360
361 bvt bv_utilst::add_sub(const bvt &op0, const bvt &op1, literalt subtract)
362{
363 const bvt op1_sign_applied=
364 select(subtract, inverted(op1), op1);
365
366 // we ignore the carry-out
367 return adder(op0, op1_sign_applied, subtract).first;
368}
369
371 const bvt &op0,
372 const bvt &op1,
373 bool subtract,
374 representationt rep)
375{
376 PRECONDITION(op0.size() == op1.size());
379
380 literalt carry_in = const_literal(subtract);
381
382 bvt tmp_op1 = subtract ? inverted(op1) : op1;
383
384 auto add_sub_result = adder(op0, tmp_op1, carry_in);
386
387 bvt result;
388 result.reserve(add_sub_result.first.size());
390 {
391 // An unsigned overflow has occurred when carry_out is not equal to
392 // subtract: addition with a carry-out means an overflow beyond the maximum
393 // representable value, subtraction without a carry-out means an underflow
394 // below zero. For saturating arithmetic the former implies that all bits
395 // should be set to 1, in the latter case all bits should be set to zero.
396 for(const auto &literal : add_sub_result.first)
397 {
398 result.push_back(
399 subtract ? prop.land(literal, carry_out)
401 }
402 }
403 else
404 {
405 // A signed overflow beyond the maximum representable value occurs when
406 // adding two positive numbers and the wrap-around result being negative, or
407 // when subtracting a negative from a positive number (and, again, the
408 // result being negative).
410 !sign_bit(op0),
411 subtract ? sign_bit(op1) : !sign_bit(op1),
412 sign_bit(add_sub_result.first)});
413 // A signed underflow below the minimum representable value occurs when
414 // adding two negative numbers and arriving at a positive result, or
415 // subtracting a positive from a negative number (and, again, obtaining a
416 // positive wrap-around result).
418 sign_bit(op0),
419 subtract ? !sign_bit(op1) : sign_bit(op1),
420 !sign_bit(add_sub_result.first)});
421
422 // set all bits except for the sign bit
423 PRECONDITION(!add_sub_result.first.empty());
424 for(std::size_t i = 0; i < add_sub_result.first.size() - 1; ++i)
425 {
426 const auto &literal = add_sub_result.first[i];
427 result.push_back(prop.land(
429 }
430 // finally add the sign bit
431 result.push_back(prop.land(
434 }
435
436 return result;
437}
438
440 const bvt &op0, const bvt &op1, representationt rep)
441{
443 {
444 // An overflow occurs if the signs of the two operands are the same
445 // and the sign of the sum is the opposite.
446
449
450 bvt result=add(op0, op1);
451 return prop.land(sign_the_same, prop.lxor(sign_bit(result), old_sign));
452 }
453 else if(rep==representationt::UNSIGNED)
454 {
455 // overflow is simply carry-out
456 return carry_out(op0, op1, const_literal(false));
457 }
458 else
460}
461
463 const bvt &op0, const bvt &op1, representationt rep)
464{
466 {
467 // We special-case x-INT_MIN, which is >=0 if
468 // x is negative, always representable, and
469 // thus not an overflow.
472
473 return
477 }
478 else if(rep==representationt::UNSIGNED)
479 {
480 // overflow is simply _negated_ carry-out
481 return !carry_out(op0, inverted(op1), const_literal(true));
482 }
483 else
485}
486
488 const bvt &op0,
489 const bvt &op1,
490 bool subtract,
491 representationt rep)
492{
493 const bvt tmp_op = subtract ? inverted(op1) : op1;
494
496 {
497 // an overflow occurs if the signs of the two operands are the same
498 // and the sign of the sum is the opposite
499
502
503 // we ignore the carry-out
504 bvt sum = adder(op0, tmp_op, const_literal(subtract)).first;
505
508
509 return sum;
510 }
511 else
512 {
513 INVARIANT(
515 "representation has either value signed or unsigned");
516 auto result = adder(op0, tmp_op, const_literal(subtract));
517 prop.l_set_to(result.second, subtract);
518 return std::move(result.first);
519 }
520}
521
522 bvt bv_utilst::adder_no_overflow(const bvt &op0, const bvt &op1)
523{
524 return adder_no_overflow(op0, op1, false, representationt::UNSIGNED);
525}
526
527 bvt bv_utilst::shift(const bvt &op, const shiftt s, const bvt &dist)
528{
529 std::size_t d=1, width=op.size();
530 bvt result=op;
531
532 for(std::size_t stage=0; stage<dist.size(); stage++)
533 {
534 if(dist[stage]!=const_literal(false))
535 {
536 bvt tmp=shift(result, s, d);
537
538 for(std::size_t i=0; i<width; i++)
539 result[i]=prop.lselect(dist[stage], tmp[i], result[i]);
540 }
541
542 d=d<<1;
543 }
544
545 return result;
546}
547
548 bvt bv_utilst::shift(const bvt &src, const shiftt s, std::size_t dist)
549{
550 bvt result;
551 result.resize(src.size());
552
553 // 'dist' is user-controlled, and thus arbitary.
554 // We thus must guard against the case in which i+dist overflows.
555 // We do so by considering the case dist>=src.size().
556
557 for(std::size_t i=0; i<src.size(); i++)
558 {
559 literalt l;
560
561 switch(s)
562 {
564 // no underflow on i-dist because of condition dist<=i
565 l=(dist<=i?src[i-dist]:const_literal(false));
566 break;
567
569 // src.size()-i won't underflow as i<src.size()
570 // Then, if dist<src.size()-i, then i+dist<src.size()
571 l = dist < src.size() - i ? src[i + dist] : sign_bit(src);
572 break;
573
575 // src.size()-i won't underflow as i<src.size()
576 // Then, if dist<src.size()-i, then i+dist<src.size()
577 l=(dist<src.size()-i?src[i+dist]:const_literal(false));
578 break;
579
581 // prevent overflows by using dist%src.size()
582 l=src[(src.size()+i-(dist%src.size()))%src.size()];
583 break;
584
586 // prevent overflows by using dist%src.size()
587 l=src[(i+(dist%src.size()))%src.size()];
588 break;
589
590 default:
592 }
593
594 result[i]=l;
595 }
596
597 return result;
598}
599
601{
602 bvt result=inverted(bv);
604 incrementer(result, const_literal(true), carry_out);
605 return result;
606}
607
609{
611 return negate(bv);
612}
613
615{
616 // a overflow on unary- can only happen with the smallest
617 // representable number 100....0
618
620 should_be_zeros.pop_back();
621
622 return prop.land(sign_bit(bv), !prop.lor(should_be_zeros));
623}
624
626 bvt &bv,
628 literalt &carry_out)
629{
631
632 for(auto &literal : bv)
633 {
637 }
638}
639
641{
642 bvt result=bv;
645 return result;
646}
647
649{
650 bvt result=bv;
651 for(auto &literal : result)
652 literal = !literal;
653 return result;
654}
655
656 bvt bv_utilst::wallace_tree(const std::vector<bvt> &pps)
657{
658 PRECONDITION(!pps.empty());
659
660 if(pps.size()==1)
661 return pps.front();
662 else if(pps.size()==2)
663 return add(pps[0], pps[1]);
664 else
665 {
666 std::vector<bvt> new_pps;
667 std::size_t no_full_adders=pps.size()/3;
668
669 // add groups of three partial products using CSA
670 for(std::size_t i=0; i<no_full_adders; i++)
671 {
672 const bvt &a=pps[i*3+0],
673 &b=pps[i*3+1],
674 &c=pps[i*3+2];
675
676 INVARIANT(a.size() == b.size(), "groups should be of equal size");
677 INVARIANT(a.size() == c.size(), "groups should be of equal size");
678
679 bvt s, t(a.size(), const_literal(false));
680 s.reserve(a.size());
681
682 for(std::size_t bit=0; bit<a.size(); bit++)
683 {
685 s.push_back(full_adder(a[bit], b[bit], c[bit], carry_out));
686 if(bit + 1 < a.size())
687 t[bit + 1] = carry_out;
688 }
689
690 new_pps.push_back(std::move(s));
691 new_pps.push_back(std::move(t));
692 }
693
694 // pass onwards up to two remaining partial products
695 for(std::size_t i=no_full_adders*3; i<pps.size(); i++)
696 new_pps.push_back(pps[i]);
697
698 POSTCONDITION(new_pps.size() < pps.size());
699 return wallace_tree(new_pps);
700 }
701}
702
703 bvt bv_utilst::dadda_tree(const std::vector<bvt> &pps)
704{
705 PRECONDITION(!pps.empty());
706
707 using columnt = std::list<literalt>;
708 std::vector<columnt> columns(pps.front().size());
709 for(const auto &pp : pps)
710 {
711 PRECONDITION(pp.size() == pps.front().size());
712 for(std::size_t i = 0; i < pp.size(); ++i)
713 {
714 if(!pp[i].is_false())
715 columns[i].push_back(pp[i]);
716 }
717 }
718
719 std::list<std::size_t> dadda_sequence;
720 for(std::size_t d = 2; d < pps.front().size(); d = (d * 3) / 2)
721 dadda_sequence.push_front(d);
722
723 for(auto d : dadda_sequence)
724 {
725 for(auto col_it = columns.begin(); col_it != columns.end();) // no ++col_it
726 {
727 if(col_it->size() <= d)
728 ++col_it;
729 else if(col_it->size() == d + 1)
730 {
731 // Dadda prescribes a half adder here, but OPTIMAL_FULL_ADDER makes
732 // full_adder actually build a half adder when carry-in is false.
734 col_it->push_back(full_adder(
735 col_it->front(),
736 *std::next(col_it->begin()),
737 const_literal(false),
738 carry_out));
739 col_it->pop_front();
740 col_it->pop_front();
741 if(std::next(col_it) != columns.end())
742 std::next(col_it)->push_back(carry_out);
743 }
744 else
745 {
746 // We could also experiment with n:2 compressors (for n > 3, n=3 is the
747 // full adder as used below) that use circuits with lower gate count
748 // than just combining multiple full adders.
750 col_it->push_back(full_adder(
751 col_it->front(),
752 *std::next(col_it->begin()),
753 *std::next(std::next(col_it->begin())),
754 carry_out));
755 col_it->pop_front();
756 col_it->pop_front();
757 col_it->pop_front();
758 if(std::next(col_it) != columns.end())
759 std::next(col_it)->push_back(carry_out);
760 }
761 }
762 }
763
764 bvt a, b;
765 a.reserve(pps.front().size());
766 b.reserve(pps.front().size());
767
768 for(const auto &col : columns)
769 {
770 PRECONDITION(col.size() <= 2);
771 switch(col.size())
772 {
773 case 0:
774 a.push_back(const_literal(false));
775 b.push_back(const_literal(false));
776 break;
777 case 1:
778 a.push_back(col.front());
779 b.push_back(const_literal(false));
780 break;
781 case 2:
782 a.push_back(col.front());
783 b.push_back(col.back());
784 }
785 }
786
787 return add(a, b);
788}
789
790// Wallace tree multiplier. This is disabled, as runtimes have
791// been observed to go up by 5%-10%, and on some models even by 20%.
792// #define WALLACE_TREE
793// Dadda' reduction scheme. This yields a smaller formula size than Wallace
794// trees (and also the default addition scheme), but remains disabled as it
795// isn't consistently more performant either.
796// #define DADDA_TREE
797
798// The following examples demonstrate the performance differences (with a
799// time-out of 7200 seconds):
800//
801// #ifndef BITWIDTH
802// #define BITWIDTH 8
803// #endif
804//
805// int main()
806// {
807// __CPROVER_bitvector[BITWIDTH] a, b;
808// __CPROVER_assert(a * 3 == a + a + a, "multiplication by 3");
809// __CPROVER_assert(3 * a == a + a + a, "multiplication by 3");
810// __CPROVER_bitvector[BITWIDTH] ab = a * b;
811// __CPROVER_bitvector[BITWIDTH * 2] ab_check =
812// (__CPROVER_bitvector[BITWIDTH * 2])a *
813// (__CPROVER_bitvector[BITWIDTH * 2])b;
814// __CPROVER_assert(
815// ab == (__CPROVER_bitvector[BITWIDTH])ab_check, "should pass");
816// }
817//
818// |----|-----------------------------|-----------------------------|
819// | | CaDiCaL | MiniSat2 |
820// |----|-----------------------------|-----------------------------|
821// | n | No tree | Wallace | Dadda | No tree | Wallace | Dadda |
822// |----|---------|---------|---------|---------|---------|---------|
823// | 1 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 |
824// | 2 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 |
825// | 3 | 0.01 | 0.01 | 0.00 | 0.00 | 0.00 | 0.00 |
826// | 4 | 0.01 | 0.01 | 0.01 | 0.01 | 0.01 | 0.01 |
827// | 5 | 0.04 | 0.04 | 0.04 | 0.01 | 0.01 | 0.01 |
828// | 6 | 0.11 | 0.13 | 0.12 | 0.04 | 0.05 | 0.06 |
829// | 7 | 0.28 | 0.46 | 0.44 | 0.15 | 0.27 | 0.31 |
830// | 8 | 0.50 | 1.55 | 1.09 | 0.90 | 1.06 | 1.36 |
831// | 9 | 2.22 | 3.63 | 2.67 | 3.40 | 5.85 | 3.44 |
832// | 10 | 2.79 | 4.81 | 4.69 | 4.32 | 28.41 | 28.01 |
833// | 11 | 8.48 | 4.45 | 11.99 | 38.24 | 98.55 | 86.46 |
834// | 12 | 14.52 | 4.86 | 5.80 | 115.00 | 140.11 | 461.70 |
835// | 13 | 33.62 | 5.56 | 6.14 | 210.24 | 805.59 | 609.01 |
836// | 14 | 37.23 | 6.11 | 8.01 | 776.75 | 689.96 | 6153.82 |
837// | 15 | 108.65 | 7.86 | 14.72 | 1048.92 | 1421.74 | 6881.78 |
838// | 16 | 102.61 | 14.08 | 18.54 | 1628.01 | timeout | 1943.85 |
839// | 17 | 117.89 | 18.53 | 9.19 | 4148.73 | timeout | timeout |
840// | 18 | 209.40 | 7.97 | 7.74 | 2760.51 | timeout | timeout |
841// | 19 | 168.21 | 18.04 | 15.00 | 2514.21 | timeout | timeout |
842// | 20 | 566.76 | 12.68 | 22.47 | 2609.09 | timeout | timeout |
843// | 21 | 786.31 | 23.80 | 23.80 | 2232.77 | timeout | timeout |
844// | 22 | 817.74 | 17.64 | 22.53 | 3866.70 | timeout | timeout |
845// | 23 | 1102.76 | 24.19 | 26.37 | timeout | timeout | timeout |
846// | 24 | 1319.59 | 27.37 | 29.95 | timeout | timeout | timeout |
847// | 25 | 1786.11 | 27.10 | 29.94 | timeout | timeout | timeout |
848// | 26 | 1952.18 | 31.08 | 33.95 | timeout | timeout | timeout |
849// | 27 | 6908.48 | 27.92 | 34.94 | timeout | timeout | timeout |
850// | 28 | 6919.34 | 36.63 | 33.78 | timeout | timeout | timeout |
851// | 29 | timeout | 27.95 | 40.69 | timeout | timeout | timeout |
852// | 30 | timeout | 36.94 | 31.59 | timeout | timeout | timeout |
853// | 31 | timeout | 38.41 | 40.04 | timeout | timeout | timeout |
854// | 32 | timeout | 33.06 | 91.38 | timeout | timeout | timeout |
855// |----|---------|---------|---------|---------|---------|---------|
856//
857// In summary, both Wallace tree and Dadda reduction are substantially more
858// efficient with CaDiCaL on the above code for all bit width > 11, but somewhat
859// slower with MiniSat.
860//
861// #ifndef BITWIDTH
862// #define BITWIDTH 8
863// #endif
864//
865// int main()
866// {
867// __CPROVER_bitvector[BITWIDTH] a, b, c, ab, bc, abc;
868// ab = a * b;
869// __CPROVER_bitvector[BITWIDTH * 2] ab_check =
870// (__CPROVER_bitvector[BITWIDTH * 2])a *
871// (__CPROVER_bitvector[BITWIDTH * 2])b;
872// __CPROVER_assume(ab == ab_check);
873// bc = b * c;
874// __CPROVER_bitvector[BITWIDTH * 2] bc_check =
875// (__CPROVER_bitvector[BITWIDTH * 2])b *
876// (__CPROVER_bitvector[BITWIDTH * 2])c;
877// __CPROVER_assume(bc == bc_check);
878// abc = ab * c;
879// __CPROVER_bitvector[BITWIDTH * 2] abc_check =
880// (__CPROVER_bitvector[BITWIDTH * 2])ab *
881// (__CPROVER_bitvector[BITWIDTH * 2])c;
882// __CPROVER_assume(abc == abc_check);
883// __CPROVER_assert(abc == a * bc, "associativity");
884// }
885//
886// |----|-----------------------------|-----------------------------|
887// | | CaDiCaL | MiniSat2 |
888// |----|-----------------------------|-----------------------------|
889// | n | No tree | Wallace | Dadda | No tree | Wallace | Dadda |
890// |----|---------|---------|---------|---------|---------|---------|
891// | 1 | 0.00 | 0.00 | 0.00 | 0.01 | 0.01 | 0.01 |
892// | 2 | 0.01 | 0.01 | 0.01 | 0.01 | 0.01 | 0.01 |
893// | 3 | 0.02 | 0.03 | 0.03 | 0.01 | 0.01 | 0.01 |
894// | 4 | 0.05 | 0.07 | 0.06 | 0.02 | 0.02 | 0.02 |
895// | 5 | 0.17 | 0.18 | 0.14 | 0.04 | 0.04 | 0.04 |
896// | 6 | 0.50 | 0.63 | 0.63 | 0.13 | 0.14 | 0.13 |
897// | 7 | 1.01 | 1.15 | 0.90 | 0.43 | 0.47 | 0.47 |
898// | 8 | 1.56 | 1.76 | 1.75 | 3.35 | 2.39 | 1.75 |
899// | 9 | 2.07 | 2.48 | 1.75 | 11.20 | 12.64 | 7.94 |
900// | 10 | 3.58 | 3.88 | 3.54 | 20.23 | 23.49 | 15.66 |
901// | 11 | 5.84 | 7.46 | 5.31 | 49.32 | 39.86 | 44.15 |
902// | 12 | 11.71 | 16.85 | 13.40 | 69.32 | 156.57 | 46.50 |
903// | 13 | 33.22 | 41.95 | 34.43 | 250.91 | 294.73 | 79.47 |
904// | 14 | 76.27 | 109.59 | 84.49 | 226.98 | 259.84 | 258.08 |
905// | 15 | 220.01 | 330.10 | 267.11 | 783.73 | 1160.47 | 1262.91 |
906// | 16 | 591.91 | 981.16 | 808.33 | 2712.20 | 4286.60 | timeout |
907// | 17 | 1634.97 | 2574.81 | 2006.27 | timeout | timeout | timeout |
908// | 18 | 4680.16 | timeout | 6704.35 | timeout | timeout | timeout |
909// | 19 | timeout | timeout | timeout | timeout | timeout | timeout |
910// | 20 | timeout | timeout | timeout | timeout | timeout | timeout |
911// | 21 | timeout | timeout | timeout | timeout | timeout | timeout |
912// | 22 | timeout | timeout | timeout | timeout | timeout | timeout |
913// | 23 | timeout | timeout | timeout | timeout | timeout | timeout |
914// | 24 | timeout | timeout | timeout | timeout | timeout | timeout |
915// | 25 | timeout | timeout | timeout | timeout | timeout | timeout |
916// | 26 | timeout | timeout | timeout | timeout | timeout | timeout |
917// | 27 | timeout | timeout | timeout | timeout | timeout | timeout |
918// | 28 | timeout | timeout | timeout | timeout | timeout | timeout |
919// | 29 | timeout | timeout | timeout | timeout | timeout | timeout |
920// | 30 | timeout | timeout | timeout | timeout | timeout | timeout |
921// | 31 | timeout | timeout | timeout | timeout | timeout | timeout |
922// | 32 | timeout | timeout | timeout | timeout | timeout | timeout |
923// |----|---------|---------|---------|---------|---------|---------|
924//
925// In summary, Wallace tree reduction is slower for both solvers and all bit
926// widths (except BITWIDTH==8 with MiniSat2). Dadda multipliers get closer to
927// our multiplier that's not using a tree reduction scheme, but aren't uniformly
928// better either.
929
931{
932 bvt op0=_op0, op1=_op1;
933
934 if(is_constant(op1))
935 std::swap(op0, op1);
936
937 // build the usual quadratic number of partial products
938 std::vector<bvt> pps;
939 pps.reserve(op0.size());
940
941 for(std::size_t bit=0; bit<op0.size(); bit++)
942 {
943 if(op0[bit] == const_literal(false))
944 continue;
945
946 // zeros according to weight
947 bvt pp = zeros(bit);
948 pp.reserve(op0.size());
949
950 for(std::size_t idx = bit; idx < op0.size(); idx++)
951 pp.push_back(prop.land(op1[idx - bit], op0[bit]));
952
953 pps.push_back(pp);
954 }
955
956 if(pps.empty())
957 return zeros(op0.size());
958 else
959 {
960#ifdef WALLACE_TREE
961 return wallace_tree(pps);
962#elif defined(DADDA_TREE)
963 return dadda_tree(pps);
964#else
965 bvt product = pps.front();
966
967 for(auto it = std::next(pps.begin()); it != pps.end(); ++it)
968 product = add(product, *it);
969
970 return product;
971#endif
972 }
973}
974
976 const bvt &op0,
977 const bvt &op1)
978{
979 bvt _op0=op0, _op1=op1;
980
981 PRECONDITION(_op0.size() == _op1.size());
982
983 if(is_constant(_op1))
984 _op0.swap(_op1);
985
986 bvt product;
987 product.resize(_op0.size());
988
989 for(std::size_t i=0; i<product.size(); i++)
990 product[i]=const_literal(false);
991
992 for(std::size_t sum=0; sum<op0.size(); sum++)
993 if(op0[sum]!=const_literal(false))
994 {
995 bvt tmpop;
996
997 tmpop.reserve(product.size());
998
999 for(std::size_t idx=0; idx<sum; idx++)
1000 tmpop.push_back(const_literal(false));
1001
1002 for(std::size_t idx=sum; idx<product.size(); idx++)
1003 tmpop.push_back(prop.land(op1[idx-sum], op0[sum]));
1004
1006
1007 for(std::size_t idx=op1.size()-sum; idx<op1.size(); idx++)
1008 prop.l_set_to_false(prop.land(op1[idx], op0[sum]));
1009 }
1010
1011 return product;
1012}
1013
1014 bvt bv_utilst::signed_multiplier(const bvt &op0, const bvt &op1)
1015{
1016 if(op0.empty() || op1.empty())
1017 return bvt();
1018
1019 literalt sign0 = sign_bit(op0);
1020 literalt sign1 = sign_bit(op1);
1021
1022 bvt neg0=cond_negate(op0, sign0);
1023 bvt neg1=cond_negate(op1, sign1);
1024
1026
1028
1029 return cond_negate(result, result_sign);
1030}
1031
1033{
1034 bvt neg_bv=negate(bv);
1035
1036 bvt result;
1037 result.resize(bv.size());
1038
1039 for(std::size_t i=0; i<bv.size(); i++)
1040 result[i]=prop.lselect(cond, neg_bv[i], bv[i]);
1041
1042 return result;
1043}
1044
1046{
1047 PRECONDITION(!bv.empty());
1048 return cond_negate(bv, sign_bit(bv));
1049}
1050
1052{
1054
1055 return cond_negate(bv, cond);
1056}
1057
1059 const bvt &op0,
1060 const bvt &op1)
1061{
1062 if(op0.empty() || op1.empty())
1063 return bvt();
1064
1065 literalt sign0 = sign_bit(op0);
1066 literalt sign1 = sign_bit(op1);
1067
1070
1072
1073 prop.l_set_to_false(sign_bit(result));
1074
1076
1077 return cond_negate_no_overflow(result, result_sign);
1078}
1079
1081 const bvt &op0,
1082 const bvt &op1,
1083 representationt rep)
1084{
1085 // We determine the result size from the operand size, and the implementation
1086 // liberally swaps the operands, so we need to arrive at the same size
1087 // whatever the order of the operands.
1088 PRECONDITION(op0.size() == op1.size());
1089
1090 switch(rep)
1091 {
1092 case representationt::SIGNED: return signed_multiplier(op0, op1);
1093 case representationt::UNSIGNED: return unsigned_multiplier(op0, op1);
1094 }
1095
1097}
1098
1100 const bvt &op0,
1101 const bvt &op1,
1102 representationt rep)
1103{
1104 switch(rep)
1105 {
1107 return signed_multiplier_no_overflow(op0, op1);
1109 return unsigned_multiplier_no_overflow(op0, op1);
1110 }
1111
1113}
1114
1116 const bvt &op0,
1117 const bvt &op1,
1118 bvt &res,
1119 bvt &rem)
1120{
1121 if(op0.empty() || op1.empty())
1122 return;
1123
1124 bvt _op0(op0), _op1(op1);
1125
1128
1130
1131 for(std::size_t i=0; i<_op0.size(); i++)
1132 _op0[i]=(prop.lselect(sign_0, neg_0[i], _op0[i]));
1133
1134 for(std::size_t i=0; i<_op1.size(); i++)
1135 _op1[i]=(prop.lselect(sign_1, neg_1[i], _op1[i]));
1136
1137 unsigned_divider(_op0, _op1, res, rem);
1138
1140
1142
1143 for(std::size_t i=0; i<res.size(); i++)
1144 res[i]=prop.lselect(result_sign, neg_res[i], res[i]);
1145
1146 for(std::size_t i=0; i<res.size(); i++)
1147 rem[i]=prop.lselect(sign_0, neg_rem[i], rem[i]);
1148}
1149
1151 const bvt &op0,
1152 const bvt &op1,
1153 bvt &result,
1154 bvt &remainer,
1155 representationt rep)
1156{
1158
1159 switch(rep)
1160 {
1162 signed_divider(op0, op1, result, remainer); break;
1164 unsigned_divider(op0, op1, result, remainer); break;
1165 }
1166}
1167
1169 const bvt &op0,
1170 const bvt &op1,
1171 bvt &res,
1172 bvt &rem)
1173{
1174 PRECONDITION(op0.size() == op1.size());
1175 std::size_t width=op0.size();
1176
1177 // If both operands are constant, compute the result directly so it folds to
1178 // constant literals downstream instead of introducing fresh variables and a
1179 // multiplier constraint. Division by zero falls through to the general
1180 // (non-deterministic) encoding below.
1181 if(is_constant(op0) && is_constant(op1))
1182 {
1183 const mp_integer n1 = from_constant(op1);
1184 if(n1 != 0)
1185 {
1186 const mp_integer n0 = from_constant(op0);
1187 res = build_constant(n0 / n1, width);
1188 rem = build_constant(n0 % n1, width);
1189 return;
1190 }
1191 }
1192
1193 // check if we divide by a power of two
1194 #if 0
1195 {
1196 std::size_t one_count=0, non_const_count=0, one_pos=0;
1197
1198 for(std::size_t i=0; i<op1.size(); i++)
1199 {
1200 literalt l=op1[i];
1201 if(l.is_true())
1202 {
1203 one_count++;
1204 one_pos=i;
1205 }
1206 else if(!l.is_false())
1208 }
1209
1210 if(non_const_count==0 && one_count==1 && one_pos!=0)
1211 {
1212 // it is a power of two!
1213 res=shift(op0, LRIGHT, one_pos);
1214
1215 // remainder is just a mask
1216 rem=op0;
1217 for(std::size_t i=one_pos; i<rem.size(); i++)
1218 rem[i]=const_literal(false);
1219 return;
1220 }
1221 }
1222 #endif
1223
1224 // Division by zero test.
1225 // Note that we produce a non-deterministic result in
1226 // case of division by zero. SMT-LIB now says the following:
1227 // bvudiv returns a vector of all 1s if the second operand is 0
1228 // bvurem returns its first operand if the second operand is 0
1229
1231
1232 // free variables for result of division
1233 res = prop.new_variables(width);
1234 rem = prop.new_variables(width);
1235
1236 // add implications
1237
1238 bvt product=
1240
1241 // res*op1 + rem = op0
1242
1244
1245 literalt is_equal=equal(sum, op0);
1246
1248
1249 // op1!=0 => rem < op1
1250
1252 prop.limplies(
1253 is_not_zero, lt_or_le(false, rem, op1, representationt::UNSIGNED)));
1254
1255 // op1!=0 => res <= op0
1256
1258 prop.limplies(
1260}
1261
1262
1263#ifdef COMPACT_EQUAL_CONST
1264// TODO : use for lt_or_le as well
1265
1269void bv_utilst::equal_const_register(const bvt &var)
1270{
1271 PRECONDITION(!is_constant(var));
1272 equal_const_registered.insert(var);
1273 return;
1274}
1275
1282literalt bv_utilst::equal_const_rec(bvt &var, bvt &constant)
1283{
1284 std::size_t size = var.size();
1285
1286 PRECONDITION(size != 0);
1287 PRECONDITION(size == constant.size());
1288 PRECONDITION(is_constant(constant));
1289
1290 if(size == 1)
1291 {
1292 literalt comp = prop.lequal(var[size - 1], constant[size - 1]);
1293 var.pop_back();
1294 constant.pop_back();
1295 return comp;
1296 }
1297 else
1298 {
1299 var_constant_pairt index(var, constant);
1300
1301 equal_const_cachet::iterator entry = equal_const_cache.find(index);
1302
1303 if(entry != equal_const_cache.end())
1304 {
1305 return entry->second;
1306 }
1307 else
1308 {
1309 literalt comp = prop.lequal(var[size - 1], constant[size - 1]);
1310 var.pop_back();
1311 constant.pop_back();
1312
1313 literalt rec = equal_const_rec(var, constant);
1314 literalt compare = prop.land(rec, comp);
1315
1316 equal_const_cache.insert(
1317 std::pair<var_constant_pairt, literalt>(index, compare));
1318
1319 return compare;
1320 }
1321 }
1322}
1323
1332literalt bv_utilst::equal_const(const bvt &var, const bvt &constant)
1333{
1334 std::size_t size = constant.size();
1335
1336 PRECONDITION(var.size() == size);
1337 PRECONDITION(!is_constant(var));
1338 PRECONDITION(is_constant(constant));
1339 PRECONDITION(size >= 2);
1340
1341 // These get modified : be careful!
1342 bvt var_upper;
1343 bvt var_lower;
1344 bvt constant_upper;
1345 bvt constant_lower;
1346
1347 /* Split the constant based on a change in parity
1348 * This is based on the observation that most constants are small,
1349 * so combinations of the lower bits are heavily used but the upper
1350 * bits are almost always either all 0 or all 1.
1351 */
1352 literalt top_bit = constant[size - 1];
1353
1354 std::size_t split = size - 1;
1355 var_upper.push_back(var[size - 1]);
1356 constant_upper.push_back(constant[size - 1]);
1357
1358 for(split = size - 2; split != 0; --split)
1359 {
1360 if(constant[split] != top_bit)
1361 {
1362 break;
1363 }
1364 else
1365 {
1366 var_upper.push_back(var[split]);
1367 constant_upper.push_back(constant[split]);
1368 }
1369 }
1370
1371 for(std::size_t i = 0; i <= split; ++i)
1372 {
1373 var_lower.push_back(var[i]);
1374 constant_lower.push_back(constant[i]);
1375 }
1376
1377 // Check we have split the array correctly
1378 INVARIANT(
1379 var_upper.size() + var_lower.size() == size,
1380 "lower size plus upper size should equal the total size");
1381 INVARIANT(
1382 constant_upper.size() + constant_lower.size() == size,
1383 "lower size plus upper size should equal the total size");
1384
1385 literalt top_comparison = equal_const_rec(var_upper, constant_upper);
1386 literalt bottom_comparison = equal_const_rec(var_lower, constant_lower);
1387
1388 return prop.land(top_comparison, bottom_comparison);
1389}
1390
1391#endif
1392
1397 literalt bv_utilst::equal(const bvt &op0, const bvt &op1)
1398{
1399 PRECONDITION(op0.size() == op1.size());
1400
1401 #ifdef COMPACT_EQUAL_CONST
1402 // simplify_expr should put the constant on the right
1403 // but bit-level simplification may result in the other cases
1404 if(is_constant(op0) && !is_constant(op1) && op0.size() > 2 &&
1406 return equal_const(op1, op0);
1407 else if(!is_constant(op0) && is_constant(op1) && op0.size() > 2 &&
1409 return equal_const(op0, op1);
1410 #endif
1411
1412 bvt equal_bv;
1413 equal_bv.resize(op0.size());
1414
1415 for(std::size_t i=0; i<op0.size(); i++)
1416 equal_bv[i]=prop.lequal(op0[i], op1[i]);
1417
1418 return prop.land(equal_bv);
1419}
1420
1425
1426 #define COMPACT_LT_OR_LE
1427/* Some clauses are not needed for correctness but they remove
1428 models (effectively setting "don't care" bits) and so may be worth
1429 including.*/
1430// #define INCLUDE_REDUNDANT_CLAUSES
1431
1433 bool or_equal,
1434 const bvt &bv0,
1435 const bvt &bv1,
1436 representationt rep)
1437{
1438 PRECONDITION(bv0.size() == bv1.size());
1439 PRECONDITION(!bv0.empty());
1440
1441#ifdef COMPACT_LT_OR_LE
1443 {
1444 if(rep == representationt::SIGNED)
1445 {
1447
1448 if(top0.is_false() && top1.is_true())
1449 return const_literal(false);
1450 else if(top0.is_true() && top1.is_false())
1451 return const_literal(true);
1452
1453 // 1-bit signed: the sign bit is the only bit
1454 if(bv0.size() == 1)
1455 {
1456 if(or_equal)
1457 return prop.lor(top0, !top1);
1458 else
1459 return prop.land(top0, !top1);
1460 }
1461
1462 INVARIANT(
1463 bv0.size() >= 2,
1464 "the compact signed comparison encoding requires at least two bits");
1465 // 1 if a compare is needed below this bit
1466 bvt compareBelow = prop.new_variables(bv0.size() - 1);
1467 size_t start = compareBelow.size() - 1;
1468
1470 if(top0.is_false())
1471 firstComp = !top1;
1472 else if(top0.is_true())
1473 firstComp = top1;
1474 else if(top1.is_false())
1475 firstComp = !top0;
1476 else if(top1.is_true())
1477 firstComp = top0;
1478
1479 literalt result = prop.new_variable();
1480
1481 // When comparing signs we are comparing the top bit
1482 // Four cases...
1483 prop.lcnf(top0, top1, firstComp); // + + compare needed
1484 prop.lcnf(top0, !top1, !result); // + - result false and no compare needed
1485 prop.lcnf(!top0, top1, result); // - + result true and no compare needed
1486 prop.lcnf(!top0, !top1, firstComp); // - - negated compare needed
1487
1488#ifdef INCLUDE_REDUNDANT_CLAUSES
1491# endif
1492
1493 // Determine the output
1494 // \forall i . cb[i] & -a[i] & b[i] => result
1495 // \forall i . cb[i] & a[i] & -b[i] => -result
1496 size_t i = start;
1497 do
1498 {
1499 if(compareBelow[i].is_false())
1500 continue;
1501
1502 prop.lcnf(!compareBelow[i], bv0[i], !bv1[i], result);
1503 prop.lcnf(!compareBelow[i], !bv0[i], bv1[i], !result);
1504 } while(i-- != 0);
1505
1506 // Chain the comparison bit
1507 // \forall i != 0 . cb[i] & a[i] & b[i] => cb[i-1]
1508 // \forall i != 0 . cb[i] & -a[i] & -b[i] => cb[i-1]
1509 for(i = start; i > 0; i--)
1510 {
1511 prop.lcnf(!compareBelow[i], !bv0[i], !bv1[i], compareBelow[i - 1]);
1512 prop.lcnf(!compareBelow[i], bv0[i], bv1[i], compareBelow[i - 1]);
1513 }
1514
1515# ifdef INCLUDE_REDUNDANT_CLAUSES
1516 // Optional zeroing of the comparison bit when not needed
1517 // \forall i != 0 . -c[i] => -c[i-1]
1518 // \forall i != 0 . c[i] & -a[i] & b[i] => -c[i-1]
1519 // \forall i != 0 . c[i] & a[i] & -b[i] => -c[i-1]
1520 for(i = start; i > 0; i--)
1521 {
1522 prop.lcnf(compareBelow[i], !compareBelow[i - 1]);
1523 prop.lcnf(!compareBelow[i], bv0[i], !bv1[i], !compareBelow[i - 1]);
1524 prop.lcnf(!compareBelow[i], !bv0[i], bv1[i], !compareBelow[i - 1]);
1525 }
1526# endif
1527
1528 // The 'base case' of the induction is the case when they are equal
1529 prop.lcnf(
1530 !compareBelow[0], !bv0[0], !bv1[0], (or_equal) ? result : !result);
1531 prop.lcnf(
1532 !compareBelow[0], bv0[0], bv1[0], (or_equal) ? result : !result);
1533
1534 return result;
1535 }
1536 else
1537 {
1538 // Unsigned is much easier
1539 // 1 if a compare is needed below this bit
1541 literalt result;
1542 size_t start = bv0.size() - 1;
1543
1544 // Determine the output
1545 // \forall i . cb[i] & -a[i] & b[i] => result
1546 // \forall i . cb[i] & a[i] & -b[i] => -result
1547 bool same_prefix = true;
1548 size_t i = start;
1549 do
1550 {
1551 if(same_prefix)
1552 {
1553 if(i == 0)
1554 {
1555 if(or_equal)
1556 return prop.lor(!bv0[0], bv1[0]);
1557 else
1558 return prop.land(!bv0[0], bv1[0]);
1559 }
1560 else if(bv0[i] == bv1[i])
1561 continue;
1562 else if(bv0[i].is_false() && bv1[i].is_true())
1563 return const_literal(true);
1564 else if(bv0[i].is_true() && bv1[i].is_false())
1565 return const_literal(false);
1566 else
1567 {
1568 same_prefix = false;
1569 start = i;
1571 compareBelow.push_back(const_literal(true));
1572 result = prop.new_variable();
1573 }
1574 }
1575
1576 prop.lcnf(!compareBelow[i], bv0[i], !bv1[i], result);
1577 prop.lcnf(!compareBelow[i], !bv0[i], bv1[i], !result);
1578 } while(i-- != 0);
1579
1580 // Chain the comparison bit
1581 // \forall i != 0 . cb[i] & a[i] & b[i] => cb[i-1]
1582 // \forall i != 0 . cb[i] & -a[i] & -b[i] => cb[i-1]
1583 for(i = start; i > 0; i--)
1584 {
1585 prop.lcnf(!compareBelow[i], !bv0[i], !bv1[i], compareBelow[i - 1]);
1586 prop.lcnf(!compareBelow[i], bv0[i], bv1[i], compareBelow[i - 1]);
1587 }
1588
1589#ifdef INCLUDE_REDUNDANT_CLAUSES
1590 // Optional zeroing of the comparison bit when not needed
1591 // \forall i != 0 . -c[i] => -c[i-1]
1592 // \forall i != 0 . c[i] & -a[i] & b[i] => -c[i-1]
1593 // \forall i != 0 . c[i] & a[i] & -b[i] => -c[i-1]
1594 for(i = start; i > 0; i--)
1595 {
1596 prop.lcnf(compareBelow[i], !compareBelow[i - 1]);
1597 prop.lcnf(!compareBelow[i], bv0[i], !bv1[i], !compareBelow[i - 1]);
1598 prop.lcnf(!compareBelow[i], !bv0[i], bv1[i], !compareBelow[i - 1]);
1599 }
1600#endif
1601
1602 // The 'base case' of the induction is the case when they are equal
1603 prop.lcnf(
1604 !compareBelow[0], !bv0[0], !bv1[0], (or_equal) ? result : !result);
1605 prop.lcnf(
1606 !compareBelow[0], bv0[0], bv1[0], (or_equal) ? result : !result);
1607
1608 return result;
1609 }
1610 }
1611 else
1612#endif
1613 {
1614 // A <= B iff there is an overflow on A-B
1617
1618 literalt result;
1619
1621 result = prop.lxor(prop.lequal(sign_bit(bv0), sign_bit(bv1)), carry);
1622 else
1623 {
1624 INVARIANT(
1626 "representation has either value signed or unsigned");
1627 result = !carry;
1628 }
1629
1630 if(or_equal)
1631 result=prop.lor(result, equal(bv0, bv1));
1632
1633 return result;
1634 }
1635}
1636
1638 const bvt &op0,
1639 const bvt &op1)
1640{
1641 return lt_or_le(false, op0, op1, representationt::UNSIGNED);
1642}
1643
1645 const bvt &bv0,
1646 const bvt &bv1)
1647{
1648 return lt_or_le(false, bv0, bv1, representationt::SIGNED);
1649}
1650
1652 const bvt &bv0,
1653 irep_idt id,
1654 const bvt &bv1,
1655 representationt rep)
1656{
1657 if(id==ID_equal)
1658 return equal(bv0, bv1);
1659 else if(id==ID_notequal)
1660 return !equal(bv0, bv1);
1661 else if(id==ID_le)
1662 return lt_or_le(true, bv0, bv1, rep);
1663 else if(id==ID_lt)
1664 return lt_or_le(false, bv0, bv1, rep);
1665 else if(id==ID_ge)
1666 return lt_or_le(true, bv1, bv0, rep); // swapped
1667 else if(id==ID_gt)
1668 return lt_or_le(false, bv1, bv0, rep); // swapped
1669 else
1671}
1672
1674{
1675 for(const auto &literal : bv)
1676 {
1677 if(!literal.is_constant())
1678 return false;
1679 }
1680
1681 return true;
1682}
1683
1685 literalt cond,
1686 const bvt &a,
1687 const bvt &b)
1688{
1689 PRECONDITION(a.size() == b.size());
1690
1692 {
1693 for(std::size_t i=0; i<a.size(); i++)
1694 {
1695 prop.lcnf(!cond, a[i], !b[i]);
1696 prop.lcnf(!cond, !a[i], b[i]);
1697 }
1698 }
1699 else
1700 {
1701 prop.limplies(cond, equal(a, b));
1702 }
1703
1704 return;
1705}
1706
1708{
1709 bvt odd_bits;
1710 odd_bits.reserve(src.size()/2);
1711
1712 // check every odd bit
1713 for(std::size_t i=0; i<src.size(); i++)
1714 {
1715 if(i%2!=0)
1716 odd_bits.push_back(src[i]);
1717 }
1718
1719 return prop.lor(odd_bits);
1720}
1721
1723{
1724 bvt even_bits;
1725 even_bits.reserve(src.size()/2);
1726
1727 // get every even bit
1728 for(std::size_t i=0; i<src.size(); i++)
1729 {
1730 if(i%2==0)
1731 even_bits.push_back(src[i]);
1732 }
1733
1734 return even_bits;
1735}
1736
1742{
1743 PRECONDITION(!bv.empty());
1744
1745 // Determine the result width: log2(bv.size()) + 1
1746 std::size_t log2 = address_bits(bv.size());
1747 CHECK_RETURN(log2 >= 1);
1748
1749 // Start with the original bit vector
1750 bvt x = bv;
1751
1752 // Apply the parallel bit counting algorithm from Hacker's Delight (pop0).
1753 // The algorithm works by summing adjacent bit groups of increasing sizes.
1754
1755 // Iterate through the stages of the algorithm, doubling the field size each
1756 // time
1757 for(std::size_t stage = 0; stage < log2; ++stage)
1758 {
1759 std::size_t shift_amount = 1 << stage; // 1, 2, 4, 8, 16, ...
1760 std::size_t field_size = 2 * shift_amount; // 2, 4, 8, 16, 32, ...
1761
1762 // Skip if the bit vector is smaller than the field size
1763 if(x.size() <= shift_amount)
1764 break;
1765
1766 // Shift the bit vector
1768
1769 // Create a mask with 'shift_amount' ones followed by 'shift_amount' zeros,
1770 // repeated
1771 bvt mask;
1772 mask.reserve(x.size());
1773 for(std::size_t i = 0; i < x.size(); i++)
1774 {
1775 if((i % field_size) < shift_amount)
1776 mask.push_back(const_literal(true));
1777 else
1778 mask.push_back(const_literal(false));
1779 }
1780
1781 // Apply the mask to both the original and shifted bit vectors
1783 masked_x.reserve(x.size());
1784 masked_shifted.reserve(x.size());
1785
1786 for(std::size_t i = 0; i < x.size(); i++)
1787 {
1788 masked_x.push_back(prop.land(x[i], mask[i]));
1789 masked_shifted.push_back(prop.land(x_shifted[i], mask[i]));
1790 }
1791
1792 // Add the masked vectors
1794 }
1795
1796 return x;
1797}
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
static bvt inverted(const bvt &op)
Definition bv_utils.cpp:648
literalt signed_less_than(const bvt &bv0, const bvt &bv1)
Definition bv_utils.cpp:1644
static bool is_constant(const bvt &bv)
Definition bv_utils.cpp:1673
std::pair< bvt, literalt > adder(const bvt &op0, const bvt &op1, literalt carry_in)
Return the sum and carry-out when adding op0 and op1 under initial carry carry_in.
Definition bv_utils.cpp:309
bvt wallace_tree(const std::vector< bvt > &pps)
Definition bv_utils.cpp:656
literalt is_not_zero(const bvt &op)
Definition bv_utils.h:151
static bvt verilog_bv_normal_bits(const bvt &)
Definition bv_utils.cpp:1722
literalt is_int_min(const bvt &op)
Definition bv_utils.h:154
static bvt extract_msb(const bvt &a, std::size_t n)
Definition bv_utils.cpp:69
static mp_integer from_constant(const bvt &bv)
Returns the unsigned integer value of the constant bitvector bv.
Definition bv_utils.cpp:27
void set_equal(const bvt &a, const bvt &b)
Definition bv_utils.cpp:46
static literalt sign_bit(const bvt &op)
Definition bv_utils.h:143
bvt multiplier_no_overflow(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.cpp:1099
bvt add_sub_no_overflow(const bvt &op0, const bvt &op1, bool subtract, representationt rep)
Definition bv_utils.cpp:340
bvt add(const bvt &op0, const bvt &op1)
Definition bv_utils.h:71
bvt absolute_value(const bvt &op)
Definition bv_utils.cpp:1045
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
Definition bv_utils.cpp:107
static bvt build_constant(const mp_integer &i, std::size_t width)
Definition bv_utils.cpp:16
void signed_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
Definition bv_utils.cpp:1115
literalt is_zero(const bvt &op)
Definition bv_utils.h:148
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition bv_utils.cpp:1397
bvt popcount(const bvt &bv)
Symbolic implementation of popcount (count of 1 bits in a bit vector) Based on the pop0 algorithm fro...
Definition bv_utils.cpp:1741
bvt signed_multiplier(const bvt &op0, const bvt &op1)
Definition bv_utils.cpp:1014
literalt overflow_add(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.cpp:439
literalt is_one(const bvt &op)
Definition bv_utils.cpp:37
bvt cond_negate_no_overflow(const bvt &bv, const literalt cond)
Definition bv_utils.cpp:1051
literalt overflow_sub(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.cpp:462
void cond_implies_equal(literalt cond, const bvt &a, const bvt &b)
Definition bv_utils.cpp:1684
literalt unsigned_less_than(const bvt &bv0, const bvt &bv1)
Definition bv_utils.cpp:1637
bvt signed_multiplier_no_overflow(const bvt &op0, const bvt &op1)
Definition bv_utils.cpp:1058
bvt incrementer(const bvt &op, literalt carry_in)
Definition bv_utils.cpp:640
bvt add_sub(const bvt &op0, const bvt &op1, bool subtract)
Definition bv_utils.cpp:349
static bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
Definition bv_utils.cpp:548
literalt lt_or_le(bool or_equal, const bvt &bv0, const bvt &bv1, representationt rep)
Definition bv_utils.cpp:1432
literalt overflow_negate(const bvt &op)
Definition bv_utils.cpp:614
static bvt concatenate(const bvt &a, const bvt &b)
Definition bv_utils.cpp:91
shiftt
Definition bv_utils.h:79
@ ROTATE_RIGHT
@ ROTATE_LEFT
@ SHIFT_LEFT
@ SHIFT_ARIGHT
@ SHIFT_LRIGHT
representationt
Definition bv_utils.h:28
@ SIGNED
@ UNSIGNED
literalt full_adder(const literalt a, const literalt b, const literalt carry_in, literalt &carry_out)
Definition bv_utils.cpp:151
bvt negate_no_overflow(const bvt &op)
Definition bv_utils.cpp:608
static bvt extract(const bvt &a, std::size_t first, std::size_t last)
Definition bv_utils.cpp:53
bvt unsigned_multiplier(const bvt &op0, const bvt &op1)
Definition bv_utils.cpp:930
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.h:94
void unsigned_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
Definition bv_utils.cpp:1168
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.cpp:1080
bvt cond_negate(const bvt &bv, const literalt cond)
Definition bv_utils.cpp:1032
bvt dadda_tree(const std::vector< bvt > &pps)
Definition bv_utils.cpp:703
literalt carry_out(const bvt &op0, const bvt &op1, literalt carry_in)
Definition bv_utils.cpp:325
bvt negate(const bvt &op)
Definition bv_utils.cpp:600
static bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
Definition bv_utils.cpp:120
static bvt extract_lsb(const bvt &a, std::size_t n)
Definition bv_utils.cpp:81
literalt verilog_bv_has_x_or_z(const bvt &)
Definition bv_utils.cpp:1707
literalt carry(literalt a, literalt b, literalt c)
Definition bv_utils.cpp:242
bvt unsigned_multiplier_no_overflow(const bvt &op0, const bvt &op1)
Definition bv_utils.cpp:975
static bvt zeros(std::size_t new_size)
Definition bv_utils.h:197
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
Definition bv_utils.cpp:1651
propt & prop
Definition bv_utils.h:233
bvt adder_no_overflow(const bvt &op0, const bvt &op1, bool subtract, representationt rep)
Definition bv_utils.cpp:487
bvt saturating_add_sub(const bvt &op0, const bvt &op1, bool subtract, representationt rep)
Definition bv_utils.cpp:370
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
bool is_true() const
Definition literal.h:156
bool is_false() const
Definition literal.h:161
void l_set_to_true(literalt a)
Definition prop.h:52
virtual literalt land(literalt a, literalt b)=0
virtual literalt limplies(literalt a, literalt b)=0
virtual literalt lselect(literalt a, literalt b, literalt c)=0
virtual bool cnf_handled_well() const
Definition prop.h:85
virtual void l_set_to(literalt a, bool value)
Definition prop.h:47
virtual literalt lxor(literalt a, literalt b)=0
void lcnf(literalt l0, literalt l1)
Definition prop.h:58
virtual void set_equal(literalt a, literalt b)
asserts a==b in the propositional formula
Definition prop.cpp:12
virtual bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition prop.cpp:30
virtual literalt new_variable()=0
virtual literalt lequal(literalt a, literalt b)=0
virtual literalt lor(literalt a, literalt b)=0
void l_set_to_false(literalt a)
Definition prop.h:54
virtual bool has_set_to() const
Definition prop.h:81
bool is_false(const literalt &l)
Definition literal.h:197
bool is_true(const literalt &l)
Definition literal.h:198
std::vector< literalt > bvt
Definition literal.h:201
literalt const_literal(bool value)
Definition literal.h:188
double log2(double x)
Definition math.c:2627
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition mp_arith.cpp:117
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition mp_arith.cpp:64
BigInt mp_integer
Definition smt_terms.h:17
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
#define POSTCONDITION(CONDITION)
Definition invariant.h:479

AltStyle によって変換されたページ (->オリジナル) /