Separate pointer/function substitutions in solver

We make the solver do two passes on the equations:
there is now one pass just for pointer and array associations before
substituting function applications.

Author: romainbrenguier

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -558,10 +558,6 @@ exprt string_constraint_generatort::add_axioms_for_function_application(
     res=add_axioms_for_intern(expr);
   else if(id==ID_cprover_string_format_func)
     res=add_axioms_for_format(expr);
-  else if(id == ID_cprover_associate_array_to_pointer_func)
-    res = associate_array_to_pointer(expr);
-  else if(id == ID_cprover_associate_length_to_array_func)
-    res = associate_length_to_array(expr);
   else if(id == ID_cprover_string_constrain_characters_func)
     res = add_axioms_for_constrain_characters(expr);
   else

src/solvers/refinement/string_refinement.cpp

@@ -283,6 +283,23 @@ static void substitute_function_applications_in_equations(
     eq.rhs() = substitute_function_applications(eq.rhs(), generator);
 }
 
+/// Fill the array_pointer correspondence and replace the right hand sides of
+/// the corresponding equations
+static void make_char_array_pointer_associations(
+  string_constraint_generatort &generator,
+  std::vector<equal_exprt> &equations)
+{
+  for(equal_exprt &eq : equations)
+  {
+    if(
+      const auto fun_app =
+        expr_try_dynamic_cast<function_application_exprt>(eq.rhs()))
+    {
+      if(const auto result = generator.make_array_pointer_association(*fun_app))
+        eq.rhs() = *result;
+    }
+  }
+}
 
 void replace_symbols_in_equations(
   const union_find_replacet &symbol_resolve,
@@ -658,6 +675,8 @@ decision_proceduret::resultt string_refinementt::dec_solve()
       string_id_symbol_resolve.replace_expr(eq.rhs());
   }
 
+  make_char_array_pointer_associations(generator, equations);
+
 #ifdef DEBUG
   output_equations(debug(), equations, ns);
 #endif
@@ -671,8 +690,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
 
 #ifdef DEBUG
   debug() << "dec_solve: arrays_of_pointers:" << eom;
-  for(auto pair :
-      generator.array_pointer_correspondance.get_arrays_of_pointers())
+  for(auto pair : generator.array_pool.get_arrays_of_pointers())
   {
     debug() << "  * " << from_expr(ns, "", pair.first) << "\t--> "
             << from_expr(ns, "", pair.second) << " : "