cprover
bv_utils.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "bv_utils.h"
10 
11 bvt 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 
31 void 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 
38 bvt 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 
54 bvt 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 
66 bvt 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 
76 bvt 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 
92 bvt 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 
335 bvt 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 
350 bvt 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 {
366  if(rep==representationt::SIGNED)
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
384  UNREACHABLE;
385 }
386 
388  const bvt &op0, const bvt &op1, representationt rep)
389 {
390  if(rep==representationt::SIGNED)
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
409  UNREACHABLE;
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 
420  if(rep==representationt::SIGNED)
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 
429  literalt carry;
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 
447 void bv_utilst::adder_no_overflow(bvt &sum, const bvt &op)
448 {
450 
451  adder(sum, op, carry_out, carry_out);
452 
453  prop.l_set_to_false(carry_out); // enforce no overflow
454 }
455 
456 bvt 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 
477 bvt 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  {
492  case shiftt::SHIFT_LEFT:
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 
509  case shiftt::ROTATE_LEFT:
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:
520  UNREACHABLE;
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 
585 bvt 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 
631 bvt 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 
740 bvt bv_utilst::signed_multiplier(const bvt &op0, const bvt &op1)
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 
758 bvt bv_utilst::cond_negate(const bvt &bv, const literalt cond)
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 
817  UNREACHABLE;
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 
833  UNREACHABLE;
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 
958  prop.limplies(
959  is_not_zero, lt_or_le(false, rem, op1, representationt::UNSIGNED)));
960 
961  // op1!=0 => res <= op0
962 
964  prop.limplies(
965  is_not_zero, lt_or_le(true, res, op0, representationt::UNSIGNED)));
966 }
967 
968 
969 #ifdef COMPACT_EQUAL_CONST
970 // TODO : use for lt_or_le as well
971 
975 void bv_utilst::equal_const_register(const bvt &var)
976 {
977  PRECONDITION(!is_constant(var));
978  equal_const_registered.insert(var);
979  return;
980 }
981 
988 literalt 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 
1038 literalt bv_utilst::equal_const(const bvt &var, const bvt &constant)
1039 {
1040  std::size_t size = constant.size();
1041 
1042  PRECONDITION(var.size() == size);
1043  PRECONDITION(!is_constant(var));
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 
1103 literalt 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  {
1238  literalt carry=
1239  carry_out(bv0, inverted(bv1), const_literal(true));
1240 
1241  literalt result;
1242 
1243  if(rep==representationt::SIGNED)
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
1298  UNREACHABLE;
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 
1319  if(prop.cnf_handled_well())
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)
Definition: bv_utils.cpp:1272
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)
Definition: bv_utils.cpp:1301
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 &)
Definition: bv_utils.cpp:1350
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.
Definition: bv_utils.cpp:1103
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)
Definition: bv_utils.cpp:1312
literalt unsigned_less_than(const bvt &bv0, const bvt &bv1)
Definition: bv_utils.cpp:1260
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 <=.
Definition: bv_utils.cpp:1142
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 &)
Definition: bv_utils.cpp:1335
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)
Definition: bv_utils.cpp:1279
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:50
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:83
virtual void l_set_to(literalt a, bool value)
Definition: prop.h:45
virtual literalt lxor(literalt a, literalt b)=0
void lcnf(literalt l0, literalt l1)
Definition: prop.h:56
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:52
virtual bool has_set_to() const
Definition: prop.h:79
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 POSTCONDITION(CONDITION)
Definition: invariant.h:479