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 {
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 {
784 
785  return cond_negate(bv, cond);
786 }
787 
789  const bvt &op0,
790  const bvt &op1)
791 {
792  if(op0.empty() || op1.empty())
793  return bvt();
794 
795  literalt sign0=op0[op0.size()-1];
796  literalt sign1=op1[op1.size()-1];
797 
798  bvt neg0=cond_negate_no_overflow(op0, sign0);
799  bvt neg1=cond_negate_no_overflow(op1, sign1);
800 
801  bvt result=unsigned_multiplier_no_overflow(neg0, neg1);
802 
803  prop.l_set_to_false(result[result.size() - 1]);
804 
805  literalt result_sign=prop.lxor(sign0, sign1);
806 
807  return cond_negate_no_overflow(result, result_sign);
808 }
809 
811  const bvt &op0,
812  const bvt &op1,
813  representationt rep)
814 {
815  switch(rep)
816  {
817  case representationt::SIGNED: return signed_multiplier(op0, op1);
818  case representationt::UNSIGNED: return unsigned_multiplier(op0, op1);
819  }
820 
821  UNREACHABLE;
822 }
823 
825  const bvt &op0,
826  const bvt &op1,
827  representationt rep)
828 {
829  switch(rep)
830  {
832  return signed_multiplier_no_overflow(op0, op1);
834  return unsigned_multiplier_no_overflow(op0, op1);
835  }
836 
837  UNREACHABLE;
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  }
891 }
892 
894  const bvt &op0,
895  const bvt &op1,
896  bvt &res,
897  bvt &rem)
898 {
899  std::size_t width=op0.size();
900 
901  // check if we divide by a power of two
902  #if 0
903  {
904  std::size_t one_count=0, non_const_count=0, one_pos=0;
905 
906  for(std::size_t i=0; i<op1.size(); i++)
907  {
908  literalt l=op1[i];
909  if(l.is_true())
910  {
911  one_count++;
912  one_pos=i;
913  }
914  else if(!l.is_false())
915  non_const_count++;
916  }
917 
918  if(non_const_count==0 && one_count==1 && one_pos!=0)
919  {
920  // it is a power of two!
921  res=shift(op0, LRIGHT, one_pos);
922 
923  // remainder is just a mask
924  rem=op0;
925  for(std::size_t i=one_pos; i<rem.size(); i++)
926  rem[i]=const_literal(false);
927  return;
928  }
929  }
930  #endif
931 
932  // Division by zero test.
933  // Note that we produce a non-deterministic result in
934  // case of division by zero. SMT-LIB now says the following:
935  // bvudiv returns a vector of all 1s if the second operand is 0
936  // bvurem returns its first operand if the second operand is 0
937 
939 
940  // free variables for result of division
941 
942  res.resize(width);
943  rem.resize(width);
944  for(std::size_t i=0; i<width; i++)
945  {
946  res[i]=prop.new_variable();
947  rem[i]=prop.new_variable();
948  }
949 
950  // add implications
951 
952  bvt product=
954 
955  // res*op1 + rem = op0
956 
957  bvt sum=product;
958 
959  adder_no_overflow(sum, rem);
960 
961  literalt is_equal=equal(sum, op0);
962 
964 
965  // op1!=0 => rem < op1
966 
968  prop.limplies(
969  is_not_zero, lt_or_le(false, rem, op1, representationt::UNSIGNED)));
970 
971  // op1!=0 => res <= op0
972 
974  prop.limplies(
975  is_not_zero, lt_or_le(true, res, op0, representationt::UNSIGNED)));
976 }
977 
978 
979 #ifdef COMPACT_EQUAL_CONST
980 // TODO : use for lt_or_le as well
981 
985 void bv_utilst::equal_const_register(const bvt &var)
986 {
987  PRECONDITION(!is_constant(var));
988  equal_const_registered.insert(var);
989  return;
990 }
991 
998 literalt bv_utilst::equal_const_rec(bvt &var, bvt &constant)
999 {
1000  std::size_t size = var.size();
1001 
1002  PRECONDITION(size != 0);
1003  PRECONDITION(size == constant.size());
1004  PRECONDITION(is_constant(constant));
1005 
1006  if(size == 1)
1007  {
1008  literalt comp = prop.lequal(var[size - 1], constant[size - 1]);
1009  var.pop_back();
1010  constant.pop_back();
1011  return comp;
1012  }
1013  else
1014  {
1015  var_constant_pairt index(var, constant);
1016 
1017  equal_const_cachet::iterator entry = equal_const_cache.find(index);
1018 
1019  if(entry != equal_const_cache.end())
1020  {
1021  return entry->second;
1022  }
1023  else
1024  {
1025  literalt comp = prop.lequal(var[size - 1], constant[size - 1]);
1026  var.pop_back();
1027  constant.pop_back();
1028 
1029  literalt rec = equal_const_rec(var, constant);
1030  literalt compare = prop.land(rec, comp);
1031 
1032  equal_const_cache.insert(
1033  std::pair<var_constant_pairt, literalt>(index, compare));
1034 
1035  return compare;
1036  }
1037  }
1038 }
1039 
1048 literalt bv_utilst::equal_const(const bvt &var, const bvt &constant)
1049 {
1050  std::size_t size = constant.size();
1051 
1052  PRECONDITION(var.size() == size);
1053  PRECONDITION(!is_constant(var));
1054  PRECONDITION(is_constant(constant));
1055  PRECONDITION(size >= 2);
1056 
1057  // These get modified : be careful!
1058  bvt var_upper;
1059  bvt var_lower;
1060  bvt constant_upper;
1061  bvt constant_lower;
1062 
1063  /* Split the constant based on a change in parity
1064  * This is based on the observation that most constants are small,
1065  * so combinations of the lower bits are heavily used but the upper
1066  * bits are almost always either all 0 or all 1.
1067  */
1068  literalt top_bit = constant[size - 1];
1069 
1070  std::size_t split = size - 1;
1071  var_upper.push_back(var[size - 1]);
1072  constant_upper.push_back(constant[size - 1]);
1073 
1074  for(split = size - 2; split != 0; --split)
1075  {
1076  if(constant[split] != top_bit)
1077  {
1078  break;
1079  }
1080  else
1081  {
1082  var_upper.push_back(var[split]);
1083  constant_upper.push_back(constant[split]);
1084  }
1085  }
1086 
1087  for(std::size_t i = 0; i <= split; ++i)
1088  {
1089  var_lower.push_back(var[i]);
1090  constant_lower.push_back(constant[i]);
1091  }
1092 
1093  // Check we have split the array correctly
1094  INVARIANT(
1095  var_upper.size() + var_lower.size() == size,
1096  "lower size plus upper size should equal the total size");
1097  INVARIANT(
1098  constant_upper.size() + constant_lower.size() == size,
1099  "lower size plus upper size should equal the total size");
1100 
1101  literalt top_comparison = equal_const_rec(var_upper, constant_upper);
1102  literalt bottom_comparison = equal_const_rec(var_lower, constant_lower);
1103 
1104  return prop.land(top_comparison, bottom_comparison);
1105 }
1106 
1107 #endif
1108 
1113 literalt bv_utilst::equal(const bvt &op0, const bvt &op1)
1114 {
1115  PRECONDITION(op0.size() == op1.size());
1116 
1117  #ifdef COMPACT_EQUAL_CONST
1118  // simplify_expr should put the constant on the right
1119  // but bit-level simplification may result in the other cases
1120  if(is_constant(op0) && !is_constant(op1) && op0.size() > 2 &&
1121  equal_const_registered.find(op1) != equal_const_registered.end())
1122  return equal_const(op1, op0);
1123  else if(!is_constant(op0) && is_constant(op1) && op0.size() > 2 &&
1124  equal_const_registered.find(op0) != equal_const_registered.end())
1125  return equal_const(op0, op1);
1126  #endif
1127 
1128  bvt equal_bv;
1129  equal_bv.resize(op0.size());
1130 
1131  for(std::size_t i=0; i<op0.size(); i++)
1132  equal_bv[i]=prop.lequal(op0[i], op1[i]);
1133 
1134  return prop.land(equal_bv);
1135 }
1136 
1141 /* Some clauses are not needed for correctness but they remove
1142  models (effectively setting "don't care" bits) and so may be worth
1143  including.*/
1144 // #define INCLUDE_REDUNDANT_CLAUSES
1145 
1146 // Saves space but slows the solver
1147 // There is a variant that uses the xor as an auxiliary that should improve both
1148 // #define COMPACT_LT_OR_LE
1149 
1150 
1151 
1153  bool or_equal,
1154  const bvt &bv0,
1155  const bvt &bv1,
1156  representationt rep)
1157 {
1158  PRECONDITION(bv0.size() == bv1.size());
1159 
1160  literalt top0=bv0[bv0.size()-1],
1161  top1=bv1[bv1.size()-1];
1162 
1163 #ifdef COMPACT_LT_OR_LE
1165  {
1166  bvt compareBelow; // 1 if a compare is needed below this bit
1167  literalt result;
1168  size_t start;
1169  size_t i;
1170 
1171  compareBelow.resize(bv0.size());
1172  Forall_literals(it, compareBelow) { (*it) = prop.new_variable(); }
1173  result = prop.new_variable();
1174 
1175  if(rep==SIGNED)
1176  {
1177  INVARIANT(
1178  bv0.size() >= 2, "signed bitvectors should have at least two bits");
1179  start = compareBelow.size() - 2;
1180 
1181  literalt firstComp=compareBelow[start];
1182 
1183  // When comparing signs we are comparing the top bit
1184 #ifdef INCLUDE_REDUNDANT_CLAUSES
1185  prop.l_set_to_true(compareBelow[start + 1])
1186 #endif
1187 
1188  // Four cases...
1189  prop.lcnf(top0, top1, firstComp); // + + compare needed
1190  prop.lcnf(top0, !top1, !result); // + - result false and no compare needed
1191  prop.lcnf(!top0, top1, result); // - + result true and no compare needed
1192  prop.lcnf(!top0, !top1, firstComp); // - - negated compare needed
1193 
1194 #ifdef INCLUDE_REDUNDANT_CLAUSES
1195  prop.lcnf(top0, !top1, !firstComp);
1196  prop.lcnf(!top0, top1, !firstComp);
1197 #endif
1198  }
1199  else
1200  {
1201  // Unsigned is much easier
1202  start = compareBelow.size() - 1;
1203  prop.l_set_to_true(compareBelow[start]);
1204  }
1205 
1206  // Determine the output
1207  // \forall i . cb[i] & -a[i] & b[i] => result
1208  // \forall i . cb[i] & a[i] & -b[i] => -result
1209  i = start;
1210  do
1211  {
1212  prop.lcnf(!compareBelow[i], bv0[i], !bv1[i], result);
1213  prop.lcnf(!compareBelow[i], !bv0[i], bv1[i], !result);
1214  }
1215  while(i-- != 0);
1216 
1217  // Chain the comparison bit
1218  // \forall i != 0 . cb[i] & a[i] & b[i] => cb[i-1]
1219  // \forall i != 0 . cb[i] & -a[i] & -b[i] => cb[i-1]
1220  for(i = start; i > 0; i--)
1221  {
1222  prop.lcnf(!compareBelow[i], !bv0[i], !bv1[i], compareBelow[i-1]);
1223  prop.lcnf(!compareBelow[i], bv0[i], bv1[i], compareBelow[i-1]);
1224  }
1225 
1226 
1227 #ifdef INCLUDE_REDUNDANT_CLAUSES
1228  // Optional zeroing of the comparison bit when not needed
1229  // \forall i != 0 . -c[i] => -c[i-1]
1230  // \forall i != 0 . c[i] & -a[i] & b[i] => -c[i-1]
1231  // \forall i != 0 . c[i] & a[i] & -b[i] => -c[i-1]
1232  for(i = start; i > 0; i--)
1233  {
1234  prop.lcnf(compareBelow[i], !compareBelow[i-1]);
1235  prop.lcnf(!compareBelow[i], bv0[i], !bv1[i], !compareBelow[i-1]);
1236  prop.lcnf(!compareBelow[i], !bv0[i], bv1[i], !compareBelow[i-1]);
1237  }
1238 #endif
1239 
1240  // The 'base case' of the induction is the case when they are equal
1241  prop.lcnf(!compareBelow[0], !bv0[0], !bv1[0], (or_equal)?result:!result);
1242  prop.lcnf(!compareBelow[0], bv0[0], bv1[0], (or_equal)?result:!result);
1243 
1244  return result;
1245  }
1246  else
1247 #endif
1248  {
1249  literalt carry=
1250  carry_out(bv0, inverted(bv1), const_literal(true));
1251 
1252  literalt result;
1253 
1254  if(rep==representationt::SIGNED)
1255  result=prop.lxor(prop.lequal(top0, top1), carry);
1256  else
1257  {
1258  INVARIANT(
1260  "representation has either value signed or unsigned");
1261  result = !carry;
1262  }
1263 
1264  if(or_equal)
1265  result=prop.lor(result, equal(bv0, bv1));
1266 
1267  return result;
1268  }
1269 }
1270 
1272  const bvt &op0,
1273  const bvt &op1)
1274 {
1275 #ifdef COMPACT_LT_OR_LE
1276  return lt_or_le(false, op0, op1, UNSIGNED);
1277 #else
1278  // A <= B iff there is an overflow on A-B
1279  return !carry_out(op0, inverted(op1), const_literal(true));
1280 #endif
1281 }
1282 
1284  const bvt &bv0,
1285  const bvt &bv1)
1286 {
1287  return lt_or_le(false, bv0, bv1, representationt::SIGNED);
1288 }
1289 
1291  const bvt &bv0,
1292  irep_idt id,
1293  const bvt &bv1,
1294  representationt rep)
1295 {
1296  if(id==ID_equal)
1297  return equal(bv0, bv1);
1298  else if(id==ID_notequal)
1299  return !equal(bv0, bv1);
1300  else if(id==ID_le)
1301  return lt_or_le(true, bv0, bv1, rep);
1302  else if(id==ID_lt)
1303  return lt_or_le(false, bv0, bv1, rep);
1304  else if(id==ID_ge)
1305  return lt_or_le(true, bv1, bv0, rep); // swapped
1306  else if(id==ID_gt)
1307  return lt_or_le(false, bv1, bv0, rep); // swapped
1308  else
1309  UNREACHABLE;
1310 }
1311 
1313 {
1314  forall_literals(it, bv)
1315  if(!it->is_constant())
1316  return false;
1317 
1318  return true;
1319 }
1320 
1322  literalt cond,
1323  const bvt &a,
1324  const bvt &b)
1325 {
1326  PRECONDITION(a.size() == b.size());
1327 
1328  if(prop.cnf_handled_well())
1329  {
1330  for(std::size_t i=0; i<a.size(); i++)
1331  {
1332  prop.lcnf(!cond, a[i], !b[i]);
1333  prop.lcnf(!cond, !a[i], b[i]);
1334  }
1335  }
1336  else
1337  {
1338  prop.limplies(cond, equal(a, b));
1339  }
1340 
1341  return;
1342 }
1343 
1345 {
1346  bvt odd_bits;
1347  odd_bits.reserve(src.size()/2);
1348 
1349  // check every odd bit
1350  for(std::size_t i=0; i<src.size(); i++)
1351  {
1352  if(i%2!=0)
1353  odd_bits.push_back(src[i]);
1354  }
1355 
1356  return prop.lor(odd_bits);
1357 }
1358 
1360 {
1361  bvt even_bits;
1362  even_bits.reserve(src.size()/2);
1363 
1364  // get every even bit
1365  for(std::size_t i=0; i<src.size(); i++)
1366  {
1367  if(i%2==0)
1368  even_bits.push_back(src[i]);
1369  }
1370 
1371  return even_bits;
1372 }
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: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:1321
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
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:313
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: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: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: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: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: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:203
propt::land
virtual literalt land(literalt a, literalt b)=0
Forall_literals
#define Forall_literals(it, bv)
Definition: literal.h:207
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
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:1271
bv_utilst::unsigned_divider
void unsigned_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
Definition: bv_utils.cpp:893
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: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: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:367
bv_utilst::signed_multiplier_no_overflow
bvt signed_multiplier_no_overflow(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:788
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:1152
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:54
bv_utilst::multiplier_no_overflow
bvt multiplier_no_overflow(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:824
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:1290
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: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: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:42
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:1283
bv_utilst::shiftt::SHIFT_LRIGHT
@ SHIFT_LRIGHT
bv_utilst::multiplier
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:810
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:166
bv_utilst::verilog_bv_normal_bits
bvt verilog_bv_normal_bits(const bvt &)
Definition: bv_utils.cpp:1359
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:1113
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:1344
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:58
validation_modet::INVARIANT
@ INVARIANT
bv_utilst::is_constant
bool is_constant(const bvt &bv)
Definition: bv_utils.cpp:1312