Get rid of calls to plus_exprt_with_overflow

This function is adding assumptions on the values of integers which may
lead to contradiction. It is better to deal with overflows at the level
of the specification of the builtin functions instead.

Author: romainbrenguier

src/solvers/refinement/string_constraint_generator_code_points.cpp

@@ -128,12 +128,11 @@ exprt string_constraint_generatort::add_axioms_for_code_point_at(
   const symbol_exprt result = fresh_symbol("char", return_type);
   const exprt index1 = from_integer(1, str.length().type());
   const exprt &char1=str[pos];
-  const exprt &char2=str[plus_exprt_with_overflow_check(pos, index1)];
+  const exprt &char2 = str[plus_exprt(pos, index1)];
   const typecast_exprt char1_as_int(char1, return_type);
   const typecast_exprt char2_as_int(char2, return_type);
   const exprt pair = pair_value(char1_as_int, char2_as_int, return_type);
-  const exprt is_low =
-    is_low_surrogate(str[plus_exprt_with_overflow_check(pos, index1)]);
+  const exprt is_low = is_low_surrogate(str[plus_exprt(pos, index1)]);
   const and_exprt return_pair(is_high_surrogate(str[pos]), is_low);
 
   lemmas.push_back(implies_exprt(return_pair, equal_exprt(result, pair)));
@@ -210,8 +209,8 @@ exprt string_constraint_generatort::add_axioms_for_offset_by_code_point(
   const typet &return_type=f.type();
   const symbol_exprt result = fresh_symbol("offset_by_code_point", return_type);
 
-  const exprt minimum = plus_exprt_with_overflow_check(index, offset);
-  const exprt maximum = plus_exprt_with_overflow_check(minimum, offset);
+  const exprt minimum = plus_exprt(index, offset);
+  const exprt maximum = plus_exprt(minimum, offset);
   lemmas.push_back(binary_relation_exprt(result, ID_le, maximum));
   lemmas.push_back(binary_relation_exprt(result, ID_ge, minimum));
 

src/solvers/refinement/string_constraint_generator_indexof.cpp

@@ -352,8 +352,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of(
   lemmas.push_back(a3);
 
   const exprt index1 = from_integer(1, index_type);
-  const exprt from_index_plus_one =
-    plus_exprt_with_overflow_check(from_index, index1);
+  const plus_exprt from_index_plus_one(from_index, index1);
   const if_exprt end_index(
     binary_relation_exprt(from_index_plus_one, ID_le, str.length()),
     from_index_plus_one,

src/solvers/refinement/string_constraint_generator_testing.cpp

@@ -36,11 +36,10 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix(
   symbol_exprt isprefix=fresh_boolean("isprefix");
   const typet &index_type=str.length().type();
 
-  implies_exprt a1(
-    isprefix,
-    str.axiom_for_length_ge(plus_exprt_with_overflow_check(
-      prefix.length(), offset)));
-  lemmas.push_back(a1);
+  // Axiom 1.
+  lemmas.push_back(
+    implies_exprt(
+      isprefix, str.axiom_for_length_ge(plus_exprt(prefix.length(), offset))));
 
   symbol_exprt qvar=fresh_univ_index("QA_isprefix", index_type);
   string_constraintt a2(

src/solvers/refinement/string_constraint_generator_transformation.cpp

@@ -175,9 +175,8 @@ exprt string_constraint_generatort::add_axioms_for_trim(
   const symbol_exprt idx = fresh_exist_index("index_trim", index_type);
   const exprt space_char = from_integer(' ', char_type);
 
-  exprt a1=str.axiom_for_length_ge(
-    plus_exprt_with_overflow_check(idx, res.length()));
-  lemmas.push_back(a1);
+  // Axiom 1.
+  lemmas.push_back(str.axiom_for_length_ge(plus_exprt(idx, res.length())));
 
   binary_relation_exprt a2(idx, ID_ge, from_integer(0, index_type));
   lemmas.push_back(a2);
@@ -197,32 +196,31 @@ exprt string_constraint_generatort::add_axioms_for_trim(
   string_constraintt a6(n, idx, non_print);
   constraints.push_back(a6);
 
-  symbol_exprt n2=fresh_univ_index("QA_index_trim2", index_type);
-  minus_exprt bound(str.length(), plus_exprt_with_overflow_check(idx,
-                                                                 res.length()));
-  binary_relation_exprt eqn2(
-    str[plus_exprt(idx, plus_exprt(res.length(), n2))],
-    ID_le,
-    space_char);
-
-  string_constraintt a7(n2, bound, eqn2);
-  constraints.push_back(a7);
+  // Axiom 7.
+  constraints.push_back([&] { // NOLINT
+    const symbol_exprt n2 = fresh_univ_index("QA_index_trim2", index_type);
+    const minus_exprt bound(minus_exprt(str.length(), idx), res.length());
+    const binary_relation_exprt eqn2(
+      str[plus_exprt(idx, plus_exprt(res.length(), n2))], ID_le, space_char);
+    return string_constraintt(n2, bound, eqn2);
+  }());
 
   symbol_exprt n3=fresh_univ_index("QA_index_trim3", index_type);
   equal_exprt eqn3(res[n3], str[plus_exprt(n3, idx)]);
   string_constraintt a8(n3, res.length(), eqn3);
   constraints.push_back(a8);
 
-  minus_exprt index_before(
-    plus_exprt_with_overflow_check(idx, res.length()),
-      from_integer(1, index_type));
-  binary_relation_exprt no_space_before(str[index_before], ID_gt, space_char);
-  or_exprt a9(
-    equal_exprt(idx, str.length()),
-    and_exprt(
-      binary_relation_exprt(str[idx], ID_gt, space_char),
-      no_space_before));
-  lemmas.push_back(a9);
+  // Axiom 9.
+  lemmas.push_back([&] {
+    const plus_exprt index_before(
+      idx, minus_exprt(res.length(), from_integer(1, index_type)));
+    const binary_relation_exprt no_space_before(
+      str[index_before], ID_gt, space_char);
+    return or_exprt(
+      equal_exprt(idx, str.length()),
+      and_exprt(
+        binary_relation_exprt(str[idx], ID_gt, space_char), no_space_before));
+  }());
   return from_integer(0, f.type());
 }
 
@@ -511,10 +509,7 @@ exprt string_constraint_generatort::add_axioms_for_delete_char_at(
   const array_string_exprt str = get_string_expr(f.arguments()[2]);
   exprt index_one=from_integer(1, str.length().type());
   return add_axioms_for_delete(
-    res,
-    str,
-    f.arguments()[3],
-    plus_exprt_with_overflow_check(f.arguments()[3], index_one));
+    res, str, f.arguments()[3], plus_exprt(f.arguments()[3], index_one));
 }
 
 /// Add axioms stating that `res` corresponds to the input `str`