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 
940  res.resize(width);
941  rem.resize(width);
942  for(std::size_t i=0; i<width; i++)
943  {
944  res[i]=prop.new_variable();
945  rem[i]=prop.new_variable();
946  }
947 
948  // add implications
949 
950  bvt product=
952 
953  // res*op1 + rem = op0
954 
955  bvt sum=product;
956 
957  adder_no_overflow(sum, rem);
958 
959  literalt is_equal=equal(sum, op0);
960 
962 
963  // op1!=0 => rem < op1
964 
966  prop.limplies(
967  is_not_zero, lt_or_le(false, rem, op1, representationt::UNSIGNED)));
968 
969  // op1!=0 => res <= op0
970 
972  prop.limplies(
973  is_not_zero, lt_or_le(true, res, op0, representationt::UNSIGNED)));
974 }
975 
976 
977 #ifdef COMPACT_EQUAL_CONST
978 // TODO : use for lt_or_le as well
979 
983 void bv_utilst::equal_const_register(const bvt &var)
984 {
985  PRECONDITION(!is_constant(var));
986  equal_const_registered.insert(var);
987  return;
988 }
989 
996 literalt bv_utilst::equal_const_rec(bvt &var, bvt &constant)
997 {
998  std::size_t size = var.size();
999 
1000  PRECONDITION(size != 0);
1001  PRECONDITION(size == constant.size());
1002  PRECONDITION(is_constant(constant));
1003 
1004  if(size == 1)
1005  {
1006  literalt comp = prop.lequal(var[size - 1], constant[size - 1]);
1007  var.pop_back();
1008  constant.pop_back();
1009  return comp;
1010  }
1011  else
1012  {
1013  var_constant_pairt index(var, constant);
1014 
1015  equal_const_cachet::iterator entry = equal_const_cache.find(index);
1016 
1017  if(entry != equal_const_cache.end())
1018  {
1019  return entry->second;
1020  }
1021  else
1022  {
1023  literalt comp = prop.lequal(var[size - 1], constant[size - 1]);
1024  var.pop_back();
1025  constant.pop_back();
1026 
1027  literalt rec = equal_const_rec(var, constant);
1028  literalt compare = prop.land(rec, comp);
1029 
1030  equal_const_cache.insert(
1031  std::pair<var_constant_pairt, literalt>(index, compare));
1032 
1033  return compare;
1034  }
1035  }
1036 }
1037 
1046 literalt bv_utilst::equal_const(const bvt &var, const bvt &constant)
1047 {
1048  std::size_t size = constant.size();
1049 
1050  PRECONDITION(var.size() == size);
1051  PRECONDITION(!is_constant(var));
1052  PRECONDITION(is_constant(constant));
1053  PRECONDITION(size >= 2);
1054 
1055  // These get modified : be careful!
1056  bvt var_upper;
1057  bvt var_lower;
1058  bvt constant_upper;
1059  bvt constant_lower;
1060 
1061  /* Split the constant based on a change in parity
1062  * This is based on the observation that most constants are small,
1063  * so combinations of the lower bits are heavily used but the upper
1064  * bits are almost always either all 0 or all 1.
1065  */
1066  literalt top_bit = constant[size - 1];
1067 
1068  std::size_t split = size - 1;
1069  var_upper.push_back(var[size - 1]);
1070  constant_upper.push_back(constant[size - 1]);
1071 
1072  for(split = size - 2; split != 0; --split)
1073  {
1074  if(constant[split] != top_bit)
1075  {
1076  break;
1077  }
1078  else
1079  {
1080  var_upper.push_back(var[split]);
1081  constant_upper.push_back(constant[split]);
1082  }
1083  }
1084 
1085  for(std::size_t i = 0; i <= split; ++i)
1086  {
1087  var_lower.push_back(var[i]);
1088  constant_lower.push_back(constant[i]);
1089  }
1090 
1091  // Check we have split the array correctly
1092  INVARIANT(
1093  var_upper.size() + var_lower.size() == size,
1094  "lower size plus upper size should equal the total size");
1095  INVARIANT(
1096  constant_upper.size() + constant_lower.size() == size,
1097  "lower size plus upper size should equal the total size");
1098 
1099  literalt top_comparison = equal_const_rec(var_upper, constant_upper);
1100  literalt bottom_comparison = equal_const_rec(var_lower, constant_lower);
1101 
1102  return prop.land(top_comparison, bottom_comparison);
1103 }
1104 
1105 #endif
1106 
1111 literalt bv_utilst::equal(const bvt &op0, const bvt &op1)
1112 {
1113  PRECONDITION(op0.size() == op1.size());
1114 
1115  #ifdef COMPACT_EQUAL_CONST
1116  // simplify_expr should put the constant on the right
1117  // but bit-level simplification may result in the other cases
1118  if(is_constant(op0) && !is_constant(op1) && op0.size() > 2 &&
1119  equal_const_registered.find(op1) != equal_const_registered.end())
1120  return equal_const(op1, op0);
1121  else if(!is_constant(op0) && is_constant(op1) && op0.size() > 2 &&
1122  equal_const_registered.find(op0) != equal_const_registered.end())
1123  return equal_const(op0, op1);
1124  #endif
1125 
1126  bvt equal_bv;
1127  equal_bv.resize(op0.size());
1128 
1129  for(std::size_t i=0; i<op0.size(); i++)
1130  equal_bv[i]=prop.lequal(op0[i], op1[i]);
1131 
1132  return prop.land(equal_bv);
1133 }
1134 
1139 /* Some clauses are not needed for correctness but they remove
1140  models (effectively setting "don't care" bits) and so may be worth
1141  including.*/
1142 // #define INCLUDE_REDUNDANT_CLAUSES
1143 
1144 // Saves space but slows the solver
1145 // There is a variant that uses the xor as an auxiliary that should improve both
1146 // #define COMPACT_LT_OR_LE
1147 
1148 
1149 
1151  bool or_equal,
1152  const bvt &bv0,
1153  const bvt &bv1,
1154  representationt rep)
1155 {
1156  PRECONDITION(bv0.size() == bv1.size());
1157 
1158  literalt top0=bv0[bv0.size()-1],
1159  top1=bv1[bv1.size()-1];
1160 
1161 #ifdef COMPACT_LT_OR_LE
1163  {
1164  bvt compareBelow; // 1 if a compare is needed below this bit
1165  literalt result;
1166  size_t start;
1167  size_t i;
1168 
1169  compareBelow.resize(bv0.size());
1170  for(auto &literal : compareBelow)
1171  literal = prop.new_variable();
1172  result = prop.new_variable();
1173 
1174  if(rep==SIGNED)
1175  {
1176  INVARIANT(
1177  bv0.size() >= 2, "signed bitvectors should have at least two bits");
1178  start = compareBelow.size() - 2;
1179 
1180  literalt firstComp=compareBelow[start];
1181 
1182  // When comparing signs we are comparing the top bit
1183 #ifdef INCLUDE_REDUNDANT_CLAUSES
1184  prop.l_set_to_true(compareBelow[start + 1])
1185 #endif
1186 
1187  // Four cases...
1188  prop.lcnf(top0, top1, firstComp); // + + compare needed
1189  prop.lcnf(top0, !top1, !result); // + - result false and no compare needed
1190  prop.lcnf(!top0, top1, result); // - + result true and no compare needed
1191  prop.lcnf(!top0, !top1, firstComp); // - - negated compare needed
1192 
1193 #ifdef INCLUDE_REDUNDANT_CLAUSES
1194  prop.lcnf(top0, !top1, !firstComp);
1195  prop.lcnf(!top0, top1, !firstComp);
1196 #endif
1197  }
1198  else
1199  {
1200  // Unsigned is much easier
1201  start = compareBelow.size() - 1;
1202  prop.l_set_to_true(compareBelow[start]);
1203  }
1204 
1205  // Determine the output
1206  // \forall i . cb[i] & -a[i] & b[i] => result
1207  // \forall i . cb[i] & a[i] & -b[i] => -result
1208  i = start;
1209  do
1210  {
1211  prop.lcnf(!compareBelow[i], bv0[i], !bv1[i], result);
1212  prop.lcnf(!compareBelow[i], !bv0[i], bv1[i], !result);
1213  }
1214  while(i-- != 0);
1215 
1216  // Chain the comparison bit
1217  // \forall i != 0 . cb[i] & a[i] & b[i] => cb[i-1]
1218  // \forall i != 0 . cb[i] & -a[i] & -b[i] => cb[i-1]
1219  for(i = start; i > 0; i--)
1220  {
1221  prop.lcnf(!compareBelow[i], !bv0[i], !bv1[i], compareBelow[i-1]);
1222  prop.lcnf(!compareBelow[i], bv0[i], bv1[i], compareBelow[i-1]);
1223  }
1224 
1225 
1226 #ifdef INCLUDE_REDUNDANT_CLAUSES
1227  // Optional zeroing of the comparison bit when not needed
1228  // \forall i != 0 . -c[i] => -c[i-1]
1229  // \forall i != 0 . c[i] & -a[i] & b[i] => -c[i-1]
1230  // \forall i != 0 . c[i] & a[i] & -b[i] => -c[i-1]
1231  for(i = start; i > 0; i--)
1232  {
1233  prop.lcnf(compareBelow[i], !compareBelow[i-1]);
1234  prop.lcnf(!compareBelow[i], bv0[i], !bv1[i], !compareBelow[i-1]);
1235  prop.lcnf(!compareBelow[i], !bv0[i], bv1[i], !compareBelow[i-1]);
1236  }
1237 #endif
1238 
1239  // The 'base case' of the induction is the case when they are equal
1240  prop.lcnf(!compareBelow[0], !bv0[0], !bv1[0], (or_equal)?result:!result);
1241  prop.lcnf(!compareBelow[0], bv0[0], bv1[0], (or_equal)?result:!result);
1242 
1243  return result;
1244  }
1245  else
1246 #endif
1247  {
1248  literalt carry=
1249  carry_out(bv0, inverted(bv1), const_literal(true));
1250 
1251  literalt result;
1252 
1253  if(rep==representationt::SIGNED)
1254  result=prop.lxor(prop.lequal(top0, top1), carry);
1255  else
1256  {
1257  INVARIANT(
1259  "representation has either value signed or unsigned");
1260  result = !carry;
1261  }
1262 
1263  if(or_equal)
1264  result=prop.lor(result, equal(bv0, bv1));
1265 
1266  return result;
1267  }
1268 }
1269 
1271  const bvt &op0,
1272  const bvt &op1)
1273 {
1274 #ifdef COMPACT_LT_OR_LE
1275  return lt_or_le(false, op0, op1, UNSIGNED);
1276 #else
1277  // A <= B iff there is an overflow on A-B
1278  return !carry_out(op0, inverted(op1), const_literal(true));
1279 #endif
1280 }
1281 
1283  const bvt &bv0,
1284  const bvt &bv1)
1285 {
1286  return lt_or_le(false, bv0, bv1, representationt::SIGNED);
1287 }
1288 
1290  const bvt &bv0,
1291  irep_idt id,
1292  const bvt &bv1,
1293  representationt rep)
1294 {
1295  if(id==ID_equal)
1296  return equal(bv0, bv1);
1297  else if(id==ID_notequal)
1298  return !equal(bv0, bv1);
1299  else if(id==ID_le)
1300  return lt_or_le(true, bv0, bv1, rep);
1301  else if(id==ID_lt)
1302  return lt_or_le(false, bv0, bv1, rep);
1303  else if(id==ID_ge)
1304  return lt_or_le(true, bv1, bv0, rep); // swapped
1305  else if(id==ID_gt)
1306  return lt_or_le(false, bv1, bv0, rep); // swapped
1307  else
1308  UNREACHABLE;
1309 }
1310 
1312 {
1313  for(const auto &literal : bv)
1314  {
1315  if(!literal.is_constant())
1316  return false;
1317  }
1318 
1319  return true;
1320 }
1321 
1323  literalt cond,
1324  const bvt &a,
1325  const bvt &b)
1326 {
1327  PRECONDITION(a.size() == b.size());
1328 
1329  if(prop.cnf_handled_well())
1330  {
1331  for(std::size_t i=0; i<a.size(); i++)
1332  {
1333  prop.lcnf(!cond, a[i], !b[i]);
1334  prop.lcnf(!cond, !a[i], b[i]);
1335  }
1336  }
1337  else
1338  {
1339  prop.limplies(cond, equal(a, b));
1340  }
1341 
1342  return;
1343 }
1344 
1346 {
1347  bvt odd_bits;
1348  odd_bits.reserve(src.size()/2);
1349 
1350  // check every odd bit
1351  for(std::size_t i=0; i<src.size(); i++)
1352  {
1353  if(i%2!=0)
1354  odd_bits.push_back(src[i]);
1355  }
1356 
1357  return prop.lor(odd_bits);
1358 }
1359 
1361 {
1362  bvt even_bits;
1363  even_bits.reserve(src.size()/2);
1364 
1365  // get every even bit
1366  for(std::size_t i=0; i<src.size(); i++)
1367  {
1368  if(i%2==0)
1369  even_bits.push_back(src[i]);
1370  }
1371 
1372  return even_bits;
1373 }
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:1322
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:1270
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:1150
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:1289
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:1282
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:1360
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:1111
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:1345
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:1311