diff --git a/src/solvers/strings/string_constraint_generator.h b/src/solvers/strings/string_constraint_generator.h index f439e5f28b3..64cc176b14f 100644 --- a/src/solvers/strings/string_constraint_generator.h +++ b/src/solvers/strings/string_constraint_generator.h @@ -143,9 +143,6 @@ class string_constraint_generatort final const function_application_exprt &f, bool swap_arguments); - std::pair add_axioms_for_is_suffix( - const function_application_exprt &f, - bool swap_arguments); std::pair add_axioms_for_length(const function_application_exprt &f); std::pair diff --git a/src/solvers/strings/string_constraint_generator_main.cpp b/src/solvers/strings/string_constraint_generator_main.cpp index 81603410ed6..1a8dfb36e58 100644 --- a/src/solvers/strings/string_constraint_generator_main.cpp +++ b/src/solvers/strings/string_constraint_generator_main.cpp @@ -231,11 +231,39 @@ string_constraint_generatort::add_axioms_for_function_application( else if(id == ID_cprover_string_is_prefix_func) return add_axioms_for_is_prefix(expr, false); else if(id == ID_cprover_string_is_suffix_func) - return add_axioms_for_is_suffix(expr, false); + { + // Replaced deprecated add_axioms_for_is_suffix with is_prefix + offset + // To check if args[0] is a suffix of args[1], we check if args[0] is + // a prefix of args[1] starting at offset args[1].length - args[0].length + const function_application_exprt::argumentst &args = expr.arguments(); + PRECONDITION(args.size() == 2); + PRECONDITION(expr.type() == bool_typet() || expr.type().id() == ID_c_bool); + const array_string_exprt &suffix = get_string_expr(array_pool, args[0]); + const array_string_exprt &str = get_string_expr(array_pool, args[1]); + const exprt offset = minus_exprt( + array_pool.get_or_create_length(str), + array_pool.get_or_create_length(suffix)); + auto pair = add_axioms_for_is_prefix(suffix, str, offset); + return {typecast_exprt(pair.first, expr.type()), std::move(pair.second)}; + } else if(id == ID_cprover_string_startswith_func) return add_axioms_for_is_prefix(expr, true); else if(id == ID_cprover_string_endswith_func) - return add_axioms_for_is_suffix(expr, true); + { + // Replaced deprecated add_axioms_for_is_suffix with is_prefix + offset + // To check if args[1] is a suffix of args[0] (swapped arguments), we check + // if args[1] is a prefix of args[0] starting at offset args[0].length - args[1].length + const function_application_exprt::argumentst &args = expr.arguments(); + PRECONDITION(args.size() == 2); + PRECONDITION(expr.type() == bool_typet() || expr.type().id() == ID_c_bool); + const array_string_exprt &suffix = get_string_expr(array_pool, args[1]); + const array_string_exprt &str = get_string_expr(array_pool, args[0]); + const exprt offset = minus_exprt( + array_pool.get_or_create_length(str), + array_pool.get_or_create_length(suffix)); + auto pair = add_axioms_for_is_prefix(suffix, str, offset); + return {typecast_exprt(pair.first, expr.type()), std::move(pair.second)}; + } else if(id == ID_cprover_string_contains_func) return add_axioms_for_contains(expr); else if(id == ID_cprover_string_index_of_func) diff --git a/src/solvers/strings/string_constraint_generator_testing.cpp b/src/solvers/strings/string_constraint_generator_testing.cpp index 9fab7d39601..fbb5629d644 100644 --- a/src/solvers/strings/string_constraint_generator_testing.cpp +++ b/src/solvers/strings/string_constraint_generator_testing.cpp @@ -145,89 +145,6 @@ string_constraint_generatort::add_axioms_for_is_empty( return {typecast_exprt(is_empty, f.type()), std::move(constraints)}; } -/// Test if the target is a suffix of the string -/// -/// Add axioms ensuring the return value is true when the first string ends with -/// the given target. -/// These axioms are: -/// 1. \f$ \texttt{issuffix} \Rightarrow |s_0| \ge |s_1| \f$ -/// 2. \f$ \forall i <|s_1|.\ {\tt issuffix} -/// \Rightarrow s_1[i] = s_0[i + |s_0| - |s_1|] -/// \f$ -/// 3. \f$ \lnot {\tt issuffix} \Rightarrow -/// (|s_1| > |s_0| \land {\tt witness}=-1) -/// \lor (|s_1| > {witness} \ge 0 -/// \land s_1[{witness}] \ne s_0[{witness} + |s_0| - |s_1|] \f$ -/// -/// \todo The primitive should be renamed `ends_with`. -/// \param f: a function application with arguments refined_string `s0` -/// and refined_string `s1` -/// \param swap_arguments: boolean flag telling whether the suffix is the second -/// argument or the first argument -/// \return Boolean expression `issuffix` -/// \deprecated Should use `strings_startwith(s0, s1, s1.length - s0.length)`. -DEPRECATED(SINCE(2018, 6, 6, "should use strings_startwith")) -std::pair -string_constraint_generatort::add_axioms_for_is_suffix( - const function_application_exprt &f, - bool swap_arguments) -{ - const function_application_exprt::argumentst &args = f.arguments(); - PRECONDITION(args.size() == 2); // bad args to string issuffix? - PRECONDITION(f.type() == bool_typet() || f.type().id() == ID_c_bool); - - string_constraintst constraints; - symbol_exprt issuffix = fresh_symbol("issuffix"); - typecast_exprt tc_issuffix(issuffix, f.type()); - const array_string_exprt &s0 = - get_string_expr(array_pool, args[swap_arguments ? 1u : 0u]); - const array_string_exprt &s1 = - get_string_expr(array_pool, args[swap_arguments ? 0u : 1u]); - const typet &index_type = s0.length_type(); - - implies_exprt a1( - issuffix, - greater_or_equal_to( - array_pool.get_or_create_length(s1), - array_pool.get_or_create_length(s0))); - constraints.existential.push_back(a1); - - symbol_exprt qvar = fresh_symbol("QA_suffix", index_type); - const plus_exprt qvar_shifted( - qvar, - minus_exprt( - array_pool.get_or_create_length(s1), - array_pool.get_or_create_length(s0))); - string_constraintt a2( - qvar, - zero_if_negative(array_pool.get_or_create_length(s0)), - implies_exprt(issuffix, equal_exprt(s0[qvar], s1[qvar_shifted])), - message_handler); - constraints.universal.push_back(a2); - - symbol_exprt witness = fresh_symbol("witness_not_suffix", index_type); - const plus_exprt shifted( - witness, - minus_exprt( - array_pool.get_or_create_length(s1), - array_pool.get_or_create_length(s0))); - or_exprt constr3( - and_exprt( - greater_than( - array_pool.get_or_create_length(s0), - array_pool.get_or_create_length(s1)), - equal_exprt(witness, from_integer(-1, index_type))), - and_exprt( - notequal_exprt(s0[witness], s1[shifted]), - and_exprt( - greater_than(array_pool.get_or_create_length(s0), witness), - is_positive(witness)))); - implies_exprt a3(not_exprt(issuffix), constr3); - - constraints.existential.push_back(a3); - return {tc_issuffix, std::move(constraints)}; -} - /// Test whether a string contains another /// /// Add axioms ensuring the returned value is true when the first string