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