Handle if_exprt in add_axioms_for_string_literal

cprover_string_literal was requiring a string constant as argument,
but we now deal with if expressions as well.
So expressions like:
`cprover_string_literal_func!0#0(cprover_string_length$3!0@1#2,
nondet_infinite_array$5!0@1, this!0@1#1 == &tmp_object_factory$17!0 ?
tmp_object_factory$17!0#4.@class_identifier :
this$object#0.@class_identifier)`
are correctly handled by the string solver.

Author: romainbrenguier

src/solvers/refinement/string_constraint_generator.h

@@ -199,6 +199,11 @@ class string_constraint_generatort final
   exprt add_axioms_for_insert_char(const function_application_exprt &f);
   exprt add_axioms_for_insert_float(const function_application_exprt &f);
   exprt add_axioms_for_insert_double(const function_application_exprt &f);
+
+  exprt add_axioms_for_cprover_string(
+    const array_string_exprt &res,
+    const exprt &arg,
+    const exprt &guard);
   exprt add_axioms_from_literal(const function_application_exprt &f);
   exprt add_axioms_from_int(const function_application_exprt &f);
   exprt add_axioms_from_int(

src/solvers/refinement/string_constraint_generator_constants.cpp

@@ -67,6 +67,39 @@ exprt string_constraint_generatort::add_axioms_for_empty_string(
   return from_integer(0, get_return_code_type());
 }
 
+/// Convert an expression of type string_typet to a string_exprt
+/// \param res: string expression for the result
+/// \param arg: expression of type string typet
+/// \param guard: condition under which `res` should be equal to arg
+/// \return 0 if constraints were added, 1 if expression could not be handled
+///         and no constraint was added. Expression we can handle are of the
+///         form \f$ e := "<string constant>" | (expr)? e : e \f$
+exprt string_constraint_generatort::add_axioms_for_cprover_string(
+  const array_string_exprt &res,
+  const exprt &arg,
+  const exprt &guard)
+{
+  if(const auto if_expr = expr_try_dynamic_cast<if_exprt>(arg))
+  {
+    const and_exprt guard_true(guard, if_expr->cond());
+    const exprt return_code_true =
+      add_axioms_for_cprover_string(res, if_expr->true_case(), guard_true);
+
+    const and_exprt guard_false(guard, not_exprt(if_expr->cond()));
+    const exprt return_code_false =
+      add_axioms_for_cprover_string(res, if_expr->false_case(), guard_false);
+
+    return if_exprt(
+      equal_exprt(return_code_true, from_integer(0, get_return_code_type())),
+      return_code_false,
+      return_code_true);
+  }
+  else if(const auto constant_expr = expr_try_dynamic_cast<constant_exprt>(arg))
+    return add_axioms_for_constant(res, constant_expr->get_value(), guard);
+  else
+    return from_integer(1, get_return_code_type());
+}
+
 /// String corresponding to an internal cprover string
 ///
 /// Add axioms ensuring that the returned string expression is equal to the
@@ -81,7 +114,5 @@ exprt string_constraint_generatort::add_axioms_from_literal(
   const function_application_exprt::argumentst &args=f.arguments();
   PRECONDITION(args.size() == 3); // Bad args to string literal?
   const array_string_exprt res = char_array_of_pointer(args[1], args[0]);
-  const exprt &arg = args[2];
-  irep_idt sval=to_constant_expr(arg).get_value();
-  return add_axioms_for_constant(res, sval);
+  return add_axioms_for_cprover_string(res, args[2], true_exprt());
 }