Remove solver handling of cprover_string_insert_*

These can no longer be produced by the java preprocessing, we can thus
drop the functions that where handling it.

Author: romainbrenguier

src/solvers/README.md

@@ -514,10 +514,7 @@ This is described in more detail \link string_builtin_functiont here. \endlink
   * `cprover_string_offset_by_code_point`, `cprover_string_concat_char`,
     `cprover_string_concat_int`, `cprover_string_concat_long`,
     `cprover_string_concat_bool`, `cprover_string_concat_double`,
-    `cprover_string_concat_float`, `cprover_string_insert_int`,
-    `cprover_string_insert_long`, `cprover_string_insert_bool`,
-    `cprover_string_insert_char`, `cprover_string_insert_double`,
-     `cprover_string_insert_float` :
+    `cprover_string_concat_float` :
     Should be done in two steps: conversion from primitive type and call
     to the string primitive.
   * `cprover_string_array_of_char_pointer`, `cprover_string_to_char_array` :

src/solvers/strings/string_constraint_generator.h

@@ -211,29 +211,6 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
   array_poolt &array_pool);
-std::pair<exprt, string_constraintst> add_axioms_for_insert_int(
-  symbol_generatort &fresh_symbol,
-  const function_application_exprt &f,
-  array_poolt &array_pool,
-  const namespacet &ns);
-std::pair<exprt, string_constraintst> add_axioms_for_insert_bool(
-  symbol_generatort &fresh_symbol,
-  const function_application_exprt &f,
-  array_poolt &array_pool);
-std::pair<exprt, string_constraintst> add_axioms_for_insert_char(
-  symbol_generatort &fresh_symbol,
-  const function_application_exprt &f,
-  array_poolt &array_pool);
-std::pair<exprt, string_constraintst> add_axioms_for_insert_float(
-  symbol_generatort &fresh_symbol,
-  const function_application_exprt &f,
-  array_poolt &array_pool,
-  const namespacet &ns);
-std::pair<exprt, string_constraintst> add_axioms_for_insert_double(
-  symbol_generatort &fresh_symbol,
-  const function_application_exprt &f,
-  array_poolt &array_pool,
-  const namespacet &ns);
 
 std::pair<exprt, string_constraintst> add_axioms_for_cprover_string(
   symbol_generatort &fresh_symbol,

src/solvers/strings/string_constraint_generator_insert.cpp

@@ -142,129 +142,3 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert(
     return add_axioms_for_insert(fresh_symbol, res, s1, s2, offset, array_pool);
   }
 }
-
-/// add axioms corresponding to the StringBuilder.insert(I) java function
-/// \deprecated should convert the value to string and call insert
-/// \param fresh_symbol: generator of fresh symbols
-/// \param f: function application with three arguments: a string, an
-///   integer offset, and an integer
-/// \param array_pool: pool of arrays representing strings
-/// \param ns: namespace
-/// \return an expression
-DEPRECATED(SINCE(2017, 10, 5, "convert the value to string and call insert"))
-std::pair<exprt, string_constraintst> add_axioms_for_insert_int(
-  symbol_generatort &fresh_symbol,
-  const function_application_exprt &f,
-  array_poolt &array_pool,
-  const namespacet &ns)
-{
-  PRECONDITION(f.arguments().size() == 5);
-  const array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[2]);
-  const array_string_exprt res =
-    array_pool.find(f.arguments()[1], f.arguments()[0]);
-  const exprt &offset = f.arguments()[3];
-  const typet &index_type = s1.length_type();
-  const typet &char_type = s1.content().type().subtype();
-  const array_string_exprt s2 = array_pool.fresh_string(index_type, char_type);
-  return combine_results(
-    add_axioms_for_string_of_int(s2, f.arguments()[4], 0, ns, array_pool),
-    add_axioms_for_insert(fresh_symbol, res, s1, s2, offset, array_pool));
-}
-
-/// add axioms corresponding to the StringBuilder.insert(Z) java function
-/// \deprecated should convert the value to string and call insert
-/// \param fresh_symbol: generator of fresh symbols
-/// \param f: function application with three arguments: a string, an
-///   integer offset, and a Boolean
-/// \param array_pool: pool of arrays representing strings
-/// \return a new string expression
-DEPRECATED(SINCE(2017, 10, 5, "convert the value to string and call insert"))
-std::pair<exprt, string_constraintst> add_axioms_for_insert_bool(
-  symbol_generatort &fresh_symbol,
-  const function_application_exprt &f,
-  array_poolt &array_pool)
-{
-  PRECONDITION(f.arguments().size() == 5);
-  const array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[0]);
-  const array_string_exprt res =
-    array_pool.find(f.arguments()[1], f.arguments()[0]);
-  const exprt &offset = f.arguments()[3];
-  const typet &index_type = s1.length_type();
-  const typet &char_type = s1.content().type().subtype();
-  const array_string_exprt s2 = array_pool.fresh_string(index_type, char_type);
-  return combine_results(
-    add_axioms_from_bool(s2, f.arguments()[4], array_pool),
-    add_axioms_for_insert(fresh_symbol, res, s1, s2, offset, array_pool));
-}
-
-/// Add axioms corresponding to the StringBuilder.insert(C) java function
-/// \todo This should be merged with add_axioms_for_insert.
-/// \param fresh_symbol: generator of fresh symbols
-/// \param f: function application with three arguments: a string, an
-///   integer offset, and a character
-/// \param array_pool: pool of arrays representing strings
-/// \return an expression
-std::pair<exprt, string_constraintst> add_axioms_for_insert_char(
-  symbol_generatort &fresh_symbol,
-  const function_application_exprt &f,
-  array_poolt &array_pool)
-{
-  PRECONDITION(f.arguments().size() == 5);
-  const array_string_exprt res =
-    array_pool.find(f.arguments()[1], f.arguments()[0]);
-  const array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[2]);
-  const exprt &offset = f.arguments()[3];
-  const typet &index_type = s1.length_type();
-  const typet &char_type = s1.content().type().subtype();
-  const array_string_exprt s2 = array_pool.fresh_string(index_type, char_type);
-  return combine_results(
-    add_axioms_from_char(s2, f.arguments()[4], array_pool),
-    add_axioms_for_insert(fresh_symbol, res, s1, s2, offset, array_pool));
-}
-
-/// add axioms corresponding to the StringBuilder.insert(D) java function
-/// \deprecated should convert the value to string and call insert
-/// \param fresh_symbol: generator of fresh symbols
-/// \param f: function application with three arguments: a string, an
-///   integer offset, and a double
-/// \param array_pool: pool of arrays representing strings
-/// \param ns: namespace
-/// \return a string expression
-DEPRECATED(SINCE(2017, 10, 5, "convert the value to string and call insert"))
-std::pair<exprt, string_constraintst> add_axioms_for_insert_double(
-  symbol_generatort &fresh_symbol,
-  const function_application_exprt &f,
-  array_poolt &array_pool,
-  const namespacet &ns)
-{
-  PRECONDITION(f.arguments().size() == 5);
-  const array_string_exprt res =
-    array_pool.find(f.arguments()[1], f.arguments()[0]);
-  const array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[2]);
-  const exprt &offset = f.arguments()[3];
-  const typet &index_type = s1.length_type();
-  const typet &char_type = s1.content().type().subtype();
-  const array_string_exprt s2 = array_pool.fresh_string(index_type, char_type);
-  return combine_results(
-    add_axioms_for_string_of_float(
-      fresh_symbol, s2, f.arguments()[4], array_pool, ns),
-    add_axioms_for_insert(fresh_symbol, res, s1, s2, offset, array_pool));
-}
-
-/// Add axioms corresponding to the StringBuilder.insert(F) java function
-/// \deprecated should convert the value to string and call insert
-/// \param fresh_symbol: generator of fresh symbols
-/// \param f: function application with three arguments: a string, an
-///   integer offset, and a float
-/// \param array_pool: pool of arrays representing strings
-/// \param ns: namespace
-/// \return a new string expression
-DEPRECATED(SINCE(2017, 10, 5, "convert the value to string and call insert"))
-std::pair<exprt, string_constraintst> add_axioms_for_insert_float(
-  symbol_generatort &fresh_symbol,
-  const function_application_exprt &f,
-  array_poolt &array_pool,
-  const namespacet &ns)
-{
-  return add_axioms_for_insert_double(fresh_symbol, f, array_pool, ns);
-}

src/solvers/strings/string_constraint_generator_main.cpp

@@ -264,18 +264,6 @@ string_constraint_generatort::add_axioms_for_function_application(
     return add_axioms_for_concat_code_point(fresh_symbol, expr, array_pool);
   else if(id == ID_cprover_string_insert_func)
     return add_axioms_for_insert(fresh_symbol, expr, array_pool);
-  else if(id == ID_cprover_string_insert_int_func)
-    return add_axioms_for_insert_int(fresh_symbol, expr, array_pool, ns);
-  else if(id == ID_cprover_string_insert_long_func)
-    return add_axioms_for_insert_int(fresh_symbol, expr, array_pool, ns);
-  else if(id == ID_cprover_string_insert_bool_func)
-    return add_axioms_for_insert_bool(fresh_symbol, expr, array_pool);
-  else if(id == ID_cprover_string_insert_char_func)
-    return add_axioms_for_insert_char(fresh_symbol, expr, array_pool);
-  else if(id == ID_cprover_string_insert_double_func)
-    return add_axioms_for_insert_double(fresh_symbol, expr, array_pool, ns);
-  else if(id == ID_cprover_string_insert_float_func)
-    return add_axioms_for_insert_float(fresh_symbol, expr, array_pool, ns);
   else if(id == ID_cprover_string_substring_func)
     return add_axioms_for_substring(fresh_symbol, expr, array_pool);
   else if(id == ID_cprover_string_trim_func)

src/util/irep_ids.def

@@ -611,12 +611,6 @@ IREP_ID_ONE(cprover_string_endswith_func)
 IREP_ID_ONE(cprover_string_format_func)
 IREP_ID_ONE(cprover_string_index_of_func)
 IREP_ID_ONE(cprover_string_insert_func)
-IREP_ID_ONE(cprover_string_insert_int_func)
-IREP_ID_ONE(cprover_string_insert_long_func)
-IREP_ID_ONE(cprover_string_insert_bool_func)
-IREP_ID_ONE(cprover_string_insert_char_func)
-IREP_ID_ONE(cprover_string_insert_float_func)
-IREP_ID_ONE(cprover_string_insert_double_func)
 IREP_ID_ONE(cprover_string_is_prefix_func)
 IREP_ID_ONE(cprover_string_is_suffix_func)
 IREP_ID_ONE(cprover_string_is_empty_func)