cprover
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 <utility>
12
13bvt bv_utilst::build_constant(const mp_integer &n, std::size_t width)
14{
15 std::string n_str=integer2binary(n, width);
16 CHECK_RETURN(n_str.size() == width);
17 bvt result;
18 result.resize(width);
19 for(std::size_t i=0; i<width; i++)
20 result[i]=const_literal(n_str[width-i-1]=='1');
21 return result;
22}
23
25{
26 PRECONDITION(!bv.empty());
27 bvt tmp;
28 tmp=bv;
29 tmp.erase(tmp.begin(), tmp.begin()+1);
30 return prop.land(is_zero(tmp), bv[0]);
31}
32
33void bv_utilst::set_equal(const bvt &a, const bvt &b)
34{
35 PRECONDITION(a.size() == b.size());
36 for(std::size_t i=0; i<a.size(); i++)
37 prop.set_equal(a[i], b[i]);
38}
39
40bvt bv_utilst::extract(const bvt &a, std::size_t first, std::size_t last)
41{
42 // preconditions
43 PRECONDITION(first < a.size());
44 PRECONDITION(last < a.size());
45 PRECONDITION(first <= last);
46
47 bvt result=a;
48 result.resize(last+1);
49 if(first!=0)
50 result.erase(result.begin(), result.begin()+first);
51
52 POSTCONDITION(result.size() == last - first + 1);
53 return result;
54}
55
56bvt bv_utilst::extract_msb(const bvt &a, std::size_t n)
57{
58 // preconditions
59 PRECONDITION(n <= a.size());
60
61 bvt result=a;
62 result.erase(result.begin(), result.begin()+(result.size()-n));
63
64 POSTCONDITION(result.size() == n);
65 return result;
66}
67
68bvt bv_utilst::extract_lsb(const bvt &a, std::size_t n)
69{
70 // preconditions
71 PRECONDITION(n <= a.size());
72
73 bvt result=a;
74 result.resize(n);
75 return result;
76}
77
79{
80 bvt result;
81
82 result.resize(a.size()+b.size());
83
84 for(std::size_t i=0; i<a.size(); i++)
85 result[i]=a[i];
86
87 for(std::size_t i=0; i<b.size(); i++)
88 result[i+a.size()]=b[i];
89
90 return result;
91}
92
95{
96 PRECONDITION(a.size() == b.size());
97
98 bvt result;
99
100 result.resize(a.size());
101 for(std::size_t i=0; i<result.size(); i++)
102 result[i]=prop.lselect(s, a[i], b[i]);
103
104 return result;
105}
106
108 const bvt &bv,
109 std::size_t new_size,
110 representationt rep)
111{
112 std::size_t old_size=bv.size();
114
115 bvt result=bv;
116 result.resize(new_size);
117
119 (rep==representationt::SIGNED && !bv.empty())?bv[old_size-1]:
120 const_literal(false);
121
122 for(std::size_t i=old_size; i<new_size; i++)
123 result[i]=extend_with;
124
125 return result;
126}
127
128
134// The optimal encoding is the default as it gives a reduction in space
135// and small performance gains
136#define OPTIMAL_FULL_ADDER
137
139 const literalt a,
140 const literalt b,
141 const literalt carry_in,
142 literalt &carry_out)
143{
144 #ifdef OPTIMAL_FULL_ADDER
146 {
147 literalt x;
148 literalt y;
149 int constantProp = -1;
150
151 if(a.is_constant())
152 {
153 x = b;
154 y = carry_in;
155 constantProp = (a.is_true()) ? 1 : 0;
156 }
157 else if(b.is_constant())
158 {
159 x = a;
160 y = carry_in;
161 constantProp = (b.is_true()) ? 1 : 0;
162 }
163 else if(carry_in.is_constant())
164 {
165 x = a;
166 y = b;
167 constantProp = (carry_in.is_true()) ? 1 : 0;
168 }
169
171
172 // Rely on prop.l* to do further constant propagation
173 if(constantProp == 1)
174 {
175 // At least one input bit is 1
176 carry_out = prop.lor(x, y);
177 sum = prop.lequal(x, y);
178 }
179 else if(constantProp == 0)
180 {
181 // At least one input bit is 0
182 carry_out = prop.land(x, y);
183 sum = prop.lxor(x, y);
184 }
185 else
186 {
189
190 // Any two inputs 1 will set the carry_out to 1
191 prop.lcnf(!a, !b, carry_out);
194
195 // Any two inputs 0 will set the carry_out to 0
196 prop.lcnf(a, b, !carry_out);
199
200 // If both carry out and sum are 1 then all inputs are 1
201 prop.lcnf(a, !sum, !carry_out);
202 prop.lcnf(b, !sum, !carry_out);
204
205 // If both carry out and sum are 0 then all inputs are 0
206 prop.lcnf(!a, sum, carry_out);
207 prop.lcnf(!b, sum, carry_out);
209
210 // If all of the inputs are 1 or all are 0 it sets the sum
211 prop.lcnf(!a, !b, !carry_in, sum);
212 prop.lcnf(a, b, carry_in, !sum);
213 }
214
215 return sum;
216 }
217 else // NOLINT(readability/braces)
218 #endif // OPTIMAL_FULL_ADDER
219 {
220 // trivial encoding
222 return prop.lxor(prop.lxor(a, b), carry_in);
223 }
224}
225
226// Daniel's carry optimisation
227#define COMPACT_CARRY
228
230{
231 #ifdef COMPACT_CARRY
233 {
234 // propagation possible?
235 const auto const_count =
236 a.is_constant() + b.is_constant() + c.is_constant();
237
238 // propagation is possible if two or three inputs are constant
239 if(const_count>=2)
240 return prop.lor(prop.lor(
241 prop.land(a, b),
242 prop.land(a, c)),
243 prop.land(b, c));
244
245 // it's also possible if two of a,b,c are the same
246 if(a==b)
247 return a;
248 else if(a==c)
249 return a;
250 else if(b==c)
251 return b;
252
253 // the below yields fewer clauses and variables,
254 // but doesn't propagate anything at all
255
256 bvt clause;
257
259
260 /*
261 carry_correct: LEMMA
262 ( a OR b OR NOT x) AND
263 ( a OR NOT b OR c OR NOT x) AND
264 ( a OR NOT b OR NOT c OR x) AND
265 (NOT a OR b OR c OR NOT x) AND
266 (NOT a OR b OR NOT c OR x) AND
267 (NOT a OR NOT b OR x)
268 IFF
269 (x=((a AND b) OR (a AND c) OR (b AND c)));
270 */
271
272 prop.lcnf(a, b, !x);
273 prop.lcnf(a, !b, c, !x);
274 prop.lcnf(a, !b, !c, x);
275 prop.lcnf(!a, b, c, !x);
276 prop.lcnf(!a, b, !c, x);
277 prop.lcnf(!a, !b, x);
278
279 return x;
280 }
281 else
282 #endif // COMPACT_CARRY
283 {
284 // trivial encoding
285 bvt tmp;
286
287 tmp.push_back(prop.land(a, b));
288 tmp.push_back(prop.land(a, c));
289 tmp.push_back(prop.land(b, c));
290
291 return prop.lor(tmp);
292 }
293}
294
295std::pair<bvt, literalt>
296bv_utilst::adder(const bvt &op0, const bvt &op1, literalt carry_in)
297{
298 PRECONDITION(op0.size() == op1.size());
299
300 std::pair<bvt, literalt> result{bvt{}, carry_in};
301 result.first.reserve(op0.size());
302 literalt &carry_out = result.second;
303
304 for(std::size_t i = 0; i < op0.size(); i++)
305 {
306 result.first.push_back(full_adder(op0[i], op1[i], carry_out, carry_out));
307 }
308
309 return result;
310}
311
313 const bvt &op0,
314 const bvt &op1,
316{
317 PRECONDITION(op0.size() == op1.size());
318
320
321 for(std::size_t i=0; i<op0.size(); i++)
322 carry_out=carry(op0[i], op1[i], carry_out);
323
324 return carry_out;
325}
326
328 const bvt &op0,
329 const bvt &op1,
330 bool subtract,
331 representationt rep)
332{
333 return adder_no_overflow(op0, op1, subtract, rep);
334}
335
336bvt bv_utilst::add_sub(const bvt &op0, const bvt &op1, bool subtract)
337{
338 PRECONDITION(op0.size() == op1.size());
339
341
342 bvt tmp_op1=subtract?inverted(op1):op1;
343
344 // we ignore the carry-out
345 return adder(op0, tmp_op1, carry_in).first;
346}
347
348bvt bv_utilst::add_sub(const bvt &op0, const bvt &op1, literalt subtract)
349{
350 const bvt op1_sign_applied=
351 select(subtract, inverted(op1), op1);
352
353 // we ignore the carry-out
354 return adder(op0, op1_sign_applied, subtract).first;
355}
356
358 const bvt &op0,
359 const bvt &op1,
360 bool subtract,
361 representationt rep)
362{
363 PRECONDITION(op0.size() == op1.size());
366
367 literalt carry_in = const_literal(subtract);
368
369 bvt tmp_op1 = subtract ? inverted(op1) : op1;
370
371 auto add_sub_result = adder(op0, tmp_op1, carry_in);
373
374 bvt result;
375 result.reserve(add_sub_result.first.size());
377 {
378 // An unsigned overflow has occurred when carry_out is not equal to
379 // subtract: addition with a carry-out means an overflow beyond the maximum
380 // representable value, subtraction without a carry-out means an underflow
381 // below zero. For saturating arithmetic the former implies that all bits
382 // should be set to 1, in the latter case all bits should be set to zero.
383 for(const auto &literal : add_sub_result.first)
384 {
385 result.push_back(
386 subtract ? prop.land(literal, carry_out)
388 }
389 }
390 else
391 {
392 // A signed overflow beyond the maximum representable value occurs when
393 // adding two positive numbers and the wrap-around result being negative, or
394 // when subtracting a negative from a positive number (and, again, the
395 // result being negative).
397 !sign_bit(op0),
398 subtract ? sign_bit(op1) : !sign_bit(op1),
399 sign_bit(add_sub_result.first)});
400 // A signed underflow below the minimum representable value occurs when
401 // adding two negative numbers and arriving at a positive result, or
402 // subtracting a positive from a negative number (and, again, obtaining a
403 // positive wrap-around result).
405 sign_bit(op0),
406 subtract ? !sign_bit(op1) : sign_bit(op1),
407 !sign_bit(add_sub_result.first)});
408
409 // set all bits except for the sign bit
410 PRECONDITION(!add_sub_result.first.empty());
411 for(std::size_t i = 0; i < add_sub_result.first.size() - 1; ++i)
412 {
413 const auto &literal = add_sub_result.first[i];
414 result.push_back(prop.land(
416 }
417 // finally add the sign bit
418 result.push_back(prop.land(
421 }
422
423 return result;
424}
425
427 const bvt &op0, const bvt &op1, representationt rep)
428{
430 {
431 // An overflow occurs if the signs of the two operands are the same
432 // and the sign of the sum is the opposite.
433
434 literalt old_sign=op0[op0.size()-1];
435 literalt sign_the_same=prop.lequal(op0[op0.size()-1], op1[op1.size()-1]);
436
437 bvt result=add(op0, op1);
438 return
439 prop.land(sign_the_same, prop.lxor(result[result.size()-1], old_sign));
440 }
441 else if(rep==representationt::UNSIGNED)
442 {
443 // overflow is simply carry-out
444 return carry_out(op0, op1, const_literal(false));
445 }
446 else
448}
449
451 const bvt &op0, const bvt &op1, representationt rep)
452{
454 {
455 // We special-case x-INT_MIN, which is >=0 if
456 // x is negative, always representable, and
457 // thus not an overflow.
459 literalt op0_is_negative=op0[op0.size()-1];
460
461 return
465 }
466 else if(rep==representationt::UNSIGNED)
467 {
468 // overflow is simply _negated_ carry-out
469 return !carry_out(op0, inverted(op1), const_literal(true));
470 }
471 else
473}
474
476 const bvt &op0,
477 const bvt &op1,
478 bool subtract,
479 representationt rep)
480{
481 const bvt tmp_op = subtract ? inverted(op1) : op1;
482
484 {
485 // an overflow occurs if the signs of the two operands are the same
486 // and the sign of the sum is the opposite
487
490
491 // we ignore the carry-out
492 bvt sum = adder(op0, tmp_op, const_literal(subtract)).first;
493
496
497 return sum;
498 }
499 else
500 {
501 INVARIANT(
503 "representation has either value signed or unsigned");
504 auto result = adder(op0, tmp_op, const_literal(subtract));
505 prop.l_set_to(result.second, subtract);
506 return std::move(result.first);
507 }
508}
509
511{
512 return adder_no_overflow(op0, op1, false, representationt::UNSIGNED);
513}
514
515bvt bv_utilst::shift(const bvt &op, const shiftt s, const bvt &dist)
516{
517 std::size_t d=1, width=op.size();
518 bvt result=op;
519
520 for(std::size_t stage=0; stage<dist.size(); stage++)
521 {
522 if(dist[stage]!=const_literal(false))
523 {
524 bvt tmp=shift(result, s, d);
525
526 for(std::size_t i=0; i<width; i++)
527 result[i]=prop.lselect(dist[stage], tmp[i], result[i]);
528 }
529
530 d=d<<1;
531 }
532
533 return result;
534}
535
536bvt bv_utilst::shift(const bvt &src, const shiftt s, std::size_t dist)
537{
538 bvt result;
539 result.resize(src.size());
540
541 // 'dist' is user-controlled, and thus arbitary.
542 // We thus must guard against the case in which i+dist overflows.
543 // We do so by considering the case dist>=src.size().
544
545 for(std::size_t i=0; i<src.size(); i++)
546 {
547 literalt l;
548
549 switch(s)
550 {
552 // no underflow on i-dist because of condition dist<=i
553 l=(dist<=i?src[i-dist]:const_literal(false));
554 break;
555
557 // src.size()-i won't underflow as i<src.size()
558 // Then, if dist<src.size()-i, then i+dist<src.size()
559 l=(dist<src.size()-i?src[i+dist]:src[src.size()-1]); // sign bit
560 break;
561
563 // src.size()-i won't underflow as i<src.size()
564 // Then, if dist<src.size()-i, then i+dist<src.size()
565 l=(dist<src.size()-i?src[i+dist]:const_literal(false));
566 break;
567
569 // prevent overflows by using dist%src.size()
570 l=src[(src.size()+i-(dist%src.size()))%src.size()];
571 break;
572
574 // prevent overflows by using dist%src.size()
575 l=src[(i+(dist%src.size()))%src.size()];
576 break;
577
578 default:
580 }
581
582 result[i]=l;
583 }
584
585 return result;
586}
587
589{
590 bvt result=inverted(bv);
592 incrementer(result, const_literal(true), carry_out);
593 return result;
594}
595
597{
599 return negate(bv);
600}
601
603{
604 // a overflow on unary- can only happen with the smallest
605 // representable number 100....0
606
608 should_be_zeros.pop_back();
609
610 return prop.land(bv[bv.size() - 1], !prop.lor(should_be_zeros));
611}
612
614 bvt &bv,
616 literalt &carry_out)
617{
619
620 for(auto &literal : bv)
621 {
625 }
626}
627
629{
630 bvt result=bv;
633 return result;
634}
635
637{
638 bvt result=bv;
639 for(auto &literal : result)
640 literal = !literal;
641 return result;
642}
643
644bvt bv_utilst::wallace_tree(const std::vector<bvt> &pps)
645{
646 PRECONDITION(!pps.empty());
647
648 if(pps.size()==1)
649 return pps.front();
650 else if(pps.size()==2)
651 return add(pps[0], pps[1]);
652 else
653 {
654 std::vector<bvt> new_pps;
655 std::size_t no_full_adders=pps.size()/3;
656
657 // add groups of three partial products using CSA
658 for(std::size_t i=0; i<no_full_adders; i++)
659 {
660 const bvt &a=pps[i*3+0],
661 &b=pps[i*3+1],
662 &c=pps[i*3+2];
663
664 INVARIANT(a.size() == b.size(), "groups should be of equal size");
665 INVARIANT(a.size() == c.size(), "groups should be of equal size");
666
667 bvt s, t(a.size(), const_literal(false));
668 s.reserve(a.size());
669
670 for(std::size_t bit=0; bit<a.size(); bit++)
671 {
673 s.push_back(full_adder(a[bit], b[bit], c[bit], carry_out));
674 if(bit + 1 < a.size())
675 t[bit + 1] = carry_out;
676 }
677
678 new_pps.push_back(std::move(s));
679 new_pps.push_back(std::move(t));
680 }
681
682 // pass onwards up to two remaining partial products
683 for(std::size_t i=no_full_adders*3; i<pps.size(); i++)
684 new_pps.push_back(pps[i]);
685
686 POSTCONDITION(new_pps.size() < pps.size());
687 return wallace_tree(new_pps);
688 }
689}
690
691bvt bv_utilst::dadda_tree(const std::vector<bvt> &pps)
692{
693 PRECONDITION(!pps.empty());
694
695 using columnt = std::list<literalt>;
696 std::vector<columnt> columns(pps.front().size());
697 for(const auto &pp : pps)
698 {
699 PRECONDITION(pp.size() == pps.front().size());
700 for(std::size_t i = 0; i < pp.size(); ++i)
701 {
702 if(!pp[i].is_false())
703 columns[i].push_back(pp[i]);
704 }
705 }
706
707 std::list<std::size_t> dadda_sequence;
708 for(std::size_t d = 2; d < pps.front().size(); d = (d * 3) / 2)
709 dadda_sequence.push_front(d);
710
711 for(auto d : dadda_sequence)
712 {
713 for(auto col_it = columns.begin(); col_it != columns.end();) // no ++col_it
714 {
715 if(col_it->size() <= d)
716 ++col_it;
717 else if(col_it->size() == d + 1)
718 {
719 // Dadda prescribes a half adder here, but OPTIMAL_FULL_ADDER makes
720 // full_adder actually build a half adder when carry-in is false.
722 col_it->push_back(full_adder(
723 col_it->front(),
724 *std::next(col_it->begin()),
725 const_literal(false),
726 carry_out));
727 col_it->pop_front();
728 col_it->pop_front();
729 if(std::next(col_it) != columns.end())
730 std::next(col_it)->push_back(carry_out);
731 }
732 else
733 {
734 // We could also experiment with n:2 compressors (for n > 3, n=3 is the
735 // full adder as used below) that use circuits with lower gate count
736 // than just combining multiple full adders.
738 col_it->push_back(full_adder(
739 col_it->front(),
740 *std::next(col_it->begin()),
741 *std::next(std::next(col_it->begin())),
742 carry_out));
743 col_it->pop_front();
744 col_it->pop_front();
745 col_it->pop_front();
746 if(std::next(col_it) != columns.end())
747 std::next(col_it)->push_back(carry_out);
748 }
749 }
750 }
751
752 bvt a, b;
753 a.reserve(pps.front().size());
754 b.reserve(pps.front().size());
755
756 for(const auto &col : columns)
757 {
758 PRECONDITION(col.size() <= 2);
759 switch(col.size())
760 {
761 case 0:
762 a.push_back(const_literal(false));
763 b.push_back(const_literal(false));
764 break;
765 case 1:
766 a.push_back(col.front());
767 b.push_back(const_literal(false));
768 break;
769 case 2:
770 a.push_back(col.front());
771 b.push_back(col.back());
772 }
773 }
774
775 return add(a, b);
776}
777
778// Wallace tree multiplier. This is disabled, as runtimes have
779// been observed to go up by 5%-10%, and on some models even by 20%.
780// #define WALLACE_TREE
781// Dadda' reduction scheme. This yields a smaller formula size than Wallace
782// trees (and also the default addition scheme), but remains disabled as it
783// isn't consistently more performant either.
784// #define DADDA_TREE
785
786// The following examples demonstrate the performance differences (with a
787// time-out of 7200 seconds):
788//
789// #ifndef BITWIDTH
790// #define BITWIDTH 8
791// #endif
792//
793// int main()
794// {
795// __CPROVER_bitvector[BITWIDTH] a, b;
796// __CPROVER_assert(a * 3 == a + a + a, "multiplication by 3");
797// __CPROVER_assert(3 * a == a + a + a, "multiplication by 3");
798// __CPROVER_bitvector[BITWIDTH] ab = a * b;
799// __CPROVER_bitvector[BITWIDTH * 2] ab_check =
800// (__CPROVER_bitvector[BITWIDTH * 2])a *
801// (__CPROVER_bitvector[BITWIDTH * 2])b;
802// __CPROVER_assert(
803// ab == (__CPROVER_bitvector[BITWIDTH])ab_check, "should pass");
804// }
805//
806// |----|-----------------------------|-----------------------------|
807// | | CaDiCaL | MiniSat2 |
808// |----|-----------------------------|-----------------------------|
809// | n | No tree | Wallace | Dadda | No tree | Wallace | Dadda |
810// |----|---------|---------|---------|---------|---------|---------|
811// | 1 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 |
812// | 2 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 |
813// | 3 | 0.01 | 0.01 | 0.00 | 0.00 | 0.00 | 0.00 |
814// | 4 | 0.01 | 0.01 | 0.01 | 0.01 | 0.01 | 0.01 |
815// | 5 | 0.04 | 0.04 | 0.04 | 0.01 | 0.01 | 0.01 |
816// | 6 | 0.11 | 0.13 | 0.12 | 0.04 | 0.05 | 0.06 |
817// | 7 | 0.28 | 0.46 | 0.44 | 0.15 | 0.27 | 0.31 |
818// | 8 | 0.50 | 1.55 | 1.09 | 0.90 | 1.06 | 1.36 |
819// | 9 | 2.22 | 3.63 | 2.67 | 3.40 | 5.85 | 3.44 |
820// | 10 | 2.79 | 4.81 | 4.69 | 4.32 | 28.41 | 28.01 |
821// | 11 | 8.48 | 4.45 | 11.99 | 38.24 | 98.55 | 86.46 |
822// | 12 | 14.52 | 4.86 | 5.80 | 115.00 | 140.11 | 461.70 |
823// | 13 | 33.62 | 5.56 | 6.14 | 210.24 | 805.59 | 609.01 |
824// | 14 | 37.23 | 6.11 | 8.01 | 776.75 | 689.96 | 6153.82 |
825// | 15 | 108.65 | 7.86 | 14.72 | 1048.92 | 1421.74 | 6881.78 |
826// | 16 | 102.61 | 14.08 | 18.54 | 1628.01 | timeout | 1943.85 |
827// | 17 | 117.89 | 18.53 | 9.19 | 4148.73 | timeout | timeout |
828// | 18 | 209.40 | 7.97 | 7.74 | 2760.51 | timeout | timeout |
829// | 19 | 168.21 | 18.04 | 15.00 | 2514.21 | timeout | timeout |
830// | 20 | 566.76 | 12.68 | 22.47 | 2609.09 | timeout | timeout |
831// | 21 | 786.31 | 23.80 | 23.80 | 2232.77 | timeout | timeout |
832// | 22 | 817.74 | 17.64 | 22.53 | 3866.70 | timeout | timeout |
833// | 23 | 1102.76 | 24.19 | 26.37 | timeout | timeout | timeout |
834// | 24 | 1319.59 | 27.37 | 29.95 | timeout | timeout | timeout |
835// | 25 | 1786.11 | 27.10 | 29.94 | timeout | timeout | timeout |
836// | 26 | 1952.18 | 31.08 | 33.95 | timeout | timeout | timeout |
837// | 27 | 6908.48 | 27.92 | 34.94 | timeout | timeout | timeout |
838// | 28 | 6919.34 | 36.63 | 33.78 | timeout | timeout | timeout |
839// | 29 | timeout | 27.95 | 40.69 | timeout | timeout | timeout |
840// | 30 | timeout | 36.94 | 31.59 | timeout | timeout | timeout |
841// | 31 | timeout | 38.41 | 40.04 | timeout | timeout | timeout |
842// | 32 | timeout | 33.06 | 91.38 | timeout | timeout | timeout |
843// |----|---------|---------|---------|---------|---------|---------|
844//
845// In summary, both Wallace tree and Dadda reduction are substantially more
846// efficient with CaDiCaL on the above code for all bit width > 11, but somewhat
847// slower with MiniSat.
848//
849// #ifndef BITWIDTH
850// #define BITWIDTH 8
851// #endif
852//
853// int main()
854// {
855// __CPROVER_bitvector[BITWIDTH] a, b, c, ab, bc, abc;
856// ab = a * b;
857// __CPROVER_bitvector[BITWIDTH * 2] ab_check =
858// (__CPROVER_bitvector[BITWIDTH * 2])a *
859// (__CPROVER_bitvector[BITWIDTH * 2])b;
860// __CPROVER_assume(ab == ab_check);
861// bc = b * c;
862// __CPROVER_bitvector[BITWIDTH * 2] bc_check =
863// (__CPROVER_bitvector[BITWIDTH * 2])b *
864// (__CPROVER_bitvector[BITWIDTH * 2])c;
865// __CPROVER_assume(bc == bc_check);
866// abc = ab * c;
867// __CPROVER_bitvector[BITWIDTH * 2] abc_check =
868// (__CPROVER_bitvector[BITWIDTH * 2])ab *
869// (__CPROVER_bitvector[BITWIDTH * 2])c;
870// __CPROVER_assume(abc == abc_check);
871// __CPROVER_assert(abc == a * bc, "associativity");
872// }
873//
874// |----|-----------------------------|-----------------------------|
875// | | CaDiCaL | MiniSat2 |
876// |----|-----------------------------|-----------------------------|
877// | n | No tree | Wallace | Dadda | No tree | Wallace | Dadda |
878// |----|---------|---------|---------|---------|---------|---------|
879// | 1 | 0.00 | 0.00 | 0.00 | 0.01 | 0.01 | 0.01 |
880// | 2 | 0.01 | 0.01 | 0.01 | 0.01 | 0.01 | 0.01 |
881// | 3 | 0.02 | 0.03 | 0.03 | 0.01 | 0.01 | 0.01 |
882// | 4 | 0.05 | 0.07 | 0.06 | 0.02 | 0.02 | 0.02 |
883// | 5 | 0.17 | 0.18 | 0.14 | 0.04 | 0.04 | 0.04 |
884// | 6 | 0.50 | 0.63 | 0.63 | 0.13 | 0.14 | 0.13 |
885// | 7 | 1.01 | 1.15 | 0.90 | 0.43 | 0.47 | 0.47 |
886// | 8 | 1.56 | 1.76 | 1.75 | 3.35 | 2.39 | 1.75 |
887// | 9 | 2.07 | 2.48 | 1.75 | 11.20 | 12.64 | 7.94 |
888// | 10 | 3.58 | 3.88 | 3.54 | 20.23 | 23.49 | 15.66 |
889// | 11 | 5.84 | 7.46 | 5.31 | 49.32 | 39.86 | 44.15 |
890// | 12 | 11.71 | 16.85 | 13.40 | 69.32 | 156.57 | 46.50 |
891// | 13 | 33.22 | 41.95 | 34.43 | 250.91 | 294.73 | 79.47 |
892// | 14 | 76.27 | 109.59 | 84.49 | 226.98 | 259.84 | 258.08 |
893// | 15 | 220.01 | 330.10 | 267.11 | 783.73 | 1160.47 | 1262.91 |
894// | 16 | 591.91 | 981.16 | 808.33 | 2712.20 | 4286.60 | timeout |
895// | 17 | 1634.97 | 2574.81 | 2006.27 | timeout | timeout | timeout |
896// | 18 | 4680.16 | timeout | 6704.35 | timeout | timeout | timeout |
897// | 19 | timeout | timeout | timeout | timeout | timeout | timeout |
898// | 20 | timeout | timeout | timeout | timeout | timeout | timeout |
899// | 21 | timeout | timeout | timeout | timeout | timeout | timeout |
900// | 22 | timeout | timeout | timeout | timeout | timeout | timeout |
901// | 23 | timeout | timeout | timeout | timeout | timeout | timeout |
902// | 24 | timeout | timeout | timeout | timeout | timeout | timeout |
903// | 25 | timeout | timeout | timeout | timeout | timeout | timeout |
904// | 26 | timeout | timeout | timeout | timeout | timeout | timeout |
905// | 27 | timeout | timeout | timeout | timeout | timeout | timeout |
906// | 28 | timeout | timeout | timeout | timeout | timeout | timeout |
907// | 29 | timeout | timeout | timeout | timeout | timeout | timeout |
908// | 30 | timeout | timeout | timeout | timeout | timeout | timeout |
909// | 31 | timeout | timeout | timeout | timeout | timeout | timeout |
910// | 32 | timeout | timeout | timeout | timeout | timeout | timeout |
911// |----|---------|---------|---------|---------|---------|---------|
912//
913// In summary, Wallace tree reduction is slower for both solvers and all bit
914// widths (except BITWIDTH==8 with MiniSat2). Dadda multipliers get closer to
915// our multiplier that's not using a tree reduction scheme, but aren't uniformly
916// better either.
917
919{
920 bvt op0=_op0, op1=_op1;
921
922 if(is_constant(op1))
923 std::swap(op0, op1);
924
925 // build the usual quadratic number of partial products
926 std::vector<bvt> pps;
927 pps.reserve(op0.size());
928
929 for(std::size_t bit=0; bit<op0.size(); bit++)
930 {
931 if(op0[bit] == const_literal(false))
932 continue;
933
934 // zeros according to weight
935 bvt pp = zeros(bit);
936 pp.reserve(op0.size());
937
938 for(std::size_t idx = bit; idx < op0.size(); idx++)
939 pp.push_back(prop.land(op1[idx - bit], op0[bit]));
940
941 pps.push_back(pp);
942 }
943
944 if(pps.empty())
945 return zeros(op0.size());
946 else
947 {
948#ifdef WALLACE_TREE
949 return wallace_tree(pps);
950#elif defined(DADDA_TREE)
951 return dadda_tree(pps);
952#else
953 bvt product = pps.front();
954
955 for(auto it = std::next(pps.begin()); it != pps.end(); ++it)
956 product = add(product, *it);
957
958 return product;
959#endif
960 }
961}
962
964 const bvt &op0,
965 const bvt &op1)
966{
967 bvt _op0=op0, _op1=op1;
968
969 PRECONDITION(_op0.size() == _op1.size());
970
971 if(is_constant(_op1))
972 _op0.swap(_op1);
973
974 bvt product;
975 product.resize(_op0.size());
976
977 for(std::size_t i=0; i<product.size(); i++)
978 product[i]=const_literal(false);
979
980 for(std::size_t sum=0; sum<op0.size(); sum++)
981 if(op0[sum]!=const_literal(false))
982 {
983 bvt tmpop;
984
985 tmpop.reserve(product.size());
986
987 for(std::size_t idx=0; idx<sum; idx++)
988 tmpop.push_back(const_literal(false));
989
990 for(std::size_t idx=sum; idx<product.size(); idx++)
991 tmpop.push_back(prop.land(op1[idx-sum], op0[sum]));
992
994
995 for(std::size_t idx=op1.size()-sum; idx<op1.size(); idx++)
996 prop.l_set_to_false(prop.land(op1[idx], op0[sum]));
997 }
998
999 return product;
1000}
1001
1003{
1004 if(op0.empty() || op1.empty())
1005 return bvt();
1006
1007 literalt sign0=op0[op0.size()-1];
1008 literalt sign1=op1[op1.size()-1];
1009
1010 bvt neg0=cond_negate(op0, sign0);
1011 bvt neg1=cond_negate(op1, sign1);
1012
1014
1016
1017 return cond_negate(result, result_sign);
1018}
1019
1021{
1022 bvt neg_bv=negate(bv);
1023
1024 bvt result;
1025 result.resize(bv.size());
1026
1027 for(std::size_t i=0; i<bv.size(); i++)
1028 result[i]=prop.lselect(cond, neg_bv[i], bv[i]);
1029
1030 return result;
1031}
1032
1034{
1035 PRECONDITION(!bv.empty());
1036 return cond_negate(bv, bv[bv.size()-1]);
1037}
1038
1040{
1042
1043 return cond_negate(bv, cond);
1044}
1045
1047 const bvt &op0,
1048 const bvt &op1)
1049{
1050 if(op0.empty() || op1.empty())
1051 return bvt();
1052
1053 literalt sign0=op0[op0.size()-1];
1054 literalt sign1=op1[op1.size()-1];
1055
1058
1060
1061 prop.l_set_to_false(result[result.size() - 1]);
1062
1064
1065 return cond_negate_no_overflow(result, result_sign);
1066}
1067
1069 const bvt &op0,
1070 const bvt &op1,
1071 representationt rep)
1072{
1073 switch(rep)
1074 {
1075 case representationt::SIGNED: return signed_multiplier(op0, op1);
1076 case representationt::UNSIGNED: return unsigned_multiplier(op0, op1);
1077 }
1078
1080}
1081
1083 const bvt &op0,
1084 const bvt &op1,
1085 representationt rep)
1086{
1087 switch(rep)
1088 {
1090 return signed_multiplier_no_overflow(op0, op1);
1092 return unsigned_multiplier_no_overflow(op0, op1);
1093 }
1094
1096}
1097
1099 const bvt &op0,
1100 const bvt &op1,
1101 bvt &res,
1102 bvt &rem)
1103{
1104 if(op0.empty() || op1.empty())
1105 return;
1106
1107 bvt _op0(op0), _op1(op1);
1108
1109 literalt sign_0=_op0[_op0.size()-1];
1110 literalt sign_1=_op1[_op1.size()-1];
1111
1113
1114 for(std::size_t i=0; i<_op0.size(); i++)
1115 _op0[i]=(prop.lselect(sign_0, neg_0[i], _op0[i]));
1116
1117 for(std::size_t i=0; i<_op1.size(); i++)
1118 _op1[i]=(prop.lselect(sign_1, neg_1[i], _op1[i]));
1119
1120 unsigned_divider(_op0, _op1, res, rem);
1121
1123
1125
1126 for(std::size_t i=0; i<res.size(); i++)
1127 res[i]=prop.lselect(result_sign, neg_res[i], res[i]);
1128
1129 for(std::size_t i=0; i<res.size(); i++)
1130 rem[i]=prop.lselect(sign_0, neg_rem[i], rem[i]);
1131}
1132
1134 const bvt &op0,
1135 const bvt &op1,
1136 bvt &result,
1137 bvt &remainer,
1138 representationt rep)
1139{
1141
1142 switch(rep)
1143 {
1145 signed_divider(op0, op1, result, remainer); break;
1147 unsigned_divider(op0, op1, result, remainer); break;
1148 }
1149}
1150
1152 const bvt &op0,
1153 const bvt &op1,
1154 bvt &res,
1155 bvt &rem)
1156{
1157 std::size_t width=op0.size();
1158
1159 // check if we divide by a power of two
1160 #if 0
1161 {
1162 std::size_t one_count=0, non_const_count=0, one_pos=0;
1163
1164 for(std::size_t i=0; i<op1.size(); i++)
1165 {
1166 literalt l=op1[i];
1167 if(l.is_true())
1168 {
1169 one_count++;
1170 one_pos=i;
1171 }
1172 else if(!l.is_false())
1174 }
1175
1176 if(non_const_count==0 && one_count==1 && one_pos!=0)
1177 {
1178 // it is a power of two!
1179 res=shift(op0, LRIGHT, one_pos);
1180
1181 // remainder is just a mask
1182 rem=op0;
1183 for(std::size_t i=one_pos; i<rem.size(); i++)
1184 rem[i]=const_literal(false);
1185 return;
1186 }
1187 }
1188 #endif
1189
1190 // Division by zero test.
1191 // Note that we produce a non-deterministic result in
1192 // case of division by zero. SMT-LIB now says the following:
1193 // bvudiv returns a vector of all 1s if the second operand is 0
1194 // bvurem returns its first operand if the second operand is 0
1195
1197
1198 // free variables for result of division
1199 res = prop.new_variables(width);
1200 rem = prop.new_variables(width);
1201
1202 // add implications
1203
1204 bvt product=
1206
1207 // res*op1 + rem = op0
1208
1210
1211 literalt is_equal=equal(sum, op0);
1212
1214
1215 // op1!=0 => rem < op1
1216
1218 prop.limplies(
1219 is_not_zero, lt_or_le(false, rem, op1, representationt::UNSIGNED)));
1220
1221 // op1!=0 => res <= op0
1222
1224 prop.limplies(
1226}
1227
1228
1229#ifdef COMPACT_EQUAL_CONST
1230// TODO : use for lt_or_le as well
1231
1235void bv_utilst::equal_const_register(const bvt &var)
1236{
1238 equal_const_registered.insert(var);
1239 return;
1240}
1241
1248literalt bv_utilst::equal_const_rec(bvt &var, bvt &constant)
1249{
1250 std::size_t size = var.size();
1251
1252 PRECONDITION(size != 0);
1253 PRECONDITION(size == constant.size());
1254 PRECONDITION(is_constant(constant));
1255
1256 if(size == 1)
1257 {
1258 literalt comp = prop.lequal(var[size - 1], constant[size - 1]);
1259 var.pop_back();
1260 constant.pop_back();
1261 return comp;
1262 }
1263 else
1264 {
1265 var_constant_pairt index(var, constant);
1266
1267 equal_const_cachet::iterator entry = equal_const_cache.find(index);
1268
1269 if(entry != equal_const_cache.end())
1270 {
1271 return entry->second;
1272 }
1273 else
1274 {
1275 literalt comp = prop.lequal(var[size - 1], constant[size - 1]);
1276 var.pop_back();
1277 constant.pop_back();
1278
1279 literalt rec = equal_const_rec(var, constant);
1280 literalt compare = prop.land(rec, comp);
1281
1282 equal_const_cache.insert(
1283 std::pair<var_constant_pairt, literalt>(index, compare));
1284
1285 return compare;
1286 }
1287 }
1288}
1289
1298literalt bv_utilst::equal_const(const bvt &var, const bvt &constant)
1299{
1300 std::size_t size = constant.size();
1301
1302 PRECONDITION(var.size() == size);
1304 PRECONDITION(is_constant(constant));
1305 PRECONDITION(size >= 2);
1306
1307 // These get modified : be careful!
1308 bvt var_upper;
1309 bvt var_lower;
1312
1313 /* Split the constant based on a change in parity
1314 * This is based on the observation that most constants are small,
1315 * so combinations of the lower bits are heavily used but the upper
1316 * bits are almost always either all 0 or all 1.
1317 */
1318 literalt top_bit = constant[size - 1];
1319
1320 std::size_t split = size - 1;
1321 var_upper.push_back(var[size - 1]);
1322 constant_upper.push_back(constant[size - 1]);
1323
1324 for(split = size - 2; split != 0; --split)
1325 {
1326 if(constant[split] != top_bit)
1327 {
1328 break;
1329 }
1330 else
1331 {
1332 var_upper.push_back(var[split]);
1333 constant_upper.push_back(constant[split]);
1334 }
1335 }
1336
1337 for(std::size_t i = 0; i <= split; ++i)
1338 {
1339 var_lower.push_back(var[i]);
1340 constant_lower.push_back(constant[i]);
1341 }
1342
1343 // Check we have split the array correctly
1344 INVARIANT(
1345 var_upper.size() + var_lower.size() == size,
1346 "lower size plus upper size should equal the total size");
1347 INVARIANT(
1348 constant_upper.size() + constant_lower.size() == size,
1349 "lower size plus upper size should equal the total size");
1350
1353
1355}
1356
1357#endif
1358
1363literalt bv_utilst::equal(const bvt &op0, const bvt &op1)
1364{
1365 PRECONDITION(op0.size() == op1.size());
1366
1367 #ifdef COMPACT_EQUAL_CONST
1368 // simplify_expr should put the constant on the right
1369 // but bit-level simplification may result in the other cases
1370 if(is_constant(op0) && !is_constant(op1) && op0.size() > 2 &&
1372 return equal_const(op1, op0);
1373 else if(!is_constant(op0) && is_constant(op1) && op0.size() > 2 &&
1375 return equal_const(op0, op1);
1376 #endif
1377
1378 bvt equal_bv;
1379 equal_bv.resize(op0.size());
1380
1381 for(std::size_t i=0; i<op0.size(); i++)
1382 equal_bv[i]=prop.lequal(op0[i], op1[i]);
1383
1384 return prop.land(equal_bv);
1385}
1386
1391
1392#define COMPACT_LT_OR_LE
1393/* Some clauses are not needed for correctness but they remove
1394 models (effectively setting "don't care" bits) and so may be worth
1395 including.*/
1396// #define INCLUDE_REDUNDANT_CLAUSES
1397
1399 bool or_equal,
1400 const bvt &bv0,
1401 const bvt &bv1,
1402 representationt rep)
1403{
1404 PRECONDITION(bv0.size() == bv1.size());
1405
1406 literalt top0=bv0[bv0.size()-1],
1407 top1=bv1[bv1.size()-1];
1408
1409#ifdef COMPACT_LT_OR_LE
1411 {
1412 bvt compareBelow; // 1 if a compare is needed below this bit
1413 literalt result;
1414 size_t start;
1415 size_t i;
1416
1417 if(rep == representationt::SIGNED)
1418 {
1419 if(top0.is_false() && top1.is_true())
1420 return const_literal(false);
1421 else if(top0.is_true() && top1.is_false())
1422 return const_literal(true);
1423
1424 INVARIANT(
1425 bv0.size() >= 2, "signed bitvectors should have at least two bits");
1426 compareBelow = prop.new_variables(bv0.size() - 1);
1427 start = compareBelow.size() - 1;
1428
1430 if(top0.is_false())
1431 firstComp = !top1;
1432 else if(top0.is_true())
1433 firstComp = top1;
1434 else if(top1.is_false())
1435 firstComp = !top0;
1436 else if(top1.is_true())
1437 firstComp = top0;
1438
1439 result = prop.new_variable();
1440
1441 // When comparing signs we are comparing the top bit
1442 // Four cases...
1443 prop.lcnf(top0, top1, firstComp); // + + compare needed
1444 prop.lcnf(top0, !top1, !result); // + - result false and no compare needed
1445 prop.lcnf(!top0, top1, result); // - + result true and no compare needed
1446 prop.lcnf(!top0, !top1, firstComp); // - - negated compare needed
1447
1448#ifdef INCLUDE_REDUNDANT_CLAUSES
1451#endif
1452 }
1453 else
1454 {
1455 // Unsigned is much easier
1456 compareBelow = prop.new_variables(bv0.size() - 1);
1457 compareBelow.push_back(const_literal(true));
1458 start = compareBelow.size() - 1;
1459 result = prop.new_variable();
1460 }
1461
1462 // Determine the output
1463 // \forall i . cb[i] & -a[i] & b[i] => result
1464 // \forall i . cb[i] & a[i] & -b[i] => -result
1465 i = start;
1466 do
1467 {
1468 if(compareBelow[i].is_false())
1469 continue;
1470 else if(compareBelow[i].is_true())
1471 {
1472 if(bv0[i].is_false() && bv1[i].is_true())
1473 return const_literal(true);
1474 else if(bv0[i].is_true() && bv1[i].is_false())
1475 return const_literal(false);
1476 }
1477
1478 prop.lcnf(!compareBelow[i], bv0[i], !bv1[i], result);
1479 prop.lcnf(!compareBelow[i], !bv0[i], bv1[i], !result);
1480 }
1481 while(i-- != 0);
1482
1483 // Chain the comparison bit
1484 // \forall i != 0 . cb[i] & a[i] & b[i] => cb[i-1]
1485 // \forall i != 0 . cb[i] & -a[i] & -b[i] => cb[i-1]
1486 for(i = start; i > 0; i--)
1487 {
1488 prop.lcnf(!compareBelow[i], !bv0[i], !bv1[i], compareBelow[i-1]);
1489 prop.lcnf(!compareBelow[i], bv0[i], bv1[i], compareBelow[i-1]);
1490 }
1491
1492
1493#ifdef INCLUDE_REDUNDANT_CLAUSES
1494 // Optional zeroing of the comparison bit when not needed
1495 // \forall i != 0 . -c[i] => -c[i-1]
1496 // \forall i != 0 . c[i] & -a[i] & b[i] => -c[i-1]
1497 // \forall i != 0 . c[i] & a[i] & -b[i] => -c[i-1]
1498 for(i = start; i > 0; i--)
1499 {
1501 prop.lcnf(!compareBelow[i], bv0[i], !bv1[i], !compareBelow[i-1]);
1502 prop.lcnf(!compareBelow[i], !bv0[i], bv1[i], !compareBelow[i-1]);
1503 }
1504#endif
1505
1506 // The 'base case' of the induction is the case when they are equal
1507 prop.lcnf(!compareBelow[0], !bv0[0], !bv1[0], (or_equal)?result:!result);
1508 prop.lcnf(!compareBelow[0], bv0[0], bv1[0], (or_equal)?result:!result);
1509
1510 return result;
1511 }
1512 else
1513#endif
1514 {
1517
1518 literalt result;
1519
1521 result=prop.lxor(prop.lequal(top0, top1), carry);
1522 else
1523 {
1524 INVARIANT(
1526 "representation has either value signed or unsigned");
1527 result = !carry;
1528 }
1529
1530 if(or_equal)
1531 result=prop.lor(result, equal(bv0, bv1));
1532
1533 return result;
1534 }
1535}
1536
1538 const bvt &op0,
1539 const bvt &op1)
1540{
1541#ifdef COMPACT_LT_OR_LE
1542 return lt_or_le(false, op0, op1, representationt::UNSIGNED);
1543#else
1544 // A <= B iff there is an overflow on A-B
1545 return !carry_out(op0, inverted(op1), const_literal(true));
1546#endif
1547}
1548
1550 const bvt &bv0,
1551 const bvt &bv1)
1552{
1553 return lt_or_le(false, bv0, bv1, representationt::SIGNED);
1554}
1555
1557 const bvt &bv0,
1558 irep_idt id,
1559 const bvt &bv1,
1560 representationt rep)
1561{
1562 if(id==ID_equal)
1563 return equal(bv0, bv1);
1564 else if(id==ID_notequal)
1565 return !equal(bv0, bv1);
1566 else if(id==ID_le)
1567 return lt_or_le(true, bv0, bv1, rep);
1568 else if(id==ID_lt)
1569 return lt_or_le(false, bv0, bv1, rep);
1570 else if(id==ID_ge)
1571 return lt_or_le(true, bv1, bv0, rep); // swapped
1572 else if(id==ID_gt)
1573 return lt_or_le(false, bv1, bv0, rep); // swapped
1574 else
1576}
1577
1579{
1580 for(const auto &literal : bv)
1581 {
1582 if(!literal.is_constant())
1583 return false;
1584 }
1585
1586 return true;
1587}
1588
1590 literalt cond,
1591 const bvt &a,
1592 const bvt &b)
1593{
1594 PRECONDITION(a.size() == b.size());
1595
1597 {
1598 for(std::size_t i=0; i<a.size(); i++)
1599 {
1600 prop.lcnf(!cond, a[i], !b[i]);
1601 prop.lcnf(!cond, !a[i], b[i]);
1602 }
1603 }
1604 else
1605 {
1606 prop.limplies(cond, equal(a, b));
1607 }
1608
1609 return;
1610}
1611
1613{
1614 bvt odd_bits;
1615 odd_bits.reserve(src.size()/2);
1616
1617 // check every odd bit
1618 for(std::size_t i=0; i<src.size(); i++)
1619 {
1620 if(i%2!=0)
1621 odd_bits.push_back(src[i]);
1622 }
1623
1624 return prop.lor(odd_bits);
1625}
1626
1628{
1629 bvt even_bits;
1630 even_bits.reserve(src.size()/2);
1631
1632 // get every even bit
1633 for(std::size_t i=0; i<src.size(); i++)
1634 {
1635 if(i%2==0)
1636 even_bits.push_back(src[i]);
1637 }
1638
1639 return even_bits;
1640}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
static bvt inverted(const bvt &op)
Definition bv_utils.cpp:636
literalt signed_less_than(const bvt &bv0, const bvt &bv1)
static bool is_constant(const bvt &bv)
NODISCARD 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:296
bvt wallace_tree(const std::vector< bvt > &pps)
Definition bv_utils.cpp:644
literalt is_not_zero(const bvt &op)
Definition bv_utils.h:147
static bvt verilog_bv_normal_bits(const bvt &)
literalt is_int_min(const bvt &op)
Definition bv_utils.h:150
static bvt extract_msb(const bvt &a, std::size_t n)
Definition bv_utils.cpp:56
void set_equal(const bvt &a, const bvt &b)
Definition bv_utils.cpp:33
static literalt sign_bit(const bvt &op)
Definition bv_utils.h:139
bvt multiplier_no_overflow(const bvt &op0, const bvt &op1, representationt rep)
bvt add_sub_no_overflow(const bvt &op0, const bvt &op1, bool subtract, representationt rep)
Definition bv_utils.cpp:327
bvt add(const bvt &op0, const bvt &op1)
Definition bv_utils.h:67
bvt absolute_value(const bvt &op)
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
Definition bv_utils.cpp:94
static bvt build_constant(const mp_integer &i, std::size_t width)
Definition bv_utils.cpp:13
void signed_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
literalt is_zero(const bvt &op)
Definition bv_utils.h:144
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
bvt signed_multiplier(const bvt &op0, const bvt &op1)
literalt overflow_add(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.cpp:426
literalt is_one(const bvt &op)
Definition bv_utils.cpp:24
bvt cond_negate_no_overflow(const bvt &bv, const literalt cond)
literalt overflow_sub(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.cpp:450
void cond_implies_equal(literalt cond, const bvt &a, const bvt &b)
literalt unsigned_less_than(const bvt &bv0, const bvt &bv1)
bvt signed_multiplier_no_overflow(const bvt &op0, const bvt &op1)
bvt incrementer(const bvt &op, literalt carry_in)
Definition bv_utils.cpp:628
bvt add_sub(const bvt &op0, const bvt &op1, bool subtract)
Definition bv_utils.cpp:336
static bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
Definition bv_utils.cpp:536
literalt lt_or_le(bool or_equal, const bvt &bv0, const bvt &bv1, representationt rep)
literalt overflow_negate(const bvt &op)
Definition bv_utils.cpp:602
static bvt concatenate(const bvt &a, const bvt &b)
Definition bv_utils.cpp:78
representationt
Definition bv_utils.h:29
literalt full_adder(const literalt a, const literalt b, const literalt carry_in, literalt &carry_out)
Definition bv_utils.cpp:138
bvt negate_no_overflow(const bvt &op)
Definition bv_utils.cpp:596
static bvt extract(const bvt &a, std::size_t first, std::size_t last)
Definition bv_utils.cpp:40
bvt unsigned_multiplier(const bvt &op0, const bvt &op1)
Definition bv_utils.cpp:918
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.h:90
void unsigned_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
bvt cond_negate(const bvt &bv, const literalt cond)
bvt dadda_tree(const std::vector< bvt > &pps)
Definition bv_utils.cpp:691
literalt carry_out(const bvt &op0, const bvt &op1, literalt carry_in)
Definition bv_utils.cpp:312
bvt negate(const bvt &op)
Definition bv_utils.cpp:588
static bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
Definition bv_utils.cpp:107
static bvt extract_lsb(const bvt &a, std::size_t n)
Definition bv_utils.cpp:68
literalt verilog_bv_has_x_or_z(const bvt &)
literalt carry(literalt a, literalt b, literalt c)
Definition bv_utils.cpp:229
bvt unsigned_multiplier_no_overflow(const bvt &op0, const bvt &op1)
Definition bv_utils.cpp:963
static bvt zeros(std::size_t new_size)
Definition bv_utils.h:193
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
propt & prop
Definition bv_utils.h:223
NODISCARD bvt adder_no_overflow(const bvt &op0, const bvt &op1, bool subtract, representationt rep)
Definition bv_utils.cpp:475
bvt saturating_add_sub(const bvt &op0, const bvt &op1, bool subtract, representationt rep)
Definition bv_utils.cpp:357
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
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
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition mp_arith.cpp:64
#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