Merge pull request #3365 from tautschnig/vs-fresh-symbol

Remove symbol generator from add_axioms_for_* that do not use it

Author: tautschnig

src/solvers/README.md

@@ -221,7 +221,7 @@ allocates a new string before calling a primitive.
   \copybrief add_axioms_for_char_at(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
   \link  add_axioms_for_char_at More... \endlink
   * `cprover_string_length` :
-  \copybrief add_axioms_for_length(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool)
+  \copybrief add_axioms_for_length(const function_application_exprt &f, array_poolt &array_pool)
   \link add_axioms_for_length More... \endlink
 
 \subsection comparisons Comparisons:

src/solvers/refinement/string_constraint_generator.h

@@ -267,11 +267,9 @@ std::pair<exprt, string_constraintst> add_axioms_for_is_suffix(
   bool swap_arguments,
   array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_for_length(
-  symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
   array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_for_empty_string(
-  symbol_generatort &fresh_symbol,
   const function_application_exprt &f);
 
 std::pair<exprt, string_constraintst> add_axioms_for_copy(
@@ -438,7 +436,6 @@ std::pair<exprt, string_constraintst> add_axioms_for_string_of_float(
   array_poolt &array_pool,
   const namespacet &ns);
 std::pair<exprt, string_constraintst> add_axioms_for_fractional_part(
-  symbol_generatort &fresh_symbol,
   const array_string_exprt &res,
   const exprt &i,
   size_t max_size);
@@ -491,11 +488,9 @@ std::pair<exprt, string_constraintst> add_axioms_for_trim(
   array_poolt &array_pool);
 
 std::pair<exprt, string_constraintst> add_axioms_for_code_point(
-  symbol_generatort &fresh_symbol,
   const array_string_exprt &res,
   const exprt &code_point);
 std::pair<exprt, string_constraintst> add_axioms_for_char_literal(
-  symbol_generatort &fresh_symbol,
   const function_application_exprt &f);
 
 /// Add axioms corresponding the String.codePointCount java function

src/solvers/refinement/string_constraint_generator_code_points.cpp

@@ -14,12 +14,10 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 
 /// add axioms for the conversion of an integer representing a java
 /// code point to a utf-16 string
-/// \param fresh_symbol: generator of fresh symbols
 /// \param res: array of characters corresponding to the result fo the function
 /// \param code_point: an expression representing a java code point
 /// \return integer expression equal to zero
 std::pair<exprt, string_constraintst> add_axioms_for_code_point(
-  symbol_generatort &fresh_symbol,
   const array_string_exprt &res,
   const exprt &code_point)
 {

src/solvers/refinement/string_constraint_generator_concat.cpp

@@ -154,6 +154,6 @@ std::pair<exprt, string_constraintst> add_axioms_for_concat_code_point(
   const array_string_exprt code_point =
     array_pool.fresh_string(index_type, char_type);
   return combine_results(
-    add_axioms_for_code_point(fresh_symbol, code_point, f.arguments()[3]),
+    add_axioms_for_code_point(code_point, f.arguments()[3]),
     add_axioms_for_concat(fresh_symbol, res, s1, code_point));
 }

src/solvers/refinement/string_constraint_generator_constants.cpp

@@ -57,12 +57,10 @@ std::pair<exprt, string_constraintst> add_axioms_for_constant(
 }
 
 /// Add axioms to say that the returned string expression is empty
-/// \param fresh_symbol: generator of fresh symbols
 /// \param f: function application with arguments integer `length` and character
 ///           pointer `ptr`.
 /// \return integer expression equal to zero
 std::pair<exprt, string_constraintst> add_axioms_for_empty_string(
-  symbol_generatort &fresh_symbol,
   const function_application_exprt &f)
 {
   PRECONDITION(f.arguments().size() == 2);

src/solvers/refinement/string_constraint_generator_float.cpp

@@ -221,8 +221,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_string_of_float(
   const mod_exprt fractional_part(shifted, max_non_exponent_notation);
   const array_string_exprt fractional_part_str =
     array_pool.fresh_string(index_type, char_type);
-  auto result1 = add_axioms_for_fractional_part(
-    fresh_symbol, fractional_part_str, fractional_part, 6);
+  auto result1 =
+    add_axioms_for_fractional_part(fractional_part_str, fractional_part, 6);
 
   // The axiom added to convert to integer should always be satisfiable even
   // when the preconditions are not satisfied.
@@ -247,14 +247,12 @@ std::pair<exprt, string_constraintst> add_axioms_for_string_of_float(
 
 /// Add axioms for representing the fractional part of a floating point starting
 /// with a dot
-/// \param fresh_symbol: generator of fresh symbols
 /// \param res: string expression for the result
 /// \param int_expr: an integer expression
 /// \param max_size: a maximal size for the string, this includes the
 ///   potential minus sign and therefore should be greater than 2
 /// \return code 0 on success
 std::pair<exprt, string_constraintst> add_axioms_for_fractional_part(
-  symbol_generatort &fresh_symbol,
   const array_string_exprt &res,
   const exprt &int_expr,
   size_t max_size)
@@ -478,7 +476,7 @@ std::pair<exprt, string_constraintst> add_axioms_from_float_scientific_notation(
   array_string_exprt string_fractional_part =
     array_pool.fresh_string(index_type, char_type);
   auto result2 = add_axioms_for_fractional_part(
-    fresh_symbol, string_fractional_part, fractional_part_shifted, 6);
+    string_fractional_part, fractional_part_shifted, 6);
 
   // string_expr_with_fractional_part =
   //   concat(string_with_do, string_fractional_part)

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -374,9 +374,9 @@ string_constraint_generatort::add_axioms_for_function_application(
   const irep_idt &id = get_function_name(expr);
 
   if(id==ID_cprover_char_literal_func)
-    return add_axioms_for_char_literal(fresh_symbol, expr);
+    return add_axioms_for_char_literal(expr);
   else if(id==ID_cprover_string_length_func)
-    return add_axioms_for_length(fresh_symbol, expr, array_pool);
+    return add_axioms_for_length(expr, array_pool);
   else if(id==ID_cprover_string_equal_func)
     return add_axioms_for_equals(fresh_symbol, expr, array_pool);
   else if(id==ID_cprover_string_equals_ignore_case_func)
@@ -436,7 +436,7 @@ string_constraint_generatort::add_axioms_for_function_application(
   else if(id==ID_cprover_string_trim_func)
     return add_axioms_for_trim(fresh_symbol, expr, array_pool);
   else if(id==ID_cprover_string_empty_string_func)
-    return add_axioms_for_empty_string(fresh_symbol, expr);
+    return add_axioms_for_empty_string(expr);
   else if(id==ID_cprover_string_copy_func)
     return add_axioms_for_copy(fresh_symbol, expr, array_pool);
   else if(id==ID_cprover_string_of_int_hex_func)
@@ -507,12 +507,10 @@ std::pair<exprt, string_constraintst> add_axioms_for_copy(
 /// Length of a string
 ///
 /// Returns the length of the string argument of the given function application
-/// \param fresh_symbol: generator of fresh symbols
 /// \param f: function application with argument string `str`
 /// \param array_pool: pool of arrays representing strings
 /// \return expression `|str|`
 std::pair<exprt, string_constraintst> add_axioms_for_length(
-  symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
   array_poolt &array_pool)
 {
@@ -529,11 +527,9 @@ exprt is_positive(const exprt &x)
 }
 
 /// add axioms stating that the returned value is equal to the argument
-/// \param fresh_symbol: generator of fresh symbols
 /// \param f: function application with one character argument
 /// \return a new character expression
 std::pair<exprt, string_constraintst> add_axioms_for_char_literal(
-  symbol_generatort &fresh_symbol,
   const function_application_exprt &f)
 {
   const function_application_exprt::argumentst &args=f.arguments();