diff --git a/src/solvers/strings/string_concatenation_builtin_function.cpp b/src/solvers/strings/string_concatenation_builtin_function.cpp index 96de6af270c..e00b26fd92b 100644 --- a/src/solvers/strings/string_concatenation_builtin_function.cpp +++ b/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 -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 string_concatenation_builtin_functiont::eval( @@ -216,7 +202,12 @@ string_constraintst string_concatenation_builtin_functiont::constraints( { auto pair = [&]() -> std::pair { 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( diff --git a/src/solvers/strings/string_constraint_generator.h b/src/solvers/strings/string_constraint_generator.h index f439e5f28b3..2a00560d2dc 100644 --- a/src/solvers/strings/string_constraint_generator.h +++ b/src/solvers/strings/string_constraint_generator.h @@ -83,11 +83,6 @@ class string_constraint_generatort final const function_application_exprt &f); public: - std::pair add_axioms_for_concat( - const array_string_exprt &res, - const array_string_exprt &s1, - const array_string_exprt &s2); - std::pair add_axioms_for_concat_substr( const array_string_exprt &res, const array_string_exprt &s1, diff --git a/src/solvers/strings/string_constraint_generator_float.cpp b/src/solvers/strings/string_constraint_generator_float.cpp index e33c5794a51..ddb77e1100e 100644 --- a/src/solvers/strings/string_constraint_generator_float.cpp +++ b/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,10 +479,12 @@ 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 = @@ -486,8 +492,12 @@ string_constraint_generatort::add_axioms_from_float_scientific_notation( 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, diff --git a/src/solvers/strings/string_constraint_generator_transformation.cpp b/src/solvers/strings/string_constraint_generator_transformation.cpp index fc33eaec861..1a165045057 100644 --- a/src/solvers/strings/string_constraint_generator_transformation.cpp +++ b/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 diff --git a/src/solvers/strings/string_format_builtin_function.cpp b/src/solvers/strings/string_format_builtin_function.cpp index 14e32a86e8c..7eb6404caf9 100644 --- a/src/solvers/strings/string_format_builtin_function.cpp +++ b/src/solvers/strings/string_format_builtin_function.cpp @@ -384,14 +384,23 @@ static std::pair 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)}; }