Merge pull request #4601 from allredj/stringsolv-remove-array-pool-arg

String solver refactor: Remove array_pool arg from non-static function [TG-7439]

Author: tautschnig

src/solvers/strings/string_constraint_generator.h

@@ -78,9 +78,8 @@ class string_constraint_generatort final
   // Add axioms corresponding to the String.hashCode java function
   // The specification is partial: the actual value is not actually computed
   // but we ensure that hash codes of equal strings are equal.
-  std::pair<exprt, string_constraintst> add_axioms_for_hash_code(
-    const function_application_exprt &f,
-    array_poolt &pool);
+  std::pair<exprt, string_constraintst>
+  add_axioms_for_hash_code(const function_application_exprt &f);
 
   // MEMBERS
   const messaget message;

src/solvers/strings/string_constraint_generator_comparison.cpp

@@ -184,16 +184,14 @@ std::pair<exprt, string_constraintst> add_axioms_for_equals_ignore_case(
 ///   * \f$ hash(str)=hash(s) \lor |str| \ne |s|
 ///       \lor (|str|=|s| \land \exists i<|s|.\ s[i]\ne str[i]) \f$
 /// \param f: function application with argument refined_string `str`
-/// \param pool: pool of arrays representing strings
 /// \return integer expression `hash(str)`
 std::pair<exprt, string_constraintst>
 string_constraint_generatort::add_axioms_for_hash_code(
-  const function_application_exprt &f,
-  array_poolt &pool)
+  const function_application_exprt &f)
 {
   PRECONDITION(f.arguments().size() == 1);
   string_constraintst hash_constraints;
-  const array_string_exprt str = get_string_expr(pool, f.arguments()[0]);
+  const array_string_exprt str = get_string_expr(array_pool, f.arguments()[0]);
   const typet &return_type = f.type();
   const typet &index_type = str.length().type();
 

src/solvers/strings/string_constraint_generator_main.cpp

@@ -241,7 +241,7 @@ string_constraint_generatort::add_axioms_for_function_application(
   else if(id == ID_cprover_string_contains_func)
     return add_axioms_for_contains(fresh_symbol, expr, array_pool);
   else if(id == ID_cprover_string_hash_code_func)
-    return add_axioms_for_hash_code(expr, array_pool);
+    return add_axioms_for_hash_code(expr);
   else if(id == ID_cprover_string_index_of_func)
     return add_axioms_for_index_of(fresh_symbol, expr, array_pool);
   else if(id == ID_cprover_string_last_index_of_func)