CBMC
interval.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: intervals
4 
5  Author: Daniel Neville (2017), Diffblue Ltd
6 
7 \*******************************************************************/
8 
9 /*
10  *
11  * Types: Should we store a type for the entire interval?
12  * IMO: I think YES (for the case where we have -inf -> inf, we don't know otherwise
13  *
14  * This initial implementation only implements support for integers.
15  */
16 
17 #include "interval.h"
18 
19 #include "arith_tools.h"
20 #include "bitvector_expr.h"
21 #include "c_types.h"
22 #include "namespace.h"
23 #include "simplify_expr.h"
24 #include "std_expr.h"
25 #include "symbol_table.h"
26 
28 {
29  return op0();
30 }
31 
33 {
34  return op1();
35 }
36 
38 {
39  return *this;
40 }
41 
43 {
45  {
46  handle_constant_unary_expression(ID_unary_minus);
47  }
48 
49  exprt lower;
50  exprt upper;
51 
52  if(has_no_upper_bound())
53  {
54  lower = min();
55  }
56  else
57  {
59  }
60 
61  if(has_no_lower_bound())
62  {
63  upper = max();
64  }
65  else
66  {
68  }
69 
70  return constant_interval_exprt(lower, upper);
71 }
72 
75 {
77  {
79  }
80 
81  exprt lower = min();
82  exprt upper = max();
83 
84  if(is_max(get_upper()) || is_max(o.get_upper()))
85  {
86  upper = max_value_exprt(type());
87  }
88  else
89  {
90  INVARIANT(
91  !is_max(get_upper()) && !is_max(o.get_upper()),
92  "We just excluded this case");
94  }
95 
96  if(is_min(get_lower()) || is_min(o.get_lower()))
97  {
98  lower = min_value_exprt(type());
99  }
100  else
101  {
102  INVARIANT(
103  !is_min(get_lower()) && !is_min(o.get_lower()),
104  "We just excluded that case");
106  }
107 
108  return simplified_interval(lower, upper);
109 }
110 
113 {
115  {
116  handle_constant_binary_expression(other, ID_minus);
117  }
118 
119  // [this.lower - other.upper, this.upper - other.lower]
120  return plus(other.unary_minus());
121 }
122 
125 {
127  {
129  }
130 
131  return get_extremes(*this, o, ID_mult);
132 }
133 
136 {
138  {
140  }
141 
142  // If other might be division by zero, set everything to top.
143  if(o.contains_zero())
144  {
145  return top();
146  }
147 
148  return get_extremes(*this, o, ID_div);
149 }
150 
153 {
154  // SEE https://stackoverflow.com/questions/11720656/modulo-operation-with-negative-numbers
155 
157  {
159  }
160 
161  if(o.is_bottom())
162  {
163  return top();
164  }
165 
166  // If the RHS is 1, or -1 (signed only), then return zero.
167  if(
169  (o.get_lower() == from_integer(1, o.type()) ||
170  (o.is_signed() && o.get_lower() == from_integer(-1, o.type()))))
171  {
173  }
174 
175  // If other might be modulo by zero, set everything to top.
176  if(o.contains_zero())
177  {
178  return top();
179  }
180 
181  if(is_zero())
182  {
184  }
185 
186  exprt lower = min();
187  exprt upper = max();
188 
189  // Positive case (cannot have zero on RHS).
190  // 10 % 5 = [0, 4], 3 % 5 = [0, 3]
191  if(!is_negative() && o.is_positive())
192  {
193  lower = zero();
194  upper = get_min(get_upper(), o.decrement().get_upper());
195  }
196 
197  // [-5, 5] % [3]
199  {
200  INVARIANT(
201  contains_zero(),
202  "Zero should be between a negative and a positive value");
203  // This can be done more accurately.
204  lower = get_min(o.get_lower(), get_lower());
205  upper = get_max(o.get_upper(), get_upper());
206  }
207 
208  if(is_negative() && o.is_negative())
209  {
210  lower = get_min(o.get_lower(), o.get_lower());
211  upper = zero();
212  }
213 
214  return constant_interval_exprt(lower, upper);
215 }
216 
218 {
219  // tvt not
220  return !is_definitely_false();
221 }
222 
224 {
225  if(is_boolean())
226  {
228  {
229  return tvt(get_lower() == false_exprt());
230  }
231  else
232  {
233  return tvt::unknown();
234  }
235  }
236 
237  if(is_single_value_interval() && get_lower() == zero())
238  {
239  return tvt(true);
240  }
241 
243  {
244  INVARIANT(
246  "If an interval contains zero its lower bound can't be positive"
247  " and its upper bound can't be negative");
248  return tvt::unknown();
249  }
250 
251  return tvt(false);
252 }
253 
255 {
258 
259  tvt a = is_definitely_true();
260  tvt b = o.is_definitely_true();
261 
262  return (a || b);
263 }
264 
266 {
269 
270  return (is_definitely_true() && o.is_definitely_true());
271 }
272 
274 {
277 
278  return (
281 }
282 
284 {
286 
288  {
289  return tvt(false);
290  }
291 
293  {
294  return tvt(true);
295  }
296 
297  return tvt::unknown();
298 }
299 
302 {
304  {
305  return handle_constant_binary_expression(o, ID_shl);
306  }
307 
308  if(is_negative(o.get_lower()))
309  {
310  return top();
311  }
312 
313  return get_extremes(*this, o, ID_shl);
314 }
315 
316 // Arithmetic
319 {
321  {
322  return handle_constant_binary_expression(o, ID_ashr);
323  }
324 
325  if(is_negative(o.get_lower()))
326  {
327  return top();
328  }
329 
330  return get_extremes(*this, o, ID_ashr);
331 }
332 
335 {
337  {
338  return handle_constant_binary_expression(o, ID_bitxor);
339  }
340 
341  return top();
342 }
343 
346 {
348  {
349  return handle_constant_binary_expression(o, ID_bitor);
350  }
351 
352  return top();
353 }
354 
357 {
359  {
360  return handle_constant_binary_expression(o, ID_bitand);
361  }
362 
363  return top();
364 }
365 
367 {
369  {
370  return handle_constant_unary_expression(ID_bitnot);
371  }
372 
373  return top();
374 }
375 
377 {
378  // [get_lower, get_upper] < [o.get_lower(), o.get_upper()]
380  {
381  return tvt(less_than(get_lower(), o.get_lower()));
382  }
383 
384  if(less_than(get_upper(), o.get_lower()))
385  {
386  return tvt(true);
387  }
388 
389  if(greater_than(get_lower(), o.get_upper()))
390  {
391  return tvt(false);
392  }
393 
394  return tvt::unknown();
395 }
396 
398  const constant_interval_exprt &o) const
399 {
400  return o.less_than(*this);
401 }
402 
404  const constant_interval_exprt &o) const
405 {
407  {
408  return tvt(less_than_or_equal(get_lower(), o.get_lower()));
409  }
410 
411  // [get_lower, get_upper] <= [o.get_lower(), o.get_upper()]
413  {
414  return tvt(true);
415  }
416 
417  if(greater_than(get_lower(), o.get_upper()))
418  {
419  return tvt(false);
420  }
421 
422  return tvt::unknown();
423 }
424 
426  const constant_interval_exprt &o) const
427 {
428  return o.less_than_or_equal(*this);
429 }
430 
432 {
434  {
435  return tvt(equal(get_lower(), o.get_lower()));
436  }
437 
438  if(equal(get_upper(), o.get_upper()) && equal(get_lower(), o.get_lower()))
439  {
440  return tvt(true);
441  }
442 
443  if(
444  less_than(o).is_true() || greater_than(o).is_true() ||
445  o.less_than(*this).is_true() || o.greater_than(*this).is_true())
446  {
447  return tvt(false);
448  }
449 
450  // Don't know. Could have [3, 5] == [4] (not equal)
451  return tvt::unknown();
452 }
453 
455 {
456  return !equal(o);
457 }
458 
460 {
461  return plus(
463 }
464 
466 {
467  return minus(
469 }
470 
472  const constant_interval_exprt &a,
473  const constant_interval_exprt &b,
474  const irep_idt &operation)
475 {
476  std::vector<exprt> results;
477 
478  generate_expression(a.get_lower(), b.get_lower(), operation, results);
479  generate_expression(a.get_lower(), b.get_upper(), operation, results);
480  generate_expression(a.get_upper(), b.get_lower(), operation, results);
481  generate_expression(a.get_upper(), b.get_upper(), operation, results);
482 
483  for(auto result : results)
484  {
485  if(!is_extreme(result) && contains_extreme(result))
486  {
487  return constant_interval_exprt(result.type());
488  }
489  }
490 
491  exprt min = get_min(results);
492  exprt max = get_max(results);
493 
494  return simplified_interval(min, max);
495 }
496 
498  std::vector<exprt> values,
499  bool min_value)
500 {
501  symbol_tablet symbol_table;
502  namespacet ns(symbol_table); // Empty
503 
504  if(values.size() == 0)
505  {
506  return nil_exprt();
507  }
508 
509  if(values.size() == 1)
510  {
511  return *(values.begin());
512  }
513 
514  if(values.size() == 2)
515  {
516  if(min_value)
517  {
518  return get_min(values.front(), values.back());
519  }
520  else
521  {
522  return get_max(values.front(), values.back());
523  }
524  }
525 
526  typet type = values.begin()->type();
527 
528  for(auto v : values)
529  {
530  if((min_value && is_min(v)) || (!min_value && is_max(v)))
531  {
532  return v;
533  }
534  }
535 
536  for(auto left : values)
537  {
538  bool all_left_OP_right = true;
539 
540  for(auto right : values)
541  {
542  if(
543  (min_value && less_than_or_equal(left, right)) ||
544  (!min_value && greater_than_or_equal(left, right)))
545  {
546  continue;
547  }
548 
549  all_left_OP_right = false;
550  break;
551  }
552 
553  if(all_left_OP_right)
554  {
555  return left;
556  }
557  }
558 
559  /* Return top */
560  if(min_value)
561  {
562  return min_value_exprt(type);
563  }
564  else
565  {
566  return max_value_exprt(type);
567  }
568 
569  UNREACHABLE;
570 }
571 
573  const exprt &lhs,
574  const exprt &rhs,
575  const irep_idt &operation,
576  std::vector<exprt> &collection)
577 {
578  if(operation == ID_mult)
579  {
580  append_multiply_expression(lhs, rhs, collection);
581  }
582  else if(operation == ID_div)
583  {
584  collection.push_back(generate_division_expression(lhs, rhs));
585  }
586  else if(operation == ID_mod)
587  {
588  collection.push_back(generate_modulo_expression(lhs, rhs));
589  }
590  else if(operation == ID_shl || operation == ID_ashr)
591  {
592  collection.push_back(generate_shift_expression(lhs, rhs, operation));
593  }
594 }
595 
602  const exprt &lower,
603  const exprt &upper,
604  std::vector<exprt> &collection)
605 {
606  PRECONDITION(lower.type().is_not_nil() && is_numeric(lower.type()));
607 
608  if(is_max(lower))
609  {
610  append_multiply_expression_max(upper, collection);
611  }
612  else if(is_max(upper))
613  {
614  append_multiply_expression_max(lower, collection);
615  }
616  else if(is_min(lower))
617  {
618  append_multiply_expression_min(lower, upper, collection);
619  }
620  else if(is_min(upper))
621  {
622  append_multiply_expression_min(upper, lower, collection);
623  }
624  else
625  {
626  INVARIANT(
627  !is_extreme(lower) && !is_extreme(upper),
628  "We ruled out extreme cases beforehand");
629 
630  auto result = mult_exprt(lower, upper);
631  collection.push_back(simplified_expr(result));
632  }
633 }
634 
640  const exprt &expr,
641  std::vector<exprt> &collection)
642 {
643  if(is_min(expr))
644  {
645  INVARIANT(!is_positive(expr), "Min value cannot be >0.");
646  INVARIANT(
647  is_negative(expr) || is_zero(expr), "Non-negative MIN must be zero.");
648  }
649 
650  if(is_zero(expr))
651  collection.push_back(expr);
652  else
653  {
654  collection.push_back(max_value_exprt(expr));
655  collection.push_back(min_value_exprt(expr));
656  }
657 }
658 
665  const exprt &min,
666  const exprt &other,
667  std::vector<exprt> &collection)
668 {
670  INVARIANT(!is_positive(min), "Min value cannot be >0.");
671  INVARIANT(is_negative(min) || is_zero(min), "Non-negative MIN must be zero.");
672 
673  if(is_zero(min))
674  collection.push_back(min);
675  else if(is_zero(other))
676  collection.push_back(other);
677  else
678  {
679  collection.push_back(min_value_exprt(min));
680  collection.push_back(max_value_exprt(min));
681  }
682 }
683 
685  const exprt &lhs,
686  const exprt &rhs)
687 {
689 
691 
692  if(rhs.is_one())
693  {
694  return lhs;
695  }
696 
697  if(is_max(lhs))
698  {
699  if(is_negative(rhs))
700  {
701  return min_value_exprt(lhs);
702  }
703 
704  return lhs;
705  }
706 
707  if(is_min(lhs))
708  {
709  if(is_negative(rhs))
710  {
711  return max_value_exprt(lhs);
712  }
713 
714  return lhs;
715  }
716 
717  INVARIANT(!is_extreme(lhs), "We ruled out extreme cases beforehand");
718 
719  if(is_max(rhs))
720  {
721  return zero(rhs);
722  }
723 
724  if(is_min(rhs))
725  {
726  INVARIANT(
727  is_signed(rhs), "We think this is a signed integer for some reason?");
728  return zero(rhs);
729  }
730 
731  INVARIANT(
732  !is_extreme(lhs) && !is_extreme(rhs),
733  "We ruled out extreme cases beforehand");
734 
735  auto div_expr = div_exprt(lhs, rhs);
736  return simplified_expr(div_expr);
737 }
738 
740  const exprt &lhs,
741  const exprt &rhs)
742 {
744 
746 
747  if(rhs.is_one())
748  {
749  return lhs;
750  }
751 
752  if(is_max(lhs))
753  {
754  if(is_negative(rhs))
755  {
756  return min_value_exprt(lhs);
757  }
758 
759  return lhs;
760  }
761 
762  if(is_min(lhs))
763  {
764  if(is_negative(rhs))
765  {
766  return max_value_exprt(lhs);
767  }
768 
769  return lhs;
770  }
771 
772  INVARIANT(!is_extreme(lhs), "We rule out this case beforehand");
773 
774  if(is_max(rhs))
775  {
776  return zero(rhs);
777  }
778 
779  if(is_min(rhs))
780  {
781  INVARIANT(is_signed(rhs), "We assume this is signed for some reason?");
782  return zero(rhs);
783  }
784 
785  INVARIANT(
786  !is_extreme(lhs) && !is_extreme(rhs),
787  "We ruled out extreme values beforehand");
788 
789  auto modulo_expr = mod_exprt(lhs, rhs);
790  return simplified_expr(modulo_expr);
791 }
792 
794 {
795  if(id == ID_unary_plus)
796  {
797  return unary_plus();
798  }
799  if(id == ID_unary_minus)
800  {
801  return unary_minus();
802  }
803  if(id == ID_bitnot)
804  {
805  return bitwise_not();
806  }
807  if(id == ID_not)
808  {
809  return tvt_to_interval(logical_not());
810  }
811 
812  return top();
813 }
814 
816  const irep_idt &binary_operator,
817  const constant_interval_exprt &other) const
818 {
819  if(binary_operator == ID_plus)
820  {
821  return plus(other);
822  }
823  if(binary_operator == ID_minus)
824  {
825  return minus(other);
826  }
827  if(binary_operator == ID_mult)
828  {
829  return multiply(other);
830  }
831  if(binary_operator == ID_div)
832  {
833  return divide(other);
834  }
835  if(binary_operator == ID_mod)
836  {
837  return modulo(other);
838  }
839  if(binary_operator == ID_shl)
840  {
841  return left_shift(other);
842  }
843  if(binary_operator == ID_ashr)
844  {
845  return right_shift(other);
846  }
847  if(binary_operator == ID_bitor)
848  {
849  return bitwise_or(other);
850  }
851  if(binary_operator == ID_bitand)
852  {
853  return bitwise_and(other);
854  }
855  if(binary_operator == ID_bitxor)
856  {
857  return bitwise_xor(other);
858  }
859  if(binary_operator == ID_lt)
860  {
861  return tvt_to_interval(less_than(other));
862  }
863  if(binary_operator == ID_le)
864  {
865  return tvt_to_interval(less_than_or_equal(other));
866  }
867  if(binary_operator == ID_gt)
868  {
869  return tvt_to_interval(greater_than(other));
870  }
871  if(binary_operator == ID_ge)
872  {
873  return tvt_to_interval(greater_than_or_equal(other));
874  }
875  if(binary_operator == ID_equal)
876  {
877  return tvt_to_interval(equal(other));
878  }
879  if(binary_operator == ID_notequal)
880  {
881  return tvt_to_interval(not_equal(other));
882  }
883  if(binary_operator == ID_and)
884  {
885  return tvt_to_interval(logical_and(other));
886  }
887  if(binary_operator == ID_or)
888  {
889  return tvt_to_interval(logical_or(other));
890  }
891  if(binary_operator == ID_xor)
892  {
893  return tvt_to_interval(logical_xor(other));
894  }
895 
896  return top();
897 }
898 
900  const exprt &lhs,
901  const exprt &rhs,
902  const irep_idt &operation)
903 {
904  PRECONDITION(operation == ID_shl || operation == ID_ashr);
905 
906  if(is_zero(lhs) || is_zero(rhs))
907  {
908  // Shifting zero does nothing.
909  // Shifting BY zero also does nothing.
910  return lhs;
911  }
912 
913  INVARIANT(!is_negative(rhs), "Should be caught at an earlier stage.");
914 
915  if(is_max(lhs))
916  {
917  return lhs;
918  }
919 
920  if(is_min(lhs))
921  {
922  return lhs;
923  }
924 
925  if(is_max(rhs))
926  {
927  return min_value_exprt(rhs);
928  }
929 
930  INVARIANT(
931  !is_extreme(lhs) && !is_extreme(rhs),
932  "We ruled out extreme cases beforehand");
933 
934  auto shift_expr = shift_exprt(lhs, operation, rhs);
935  return simplified_expr(shift_expr);
936 }
937 
940  const irep_idt &op) const
941 {
943  {
944  auto expr = unary_exprt(op, get_lower());
946  }
947  return top();
948 }
949 
952  const constant_interval_exprt &other,
953  const irep_idt &op) const
954 {
956  auto expr = binary_exprt(get_lower(), op, other.get_lower());
958 }
959 
961 {
962  return greater_than(a, b) ? a : b;
963 }
964 
966 {
967  return less_than(a, b) ? a : b;
968 }
969 
970 exprt constant_interval_exprt::get_min(std::vector<exprt> &values)
971 {
972  return get_extreme(values, true);
973 }
974 
975 exprt constant_interval_exprt::get_max(std::vector<exprt> &values)
976 {
977  return get_extreme(values, false);
978 }
979 
980 /* we don't simplify in the constructor otherwise */
983 {
985 }
986 
988 {
989  symbol_tablet symbol_table;
990  const namespacet ns(symbol_table);
991 
993 
994  return simplify_expr(expr, ns);
995 }
996 
998 {
1000  INVARIANT(
1001  zero.is_zero() || (type.id() == ID_bool && zero.is_false()),
1002  "The value created from 0 should be zero or false");
1003  return zero;
1004 }
1005 
1007 {
1008  return zero(expr.type());
1009 }
1010 
1013 {
1014  return zero(interval.type());
1015 }
1016 
1018 {
1019  return zero(type());
1020 }
1021 
1023 {
1024  return min_value_exprt(type());
1025 }
1026 
1028 {
1029  return max_value_exprt(type());
1030 }
1031 
1033 {
1034  return (has_no_lower_bound() && has_no_upper_bound());
1035 }
1036 
1038 {
1039  // This should ONLY happen for bottom.
1040  return is_min(get_upper()) || is_max(get_lower());
1041 }
1042 
1044 {
1045  return constant_interval_exprt(type);
1046 }
1047 
1049 {
1051 }
1052 
1054 {
1055  return constant_interval_exprt(type());
1056 }
1057 
1059 {
1060  return bottom(type());
1061 }
1062 
1063 /* Helpers */
1064 
1066 {
1067  return is_int(type());
1068 }
1069 
1071 {
1072  return is_float(type());
1073 }
1074 
1076 {
1077  return is_int(type) || is_float(type);
1078 }
1079 
1081 {
1082  return is_numeric(type());
1083 }
1084 
1086 {
1087  return is_numeric(expr.type());
1088 }
1089 
1092 {
1093  return interval.is_numeric();
1094 }
1095 
1097 {
1098  return is_signed(type) || is_unsigned(type) || type.id() == ID_integer;
1099 }
1100 
1102 {
1103  return src.id() == ID_floatbv;
1104 }
1105 
1107 {
1108  return is_int(expr.type());
1109 }
1110 
1112 {
1113  return interval.is_int();
1114 }
1115 
1117 {
1118  return is_float(expr.type());
1119 }
1120 
1122 {
1123  return interval.is_float();
1124 }
1125 
1127 {
1128  return t.id() == ID_bv || t.id() == ID_signedbv || t.id() == ID_unsignedbv ||
1129  t.id() == ID_c_bool ||
1130  (t.id() == ID_c_bit_field &&
1131  is_bitvector(to_c_bit_field_type(t).underlying_type()));
1132 }
1133 
1135 {
1136  return t.id() == ID_signedbv ||
1137  (t.id() == ID_c_bit_field &&
1138  is_signed(to_c_bit_field_type(t).underlying_type()));
1139 }
1140 
1142 {
1143  return t.id() == ID_bv || t.id() == ID_unsignedbv || t.id() == ID_c_bool ||
1144  t.id() == ID_c_enum ||
1145  (t.id() == ID_c_bit_field &&
1146  is_unsigned(to_c_bit_field_type(t).underlying_type()));
1147 }
1148 
1150 {
1151  return is_signed(interval.type());
1152 }
1153 
1156 {
1157  return is_unsigned(interval.type());
1158 }
1159 
1162 {
1163  return is_bitvector(interval.type());
1164 }
1165 
1167 {
1168  return is_signed(expr.type());
1169 }
1170 
1172 {
1173  return is_unsigned(expr.type());
1174 }
1175 
1177 {
1178  return is_bitvector(expr.type());
1179 }
1180 
1182 {
1183  return is_signed(type());
1184 }
1185 
1187 {
1188  return is_unsigned(type());
1189 }
1190 
1192 {
1193  return is_bitvector(type());
1194 }
1195 
1197 {
1198  return (is_max(expr) || is_min(expr));
1199 }
1200 
1201 bool constant_interval_exprt::is_extreme(const exprt &expr1, const exprt &expr2)
1202 {
1203  return is_extreme(expr1) || is_extreme(expr2);
1204 }
1205 
1207 {
1208  return is_max(get_upper());
1209 }
1210 
1212 {
1213  return is_min(get_lower());
1214 }
1215 
1217 {
1218  return expr.id() == ID_max_value;
1219 }
1220 
1222 {
1223  return expr.id() == ID_min_value;
1224 }
1225 
1227 {
1228  exprt simplified = simplified_expr(expr);
1229 
1230  if(expr.is_nil() || !simplified.is_constant() || expr.get(ID_value) == "")
1231  {
1232  return false;
1233  }
1234 
1235  if(is_unsigned(expr) || is_max(expr))
1236  {
1237  return true;
1238  }
1239 
1240  INVARIANT(is_signed(expr), "Not implemented for floats");
1241  // Floats later
1242 
1243  if(is_min(expr))
1244  {
1245  return false;
1246  }
1247 
1248  return greater_than(expr, zero(expr));
1249 }
1250 
1252 {
1253  if(is_min(expr))
1254  {
1255  if(is_unsigned(expr))
1256  {
1257  return true;
1258  }
1259  else
1260  {
1261  return false;
1262  }
1263  }
1264 
1265  if(is_max(expr))
1266  {
1267  return false;
1268  }
1269 
1270  INVARIANT(!is_max(expr) && !is_min(expr), "We excluded those cases");
1271 
1272  if(expr.is_zero())
1273  {
1274  return true;
1275  }
1276 
1277  return equal(expr, zero(expr));
1278 }
1279 
1281 {
1282  if(is_unsigned(expr) || is_max(expr))
1283  {
1284  return false;
1285  }
1286 
1287  INVARIANT(
1288  is_signed(expr), "We don't support anything other than integers yet");
1289 
1290  if(is_min(expr))
1291  {
1292  return true;
1293  }
1294 
1295  INVARIANT(!is_extreme(expr), "We excluded these cases before");
1296 
1297  return less_than(expr, zero(expr));
1298 }
1299 
1301 {
1302  if(is_signed(expr) && is_min(expr))
1303  {
1304  return max_value_exprt(expr);
1305  }
1306 
1307  if(is_max(expr) || is_unsigned(expr) || is_zero(expr) || is_positive(expr))
1308  {
1309  return expr;
1310  }
1311 
1312  return simplified_expr(unary_minus_exprt(expr));
1313 }
1314 
1316 {
1317  if(a == b)
1318  {
1319  return true;
1320  }
1321 
1322  if(!is_numeric(a) || !is_numeric(b))
1323  {
1324  INVARIANT(
1325  !(a == b),
1326  "Best we can do now is a==b?, but this is covered by the above, so "
1327  "always false");
1328  return false;
1329  }
1330 
1331  if(is_max(a) && is_max(b))
1332  {
1333  return true;
1334  }
1335 
1336  exprt l = (is_min(a) && is_unsigned(a)) ? zero(a) : a;
1337  exprt r = (is_min(b) && is_unsigned(b)) ? zero(b) : b;
1338 
1339  // CANNOT use is_zero(X) but can use X.is_zero();
1340  if((is_min(l) && is_min(r)))
1341  {
1342  return true;
1343  }
1344 
1345  if(
1346  (is_max(l) && !is_max(r)) || (is_min(l) && !is_min(r)) ||
1347  (is_max(r) && !is_max(l)) || (is_min(r) && !is_min(l)))
1348  {
1349  return false;
1350  }
1351 
1352  INVARIANT(!is_extreme(l, r), "We've excluded this before");
1353 
1354  return simplified_expr(equal_exprt(l, r)).is_true();
1355 }
1356 
1357 // TODO: Signed/unsigned comparisons.
1359 {
1360  if(!is_numeric(a) || !is_numeric(b))
1361  {
1362  return false;
1363  }
1364 
1365  exprt l = (is_min(a) && is_unsigned(a)) ? zero(a) : a;
1366  exprt r = (is_min(b) && is_unsigned(b)) ? zero(b) : b;
1367 
1368  if(is_max(l))
1369  {
1370  return false;
1371  }
1372 
1373  INVARIANT(!is_max(l), "We've just excluded this case");
1374 
1375  if(is_min(r))
1376  {
1377  // Can't be smaller than min.
1378  return false;
1379  }
1380 
1381  INVARIANT(!is_max(l) && !is_min(r), "We've excluded these cases");
1382 
1383  if(is_min(l))
1384  {
1385  return true;
1386  }
1387 
1388  INVARIANT(
1389  !is_max(l) && !is_min(r) && !is_min(l),
1390  "These cases should have all been handled before this point");
1391 
1392  if(is_max(r))
1393  {
1394  // If r is max, then l is less, unless l is max.
1395  return !is_max(l);
1396  }
1397 
1398  INVARIANT(
1399  !is_extreme(l) && !is_extreme(r),
1400  "We have excluded all of these cases in the code above");
1401 
1402  return simplified_expr(binary_relation_exprt(l, ID_lt, r)).is_true();
1403 }
1404 
1406 {
1407  return less_than(b, a);
1408 }
1409 
1411 {
1412  return less_than(a, b) || equal(a, b);
1413 }
1414 
1416  const exprt &a,
1417  const exprt &b)
1418 {
1419  return greater_than(a, b) || equal(a, b);
1420 }
1421 
1423 {
1424  return !equal(a, b);
1425 }
1426 
1428  const constant_interval_exprt &interval) const
1429 {
1430  // [a, b] Contains [c, d] If c >= a and d <= b.
1431  return (
1432  less_than_or_equal(interval.get_upper(), get_upper()) &&
1433  greater_than_or_equal(interval.get_lower(), get_lower()));
1434 }
1435 
1437 {
1438  std::stringstream out;
1439  out << *this;
1440  return out.str();
1441 }
1442 
1443 std::ostream &operator<<(std::ostream &out, const constant_interval_exprt &i)
1444 {
1445  out << "[";
1446 
1447  if(!i.has_no_lower_bound())
1448  {
1449  // FIXME Not everything that's a bitvector is also an integer
1450  if(i.is_bitvector(i.get_lower()))
1451  {
1452  out << integer2string(*numeric_cast<mp_integer>(i.get_lower()));
1453  }
1454  else
1455  {
1456  // TODO handle floating point numbers?
1457  out << i.get_lower().get(ID_value);
1458  }
1459  }
1460  else
1461  {
1462  if(i.is_signed(i.get_lower()))
1463  {
1464  out << "MIN";
1465  }
1466  else
1467  {
1468  // FIXME Extremely sketchy, the opposite of
1469  // FIXME "signed" isn't "unsigned" but
1470  // FIXME "literally anything else"
1471  out << "0";
1472  }
1473  }
1474 
1475  out << ",";
1476 
1477  // FIXME See comments on is_min
1478  if(!i.has_no_upper_bound())
1479  {
1480  if(i.is_bitvector(i.get_upper()))
1481  {
1482  out << integer2string(*numeric_cast<mp_integer>(i.get_upper()));
1483  }
1484  else
1485  {
1486  out << i.get_upper().get(ID_value);
1487  }
1488  }
1489  else
1490  out << "MAX";
1491 
1492  out << "]";
1493 
1494  return out;
1495 }
1496 
1498  const constant_interval_exprt &lhs,
1499  const constant_interval_exprt &rhs)
1500 {
1501  return lhs.less_than(rhs).is_true();
1502 }
1503 
1505  const constant_interval_exprt &lhs,
1506  const constant_interval_exprt &rhs)
1507 {
1508  return lhs.greater_than(rhs).is_true();
1509 }
1510 
1512  const constant_interval_exprt &lhs,
1513  const constant_interval_exprt &rhs)
1514 {
1515  return lhs.less_than_or_equal(rhs).is_true();
1516 }
1517 
1519  const constant_interval_exprt &lhs,
1520  const constant_interval_exprt &rhs)
1521 {
1522  return lhs.greater_than(rhs).is_true();
1523 }
1524 
1526  const constant_interval_exprt &lhs,
1527  const constant_interval_exprt &rhs)
1528 {
1529  return lhs.equal(rhs).is_true();
1530 }
1531 
1533  const constant_interval_exprt &lhs,
1534  const constant_interval_exprt &rhs)
1535 {
1536  return lhs.not_equal(rhs).is_true();
1537 }
1538 
1540  const constant_interval_exprt &lhs,
1541  const constant_interval_exprt &rhs)
1542 {
1543  return lhs.unary_plus(rhs);
1544 }
1545 
1547  const constant_interval_exprt &lhs,
1548  const constant_interval_exprt &rhs)
1549 {
1550  return lhs.minus(rhs);
1551 }
1552 
1554  const constant_interval_exprt &lhs,
1555  const constant_interval_exprt &rhs)
1556 {
1557  return lhs.divide(rhs);
1558 }
1559 
1561  const constant_interval_exprt &lhs,
1562  const constant_interval_exprt &rhs)
1563 {
1564  return lhs.multiply(rhs);
1565 }
1566 
1568  const constant_interval_exprt &lhs,
1569  const constant_interval_exprt &rhs)
1570 {
1571  return lhs.modulo(rhs);
1572 }
1573 
1575  const constant_interval_exprt &lhs,
1576  const constant_interval_exprt &rhs)
1577 {
1578  return lhs.bitwise_and(rhs);
1579 }
1580 
1582  const constant_interval_exprt &lhs,
1583  const constant_interval_exprt &rhs)
1584 {
1585  return lhs.bitwise_or(rhs);
1586 }
1587 
1589  const constant_interval_exprt &lhs,
1590  const constant_interval_exprt &rhs)
1591 {
1592  return lhs.bitwise_xor(rhs);
1593 }
1594 
1596 {
1597  return lhs.bitwise_not();
1598 }
1599 
1601  const constant_interval_exprt &lhs,
1602  const constant_interval_exprt &rhs)
1603 {
1604  return lhs.left_shift(rhs);
1605 }
1606 
1608  const constant_interval_exprt &lhs,
1609  const constant_interval_exprt &rhs)
1610 {
1611  return lhs.right_shift(rhs);
1612 }
1613 
1616 {
1617  return a.unary_plus();
1618 }
1619 
1622 {
1623  return a.unary_minus();
1624 }
1625 
1628 {
1629  if(is_boolean() && is_int(type))
1630  {
1631  bool lower = !has_no_lower_bound() && get_lower().is_true();
1632  bool upper = has_no_upper_bound() || get_upper().is_true();
1633 
1634  INVARIANT(!lower || upper, "");
1635 
1636  constant_exprt lower_num = from_integer(lower, type);
1637  constant_exprt upper_num = from_integer(upper, type);
1638 
1639  return constant_interval_exprt(lower_num, upper_num, type);
1640  }
1641  else
1642  {
1643  auto do_typecast = [&type](exprt e) {
1644  if(e.id() == ID_min_value || e.id() == ID_max_value)
1645  {
1646  e.type() = type;
1647  }
1648  else
1649  {
1651  }
1652  return e;
1653  };
1654 
1655  exprt lower = do_typecast(get_lower());
1656  POSTCONDITION(lower.id() == get_lower().id());
1657 
1658  exprt upper = do_typecast(get_upper());
1659  POSTCONDITION(upper.id() == get_upper().id());
1660 
1661  return constant_interval_exprt(lower, upper, type);
1662  }
1663 }
1664 
1665 /* Binary */
1667  const constant_interval_exprt &a,
1668  const constant_interval_exprt &b)
1669 {
1670  return a.plus(b);
1671 }
1672 
1674  const constant_interval_exprt &a,
1675  const constant_interval_exprt &b)
1676 {
1677  return a.minus(b);
1678 }
1679 
1681  const constant_interval_exprt &a,
1682  const constant_interval_exprt &b)
1683 {
1684  return a.multiply(b);
1685 }
1686 
1688  const constant_interval_exprt &a,
1689  const constant_interval_exprt &b)
1690 {
1691  return a.divide(b);
1692 }
1693 
1695  const constant_interval_exprt &a,
1696  const constant_interval_exprt &b)
1697 {
1698  return a.modulo(b);
1699 }
1700 
1701 /* Binary shifts */
1703  const constant_interval_exprt &a,
1704  const constant_interval_exprt &b)
1705 {
1706  return a.left_shift(b);
1707 }
1708 
1710  const constant_interval_exprt &a,
1711  const constant_interval_exprt &b)
1712 {
1713  return a.right_shift(b);
1714 }
1715 
1716 /* Unary bitwise */
1719 {
1720  return a.bitwise_not();
1721 }
1722 
1723 /* Binary bitwise */
1725  const constant_interval_exprt &a,
1726  const constant_interval_exprt &b)
1727 {
1728  return a.bitwise_xor(b);
1729 }
1730 
1732  const constant_interval_exprt &a,
1733  const constant_interval_exprt &b)
1734 {
1735  return a.bitwise_or(b);
1736 }
1737 
1739  const constant_interval_exprt &a,
1740  const constant_interval_exprt &b)
1741 {
1742  return a.bitwise_and(b);
1743 }
1744 
1746  const constant_interval_exprt &a,
1747  const constant_interval_exprt &b)
1748 {
1749  return a.less_than(b);
1750 }
1751 
1753  const constant_interval_exprt &a,
1754  const constant_interval_exprt &b)
1755 {
1756  return a.greater_than(b);
1757 }
1758 
1760  const constant_interval_exprt &a,
1761  const constant_interval_exprt &b)
1762 {
1763  return a.less_than_or_equal(b);
1764 }
1765 
1767  const constant_interval_exprt &a,
1768  const constant_interval_exprt &b)
1769 {
1770  return a.greater_than_or_equal(b);
1771 }
1772 
1774  const constant_interval_exprt &a,
1775  const constant_interval_exprt &b)
1776 {
1777  return a.equal(b);
1778 }
1779 
1781  const constant_interval_exprt &a,
1782  const constant_interval_exprt &b)
1783 {
1784  return a.equal(b);
1785 }
1786 
1789 {
1790  return a.increment();
1791 }
1792 
1795 {
1796  return a.decrement();
1797 }
1798 
1800 {
1801  return a.is_empty();
1802 }
1803 
1805  const constant_interval_exprt &a)
1806 {
1807  return a.is_single_value_interval();
1808 }
1809 
1811 {
1812  return a.is_top();
1813 }
1814 
1816 {
1817  return a.is_bottom();
1818 }
1819 
1821 {
1822  return a.has_no_lower_bound();
1823 }
1824 
1826 {
1827  return a.has_no_upper_bound();
1828 }
1829 
1831 {
1832  for(const auto &op : expr.operands())
1833  {
1834  if(is_extreme(op))
1835  {
1836  return true;
1837  }
1838 
1839  if(op.has_operands())
1840  {
1841  return contains_extreme(op);
1842  }
1843  }
1844 
1845  return false;
1846 }
1847 
1849  const exprt expr1,
1850  const exprt expr2)
1851 {
1852  return contains_extreme(expr1) || contains_extreme(expr2);
1853 }
1854 
1856 {
1857  if(greater_than(get_lower(), get_upper()))
1858  {
1859  return false;
1860  }
1861 
1862  return true;
1863 }
1864 
1866 {
1867  return !is_extreme(get_lower()) && !is_extreme(get_upper()) &&
1868  equal(get_lower(), get_upper());
1869 }
1870 
1872 {
1873  if(!is_numeric())
1874  {
1875  return false;
1876  }
1877 
1878  if(get_lower().is_zero() || get_upper().is_zero())
1879  {
1880  return true;
1881  }
1882 
1883  if(is_unsigned() && is_min(get_lower()))
1884  {
1885  return true;
1886  }
1887 
1888  if(
1891  {
1892  return true;
1893  }
1894 
1895  return false;
1896 }
1897 
1900 {
1901  return interval.is_positive();
1902 }
1903 
1905 {
1906  return interval.is_zero();
1907 }
1908 
1911 {
1912  return interval.is_negative();
1913 }
1914 
1916 {
1917  return is_positive(get_lower()) && is_positive(get_upper());
1918 }
1919 
1921 {
1922  return is_zero(get_lower()) && is_zero(get_upper());
1923 }
1924 
1926 {
1927  return is_negative(get_lower()) && is_negative(get_upper());
1928 }
1929 
1931 {
1932  return a.is_definitely_true();
1933 }
1934 
1936 {
1937  return a.is_definitely_false();
1938 }
1939 
1941  const constant_interval_exprt &a,
1942  const constant_interval_exprt &b)
1943 {
1944  return a.logical_and(b);
1945 }
1946 
1948  const constant_interval_exprt &a,
1949  const constant_interval_exprt &b)
1950 {
1951  return a.logical_or(b);
1952 }
1953 
1955  const constant_interval_exprt &a,
1956  const constant_interval_exprt &b)
1957 {
1958  return a.logical_xor(b);
1959 }
1960 
1962 {
1963  return a.logical_not();
1964 }
1965 
1967 {
1968  if(val.is_true())
1969  {
1971  }
1972  else if(val.is_false())
1973  {
1975  }
1976  else
1977  {
1979  }
1980 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
API to expression classes for bitvectors.
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition: c_types.h:80
binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
Definition: std_expr.h:640
exprt & op1()
Definition: expr.h:136
exprt & lhs()
Definition: std_expr.h:668
exprt & op0()
Definition: expr.h:133
exprt & rhs()
Definition: std_expr.h:678
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:762
The Boolean type.
Definition: std_types.h:36
A constant literal expression.
Definition: std_expr.h:2995
Represents an interval of values.
Definition: interval.h:52
static constant_interval_exprt get_extremes(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs, const irep_idt &operation)
Definition: interval.cpp:471
bool is_negative() const
Definition: interval.cpp:1925
constant_interval_exprt(exprt lower, exprt upper, typet type)
Definition: interval.h:54
max_value_exprt max() const
Definition: interval.cpp:1027
static exprt generate_division_expression(const exprt &lhs, const exprt &rhs)
Definition: interval.cpp:684
static bool is_bottom(const constant_interval_exprt &a)
Definition: interval.cpp:1815
constant_interval_exprt bottom() const
Definition: interval.cpp:1058
constant_interval_exprt minus(const constant_interval_exprt &other) const
Definition: interval.cpp:112
tvt greater_than_or_equal(const constant_interval_exprt &o) const
Definition: interval.cpp:425
min_value_exprt min() const
Definition: interval.cpp:1022
bool is_signed() const
Definition: interval.cpp:1181
tvt greater_than(const constant_interval_exprt &o) const
Definition: interval.cpp:397
constant_interval_exprt bitwise_or(const constant_interval_exprt &o) const
Definition: interval.cpp:345
constant_interval_exprt decrement() const
Definition: interval.cpp:465
tvt less_than_or_equal(const constant_interval_exprt &o) const
Definition: interval.cpp:403
tvt is_definitely_false() const
Definition: interval.cpp:223
constant_interval_exprt left_shift(const constant_interval_exprt &o) const
Definition: interval.cpp:301
tvt not_equal(const constant_interval_exprt &o) const
Definition: interval.cpp:454
static exprt generate_shift_expression(const exprt &lhs, const exprt &rhs, const irep_idt &operation)
Definition: interval.cpp:899
bool has_no_upper_bound() const
Definition: interval.cpp:1206
bool is_bottom() const
Definition: interval.cpp:1037
static bool is_top(const constant_interval_exprt &a)
Definition: interval.cpp:1810
constant_interval_exprt typecast(const typet &type) const
Definition: interval.cpp:1627
constant_interval_exprt multiply(const constant_interval_exprt &o) const
Definition: interval.cpp:124
static constant_interval_exprt tvt_to_interval(const tvt &val)
Definition: interval.cpp:1966
constant_interval_exprt unary_plus() const
Definition: interval.cpp:37
constant_interval_exprt plus(const constant_interval_exprt &o) const
Definition: interval.cpp:74
static exprt get_extreme(std::vector< exprt > values, bool min=true)
Definition: interval.cpp:497
bool is_numeric() const
Definition: interval.cpp:1080
static void append_multiply_expression(const exprt &lower, const exprt &upper, std::vector< exprt > &collection)
Adds all possible values that may arise from multiplication (more than one, in case of past the type ...
Definition: interval.cpp:601
constant_interval_exprt bitwise_xor(const constant_interval_exprt &o) const
Definition: interval.cpp:334
bool is_positive() const
Definition: interval.cpp:1915
bool is_single_value_interval() const
Definition: interval.cpp:1865
constant_interval_exprt increment() const
Definition: interval.cpp:459
bool is_bitvector() const
Definition: interval.cpp:1191
std::string to_string() const
Definition: interval.cpp:1436
bool contains(const constant_interval_exprt &interval) const
Definition: interval.cpp:1427
static bool is_extreme(const exprt &expr)
Definition: interval.cpp:1196
tvt logical_or(const constant_interval_exprt &o) const
Definition: interval.cpp:254
static constant_interval_exprt singleton(const exprt &x)
Definition: interval.h:99
static exprt simplified_expr(exprt expr)
Definition: interval.cpp:987
bool contains_zero() const
Definition: interval.cpp:1871
constant_interval_exprt handle_constant_unary_expression(const irep_idt &op) const
SET OF ARITHMETIC OPERATORS.
Definition: interval.cpp:939
constant_interval_exprt modulo(const constant_interval_exprt &o) const
Definition: interval.cpp:152
static exprt get_max(const exprt &a, const exprt &b)
Definition: interval.cpp:960
bool has_no_lower_bound() const
Definition: interval.cpp:1211
static exprt get_min(const exprt &a, const exprt &b)
Definition: interval.cpp:965
static bool is_max(const constant_interval_exprt &a)
Definition: interval.cpp:1825
static void generate_expression(const exprt &lhs, const exprt &rhs, const irep_idt &operation, std::vector< exprt > &collection)
Definition: interval.cpp:572
constant_interval_exprt eval(const irep_idt &unary_operator) const
Definition: interval.cpp:793
tvt is_definitely_true() const
Definition: interval.cpp:217
bool is_unsigned() const
Definition: interval.cpp:1186
static bool is_min(const constant_interval_exprt &a)
Definition: interval.cpp:1820
static exprt generate_modulo_expression(const exprt &lhs, const exprt &rhs)
Definition: interval.cpp:739
tvt logical_xor(const constant_interval_exprt &o) const
Definition: interval.cpp:273
const exprt & get_lower() const
Definition: interval.cpp:27
static void append_multiply_expression_min(const exprt &min, const exprt &other, std::vector< exprt > &collection)
Appends interval bounds that could arise from MIN * other.
Definition: interval.cpp:664
constant_interval_exprt right_shift(const constant_interval_exprt &o) const
Definition: interval.cpp:318
tvt logical_and(const constant_interval_exprt &o) const
Definition: interval.cpp:265
static void append_multiply_expression_max(const exprt &expr, std::vector< exprt > &collection)
Appends interval bounds that could arise from MAX * expr.
Definition: interval.cpp:639
constant_interval_exprt bitwise_and(const constant_interval_exprt &o) const
Definition: interval.cpp:356
constant_interval_exprt top() const
Definition: interval.cpp:1053
static bool contains_extreme(const exprt expr)
Definition: interval.cpp:1830
constant_interval_exprt unary_minus() const
Definition: interval.cpp:42
constant_exprt zero() const
Definition: interval.cpp:1017
tvt less_than(const constant_interval_exprt &o) const
Definition: interval.cpp:376
static exprt abs(const exprt &expr)
Definition: interval.cpp:1300
constant_interval_exprt bitwise_not() const
Definition: interval.cpp:366
constant_interval_exprt divide(const constant_interval_exprt &o) const
Definition: interval.cpp:135
static constant_interval_exprt simplified_interval(exprt &l, exprt &r)
Definition: interval.cpp:982
constant_interval_exprt handle_constant_binary_expression(const constant_interval_exprt &other, const irep_idt &) const
Definition: interval.cpp:951
tvt logical_not() const
Definition: interval.cpp:283
const exprt & get_upper() const
Definition: interval.cpp:32
tvt equal(const constant_interval_exprt &o) const
Definition: interval.cpp:431
Division.
Definition: std_expr.h:1157
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Equality.
Definition: std_expr.h:1366
Base class for all expressions.
Definition: expr.h:56
bool is_one() const
Return whether the expression is a constant representing 1.
Definition: expr.cpp:96
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:27
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.h:224
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:34
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:47
typet & type()
Return the type of the expression.
Definition: expr.h:84
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.h:212
operandst & operands()
Definition: expr.h:94
The Boolean constant false.
Definition: std_expr.h:3077
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
bool is_not_nil() const
Definition: irep.h:372
const irep_idt & id() const
Definition: irep.h:388
bool is_nil() const
Definition: irep.h:368
+∞ upper bound for intervals
Definition: interval.h:18
-∞ upper bound for intervals
Definition: interval.h:33
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition: std_expr.h:1228
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1107
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
The NIL expression.
Definition: std_expr.h:3086
The plus expression Associativity is not specified.
Definition: std_expr.h:1002
A base class for shift and rotate operators.
The symbol table.
Definition: symbol_table.h:14
The Boolean constant true.
Definition: std_expr.h:3068
Definition: threeval.h:20
bool is_false() const
Definition: threeval.h:26
bool is_true() const
Definition: threeval.h:25
static tvt unknown()
Definition: threeval.h:33
Semantic type conversion.
Definition: std_expr.h:2073
The type of an expression, extends irept.
Definition: type.h:29
Generic base class for unary expressions.
Definition: std_expr.h:361
The unary minus expression.
Definition: std_expr.h:484
const constant_interval_exprt operator/(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1553
bool operator<=(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1511
const constant_interval_exprt operator%(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1567
const constant_interval_exprt operator>>(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1607
std::ostream & operator<<(std::ostream &out, const constant_interval_exprt &i)
Definition: interval.cpp:1443
bool operator==(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1525
bool operator<(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1497
const constant_interval_exprt operator&(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1574
bool operator>(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1504
const constant_interval_exprt operator+(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1539
bool operator!=(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1532
const constant_interval_exprt operator-(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1546
const constant_interval_exprt operator*(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1560
const constant_interval_exprt operator^(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1588
const constant_interval_exprt operator|(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1581
bool operator>=(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1518
const constant_interval_exprt operator!(const constant_interval_exprt &lhs)
Definition: interval.cpp:1595
static int8_t r
Definition: irep_hash.h:60
exprt simplify_expr(exprt src, const namespacet &ns)
BigInt mp_integer
Definition: smt_terms.h:17
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define POSTCONDITION(CONDITION)
Definition: invariant.h:479
API to expression classes.
Author: Diffblue Ltd.