Add an at function for access in sparse arrays

Author: romainbrenguier

src/solvers/refinement/string_refinement_util.cpp

@@ -123,6 +123,12 @@ exprt sparse_arrayt::to_if_expression(const exprt &index) const
     });
 }
 
+exprt sparse_arrayt::at(const std::size_t index) const
+{
+  const auto it = entries.find(index);
+  return it != entries.end() ? it->second : default_value;
+}
+
 exprt interval_sparse_arrayt::to_if_expression(const exprt &index) const
 {
   return std::accumulate(
@@ -188,6 +194,13 @@ interval_sparse_arrayt::of_expr(const exprt &expr, const exprt &extra_value)
   return {};
 }
 
+exprt interval_sparse_arrayt::at(const std::size_t index) const
+{
+  // First element at or after index
+  const auto it = entries.lower_bound(index);
+  return it != entries.end() ? it->second : default_value;
+}
+
 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

@@ -96,6 +96,10 @@ class sparse_arrayt
   /// at the given index
   virtual exprt to_if_expression(const exprt &index) const;
 
+  /// Get the value at the specified index.
+  /// Complexity is linear in the number of entries.
+  virtual exprt at(std::size_t index) const;
+
 protected:
   exprt default_value;
   std::map<std::size_t, exprt> entries;
@@ -137,6 +141,10 @@ class interval_sparse_arrayt final : public sparse_arrayt
   static optionalt<interval_sparse_arrayt>
   of_expr(const exprt &expr, const exprt &extra_value);
 
+  /// Get the value at the specified index.
+  /// Complexity is linear in the number of entries.
+  exprt at(std::size_t index) const override;
+
 private:
   explicit interval_sparse_arrayt(exprt default_value)
     : sparse_arrayt(default_value)