Merge pull request #4607 from allredj/cleanup/arraypool

Cleanup string solver: use same name for arraypool arg everywhere [TG-7439]

Author: tautschnig

src/solvers/strings/array_pool.cpp

@@ -129,9 +129,9 @@ array_string_exprt of_argument(array_poolt &array_pool, const exprt &arg)
   return array_pool.find(string_argument.op1(), string_argument.op0());
 }
 
-array_string_exprt get_string_expr(array_poolt &pool, const exprt &expr)
+array_string_exprt get_string_expr(array_poolt &array_pool, const exprt &expr)
 {
   PRECONDITION(is_refined_string_type(expr.type()));
   const refined_string_exprt &str = to_string_expr(expr);
-  return pool.find(str.content(), str.length());
+  return array_pool.find(str.content(), str.length());
 }

src/solvers/strings/array_pool.h

@@ -98,9 +98,9 @@ class array_poolt final
 array_string_exprt of_argument(array_poolt &array_pool, const exprt &arg);
 
 /// Fetch the string_exprt corresponding to the given refined_string_exprt
-/// \param pool: pool of arrays representing strings
+/// \param array_pool: pool of arrays representing strings
 /// \param expr: an expression of refined string type
 /// \return a string expression
-array_string_exprt get_string_expr(array_poolt &pool, const exprt &expr);
+array_string_exprt get_string_expr(array_poolt &array_pool, const exprt &expr);
 
 #endif // CPROVER_SOLVERS_STRINGS_ARRAY_POOL_H

src/solvers/strings/string_constraint_generator.h

@@ -141,23 +141,23 @@ std::pair<exprt, string_constraintst> add_axioms_for_char_at(
 std::pair<exprt, string_constraintst> add_axioms_for_code_point_at(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
-  array_poolt &pool);
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_for_code_point_before(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
-  array_poolt &pool);
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_for_contains(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
   array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_for_equals(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
-  array_poolt &pool);
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_for_equals_ignore_case(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
-  array_poolt &pool);
+  array_poolt &array_pool);
 
 std::pair<exprt, string_constraintst> add_axioms_for_is_empty(
   symbol_generatort &fresh_symbol,
@@ -231,7 +231,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_format(
 std::pair<exprt, string_constraintst> add_axioms_for_insert(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
-  array_poolt &pool);
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_for_insert_int(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
@@ -402,7 +402,7 @@ DEPRECATED(SINCE(2017, 10, 5, "Java specific, should be implemented in Java"))
 std::pair<exprt, string_constraintst> add_axioms_for_code_point_count(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
-  array_poolt &pool);
+  array_poolt &array_pool);
 
 /// Add axioms corresponding the String.offsetByCodePointCount java function
 /// \todo This function is underspecified, it should return the index within

src/solvers/strings/string_constraint_generator_comparison.cpp

@@ -27,19 +27,19 @@ Author: Romain Brenguier, [email protected]
 /// \param fresh_symbol: generator of fresh symbols
 /// \param f: function application with arguments refined_string `s1` and
 ///   refined_string `s2`
-/// \param pool: pool of arrays representing strings
+/// \param array_pool: pool of arrays representing strings
 /// \return Boolean expression `eq`
 std::pair<exprt, string_constraintst> add_axioms_for_equals(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
-  array_poolt &pool)
+  array_poolt &array_pool)
 {
   PRECONDITION(f.type() == bool_typet() || f.type().id() == ID_c_bool);
   PRECONDITION(f.arguments().size() == 2);
 
   string_constraintst constraints;
-  array_string_exprt s1 = get_string_expr(pool, f.arguments()[0]);
-  array_string_exprt s2 = get_string_expr(pool, f.arguments()[1]);
+  array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[0]);
+  array_string_exprt s2 = get_string_expr(array_pool, f.arguments()[1]);
   symbol_exprt eq = fresh_symbol("equal");
   typecast_exprt tc_eq(eq, f.type());
 
@@ -128,19 +128,19 @@ static exprt character_equals_ignore_case(
 /// \param fresh_symbol: generator of fresh symbols
 /// \param f: function application with arguments refined_string `s1` and
 ///   refined_string `s2`
-/// \param pool: pool of arrays representing strings
+/// \param array_pool: pool of arrays representing strings
 /// \return Boolean expression `eq`
 std::pair<exprt, string_constraintst> add_axioms_for_equals_ignore_case(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
-  array_poolt &pool)
+  array_poolt &array_pool)
 {
   PRECONDITION(f.type() == bool_typet() || f.type().id() == ID_c_bool);
   PRECONDITION(f.arguments().size() == 2);
   string_constraintst constraints;
   const symbol_exprt eq = fresh_symbol("equal_ignore_case");
-  const array_string_exprt s1 = get_string_expr(pool, f.arguments()[0]);
-  const array_string_exprt s2 = get_string_expr(pool, f.arguments()[1]);
+  const array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[0]);
+  const array_string_exprt s2 = get_string_expr(array_pool, f.arguments()[1]);
   const typet char_type = s1.content().type().subtype();
   const exprt char_a = from_integer('a', char_type);
   const exprt char_A = from_integer('A', char_type);
@@ -233,19 +233,19 @@ string_constraint_generatort::add_axioms_for_hash_code(
 /// \param fresh_symbol: generator of fresh symbols
 /// \param f: function application with arguments refined_string `s1` and
 ///   refined_string `s2`
-/// \param pool: pool of arrays representing strings
+/// \param array_pool: pool of arrays representing strings
 /// \return integer expression `res`
 std::pair<exprt, string_constraintst> add_axioms_for_compare_to(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
-  array_poolt &pool)
+  array_poolt &array_pool)
 {
   PRECONDITION(f.arguments().size() == 2);
   const typet &return_type = f.type();
   PRECONDITION(return_type.id() == ID_signedbv);
   string_constraintst constraints;
-  const array_string_exprt &s1 = get_string_expr(pool, f.arguments()[0]);
-  const array_string_exprt &s2 = get_string_expr(pool, f.arguments()[1]);
+  const array_string_exprt &s1 = get_string_expr(array_pool, f.arguments()[0]);
+  const array_string_exprt &s2 = get_string_expr(array_pool, f.arguments()[1]);
   const symbol_exprt res = fresh_symbol("compare_to", return_type);
   const typet &index_type = s1.length().type();
 

src/solvers/strings/string_constraint_generator_insert.cpp

@@ -100,18 +100,18 @@ exprt length_constraint_for_insert(
 /// \param f: function application with arguments integer `|res|`, character
 ///   pointer `&res[0]`, refined_string `s1`, refined_string`s2`, integer
 ///   `offset`, optional integer `start` and optional integer `end`
-/// \param pool: pool of arrays representing strings
+/// \param array_pool: pool of arrays representing strings
 /// \return an integer expression which is different from zero if there is an
 ///   exception to signal
 std::pair<exprt, string_constraintst> add_axioms_for_insert(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
-  array_poolt &pool)
+  array_poolt &array_pool)
 {
   PRECONDITION(f.arguments().size() == 5 || f.arguments().size() == 7);
-  array_string_exprt s1 = get_string_expr(pool, f.arguments()[2]);
-  array_string_exprt s2 = get_string_expr(pool, f.arguments()[4]);
-  array_string_exprt res = pool.find(f.arguments()[1], f.arguments()[0]);
+  array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[2]);
+  array_string_exprt s2 = get_string_expr(array_pool, f.arguments()[4]);
+  array_string_exprt res = array_pool.find(f.arguments()[1], f.arguments()[0]);
   const exprt &offset = f.arguments()[3];
   if(f.arguments().size() == 7)
   {
@@ -120,7 +120,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert(
     const typet &char_type = s1.content().type().subtype();
     const typet &index_type = s1.length().type();
     const array_string_exprt substring =
-      pool.fresh_string(index_type, char_type);
+      array_pool.fresh_string(index_type, char_type);
     return combine_results(
       add_axioms_for_substring(fresh_symbol, substring, s2, start, end),
       add_axioms_for_insert(fresh_symbol, res, s1, substring, offset));