Remove handling of bool and char to string from the string solver

Author: danpoe

src/solvers/README.md

@@ -499,9 +499,6 @@ This is described in more detail \link string_builtin_functiont here. \endlink
   * `cprover_string_of_float_scientific_notation` :
     \copybrief add_axioms_from_float_scientific_notation
     \link 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
   * `cprover_string_parse_int` :
     \copybrief add_axioms_for_parse_int
     \link 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`.

src/solvers/strings/string_constraint_generator_main.cpp

@@ -281,10 +281,6 @@ string_constraint_generatort::add_axioms_for_function_application(
     return add_axioms_from_double(fresh_symbol, expr, array_pool, ns);
   else if(id == ID_cprover_string_of_long_func)
     return add_axioms_from_long(expr, array_pool, ns);
-  else if(id == ID_cprover_string_of_bool_func)
-    return add_axioms_from_bool(expr, array_pool);
-  else if(id == ID_cprover_string_of_char_func)
-    return add_axioms_from_char(expr, array_pool);
   else if(id == ID_cprover_string_set_length_func)
     return add_axioms_for_set_length(fresh_symbol, expr, array_pool);
   else if(id == ID_cprover_string_delete_func)

src/solvers/strings/string_constraint_generator_valueof.cpp

@@ -59,22 +59,6 @@ std::pair<exprt, string_constraintst> add_axioms_from_long(
       res, f.arguments()[2], 0, ns, array_pool);
 }
 
-/// 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
-/// \param array_pool: pool of arrays representing strings
-/// \return a new string expression
-DEPRECATED(SINCE(2017, 10, 5, "Java specific, should be implemented in Java"))
-std::pair<exprt, string_constraintst> add_axioms_from_bool(
-  const function_application_exprt &f,
-  array_poolt &array_pool)
-{
-  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], array_pool);
-}
-
 /// 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
@@ -296,46 +280,6 @@ std::pair<exprt, string_constraintst> add_axioms_from_int_hex(
   return add_axioms_from_int_hex(res, f.arguments()[2], array_pool);
 }
 
-/// Conversion from char to string
-///
-// NOLINTNEXTLINE
-/// \copybrief add_axioms_from_char(const array_string_exprt &res, const exprt &c, array_poolt &)
-// NOLINTNEXTLINE
-/// \link add_axioms_from_char(const array_string_exprt &res, const exprt &c, array_poolt &)
-///   (More...) \endlink
-/// \param f: function application with arguments integer `|res|`, character
-///   pointer `&res[0]` and character `c`
-/// \param array_pool: pool of arrays representing strings
-/// \return code 0 on success
-std::pair<exprt, string_constraintst> add_axioms_from_char(
-  const function_application_exprt &f,
-  array_poolt &array_pool)
-{
-  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], array_pool);
-}
-
-/// 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
-/// \param array_pool: pool of arrays representing strings
-/// \return code 0 on success
-std::pair<exprt, string_constraintst> add_axioms_from_char(
-  const array_string_exprt &res,
-  const exprt &c,
-  array_poolt &array_pool)
-{
-  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

src/util/irep_ids.def

@@ -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)