Initialization of sparse array from array-list

Author: romainbrenguier

src/solvers/refinement/string_refinement_util.cpp

@@ -158,6 +158,24 @@ interval_sparse_arrayt::interval_sparse_arrayt(
   }
 }
 
+interval_sparse_arrayt interval_sparse_arrayt::of_array_list(
+  const exprt &expr,
+  const exprt &extra_value)
+{
+  PRECONDITION(expr.operands().size() % 2 == 0);
+  interval_sparse_arrayt sparse_array(extra_value);
+  for(std::size_t i = 0; i < expr.operands().size(); i += 2)
+  {
+    const auto index = numeric_cast<std::size_t>(expr.operands()[i]);
+    INVARIANT(
+      expr.operands()[i + 1].type() == extra_value.type(),
+      "all values in array should have the same type");
+    if(index.has_value() && expr.operands()[i + 1].id() != ID_unknown)
+      sparse_array.entries[*index] = expr.operands()[i + 1];
+  }
+  return sparse_array;
+}
+
 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

@@ -124,7 +124,19 @@ class interval_sparse_arrayt final : public sparse_arrayt
   /// `extra_value`.
   interval_sparse_arrayt(const array_exprt &expr, const exprt &extra_value);
 
+  /// Initialize a sparse array from an array represented by a list of
+  /// index-value pairs, and setting the default to `extra_value`.
+  /// Indexes must be constant expressions, and negative indexes are ignored.
+  static interval_sparse_arrayt
+  of_array_list(const exprt &expr, const exprt &extra_value);
+
   exprt to_if_expression(const exprt &index) const override;
+
+private:
+  explicit interval_sparse_arrayt(exprt default_value)
+    : sparse_arrayt(default_value)
+  {
+  }
 };
 
 /// Maps equation to expressions contained in them and conversely expressions to