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
11bvt bv_utilst::build_constant(const mp_integer &n, std::size_t width)
12{
13 std::string n_str=integer2binary(n, width);
14 CHECK_RETURN(n_str.size() == width);
15 bvt result;
16 result.resize(width);
17 for(std::size_t i=0; i<width; i++)
18 result[i]=const_literal(n_str[width-i-1]=='1');
19 return result;
20}
21
23{
24 PRECONDITION(!bv.empty());
25 bvt tmp;
26 tmp=bv;
27 tmp.erase(tmp.begin(), tmp.begin()+1);
28 return prop.land(is_zero(tmp), bv[0]);
29}
30
31void bv_utilst::set_equal(const bvt &a, const bvt &b)
32{
33 PRECONDITION(a.size() == b.size());
34 for(std::size_t i=0; i<a.size(); i++)
35 prop.set_equal(a[i], b[i]);
36}
37
38bvt bv_utilst::extract(const bvt &a, std::size_t first, std::size_t last)
39{
40 // preconditions
41 PRECONDITION(first < a.size());
42 PRECONDITION(last < a.size());
43 PRECONDITION(first <= last);
44
45 bvt result=a;
46 result.resize(last+1);
47 if(first!=0)
48 result.erase(result.begin(), result.begin()+first);
49
50 POSTCONDITION(result.size() == last - first + 1);
51 return result;
52}
53
54bvt bv_utilst::extract_msb(const bvt &a, std::size_t n)
55{
56 // preconditions
57 PRECONDITION(n <= a.size());
58
59 bvt result=a;
60 result.erase(result.begin(), result.begin()+(result.size()-n));
61
62 POSTCONDITION(result.size() == n);
63 return result;
64}
65
66bvt bv_utilst::extract_lsb(const bvt &a, std::size_t n)
67{
68 // preconditions
69 PRECONDITION(n <= a.size());
70
71 bvt result=a;
72 result.resize(n);
73 return result;
74}
75
76bvt bv_utilst::concatenate(const bvt &a, const bvt &b)
77{
78 bvt result;
79
80 result.resize(a.size()+b.size());
81
82 for(std::size_t i=0; i<a.size(); i++)
83 result[i]=a[i];
84
85 for(std::size_t i=0; i<b.size(); i++)
86 result[i+a.size()]=b[i];
87
88 return result;
89}
90
92bvt bv_utilst::select(literalt s, const bvt &a, const bvt &b)
93{
94 PRECONDITION(a.size() == b.size());
95
96 bvt result;
97
98 result.resize(a.size());
99 for(std::size_t i=0; i<result.size(); i++)
100 result[i]=prop.lselect(s, a[i], b[i]);
101
102 return result;
103}
104
106 const bvt &bv,
107 std::size_t new_size,
108 representationt rep)
109{
110 std::size_t old_size=bv.size();
111 PRECONDITION(old_size != 0);
112
113 bvt result=bv;
114 result.resize(new_size);
115
116 literalt extend_with=
117 (rep==representationt::SIGNED && !bv.empty())?bv[old_size-1]:
118 const_literal(false);
119
120 for(std::size_t i=old_size; i<new_size; i++)
121 result[i]=extend_with;
122
123 return result;
124}
125
126
132// The optimal encoding is the default as it gives a reduction in space
133// and small performance gains
134#define OPTIMAL_FULL_ADDER
135
137 const literalt a,
138 const literalt b,
139 const literalt carry_in,
140 literalt &carry_out)
141{
142 #ifdef OPTIMAL_FULL_ADDER
144 {
145 literalt x;
146 literalt y;
147 int constantProp = -1;
148
149 if(a.is_constant())
150 {
151 x = b;
152 y = carry_in;
153 constantProp = (a.is_true()) ? 1 : 0;
154 }
155 else if(b.is_constant())
156 {
157 x = a;
158 y = carry_in;
159 constantProp = (b.is_true()) ? 1 : 0;
160 }
161 else if(carry_in.is_constant())
162 {
163 x = a;
164 y = b;
165 constantProp = (carry_in.is_true()) ? 1 : 0;
166 }
167
168 literalt sum;
169
170 // Rely on prop.l* to do further constant propagation
171 if(constantProp == 1)
172 {
173 // At least one input bit is 1
174 carry_out = prop.lor(x, y);
175 sum = prop.lequal(x, y);
176 }
177 else if(constantProp == 0)
178 {
179 // At least one input bit is 0
180 carry_out = prop.land(x, y);
181 sum = prop.lxor(x, y);
182 }
183 else
184 {
186 sum = prop.new_variable();
187
188 // Any two inputs 1 will set the carry_out to 1
189 prop.lcnf(!a, !b, carry_out);
190 prop.lcnf(!a, !carry_in, carry_out);
191 prop.lcnf(!b, !carry_in, carry_out);
192
193 // Any two inputs 0 will set the carry_out to 0
194 prop.lcnf(a, b, !carry_out);
195 prop.lcnf(a, carry_in, !carry_out);
196 prop.lcnf(b, carry_in, !carry_out);
197
198 // If both carry out and sum are 1 then all inputs are 1
199 prop.lcnf(a, !sum, !carry_out);
200 prop.lcnf(b, !sum, !carry_out);
201 prop.lcnf(carry_in, !sum, !carry_out);
202
203 // If both carry out and sum are 0 then all inputs are 0
204 prop.lcnf(!a, sum, carry_out);
205 prop.lcnf(!b, sum, carry_out);
206 prop.lcnf(!carry_in, sum, carry_out);
207
208 // If all of the inputs are 1 or all are 0 it sets the sum
209 prop.lcnf(!a, !b, !carry_in, sum);
210 prop.lcnf(a, b, carry_in, !sum);
211 }
212
213 return sum;
214 }
215 else // NOLINT(readability/braces)
216 #endif // OPTIMAL_FULL_ADDER
217 {
218 // trivial encoding
219 carry_out=carry(a, b, carry_in);
220 return prop.lxor(prop.lxor(a, b), carry_in);
221 }
222}
223
224// Daniel's carry optimisation
225#define COMPACT_CARRY
226
228{
229 #ifdef COMPACT_CARRY
231 {
232 // propagation possible?
233 const auto const_count =
234 a.is_constant() + b.is_constant() + c.is_constant();
235
236 // propagation is possible if two or three inputs are constant
237 if(const_count>=2)
238 return prop.lor(prop.lor(
239 prop.land(a, b),
240 prop.land(a, c)),
241 prop.land(b, c));
242
243 // it's also possible if two of a,b,c are the same
244 if(a==b)
245 return a;
246 else if(a==c)
247 return a;
248 else if(b==c)
249 return b;
250
251 // the below yields fewer clauses and variables,
252 // but doesn't propagate anything at all
253
254 bvt clause;
255
257
258 /*
259 carry_correct: LEMMA
260 ( a OR b OR NOT x) AND
261 ( a OR NOT b OR c OR NOT x) AND
262 ( a OR NOT b OR NOT c OR x) AND
263 (NOT a OR b OR c OR NOT x) AND
264 (NOT a OR b OR NOT c OR x) AND
265 (NOT a OR NOT b OR x)
266 IFF
267 (x=((a AND b) OR (a AND c) OR (b AND c)));
268 */
269
270 prop.lcnf(a, b, !x);
271 prop.lcnf(a, !b, c, !x);
272 prop.lcnf(a, !b, !c, x);
273 prop.lcnf(!a, b, c, !x);
274 prop.lcnf(!a, b, !c, x);
275 prop.lcnf(!a, !b, x);
276
277 return x;
278 }
279 else
280 #endif // COMPACT_CARRY
281 {
282 // trivial encoding
283 bvt tmp;
284
285 tmp.push_back(prop.land(a, b));
286 tmp.push_back(prop.land(a, c));
287 tmp.push_back(prop.land(b, c));
288
289 return prop.lor(tmp);
290 }
291}
292
294 bvt &sum,
295 const bvt &op,
296 literalt carry_in,
297 literalt &carry_out)
298{
299 PRECONDITION(sum.size() == op.size());
300
301 carry_out=carry_in;
302
303 for(std::size_t i=0; i<sum.size(); i++)
304 {
305 sum[i] = full_adder(sum[i], op[i], carry_out, carry_out);
306 }
307}
308
310 const bvt &op0,
311 const bvt &op1,
312 literalt carry_in)
313{
314 PRECONDITION(op0.size() == op1.size());
315
316 literalt carry_out=carry_in;
317
318 for(std::size_t i=0; i<op0.size(); i++)
319 carry_out=carry(op0[i], op1[i], carry_out);
320
321 return carry_out;
322}
323
325 const bvt &op0,
326 const bvt &op1,
327 bool subtract,
328 representationt rep)
329{
330 bvt sum=op0;
331 adder_no_overflow(sum, op1, subtract, rep);
332 return sum;
333}
334
335bvt bv_utilst::add_sub(const bvt &op0, const bvt &op1, bool subtract)
336{
337 PRECONDITION(op0.size() == op1.size());
338
339 literalt carry_in=const_literal(subtract);
341
342 bvt result=op0;
343 bvt tmp_op1=subtract?inverted(op1):op1;
344
345 adder(result, tmp_op1, carry_in, carry_out);
346
347 return result;
348}
349
350bvt bv_utilst::add_sub(const bvt &op0, const bvt &op1, literalt subtract)
351{
352 const bvt op1_sign_applied=
353 select(subtract, inverted(op1), op1);
354
355 bvt result=op0;
357
358 adder(result, op1_sign_applied, subtract, carry_out);
359
360 return result;
361}
362
364 const bvt &op0, const bvt &op1, representationt rep)
365{
367 {
368 // An overflow occurs if the signs of the two operands are the same
369 // and the sign of the sum is the opposite.
370
371 literalt old_sign=op0[op0.size()-1];
372 literalt sign_the_same=prop.lequal(op0[op0.size()-1], op1[op1.size()-1]);
373
374 bvt result=add(op0, op1);
375 return
376 prop.land(sign_the_same, prop.lxor(result[result.size()-1], old_sign));
377 }
378 else if(rep==representationt::UNSIGNED)
379 {
380 // overflow is simply carry-out
381 return carry_out(op0, op1, const_literal(false));
382 }
383 else
385}
386
388 const bvt &op0, const bvt &op1, representationt rep)
389{
391 {
392 // We special-case x-INT_MIN, which is >=0 if
393 // x is negative, always representable, and
394 // thus not an overflow.
395 literalt op1_is_int_min=is_int_min(op1);
396 literalt op0_is_negative=op0[op0.size()-1];
397
398 return
399 prop.lselect(op1_is_int_min,
400 !op0_is_negative,
402 }
403 else if(rep==representationt::UNSIGNED)
404 {
405 // overflow is simply _negated_ carry-out
406 return !carry_out(op0, inverted(op1), const_literal(true));
407 }
408 else
410}
411
413 bvt &sum,
414 const bvt &op,
415 bool subtract,
416 representationt rep)
417{
418 const bvt tmp_op=subtract?inverted(op):op;
419
421 {
422 // an overflow occurs if the signs of the two operands are the same
423 // and the sign of the sum is the opposite
424
425 literalt old_sign=sum[sum.size()-1];
426 literalt sign_the_same=
427 prop.lequal(sum[sum.size()-1], tmp_op[tmp_op.size()-1]);
428
430 adder(sum, tmp_op, const_literal(subtract), carry);
431
432 // result of addition in sum
434 prop.land(sign_the_same, prop.lxor(sum[sum.size()-1], old_sign)));
435 }
436 else
437 {
438 INVARIANT(
440 "representation has either value signed or unsigned");
442 adder(sum, tmp_op, const_literal(subtract), carry_out);
443 prop.l_set_to(carry_out, subtract);
444 }
445}
446
448{
450
451 adder(sum, op, carry_out, carry_out);
452
453 prop.l_set_to_false(carry_out); // enforce no overflow
454}
455
456bvt bv_utilst::shift(const bvt &op, const shiftt s, const bvt &dist)
457{
458 std::size_t d=1, width=op.size();
459 bvt result=op;
460
461 for(std::size_t stage=0; stage<dist.size(); stage++)
462 {
463 if(dist[stage]!=const_literal(false))
464 {
465 bvt tmp=shift(result, s, d);
466
467 for(std::size_t i=0; i<width; i++)
468 result[i]=prop.lselect(dist[stage], tmp[i], result[i]);
469 }
470
471 d=d<<1;
472 }
473
474 return result;
475}
476
477bvt bv_utilst::shift(const bvt &src, const shiftt s, std::size_t dist)
478{
479 bvt result;
480 result.resize(src.size());
481
482 // 'dist' is user-controlled, and thus arbitary.
483 // We thus must guard against the case in which i+dist overflows.
484 // We do so by considering the case dist>=src.size().
485
486 for(std::size_t i=0; i<src.size(); i++)
487 {
488 literalt l;
489
490 switch(s)
491 {
493 // no underflow on i-dist because of condition dist<=i
494 l=(dist<=i?src[i-dist]:const_literal(false));
495 break;
496
498 // src.size()-i won't underflow as i<src.size()
499 // Then, if dist<src.size()-i, then i+dist<src.size()
500 l=(dist<src.size()-i?src[i+dist]:src[src.size()-1]); // sign bit
501 break;
502
504 // src.size()-i won't underflow as i<src.size()
505 // Then, if dist<src.size()-i, then i+dist<src.size()
506 l=(dist<src.size()-i?src[i+dist]:const_literal(false));
507 break;
508
510 // prevent overflows by using dist%src.size()
511 l=src[(src.size()+i-(dist%src.size()))%src.size()];
512 break;
513
515 // prevent overflows by using dist%src.size()
516 l=src[(i+(dist%src.size()))%src.size()];
517 break;
518
519 default:
521 }
522
523 result[i]=l;
524 }
525
526 return result;
527}
528
530{
531 bvt result=inverted(bv);
533 incrementer(result, const_literal(true), carry_out);
534 return result;
535}
536
538{
540 return negate(bv);
541}
542
544{
545 // a overflow on unary- can only happen with the smallest
546 // representable number 100....0
547
548 bvt zeros(bv);
549 zeros.erase(--zeros.end());
550
551 return prop.land(bv[bv.size()-1], !prop.lor(zeros));
552}
553
555 bvt &bv,
556 literalt carry_in,
557 literalt &carry_out)
558{
559 carry_out=carry_in;
560
561 for(auto &literal : bv)
562 {
563 literalt new_carry = prop.land(carry_out, literal);
564 literal = prop.lxor(literal, carry_out);
565 carry_out=new_carry;
566 }
567}
568
570{
571 bvt result=bv;
573 incrementer(result, carry_in, carry_out);
574 return result;
575}
576
578{
579 bvt result=bv;
580 for(auto &literal : result)
581 literal = !literal;
582 return result;
583}
584
585bvt bv_utilst::wallace_tree(const std::vector<bvt> &pps)
586{
587 PRECONDITION(!pps.empty());
588
589 if(pps.size()==1)
590 return pps.front();
591 else if(pps.size()==2)
592 return add(pps[0], pps[1]);
593 else
594 {
595 std::vector<bvt> new_pps;
596 std::size_t no_full_adders=pps.size()/3;
597
598 // add groups of three partial products using CSA
599 for(std::size_t i=0; i<no_full_adders; i++)
600 {
601 const bvt &a=pps[i*3+0],
602 &b=pps[i*3+1],
603 &c=pps[i*3+2];
604
605 INVARIANT(a.size() == b.size(), "groups should be of equal size");
606 INVARIANT(a.size() == c.size(), "groups should be of equal size");
607
608 bvt s(a.size()), t(a.size());
609
610 for(std::size_t bit=0; bit<a.size(); bit++)
611 {
612 // \todo reformulate using full_adder
613 s[bit]=prop.lxor(a[bit], prop.lxor(b[bit], c[bit]));
614 t[bit]=(bit==0)?const_literal(false):
615 carry(a[bit-1], b[bit-1], c[bit-1]);
616 }
617
618 new_pps.push_back(s);
619 new_pps.push_back(t);
620 }
621
622 // pass onwards up to two remaining partial products
623 for(std::size_t i=no_full_adders*3; i<pps.size(); i++)
624 new_pps.push_back(pps[i]);
625
626 POSTCONDITION(new_pps.size() < pps.size());
627 return wallace_tree(new_pps);
628 }
629}
630
631bvt bv_utilst::unsigned_multiplier(const bvt &_op0, const bvt &_op1)
632{
633 #if 1
634 bvt op0=_op0, op1=_op1;
635
636 if(is_constant(op1))
637 std::swap(op0, op1);
638
639 bvt product;
640 product.resize(op0.size());
641
642 for(std::size_t i=0; i<product.size(); i++)
643 product[i]=const_literal(false);
644
645 for(std::size_t sum=0; sum<op0.size(); sum++)
646 if(op0[sum]!=const_literal(false))
647 {
648 bvt tmpop;
649
650 tmpop.reserve(op0.size());
651
652 for(std::size_t idx=0; idx<sum; idx++)
653 tmpop.push_back(const_literal(false));
654
655 for(std::size_t idx=sum; idx<op0.size(); idx++)
656 tmpop.push_back(prop.land(op1[idx-sum], op0[sum]));
657
658 product=add(product, tmpop);
659 }
660
661 return product;
662 #else
663 // Wallace tree multiplier. This is disabled, as runtimes have
664 // been observed to go up by 5%-10%, and on some models even by 20%.
665
666 // build the usual quadratic number of partial products
667
668 bvt op0=_op0, op1=_op1;
669
670 if(is_constant(op1))
671 std::swap(op0, op1);
672
673 std::vector<bvt> pps;
674 pps.reserve(op0.size());
675
676 for(std::size_t bit=0; bit<op0.size(); bit++)
677 if(op0[bit]!=const_literal(false))
678 {
679 bvt pp;
680
681 pp.reserve(op0.size());
682
683 // zeros according to weight
684 for(std::size_t idx=0; idx<bit; idx++)
685 pp.push_back(const_literal(false));
686
687 for(std::size_t idx=bit; idx<op0.size(); idx++)
688 pp.push_back(prop.land(op1[idx-bit], op0[bit]));
689
690 pps.push_back(pp);
691 }
692
693 if(pps.empty())
694 return zeros(op0.size());
695 else
696 return wallace_tree(pps);
697
698 #endif
699}
700
702 const bvt &op0,
703 const bvt &op1)
704{
705 bvt _op0=op0, _op1=op1;
706
707 PRECONDITION(_op0.size() == _op1.size());
708
709 if(is_constant(_op1))
710 _op0.swap(_op1);
711
712 bvt product;
713 product.resize(_op0.size());
714
715 for(std::size_t i=0; i<product.size(); i++)
716 product[i]=const_literal(false);
717
718 for(std::size_t sum=0; sum<op0.size(); sum++)
719 if(op0[sum]!=const_literal(false))
720 {
721 bvt tmpop;
722
723 tmpop.reserve(product.size());
724
725 for(std::size_t idx=0; idx<sum; idx++)
726 tmpop.push_back(const_literal(false));
727
728 for(std::size_t idx=sum; idx<product.size(); idx++)
729 tmpop.push_back(prop.land(op1[idx-sum], op0[sum]));
730
731 adder_no_overflow(product, tmpop);
732
733 for(std::size_t idx=op1.size()-sum; idx<op1.size(); idx++)
734 prop.l_set_to_false(prop.land(op1[idx], op0[sum]));
735 }
736
737 return product;
738}
739
741{
742 if(op0.empty() || op1.empty())
743 return bvt();
744
745 literalt sign0=op0[op0.size()-1];
746 literalt sign1=op1[op1.size()-1];
747
748 bvt neg0=cond_negate(op0, sign0);
749 bvt neg1=cond_negate(op1, sign1);
750
751 bvt result=unsigned_multiplier(neg0, neg1);
752
753 literalt result_sign=prop.lxor(sign0, sign1);
754
755 return cond_negate(result, result_sign);
756}
757
759{
760 bvt neg_bv=negate(bv);
761
762 bvt result;
763 result.resize(bv.size());
764
765 for(std::size_t i=0; i<bv.size(); i++)
766 result[i]=prop.lselect(cond, neg_bv[i], bv[i]);
767
768 return result;
769}
770
772{
773 PRECONDITION(!bv.empty());
774 return cond_negate(bv, bv[bv.size()-1]);
775}
776
778{
780
781 return cond_negate(bv, cond);
782}
783
785 const bvt &op0,
786 const bvt &op1)
787{
788 if(op0.empty() || op1.empty())
789 return bvt();
790
791 literalt sign0=op0[op0.size()-1];
792 literalt sign1=op1[op1.size()-1];
793
794 bvt neg0=cond_negate_no_overflow(op0, sign0);
795 bvt neg1=cond_negate_no_overflow(op1, sign1);
796
797 bvt result=unsigned_multiplier_no_overflow(neg0, neg1);
798
799 prop.l_set_to_false(result[result.size() - 1]);
800
801 literalt result_sign=prop.lxor(sign0, sign1);
802
803 return cond_negate_no_overflow(result, result_sign);
804}
805
807 const bvt &op0,
808 const bvt &op1,
809 representationt rep)
810{
811 switch(rep)
812 {
813 case representationt::SIGNED: return signed_multiplier(op0, op1);
814 case representationt::UNSIGNED: return unsigned_multiplier(op0, op1);
815 }
816
818}
819
821 const bvt &op0,
822 const bvt &op1,
823 representationt rep)
824{
825 switch(rep)
826 {
828 return signed_multiplier_no_overflow(op0, op1);
830 return unsigned_multiplier_no_overflow(op0, op1);
831 }
832
834}
835
837 const bvt &op0,
838 const bvt &op1,
839 bvt &res,
840 bvt &rem)
841{
842 if(op0.empty() || op1.empty())
843 return;
844
845 bvt _op0(op0), _op1(op1);
846
847 literalt sign_0=_op0[_op0.size()-1];
848 literalt sign_1=_op1[_op1.size()-1];
849
850 bvt neg_0=negate(_op0), neg_1=negate(_op1);
851
852 for(std::size_t i=0; i<_op0.size(); i++)
853 _op0[i]=(prop.lselect(sign_0, neg_0[i], _op0[i]));
854
855 for(std::size_t i=0; i<_op1.size(); i++)
856 _op1[i]=(prop.lselect(sign_1, neg_1[i], _op1[i]));
857
858 unsigned_divider(_op0, _op1, res, rem);
859
860 bvt neg_res=negate(res), neg_rem=negate(rem);
861
862 literalt result_sign=prop.lxor(sign_0, sign_1);
863
864 for(std::size_t i=0; i<res.size(); i++)
865 res[i]=prop.lselect(result_sign, neg_res[i], res[i]);
866
867 for(std::size_t i=0; i<res.size(); i++)
868 rem[i]=prop.lselect(sign_0, neg_rem[i], rem[i]);
869}
870
872 const bvt &op0,
873 const bvt &op1,
874 bvt &result,
875 bvt &remainer,
876 representationt rep)
877{
879
880 switch(rep)
881 {
883 signed_divider(op0, op1, result, remainer); break;
885 unsigned_divider(op0, op1, result, remainer); break;
886 }
887}
888
890 const bvt &op0,
891 const bvt &op1,
892 bvt &res,
893 bvt &rem)
894{
895 std::size_t width=op0.size();
896
897 // check if we divide by a power of two
898 #if 0
899 {
900 std::size_t one_count=0, non_const_count=0, one_pos=0;
901
902 for(std::size_t i=0; i<op1.size(); i++)
903 {
904 literalt l=op1[i];
905 if(l.is_true())
906 {
907 one_count++;
908 one_pos=i;
909 }
910 else if(!l.is_false())
911 non_const_count++;
912 }
913
914 if(non_const_count==0 && one_count==1 && one_pos!=0)
915 {
916 // it is a power of two!
917 res=shift(op0, LRIGHT, one_pos);
918
919 // remainder is just a mask
920 rem=op0;
921 for(std::size_t i=one_pos; i<rem.size(); i++)
922 rem[i]=const_literal(false);
923 return;
924 }
925 }
926 #endif
927
928 // Division by zero test.
929 // Note that we produce a non-deterministic result in
930 // case of division by zero. SMT-LIB now says the following:
931 // bvudiv returns a vector of all 1s if the second operand is 0
932 // bvurem returns its first operand if the second operand is 0
933
935
936 // free variables for result of division
937 res = prop.new_variables(width);
938 rem = prop.new_variables(width);
939
940 // add implications
941
942 bvt product=
944
945 // res*op1 + rem = op0
946
947 bvt sum=product;
948
949 adder_no_overflow(sum, rem);
950
951 literalt is_equal=equal(sum, op0);
952
954
955 // op1!=0 => rem < op1
956
960
961 // op1!=0 => res <= op0
962
966}
967
968
969#ifdef COMPACT_EQUAL_CONST
970// TODO : use for lt_or_le as well
971
975void bv_utilst::equal_const_register(const bvt &var)
976{
978 equal_const_registered.insert(var);
979 return;
980}
981
988literalt bv_utilst::equal_const_rec(bvt &var, bvt &constant)
989{
990 std::size_t size = var.size();
991
992 PRECONDITION(size != 0);
993 PRECONDITION(size == constant.size());
994 PRECONDITION(is_constant(constant));
995
996 if(size == 1)
997 {
998 literalt comp = prop.lequal(var[size - 1], constant[size - 1]);
999 var.pop_back();
1000 constant.pop_back();
1001 return comp;
1002 }
1003 else
1004 {
1005 var_constant_pairt index(var, constant);
1006
1007 equal_const_cachet::iterator entry = equal_const_cache.find(index);
1008
1009 if(entry != equal_const_cache.end())
1010 {
1011 return entry->second;
1012 }
1013 else
1014 {
1015 literalt comp = prop.lequal(var[size - 1], constant[size - 1]);
1016 var.pop_back();
1017 constant.pop_back();
1018
1019 literalt rec = equal_const_rec(var, constant);
1020 literalt compare = prop.land(rec, comp);
1021
1022 equal_const_cache.insert(
1023 std::pair<var_constant_pairt, literalt>(index, compare));
1024
1025 return compare;
1026 }
1027 }
1028}
1029
1038literalt bv_utilst::equal_const(const bvt &var, const bvt &constant)
1039{
1040 std::size_t size = constant.size();
1041
1042 PRECONDITION(var.size() == size);
1044 PRECONDITION(is_constant(constant));
1045 PRECONDITION(size >= 2);
1046
1047 // These get modified : be careful!
1048 bvt var_upper;
1049 bvt var_lower;
1050 bvt constant_upper;
1051 bvt constant_lower;
1052
1053 /* Split the constant based on a change in parity
1054 * This is based on the observation that most constants are small,
1055 * so combinations of the lower bits are heavily used but the upper
1056 * bits are almost always either all 0 or all 1.
1057 */
1058 literalt top_bit = constant[size - 1];
1059
1060 std::size_t split = size - 1;
1061 var_upper.push_back(var[size - 1]);
1062 constant_upper.push_back(constant[size - 1]);
1063
1064 for(split = size - 2; split != 0; --split)
1065 {
1066 if(constant[split] != top_bit)
1067 {
1068 break;
1069 }
1070 else
1071 {
1072 var_upper.push_back(var[split]);
1073 constant_upper.push_back(constant[split]);
1074 }
1075 }
1076
1077 for(std::size_t i = 0; i <= split; ++i)
1078 {
1079 var_lower.push_back(var[i]);
1080 constant_lower.push_back(constant[i]);
1081 }
1082
1083 // Check we have split the array correctly
1084 INVARIANT(
1085 var_upper.size() + var_lower.size() == size,
1086 "lower size plus upper size should equal the total size");
1087 INVARIANT(
1088 constant_upper.size() + constant_lower.size() == size,
1089 "lower size plus upper size should equal the total size");
1090
1091 literalt top_comparison = equal_const_rec(var_upper, constant_upper);
1092 literalt bottom_comparison = equal_const_rec(var_lower, constant_lower);
1093
1094 return prop.land(top_comparison, bottom_comparison);
1095}
1096
1097#endif
1098
1103literalt bv_utilst::equal(const bvt &op0, const bvt &op1)
1104{
1105 PRECONDITION(op0.size() == op1.size());
1106
1107 #ifdef COMPACT_EQUAL_CONST
1108 // simplify_expr should put the constant on the right
1109 // but bit-level simplification may result in the other cases
1110 if(is_constant(op0) && !is_constant(op1) && op0.size() > 2 &&
1111 equal_const_registered.find(op1) != equal_const_registered.end())
1112 return equal_const(op1, op0);
1113 else if(!is_constant(op0) && is_constant(op1) && op0.size() > 2 &&
1114 equal_const_registered.find(op0) != equal_const_registered.end())
1115 return equal_const(op0, op1);
1116 #endif
1117
1118 bvt equal_bv;
1119 equal_bv.resize(op0.size());
1120
1121 for(std::size_t i=0; i<op0.size(); i++)
1122 equal_bv[i]=prop.lequal(op0[i], op1[i]);
1123
1124 return prop.land(equal_bv);
1125}
1126
1131/* Some clauses are not needed for correctness but they remove
1132 models (effectively setting "don't care" bits) and so may be worth
1133 including.*/
1134// #define INCLUDE_REDUNDANT_CLAUSES
1135
1136// Saves space but slows the solver
1137// There is a variant that uses the xor as an auxiliary that should improve both
1138// #define COMPACT_LT_OR_LE
1139
1140
1141
1143 bool or_equal,
1144 const bvt &bv0,
1145 const bvt &bv1,
1146 representationt rep)
1147{
1148 PRECONDITION(bv0.size() == bv1.size());
1149
1150 literalt top0=bv0[bv0.size()-1],
1151 top1=bv1[bv1.size()-1];
1152
1153#ifdef COMPACT_LT_OR_LE
1155 {
1156 bvt compareBelow; // 1 if a compare is needed below this bit
1157 literalt result;
1158 size_t start;
1159 size_t i;
1160
1161 compareBelow = prop.new_variables(bv0.size());
1162 result = prop.new_variable();
1163
1164 if(rep==SIGNED)
1165 {
1166 INVARIANT(
1167 bv0.size() >= 2, "signed bitvectors should have at least two bits");
1168 start = compareBelow.size() - 2;
1169
1170 literalt firstComp=compareBelow[start];
1171
1172 // When comparing signs we are comparing the top bit
1173#ifdef INCLUDE_REDUNDANT_CLAUSES
1174 prop.l_set_to_true(compareBelow[start + 1])
1175#endif
1176
1177 // Four cases...
1178 prop.lcnf(top0, top1, firstComp); // + + compare needed
1179 prop.lcnf(top0, !top1, !result); // + - result false and no compare needed
1180 prop.lcnf(!top0, top1, result); // - + result true and no compare needed
1181 prop.lcnf(!top0, !top1, firstComp); // - - negated compare needed
1182
1183#ifdef INCLUDE_REDUNDANT_CLAUSES
1184 prop.lcnf(top0, !top1, !firstComp);
1185 prop.lcnf(!top0, top1, !firstComp);
1186#endif
1187 }
1188 else
1189 {
1190 // Unsigned is much easier
1191 start = compareBelow.size() - 1;
1192 prop.l_set_to_true(compareBelow[start]);
1193 }
1194
1195 // Determine the output
1196 // \forall i . cb[i] & -a[i] & b[i] => result
1197 // \forall i . cb[i] & a[i] & -b[i] => -result
1198 i = start;
1199 do
1200 {
1201 prop.lcnf(!compareBelow[i], bv0[i], !bv1[i], result);
1202 prop.lcnf(!compareBelow[i], !bv0[i], bv1[i], !result);
1203 }
1204 while(i-- != 0);
1205
1206 // Chain the comparison bit
1207 // \forall i != 0 . cb[i] & a[i] & b[i] => cb[i-1]
1208 // \forall i != 0 . cb[i] & -a[i] & -b[i] => cb[i-1]
1209 for(i = start; i > 0; i--)
1210 {
1211 prop.lcnf(!compareBelow[i], !bv0[i], !bv1[i], compareBelow[i-1]);
1212 prop.lcnf(!compareBelow[i], bv0[i], bv1[i], compareBelow[i-1]);
1213 }
1214
1215
1216#ifdef INCLUDE_REDUNDANT_CLAUSES
1217 // Optional zeroing of the comparison bit when not needed
1218 // \forall i != 0 . -c[i] => -c[i-1]
1219 // \forall i != 0 . c[i] & -a[i] & b[i] => -c[i-1]
1220 // \forall i != 0 . c[i] & a[i] & -b[i] => -c[i-1]
1221 for(i = start; i > 0; i--)
1222 {
1223 prop.lcnf(compareBelow[i], !compareBelow[i-1]);
1224 prop.lcnf(!compareBelow[i], bv0[i], !bv1[i], !compareBelow[i-1]);
1225 prop.lcnf(!compareBelow[i], !bv0[i], bv1[i], !compareBelow[i-1]);
1226 }
1227#endif
1228
1229 // The 'base case' of the induction is the case when they are equal
1230 prop.lcnf(!compareBelow[0], !bv0[0], !bv1[0], (or_equal)?result:!result);
1231 prop.lcnf(!compareBelow[0], bv0[0], bv1[0], (or_equal)?result:!result);
1232
1233 return result;
1234 }
1235 else
1236#endif
1237 {
1239 carry_out(bv0, inverted(bv1), const_literal(true));
1240
1241 literalt result;
1242
1244 result=prop.lxor(prop.lequal(top0, top1), carry);
1245 else
1246 {
1247 INVARIANT(
1249 "representation has either value signed or unsigned");
1250 result = !carry;
1251 }
1252
1253 if(or_equal)
1254 result=prop.lor(result, equal(bv0, bv1));
1255
1256 return result;
1257 }
1258}
1259
1261 const bvt &op0,
1262 const bvt &op1)
1263{
1264#ifdef COMPACT_LT_OR_LE
1265 return lt_or_le(false, op0, op1, UNSIGNED);
1266#else
1267 // A <= B iff there is an overflow on A-B
1268 return !carry_out(op0, inverted(op1), const_literal(true));
1269#endif
1270}
1271
1273 const bvt &bv0,
1274 const bvt &bv1)
1275{
1276 return lt_or_le(false, bv0, bv1, representationt::SIGNED);
1277}
1278
1280 const bvt &bv0,
1281 irep_idt id,
1282 const bvt &bv1,
1283 representationt rep)
1284{
1285 if(id==ID_equal)
1286 return equal(bv0, bv1);
1287 else if(id==ID_notequal)
1288 return !equal(bv0, bv1);
1289 else if(id==ID_le)
1290 return lt_or_le(true, bv0, bv1, rep);
1291 else if(id==ID_lt)
1292 return lt_or_le(false, bv0, bv1, rep);
1293 else if(id==ID_ge)
1294 return lt_or_le(true, bv1, bv0, rep); // swapped
1295 else if(id==ID_gt)
1296 return lt_or_le(false, bv1, bv0, rep); // swapped
1297 else
1299}
1300
1302{
1303 for(const auto &literal : bv)
1304 {
1305 if(!literal.is_constant())
1306 return false;
1307 }
1308
1309 return true;
1310}
1311
1313 literalt cond,
1314 const bvt &a,
1315 const bvt &b)
1316{
1317 PRECONDITION(a.size() == b.size());
1318
1320 {
1321 for(std::size_t i=0; i<a.size(); i++)
1322 {
1323 prop.lcnf(!cond, a[i], !b[i]);
1324 prop.lcnf(!cond, !a[i], b[i]);
1325 }
1326 }
1327 else
1328 {
1329 prop.limplies(cond, equal(a, b));
1330 }
1331
1332 return;
1333}
1334
1336{
1337 bvt odd_bits;
1338 odd_bits.reserve(src.size()/2);
1339
1340 // check every odd bit
1341 for(std::size_t i=0; i<src.size(); i++)
1342 {
1343 if(i%2!=0)
1344 odd_bits.push_back(src[i]);
1345 }
1346
1347 return prop.lor(odd_bits);
1348}
1349
1351{
1352 bvt even_bits;
1353 even_bits.reserve(src.size()/2);
1354
1355 // get every even bit
1356 for(std::size_t i=0; i<src.size(); i++)
1357 {
1358 if(i%2==0)
1359 even_bits.push_back(src[i]);
1360 }
1361
1362 return even_bits;
1363}
static bvt inverted(const bvt &op)
Definition bv_utils.cpp:577
literalt signed_less_than(const bvt &bv0, const bvt &bv1)
void adder_no_overflow(bvt &sum, const bvt &op, bool subtract, representationt rep)
Definition bv_utils.cpp:412
static bool is_constant(const bvt &bv)
bvt wallace_tree(const std::vector< bvt > &pps)
Definition bv_utils.cpp:585
literalt is_not_zero(const bvt &op)
Definition bv_utils.h:141
static bvt verilog_bv_normal_bits(const bvt &)
literalt is_int_min(const bvt &op)
Definition bv_utils.h:144
static bvt extract_msb(const bvt &a, std::size_t n)
Definition bv_utils.cpp:54
void set_equal(const bvt &a, const bvt &b)
Definition bv_utils.cpp:31
bvt multiplier_no_overflow(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.cpp:820
bvt add_sub_no_overflow(const bvt &op0, const bvt &op1, bool subtract, representationt rep)
Definition bv_utils.cpp:324
bvt add(const bvt &op0, const bvt &op1)
Definition bv_utils.h:61
void adder(bvt &sum, const bvt &op, literalt carry_in, literalt &carry_out)
Definition bv_utils.cpp:293
bvt absolute_value(const bvt &op)
Definition bv_utils.cpp:771
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
Definition bv_utils.cpp:92
static bvt build_constant(const mp_integer &i, std::size_t width)
Definition bv_utils.cpp:11
void signed_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
Definition bv_utils.cpp:836
literalt is_zero(const bvt &op)
Definition bv_utils.h:138
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)
Definition bv_utils.cpp:740
literalt overflow_add(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.cpp:363
literalt is_one(const bvt &op)
Definition bv_utils.cpp:22
bvt cond_negate_no_overflow(const bvt &bv, const literalt cond)
Definition bv_utils.cpp:777
literalt overflow_sub(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.cpp:387
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)
Definition bv_utils.cpp:784
bvt incrementer(const bvt &op, literalt carry_in)
Definition bv_utils.cpp:569
bvt add_sub(const bvt &op0, const bvt &op1, bool subtract)
Definition bv_utils.cpp:335
static bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
Definition bv_utils.cpp:477
literalt lt_or_le(bool or_equal, const bvt &bv0, const bvt &bv1, representationt rep)
To provide a bitwise model of < or <=.
literalt overflow_negate(const bvt &op)
Definition bv_utils.cpp:543
static bvt concatenate(const bvt &a, const bvt &b)
Definition bv_utils.cpp:76
representationt
Definition bv_utils.h:28
literalt full_adder(const literalt a, const literalt b, const literalt carry_in, literalt &carry_out)
Definition bv_utils.cpp:136
bvt negate_no_overflow(const bvt &op)
Definition bv_utils.cpp:537
static bvt extract(const bvt &a, std::size_t first, std::size_t last)
Definition bv_utils.cpp:38
bvt unsigned_multiplier(const bvt &op0, const bvt &op1)
Definition bv_utils.cpp:631
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.h:84
void unsigned_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
Definition bv_utils.cpp:889
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.cpp:806
bvt cond_negate(const bvt &bv, const literalt cond)
Definition bv_utils.cpp:758
literalt carry_out(const bvt &op0, const bvt &op1, literalt carry_in)
Definition bv_utils.cpp:309
bvt negate(const bvt &op)
Definition bv_utils.cpp:529
static bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
Definition bv_utils.cpp:105
static bvt extract_lsb(const bvt &a, std::size_t n)
Definition bv_utils.cpp:66
literalt verilog_bv_has_x_or_z(const bvt &)
literalt carry(literalt a, literalt b, literalt c)
Definition bv_utils.cpp:227
bvt unsigned_multiplier_no_overflow(const bvt &op0, const bvt &op1)
Definition bv_utils.cpp:701
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
propt & prop
Definition bv_utils.h:219
bvt zeros(std::size_t new_size) const
Definition bv_utils.h:187
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
bool is_true() const
Definition literal.h:156
bool is_constant() const
Definition literal.h:166
bool is_false() const
Definition literal.h:161
void l_set_to_true(literalt a)
Definition prop.h:51
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:84
virtual void l_set_to(literalt a, bool value)
Definition prop.h:46
virtual literalt lxor(literalt a, literalt b)=0
void lcnf(literalt l0, literalt l1)
Definition prop.h:57
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:20
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:53
virtual bool has_set_to() const
Definition prop.h:80
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
BigInt mp_integer
Definition smt_terms.h:12
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:503
#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