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  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  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  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 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  // 'dist' is user-controlled, and thus arbitary.
486  // We thus must guard against the case in which i+dist overflows.
487  // We do so by considering the case dist>=src.size().
488 
489  for(std::size_t i=0; i<src.size(); i++)
490  {
491  literalt l;
492 
493  switch(s)
494  {
495  case shiftt::SHIFT_LEFT:
496  // no underflow on i-dist because of condition dist<=i
497  l=(dist<=i?src[i-dist]:const_literal(false));
498  break;
499 
501  // src.size()-i won't underflow as i<src.size()
502  // Then, if dist<src.size()-i, then i+dist<src.size()
503  l=(dist<src.size()-i?src[i+dist]:src[src.size()-1]); // sign bit
504  break;
505 
507  // src.size()-i won't underflow as i<src.size()
508  // Then, if dist<src.size()-i, then i+dist<src.size()
509  l=(dist<src.size()-i?src[i+dist]:const_literal(false));
510  break;
511 
512  case shiftt::ROTATE_LEFT:
513  // prevent overflows by using dist%src.size()
514  l=src[(src.size()+i-(dist%src.size()))%src.size()];
515  break;
516 
518  // prevent overflows by using dist%src.size()
519  l=src[(i+(dist%src.size()))%src.size()];
520  break;
521 
522  default:
523  UNREACHABLE;
524  }
525 
526  result[i]=l;
527  }
528 
529  return result;
530 }
531 
533 {
534  bvt result=inverted(bv);
536  incrementer(result, const_literal(true), carry_out);
537  return result;
538 }
539 
541 {
542  prop.l_set_to(overflow_negate(bv), false);
543  return negate(bv);
544 }
545 
547 {
548  // a overflow on unary- can only happen with the smallest
549  // representable number 100....0
550 
551  bvt zeros(bv);
552  zeros.erase(--zeros.end());
553 
554  return prop.land(bv[bv.size()-1], !prop.lor(zeros));
555 }
556 
558  bvt &bv,
559  literalt carry_in,
560  literalt &carry_out)
561 {
562  carry_out=carry_in;
563 
564  Forall_literals(it, bv)
565  {
566  literalt new_carry=prop.land(carry_out, *it);
567  *it=prop.lxor(*it, carry_out);
568  carry_out=new_carry;
569  }
570 }
571 
573 {
574  bvt result=bv;
576  incrementer(result, carry_in, carry_out);
577  return result;
578 }
579 
581 {
582  bvt result=bv;
583  Forall_literals(it, result)
584  *it=!*it;
585  return result;
586 }
587 
588 bvt bv_utilst::wallace_tree(const std::vector<bvt> &pps)
589 {
590  assert(!pps.empty());
591 
592  if(pps.size()==1)
593  return pps.front();
594  else if(pps.size()==2)
595  return add(pps[0], pps[1]);
596  else
597  {
598  std::vector<bvt> new_pps;
599  std::size_t no_full_adders=pps.size()/3;
600 
601  // add groups of three partial products using CSA
602  for(std::size_t i=0; i<no_full_adders; i++)
603  {
604  const bvt &a=pps[i*3+0],
605  &b=pps[i*3+1],
606  &c=pps[i*3+2];
607 
608  assert(a.size()==b.size() && a.size()==c.size());
609 
610  bvt s(a.size()), t(a.size());
611 
612  for(std::size_t bit=0; bit<a.size(); bit++)
613  {
614  // \todo reformulate using full_adder
615  s[bit]=prop.lxor(a[bit], prop.lxor(b[bit], c[bit]));
616  t[bit]=(bit==0)?const_literal(false):
617  carry(a[bit-1], b[bit-1], c[bit-1]);
618  }
619 
620  new_pps.push_back(s);
621  new_pps.push_back(t);
622  }
623 
624  // pass onwards up to two remaining partial products
625  for(std::size_t i=no_full_adders*3; i<pps.size(); i++)
626  new_pps.push_back(pps[i]);
627 
628  assert(new_pps.size()<pps.size());
629  return wallace_tree(new_pps);
630  }
631 }
632 
633 bvt bv_utilst::unsigned_multiplier(const bvt &_op0, const bvt &_op1)
634 {
635  #if 1
636  bvt op0=_op0, op1=_op1;
637 
638  if(is_constant(op1))
639  std::swap(op0, op1);
640 
641  bvt product;
642  product.resize(op0.size());
643 
644  for(std::size_t i=0; i<product.size(); i++)
645  product[i]=const_literal(false);
646 
647  for(std::size_t sum=0; sum<op0.size(); sum++)
648  if(op0[sum]!=const_literal(false))
649  {
650  bvt tmpop;
651 
652  tmpop.reserve(op0.size());
653 
654  for(std::size_t idx=0; idx<sum; idx++)
655  tmpop.push_back(const_literal(false));
656 
657  for(std::size_t idx=sum; idx<op0.size(); idx++)
658  tmpop.push_back(prop.land(op1[idx-sum], op0[sum]));
659 
660  product=add(product, tmpop);
661  }
662 
663  return product;
664  #else
665  // Wallace tree multiplier. This is disabled, as runtimes have
666  // been observed to go up by 5%-10%, and on some models even by 20%.
667 
668  // build the usual quadratic number of partial products
669 
670  bvt op0=_op0, op1=_op1;
671 
672  if(is_constant(op1))
673  std::swap(op0, op1);
674 
675  std::vector<bvt> pps;
676  pps.reserve(op0.size());
677 
678  for(std::size_t bit=0; bit<op0.size(); bit++)
679  if(op0[bit]!=const_literal(false))
680  {
681  bvt pp;
682 
683  pp.reserve(op0.size());
684 
685  // zeros according to weight
686  for(std::size_t idx=0; idx<bit; idx++)
687  pp.push_back(const_literal(false));
688 
689  for(std::size_t idx=bit; idx<op0.size(); idx++)
690  pp.push_back(prop.land(op1[idx-bit], op0[bit]));
691 
692  pps.push_back(pp);
693  }
694 
695  if(pps.empty())
696  return zeros(op0.size());
697  else
698  return wallace_tree(pps);
699 
700  #endif
701 }
702 
704  const bvt &op0,
705  const bvt &op1)
706 {
707  bvt _op0=op0, _op1=op1;
708 
709  if(is_constant(_op1))
710  _op0.swap(_op1);
711 
712  assert(_op0.size()==_op1.size());
713 
714  bvt product;
715  product.resize(_op0.size());
716 
717  for(std::size_t i=0; i<product.size(); i++)
718  product[i]=const_literal(false);
719 
720  for(std::size_t sum=0; sum<op0.size(); sum++)
721  if(op0[sum]!=const_literal(false))
722  {
723  bvt tmpop;
724 
725  tmpop.reserve(product.size());
726 
727  for(std::size_t idx=0; idx<sum; idx++)
728  tmpop.push_back(const_literal(false));
729 
730  for(std::size_t idx=sum; idx<product.size(); idx++)
731  tmpop.push_back(prop.land(op1[idx-sum], op0[sum]));
732 
733  adder_no_overflow(product, tmpop);
734 
735  for(std::size_t idx=op1.size()-sum; idx<op1.size(); idx++)
736  prop.l_set_to_false(prop.land(op1[idx], op0[sum]));
737  }
738 
739  return product;
740 }
741 
742 bvt bv_utilst::signed_multiplier(const bvt &op0, const bvt &op1)
743 {
744  if(op0.empty() || op1.empty())
745  return bvt();
746 
747  literalt sign0=op0[op0.size()-1];
748  literalt sign1=op1[op1.size()-1];
749 
750  bvt neg0=cond_negate(op0, sign0);
751  bvt neg1=cond_negate(op1, sign1);
752 
753  bvt result=unsigned_multiplier(neg0, neg1);
754 
755  literalt result_sign=prop.lxor(sign0, sign1);
756 
757  return cond_negate(result, result_sign);
758 }
759 
760 bvt bv_utilst::cond_negate(const bvt &bv, const literalt cond)
761 {
762  bvt neg_bv=negate(bv);
763 
764  bvt result;
765  result.resize(bv.size());
766 
767  for(std::size_t i=0; i<bv.size(); i++)
768  result[i]=prop.lselect(cond, neg_bv[i], bv[i]);
769 
770  return result;
771 }
772 
774 {
775  assert(!bv.empty());
776  return cond_negate(bv, bv[bv.size()-1]);
777 }
778 
780 {
781  prop.l_set_to(
782  prop.limplies(cond, !overflow_negate(bv)),
783  true);
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(result[result.size()-1], false);
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  default: UNREACHABLE;
820  }
821 }
822 
824  const bvt &op0,
825  const bvt &op1,
826  representationt rep)
827 {
828  switch(rep)
829  {
831  return signed_multiplier_no_overflow(op0, op1);
833  return unsigned_multiplier_no_overflow(op0, op1);
834  default: UNREACHABLE;
835  }
836 }
837 
839  const bvt &op0,
840  const bvt &op1,
841  bvt &res,
842  bvt &rem)
843 {
844  if(op0.empty() || op1.empty())
845  return;
846 
847  bvt _op0(op0), _op1(op1);
848 
849  literalt sign_0=_op0[_op0.size()-1];
850  literalt sign_1=_op1[_op1.size()-1];
851 
852  bvt neg_0=negate(_op0), neg_1=negate(_op1);
853 
854  for(std::size_t i=0; i<_op0.size(); i++)
855  _op0[i]=(prop.lselect(sign_0, neg_0[i], _op0[i]));
856 
857  for(std::size_t i=0; i<_op1.size(); i++)
858  _op1[i]=(prop.lselect(sign_1, neg_1[i], _op1[i]));
859 
860  unsigned_divider(_op0, _op1, res, rem);
861 
862  bvt neg_res=negate(res), neg_rem=negate(rem);
863 
864  literalt result_sign=prop.lxor(sign_0, sign_1);
865 
866  for(std::size_t i=0; i<res.size(); i++)
867  res[i]=prop.lselect(result_sign, neg_res[i], res[i]);
868 
869  for(std::size_t i=0; i<res.size(); i++)
870  rem[i]=prop.lselect(sign_0, neg_rem[i], rem[i]);
871 }
872 
874  const bvt &op0,
875  const bvt &op1,
876  bvt &result,
877  bvt &remainer,
878  representationt rep)
879 {
880  assert(prop.has_set_to());
881 
882  switch(rep)
883  {
885  signed_divider(op0, op1, result, remainer); break;
887  unsigned_divider(op0, op1, result, remainer); break;
888  default: assert(false);
889  }
890 }
891 
893  const bvt &op0,
894  const bvt &op1,
895  bvt &res,
896  bvt &rem)
897 {
898  std::size_t width=op0.size();
899 
900  // check if we divide by a power of two
901  #if 0
902  {
903  std::size_t one_count=0, non_const_count=0, one_pos=0;
904 
905  for(std::size_t i=0; i<op1.size(); i++)
906  {
907  literalt l=op1[i];
908  if(l.is_true())
909  {
910  one_count++;
911  one_pos=i;
912  }
913  else if(!l.is_false())
914  non_const_count++;
915  }
916 
917  if(non_const_count==0 && one_count==1 && one_pos!=0)
918  {
919  // it is a power of two!
920  res=shift(op0, LRIGHT, one_pos);
921 
922  // remainder is just a mask
923  rem=op0;
924  for(std::size_t i=one_pos; i<rem.size(); i++)
925  rem[i]=const_literal(false);
926  return;
927  }
928  }
929  #endif
930 
931  // Division by zero test.
932  // Note that we produce a non-deterministic result in
933  // case of division by zero. SMT-LIB now says the following:
934  // bvudiv returns a vector of all 1s if the second operand is 0
935  // bvurem returns its first operand if the second operand is 0
936 
938 
939  // free variables for result of division
940 
941  res.resize(width);
942  rem.resize(width);
943  for(std::size_t i=0; i<width; i++)
944  {
945  res[i]=prop.new_variable();
946  rem[i]=prop.new_variable();
947  }
948 
949  // add implications
950 
951  bvt product=
953 
954  // res*op1 + rem = op0
955 
956  bvt sum=product;
957 
958  adder_no_overflow(sum, rem);
959 
960  literalt is_equal=equal(sum, op0);
961 
963 
964  // op1!=0 => rem < op1
965 
967  prop.limplies(
968  is_not_zero, lt_or_le(false, rem, op1, representationt::UNSIGNED)));
969 
970  // op1!=0 => res <= op0
971 
973  prop.limplies(
974  is_not_zero, lt_or_le(true, res, op0, representationt::UNSIGNED)));
975 }
976 
977 
978 #ifdef COMPACT_EQUAL_CONST
979 // TODO : use for lt_or_le as well
980 
984 void bv_utilst::equal_const_register(const bvt &var)
985 {
986  assert(!is_constant(var));
987  equal_const_registered.insert(var);
988  return;
989 }
990 
991 
998 literalt bv_utilst::equal_const_rec(bvt &var, bvt &constant)
999 {
1000  std::size_t size = var.size();
1001 
1002  assert(size != 0);
1003  assert(size == constant.size());
1004  assert(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  assert(var.size() == size);
1053  assert(!is_constant(var));
1054  assert(is_constant(constant));
1055  assert(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  assert(var_upper.size() + var_lower.size() == size);
1095  assert(constant_upper.size() + constant_lower.size() == size);
1096 
1097  literalt top_comparison = equal_const_rec(var_upper, constant_upper);
1098  literalt bottom_comparison = equal_const_rec(var_lower, constant_lower);
1099 
1100  return prop.land(top_comparison, bottom_comparison);
1101 }
1102 
1103 #endif
1104 
1108 literalt bv_utilst::equal(const bvt &op0, const bvt &op1)
1109 {
1110  assert(op0.size()==op1.size());
1111 
1112  #ifdef COMPACT_EQUAL_CONST
1113  // simplify_expr should put the constant on the right
1114  // but bit-level simplification may result in the other cases
1115  if(is_constant(op0) && !is_constant(op1) && op0.size() > 2 &&
1116  equal_const_registered.find(op1) != equal_const_registered.end())
1117  return equal_const(op1, op0);
1118  else if(!is_constant(op0) && is_constant(op1) && op0.size() > 2 &&
1119  equal_const_registered.find(op0) != equal_const_registered.end())
1120  return equal_const(op0, op1);
1121  #endif
1122 
1123  bvt equal_bv;
1124  equal_bv.resize(op0.size());
1125 
1126  for(std::size_t i=0; i<op0.size(); i++)
1127  equal_bv[i]=prop.lequal(op0[i], op1[i]);
1128 
1129  return prop.land(equal_bv);
1130 }
1131 
1136 /* Some clauses are not needed for correctness but they remove
1137  models (effectively setting "don't care" bits) and so may be worth
1138  including.*/
1139 // #define INCLUDE_REDUNDANT_CLAUSES
1140 
1141 // Saves space but slows the solver
1142 // There is a variant that uses the xor as an auxiliary that should improve both
1143 // #define COMPACT_LT_OR_LE
1144 
1145 
1146 
1148  bool or_equal,
1149  const bvt &bv0,
1150  const bvt &bv1,
1151  representationt rep)
1152 {
1153  assert(bv0.size() == bv1.size());
1154 
1155  literalt top0=bv0[bv0.size()-1],
1156  top1=bv1[bv1.size()-1];
1157 
1158 #ifdef COMPACT_LT_OR_LE
1160  {
1161  bvt compareBelow; // 1 if a compare is needed below this bit
1162  literalt result;
1163  size_t start;
1164  size_t i;
1165 
1166  compareBelow.resize(bv0.size());
1167  Forall_literals(it, compareBelow) { (*it) = prop.new_variable(); }
1168  result = prop.new_variable();
1169 
1170  if(rep==SIGNED)
1171  {
1172  assert(bv0.size() >= 2);
1173  start = compareBelow.size() - 2;
1174 
1175  literalt firstComp=compareBelow[start];
1176 
1177  // When comparing signs we are comparing the top bit
1178 #ifdef INCLUDE_REDUNDANT_CLAUSES
1179  prop.l_set_to_true(compareBelow[start + 1])
1180 #endif
1181 
1182  // Four cases...
1183  prop.lcnf(top0, top1, firstComp); // + + compare needed
1184  prop.lcnf(top0, !top1, !result); // + - result false and no compare needed
1185  prop.lcnf(!top0, top1, result); // - + result true and no compare needed
1186  prop.lcnf(!top0, !top1, firstComp); // - - negated compare needed
1187 
1188 #ifdef INCLUDE_REDUNDANT_CLAUSES
1189  prop.lcnf(top0, !top1, !firstComp);
1190  prop.lcnf(!top0, top1, !firstComp);
1191 #endif
1192  }
1193  else
1194  {
1195  // Unsigned is much easier
1196  start = compareBelow.size() - 1;
1197  prop.l_set_to_true(compareBelow[start]);
1198  }
1199 
1200  // Determine the output
1201  // \forall i . cb[i] & -a[i] & b[i] => result
1202  // \forall i . cb[i] & a[i] & -b[i] => -result
1203  i = start;
1204  do
1205  {
1206  prop.lcnf(!compareBelow[i], bv0[i], !bv1[i], result);
1207  prop.lcnf(!compareBelow[i], !bv0[i], bv1[i], !result);
1208  }
1209  while(i-- != 0);
1210 
1211  // Chain the comparison bit
1212  // \forall i != 0 . cb[i] & a[i] & b[i] => cb[i-1]
1213  // \forall i != 0 . cb[i] & -a[i] & -b[i] => cb[i-1]
1214  for(i = start; i > 0; i--)
1215  {
1216  prop.lcnf(!compareBelow[i], !bv0[i], !bv1[i], compareBelow[i-1]);
1217  prop.lcnf(!compareBelow[i], bv0[i], bv1[i], compareBelow[i-1]);
1218  }
1219 
1220 
1221 #ifdef INCLUDE_REDUNDANT_CLAUSES
1222  // Optional zeroing of the comparison bit when not needed
1223  // \forall i != 0 . -c[i] => -c[i-1]
1224  // \forall i != 0 . c[i] & -a[i] & b[i] => -c[i-1]
1225  // \forall i != 0 . c[i] & a[i] & -b[i] => -c[i-1]
1226  for(i = start; i > 0; i--)
1227  {
1228  prop.lcnf(compareBelow[i], !compareBelow[i-1]);
1229  prop.lcnf(!compareBelow[i], bv0[i], !bv1[i], !compareBelow[i-1]);
1230  prop.lcnf(!compareBelow[i], !bv0[i], bv1[i], !compareBelow[i-1]);
1231  }
1232 #endif
1233 
1234  // The 'base case' of the induction is the case when they are equal
1235  prop.lcnf(!compareBelow[0], !bv0[0], !bv1[0], (or_equal)?result:!result);
1236  prop.lcnf(!compareBelow[0], bv0[0], bv1[0], (or_equal)?result:!result);
1237 
1238  return result;
1239  }
1240  else
1241 #endif
1242  {
1243  literalt carry=
1244  carry_out(bv0, inverted(bv1), const_literal(true));
1245 
1246  literalt result;
1247 
1248  if(rep==representationt::SIGNED)
1249  result=prop.lxor(prop.lequal(top0, top1), carry);
1250  else if(rep==representationt::UNSIGNED)
1251  result=!carry;
1252  else
1253  assert(false);
1254 
1255  if(or_equal)
1256  result=prop.lor(result, equal(bv0, bv1));
1257 
1258  return result;
1259  }
1260 }
1261 
1263  const bvt &op0,
1264  const bvt &op1)
1265 {
1266 #ifdef COMPACT_LT_OR_LE
1267  return lt_or_le(false, op0, op1, UNSIGNED);
1268 #else
1269  // A <= B iff there is an overflow on A-B
1270  return !carry_out(op0, inverted(op1), const_literal(true));
1271 #endif
1272 }
1273 
1275  const bvt &bv0,
1276  const bvt &bv1)
1277 {
1278  return lt_or_le(false, bv0, bv1, representationt::SIGNED);
1279 }
1280 
1282  const bvt &bv0,
1283  irep_idt id,
1284  const bvt &bv1,
1285  representationt rep)
1286 {
1287  if(id==ID_equal)
1288  return equal(bv0, bv1);
1289  else if(id==ID_notequal)
1290  return !equal(bv0, bv1);
1291  else if(id==ID_le)
1292  return lt_or_le(true, bv0, bv1, rep);
1293  else if(id==ID_lt)
1294  return lt_or_le(false, bv0, bv1, rep);
1295  else if(id==ID_ge)
1296  return lt_or_le(true, bv1, bv0, rep); // swapped
1297  else if(id==ID_gt)
1298  return lt_or_le(false, bv1, bv0, rep); // swapped
1299  else
1300  UNREACHABLE;
1301 }
1302 
1304 {
1305  forall_literals(it, bv)
1306  if(!it->is_constant())
1307  return false;
1308 
1309  return true;
1310 }
1311 
1313  literalt cond,
1314  const bvt &a,
1315  const bvt &b)
1316 {
1317  assert(a.size()==b.size());
1318 
1319  if(prop.cnf_handled_well())
1320  {
1321  for(std::size_t i=0; i<a.size(); i++)
1322  {
1323  prop.lcnf(!cond, a[i], !b[i]);
1324  prop.lcnf(!cond, !a[i], b[i]);
1325  }
1326  }
1327  else
1328  {
1329  prop.limplies(cond, equal(a, b));
1330  }
1331 
1332  return;
1333 }
1334 
1336 {
1337  bvt odd_bits;
1338  odd_bits.reserve(src.size()/2);
1339 
1340  // check every odd bit
1341  for(std::size_t i=0; i<src.size(); i++)
1342  {
1343  if(i%2!=0)
1344  odd_bits.push_back(src[i]);
1345  }
1346 
1347  return prop.lor(odd_bits);
1348 }
1349 
1351 {
1352  bvt even_bits;
1353  even_bits.reserve(src.size()/2);
1354 
1355  // get every even bit
1356  for(std::size_t i=0; i<src.size(); i++)
1357  {
1358  if(i%2==0)
1359  even_bits.push_back(src[i]);
1360  }
1361 
1362  return even_bits;
1363 }
bvt wallace_tree(const std::vector< bvt > &pps)
Definition: bv_utils.cpp:588
propt & prop
Definition: bv_utils.h:221
bvt inverted(const bvt &op)
Definition: bv_utils.cpp:580
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:823
BigInt mp_integer
Definition: mp_arith.h:22
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:55
literalt is_int_min(const bvt &op)
Definition: bv_utils.h:147
bvt cond_negate(const bvt &bv, const literalt cond)
Definition: bv_utils.cpp:760
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:87
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1108
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:1303
literalt is_zero(const bvt &op)
Definition: bv_utils.h:141
bvt unsigned_multiplier_no_overflow(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:703
#define forall_literals(it, bv)
Definition: literal.h:202
virtual literalt limplies(literalt a, literalt b)=0
void l_set_to_true(literalt a)
Definition: prop.h:49
bvt signed_multiplier_no_overflow(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:788
virtual void set_equal(literalt a, literalt b)
asserts a==b in the propositional formula
Definition: prop.cpp:12
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:1147
virtual literalt new_variable()=0
#define Forall_literals(it, bv)
Definition: literal.h:206
literalt overflow_negate(const bvt &op)
Definition: bv_utils.cpp:546
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:742
virtual void l_set_to(literalt a, bool value)
Definition: prop.h:44
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
Definition: bv_utils.cpp:1281
bvt negate(const bvt &op)
Definition: bv_utils.cpp:532
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:144
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:810
void signed_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
Definition: bv_utils.cpp:838
void l_set_to_false(literalt a)
Definition: prop.h:51
virtual bool cnf_handled_well() const
Definition: prop.h:82
bvt absolute_value(const bvt &op)
Definition: bv_utils.cpp:773
bvt unsigned_multiplier(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:633
literalt signed_less_than(const bvt &bv0, const bvt &bv1)
Definition: bv_utils.cpp:1274
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
literalt verilog_bv_has_x_or_z(const bvt &)
Definition: bv_utils.cpp:1335
bvt verilog_bv_normal_bits(const bvt &)
Definition: bv_utils.cpp:1350
void unsigned_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
Definition: bv_utils.cpp:892
bvt incrementer(const bvt &op, literalt carry_in)
Definition: bv_utils.cpp:572
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:1262
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:779
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:78
bvt negate_no_overflow(const bvt &op)
Definition: bv_utils.cpp:540
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:67
#define UNREACHABLE
Definition: invariant.h:271
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:1312
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:200
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:189
bool is_false() const
Definition: literal.h:160