Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 0 additions & 3 deletions src/solvers/strings/string_constraint_generator.h
Original file line number Diff line number Diff line change
Expand Up @@ -143,9 +143,6 @@ class string_constraint_generatort final
const function_application_exprt &f,
bool swap_arguments);

std::pair<exprt, string_constraintst> add_axioms_for_is_suffix(
const function_application_exprt &f,
bool swap_arguments);
std::pair<exprt, string_constraintst>
add_axioms_for_length(const function_application_exprt &f);
std::pair<exprt, string_constraintst>
Expand Down
32 changes: 30 additions & 2 deletions src/solvers/strings/string_constraint_generator_main.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
83 changes: 0 additions & 83 deletions src/solvers/strings/string_constraint_generator_testing.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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<exprt, string_constraintst>
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
Expand Down
Loading