Address commenters' suggestions

Author: Lukasz A.J. Wrona

src/solvers/refinement/bv_refinement_loop.cpp

@@ -45,7 +45,7 @@ decision_proceduret::resultt bv_refinementt::dec_solve()
     {
       xmlt xml("refinement-iteration");
       xml.data=std::to_string(iteration);
-      std::cout << xml << '\n';
+      status() << xml << '\n';
     }
 
     switch(prop_solve())

src/solvers/refinement/string_constraint_generator.h

@@ -46,8 +46,7 @@ class string_constraint_generatort final
     bool string_printable=false;
   };
 
-  explicit string_constraint_generatort(
-    const infot& info, const namespacet& ns);
+  string_constraint_generatort(const infot& info, const namespacet& ns);
 
   /// Axioms are of three kinds: universally quantified string constraint,
   /// not contains string constraints and simple formulas.
@@ -81,6 +80,11 @@ class string_constraint_generatort final
 
   symbol_exprt fresh_exist_index(const irep_idt &prefix, const typet &type);
 
+  /// remove functions applications and create the necessary axioms
+  /// \par parameters: an expression containing function applications
+  /// \return an expression containing no function application
+  exprt substitute_function_applications(const exprt& expr);
+
 private:
   symbol_exprt fresh_boolean(const irep_idt &prefix);
   string_exprt fresh_string(const refined_string_typet &type);

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -628,3 +628,19 @@ exprt string_constraint_generatort::add_axioms_for_to_char_array(
   string_exprt str=get_string_expr(args(f, 1)[0]);
   return str.content();
 }
+
+exprt string_constraint_generatort::substitute_function_applications(
+  const exprt &expr)
+{
+  exprt copy=expr;
+  for(exprt &operand : copy.operands())
+    operand=substitute_function_applications(exprt(operand));
+
+  if(copy.id()==ID_function_application)
+  {
+    function_application_exprt f=to_function_application_expr(copy);
+    return this->add_axioms_for_function_application(f);
+  }
+
+  return copy;
+}