Add an interval_sparse_array::of_expr function

This initialize a sparse array from the array expression we know how to
deal with.

Author: romainbrenguier

src/solvers/refinement/string_refinement_util.cpp

@@ -176,6 +176,18 @@ interval_sparse_arrayt interval_sparse_arrayt::of_array_list(
   return sparse_array;
 }
 
+optionalt<interval_sparse_arrayt>
+interval_sparse_arrayt::of_expr(const exprt &expr, const exprt &extra_value)
+{
+  if(const auto &array_expr = expr_try_dynamic_cast<array_exprt>(expr))
+    return interval_sparse_arrayt(*array_expr, extra_value);
+  if(const auto &with_expr = expr_try_dynamic_cast<with_exprt>(expr))
+    return interval_sparse_arrayt(*with_expr);
+  if(expr.id() == "array-list")
+    return of_array_list(expr, extra_value);
+  return {};
+}
+
 void equation_symbol_mappingt::add(const std::size_t i, const exprt &expr)
 {
   equations_containing[expr].push_back(i);

src/solvers/refinement/string_refinement_util.h

@@ -132,6 +132,11 @@ class interval_sparse_arrayt final : public sparse_arrayt
 
   exprt to_if_expression(const exprt &index) const override;
 
+  /// If the expression is an array_exprt or a with_exprt uses the appropriate
+  /// constructor, otherwise returns empty optional.
+  static optionalt<interval_sparse_arrayt>
+  of_expr(const exprt &expr, const exprt &extra_value);
+
 private:
   explicit interval_sparse_arrayt(exprt default_value)
     : sparse_arrayt(default_value)