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 #include <util/arith_tools.h>
12 
13 bvt 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 
33 void 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 
40 bvt 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 
56 bvt 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 
68 bvt 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 
78 bvt bv_utilst::concatenate(const bvt &a, const bvt &b)
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 
94 bvt bv_utilst::select(literalt s, const bvt &a, const bvt &b)
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();
113  PRECONDITION(old_size != 0);
114 
115  bvt result=bv;
116  result.resize(new_size);
117 
118  literalt extend_with=
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 
170  literalt sum;
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  {
188  sum = prop.new_variable();
189 
190  // Any two inputs 1 will set the carry_out to 1
191  prop.lcnf(!a, !b, carry_out);
192  prop.lcnf(!a, !carry_in, carry_out);
193  prop.lcnf(!b, !carry_in, carry_out);
194 
195  // Any two inputs 0 will set the carry_out to 0
196  prop.lcnf(a, b, !carry_out);
197  prop.lcnf(a, carry_in, !carry_out);
198  prop.lcnf(b, carry_in, !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);
203  prop.lcnf(carry_in, !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);
208  prop.lcnf(!carry_in, 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
221  carry_out=carry(a, b, carry_in);
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 
296  bvt &sum,
297  const bvt &op,
298  literalt carry_in,
299  literalt &carry_out)
300 {
301  PRECONDITION(sum.size() == op.size());
302 
303  carry_out=carry_in;
304 
305  for(std::size_t i=0; i<sum.size(); i++)
306  {
307  sum[i] = full_adder(sum[i], op[i], carry_out, carry_out);
308  }
309 }
310 
312  const bvt &op0,
313  const bvt &op1,
314  literalt carry_in)
315 {
316  PRECONDITION(op0.size() == op1.size());
317 
318  literalt carry_out=carry_in;
319 
320  for(std::size_t i=0; i<op0.size(); i++)
321  carry_out=carry(op0[i], op1[i], carry_out);
322 
323  return carry_out;
324 }
325 
327  const bvt &op0,
328  const bvt &op1,
329  bool subtract,
330  representationt rep)
331 {
332  bvt sum=op0;
333  adder_no_overflow(sum, op1, subtract, rep);
334  return sum;
335 }
336 
337 bvt bv_utilst::add_sub(const bvt &op0, const bvt &op1, bool subtract)
338 {
339  PRECONDITION(op0.size() == op1.size());
340 
341  literalt carry_in=const_literal(subtract);
343 
344  bvt result=op0;
345  bvt tmp_op1=subtract?inverted(op1):op1;
346 
347  adder(result, tmp_op1, carry_in, carry_out);
348 
349  return result;
350 }
351 
352 bvt bv_utilst::add_sub(const bvt &op0, const bvt &op1, literalt subtract)
353 {
354  const bvt op1_sign_applied=
355  select(subtract, inverted(op1), op1);
356 
357  bvt result=op0;
359 
360  adder(result, op1_sign_applied, subtract, carry_out);
361 
362  return result;
363 }
364 
366  const bvt &op0, const bvt &op1, representationt rep)
367 {
368  if(rep==representationt::SIGNED)
369  {
370  // An overflow occurs if the signs of the two operands are the same
371  // and the sign of the sum is the opposite.
372 
373  literalt old_sign=op0[op0.size()-1];
374  literalt sign_the_same=prop.lequal(op0[op0.size()-1], op1[op1.size()-1]);
375 
376  bvt result=add(op0, op1);
377  return
378  prop.land(sign_the_same, prop.lxor(result[result.size()-1], old_sign));
379  }
380  else if(rep==representationt::UNSIGNED)
381  {
382  // overflow is simply carry-out
383  return carry_out(op0, op1, const_literal(false));
384  }
385  else
386  UNREACHABLE;
387 }
388 
390  const bvt &op0, const bvt &op1, representationt rep)
391 {
392  if(rep==representationt::SIGNED)
393  {
394  // We special-case x-INT_MIN, which is >=0 if
395  // x is negative, always representable, and
396  // thus not an overflow.
397  literalt op1_is_int_min=is_int_min(op1);
398  literalt op0_is_negative=op0[op0.size()-1];
399 
400  return
401  prop.lselect(op1_is_int_min,
402  !op0_is_negative,
404  }
405  else if(rep==representationt::UNSIGNED)
406  {
407  // overflow is simply _negated_ carry-out
408  return !carry_out(op0, inverted(op1), const_literal(true));
409  }
410  else
411  UNREACHABLE;
412 }
413 
415  bvt &sum,
416  const bvt &op,
417  bool subtract,
418  representationt rep)
419 {
420  const bvt tmp_op=subtract?inverted(op):op;
421 
422  if(rep==representationt::SIGNED)
423  {
424  // an overflow occurs if the signs of the two operands are the same
425  // and the sign of the sum is the opposite
426 
427  literalt old_sign=sum[sum.size()-1];
428  literalt sign_the_same=
429  prop.lequal(sum[sum.size()-1], tmp_op[tmp_op.size()-1]);
430 
431  literalt carry;
432  adder(sum, tmp_op, const_literal(subtract), carry);
433 
434  // result of addition in sum
436  prop.land(sign_the_same, prop.lxor(sum[sum.size()-1], old_sign)));
437  }
438  else
439  {
440  INVARIANT(
442  "representation has either value signed or unsigned");
444  adder(sum, tmp_op, const_literal(subtract), carry_out);
445  prop.l_set_to(carry_out, subtract);
446  }
447 }
448 
449 void bv_utilst::adder_no_overflow(bvt &sum, const bvt &op)
450 {
452 
453  adder(sum, op, carry_out, carry_out);
454 
455  prop.l_set_to_false(carry_out); // enforce no overflow
456 }
457 
458 bvt bv_utilst::shift(const bvt &op, const shiftt s, const bvt &dist)
459 {
460  std::size_t d=1, width=op.size();
461  bvt result=op;
462 
463  for(std::size_t stage=0; stage<dist.size(); stage++)
464  {
465  if(dist[stage]!=const_literal(false))
466  {
467  bvt tmp=shift(result, s, d);
468 
469  for(std::size_t i=0; i<width; i++)
470  result[i]=prop.lselect(dist[stage], tmp[i], result[i]);
471  }
472 
473  d=d<<1;
474  }
475 
476  return result;
477 }
478 
479 bvt bv_utilst::shift(const bvt &src, const shiftt s, std::size_t dist)
480 {
481  bvt result;
482  result.resize(src.size());
483 
484  // 'dist' is user-controlled, and thus arbitary.
485  // We thus must guard against the case in which i+dist overflows.
486  // We do so by considering the case dist>=src.size().
487 
488  for(std::size_t i=0; i<src.size(); i++)
489  {
490  literalt l;
491 
492  switch(s)
493  {
494  case shiftt::SHIFT_LEFT:
495  // no underflow on i-dist because of condition dist<=i
496  l=(dist<=i?src[i-dist]:const_literal(false));
497  break;
498 
500  // src.size()-i won't underflow as i<src.size()
501  // Then, if dist<src.size()-i, then i+dist<src.size()
502  l=(dist<src.size()-i?src[i+dist]:src[src.size()-1]); // sign bit
503  break;
504 
506  // src.size()-i won't underflow as i<src.size()
507  // Then, if dist<src.size()-i, then i+dist<src.size()
508  l=(dist<src.size()-i?src[i+dist]:const_literal(false));
509  break;
510 
511  case shiftt::ROTATE_LEFT:
512  // prevent overflows by using dist%src.size()
513  l=src[(src.size()+i-(dist%src.size()))%src.size()];
514  break;
515 
517  // prevent overflows by using dist%src.size()
518  l=src[(i+(dist%src.size()))%src.size()];
519  break;
520 
521  default:
522  UNREACHABLE;
523  }
524 
525  result[i]=l;
526  }
527 
528  return result;
529 }
530 
532 {
533  bvt result=inverted(bv);
535  incrementer(result, const_literal(true), carry_out);
536  return result;
537 }
538 
540 {
542  return negate(bv);
543 }
544 
546 {
547  // a overflow on unary- can only happen with the smallest
548  // representable number 100....0
549 
550  bvt zeros(bv);
551  zeros.erase(--zeros.end());
552 
553  return prop.land(bv[bv.size()-1], !prop.lor(zeros));
554 }
555 
557  bvt &bv,
558  literalt carry_in,
559  literalt &carry_out)
560 {
561  carry_out=carry_in;
562 
563  for(auto &literal : bv)
564  {
565  literalt new_carry = prop.land(carry_out, literal);
566  literal = prop.lxor(literal, carry_out);
567  carry_out=new_carry;
568  }
569 }
570 
572 {
573  bvt result=bv;
575  incrementer(result, carry_in, carry_out);
576  return result;
577 }
578 
580 {
581  bvt result=bv;
582  for(auto &literal : result)
583  literal = !literal;
584  return result;
585 }
586 
587 bvt bv_utilst::wallace_tree(const std::vector<bvt> &pps)
588 {
589  PRECONDITION(!pps.empty());
590 
591  if(pps.size()==1)
592  return pps.front();
593  else if(pps.size()==2)
594  return add(pps[0], pps[1]);
595  else
596  {
597  std::vector<bvt> new_pps;
598  std::size_t no_full_adders=pps.size()/3;
599 
600  // add groups of three partial products using CSA
601  for(std::size_t i=0; i<no_full_adders; i++)
602  {
603  const bvt &a=pps[i*3+0],
604  &b=pps[i*3+1],
605  &c=pps[i*3+2];
606 
607  INVARIANT(a.size() == b.size(), "groups should be of equal size");
608  INVARIANT(a.size() == c.size(), "groups should be of equal size");
609 
610  bvt s(a.size()), t(a.size());
611 
612  for(std::size_t bit=0; bit<a.size(); bit++)
613  {
614  // \todo reformulate using full_adder
615  s[bit]=prop.lxor(a[bit], prop.lxor(b[bit], c[bit]));
616  t[bit]=(bit==0)?const_literal(false):
617  carry(a[bit-1], b[bit-1], c[bit-1]);
618  }
619 
620  new_pps.push_back(s);
621  new_pps.push_back(t);
622  }
623 
624  // pass onwards up to two remaining partial products
625  for(std::size_t i=no_full_adders*3; i<pps.size(); i++)
626  new_pps.push_back(pps[i]);
627 
628  POSTCONDITION(new_pps.size() < pps.size());
629  return wallace_tree(new_pps);
630  }
631 }
632 
633 bvt bv_utilst::unsigned_multiplier(const bvt &_op0, const bvt &_op1)
634 {
635  #if 1
636  bvt op0=_op0, op1=_op1;
637 
638  if(is_constant(op1))
639  std::swap(op0, op1);
640 
641  bvt product;
642  product.resize(op0.size());
643 
644  for(std::size_t i=0; i<product.size(); i++)
645  product[i]=const_literal(false);
646 
647  for(std::size_t sum=0; sum<op0.size(); sum++)
648  if(op0[sum]!=const_literal(false))
649  {
650  bvt tmpop;
651 
652  tmpop.reserve(op0.size());
653 
654  for(std::size_t idx=0; idx<sum; idx++)
655  tmpop.push_back(const_literal(false));
656 
657  for(std::size_t idx=sum; idx<op0.size(); idx++)
658  tmpop.push_back(prop.land(op1[idx-sum], op0[sum]));
659 
660  product=add(product, tmpop);
661  }
662 
663  return product;
664  #else
665  // Wallace tree multiplier. This is disabled, as runtimes have
666  // been observed to go up by 5%-10%, and on some models even by 20%.
667 
668  // build the usual quadratic number of partial products
669 
670  bvt op0=_op0, op1=_op1;
671 
672  if(is_constant(op1))
673  std::swap(op0, op1);
674 
675  std::vector<bvt> pps;
676  pps.reserve(op0.size());
677 
678  for(std::size_t bit=0; bit<op0.size(); bit++)
679  if(op0[bit]!=const_literal(false))
680  {
681  bvt pp;
682 
683  pp.reserve(op0.size());
684 
685  // zeros according to weight
686  for(std::size_t idx=0; idx<bit; idx++)
687  pp.push_back(const_literal(false));
688 
689  for(std::size_t idx=bit; idx<op0.size(); idx++)
690  pp.push_back(prop.land(op1[idx-bit], op0[bit]));
691 
692  pps.push_back(pp);
693  }
694 
695  if(pps.empty())
696  return zeros(op0.size());
697  else
698  return wallace_tree(pps);
699 
700  #endif
701 }
702 
704  const bvt &op0,
705  const bvt &op1)
706 {
707  bvt _op0=op0, _op1=op1;
708 
709  PRECONDITION(_op0.size() == _op1.size());
710 
711  if(is_constant(_op1))
712  _op0.swap(_op1);
713 
714  bvt product;
715  product.resize(_op0.size());
716 
717  for(std::size_t i=0; i<product.size(); i++)
718  product[i]=const_literal(false);
719 
720  for(std::size_t sum=0; sum<op0.size(); sum++)
721  if(op0[sum]!=const_literal(false))
722  {
723  bvt tmpop;
724 
725  tmpop.reserve(product.size());
726 
727  for(std::size_t idx=0; idx<sum; idx++)
728  tmpop.push_back(const_literal(false));
729 
730  for(std::size_t idx=sum; idx<product.size(); idx++)
731  tmpop.push_back(prop.land(op1[idx-sum], op0[sum]));
732 
733  adder_no_overflow(product, tmpop);
734 
735  for(std::size_t idx=op1.size()-sum; idx<op1.size(); idx++)
736  prop.l_set_to_false(prop.land(op1[idx], op0[sum]));
737  }
738 
739  return product;
740 }
741 
742 bvt bv_utilst::signed_multiplier(const bvt &op0, const bvt &op1)
743 {
744  if(op0.empty() || op1.empty())
745  return bvt();
746 
747  literalt sign0=op0[op0.size()-1];
748  literalt sign1=op1[op1.size()-1];
749 
750  bvt neg0=cond_negate(op0, sign0);
751  bvt neg1=cond_negate(op1, sign1);
752 
753  bvt result=unsigned_multiplier(neg0, neg1);
754 
755  literalt result_sign=prop.lxor(sign0, sign1);
756 
757  return cond_negate(result, result_sign);
758 }
759 
760 bvt bv_utilst::cond_negate(const bvt &bv, const literalt cond)
761 {
762  bvt neg_bv=negate(bv);
763 
764  bvt result;
765  result.resize(bv.size());
766 
767  for(std::size_t i=0; i<bv.size(); i++)
768  result[i]=prop.lselect(cond, neg_bv[i], bv[i]);
769 
770  return result;
771 }
772 
774 {
775  PRECONDITION(!bv.empty());
776  return cond_negate(bv, bv[bv.size()-1]);
777 }
778 
780 {
782 
783  return cond_negate(bv, cond);
784 }
785 
787  const bvt &op0,
788  const bvt &op1)
789 {
790  if(op0.empty() || op1.empty())
791  return bvt();
792 
793  literalt sign0=op0[op0.size()-1];
794  literalt sign1=op1[op1.size()-1];
795 
796  bvt neg0=cond_negate_no_overflow(op0, sign0);
797  bvt neg1=cond_negate_no_overflow(op1, sign1);
798 
799  bvt result=unsigned_multiplier_no_overflow(neg0, neg1);
800 
801  prop.l_set_to_false(result[result.size() - 1]);
802 
803  literalt result_sign=prop.lxor(sign0, sign1);
804 
805  return cond_negate_no_overflow(result, result_sign);
806 }
807 
809  const bvt &op0,
810  const bvt &op1,
811  representationt rep)
812 {
813  switch(rep)
814  {
815  case representationt::SIGNED: return signed_multiplier(op0, op1);
816  case representationt::UNSIGNED: return unsigned_multiplier(op0, op1);
817  }
818 
819  UNREACHABLE;
820 }
821 
823  const bvt &op0,
824  const bvt &op1,
825  representationt rep)
826 {
827  switch(rep)
828  {
830  return signed_multiplier_no_overflow(op0, op1);
832  return unsigned_multiplier_no_overflow(op0, op1);
833  }
834 
835  UNREACHABLE;
836 }
837 
839  const bvt &op0,
840  const bvt &op1,
841  bvt &res,
842  bvt &rem)
843 {
844  if(op0.empty() || op1.empty())
845  return;
846 
847  bvt _op0(op0), _op1(op1);
848 
849  literalt sign_0=_op0[_op0.size()-1];
850  literalt sign_1=_op1[_op1.size()-1];
851 
852  bvt neg_0=negate(_op0), neg_1=negate(_op1);
853 
854  for(std::size_t i=0; i<_op0.size(); i++)
855  _op0[i]=(prop.lselect(sign_0, neg_0[i], _op0[i]));
856 
857  for(std::size_t i=0; i<_op1.size(); i++)
858  _op1[i]=(prop.lselect(sign_1, neg_1[i], _op1[i]));
859 
860  unsigned_divider(_op0, _op1, res, rem);
861 
862  bvt neg_res=negate(res), neg_rem=negate(rem);
863 
864  literalt result_sign=prop.lxor(sign_0, sign_1);
865 
866  for(std::size_t i=0; i<res.size(); i++)
867  res[i]=prop.lselect(result_sign, neg_res[i], res[i]);
868 
869  for(std::size_t i=0; i<res.size(); i++)
870  rem[i]=prop.lselect(sign_0, neg_rem[i], rem[i]);
871 }
872 
874  const bvt &op0,
875  const bvt &op1,
876  bvt &result,
877  bvt &remainer,
878  representationt rep)
879 {
881 
882  switch(rep)
883  {
885  signed_divider(op0, op1, result, remainer); break;
887  unsigned_divider(op0, op1, result, remainer); break;
888  }
889 }
890 
892  const bvt &op0,
893  const bvt &op1,
894  bvt &res,
895  bvt &rem)
896 {
897  std::size_t width=op0.size();
898 
899  // check if we divide by a power of two
900  #if 0
901  {
902  std::size_t one_count=0, non_const_count=0, one_pos=0;
903 
904  for(std::size_t i=0; i<op1.size(); i++)
905  {
906  literalt l=op1[i];
907  if(l.is_true())
908  {
909  one_count++;
910  one_pos=i;
911  }
912  else if(!l.is_false())
913  non_const_count++;
914  }
915 
916  if(non_const_count==0 && one_count==1 && one_pos!=0)
917  {
918  // it is a power of two!
919  res=shift(op0, LRIGHT, one_pos);
920 
921  // remainder is just a mask
922  rem=op0;
923  for(std::size_t i=one_pos; i<rem.size(); i++)
924  rem[i]=const_literal(false);
925  return;
926  }
927  }
928  #endif
929 
930  // Division by zero test.
931  // Note that we produce a non-deterministic result in
932  // case of division by zero. SMT-LIB now says the following:
933  // bvudiv returns a vector of all 1s if the second operand is 0
934  // bvurem returns its first operand if the second operand is 0
935 
937 
938  // free variables for result of division
939  res = prop.new_variables(width);
940  rem = prop.new_variables(width);
941 
942  // add implications
943 
944  bvt product=
946 
947  // res*op1 + rem = op0
948 
949  bvt sum=product;
950 
951  adder_no_overflow(sum, rem);
952 
953  literalt is_equal=equal(sum, op0);
954 
956 
957  // op1!=0 => rem < op1
958 
960  prop.limplies(
961  is_not_zero, lt_or_le(false, rem, op1, representationt::UNSIGNED)));
962 
963  // op1!=0 => res <= op0
964 
966  prop.limplies(
967  is_not_zero, lt_or_le(true, res, op0, representationt::UNSIGNED)));
968 }
969 
970 
971 #ifdef COMPACT_EQUAL_CONST
972 // TODO : use for lt_or_le as well
973 
977 void bv_utilst::equal_const_register(const bvt &var)
978 {
979  PRECONDITION(!is_constant(var));
980  equal_const_registered.insert(var);
981  return;
982 }
983 
990 literalt bv_utilst::equal_const_rec(bvt &var, bvt &constant)
991 {
992  std::size_t size = var.size();
993 
994  PRECONDITION(size != 0);
995  PRECONDITION(size == constant.size());
996  PRECONDITION(is_constant(constant));
997 
998  if(size == 1)
999  {
1000  literalt comp = prop.lequal(var[size - 1], constant[size - 1]);
1001  var.pop_back();
1002  constant.pop_back();
1003  return comp;
1004  }
1005  else
1006  {
1007  var_constant_pairt index(var, constant);
1008 
1009  equal_const_cachet::iterator entry = equal_const_cache.find(index);
1010 
1011  if(entry != equal_const_cache.end())
1012  {
1013  return entry->second;
1014  }
1015  else
1016  {
1017  literalt comp = prop.lequal(var[size - 1], constant[size - 1]);
1018  var.pop_back();
1019  constant.pop_back();
1020 
1021  literalt rec = equal_const_rec(var, constant);
1022  literalt compare = prop.land(rec, comp);
1023 
1024  equal_const_cache.insert(
1025  std::pair<var_constant_pairt, literalt>(index, compare));
1026 
1027  return compare;
1028  }
1029  }
1030 }
1031 
1040 literalt bv_utilst::equal_const(const bvt &var, const bvt &constant)
1041 {
1042  std::size_t size = constant.size();
1043 
1044  PRECONDITION(var.size() == size);
1045  PRECONDITION(!is_constant(var));
1046  PRECONDITION(is_constant(constant));
1047  PRECONDITION(size >= 2);
1048 
1049  // These get modified : be careful!
1050  bvt var_upper;
1051  bvt var_lower;
1052  bvt constant_upper;
1053  bvt constant_lower;
1054 
1055  /* Split the constant based on a change in parity
1056  * This is based on the observation that most constants are small,
1057  * so combinations of the lower bits are heavily used but the upper
1058  * bits are almost always either all 0 or all 1.
1059  */
1060  literalt top_bit = constant[size - 1];
1061 
1062  std::size_t split = size - 1;
1063  var_upper.push_back(var[size - 1]);
1064  constant_upper.push_back(constant[size - 1]);
1065 
1066  for(split = size - 2; split != 0; --split)
1067  {
1068  if(constant[split] != top_bit)
1069  {
1070  break;
1071  }
1072  else
1073  {
1074  var_upper.push_back(var[split]);
1075  constant_upper.push_back(constant[split]);
1076  }
1077  }
1078 
1079  for(std::size_t i = 0; i <= split; ++i)
1080  {
1081  var_lower.push_back(var[i]);
1082  constant_lower.push_back(constant[i]);
1083  }
1084 
1085  // Check we have split the array correctly
1086  INVARIANT(
1087  var_upper.size() + var_lower.size() == size,
1088  "lower size plus upper size should equal the total size");
1089  INVARIANT(
1090  constant_upper.size() + constant_lower.size() == size,
1091  "lower size plus upper size should equal the total size");
1092 
1093  literalt top_comparison = equal_const_rec(var_upper, constant_upper);
1094  literalt bottom_comparison = equal_const_rec(var_lower, constant_lower);
1095 
1096  return prop.land(top_comparison, bottom_comparison);
1097 }
1098 
1099 #endif
1100 
1105 literalt bv_utilst::equal(const bvt &op0, const bvt &op1)
1106 {
1107  PRECONDITION(op0.size() == op1.size());
1108 
1109  #ifdef COMPACT_EQUAL_CONST
1110  // simplify_expr should put the constant on the right
1111  // but bit-level simplification may result in the other cases
1112  if(is_constant(op0) && !is_constant(op1) && op0.size() > 2 &&
1113  equal_const_registered.find(op1) != equal_const_registered.end())
1114  return equal_const(op1, op0);
1115  else if(!is_constant(op0) && is_constant(op1) && op0.size() > 2 &&
1116  equal_const_registered.find(op0) != equal_const_registered.end())
1117  return equal_const(op0, op1);
1118  #endif
1119 
1120  bvt equal_bv;
1121  equal_bv.resize(op0.size());
1122 
1123  for(std::size_t i=0; i<op0.size(); i++)
1124  equal_bv[i]=prop.lequal(op0[i], op1[i]);
1125 
1126  return prop.land(equal_bv);
1127 }
1128 
1133 /* Some clauses are not needed for correctness but they remove
1134  models (effectively setting "don't care" bits) and so may be worth
1135  including.*/
1136 // #define INCLUDE_REDUNDANT_CLAUSES
1137 
1138 // Saves space but slows the solver
1139 // There is a variant that uses the xor as an auxiliary that should improve both
1140 // #define COMPACT_LT_OR_LE
1141 
1142 
1143 
1145  bool or_equal,
1146  const bvt &bv0,
1147  const bvt &bv1,
1148  representationt rep)
1149 {
1150  PRECONDITION(bv0.size() == bv1.size());
1151 
1152  literalt top0=bv0[bv0.size()-1],
1153  top1=bv1[bv1.size()-1];
1154 
1155 #ifdef COMPACT_LT_OR_LE
1157  {
1158  bvt compareBelow; // 1 if a compare is needed below this bit
1159  literalt result;
1160  size_t start;
1161  size_t i;
1162 
1163  compareBelow = prop.new_variables(bv0.size());
1164  result = prop.new_variable();
1165 
1166  if(rep==SIGNED)
1167  {
1168  INVARIANT(
1169  bv0.size() >= 2, "signed bitvectors should have at least two bits");
1170  start = compareBelow.size() - 2;
1171 
1172  literalt firstComp=compareBelow[start];
1173 
1174  // When comparing signs we are comparing the top bit
1175 #ifdef INCLUDE_REDUNDANT_CLAUSES
1176  prop.l_set_to_true(compareBelow[start + 1])
1177 #endif
1178 
1179  // Four cases...
1180  prop.lcnf(top0, top1, firstComp); // + + compare needed
1181  prop.lcnf(top0, !top1, !result); // + - result false and no compare needed
1182  prop.lcnf(!top0, top1, result); // - + result true and no compare needed
1183  prop.lcnf(!top0, !top1, firstComp); // - - negated compare needed
1184 
1185 #ifdef INCLUDE_REDUNDANT_CLAUSES
1186  prop.lcnf(top0, !top1, !firstComp);
1187  prop.lcnf(!top0, top1, !firstComp);
1188 #endif
1189  }
1190  else
1191  {
1192  // Unsigned is much easier
1193  start = compareBelow.size() - 1;
1194  prop.l_set_to_true(compareBelow[start]);
1195  }
1196 
1197  // Determine the output
1198  // \forall i . cb[i] & -a[i] & b[i] => result
1199  // \forall i . cb[i] & a[i] & -b[i] => -result
1200  i = start;
1201  do
1202  {
1203  prop.lcnf(!compareBelow[i], bv0[i], !bv1[i], result);
1204  prop.lcnf(!compareBelow[i], !bv0[i], bv1[i], !result);
1205  }
1206  while(i-- != 0);
1207 
1208  // Chain the comparison bit
1209  // \forall i != 0 . cb[i] & a[i] & b[i] => cb[i-1]
1210  // \forall i != 0 . cb[i] & -a[i] & -b[i] => cb[i-1]
1211  for(i = start; i > 0; i--)
1212  {
1213  prop.lcnf(!compareBelow[i], !bv0[i], !bv1[i], compareBelow[i-1]);
1214  prop.lcnf(!compareBelow[i], bv0[i], bv1[i], compareBelow[i-1]);
1215  }
1216 
1217 
1218 #ifdef INCLUDE_REDUNDANT_CLAUSES
1219  // Optional zeroing of the comparison bit when not needed
1220  // \forall i != 0 . -c[i] => -c[i-1]
1221  // \forall i != 0 . c[i] & -a[i] & b[i] => -c[i-1]
1222  // \forall i != 0 . c[i] & a[i] & -b[i] => -c[i-1]
1223  for(i = start; i > 0; i--)
1224  {
1225  prop.lcnf(compareBelow[i], !compareBelow[i-1]);
1226  prop.lcnf(!compareBelow[i], bv0[i], !bv1[i], !compareBelow[i-1]);
1227  prop.lcnf(!compareBelow[i], !bv0[i], bv1[i], !compareBelow[i-1]);
1228  }
1229 #endif
1230 
1231  // The 'base case' of the induction is the case when they are equal
1232  prop.lcnf(!compareBelow[0], !bv0[0], !bv1[0], (or_equal)?result:!result);
1233  prop.lcnf(!compareBelow[0], bv0[0], bv1[0], (or_equal)?result:!result);
1234 
1235  return result;
1236  }
1237  else
1238 #endif
1239  {
1240  literalt carry=
1241  carry_out(bv0, inverted(bv1), const_literal(true));
1242 
1243  literalt result;
1244 
1245  if(rep==representationt::SIGNED)
1246  result=prop.lxor(prop.lequal(top0, top1), carry);
1247  else
1248  {
1249  INVARIANT(
1251  "representation has either value signed or unsigned");
1252  result = !carry;
1253  }
1254 
1255  if(or_equal)
1256  result=prop.lor(result, equal(bv0, bv1));
1257 
1258  return result;
1259  }
1260 }
1261 
1263  const bvt &op0,
1264  const bvt &op1)
1265 {
1266 #ifdef COMPACT_LT_OR_LE
1267  return lt_or_le(false, op0, op1, UNSIGNED);
1268 #else
1269  // A <= B iff there is an overflow on A-B
1270  return !carry_out(op0, inverted(op1), const_literal(true));
1271 #endif
1272 }
1273 
1275  const bvt &bv0,
1276  const bvt &bv1)
1277 {
1278  return lt_or_le(false, bv0, bv1, representationt::SIGNED);
1279 }
1280 
1282  const bvt &bv0,
1283  irep_idt id,
1284  const bvt &bv1,
1285  representationt rep)
1286 {
1287  if(id==ID_equal)
1288  return equal(bv0, bv1);
1289  else if(id==ID_notequal)
1290  return !equal(bv0, bv1);
1291  else if(id==ID_le)
1292  return lt_or_le(true, bv0, bv1, rep);
1293  else if(id==ID_lt)
1294  return lt_or_le(false, bv0, bv1, rep);
1295  else if(id==ID_ge)
1296  return lt_or_le(true, bv1, bv0, rep); // swapped
1297  else if(id==ID_gt)
1298  return lt_or_le(false, bv1, bv0, rep); // swapped
1299  else
1300  UNREACHABLE;
1301 }
1302 
1304 {
1305  for(const auto &literal : bv)
1306  {
1307  if(!literal.is_constant())
1308  return false;
1309  }
1310 
1311  return true;
1312 }
1313 
1315  literalt cond,
1316  const bvt &a,
1317  const bvt &b)
1318 {
1319  PRECONDITION(a.size() == b.size());
1320 
1321  if(prop.cnf_handled_well())
1322  {
1323  for(std::size_t i=0; i<a.size(); i++)
1324  {
1325  prop.lcnf(!cond, a[i], !b[i]);
1326  prop.lcnf(!cond, !a[i], b[i]);
1327  }
1328  }
1329  else
1330  {
1331  prop.limplies(cond, equal(a, b));
1332  }
1333 
1334  return;
1335 }
1336 
1338 {
1339  bvt odd_bits;
1340  odd_bits.reserve(src.size()/2);
1341 
1342  // check every odd bit
1343  for(std::size_t i=0; i<src.size(); i++)
1344  {
1345  if(i%2!=0)
1346  odd_bits.push_back(src[i]);
1347  }
1348 
1349  return prop.lor(odd_bits);
1350 }
1351 
1353 {
1354  bvt even_bits;
1355  even_bits.reserve(src.size()/2);
1356 
1357  // get every even bit
1358  for(std::size_t i=0; i<src.size(); i++)
1359  {
1360  if(i%2==0)
1361  even_bits.push_back(src[i]);
1362  }
1363 
1364  return even_bits;
1365 }
bv_utilst::shiftt::SHIFT_LEFT
@ SHIFT_LEFT
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bv_utilst::cond_negate_no_overflow
bvt cond_negate_no_overflow(const bvt &bv, const literalt cond)
Definition: bv_utils.cpp:779
arith_tools.h
bv_utilst::extract_lsb
static bvt extract_lsb(const bvt &a, std::size_t n)
Definition: bv_utils.cpp:68
bv_utilst::cond_implies_equal
void cond_implies_equal(literalt cond, const bvt &a, const bvt &b)
Definition: bv_utils.cpp:1314
propt::new_variables
virtual bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition: prop.cpp:20
bv_utilst::carry
literalt carry(literalt a, literalt b, literalt c)
Definition: bv_utils.cpp:229
bv_utilst::full_adder
literalt full_adder(const literalt a, const literalt b, const literalt carry_in, literalt &carry_out)
Definition: bv_utils.cpp:138
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
bv_utilst::is_not_zero
literalt is_not_zero(const bvt &op)
Definition: bv_utils.h:144
bv_utilst::carry_out
literalt carry_out(const bvt &op0, const bvt &op1, literalt carry_in)
Definition: bv_utils.cpp:311
bvt
std::vector< literalt > bvt
Definition: literal.h:201
bv_utilst::negate_no_overflow
bvt negate_no_overflow(const bvt &op)
Definition: bv_utils.cpp:539
bv_utilst::adder_no_overflow
void adder_no_overflow(bvt &sum, const bvt &op, bool subtract, representationt rep)
Definition: bv_utils.cpp:414
bv_utilst::signed_multiplier
bvt signed_multiplier(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:742
bv_utilst::shiftt::SHIFT_ARIGHT
@ SHIFT_ARIGHT
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
propt::set_equal
virtual void set_equal(literalt a, literalt b)
asserts a==b in the propositional formula
Definition: prop.cpp:12
bv_utilst::representationt::UNSIGNED
@ UNSIGNED
bv_utilst::set_equal
void set_equal(const bvt &a, const bvt &b)
Definition: bv_utils.cpp:33
bv_utils.h
bv_utilst::signed_divider
void signed_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
Definition: bv_utils.cpp:838
propt::new_variable
virtual literalt new_variable()=0
propt::lor
virtual literalt lor(literalt a, literalt b)=0
propt::l_set_to_true
void l_set_to_true(literalt a)
Definition: prop.h:52
propt::l_set_to
virtual void l_set_to(literalt a, bool value)
Definition: prop.h:47
bv_utilst::prop
propt & prop
Definition: bv_utils.h:222
bv_utilst::incrementer
bvt incrementer(const bvt &op, literalt carry_in)
Definition: bv_utils.cpp:571
bv_utilst::inverted
static bvt inverted(const bvt &op)
Definition: bv_utils.cpp:579
bv_utilst::absolute_value
bvt absolute_value(const bvt &op)
Definition: bv_utils.cpp:773
bv_utilst::zeros
bvt zeros(std::size_t new_size) const
Definition: bv_utils.h:190
bv_utilst::unsigned_multiplier
bvt unsigned_multiplier(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:633
propt::land
virtual literalt land(literalt a, literalt b)=0
bv_utilst::select
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
Definition: bv_utils.cpp:94
bv_utilst::shift
static bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
Definition: bv_utils.cpp:479
bv_utilst::unsigned_less_than
literalt unsigned_less_than(const bvt &bv0, const bvt &bv1)
Definition: bv_utils.cpp:1262
bv_utilst::unsigned_divider
void unsigned_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
Definition: bv_utils.cpp:891
literalt::is_true
bool is_true() const
Definition: literal.h:156
propt::lxor
virtual literalt lxor(literalt a, literalt b)=0
bv_utilst::is_int_min
literalt is_int_min(const bvt &op)
Definition: bv_utils.h:147
bv_utilst::add
bvt add(const bvt &op0, const bvt &op1)
Definition: bv_utils.h:64
propt::limplies
virtual literalt limplies(literalt a, literalt b)=0
bv_utilst::representationt::SIGNED
@ SIGNED
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
propt::cnf_handled_well
virtual bool cnf_handled_well() const
Definition: prop.h:85
bv_utilst::representationt
representationt
Definition: bv_utils.h:31
bv_utilst::cond_negate
bvt cond_negate(const bvt &bv, const literalt cond)
Definition: bv_utils.cpp:760
bv_utilst::overflow_sub
literalt overflow_sub(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:389
literalt::is_false
bool is_false() const
Definition: literal.h:161
const_literal
literalt const_literal(bool value)
Definition: literal.h:188
bv_utilst::overflow_add
literalt overflow_add(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:365
bv_utilst::signed_multiplier_no_overflow
bvt signed_multiplier_no_overflow(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:786
bv_utilst::unsigned_multiplier_no_overflow
bvt unsigned_multiplier_no_overflow(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:703
bv_utilst::concatenate
static bvt concatenate(const bvt &a, const bvt &b)
Definition: bv_utils.cpp:78
bv_utilst::lt_or_le
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:1144
bv_utilst::add_sub
bvt add_sub(const bvt &op0, const bvt &op1, bool subtract)
Definition: bv_utils.cpp:337
bv_utilst::wallace_tree
bvt wallace_tree(const std::vector< bvt > &pps)
Definition: bv_utils.cpp:587
propt::l_set_to_false
void l_set_to_false(literalt a)
Definition: prop.h:54
bv_utilst::multiplier_no_overflow
bvt multiplier_no_overflow(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:822
bv_utilst::build_constant
static bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:13
propt::lequal
virtual literalt lequal(literalt a, literalt b)=0
bv_utilst::rel
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
Definition: bv_utils.cpp:1281
POSTCONDITION
#define POSTCONDITION(CONDITION)
Definition: invariant.h:480
bv_utilst::shiftt
shiftt
Definition: bv_utils.h:72
bv_utilst::negate
bvt negate(const bvt &op)
Definition: bv_utils.cpp:531
bv_utilst::overflow_negate
literalt overflow_negate(const bvt &op)
Definition: bv_utils.cpp:545
bv_utilst::shiftt::ROTATE_RIGHT
@ ROTATE_RIGHT
bv_utilst::extension
static bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
Definition: bv_utils.cpp:107
literalt
Definition: literal.h:26
bv_utilst::divider
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.h:87
bv_utilst::extract
static bvt extract(const bvt &a, std::size_t first, std::size_t last)
Definition: bv_utils.cpp:40
propt::has_set_to
virtual bool has_set_to() const
Definition: prop.h:81
bv_utilst::signed_less_than
literalt signed_less_than(const bvt &bv0, const bvt &bv1)
Definition: bv_utils.cpp:1274
bv_utilst::shiftt::SHIFT_LRIGHT
@ SHIFT_LRIGHT
bv_utilst::multiplier
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:808
bv_utilst::extract_msb
static bvt extract_msb(const bvt &a, std::size_t n)
Definition: bv_utils.cpp:56
literalt::is_constant
bool is_constant() const
Definition: literal.h:166
bv_utilst::verilog_bv_normal_bits
static bvt verilog_bv_normal_bits(const bvt &)
Definition: bv_utils.cpp:1352
bv_utilst::adder
void adder(bvt &sum, const bvt &op, literalt carry_in, literalt &carry_out)
Definition: bv_utils.cpp:295
integer2binary
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:67
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
bv_utilst::add_sub_no_overflow
bvt add_sub_no_overflow(const bvt &op0, const bvt &op1, bool subtract, representationt rep)
Definition: bv_utils.cpp:326
bv_utilst::equal
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1105
bv_utilst::is_zero
literalt is_zero(const bvt &op)
Definition: bv_utils.h:141
bv_utilst::shiftt::ROTATE_LEFT
@ ROTATE_LEFT
propt::lselect
virtual literalt lselect(literalt a, literalt b, literalt c)=0
bv_utilst::verilog_bv_has_x_or_z
literalt verilog_bv_has_x_or_z(const bvt &)
Definition: bv_utils.cpp:1337
bv_utilst::is_one
literalt is_one(const bvt &op)
Definition: bv_utils.cpp:24
propt::lcnf
void lcnf(literalt l0, literalt l1)
Definition: prop.h:58
bv_utilst::is_constant
static bool is_constant(const bvt &bv)
Definition: bv_utils.cpp:1303