Renaming add_axioms_from_float to add_axioms_for_string_of_float

This function name is more explicit about what the function does

Author: romainbrenguier

src/solvers/refinement/string_constraint_generator.h

@@ -236,8 +236,9 @@ class string_constraint_generatort
   // and minus infinity the string are "Infinity" and "-Infinity respectively
   // otherwise the string contains only characters in [0123456789.] and '-' at
   // the start for negative number
-  string_exprt add_axioms_from_float(const function_application_exprt &f);
-  string_exprt add_axioms_from_float(
+  string_exprt add_axioms_for_string_of_float(
+    const function_application_exprt &f);
+  string_exprt add_axioms_for_string_of_float(
     const exprt &f, const refined_string_typet &ref_type);
 
   string_exprt add_axioms_for_fractional_part(

src/solvers/refinement/string_constraint_generator_concat.cpp

@@ -174,7 +174,7 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_double(
   string_exprt s1=get_string_expr(args(f, 2)[0]);
   PRECONDITION(refined_string_typet::is_refined_string_type(f.type()));
   refined_string_typet ref_type=to_refined_string_type(f.type());
-  string_exprt s2=add_axioms_from_float(args(f, 2)[1], ref_type, true);
+  string_exprt s2=add_axioms_for_string_of_float(args(f, 2)[1], ref_type);
   return add_axioms_for_concat(s1, s2);
 }
 
@@ -187,7 +187,7 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_float(
   string_exprt s1=get_string_expr(args(f, 2)[0]);
   PRECONDITION(refined_string_typet::is_refined_string_type(f.type()));
   refined_string_typet ref_type=to_refined_string_type(f.type());
-  string_exprt s2=add_axioms_from_float(args(f, 2)[1], ref_type, false);
+  string_exprt s2=add_axioms_for_string_of_float(args(f, 2)[1], ref_type);
   return add_axioms_for_concat(s1, s2);
 }
 

src/solvers/refinement/string_constraint_generator_float.cpp

@@ -150,11 +150,11 @@ exprt estimate_decimal_exponent(const exprt &f, const ieee_float_spect &spec)
 /// Add axioms corresponding to the String.valueOf(F) java function
 /// \param f: function application with one float argument
 /// \return a new string expression
-string_exprt string_constraint_generatort::add_axioms_from_float(
+string_exprt string_constraint_generatort::add_axioms_for_string_of_float(
   const function_application_exprt &f)
 {
-  const refined_string_typet &ref_type=to_refined_string_type(f.type());
-  return add_axioms_from_float(args(f, 1)[0], ref_type);
+  return add_axioms_for_string_of_float(
+    args(f, 1)[0], to_refined_string_type(f.type()));
 }
 
 /// Add axioms corresponding to the String.valueOf(D) java function
@@ -163,8 +163,8 @@ string_exprt string_constraint_generatort::add_axioms_from_float(
 string_exprt string_constraint_generatort::add_axioms_from_double(
   const function_application_exprt &f)
 {
-  const refined_string_typet &ref_type=to_refined_string_type(f.type());
-  return add_axioms_from_float(args(f, 1)[0], ref_type);
+  return add_axioms_for_string_of_float(
+    args(f, 1)[0], to_refined_string_type(f.type()));
 }
 
 /// Add axioms corresponding to the integer part of m, in decimal form with no
@@ -176,7 +176,7 @@ string_exprt string_constraint_generatort::add_axioms_from_double(
 /// \param f: expression representing a float
 /// \param ref_type: refined type for strings
 /// \return a new string expression
-string_exprt string_constraint_generatort::add_axioms_from_float(
+string_exprt string_constraint_generatort::add_axioms_for_string_of_float(
   const exprt &f, const refined_string_typet &ref_type)
 {
   const floatbv_typet &type=to_floatbv_type(f.type());

src/solvers/refinement/string_constraint_generator_insert.cpp

@@ -119,7 +119,7 @@ string_exprt string_constraint_generatort::add_axioms_for_insert_double(
 {
   string_exprt s1=get_string_expr(args(f, 3)[0]);
   const refined_string_typet &ref_type=to_refined_string_type(s1.type());
-  string_exprt s2=add_axioms_from_float(args(f, 3)[2], ref_type);
+  string_exprt s2=add_axioms_for_string_of_float(args(f, 3)[2], ref_type);
   return add_axioms_for_insert(s1, s2, args(f, 3)[1]);
 }
 
@@ -133,7 +133,7 @@ string_exprt string_constraint_generatort::add_axioms_for_insert_float(
 {
   string_exprt s1=get_string_expr(args(f, 3)[0]);
   const refined_string_typet &ref_type=to_refined_string_type(s1.type());
-  string_exprt s2=add_axioms_from_float(args(f, 3)[2], ref_type);
+  string_exprt s2=add_axioms_for_string_of_float(args(f, 3)[2], ref_type);
   return add_axioms_for_insert(s1, s2, args(f, 3)[1]);
 }
 

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -453,7 +453,7 @@ exprt string_constraint_generatort::add_axioms_for_function_application(
   else if(id==ID_cprover_string_of_int_hex_func)
     res=add_axioms_from_int_hex(expr);
   else if(id==ID_cprover_string_of_float_func)
-    res=add_axioms_from_float(expr);
+    res=add_axioms_for_string_of_float(expr);
   else if(id==ID_cprover_string_of_float_scientific_notation_func)
     res=add_axioms_from_float_scientific_notation(expr);
   else if(id==ID_cprover_string_of_double_func)