Declaring concretize_arrays_in_expression in header file

This allows in particular to unit test it

Also update its documentation

Also renamed from concretize_array_expression: this reflects more
precisely what this function is doing.

Author: romainbrenguier

src/solvers/refinement/string_refinement.cpp

@@ -1098,14 +1098,14 @@ static exprt negation_of_constraint(const string_constraintt &axiom)
 
 /// Result of the solver `supert` should not be interpreted literally for char
 /// arrays as not all indices are present in the index set.
-/// We populate the values for which the solver has no constraint by padding
-/// the array to the left.
+/// In the given expression, we populate arrays at the indices for which the
+/// solver has no constraint by copying values to the left.
 /// For example an expression `ARRAY_OF(0) WITH [1:=2] WITH [4:=3]` would
 /// be interpreted as `{ 2, 2, 3, 3, 3}`.
 /// \param expr: expression to interpret
-/// \param string_max_length: maximum size of arrays to concider
+/// \param string_max_length: maximum size of arrays to consider
 /// \return the interpreted expression
-static exprt concretize_array_expression(
+exprt concretize_arrays_in_expression(
   const exprt &expr, std::size_t string_max_length)
 {
   if(expr.id()==ID_index)
@@ -1122,7 +1122,7 @@ static exprt concretize_array_expression(
   {
     exprt copy=expr;
     for(exprt &op : copy.operands())
-      op=concretize_array_expression(op, string_max_length);
+      op=concretize_arrays_in_expression(op, string_max_length);
     return copy;
   }
 }
@@ -1160,7 +1160,7 @@ bool string_refinementt::check_axioms()
     debug() << "  - negated_axiom:\n"
             << "     " << from_expr(ns, "", negaxiom) << eom;
 
-    exprt with_concretized_arrays=concretize_array_expression(
+    exprt with_concretized_arrays=concretize_arrays_in_expression(
       negaxiom, generator.max_string_length);
     debug() << "  - negated_axiom_with_concretized_array_access:\n"
             << "     " << from_expr(ns, "", with_concretized_arrays) << eom;

src/solvers/refinement/string_refinement.h

@@ -160,6 +160,9 @@ class string_refinementt: public bv_refinementt
 
 exprt substitute_array_lists(exprt expr, size_t string_max_length);
 
+exprt concretize_arrays_in_expression(
+  const exprt &expr, std::size_t string_max_length);
+
 /// Utility function for concretization of strings. Copies concretized values to
 /// the left to initialize the unconcretized indices of concrete_array.
 /// \param concrete_array: the vector to populate