Rename function to add_axioms_for_string_of_int

This is more uniform with the other builtin string functions

Author: romainbrenguier

src/solvers/README.md

@@ -281,7 +281,7 @@ allocates a new string before calling a primitive.
     \link string_constraint_generatort::add_axioms_from_literal(const function_application_exprt &f) More... \endlink
   * `cprover_string_of_int` :
     \copybrief string_constraint_generatort::add_axioms_from_int(const function_application_exprt &f)
-    \link string_constraint_generatort::add_axioms_from_int(const function_application_exprt &f) More... \endlink
+    \link string_constraint_generatort::add_axioms_for_string_of_int(const function_application_exprt &f) More... \endlink
   * `cprover_string_of_float` :
     \copybrief string_constraint_generatort::add_axioms_for_string_of_float(const function_application_exprt &f)
     \link string_constraint_generatort::add_axioms_for_string_of_float(const function_application_exprt &f) More... \endlink

src/solvers/refinement/string_constraint_generator.h

@@ -165,6 +165,11 @@ class string_constraint_generatort final
     const array_string_exprt &s1,
     const array_string_exprt &s2,
     const exprt &offset);
+  exprt add_axioms_for_string_of_int_with_radix(
+    const array_string_exprt &res,
+    const exprt &input_int,
+    const exprt &radix,
+    size_t max_size = 0);
 
 private:
   symbol_exprt fresh_boolean(const irep_idt &prefix);
@@ -258,15 +263,10 @@ class string_constraint_generatort final
     const exprt &guard);
   exprt add_axioms_from_literal(const function_application_exprt &f);
   exprt add_axioms_from_int(const function_application_exprt &f);
-  exprt add_axioms_from_int(
+  exprt add_axioms_for_string_of_int(
     const array_string_exprt &res,
     const exprt &input_int,
     size_t max_size = 0);
-  exprt add_axioms_from_int_with_radix(
-    const array_string_exprt &res,
-    const exprt &input_int,
-    const exprt &radix,
-    size_t max_size = 0);
   exprt add_axioms_from_int_hex(const array_string_exprt &res, const exprt &i);
   exprt add_axioms_from_int_hex(const function_application_exprt &f);
   exprt add_axioms_from_long(const function_application_exprt &f);

src/solvers/refinement/string_constraint_generator_float.cpp

@@ -214,7 +214,7 @@ exprt string_constraint_generatort::add_axioms_for_string_of_float(
   const array_string_exprt integer_part_str =
     fresh_string(index_type, char_type);
   const exprt return_code2 =
-    add_axioms_from_int(integer_part_str, integer_part, 8);
+    add_axioms_for_string_of_int(integer_part_str, integer_part, 8);
 
   return add_axioms_for_concat(res, integer_part_str, fractional_part_str);
 }
@@ -423,8 +423,8 @@ exprt string_constraint_generatort::add_axioms_from_float_scientific_notation(
 
   array_string_exprt string_expr_integer_part =
     fresh_string(index_type, char_type);
-  exprt return_code1 =
-    add_axioms_from_int(string_expr_integer_part, dec_significand_int, 3);
+  exprt return_code1 = add_axioms_for_string_of_int(
+    string_expr_integer_part, dec_significand_int, 3);
   minus_exprt fractional_part(
     dec_significand, floatbv_of_int_expr(dec_significand_int, float_spec));
 
@@ -467,7 +467,7 @@ exprt string_constraint_generatort::add_axioms_from_float_scientific_notation(
   const array_string_exprt exponent_string =
     fresh_string(index_type, char_type);
   const exprt return_code6 =
-    add_axioms_from_int(exponent_string, decimal_exponent, 3);
+    add_axioms_for_string_of_int(exponent_string, decimal_exponent, 3);
 
   // string_expr = concat(string_expr_with_E, exponent_string)
   return add_axioms_for_concat(res, string_expr_with_E, exponent_string);

src/solvers/refinement/string_constraint_generator_format.cpp

@@ -269,7 +269,7 @@ string_constraint_generatort::add_axioms_for_format_specifier(
   {
   case format_specifiert::DECIMAL_INTEGER:
     return_code =
-      add_axioms_from_int(res, get_component_in_struct(arg, ID_int));
+      add_axioms_for_string_of_int(res, get_component_in_struct(arg, ID_int));
     return res;
   case format_specifiert::HEXADECIMAL_INTEGER:
     return_code =
@@ -293,8 +293,8 @@ string_constraint_generatort::add_axioms_for_format_specifier(
   case format_specifiert::STRING:
     return get_string_expr(get_component_in_struct(arg, "string_expr"));
   case format_specifiert::HASHCODE:
-    return_code =
-      add_axioms_from_int(res, get_component_in_struct(arg, "hashcode"));
+    return_code = add_axioms_for_string_of_int(
+      res, get_component_in_struct(arg, "hashcode"));
     return res;
   case format_specifiert::LINE_SEPARATOR:
     // TODO: the constant should depend on the system: System.lineSeparator()

src/solvers/refinement/string_constraint_generator_insert.cpp

@@ -144,7 +144,7 @@ exprt string_constraint_generatort::add_axioms_for_insert_int(
   const typet &index_type = s1.length().type();
   const typet &char_type = s1.content().type().subtype();
   array_string_exprt s2 = fresh_string(index_type, char_type);
-  exprt return_code = add_axioms_from_int(s2, f.arguments()[4]);
+  exprt return_code = add_axioms_for_string_of_int(s2, f.arguments()[4]);
   return add_axioms_for_insert(res, s1, s2, offset);
 }
 

src/solvers/refinement/string_constraint_generator_valueof.cpp

@@ -31,28 +31,28 @@ exprt string_constraint_generatort::add_axioms_from_int(
   const array_string_exprt res =
     char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
   if(f.arguments().size() == 4)
-    return add_axioms_from_int_with_radix(
+    return add_axioms_for_string_of_int_with_radix(
       res, f.arguments()[2], f.arguments()[3]);
   else // f.arguments.size()==3
-    return add_axioms_from_int(res, f.arguments()[2]);
+    return add_axioms_for_string_of_int(res, f.arguments()[2]);
 }
 
 /// Add axioms corresponding to the String.valueOf(J) java function.
 /// \deprecated should use add_axioms_from_int instead
 /// \param f: function application with one long argument
 /// \return a new string expression
-DEPRECATED("should use add_axioms_from_int instead")
+DEPRECATED("should use add_axioms_for_string_of_int instead")
 exprt string_constraint_generatort::add_axioms_from_long(
   const function_application_exprt &f)
 {
   PRECONDITION(f.arguments().size() == 3 || f.arguments().size() == 4);
   const array_string_exprt res =
     char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
   if(f.arguments().size() == 4)
-    return add_axioms_from_int_with_radix(
+    return add_axioms_for_string_of_int_with_radix(
       res, f.arguments()[2], f.arguments()[3]);
   else
-    return add_axioms_from_int(res, f.arguments()[2]);
+    return add_axioms_for_string_of_int(res, f.arguments()[2]);
 }
 
 /// Add axioms corresponding to the String.valueOf(Z) java function.
@@ -124,13 +124,14 @@ exprt string_constraint_generatort::add_axioms_from_bool(
 /// \param max_size: a maximal size for the string representation (default 0,
 ///   which is interpreted to mean "as large as is needed for this type")
 /// \return code 0 on success
-exprt string_constraint_generatort::add_axioms_from_int(
+exprt string_constraint_generatort::add_axioms_for_string_of_int(
   const array_string_exprt &res,
   const exprt &input_int,
   size_t max_size)
 {
   const constant_exprt radix=from_integer(10, input_int.type());
-  return add_axioms_from_int_with_radix(res, input_int, radix, max_size);
+  return add_axioms_for_string_of_int_with_radix(
+    res, input_int, radix, max_size);
 }
 
 /// Add axioms enforcing that the string corresponds to the result
@@ -142,7 +143,7 @@ exprt string_constraint_generatort::add_axioms_from_int(
 /// \param max_size: a maximal size for the string representation (default 0,
 ///   which is interpreted to mean "as large as is needed for this type")
 /// \return code 0 on success
-exprt string_constraint_generatort::add_axioms_from_int_with_radix(
+exprt string_constraint_generatort::add_axioms_for_string_of_int_with_radix(
   const array_string_exprt &res,
   const exprt &input_int,
   const exprt &radix,
@@ -204,7 +205,8 @@ exprt string_constraint_generatort::int_of_hex_char(const exprt &chr)
 /// \param res: string expression for the result
 /// \param i: an integer argument
 /// \return code 0 on success
-DEPRECATED("use add_axioms_from_int which takes a radix argument instead")
+DEPRECATED(
+  "use add_axioms_for_string_of_int which takes a radix argument instead")
 exprt string_constraint_generatort::add_axioms_from_int_hex(
   const array_string_exprt &res,
   const exprt &i)