Skip to content

Simplify when combining string-refinement result constraints #4957

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

Merged
merged 2 commits into from
Sep 3, 2019
Merged

Simplify when combining string-refinement result constraints #4957

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
4c48218
Move add_axiom methods to string_constraint_generator
JohnDumbell Aug 13, 2019
303ec4d
Simplify when combining string-refinement result constraints
JohnDumbell Jul 25, 2019
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
84 changes: 42 additions & 42 deletions src/solvers/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -419,92 +419,92 @@ This is described in more detail \link string_builtin_functiont here. \endlink
* `cprover_string_associate_length_to_array` : Link the length of the array
with the given integer value.
* `cprover_string_char_at` :
\copybrief add_axioms_for_char_at(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
\link add_axioms_for_char_at More... \endlink
\copybrief string_constraint_generatort::add_axioms_for_char_at(const function_application_exprt &f)
\link string_constraint_generatort::add_axioms_for_char_at More... \endlink
* `cprover_string_length` :
\copybrief add_axioms_for_length(const function_application_exprt &f, array_poolt &array_pool)
\link add_axioms_for_length More... \endlink
\copybrief string_constraint_generatort::add_axioms_for_length(const function_application_exprt &f)
\link string_constraint_generatort::add_axioms_for_length More... \endlink

\subsection comparisons Comparisons:

* `cprover_string_compare_to` :
\copybrief add_axioms_for_compare_to(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool)
\link add_axioms_for_compare_to(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) More... \endlink
\copybrief string_constraint_generatort::add_axioms_for_compare_to(const function_application_exprt &f)
\link string_constraint_generatort::add_axioms_for_compare_to(const function_application_exprt &f) More... \endlink
* `cprover_string_contains` :
\copybrief add_axioms_for_contains(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool)
\link add_axioms_for_contains(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) More... \endlink
\copybrief string_constraint_generatort::add_axioms_for_contains(const function_application_exprt &f)
\link string_constraint_generatort::add_axioms_for_contains(const function_application_exprt &f) More... \endlink
* `cprover_string_equals` :
\copybrief add_axioms_for_equals(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool)
\link add_axioms_for_equals(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) More... \endlink
\copybrief string_constraint_generatort::add_axioms_for_equals(const function_application_exprt &f)
\link string_constraint_generatort::add_axioms_for_equals(const function_application_exprt &f) More... \endlink
* `cprover_string_equals_ignore_case` :
\copybrief add_axioms_for_equals_ignore_case(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool)
\link add_axioms_for_equals_ignore_case(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) More... \endlink
\copybrief string_constraint_generatort::add_axioms_for_equals_ignore_case(const function_application_exprt &f)
\link string_constraint_generatort::add_axioms_for_equals_ignore_case(const function_application_exprt &f) More... \endlink
* `cprover_string_is_prefix` :
\copybrief add_axioms_for_is_prefix
\link add_axioms_for_is_prefix More... \endlink
\copybrief string_constraint_generatort::add_axioms_for_is_prefix
\link string_constraint_generatort::add_axioms_for_is_prefix More... \endlink
* `cprover_string_index_of` :
\copybrief add_axioms_for_index_of(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
\link add_axioms_for_index_of(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
\copybrief string_constraint_generatort::add_axioms_for_index_of(const function_application_exprt &f=)
\link string_constraint_generatort::add_axioms_for_index_of(const function_application_exprt &f) More... \endlink
* `cprover_string_last_index_of` :
\copybrief add_axioms_for_last_index_of(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
\link add_axioms_for_last_index_of(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
\copybrief string_constraint_generatort::add_axioms_for_last_index_of(const function_application_exprt &f)
\link string_constraint_generatort::add_axioms_for_last_index_of(const function_application_exprt &f) More... \endlink

\subsection transformations Transformations:

* `cprover_string_char_set` :
\copybrief string_set_char_builtin_functiont::constraints
\link string_set_char_builtin_functiont::constraints More... \endlink
* `cprover_string_concat` :
\copybrief add_axioms_for_concat
\link add_axioms_for_concat More... \endlink
\copybrief string_constraint_generatort::add_axioms_for_concat
\link string_constraint_generatort::add_axioms_for_concat More... \endlink
* `cprover_string_delete` :
\copybrief add_axioms_for_delete(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
\link add_axioms_for_delete(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
\copybrief string_constraint_generatort::add_axioms_for_delete(const function_application_exprt &f)
\link string_constraint_generatort::add_axioms_for_delete(const function_application_exprt &f) More... \endlink
* `cprover_string_insert` :
\copybrief string_insertion_builtin_functiont::constraints(string_constraint_generatort &generator) const
\link string_insertion_builtin_functiont::constraints(string_constraint_generatort &generator) const More... \endlink
* `cprover_string_replace` :
\copybrief add_axioms_for_replace(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
\link add_axioms_for_replace(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
\copybrief string_constraint_generatort::add_axioms_for_replace(const function_application_exprt &f)
\link string_constraint_generatort::add_axioms_for_replace(const function_application_exprt &f) More... \endlink
* `cprover_string_set_length` :
\copybrief add_axioms_for_set_length(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
\link add_axioms_for_set_length(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
\copybrief string_constraint_generatort::add_axioms_for_set_length(const function_application_exprt &f)
\link string_constraint_generatort::add_axioms_for_set_length(const function_application_exprt &f) More... \endlink
* `cprover_string_substring` :
\copybrief add_axioms_for_substring(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
\link add_axioms_for_substring(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
\copybrief string_constraint_generatort::add_axioms_for_substring(const function_application_exprt &f)
\link string_constraint_generatort::add_axioms_for_substring(const function_application_exprt &f) More... \endlink
* `cprover_string_to_lower_case` :
\copybrief string_to_lower_case_builtin_functiont::constraints
\link string_to_lower_case_builtin_functiont::constraints More... \endlink
* `cprover_string_to_upper_case` :
\copybrief string_to_upper_case_builtin_functiont::constraints
\link string_to_upper_case_builtin_functiont::constraints More... \endlink
* `cprover_string_trim` :
\copybrief add_axioms_for_trim(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
\link add_axioms_for_trim(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
\copybrief string_constraint_generatort::add_axioms_for_trim(const function_application_exprt &f)
\link string_constraint_generatort::add_axioms_for_trim(const function_application_exprt &f) More... \endlink

\subsection conversions Conversions:

* `cprover_string_format` :
\copybrief add_axioms_for_format
\link add_axioms_for_format More... \endlink
* `cprover_string_from_literal` :
\copybrief add_axioms_from_literal(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
\link add_axioms_from_literal(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
\copybrief string_constraint_generatort::add_axioms_from_literal(const function_application_exprt &f)
\link string_constraint_generatort::add_axioms_from_literal(const function_application_exprt &f) More... \endlink
* `cprover_string_of_int` :
\copybrief add_axioms_for_string_of_int
\link add_axioms_for_string_of_int More... \endlink
\copybrief string_constraint_generatort::add_axioms_for_string_of_int
\link string_constraint_generatort::add_axioms_for_string_of_int More... \endlink
* `cprover_string_of_float` :
\copybrief add_axioms_for_string_of_float
\link add_axioms_for_string_of_float More... \endlink
\copybrief string_constraint_generatort::add_axioms_for_string_of_float
\link string_constraint_generatort::add_axioms_for_string_of_float More... \endlink
* `cprover_string_of_float_scientific_notation` :
\copybrief add_axioms_from_float_scientific_notation
\link add_axioms_from_float_scientific_notation More... \endlink
\copybrief string_constraint_generatort::add_axioms_from_float_scientific_notation
\link string_constraint_generatort::add_axioms_from_float_scientific_notation More... \endlink
* `cprover_string_of_char` :
\copybrief add_axioms_from_char(const function_application_exprt &f, array_poolt &array_pool)
\link add_axioms_from_char(const function_application_exprt &f, array_poolt &array_pool) More... \endlink
\copybrief string_constraint_generatort::add_axioms_from_char(const function_application_exprt &f)
\link string_constraint_generatort::add_axioms_from_char(const function_application_exprt &f) More... \endlink
* `cprover_string_parse_int` :
\copybrief add_axioms_for_parse_int
\link add_axioms_for_parse_int More... \endlink
\copybrief string_constraint_generatort::add_axioms_for_parse_int
\link string_constraint_generatort::add_axioms_for_parse_int More... \endlink

\subsection solvers-deprecated Deprecated primitives:

Expand Down
4 changes: 2 additions & 2 deletions src/solvers/strings/string_builtin_function.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -407,8 +407,8 @@ optionalt<exprt> string_of_int_builtin_functiont::eval(
string_constraintst string_of_int_builtin_functiont::constraints(
string_constraint_generatort &generator) const
{
auto pair = add_axioms_for_string_of_int_with_radix(
result, arg, radix, 0, generator.ns, array_pool);
auto pair =
generator.add_axioms_for_string_of_int_with_radix(result, arg, radix, 0);
pair.second.existential.push_back(equal_exprt(pair.first, return_code));
return pair.second;
}
Expand Down
52 changes: 15 additions & 37 deletions src/solvers/strings/string_concatenation_builtin_function.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,22 +43,19 @@ string_concatenation_builtin_functiont::string_concatenation_builtin_functiont(
/// 2. \f$\forall i<|s_1|. res[i]=s_1[i] \f$
/// 3. \f$\forall i< |res| - |s_1|.\ res[i+|s_1|] = s_2[start\_index'+i]\f$
///
/// \param fresh_symbol: generator of fresh symbols
/// \param res: an array of characters expression
/// \param s1: an array of characters expression
/// \param s2: an array of characters expression
/// \param start_index: integer expression
/// \param end_index: integer expression
/// \param array_pool: pool of arrays representing strings
/// \return integer expression `0`
std::pair<exprt, string_constraintst> add_axioms_for_concat_substr(
symbol_generatort &fresh_symbol,
std::pair<exprt, string_constraintst>
string_constraint_generatort::add_axioms_for_concat_substr(
const array_string_exprt &res,
const array_string_exprt &s1,
const array_string_exprt &s2,
const exprt &start_index,
const exprt &end_index,
array_poolt &array_pool)
const exprt &end_index)
{
string_constraintst constraints;
const typet &index_type = start_index.type();
Expand Down Expand Up @@ -153,40 +150,28 @@ exprt length_constraint_for_concat_char(
/// `s2`.
///
/// \deprecated should use concat_substr instead
/// \param fresh_symbol: generator of fresh symbols
/// \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
/// \param array_pool: pool of arrays representing strings
/// \return an integer expression
std::pair<exprt, string_constraintst> add_axioms_for_concat(
symbol_generatort &fresh_symbol,
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,
array_poolt &array_pool)
const array_string_exprt &s2)
{
exprt index_zero = from_integer(0, s2.length_type());
return add_axioms_for_concat_substr(
fresh_symbol,
res,
s1,
s2,
index_zero,
array_pool.get_or_create_length(s2),
array_pool);
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 fresh_symbol: generator of fresh symbols
/// \param f: function application with two arguments: a string and a code point
/// \param array_pool: pool of arrays representing strings
/// \return an expression
std::pair<exprt, string_constraintst> add_axioms_for_concat_code_point(
symbol_generatort &fresh_symbol,
const function_application_exprt &f,
array_poolt &array_pool)
std::pair<exprt, string_constraintst>
string_constraint_generatort::add_axioms_for_concat_code_point(
const function_application_exprt &f)
{
PRECONDITION(f.arguments().size() == 4);
const array_string_exprt res =
Expand All @@ -197,8 +182,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_concat_code_point(
const array_string_exprt code_point =
array_pool.fresh_string(index_type, char_type);
return combine_results(
add_axioms_for_code_point(code_point, f.arguments()[3], array_pool),
add_axioms_for_concat(fresh_symbol, res, s1, code_point, array_pool));
add_axioms_for_code_point(code_point, f.arguments()[3]),
add_axioms_for_concat(res, s1, code_point));
}

std::vector<mp_integer> string_concatenation_builtin_functiont::eval(
Expand Down Expand Up @@ -228,18 +213,11 @@ string_constraintst string_concatenation_builtin_functiont::constraints(
{
auto pair = [&]() -> std::pair<exprt, string_constraintst> {
if(args.size() == 0)
return add_axioms_for_concat(
generator.fresh_symbol, result, input1, input2, array_pool);
return generator.add_axioms_for_concat(result, input1, input2);
if(args.size() == 2)
{
return add_axioms_for_concat_substr(
generator.fresh_symbol,
result,
input1,
input2,
args[0],
args[1],
array_pool);
return generator.add_axioms_for_concat_substr(
result, input1, input2, args[0], args[1]);
}
UNREACHABLE;
}();
Expand Down
Loading