(interval_)sparse_arrayt: Remove unnecessary use of "virtual" and fur…

…ther cleanup

src/solvers/refinement/string_refinement.cpp

@@ -1067,7 +1067,7 @@ static exprt substitute_array_access(
   const bool left_propagate)
 {
   return left_propagate ? interval_sparse_arrayt(expr).to_if_expression(index)
-                        : sparse_arrayt(expr).to_if_expression(index);
+                        : sparse_arrayt::to_if_expression(expr, index);
 }
 
 /// Create an equivalent expression where array accesses are replaced by 'if'

src/solvers/refinement/string_refinement_util.cpp

@@ -73,12 +73,16 @@ sparse_arrayt::sparse_arrayt(const with_exprt &expr)
   default_value = expr_dynamic_cast<array_of_exprt>(ref.get()).what();
 }
 
-exprt sparse_arrayt::to_if_expression(const exprt &index) const
+exprt sparse_arrayt::to_if_expression(
+  const with_exprt &expr,
+  const exprt &index)
 {
+  sparse_arrayt sparse_array(expr);
+
   return std::accumulate(
-    entries.begin(),
-    entries.end(),
-    default_value,
+    sparse_array.entries.begin(),
+    sparse_array.entries.end(),
+    sparse_array.default_value,
     [&](
       const exprt if_expr,
       const std::pair<std::size_t, exprt> &entry) { // NOLINT
@@ -90,12 +94,6 @@ 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(

src/solvers/refinement/string_refinement_util.h

@@ -73,11 +73,7 @@ class sparse_arrayt
 
   /// Creates an if_expr corresponding to the result of accessing the array
   /// 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;
+  static exprt to_if_expression(const with_exprt &expr, const exprt &index);
 
 protected:
   exprt default_value;
@@ -114,7 +110,7 @@ class interval_sparse_arrayt final : public sparse_arrayt
     const array_list_exprt &expr,
     const exprt &extra_value);
 
-  exprt to_if_expression(const exprt &index) const override;
+  exprt to_if_expression(const exprt &index) const;
 
   /// If the expression is an array_exprt or a with_exprt uses the appropriate
   /// constructor, otherwise returns empty optional.
@@ -125,8 +121,8 @@ class interval_sparse_arrayt final : public sparse_arrayt
   array_exprt concretize(std::size_t size, const typet &index_type) const;
 
   /// Get the value at the specified index.
-  /// Complexity is linear in the number of entries.
-  exprt at(std::size_t index) const override;
+  /// Complexity is logarithmic in the number of entries.
+  exprt at(std::size_t index) const;
 
   /// Array containing the same value at each index.
   explicit interval_sparse_arrayt(exprt default_value)

unit/solvers/refinement/string_refinement/sparse_array.cpp

@@ -45,7 +45,6 @@ SCENARIO("sparse_array", "[core][solvers][refinement][string_refinement]")
 
     WHEN("It is converted to a sparse array")
     {
-      const sparse_arrayt sparse_array(input_expr);
       THEN("The resulting if expression is index=100?z:index=4?x:index=1?y:0")
       {
         const symbol_exprt index("index", int_type);
@@ -57,7 +56,7 @@ SCENARIO("sparse_array", "[core][solvers][refinement][string_refinement]")
             charx,
             if_exprt(
               equal_exprt(index, index1), chary, from_integer(0, char_type))));
-        REQUIRE(sparse_array.to_if_expression(index) == expected);
+        REQUIRE(sparse_arrayt::to_if_expression(input_expr, index) == expected);
       }
     }