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