cprover
simplify_expr_int.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 "simplify_expr_class.h"
10 
11 #include <cassert>
12 
13 #include "base_type.h"
14 #include "rational.h"
15 #include "expr.h"
16 #include "namespace.h"
17 #include "config.h"
18 #include "bv_arithmetic.h"
19 #include "std_expr.h"
20 #include "expr_util.h"
21 #include "arith_tools.h"
22 #include "fixedbv.h"
23 #include "rational_tools.h"
24 #include "ieee_float.h"
25 
27 {
28  if(expr.type().id()==ID_unsignedbv &&
29  expr.operands().size()==1 &&
30  expr.op0().type()==expr.type() &&
31  expr.op0().is_constant())
32  {
33  std::size_t width=to_bitvector_type(expr.type()).get_width();
34  mp_integer value;
35  to_integer(expr.op0(), value);
36  std::vector<mp_integer> bytes;
37 
38  // take apart
39  for(std::size_t bit=0; bit<width; bit+=8)
40  bytes.push_back((value >> bit)%256);
41 
42  // put back together, but backwards
43  mp_integer new_value=0;
44  for(std::size_t bit=0; bit<width; bit+=8)
45  {
46  assert(!bytes.empty());
47  new_value+=bytes.back()<<bit;
48  bytes.pop_back();
49  }
50 
51  expr=from_integer(new_value, expr.type());
52  return false;
53  }
54 
55  return true;
56 }
57 
59 {
60  // check to see if it is a number type
61  if(!is_number(expr.type()))
62  return true;
63 
64  // vector of operands
65  exprt::operandst &operands=expr.operands();
66 
67  // result of the simplification
68  bool result = true;
69 
70  // position of the constant
71  exprt::operandst::iterator constant;
72 
73  // true if we have found a constant
74  bool found = false;
75 
76  typet c_sizeof_type=nil_typet();
77 
78  // scan all the operands
79  for(exprt::operandst::iterator it=operands.begin();
80  it!=operands.end();)
81  {
82  // if one of the operands is not a number return
83  if(!is_number(it->type()))
84  return true;
85 
86  // if one of the operands is zero the result is zero
87  // note: not true on IEEE floating point arithmetic
88  if(it->is_zero() &&
89  it->type().id()!=ID_floatbv)
90  {
91  expr=from_integer(0, expr.type());
92  return false;
93  }
94 
95  // true if the given operand has to be erased
96  bool do_erase = false;
97 
98  // if this is a constant of the same time as the result
99  if(it->is_constant() && it->type()==expr.type())
100  {
101  // preserve the sizeof type annotation
102  if(c_sizeof_type.is_nil())
103  c_sizeof_type=
104  static_cast<const typet &>(it->find(ID_C_c_sizeof_type));
105 
106  if(found)
107  {
108  // update the constant factor
109  if(!constant->mul(*it))
110  do_erase=true;
111  }
112  else
113  {
114  // set it as the constant factor if this is the first
115  constant=it;
116  found=true;
117  }
118  }
119 
120  // erase the factor if necessary
121  if(do_erase)
122  {
123  it=operands.erase(it);
124  result = false;
125  }
126  else
127  it++; // move to the next operand
128  }
129 
130  if(c_sizeof_type.is_not_nil())
131  {
132  assert(found);
133  constant->set(ID_C_c_sizeof_type, c_sizeof_type);
134  }
135 
136  if(operands.size()==1)
137  {
138  exprt product(operands.front());
139  expr.swap(product);
140 
141  result = false;
142  }
143  else
144  {
145  // if the constant is a one and there are other factors
146  if(found && constant->is_one())
147  {
148  // just delete it
149  operands.erase(constant);
150  result=false;
151 
152  if(operands.size()==1)
153  {
154  exprt product(operands.front());
155  expr.swap(product);
156  }
157  }
158  }
159 
160  return result;
161 }
162 
164 {
165  if(!is_number(expr.type()))
166  return true;
167 
168  if(expr.operands().size()!=2)
169  return true;
170 
171  const typet &expr_type=expr.type();
172 
173  if(expr_type!=expr.op0().type() ||
174  expr_type!=expr.op1().type())
175  return true;
176 
177  if(expr_type.id()==ID_signedbv ||
178  expr_type.id()==ID_unsignedbv ||
179  expr_type.id()==ID_natural ||
180  expr_type.id()==ID_integer)
181  {
182  mp_integer int_value0, int_value1;
183  bool ok0, ok1;
184 
185  ok0=!to_integer(expr.op0(), int_value0);
186  ok1=!to_integer(expr.op1(), int_value1);
187 
188  // division by zero?
189  if(ok1 && int_value1==0)
190  return true;
191 
192  // x/1?
193  if(ok1 && int_value1==1)
194  {
195  exprt tmp;
196  tmp.swap(expr.op0());
197  expr.swap(tmp);
198  return false;
199  }
200 
201  // 0/x?
202  if(ok0 && int_value0==0)
203  {
204  exprt tmp;
205  tmp.swap(expr.op0());
206  expr.swap(tmp);
207  return false;
208  }
209 
210  if(ok0 && ok1)
211  {
212  mp_integer result=int_value0/int_value1;
213  exprt tmp=from_integer(result, expr_type);
214 
215  if(tmp.is_not_nil())
216  {
217  expr.swap(tmp);
218  return false;
219  }
220  }
221  }
222  else if(expr_type.id()==ID_rational)
223  {
224  rationalt rat_value0, rat_value1;
225  bool ok0, ok1;
226 
227  ok0=!to_rational(expr.op0(), rat_value0);
228  ok1=!to_rational(expr.op1(), rat_value1);
229 
230  if(ok1 && rat_value1.is_zero())
231  return true;
232 
233  if((ok1 && rat_value1.is_one()) ||
234  (ok0 && rat_value0.is_zero()))
235  {
236  exprt tmp;
237  tmp.swap(expr.op0());
238  expr.swap(tmp);
239  return false;
240  }
241 
242  if(ok0 && ok1)
243  {
244  rationalt result=rat_value0/rat_value1;
245  exprt tmp=from_rational(result);
246 
247  if(tmp.is_not_nil())
248  {
249  expr.swap(tmp);
250  return false;
251  }
252  }
253  }
254  else if(expr_type.id()==ID_fixedbv)
255  {
256  // division by one?
257  if(expr.op1().is_constant() &&
258  expr.op1().is_one())
259  {
260  exprt tmp;
261  tmp.swap(expr.op0());
262  expr.swap(tmp);
263  return false;
264  }
265 
266  if(expr.op0().is_constant() &&
267  expr.op1().is_constant())
268  {
269  fixedbvt f0(to_constant_expr(expr.op0()));
270  fixedbvt f1(to_constant_expr(expr.op1()));
271  if(!f1.is_zero())
272  {
273  f0/=f1;
274  expr=f0.to_expr();
275  return false;
276  }
277  }
278  }
279 
280  return true;
281 }
282 
284 {
285  if(!is_number(expr.type()))
286  return true;
287 
288  if(expr.operands().size()!=2)
289  return true;
290 
291  if(expr.type().id()==ID_signedbv ||
292  expr.type().id()==ID_unsignedbv ||
293  expr.type().id()==ID_natural ||
294  expr.type().id()==ID_integer)
295  {
296  if(expr.type()==expr.op0().type() &&
297  expr.type()==expr.op1().type())
298  {
299  mp_integer int_value0, int_value1;
300  bool ok0, ok1;
301 
302  ok0=!to_integer(expr.op0(), int_value0);
303  ok1=!to_integer(expr.op1(), int_value1);
304 
305  if(ok1 && int_value1==0)
306  return true; // division by zero
307 
308  if((ok1 && int_value1==1) ||
309  (ok0 && int_value0==0))
310  {
311  expr=from_integer(0, expr.type());
312  return false;
313  }
314 
315  if(ok0 && ok1)
316  {
317  mp_integer result=int_value0%int_value1;
318  exprt tmp=from_integer(result, expr.type());
319 
320  if(tmp.is_not_nil())
321  {
322  expr.swap(tmp);
323  return false;
324  }
325  }
326  }
327  }
328 
329  return true;
330 }
331 
333 {
334  if(!is_number(expr.type()) &&
335  expr.type().id()!=ID_pointer)
336  return true;
337 
338  bool result=true;
339 
340  exprt::operandst &operands=expr.operands();
341 
342  assert(expr.id()==ID_plus);
343 
344  // floating-point addition is _NOT_ associative; thus,
345  // there is special case for float
346 
347  if(ns.follow(expr.type()).id()==ID_floatbv)
348  {
349  // we only merge neighboring constants!
350  Forall_expr(it, operands)
351  {
352  exprt::operandst::iterator next=it;
353  next++;
354 
355  if(next!=operands.end())
356  {
357  if(it->type()==next->type() &&
358  it->is_constant() &&
359  next->is_constant())
360  {
361  it->sum(*next);
362  operands.erase(next);
363  }
364  }
365  }
366  }
367  else
368  {
369  // ((T*)p+a)+b -> (T*)p+(a+b)
370  if(expr.type().id()==ID_pointer &&
371  expr.operands().size()==2 &&
372  expr.op0().id()==ID_plus &&
373  expr.op0().operands().size()==2)
374  {
375  exprt op0=expr.op0();
376 
377  if(expr.op0().op1().id()==ID_plus)
378  op0.op1().copy_to_operands(expr.op1());
379  else
380  op0.op1()=plus_exprt(op0.op1(), expr.op1());
381 
382  expr.swap(op0);
383 
384  simplify_plus(expr.op1());
385  simplify_plus(expr);
386 
387  return false;
388  }
389 
390  // count the constants
391  size_t count=0;
392  forall_operands(it, expr)
393  if(is_number(it->type()) && it->is_constant())
394  count++;
395 
396  // merge constants?
397  if(count>=2)
398  {
399  exprt::operandst::iterator const_sum;
400  bool const_sum_set=false;
401 
402  Forall_operands(it, expr)
403  {
404  if(is_number(it->type()) && it->is_constant())
405  {
406  if(!const_sum_set)
407  {
408  const_sum=it;
409  const_sum_set=true;
410  }
411  else
412  {
413  if(!const_sum->sum(*it))
414  {
415  *it=from_integer(0, it->type());
416  assert(it->is_not_nil());
417  result=false;
418  }
419  }
420  }
421  }
422  }
423 
424  // search for a and -a
425  // first gather all the a's with -a
426  typedef std::unordered_map<exprt, exprt::operandst::iterator, irep_hash>
427  expr_mapt;
428  expr_mapt expr_map;
429 
430  Forall_expr(it, operands)
431  if(it->id()==ID_unary_minus &&
432  it->operands().size()==1)
433  expr_map.insert(std::make_pair(it->op0(), it));
434 
435  // now search for a
436  Forall_expr(it, operands)
437  {
438  if(expr_map.empty())
439  break;
440  else if(it->id()==ID_unary_minus)
441  continue;
442 
443  expr_mapt::iterator itm=expr_map.find(*it);
444 
445  if(itm!=expr_map.end())
446  {
447  *(itm->second)=from_integer(0, expr.type());
448  *it=from_integer(0, expr.type());
449  assert(it->is_not_nil());
450  expr_map.erase(itm);
451  result=false;
452  }
453  }
454 
455  // delete zeros
456  // (can't do for floats, as the result of 0.0 + (-0.0)
457  // need not be -0.0 in std rounding)
458  for(exprt::operandst::iterator
459  it=operands.begin();
460  it!=operands.end();
461  /* no it++ */)
462  {
463  if(is_number(it->type()) && it->is_zero())
464  {
465  it=operands.erase(it);
466  result=false;
467  }
468  else
469  it++;
470  }
471  }
472 
473  if(operands.empty())
474  {
475  expr=from_integer(0, expr.type());
476  assert(expr.is_not_nil());
477  return false;
478  }
479  else if(operands.size()==1)
480  {
481  exprt tmp(operands.front());
482  expr.swap(tmp);
483  return false;
484  }
485 
486  return result;
487 }
488 
490 {
491  if(!is_number(expr.type()) &&
492  expr.type().id()!=ID_pointer)
493  return true;
494 
495  exprt::operandst &operands=expr.operands();
496 
497  assert(expr.id()==ID_minus);
498 
499  if(operands.size()!=2)
500  return true;
501 
502  if(is_number(expr.type()) &&
503  is_number(operands[0].type()) &&
504  is_number(operands[1].type()))
505  {
506  // rewrite "a-b" to "a+(-b)"
507  unary_minus_exprt tmp2(operands[1]);
508  simplify_unary_minus(tmp2);
509 
510  plus_exprt tmp(operands[0], tmp2);
511  simplify_node(tmp);
512 
513  expr.swap(tmp);
514  return false;
515  }
516  else if(expr.type().id()==ID_pointer &&
517  operands[0].type().id()==ID_pointer &&
518  is_number(operands[1].type()))
519  {
520  // pointer arithmetic: rewrite "p-i" to "p+(-i)"
521  unary_minus_exprt tmp2(operands[1]);
522  simplify_unary_minus(tmp2);
523 
524  plus_exprt tmp(operands[0], tmp2);
525  simplify_plus(tmp);
526 
527  expr.swap(tmp);
528  return false;
529  }
530  else if(is_number(expr.type()) &&
531  operands[0].type().id()==ID_pointer &&
532  operands[1].type().id()==ID_pointer)
533  {
534  // pointer arithmetic: rewrite "p-p" to "0"
535 
536  if(operands[0]==operands[1])
537  {
538  exprt zero=from_integer(0, expr.type());
539  assert(zero.is_not_nil());
540  expr=zero;
541  return false;
542  }
543  }
544 
545  return true;
546 }
547 
549 {
550  if(!is_bitvector_type(expr.type()))
551  return true;
552 
553  // check if these are really boolean
554  if(expr.type().id()!=ID_bool)
555  {
556  bool all_bool=true;
557 
558  forall_operands(it, expr)
559  {
560  if(it->id()==ID_typecast &&
561  it->operands().size()==1 &&
562  ns.follow(it->op0().type()).id()==ID_bool)
563  {
564  }
565  else if(it->is_zero() || it->is_one())
566  {
567  }
568  else
569  all_bool=false;
570  }
571 
572  if(all_bool)
573  {
574  // re-write to boolean+typecast
575  exprt new_expr=expr;
576 
577  if(expr.id()==ID_bitand)
578  new_expr.id(ID_and);
579  else if(expr.id()==ID_bitor)
580  new_expr.id(ID_or);
581  else if(expr.id()==ID_bitxor)
582  new_expr.id(ID_xor);
583  else
584  assert(false);
585 
586  Forall_operands(it, new_expr)
587  {
588  if(it->id()==ID_typecast)
589  {
590  exprt tmp;
591  tmp=it->op0();
592  it->swap(tmp);
593  }
594  else if(it->is_zero())
595  *it=false_exprt();
596  else if(it->is_one())
597  *it=true_exprt();
598  }
599 
600  new_expr.type()=bool_typet();
601  simplify_node(new_expr);
602 
603  new_expr.make_typecast(expr.type());
604  simplify_node(new_expr);
605 
606  expr.swap(new_expr);
607  return false;
608  }
609  }
610 
611  bool result=true;
612 
613  // try to merge constants
614 
615  std::size_t width=to_bitvector_type(expr.type()).get_width();
616 
617  while(expr.operands().size()>=2)
618  {
619  const irep_idt &a_str=expr.op0().get(ID_value);
620  const irep_idt &b_str=expr.op1().get(ID_value);
621 
622  if(!expr.op0().is_constant())
623  break;
624 
625  if(!expr.op1().is_constant())
626  break;
627 
628  if(expr.op0().type()!=expr.type())
629  break;
630 
631  if(expr.op1().type()!=expr.type())
632  break;
633 
634  assert(a_str.size()==b_str.size());
635 
636  constant_exprt new_op(expr.type());
637  std::string new_value;
638  new_value.resize(width);
639 
640  if(expr.id()==ID_bitand)
641  {
642  for(std::size_t i=0; i<width; i++)
643  new_value[i]=(a_str[i]=='1' && b_str[i]=='1')?'1':'0';
644  }
645  else if(expr.id()==ID_bitor)
646  {
647  for(std::size_t i=0; i<width; i++)
648  new_value[i]=(a_str[i]=='1' || b_str[i]=='1')?'1':'0';
649  }
650  else if(expr.id()==ID_bitxor)
651  {
652  for(std::size_t i=0; i<width; i++)
653  new_value[i]=((a_str[i]=='1')!=(b_str[i]=='1'))?'1':'0';
654  }
655  else
656  break;
657 
658  new_op.set_value(new_value);
659 
660  // erase first operand
661  expr.operands().erase(expr.operands().begin());
662  expr.op0().swap(new_op);
663 
664  result=false;
665  }
666 
667  // now erase 'all zeros' out of bitor, bitxor
668 
669  if(expr.id()==ID_bitor || expr.id()==ID_bitxor)
670  {
671  for(exprt::operandst::iterator
672  it=expr.operands().begin();
673  it!=expr.operands().end();
674  ) // no it++
675  {
676  if(it->is_zero() && expr.operands().size()>1)
677  {
678  it=expr.operands().erase(it);
679  result=false;
680  }
681  else
682  it++;
683  }
684  }
685 
686  // now erase 'all ones' out of bitand
687 
688  if(expr.id()==ID_bitand)
689  {
690  for(exprt::operandst::iterator
691  it=expr.operands().begin();
692  it!=expr.operands().end();
693  ) // no it++
694  {
695  if(it->is_constant() &&
696  id2string(to_constant_expr(*it).get_value()).find('0')==
697  std::string::npos &&
698  expr.operands().size()>1)
699  {
700  it=expr.operands().erase(it);
701  result=false;
702  }
703  else
704  it++;
705  }
706  }
707 
708  // two operands that are syntactically the same
709 
710  if(expr.operands().size()==2 &&
711  expr.op0()==expr.op1())
712  {
713  if(expr.id()==ID_bitand || expr.id()==ID_bitor)
714  {
715  exprt tmp;
716  tmp.swap(expr.op0());
717  expr.swap(tmp);
718  return false;
719  }
720  else if(expr.id()==ID_bitxor)
721  {
722  constant_exprt new_op(expr.type());
723  new_op.set_value(integer2binary(0, width));
724  expr.swap(new_op);
725  return false;
726  }
727  }
728 
729  if(expr.operands().size()==1)
730  {
731  exprt tmp;
732  tmp.swap(expr.op0());
733  expr.swap(tmp);
734  return false;
735  }
736 
737  return result;
738 }
739 
741 {
742  const typet &op0_type=expr.op0().type();
743 
744  if(!is_bitvector_type(op0_type))
745  return true;
746 
747  std::size_t width=to_bitvector_type(op0_type).get_width();
748 
749  assert(expr.operands().size()==2);
750 
751  mp_integer i;
752 
753  if(to_integer(expr.op1(), i))
754  return true;
755 
756  if(!expr.op0().is_constant())
757  return true;
758 
759  if(i<0 || i>=width)
760  return true;
761 
762  const irep_idt &value=expr.op0().get(ID_value);
763 
764  if(value.size()!=width)
765  return true;
766 
767  bool bit=(id2string(value)[width-integer2size_t(i)-1]=='1');
768 
769  expr.make_bool(bit);
770 
771  return false;
772 }
773 
775 {
776  bool result=true;
777 
778  if(is_bitvector_type(expr.type()))
779  {
780  // first, turn bool into bvec[1]
781  Forall_operands(it, expr)
782  {
783  exprt &op=*it;
784  if(op.is_true() || op.is_false())
785  {
786  bool value=op.is_true();
787  op=constant_exprt(value?ID_1:ID_0, unsignedbv_typet(1));
788  }
789  }
790 
791  // search for neighboring constants to merge
792  size_t i=0;
793 
794  while(i<expr.operands().size()-1)
795  {
796  exprt &opi=expr.operands()[i];
797  exprt &opn=expr.operands()[i+1];
798 
799  if(opi.is_constant() &&
800  opn.is_constant() &&
801  is_bitvector_type(opi.type()) &&
802  is_bitvector_type(opn.type()))
803  {
804  // merge!
805  const std::string new_value=
806  opi.get_string(ID_value)+opn.get_string(ID_value);
807  opi.set(ID_value, new_value);
808  opi.type().set(ID_width, new_value.size());
809  // erase opn
810  expr.operands().erase(expr.operands().begin()+i+1);
811  result=true;
812  }
813  else
814  i++;
815  }
816  }
817  else if(expr.type().id()==ID_verilog_unsignedbv)
818  {
819  // search for neighboring constants to merge
820  size_t i=0;
821 
822  while(i<expr.operands().size()-1)
823  {
824  exprt &opi=expr.operands()[i];
825  exprt &opn=expr.operands()[i+1];
826 
827  if(opi.is_constant() &&
828  opn.is_constant() &&
829  (opi.type().id()==ID_verilog_unsignedbv ||
830  is_bitvector_type(opi.type())) &&
831  (opn.type().id()==ID_verilog_unsignedbv ||
832  is_bitvector_type(opn.type())))
833  {
834  // merge!
835  const std::string new_value=
836  opi.get_string(ID_value)+opn.get_string(ID_value);
837  opi.set(ID_value, new_value);
838  opi.type().set(ID_width, new_value.size());
839  opi.type().id(ID_verilog_unsignedbv);
840  // erase opn
841  expr.operands().erase(expr.operands().begin()+i+1);
842  result=true;
843  }
844  else
845  i++;
846  }
847  }
848 
849  // { x } = x
850  if(expr.operands().size()==1)
851  {
852  exprt tmp;
853  tmp.swap(expr.op0());
854  expr.swap(tmp);
855  result=false;
856  }
857 
858  return result;
859 }
860 
862 {
863  if(!is_number(expr.type()))
864  return true;
865 
866  if(expr.operands().size()!=2)
867  return true;
868 
869  mp_integer distance;
870 
871  if(to_integer(expr.op1(), distance))
872  return true;
873 
874  if(distance==0)
875  {
876  exprt tmp;
877  tmp.swap(expr.op0());
878  expr.swap(tmp);
879  return false;
880  }
881 
882  mp_integer value;
883 
884  if(to_integer(expr.op0(), value))
885  return true;
886 
887  if(expr.op0().type().id()==ID_unsignedbv ||
888  expr.op0().type().id()==ID_signedbv)
889  {
890  mp_integer width=
891  string2integer(id2string(expr.op0().type().get(ID_width)));
892 
893  if(expr.id()==ID_lshr)
894  {
895  // this is to guard against large values of distance
896  if(distance>=width)
897  {
898  expr=from_integer(0, expr.type());
899  return false;
900  }
901  else if(distance>=0)
902  {
903  value/=power(2, distance);
904  expr=from_integer(value, expr.type());
905  return false;
906  }
907  }
908  else if(expr.id()==ID_ashr)
909  {
910  if(distance>=0)
911  {
912  // this is to simulate an arithmetic right shift
913  mp_integer new_value=value>>distance; // NOLINT(whitespace/operators)
914  expr=from_integer(new_value, expr.type());
915  return false;
916  }
917  }
918  else if(expr.id()==ID_shl)
919  {
920  // this is to guard against large values of distance
921  if(distance>=width)
922  {
923  expr=from_integer(0, expr.type());
924  return false;
925  }
926  else if(distance>=0)
927  {
928  value*=power(2, distance);
929  expr=from_integer(value, expr.type());
930  return false;
931  }
932  }
933  }
934  else if(expr.op0().type().id()==ID_integer ||
935  expr.op0().type().id()==ID_natural)
936  {
937  if(expr.id()==ID_lshr)
938  {
939  if(distance>=0)
940  {
941  value/=power(2, distance);
942  expr=from_integer(value, expr.type());
943  return false;
944  }
945  }
946  else if(expr.id()==ID_ashr)
947  {
948  // this is to simulate an arithmetic right shift
949  if(distance>=0)
950  {
951  mp_integer new_value=value/power(2, distance);
952  if(value<0 && new_value==0)
953  new_value=-1;
954 
955  expr=from_integer(new_value, expr.type());
956  return false;
957  }
958  }
959  else if(expr.id()==ID_shl)
960  {
961  if(distance>=0)
962  {
963  value*=power(2, distance);
964  expr=from_integer(value, expr.type());
965  return false;
966  }
967  }
968  }
969 
970  return true;
971 }
972 
974 {
975  if(!is_number(expr.type()))
976  return true;
977 
978  if(expr.operands().size()!=2)
979  return true;
980 
981  mp_integer base, exponent;
982 
983  if(to_integer(expr.op0(), base))
984  return true;
985 
986  if(to_integer(expr.op1(), exponent))
987  return true;
988 
989  mp_integer result=power(base, exponent);
990 
991  expr=from_integer(result, expr.type());
992  return false;
993 }
994 
997 {
998  assert(expr.operands().size()==3);
999 
1000  const typet &op0_type=expr.op0().type();
1001 
1002  if(!is_bitvector_type(op0_type) &&
1003  !is_bitvector_type(expr.type()))
1004  return true;
1005 
1006  if(expr.op0().is_constant())
1007  {
1008  std::size_t width=to_bitvector_type(op0_type).get_width();
1009  mp_integer start, end;
1010 
1011  if(to_integer(expr.op1(), start))
1012  return true;
1013 
1014  if(to_integer(expr.op2(), end))
1015  return true;
1016 
1017  if(start<0 || start>=width ||
1018  end<0 || end>=width)
1019  return true;
1020 
1021  assert(start>=end); // is this always the case??
1022 
1023  const irep_idt &value=expr.op0().get(ID_value);
1024 
1025  if(value.size()!=width)
1026  return true;
1027 
1028  std::string svalue=id2string(value);
1029 
1030  std::string extracted_value=
1031  svalue.substr(width-integer2size_t(start)-1,
1032  integer2size_t(start-end+1));
1033 
1034  exprt tmp(ID_constant, expr.type());
1035  tmp.set(ID_value, extracted_value);
1036  expr.swap(tmp);
1037 
1038  return false;
1039  }
1040 
1041  return true;
1042 }
1043 
1045 {
1046  if(expr.operands().size()!=1)
1047  return true;
1048 
1049  // simply remove, this is always 'nop'
1050  expr=expr.op0();
1051  return false;
1052 }
1053 
1055 {
1056  if(expr.operands().size()!=1)
1057  return true;
1058 
1059  if(!is_number(expr.type()))
1060  return true;
1061 
1062  exprt &operand=expr.op0();
1063 
1064  if(expr.type()!=operand.type())
1065  return true;
1066 
1067  if(operand.id()==ID_unary_minus)
1068  {
1069  // cancel out "-(-x)" to "x"
1070  if(operand.operands().size()!=1)
1071  return true;
1072 
1073  if(!is_number(operand.op0().type()))
1074  return true;
1075 
1076  exprt tmp;
1077  tmp.swap(expr.op0().op0());
1078  expr.swap(tmp);
1079  return false;
1080  }
1081  else if(operand.id()==ID_constant)
1082  {
1083  const irep_idt &type_id=expr.type().id();
1084 
1085  if(type_id==ID_integer ||
1086  type_id==ID_signedbv ||
1087  type_id==ID_unsignedbv)
1088  {
1089  mp_integer int_value;
1090 
1091  if(to_integer(expr.op0(), int_value))
1092  return true;
1093 
1094  exprt tmp=from_integer(-int_value, expr.type());
1095 
1096  if(tmp.is_nil())
1097  return true;
1098 
1099  expr.swap(tmp);
1100 
1101  return false;
1102  }
1103  else if(type_id==ID_rational)
1104  {
1105  rationalt r;
1106  if(to_rational(expr.op0(), r))
1107  return true;
1108 
1109  expr=from_rational(-r);
1110  return false;
1111  }
1112  else if(type_id==ID_fixedbv)
1113  {
1114  fixedbvt f(to_constant_expr(expr.op0()));
1115  f.negate();
1116  expr=f.to_expr();
1117  return false;
1118  }
1119  else if(type_id==ID_floatbv)
1120  {
1121  ieee_floatt f(to_constant_expr(expr.op0()));
1122  f.negate();
1123  expr=f.to_expr();
1124  return false;
1125  }
1126  }
1127 
1128  return true;
1129 }
1130 
1132 {
1133  if(!expr.has_operands())
1134  return true;
1135 
1136  exprt::operandst &operands=expr.operands();
1137 
1138  if(operands.size()!=1)
1139  return true;
1140 
1141  exprt &op=operands.front();
1142 
1143  if(expr.type().id()==ID_bv ||
1144  expr.type().id()==ID_unsignedbv ||
1145  expr.type().id()==ID_signedbv)
1146  {
1147  if(op.type()==expr.type())
1148  {
1149  if(op.id()==ID_constant)
1150  {
1151  std::string value=op.get_string(ID_value);
1152 
1153  for(auto &ch : value)
1154  ch=(ch=='0')?'1':'0';
1155 
1156  exprt tmp(ID_constant, op.type());
1157  tmp.set(ID_value, value);
1158  expr.swap(tmp);
1159  return false;
1160  }
1161  }
1162  }
1163 
1164  return true;
1165 }
1166 
1169 {
1170  exprt::operandst &operands=expr.operands();
1171 
1172  if(expr.type().id()!=ID_bool)
1173  return true;
1174 
1175  if(operands.size()!=2)
1176  return true;
1177 
1178  exprt tmp0=expr.op0();
1179  exprt tmp1=expr.op1();
1180 
1181  // types must match
1182  if(!base_type_eq(tmp0.type(), tmp1.type(), ns))
1183  return true;
1184 
1185  // if rhs is ID_if (and lhs is not), swap operands for == and !=
1186  if((expr.id()==ID_equal || expr.id()==ID_notequal) &&
1187  tmp0.id()!=ID_if &&
1188  tmp1.id()==ID_if)
1189  {
1190  expr.op0().swap(expr.op1());
1191  return simplify_inequality(expr);
1192  }
1193 
1194  if(tmp0.id()==ID_if && tmp0.operands().size()==3)
1195  {
1196  if_exprt if_expr=lift_if(expr, 0);
1197  simplify_inequality(if_expr.true_case());
1198  simplify_inequality(if_expr.false_case());
1199  simplify_if(if_expr);
1200  expr.swap(if_expr);
1201 
1202  return false;
1203  }
1204 
1205  // see if we are comparing pointers that are address_of
1206  if((tmp0.id()==ID_address_of ||
1207  (tmp0.id()==ID_typecast && tmp0.op0().id()==ID_address_of)) &&
1208  (tmp1.id()==ID_address_of ||
1209  (tmp1.id()==ID_typecast && tmp1.op0().id()==ID_address_of)) &&
1210  (expr.id()==ID_equal || expr.id()==ID_notequal))
1211  return simplify_inequality_address_of(expr);
1212 
1213  if(tmp0.id()==ID_pointer_object &&
1214  tmp1.id()==ID_pointer_object &&
1215  (expr.id()==ID_equal || expr.id()==ID_notequal))
1217 
1218  // first see if we compare to a constant
1219 
1220  bool op0_is_const=tmp0.is_constant();
1221  bool op1_is_const=tmp1.is_constant();
1222 
1223  ns.follow_symbol(tmp0.type());
1224  ns.follow_symbol(tmp1.type());
1225 
1226  if(tmp0.type().id()==ID_c_enum_tag)
1227  tmp0.type()=ns.follow_tag(to_c_enum_tag_type(tmp0.type()));
1228 
1229  if(tmp1.type().id()==ID_c_enum_tag)
1230  tmp1.type()=ns.follow_tag(to_c_enum_tag_type(tmp1.type()));
1231 
1232  // are _both_ constant?
1233  if(op0_is_const && op1_is_const)
1234  {
1235  if(tmp0.type().id()==ID_bool)
1236  {
1237  bool v0=tmp0.is_true();
1238  bool v1=tmp1.is_true();
1239 
1240  if(expr.id()==ID_equal)
1241  {
1242  expr.make_bool(v0==v1);
1243  return false;
1244  }
1245  else if(expr.id()==ID_notequal)
1246  {
1247  expr.make_bool(v0!=v1);
1248  return false;
1249  }
1250  }
1251  else if(tmp0.type().id()==ID_fixedbv)
1252  {
1253  fixedbvt f0(to_constant_expr(tmp0));
1254  fixedbvt f1(to_constant_expr(tmp1));
1255 
1256  if(expr.id()==ID_notequal)
1257  expr.make_bool(f0!=f1);
1258  else if(expr.id()==ID_equal)
1259  expr.make_bool(f0==f1);
1260  else if(expr.id()==ID_ge)
1261  expr.make_bool(f0>=f1);
1262  else if(expr.id()==ID_le)
1263  expr.make_bool(f0<=f1);
1264  else if(expr.id()==ID_gt)
1265  expr.make_bool(f0>f1);
1266  else if(expr.id()==ID_lt)
1267  expr.make_bool(f0<f1);
1268  else
1269  assert(false);
1270 
1271  return false;
1272  }
1273  else if(tmp0.type().id()==ID_floatbv)
1274  {
1275  ieee_floatt f0(to_constant_expr(tmp0));
1276  ieee_floatt f1(to_constant_expr(tmp1));
1277 
1278  if(expr.id()==ID_notequal)
1279  expr.make_bool(f0!=f1);
1280  else if(expr.id()==ID_equal)
1281  expr.make_bool(f0==f1);
1282  else if(expr.id()==ID_ge)
1283  expr.make_bool(f0>=f1);
1284  else if(expr.id()==ID_le)
1285  expr.make_bool(f0<=f1);
1286  else if(expr.id()==ID_gt)
1287  expr.make_bool(f0>f1);
1288  else if(expr.id()==ID_lt)
1289  expr.make_bool(f0<f1);
1290  else
1291  assert(false);
1292 
1293  return false;
1294  }
1295  else if(tmp0.type().id()==ID_rational)
1296  {
1297  rationalt r0, r1;
1298 
1299  if(to_rational(tmp0, r0))
1300  return true;
1301 
1302  if(to_rational(tmp1, r1))
1303  return true;
1304 
1305  if(expr.id()==ID_notequal)
1306  expr.make_bool(r0!=r1);
1307  else if(expr.id()==ID_equal)
1308  expr.make_bool(r0==r1);
1309  else if(expr.id()==ID_ge)
1310  expr.make_bool(r0>=r1);
1311  else if(expr.id()==ID_le)
1312  expr.make_bool(r0<=r1);
1313  else if(expr.id()==ID_gt)
1314  expr.make_bool(r0>r1);
1315  else if(expr.id()==ID_lt)
1316  expr.make_bool(r0<r1);
1317  else
1318  assert(false);
1319 
1320  return false;
1321  }
1322  else
1323  {
1324  mp_integer v0, v1;
1325 
1326  if(to_integer(tmp0, v0))
1327  return true;
1328 
1329  if(to_integer(tmp1, v1))
1330  return true;
1331 
1332  if(expr.id()==ID_notequal)
1333  expr.make_bool(v0!=v1);
1334  else if(expr.id()==ID_equal)
1335  expr.make_bool(v0==v1);
1336  else if(expr.id()==ID_ge)
1337  expr.make_bool(v0>=v1);
1338  else if(expr.id()==ID_le)
1339  expr.make_bool(v0<=v1);
1340  else if(expr.id()==ID_gt)
1341  expr.make_bool(v0>v1);
1342  else if(expr.id()==ID_lt)
1343  expr.make_bool(v0<v1);
1344  else
1345  assert(false);
1346 
1347  return false;
1348  }
1349  }
1350  else if(op0_is_const)
1351  {
1352  // we want the constant on the RHS
1353 
1354  if(expr.id()==ID_ge)
1355  expr.id(ID_le);
1356  else if(expr.id()==ID_le)
1357  expr.id(ID_ge);
1358  else if(expr.id()==ID_gt)
1359  expr.id(ID_lt);
1360  else if(expr.id()==ID_lt)
1361  expr.id(ID_gt);
1362 
1363  expr.op0().swap(expr.op1());
1364 
1365  // one is constant
1367  return false;
1368  }
1369  else if(op1_is_const)
1370  {
1371  // one is constant
1372  return simplify_inequality_constant(expr);
1373  }
1374  else
1375  {
1376  // both are not constant
1377  return simplify_inequality_not_constant(expr);
1378  }
1379 
1380  assert(false);
1381  return false;
1382 }
1383 
1385  exprt &op0,
1386  exprt &op1)
1387 {
1388  // we can't eliminate zeros
1389  if(op0.is_zero() ||
1390  op1.is_zero() ||
1391  (op0.is_constant() &&
1392  to_constant_expr(op0).get_value()==ID_NULL) ||
1393  (op1.is_constant() &&
1394  to_constant_expr(op1).get_value()==ID_NULL))
1395  return true;
1396 
1397  if(op0.id()==ID_plus)
1398  {
1399  bool result=true;
1400 
1401  Forall_operands(it, op0)
1402  if(!eliminate_common_addends(*it, op1))
1403  result=false;
1404 
1405  return result;
1406  }
1407  else if(op1.id()==ID_plus)
1408  {
1409  bool result=true;
1410 
1411  Forall_operands(it, op1)
1412  if(!eliminate_common_addends(op0, *it))
1413  result=false;
1414 
1415  return result;
1416  }
1417  else if(op0==op1)
1418  {
1419  if(!op0.is_zero() &&
1420  op0.type().id()!=ID_complex)
1421  {
1422  // elimination!
1423  op0=from_integer(0, op0.type());
1424  op1=from_integer(0, op1.type());
1425  return false;
1426  }
1427  }
1428 
1429  return true;
1430 }
1431 
1433 {
1434  exprt::operandst &operands=expr.operands();
1435 
1436  // pretty much all of the simplifications below are unsound
1437  // for IEEE float because of NaN!
1438 
1439  if(ns.follow(expr.op0().type()).id()==ID_floatbv)
1440  return true;
1441 
1442  // eliminate strict inequalities
1443  if(expr.id()==ID_notequal)
1444  {
1445  expr.id(ID_equal);
1447  expr.make_not();
1448  simplify_node(expr);
1449  return false;
1450  }
1451  else if(expr.id()==ID_gt)
1452  {
1453  expr.id(ID_ge);
1454  // swap operands
1455  expr.op0().swap(expr.op1());
1457  expr.make_not();
1458  simplify_node(expr);
1459  return false;
1460  }
1461  else if(expr.id()==ID_lt)
1462  {
1463  expr.id(ID_ge);
1465  expr.make_not();
1466  simplify_node(expr);
1467  return false;
1468  }
1469  else if(expr.id()==ID_le)
1470  {
1471  expr.id(ID_ge);
1472  // swap operands
1473  expr.op0().swap(expr.op1());
1475  return false;
1476  }
1477 
1478  // now we only have >=, =
1479 
1480  assert(expr.id()==ID_ge || expr.id()==ID_equal);
1481 
1482  // syntactically equal?
1483 
1484  if(operands.front()==operands.back())
1485  {
1486  expr=true_exprt();
1487  return false;
1488  }
1489 
1490  // try constants
1491 
1492  value_listt values0, values1;
1493 
1494  bool ok0=!get_values(expr.op0(), values0);
1495  bool ok1=!get_values(expr.op1(), values1);
1496 
1497  if(ok0 && ok1)
1498  {
1499  bool first=true;
1500  bool result=false; // dummy initialization to prevent warning
1501  bool ok=true;
1502 
1503  // compare possible values
1504 
1505  forall_value_list(it0, values0)
1506  forall_value_list(it1, values1)
1507  {
1508  bool tmp;
1509  const mp_integer &int_value0=*it0;
1510  const mp_integer &int_value1=*it1;
1511 
1512  if(expr.id()==ID_ge)
1513  tmp=(int_value0>=int_value1);
1514  else if(expr.id()==ID_equal)
1515  tmp=(int_value0==int_value1);
1516  else
1517  {
1518  tmp=false;
1519  assert(0);
1520  }
1521 
1522  if(first)
1523  {
1524  result=tmp;
1525  first=false;
1526  }
1527  else if(result!=tmp)
1528  {
1529  ok=false;
1530  break;
1531  }
1532  }
1533 
1534  if(ok)
1535  {
1536  expr.make_bool(result);
1537  return false;
1538  }
1539  }
1540 
1541  // See if we can eliminate common addends on both sides.
1542  // On bit-vectors, this is only sound on '='.
1543  if(expr.id()==ID_equal)
1544  {
1545  if(!eliminate_common_addends(expr.op0(), expr.op1()))
1546  {
1547  // remove zeros
1548  simplify_node(expr.op0());
1549  simplify_node(expr.op1());
1550  simplify_inequality(expr); // recursive call
1551  return false;
1552  }
1553  }
1554 
1555  return true;
1556 }
1557 
1560 {
1561  // the constant is always on the RHS
1562  assert(expr.op1().is_constant());
1563 
1564  if(expr.op0().id()==ID_if && expr.op0().operands().size()==3)
1565  {
1566  if_exprt if_expr=lift_if(expr, 0);
1569  simplify_if(if_expr);
1570  expr.swap(if_expr);
1571 
1572  return false;
1573  }
1574 
1575  // do we deal with pointers?
1576  if(expr.op1().type().id()==ID_pointer)
1577  {
1578  if(expr.id()==ID_notequal)
1579  {
1580  expr.id(ID_equal);
1582  expr.make_not();
1583  simplify_node(expr);
1584  return false;
1585  }
1586 
1587  // very special case for pointers
1588  if(expr.id()==ID_equal &&
1589  expr.op1().is_constant() &&
1590  expr.op1().get(ID_value)==ID_NULL)
1591  {
1592  // the address of an object is never NULL
1593 
1594  if(expr.op0().id()==ID_address_of &&
1595  expr.op0().operands().size()==1)
1596  {
1597  if(expr.op0().op0().id()==ID_symbol ||
1598  expr.op0().op0().id()==ID_dynamic_object ||
1599  expr.op0().op0().id()==ID_member ||
1600  expr.op0().op0().id()==ID_index ||
1601  expr.op0().op0().id()==ID_string_constant)
1602  {
1603  expr=false_exprt();
1604  return false;
1605  }
1606  }
1607  else if(expr.op0().id()==ID_typecast &&
1608  expr.op0().operands().size()==1 &&
1609  expr.op0().type().id()==ID_pointer &&
1610  expr.op0().op0().id()==ID_address_of &&
1611  expr.op0().op0().operands().size()==1)
1612  {
1613  if(expr.op0().op0().op0().id()==ID_symbol ||
1614  expr.op0().op0().op0().id()==ID_dynamic_object ||
1615  expr.op0().op0().op0().id()==ID_member ||
1616  expr.op0().op0().op0().id()==ID_index ||
1617  expr.op0().op0().op0().id()==ID_string_constant)
1618  {
1619  expr=false_exprt();
1620  return false;
1621  }
1622  }
1623  else if(expr.op0().id()==ID_typecast &&
1624  expr.op0().operands().size()==1 &&
1625  expr.op0().type().id()==ID_pointer &&
1626  (expr.op0().op0().type().id()==ID_pointer ||
1628  {
1629  // (type)ptr == NULL -> ptr == NULL
1630  // note that 'ptr' may be an integer
1631  exprt op=expr.op0().op0();
1632  expr.op0().swap(op);
1633  if(expr.op0().type().id()!=ID_pointer)
1634  expr.op1()=from_integer(0, expr.op0().type());
1635  else
1636  expr.op1().type()=expr.op0().type();
1637  simplify_inequality(expr); // do again!
1638  return false;
1639  }
1640  }
1641 
1642  // all we are doing with pointers
1643  return true;
1644  }
1645 
1646  // is it a separation predicate?
1647 
1648  if(expr.op0().id()==ID_plus)
1649  {
1650  // see if there is a constant in the sum
1651 
1652  if(expr.id()==ID_equal || expr.id()==ID_notequal)
1653  {
1654  mp_integer constant=0;
1655  bool changed=false;
1656 
1657  Forall_operands(it, expr.op0())
1658  {
1659  if(it->is_constant())
1660  {
1661  mp_integer i;
1662  if(!to_integer(*it, i))
1663  {
1664  constant+=i;
1665  *it=from_integer(0, it->type());
1666  assert(it->is_not_nil());
1667  changed=true;
1668  }
1669  }
1670  }
1671 
1672  if(changed)
1673  {
1674  // adjust constant
1675  mp_integer i;
1676  to_integer(expr.op1(), i);
1677  i-=constant;
1678  expr.op1()=from_integer(i, expr.op1().type());
1679 
1680  simplify_plus(expr.op0());
1681  simplify_inequality(expr);
1682  return false;
1683  }
1684  }
1685  }
1686 
1687  #if 1
1688  // (double)value REL const ---> value rel const
1689  // if 'const' can be represented exactly.
1690 
1691  if(expr.op0().id()==ID_typecast &&
1692  expr.op0().operands().size()==1 &&
1693  ns.follow(expr.op0().type()).id()==ID_floatbv &&
1694  ns.follow(expr.op0().op0().type()).id()==ID_floatbv)
1695  {
1696  ieee_floatt const_val(to_constant_expr(expr.op1()));
1697  ieee_floatt const_val_converted=const_val;
1698  const_val_converted.change_spec(
1700  ieee_floatt const_val_converted_back=const_val_converted;
1701  const_val_converted_back.change_spec(
1703  if(const_val_converted_back==const_val)
1704  {
1705  exprt result=expr;
1706  result.op0()=expr.op0().op0();
1707  result.op1()=const_val_converted.to_expr();
1708  expr.swap(result);
1709  return false;
1710  }
1711  }
1712  #endif
1713 
1714  // is the constant zero?
1715 
1716  if(expr.op1().is_zero())
1717  {
1718  if(expr.id()==ID_ge &&
1719  expr.op0().type().id()==ID_unsignedbv)
1720  {
1721  // zero is always smaller or equal something unsigned
1722  expr=true_exprt();
1723  return false;
1724  }
1725 
1726  exprt &operand=expr.op0();
1727 
1728  if(expr.id()==ID_equal)
1729  {
1730  // rules below do not hold for >=
1731  if(operand.id()==ID_unary_minus)
1732  {
1733  if(operand.operands().size()!=1)
1734  return true;
1735  exprt tmp;
1736  tmp.swap(operand.op0());
1737  operand.swap(tmp);
1738  return false;
1739  }
1740  else if(operand.id()==ID_plus)
1741  {
1742  // simplify a+-b=0 to a=b
1743 
1744  if(operand.operands().size()==2)
1745  {
1746  // if we have -b+a=0, make that a+(-b)=0
1747 
1748  if(operand.op0().id()==ID_unary_minus)
1749  operand.op0().swap(operand.op1());
1750 
1751  if(operand.op1().id()==ID_unary_minus &&
1752  operand.op1().operands().size()==1)
1753  {
1754  exprt tmp(expr.id(), expr.type());
1755  tmp.operands().resize(2);
1756  tmp.op0().swap(operand.op0());
1757  tmp.op1().swap(operand.op1().op0());
1758  expr.swap(tmp);
1759  return false;
1760  }
1761  }
1762  }
1763  }
1764  }
1765 
1766  // are we comparing with a typecast from bool?
1767  if(expr.op0().id()==ID_typecast &&
1768  expr.op0().operands().size()==1 &&
1769  expr.op0().op0().type().id()==ID_bool)
1770  {
1771  // we re-write (TYPE)boolean == 0 -> !boolean
1772  if(expr.op1().is_zero() && expr.id()==ID_equal)
1773  {
1774  expr=expr.op0().op0();
1775  expr.make_not();
1776  return false;
1777  }
1778 
1779  // we re-write (TYPE)boolean != 0 -> boolean
1780  if(expr.op1().is_zero() && expr.id()==ID_notequal)
1781  {
1782  expr=expr.op0().op0();
1783  return false;
1784  }
1785  }
1786 
1787  #define NORMALISE_CONSTANT_TESTS
1788  #ifdef NORMALISE_CONSTANT_TESTS
1789  // Normalise to >= and = to improve caching and term sharing
1790  if(expr.op0().type().id()==ID_unsignedbv ||
1791  expr.op0().type().id()==ID_signedbv)
1792  {
1793  bv_spect spec(expr.op0().type());
1794  mp_integer max(spec.max_value());
1795 
1796  if(expr.id()==ID_notequal)
1797  {
1798  expr.id(ID_equal);
1800  expr.make_not();
1801  simplify_node(expr);
1802  return false;
1803  }
1804  else if(expr.id()==ID_gt)
1805  {
1806  mp_integer i;
1807  if(to_integer(expr.op1(), i))
1808  throw "bit-vector constant unexpectedly non-integer";
1809 
1810  if(i==max)
1811  {
1812  expr=false_exprt();
1813  return false;
1814  }
1815 
1816  expr.id(ID_ge);
1817  ++i;
1818  expr.op1()=from_integer(i, expr.op1().type());
1820  return false;
1821  }
1822  else if(expr.id()==ID_lt)
1823  {
1824  expr.id(ID_ge);
1826  expr.make_not();
1827  simplify_node(expr);
1828  return false;
1829  }
1830  else if(expr.id()==ID_le)
1831  {
1832  mp_integer i;
1833  if(to_integer(expr.op1(), i))
1834  throw "bit-vector constant unexpectedly non-integer";
1835 
1836  if(i==max)
1837  {
1838  expr=true_exprt();
1839  return false;
1840  }
1841 
1842  expr.id(ID_ge);
1843  ++i;
1844  expr.op1()=from_integer(i, expr.op1().type());
1846  expr.make_not();
1847  simplify_node(expr);
1848  return false;
1849  }
1850  }
1851 #endif
1852  return true;
1853 }
The type of an expression.
Definition: type.h:20
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
struct configt::ansi_ct ansi_c
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1125
exprt & true_case()
Definition: std_expr.h:2805
constant_exprt from_rational(const rationalt &a)
static int8_t r
Definition: irep_hash.h:59
BigInt mp_integer
Definition: mp_arith.h:19
bool is_one() const
Definition: rational.h:82
bool is_nil() const
Definition: irep.h:103
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:53
bool simplify_node(exprt &expr)
exprt & op0()
Definition: expr.h:84
constant_exprt to_expr() const
Definition: ieee_float.cpp:686
bool simplify_shifts(exprt &expr)
bool to_rational(const exprt &expr, rationalt &rational_value)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:270
Deprecated expression utility functions.
bool simplify_concatenation(exprt &expr)
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
bool is_false() const
Definition: expr.cpp:140
const irep_idt & get_value() const
Definition: std_expr.h:3702
bool simplify_inequality_pointer_object(exprt &expr)
bool NULL_is_zero
Definition: config.h:86
The trinary if-then-else operator.
Definition: std_expr.h:2771
bool is_true() const
Definition: expr.cpp:133
bool simplify_mult(exprt &expr)
typet & type()
Definition: expr.h:60
The proper Booleans.
Definition: std_types.h:33
A constant literal expression.
Definition: std_expr.h:3685
void make_bool(bool value)
Definition: expr.cpp:147
configt config
Definition: config.cpp:21
bool simplify_mod(exprt &expr)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1286
void change_spec(const ieee_float_spect &dest_spec)
const typet & follow_tag(const union_tag_typet &src) const
Definition: namespace.cpp:83
bool simplify_if(if_exprt &expr)
bool simplify_inequality_constant(exprt &expr)
const irep_idt & id() const
Definition: irep.h:189
void set_value(const irep_idt &value)
Definition: std_expr.h:3707
The boolean constant true.
Definition: std_expr.h:3742
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
Definition: std_types.h:717
#define Forall_expr(it, expr)
Definition: expr.h:32
bool simplify_div(exprt &expr)
bool is_zero() const
Definition: fixedbv.h:71
API to expression classes.
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
#define forall_value_list(it, value_list)
bool simplify_extractbits(exprt &expr)
Simplifies extracting of bits from a constant.
#define forall_operands(it, expr)
Definition: expr.h:17
The plus expression.
Definition: std_expr.h:702
bool is_zero() const
Definition: rational.h:79
size_t size() const
Definition: dstring.h:77
The unary minus expression.
Definition: std_expr.h:346
exprt & false_case()
Definition: std_expr.h:2815
constant_exprt to_expr() const
Definition: fixedbv.cpp:43
bool has_operands() const
Definition: expr.h:67
The boolean constant false.
Definition: std_expr.h:3753
bool simplify_unary_plus(exprt &expr)
bool is_constant() const
Definition: expr.cpp:128
std::size_t get_width() const
Definition: std_types.h:1030
bool get_values(const exprt &expr, value_listt &value_list)
bool simplify_bswap(exprt &expr)
std::vector< exprt > operandst
Definition: expr.h:49
void follow_symbol(irept &irep) const
Definition: namespace.cpp:43
void make_not()
Definition: expr.cpp:100
bool eliminate_common_addends(exprt &op0, exprt &op1)
bool is_number(const typet &type)
Definition: type.cpp:24
bool simplify_unary_minus(exprt &expr)
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Definition: expr_util.cpp:144
Base class for all expressions.
Definition: expr.h:46
bool simplify_power(exprt &expr)
bool simplify_bitwise(exprt &expr)
void negate()
Definition: ieee_float.h:156
const namespacet & ns
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:63
The NIL type.
Definition: std_types.h:43
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
bool is_zero() const
Definition: expr.cpp:236
exprt & op2()
Definition: expr.h:90
void negate()
Definition: fixedbv.cpp:87
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
bool simplify_inequality_not_constant(exprt &expr)
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
bool simplify_inequality_address_of(exprt &expr)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:3725
bool simplify_extractbit(exprt &expr)
bool simplify_minus(exprt &expr)
Base Type Computation.
std::set< mp_integer > value_listt
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
void make_typecast(const typet &_type)
Definition: expr.cpp:90
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
bool simplify_plus(exprt &expr)
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
bool simplify_inequality(exprt &expr)
simplifies inequalities !=, <=, <, >=, >, and also ==
static bool is_bitvector_type(const typet &type)
bool simplify_bitnot(exprt &expr)
bool is_one() const
Definition: expr.cpp:280
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
Definition: std_types.h:1051