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  bvt result;
19  result.resize(width);
20  assert(n_str.size()==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  assert(!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  assert(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  assert(first<a.size());
46  assert(last<a.size());
47  assert(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  assert(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  assert(n<=a.size());
62 
63  bvt result=a;
64  result.erase(result.begin(), result.begin()+(result.size()-n));
65 
66  assert(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  assert(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  assert(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  bvt result=bv;
116  result.resize(new_size);
117 
118  assert(old_size!=0);
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  unsigned 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  assert(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  assert(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  assert(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  assert(false);
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  assert(false);
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 if(rep==representationt::UNSIGNED)
441  {
443  adder(sum, tmp_op, const_literal(subtract), carry_out);
444  prop.l_set_to(carry_out, subtract);
445  }
446  else
447  assert(false);
448 }
449 
450 void bv_utilst::adder_no_overflow(bvt &sum, const bvt &op)
451 {
453 
454  adder(sum, op, carry_out, carry_out);
455 
456  prop.l_set_to_false(carry_out); // enforce no overflow
457 }
458 
459 bvt bv_utilst::shift(const bvt &op, const shiftt s, const bvt &dist)
460 {
461  std::size_t d=1, width=op.size();
462  bvt result=op;
463 
464  for(std::size_t stage=0; stage<dist.size(); stage++)
465  {
466  if(dist[stage]!=const_literal(false))
467  {
468  bvt tmp=shift(result, s, d);
469 
470  for(std::size_t i=0; i<width; i++)
471  result[i]=prop.lselect(dist[stage], tmp[i], result[i]);
472  }
473 
474  d=d<<1;
475  }
476 
477  return result;
478 }
479 
480 bvt bv_utilst::shift(const bvt &src, const shiftt s, std::size_t dist)
481 {
482  bvt result;
483  result.resize(src.size());
484 
485  for(std::size_t i=0; i<src.size(); i++)
486  {
487  literalt l;
488 
489  switch(s)
490  {
491  case shiftt::LEFT:
492  l=(dist<=i?src[i-dist]:const_literal(false));
493  break;
494 
495  case shiftt::ARIGHT:
496  l=(i+dist<src.size()?src[i+dist]:src[src.size()-1]); // sign bit
497  break;
498 
499  case shiftt::LRIGHT:
500  l=(i+dist<src.size()?src[i+dist]:const_literal(false));
501  break;
502 
503  default:
504  assert(false);
505  }
506 
507  result[i]=l;
508  }
509 
510  return result;
511 }
512 
514 {
515  bvt result=inverted(bv);
517  incrementer(result, const_literal(true), carry_out);
518  return result;
519 }
520 
522 {
523  prop.l_set_to(overflow_negate(bv), false);
524  return negate(bv);
525 }
526 
528 {
529  // a overflow on unary- can only happen with the smallest
530  // representable number 100....0
531 
532  bvt zeros(bv);
533  zeros.erase(--zeros.end());
534 
535  return prop.land(bv[bv.size()-1], !prop.lor(zeros));
536 }
537 
539  bvt &bv,
540  literalt carry_in,
541  literalt &carry_out)
542 {
543  carry_out=carry_in;
544 
545  Forall_literals(it, bv)
546  {
547  literalt new_carry=prop.land(carry_out, *it);
548  *it=prop.lxor(*it, carry_out);
549  carry_out=new_carry;
550  }
551 }
552 
554 {
555  bvt result=bv;
557  incrementer(result, carry_in, carry_out);
558  return result;
559 }
560 
562 {
563  bvt result=bv;
564  Forall_literals(it, result)
565  *it=!*it;
566  return result;
567 }
568 
569 bvt bv_utilst::wallace_tree(const std::vector<bvt> &pps)
570 {
571  assert(!pps.empty());
572 
573  if(pps.size()==1)
574  return pps.front();
575  else if(pps.size()==2)
576  return add(pps[0], pps[1]);
577  else
578  {
579  std::vector<bvt> new_pps;
580  std::size_t no_full_adders=pps.size()/3;
581 
582  // add groups of three partial products using CSA
583  for(std::size_t i=0; i<no_full_adders; i++)
584  {
585  const bvt &a=pps[i*3+0],
586  &b=pps[i*3+1],
587  &c=pps[i*3+2];
588 
589  assert(a.size()==b.size() && a.size()==c.size());
590 
591  bvt s(a.size()), t(a.size());
592 
593  for(std::size_t bit=0; bit<a.size(); bit++)
594  {
595  // \todo reformulate using full_adder
596  s[bit]=prop.lxor(a[bit], prop.lxor(b[bit], c[bit]));
597  t[bit]=(bit==0)?const_literal(false):
598  carry(a[bit-1], b[bit-1], c[bit-1]);
599  }
600 
601  new_pps.push_back(s);
602  new_pps.push_back(t);
603  }
604 
605  // pass onwards up to two remaining partial products
606  for(std::size_t i=no_full_adders*3; i<pps.size(); i++)
607  new_pps.push_back(pps[i]);
608 
609  assert(new_pps.size()<pps.size());
610  return wallace_tree(new_pps);
611  }
612 }
613 
614 bvt bv_utilst::unsigned_multiplier(const bvt &_op0, const bvt &_op1)
615 {
616  #if 1
617  bvt op0=_op0, op1=_op1;
618 
619  if(is_constant(op1))
620  std::swap(op0, op1);
621 
622  bvt product;
623  product.resize(op0.size());
624 
625  for(std::size_t i=0; i<product.size(); i++)
626  product[i]=const_literal(false);
627 
628  for(std::size_t sum=0; sum<op0.size(); sum++)
629  if(op0[sum]!=const_literal(false))
630  {
631  bvt tmpop;
632 
633  tmpop.reserve(op0.size());
634 
635  for(std::size_t idx=0; idx<sum; idx++)
636  tmpop.push_back(const_literal(false));
637 
638  for(std::size_t idx=sum; idx<op0.size(); idx++)
639  tmpop.push_back(prop.land(op1[idx-sum], op0[sum]));
640 
641  product=add(product, tmpop);
642  }
643 
644  return product;
645  #else
646  // Wallace tree multiplier. This is disabled, as runtimes have
647  // been observed to go up by 5%-10%, and on some models even by 20%.
648 
649  // build the usual quadratic number of partial products
650 
651  bvt op0=_op0, op1=_op1;
652 
653  if(is_constant(op1))
654  std::swap(op0, op1);
655 
656  std::vector<bvt> pps;
657  pps.reserve(op0.size());
658 
659  for(std::size_t bit=0; bit<op0.size(); bit++)
660  if(op0[bit]!=const_literal(false))
661  {
662  bvt pp;
663 
664  pp.reserve(op0.size());
665 
666  // zeros according to weight
667  for(std::size_t idx=0; idx<bit; idx++)
668  pp.push_back(const_literal(false));
669 
670  for(std::size_t idx=bit; idx<op0.size(); idx++)
671  pp.push_back(prop.land(op1[idx-bit], op0[bit]));
672 
673  pps.push_back(pp);
674  }
675 
676  if(pps.empty())
677  return zeros(op0.size());
678  else
679  return wallace_tree(pps);
680 
681  #endif
682 }
683 
685  const bvt &op0,
686  const bvt &op1)
687 {
688  bvt _op0=op0, _op1=op1;
689 
690  if(is_constant(_op1))
691  _op0.swap(_op1);
692 
693  assert(_op0.size()==_op1.size());
694 
695  bvt product;
696  product.resize(_op0.size());
697 
698  for(std::size_t i=0; i<product.size(); i++)
699  product[i]=const_literal(false);
700 
701  for(std::size_t sum=0; sum<op0.size(); sum++)
702  if(op0[sum]!=const_literal(false))
703  {
704  bvt tmpop;
705 
706  tmpop.reserve(product.size());
707 
708  for(std::size_t idx=0; idx<sum; idx++)
709  tmpop.push_back(const_literal(false));
710 
711  for(std::size_t idx=sum; idx<product.size(); idx++)
712  tmpop.push_back(prop.land(op1[idx-sum], op0[sum]));
713 
714  adder_no_overflow(product, tmpop);
715 
716  for(std::size_t idx=op1.size()-sum; idx<op1.size(); idx++)
717  prop.l_set_to_false(prop.land(op1[idx], op0[sum]));
718  }
719 
720  return product;
721 }
722 
723 bvt bv_utilst::signed_multiplier(const bvt &op0, const bvt &op1)
724 {
725  if(op0.empty() || op1.empty())
726  return bvt();
727 
728  literalt sign0=op0[op0.size()-1];
729  literalt sign1=op1[op1.size()-1];
730 
731  bvt neg0=cond_negate(op0, sign0);
732  bvt neg1=cond_negate(op1, sign1);
733 
734  bvt result=unsigned_multiplier(neg0, neg1);
735 
736  literalt result_sign=prop.lxor(sign0, sign1);
737 
738  return cond_negate(result, result_sign);
739 }
740 
741 bvt bv_utilst::cond_negate(const bvt &bv, const literalt cond)
742 {
743  bvt neg_bv=negate(bv);
744 
745  bvt result;
746  result.resize(bv.size());
747 
748  for(std::size_t i=0; i<bv.size(); i++)
749  result[i]=prop.lselect(cond, neg_bv[i], bv[i]);
750 
751  return result;
752 }
753 
755 {
756  assert(!bv.empty());
757  return cond_negate(bv, bv[bv.size()-1]);
758 }
759 
761 {
762  prop.l_set_to(
763  prop.limplies(cond, !overflow_negate(bv)),
764  true);
765 
766  return cond_negate(bv, cond);
767 }
768 
770  const bvt &op0,
771  const bvt &op1)
772 {
773  if(op0.empty() || op1.empty())
774  return bvt();
775 
776  literalt sign0=op0[op0.size()-1];
777  literalt sign1=op1[op1.size()-1];
778 
779  bvt neg0=cond_negate_no_overflow(op0, sign0);
780  bvt neg1=cond_negate_no_overflow(op1, sign1);
781 
782  bvt result=unsigned_multiplier_no_overflow(neg0, neg1);
783 
784  prop.l_set_to(result[result.size()-1], false);
785 
786  literalt result_sign=prop.lxor(sign0, sign1);
787 
788  return cond_negate_no_overflow(result, result_sign);
789 }
790 
792  const bvt &op0,
793  const bvt &op1,
794  representationt rep)
795 {
796  switch(rep)
797  {
798  case representationt::SIGNED: return signed_multiplier(op0, op1);
799  case representationt::UNSIGNED: return unsigned_multiplier(op0, op1);
800  default: assert(false);
801  }
802 }
803 
805  const bvt &op0,
806  const bvt &op1,
807  representationt rep)
808 {
809  switch(rep)
810  {
812  return signed_multiplier_no_overflow(op0, op1);
814  return unsigned_multiplier_no_overflow(op0, op1);
815  default: assert(false);
816  }
817 }
818 
820  const bvt &op0,
821  const bvt &op1,
822  bvt &res,
823  bvt &rem)
824 {
825  if(op0.empty() || op1.empty())
826  return;
827 
828  bvt _op0(op0), _op1(op1);
829 
830  literalt sign_0=_op0[_op0.size()-1];
831  literalt sign_1=_op1[_op1.size()-1];
832 
833  bvt neg_0=negate(_op0), neg_1=negate(_op1);
834 
835  for(std::size_t i=0; i<_op0.size(); i++)
836  _op0[i]=(prop.lselect(sign_0, neg_0[i], _op0[i]));
837 
838  for(std::size_t i=0; i<_op1.size(); i++)
839  _op1[i]=(prop.lselect(sign_1, neg_1[i], _op1[i]));
840 
841  unsigned_divider(_op0, _op1, res, rem);
842 
843  bvt neg_res=negate(res), neg_rem=negate(rem);
844 
845  literalt result_sign=prop.lxor(sign_0, sign_1);
846 
847  for(std::size_t i=0; i<res.size(); i++)
848  res[i]=prop.lselect(result_sign, neg_res[i], res[i]);
849 
850  for(std::size_t i=0; i<res.size(); i++)
851  rem[i]=prop.lselect(sign_0, neg_rem[i], rem[i]);
852 }
853 
855  const bvt &op0,
856  const bvt &op1,
857  bvt &result,
858  bvt &remainer,
859  representationt rep)
860 {
861  assert(prop.has_set_to());
862 
863  switch(rep)
864  {
866  signed_divider(op0, op1, result, remainer); break;
868  unsigned_divider(op0, op1, result, remainer); break;
869  default: assert(false);
870  }
871 }
872 
874  const bvt &op0,
875  const bvt &op1,
876  bvt &res,
877  bvt &rem)
878 {
879  std::size_t width=op0.size();
880 
881  // check if we divide by a power of two
882  #if 0
883  {
884  std::size_t one_count=0, non_const_count=0, one_pos=0;
885 
886  for(std::size_t i=0; i<op1.size(); i++)
887  {
888  literalt l=op1[i];
889  if(l.is_true())
890  {
891  one_count++;
892  one_pos=i;
893  }
894  else if(!l.is_false())
895  non_const_count++;
896  }
897 
898  if(non_const_count==0 && one_count==1 && one_pos!=0)
899  {
900  // it is a power of two!
901  res=shift(op0, LRIGHT, one_pos);
902 
903  // remainder is just a mask
904  rem=op0;
905  for(std::size_t i=one_pos; i<rem.size(); i++)
906  rem[i]=const_literal(false);
907  return;
908  }
909  }
910  #endif
911 
912  // Division by zero test.
913  // Note that we produce a non-deterministic result in
914  // case of division by zero. SMT-LIB now says the following:
915  // bvudiv returns a vector of all 1s if the second operand is 0
916  // bvurem returns its first operand if the second operand is 0
917 
919 
920  // free variables for result of division
921 
922  res.resize(width);
923  rem.resize(width);
924  for(std::size_t i=0; i<width; i++)
925  {
926  res[i]=prop.new_variable();
927  rem[i]=prop.new_variable();
928  }
929 
930  // add implications
931 
932  bvt product=
934 
935  // res*op1 + rem = op0
936 
937  bvt sum=product;
938 
939  adder_no_overflow(sum, rem);
940 
941  literalt is_equal=equal(sum, op0);
942 
944 
945  // op1!=0 => rem < op1
946 
948  prop.limplies(
949  is_not_zero, lt_or_le(false, rem, op1, representationt::UNSIGNED)));
950 
951  // op1!=0 => res <= op0
952 
954  prop.limplies(
955  is_not_zero, lt_or_le(true, res, op0, representationt::UNSIGNED)));
956 }
957 
958 
959 #ifdef COMPACT_EQUAL_CONST
960 // TODO : use for lt_or_le as well
961 
965 void bv_utilst::equal_const_register(const bvt &var)
966 {
967  assert(!is_constant(var));
968  equal_const_registered.insert(var);
969  return;
970 }
971 
972 
979 literalt bv_utilst::equal_const_rec(bvt &var, bvt &constant)
980 {
981  std::size_t size = var.size();
982 
983  assert(size != 0);
984  assert(size == constant.size());
985  assert(is_constant(constant));
986 
987  if(size == 1)
988  {
989  literalt comp = prop.lequal(var[size - 1], constant[size - 1]);
990  var.pop_back();
991  constant.pop_back();
992  return comp;
993  }
994  else
995  {
996  var_constant_pairt index(var, constant);
997 
998  equal_const_cachet::iterator entry = equal_const_cache.find(index);
999 
1000  if(entry != equal_const_cache.end())
1001  {
1002  return entry->second;
1003  }
1004  else
1005  {
1006  literalt comp = prop.lequal(var[size - 1], constant[size - 1]);
1007  var.pop_back();
1008  constant.pop_back();
1009 
1010  literalt rec = equal_const_rec(var, constant);
1011  literalt compare = prop.land(rec, comp);
1012 
1013  equal_const_cache.insert(
1014  std::pair<var_constant_pairt, literalt>(index, compare));
1015 
1016  return compare;
1017  }
1018  }
1019 }
1020 
1029 literalt bv_utilst::equal_const(const bvt &var, const bvt &constant)
1030 {
1031  std::size_t size = constant.size();
1032 
1033  assert(var.size() == size);
1034  assert(!is_constant(var));
1035  assert(is_constant(constant));
1036  assert(size >= 2);
1037 
1038  // These get modified : be careful!
1039  bvt var_upper;
1040  bvt var_lower;
1041  bvt constant_upper;
1042  bvt constant_lower;
1043 
1044  /* Split the constant based on a change in parity
1045  * This is based on the observation that most constants are small,
1046  * so combinations of the lower bits are heavily used but the upper
1047  * bits are almost always either all 0 or all 1.
1048  */
1049  literalt top_bit = constant[size - 1];
1050 
1051  std::size_t split = size - 1;
1052  var_upper.push_back(var[size - 1]);
1053  constant_upper.push_back(constant[size - 1]);
1054 
1055  for(split = size - 2; split != 0; --split)
1056  {
1057  if(constant[split] != top_bit)
1058  {
1059  break;
1060  }
1061  else
1062  {
1063  var_upper.push_back(var[split]);
1064  constant_upper.push_back(constant[split]);
1065  }
1066  }
1067 
1068  for(std::size_t i = 0; i <= split; ++i)
1069  {
1070  var_lower.push_back(var[i]);
1071  constant_lower.push_back(constant[i]);
1072  }
1073 
1074  // Check we have split the array correctly
1075  assert(var_upper.size() + var_lower.size() == size);
1076  assert(constant_upper.size() + constant_lower.size() == size);
1077 
1078  literalt top_comparison = equal_const_rec(var_upper, constant_upper);
1079  literalt bottom_comparison = equal_const_rec(var_lower, constant_lower);
1080 
1081  return prop.land(top_comparison, bottom_comparison);
1082 }
1083 
1084 #endif
1085 
1089 literalt bv_utilst::equal(const bvt &op0, const bvt &op1)
1090 {
1091  assert(op0.size()==op1.size());
1092 
1093  #ifdef COMPACT_EQUAL_CONST
1094  // simplify_expr should put the constant on the right
1095  // but bit-level simplification may result in the other cases
1096  if(is_constant(op0) && !is_constant(op1) && op0.size() > 2 &&
1097  equal_const_registered.find(op1) != equal_const_registered.end())
1098  return equal_const(op1, op0);
1099  else if(!is_constant(op0) && is_constant(op1) && op0.size() > 2 &&
1100  equal_const_registered.find(op0) != equal_const_registered.end())
1101  return equal_const(op0, op1);
1102  #endif
1103 
1104  bvt equal_bv;
1105  equal_bv.resize(op0.size());
1106 
1107  for(std::size_t i=0; i<op0.size(); i++)
1108  equal_bv[i]=prop.lequal(op0[i], op1[i]);
1109 
1110  return prop.land(equal_bv);
1111 }
1112 
1117 /* Some clauses are not needed for correctness but they remove
1118  models (effectively setting "don't care" bits) and so may be worth
1119  including.*/
1120 // #define INCLUDE_REDUNDANT_CLAUSES
1121 
1122 // Saves space but slows the solver
1123 // There is a variant that uses the xor as an auxiliary that should improve both
1124 // #define COMPACT_LT_OR_LE
1125 
1126 
1127 
1129  bool or_equal,
1130  const bvt &bv0,
1131  const bvt &bv1,
1132  representationt rep)
1133 {
1134  assert(bv0.size() == bv1.size());
1135 
1136  literalt top0=bv0[bv0.size()-1],
1137  top1=bv1[bv1.size()-1];
1138 
1139 #ifdef COMPACT_LT_OR_LE
1141  {
1142  bvt compareBelow; // 1 if a compare is needed below this bit
1143  literalt result;
1144  size_t start;
1145  size_t i;
1146 
1147  compareBelow.resize(bv0.size());
1148  Forall_literals(it, compareBelow) { (*it) = prop.new_variable(); }
1149  result = prop.new_variable();
1150 
1151  if(rep==SIGNED)
1152  {
1153  assert(bv0.size() >= 2);
1154  start = compareBelow.size() - 2;
1155 
1156  literalt firstComp=compareBelow[start];
1157 
1158  // When comparing signs we are comparing the top bit
1159 #ifdef INCLUDE_REDUNDANT_CLAUSES
1160  prop.l_set_to_true(compareBelow[start + 1])
1161 #endif
1162 
1163  // Four cases...
1164  prop.lcnf(top0, top1, firstComp); // + + compare needed
1165  prop.lcnf(top0, !top1, !result); // + - result false and no compare needed
1166  prop.lcnf(!top0, top1, result); // - + result true and no compare needed
1167  prop.lcnf(!top0, !top1, firstComp); // - - negated compare needed
1168 
1169 #ifdef INCLUDE_REDUNDANT_CLAUSES
1170  prop.lcnf(top0, !top1, !firstComp);
1171  prop.lcnf(!top0, top1, !firstComp);
1172 #endif
1173  }
1174  else
1175  {
1176  // Unsigned is much easier
1177  start = compareBelow.size() - 1;
1178  prop.l_set_to_true(compareBelow[start]);
1179  }
1180 
1181  // Determine the output
1182  // \forall i . cb[i] & -a[i] & b[i] => result
1183  // \forall i . cb[i] & a[i] & -b[i] => -result
1184  i = start;
1185  do
1186  {
1187  prop.lcnf(!compareBelow[i], bv0[i], !bv1[i], result);
1188  prop.lcnf(!compareBelow[i], !bv0[i], bv1[i], !result);
1189  }
1190  while(i-- != 0);
1191 
1192  // Chain the comparison bit
1193  // \forall i != 0 . cb[i] & a[i] & b[i] => cb[i-1]
1194  // \forall i != 0 . cb[i] & -a[i] & -b[i] => cb[i-1]
1195  for(i = start; i > 0; i--)
1196  {
1197  prop.lcnf(!compareBelow[i], !bv0[i], !bv1[i], compareBelow[i-1]);
1198  prop.lcnf(!compareBelow[i], bv0[i], bv1[i], compareBelow[i-1]);
1199  }
1200 
1201 
1202 #ifdef INCLUDE_REDUNDANT_CLAUSES
1203  // Optional zeroing of the comparison bit when not needed
1204  // \forall i != 0 . -c[i] => -c[i-1]
1205  // \forall i != 0 . c[i] & -a[i] & b[i] => -c[i-1]
1206  // \forall i != 0 . c[i] & a[i] & -b[i] => -c[i-1]
1207  for(i = start; i > 0; i--)
1208  {
1209  prop.lcnf(compareBelow[i], !compareBelow[i-1]);
1210  prop.lcnf(!compareBelow[i], bv0[i], !bv1[i], !compareBelow[i-1]);
1211  prop.lcnf(!compareBelow[i], !bv0[i], bv1[i], !compareBelow[i-1]);
1212  }
1213 #endif
1214 
1215  // The 'base case' of the induction is the case when they are equal
1216  prop.lcnf(!compareBelow[0], !bv0[0], !bv1[0], (or_equal)?result:!result);
1217  prop.lcnf(!compareBelow[0], bv0[0], bv1[0], (or_equal)?result:!result);
1218 
1219  return result;
1220  }
1221  else
1222 #endif
1223  {
1224  literalt carry=
1225  carry_out(bv0, inverted(bv1), const_literal(true));
1226 
1227  literalt result;
1228 
1229  if(rep==representationt::SIGNED)
1230  result=prop.lxor(prop.lequal(top0, top1), carry);
1231  else if(rep==representationt::UNSIGNED)
1232  result=!carry;
1233  else
1234  assert(false);
1235 
1236  if(or_equal)
1237  result=prop.lor(result, equal(bv0, bv1));
1238 
1239  return result;
1240  }
1241 }
1242 
1244  const bvt &op0,
1245  const bvt &op1)
1246 {
1247 #ifdef COMPACT_LT_OR_LE
1248  return lt_or_le(false, op0, op1, UNSIGNED);
1249 #else
1250  // A <= B iff there is an overflow on A-B
1251  return !carry_out(op0, inverted(op1), const_literal(true));
1252 #endif
1253 }
1254 
1256  const bvt &bv0,
1257  const bvt &bv1)
1258 {
1259  return lt_or_le(false, bv0, bv1, representationt::SIGNED);
1260 }
1261 
1263  const bvt &bv0,
1264  irep_idt id,
1265  const bvt &bv1,
1266  representationt rep)
1267 {
1268  if(id==ID_equal)
1269  return equal(bv0, bv1);
1270  else if(id==ID_notequal)
1271  return !equal(bv0, bv1);
1272  else if(id==ID_le)
1273  return lt_or_le(true, bv0, bv1, rep);
1274  else if(id==ID_lt)
1275  return lt_or_le(false, bv0, bv1, rep);
1276  else if(id==ID_ge)
1277  return lt_or_le(true, bv1, bv0, rep); // swapped
1278  else if(id==ID_gt)
1279  return lt_or_le(false, bv1, bv0, rep); // swapped
1280  else
1281  assert(false);
1282 }
1283 
1285 {
1286  forall_literals(it, bv)
1287  if(!it->is_constant())
1288  return false;
1289 
1290  return true;
1291 }
1292 
1294  literalt cond,
1295  const bvt &a,
1296  const bvt &b)
1297 {
1298  assert(a.size()==b.size());
1299 
1300  if(prop.cnf_handled_well())
1301  {
1302  for(std::size_t i=0; i<a.size(); i++)
1303  {
1304  prop.lcnf(!cond, a[i], !b[i]);
1305  prop.lcnf(!cond, !a[i], b[i]);
1306  }
1307  }
1308  else
1309  {
1310  prop.limplies(cond, equal(a, b));
1311  }
1312 
1313  return;
1314 }
1315 
1317 {
1318  bvt odd_bits;
1319  odd_bits.reserve(src.size()/2);
1320 
1321  // check every odd bit
1322  for(std::size_t i=0; i<src.size(); i++)
1323  {
1324  if(i%2!=0)
1325  odd_bits.push_back(src[i]);
1326  }
1327 
1328  return prop.lor(odd_bits);
1329 }
1330 
1332 {
1333  bvt even_bits;
1334  even_bits.reserve(src.size()/2);
1335 
1336  // get every even bit
1337  for(std::size_t i=0; i<src.size(); i++)
1338  {
1339  if(i%2==0)
1340  even_bits.push_back(src[i]);
1341  }
1342 
1343  return even_bits;
1344 }
bvt wallace_tree(const std::vector< bvt > &pps)
Definition: bv_utils.cpp:569
propt & prop
Definition: bv_utils.h:217
bvt inverted(const bvt &op)
Definition: bv_utils.cpp:561
bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
Definition: bv_utils.cpp:109
bvt multiplier_no_overflow(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:804
BigInt mp_integer
Definition: mp_arith.h:19
static bvt extract(const bvt &a, std::size_t first, std::size_t last)
Definition: bv_utils.cpp:42
void lcnf(literalt l0, literalt l1)
Definition: prop.h:53
literalt is_int_min(const bvt &op)
Definition: bv_utils.h:143
bvt cond_negate(const bvt &bv, const literalt cond)
Definition: bv_utils.cpp:741
bvt add_sub_no_overflow(const bvt &op0, const bvt &op1, bool subtract, representationt rep)
Definition: bv_utils.cpp:328
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.h:83
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1089
virtual literalt lor(literalt a, literalt b)=0
representationt
Definition: bv_utils.h:31
void adder(bvt &sum, const bvt &op, literalt carry_in, literalt &carry_out)
Definition: bv_utils.cpp:297
bool is_constant(const bvt &bv)
Definition: bv_utils.cpp:1284
literalt is_zero(const bvt &op)
Definition: bv_utils.h:137
bvt unsigned_multiplier_no_overflow(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:684
#define forall_literals(it, bv)
Definition: literal.h:199
virtual literalt limplies(literalt a, literalt b)=0
void l_set_to_true(literalt a)
Definition: prop.h:47
bvt signed_multiplier_no_overflow(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:769
virtual void set_equal(literalt a, literalt b)
asserts a==b in the propositional formula
Definition: prop.cpp:14
virtual literalt land(literalt a, literalt b)=0
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:1128
virtual literalt new_variable()=0
#define Forall_literals(it, bv)
Definition: literal.h:203
literalt overflow_negate(const bvt &op)
Definition: bv_utils.cpp:527
void adder_no_overflow(bvt &sum, const bvt &op, bool subtract, representationt rep)
Definition: bv_utils.cpp:416
bvt concatenate(const bvt &a, const bvt &b) const
Definition: bv_utils.cpp:80
bvt signed_multiplier(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:723
virtual void l_set_to(literalt a, bool value)
Definition: prop.h:42
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
Definition: bv_utils.cpp:1262
bvt negate(const bvt &op)
Definition: bv_utils.cpp:513
virtual literalt lxor(literalt a, literalt b)=0
bool is_true() const
Definition: literal.h:155
literalt is_not_zero(const bvt &op)
Definition: bv_utils.h:140
static bvt extract_msb(const bvt &a, std::size_t n)
Definition: bv_utils.cpp:58
literalt full_adder(const literalt a, const literalt b, const literalt carry_in, literalt &carry_out)
Definition: bv_utils.cpp:140
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:791
void signed_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
Definition: bv_utils.cpp:819
void l_set_to_false(literalt a)
Definition: prop.h:49
virtual bool cnf_handled_well() const
Definition: prop.h:80
bvt absolute_value(const bvt &op)
Definition: bv_utils.cpp:754
bvt unsigned_multiplier(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:614
literalt signed_less_than(const bvt &bv0, const bvt &bv1)
Definition: bv_utils.cpp:1255
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
Definition: bv_utils.cpp:96
void set_equal(const bvt &a, const bvt &b)
Definition: bv_utils.cpp:35
literalt verilog_bv_has_x_or_z(const bvt &)
Definition: bv_utils.cpp:1316
bvt verilog_bv_normal_bits(const bvt &)
Definition: bv_utils.cpp:1331
void unsigned_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
Definition: bv_utils.cpp:873
bvt incrementer(const bvt &op, literalt carry_in)
Definition: bv_utils.cpp:553
virtual literalt lequal(literalt a, literalt b)=0
bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
Definition: bv_utils.cpp:480
literalt unsigned_less_than(const bvt &bv0, const bvt &bv1)
Definition: bv_utils.cpp:1243
literalt const_literal(bool value)
Definition: literal.h:187
bvt add(const bvt &op0, const bvt &op1)
Definition: bv_utils.h:64
literalt is_one(const bvt &op)
Definition: bv_utils.cpp:26
bvt cond_negate_no_overflow(const bvt &bv, const literalt cond)
Definition: bv_utils.cpp:760
bool is_constant() const
Definition: literal.h:165
static bvt extract_lsb(const bvt &a, std::size_t n)
Definition: bv_utils.cpp:70
virtual bool has_set_to() const
Definition: prop.h:76
bvt negate_no_overflow(const bvt &op)
Definition: bv_utils.cpp:521
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:63
literalt carry_out(const bvt &op0, const bvt &op1, literalt carry_in)
Definition: bv_utils.cpp:313
void cond_implies_equal(literalt cond, const bvt &a, const bvt &b)
Definition: bv_utils.cpp:1293
literalt carry(literalt a, literalt b, literalt c)
Definition: bv_utils.cpp:231
literalt overflow_sub(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:391
virtual literalt lselect(literalt a, literalt b, literalt c)=0
literalt overflow_add(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:367
bvt add_sub(const bvt &op0, const bvt &op1, bool subtract)
Definition: bv_utils.cpp:339
std::vector< literalt > bvt
Definition: literal.h:197
bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:15
bvt zeros(std::size_t new_size) const
Definition: bv_utils.h:185
bool is_false() const
Definition: literal.h:160