Remove deprecated add_axioms_for_concat function

src/solvers/strings/string_concatenation_builtin_function.cpp

@@ -148,25 +148,6 @@ exprt length_constraint_for_concat_char(
       array_pool.get_or_create_length(s1), from_integer(1, s1.length_type())));
 }
 
-/// Add axioms enforcing that `res` is equal to the concatenation of `s1` and
-/// `s2`.
-///
-/// \deprecated should use concat_substr instead
-/// \param res: string_expression corresponding to the result
-/// \param s1: the string expression to append to
-/// \param s2: the string expression to append to the first one
-/// \return an integer expression
-std::pair<exprt, string_constraintst>
-string_constraint_generatort::add_axioms_for_concat(
-  const array_string_exprt &res,
-  const array_string_exprt &s1,
-  const array_string_exprt &s2)
-{
-  exprt index_zero = from_integer(0, s2.length_type());
-  return add_axioms_for_concat_substr(
-    res, s1, s2, index_zero, array_pool.get_or_create_length(s2));
-}
-
 /// Add axioms corresponding to the StringBuilder.appendCodePoint(I) function
 /// \deprecated java specific
 /// \param f: function application with two arguments: a string and a code point
@@ -185,7 +166,12 @@ string_constraint_generatort::add_axioms_for_concat_code_point(
     array_pool.fresh_string(index_type, char_type);
   return combine_results(
     add_axioms_for_code_point(code_point, f.arguments()[3]),
-    add_axioms_for_concat(res, s1, code_point));
+    add_axioms_for_concat_substr(
+      res,
+      s1,
+      code_point,
+      from_integer(0, code_point.length_type()),
+      array_pool.get_or_create_length(code_point)));
 }
 
 std::vector<mp_integer> string_concatenation_builtin_functiont::eval(
@@ -216,7 +202,12 @@ string_constraintst string_concatenation_builtin_functiont::constraints(
 {
   auto pair = [&]() -> std::pair<exprt, string_constraintst> {
     if(args.size() == 0)
-      return generator.add_axioms_for_concat(result, input1, input2);
+      return generator.add_axioms_for_concat_substr(
+        result,
+        input1,
+        input2,
+        from_integer(0, input2.length_type()),
+        generator.array_pool.get_or_create_length(input2));
     if(args.size() == 2)
     {
       return generator.add_axioms_for_concat_substr(

src/solvers/strings/string_constraint_generator.h

@@ -83,11 +83,6 @@ class string_constraint_generatort final
     const function_application_exprt &f);
 
 public:
-  std::pair<exprt, string_constraintst> add_axioms_for_concat(
-    const array_string_exprt &res,
-    const array_string_exprt &s1,
-    const array_string_exprt &s2);
-
   std::pair<exprt, string_constraintst> add_axioms_for_concat_substr(
     const array_string_exprt &res,
     const array_string_exprt &s1,

src/solvers/strings/string_constraint_generator_float.cpp

@@ -223,8 +223,12 @@ string_constraint_generatort::add_axioms_for_string_of_float(
   auto result2 =
     add_axioms_for_string_of_int(integer_part_str, integer_part, 8);
 
-  auto result3 =
-    add_axioms_for_concat(res, integer_part_str, fractional_part_str);
+  auto result3 = add_axioms_for_concat_substr(
+    res,
+    integer_part_str,
+    fractional_part_str,
+    from_integer(0, fractional_part_str.length_type()),
+    array_pool.get_or_create_length(fractional_part_str));
   merge(result3.second, std::move(result1.second));
   merge(result3.second, std::move(result2.second));
 
@@ -475,19 +479,25 @@ string_constraint_generatort::add_axioms_from_float_scientific_notation(
   //   concat(string_with_do, string_fractional_part)
   const array_string_exprt string_expr_with_fractional_part =
     array_pool.fresh_string(index_type, char_type);
-  auto result3 = add_axioms_for_concat(
+  auto result3 = add_axioms_for_concat_substr(
     string_expr_with_fractional_part,
     string_expr_integer_part,
-    string_fractional_part);
+    string_fractional_part,
+    from_integer(0, string_fractional_part.length_type()),
+    array_pool.get_or_create_length(string_fractional_part));
 
   // string_expr_with_E = concat(string_fraction, string_lit_E)
   const array_string_exprt stringE =
     array_pool.fresh_string(index_type, char_type);
   auto result4 = add_axioms_for_constant(stringE, "E");
   const array_string_exprt string_expr_with_E =
     array_pool.fresh_string(index_type, char_type);
-  auto result5 = add_axioms_for_concat(
-    string_expr_with_E, string_expr_with_fractional_part, stringE);
+  auto result5 = add_axioms_for_concat_substr(
+    string_expr_with_E,
+    string_expr_with_fractional_part,
+    stringE,
+    from_integer(0, stringE.length_type()),
+    array_pool.get_or_create_length(stringE));
 
   // exponent_string = string_of_int(decimal_exponent)
   const array_string_exprt exponent_string =
@@ -496,8 +506,12 @@ string_constraint_generatort::add_axioms_from_float_scientific_notation(
     add_axioms_for_string_of_int(exponent_string, decimal_exponent, 3);
 
   // string_expr = concat(string_expr_with_E, exponent_string)
-  auto result7 =
-    add_axioms_for_concat(res, string_expr_with_E, exponent_string);
+  auto result7 = add_axioms_for_concat_substr(
+    res,
+    string_expr_with_E,
+    exponent_string,
+    from_integer(0, exponent_string.length_type()),
+    array_pool.get_or_create_length(exponent_string));
 
   const exprt return_code = maximum(
     result1.first,

src/solvers/strings/string_constraint_generator_transformation.cpp

@@ -372,8 +372,6 @@ string_constraint_generatort::add_axioms_for_delete_char_at(
 /// These axioms are the same as would be generated for:
 /// `concat(substring(str, 0, start), substring(end, |str|))`
 /// (see \ref add_axioms_for_substring and \ref add_axioms_for_concat_substr).
-/// \todo Should use add_axioms_for_concat_substr instead
-///       of add_axioms_for_concat
 /// \param res: array of characters expression
 /// \param str: array of characters expression
 /// \param start: integer expression
@@ -400,7 +398,12 @@ string_constraint_generatort::add_axioms_for_delete(
     combine_results(
       add_axioms_for_substring(
         sub2, str, end, array_pool.get_or_create_length(str)),
-      add_axioms_for_concat(res, sub1, sub2)));
+      add_axioms_for_concat_substr(
+        res,
+        sub1,
+        sub2,
+        from_integer(0, sub2.length_type()),
+        array_pool.get_or_create_length(sub2))));
 }
 
 /// Remove a portion of a string

src/solvers/strings/string_format_builtin_function.cpp

@@ -384,14 +384,23 @@ static std::pair<exprt, string_constraintst> add_axioms_for_format(
     const array_string_exprt &intermediary = intermediary_strings[i];
     const array_string_exprt fresh =
       array_pool.fresh_string(index_type, char_type);
-    auto result = generator.add_axioms_for_concat(fresh, str, intermediary);
+    auto result = generator.add_axioms_for_concat_substr(
+      fresh,
+      str,
+      intermediary,
+      from_integer(0, intermediary.length_type()),
+      array_pool.get_or_create_length(intermediary));
     return_code = maximum(return_code, result.first);
     merge(constraints, std::move(result.second));
     str = fresh;
   }
 
-  auto result =
-    generator.add_axioms_for_concat(res, str, intermediary_strings.back());
+  auto result = generator.add_axioms_for_concat_substr(
+    res,
+    str,
+    intermediary_strings.back(),
+    from_integer(0, intermediary_strings.back().length_type()),
+    array_pool.get_or_create_length(intermediary_strings.back()));
   merge(constraints, std::move(result.second));
   return {maximum(result.first, return_code), std::move(constraints)};
 }