Skip to content

Remove deprecated add_axioms_for_is_empty method #8915

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
tautschnig wants to merge 1 commit into
base: develop
Choose a base branch
from
Draft

Remove deprecated add_axioms_for_is_empty method #8915

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
2 changes: 0 additions & 2 deletions src/solvers/strings/string_constraint_generator.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -133,8 +133,6 @@ class string_constraint_generatort final
std::pair<exprt, string_constraintst>
add_axioms_for_equals_ignore_case(const function_application_exprt &f);

std::pair<exprt, string_constraintst>
add_axioms_for_is_empty(const function_application_exprt &f);
std::pair<exprt, string_constraintst> add_axioms_for_is_prefix(
const array_string_exprt &prefix,
const array_string_exprt &str,
Expand Down
16 changes: 15 additions & 1 deletion src/solvers/strings/string_constraint_generator_main.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -225,7 +225,21 @@ string_constraint_generatort::add_axioms_for_function_application(
else if(id == ID_cprover_string_equals_ignore_case_func)
return add_axioms_for_equals_ignore_case(expr);
else if(id == ID_cprover_string_is_empty_func)
return add_axioms_for_is_empty(expr);
{
// Inlined logic from deprecated add_axioms_for_is_empty
// Returns true when the string is empty (length == 0)
PRECONDITION(expr.type() == bool_typet() || expr.type().id() == ID_c_bool);
PRECONDITION(expr.arguments().size() == 1);
const array_string_exprt s0 =
get_string_expr(array_pool, expr.arguments()[0]);
const symbol_exprt is_empty = fresh_symbol("is_empty");
string_constraintst constraints;
constraints.existential = {
implies_exprt(is_empty, equal_to(array_pool.get_or_create_length(s0), 0)),
implies_exprt(
equal_to(array_pool.get_or_create_length(s0), 0), is_empty)};
return {typecast_exprt(is_empty, expr.type()), std::move(constraints)};
}
else if(id == ID_cprover_string_char_at_func)
return add_axioms_for_char_at(expr);
else if(id == ID_cprover_string_is_prefix_func)
Expand Down
30 changes: 2 additions & 28 deletions src/solvers/strings/string_constraint_generator_testing.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,11 +10,10 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
/// \file
/// Generates string constraints for string functions that return Boolean values

#include "string_constraint_generator.h"

#include <util/deprecate.h>
#include <util/mathematical_expr.h>

#include "string_constraint_generator.h"

/// Add axioms stating that the returned expression is true exactly when the
/// offset is greater or equal to 0 and the first string is a prefix of the
/// second one, starting at position offset.
Expand Down Expand Up @@ -120,31 +119,6 @@ string_constraint_generatort::add_axioms_for_is_prefix(
return {typecast_exprt(pair.first, f.type()), std::move(pair.second)};
}

/// Add axioms stating that the returned value is true exactly when the argument
/// string is empty.
/// \deprecated should use `string_length(s)==0` instead
/// \param f: function application with a string argument
/// \return a Boolean expression
DEPRECATED(SINCE(2017, 10, 5, "should use `string_length s == 0` instead"))
std::pair<exprt, string_constraintst>
string_constraint_generatort::add_axioms_for_is_empty(
const function_application_exprt &f)
{
PRECONDITION(f.type() == bool_typet() || f.type().id() == ID_c_bool);
PRECONDITION(f.arguments().size() == 1);
// We add axioms:
// a1 : is_empty => |s0| = 0
// a2 : s0 => is_empty

symbol_exprt is_empty = fresh_symbol("is_empty");
array_string_exprt s0 = get_string_expr(array_pool, f.arguments()[0]);
string_constraintst constraints;
constraints.existential = {
implies_exprt(is_empty, equal_to(array_pool.get_or_create_length(s0), 0)),
implies_exprt(equal_to(array_pool.get_or_create_length(s0), 0), 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
Expand Down
Loading