Remove handling of bool and char to string from the string solver
This commit is contained in:
parent
b32de0a886
commit
70fc569a95
|
@ -499,9 +499,6 @@ This is described in more detail \link string_builtin_functiont here. \endlink
|
|||
* `cprover_string_of_float_scientific_notation` :
|
||||
\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 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 string_constraint_generatort::add_axioms_for_parse_int
|
||||
\link string_constraint_generatort::add_axioms_for_parse_int More... \endlink
|
||||
|
@ -530,8 +527,6 @@ This is described in more detail \link string_builtin_functiont here. \endlink
|
|||
* `cprover_string_delete_char_at` : A call to
|
||||
`cprover_string_delete_char_at(s, i)` would be the same thing as
|
||||
`cprover_string_delete(s, i, i+1)`.
|
||||
* `cprover_string_of_bool` :
|
||||
Language dependent, should be implemented in the models.
|
||||
* `cprover_string_copy` : Same as `cprover_string_substring(s, 0)`.
|
||||
* `cprover_string_of_int_hex` : Same as `cprover_string_of_int(s, 16)`.
|
||||
* `cprover_string_of_double` : Same as `cprover_string_of_float`.
|
||||
|
|
|
@ -273,10 +273,6 @@ string_constraint_generatort::add_axioms_for_function_application(
|
|||
return add_axioms_from_double(expr);
|
||||
else if(id == ID_cprover_string_of_long_func)
|
||||
return add_axioms_from_long(expr);
|
||||
else if(id == ID_cprover_string_of_bool_func)
|
||||
return add_axioms_from_bool(expr);
|
||||
else if(id == ID_cprover_string_of_char_func)
|
||||
return add_axioms_from_char(expr);
|
||||
else if(id == ID_cprover_string_set_length_func)
|
||||
return add_axioms_for_set_length(expr);
|
||||
else if(id == ID_cprover_string_delete_func)
|
||||
|
|
|
@ -55,21 +55,6 @@ string_constraint_generatort::add_axioms_from_long(
|
|||
return add_axioms_for_string_of_int(res, f.arguments()[2], 0);
|
||||
}
|
||||
|
||||
/// Add axioms corresponding to the String.valueOf(Z) java function.
|
||||
/// \deprecated This is Java specific and should be implemented in Java instead
|
||||
/// \param f: function application with a Boolean argument
|
||||
/// \return a new string expression
|
||||
DEPRECATED(SINCE(2017, 10, 5, "Java specific, should be implemented in Java"))
|
||||
std::pair<exprt, string_constraintst>
|
||||
string_constraint_generatort::add_axioms_from_bool(
|
||||
const function_application_exprt &f)
|
||||
{
|
||||
PRECONDITION(f.arguments().size() == 3);
|
||||
const array_string_exprt res =
|
||||
array_pool.find(f.arguments()[1], f.arguments()[0]);
|
||||
return add_axioms_from_bool(res, f.arguments()[2]);
|
||||
}
|
||||
|
||||
/// Add axioms stating that the returned string equals "true" when the Boolean
|
||||
/// expression is true and "false" when it is false.
|
||||
/// \deprecated This is Java specific and should be implemented in Java instead
|
||||
|
@ -281,44 +266,6 @@ string_constraint_generatort::add_axioms_from_int_hex(
|
|||
return add_axioms_from_int_hex(res, f.arguments()[2]);
|
||||
}
|
||||
|
||||
/// Conversion from char to string
|
||||
///
|
||||
// NOLINTNEXTLINE
|
||||
/// \copybrief add_axioms_from_char(const array_string_exprt &res, const exprt &c)
|
||||
// NOLINTNEXTLINE
|
||||
/// \link add_axioms_from_char(const array_string_exprt &res, const exprt &c)
|
||||
/// (More...) \endlink
|
||||
/// \param f: function application with arguments integer `|res|`, character
|
||||
/// pointer `&res[0]` and character `c`
|
||||
/// \return code 0 on success
|
||||
std::pair<exprt, string_constraintst>
|
||||
string_constraint_generatort::add_axioms_from_char(
|
||||
const function_application_exprt &f)
|
||||
{
|
||||
PRECONDITION(f.arguments().size() == 3);
|
||||
const array_string_exprt res =
|
||||
array_pool.find(f.arguments()[1], f.arguments()[0]);
|
||||
return add_axioms_from_char(res, f.arguments()[2]);
|
||||
}
|
||||
|
||||
/// Add axiom stating that string `res` has length 1 and the character
|
||||
/// it contains equals `c`.
|
||||
///
|
||||
/// This axiom is: \f$ |{\tt res}| = 1 \land {\tt res}[0] = {\tt c} \f$.
|
||||
/// \param res: array of characters expression
|
||||
/// \param c: character expression
|
||||
/// \return code 0 on success
|
||||
std::pair<exprt, string_constraintst>
|
||||
string_constraint_generatort::add_axioms_from_char(
|
||||
const array_string_exprt &res,
|
||||
const exprt &c)
|
||||
{
|
||||
string_constraintst constraints;
|
||||
constraints.existential = {and_exprt(
|
||||
equal_exprt(res[0], c), equal_to(array_pool.get_or_create_length(res), 1))};
|
||||
return {from_integer(0, get_return_code_type()), std::move(constraints)};
|
||||
}
|
||||
|
||||
/// Add axioms making the return value true if the given string is a correct
|
||||
/// number in the given radix
|
||||
/// \param str: string expression
|
||||
|
|
|
@ -619,11 +619,9 @@ IREP_ID_ONE(cprover_string_length_func)
|
|||
IREP_ID_ONE(cprover_string_of_int_func)
|
||||
IREP_ID_ONE(cprover_string_of_int_hex_func)
|
||||
IREP_ID_ONE(cprover_string_of_long_func)
|
||||
IREP_ID_ONE(cprover_string_of_bool_func)
|
||||
IREP_ID_ONE(cprover_string_of_float_func)
|
||||
IREP_ID_ONE(cprover_string_of_float_scientific_notation_func)
|
||||
IREP_ID_ONE(cprover_string_of_double_func)
|
||||
IREP_ID_ONE(cprover_string_of_char_func)
|
||||
IREP_ID_ONE(cprover_string_parse_int_func)
|
||||
IREP_ID_ONE(cprover_string_replace_func)
|
||||
IREP_ID_ONE(cprover_string_set_length_func)
|
||||
|
|
Loading…
Reference in New Issue