Correct find_index function for if-expressions

find_index would give up if the array in the index expression does not
correspond exactly to the given `str`, however it could be an expression
that contains str. For instance `(cond?str1:str2)[i+1]` is equivalent to
`cond?(str1[i+1]):(str2[i+1])`, so in both cases `find_index(e, str1, i)`
should return `i+1`.

Author: romainbrenguier

src/solvers/refinement/string_refinement.cpp

@@ -2091,23 +2091,26 @@ static void update_index_set(
 /// \param [in] expr: the expression to search
 /// \param [in] str: the string which must be indexed
 /// \param [in] qvar: the universal variable that must be in the index
-/// \return an index expression in `expr` on `str` containing `qvar`
-static exprt find_index(
-  const exprt &expr, const exprt &str, const symbol_exprt &qvar)
+/// \return an index expression in `expr` on `str` containing `qvar`. Returns
+///   an empty optional when `expr` does not contain `str`.
+static optionalt<exprt>
+find_index(const exprt &expr, const exprt &str, const symbol_exprt &qvar)
 {
-  const auto it=std::find_if(
-    expr.depth_begin(),
-    expr.depth_end(),
-    [&] (const exprt &e) -> bool
-    {
-      return e.id()==ID_index
-             && to_index_expr(e).array()==str
-             && find_qvar(to_index_expr(e).index(), qvar);
+  const auto it = std::find_if(
+    expr.depth_begin(), expr.depth_end(), [&](const exprt &e) { // NOLINT
+      if(auto index_expr = expr_try_dynamic_cast<index_exprt>(e))
+      {
+        const auto &arr = index_expr->array();
+        const auto str_it = std::find(arr.depth_begin(), arr.depth_end(), str);
+        return str_it != arr.depth_end() &&
+               find_qvar(index_expr->index(), qvar);
+      }
+      return false;
     });
 
-  return it==expr.depth_end()
-         ?nil_exprt()
-         :to_index_expr(*it).index();
+  if(it != expr.depth_end())
+    return to_index_expr(*it).index();
+  return {};
 }
 
 /// Instantiates a string constraint by substituting the quantifiers.
@@ -2128,11 +2131,11 @@ static exprt instantiate(
   const exprt &str,
   const exprt &val)
 {
-  const exprt idx = find_index(axiom.body(), str, axiom.univ_var());
-  if(idx.is_nil())
+  const optionalt<exprt> idx = find_index(axiom.body(), str, axiom.univ_var());
+  if(!idx.has_value())
     return true_exprt();
 
-  const exprt r = compute_inverse_function(stream, axiom.univ_var(), val, idx);
+  const exprt r = compute_inverse_function(stream, axiom.univ_var(), val, *idx);
   implies_exprt instance(
     and_exprt(
       binary_relation_exprt(axiom.univ_var(), ID_ge, axiom.lower_bound()),