extend the array_list_exprt API

The new API encourages maintaining the class invariants (type and even
number of operands).

Author: Daniel Kroening

src/util/std_expr.h

@@ -1728,6 +1728,22 @@ class array_list_exprt : public multi_ary_exprt
     : multi_ary_exprt(ID_array_list, std::move(_operands), _type)
   {
   }
+
+  const array_typet &type() const
+  {
+    return static_cast<const array_typet &>(multi_ary_exprt::type());
+  }
+
+  array_typet &type()
+  {
+    return static_cast<array_typet &>(multi_ary_exprt::type());
+  }
+
+  /// add an index/value pair
+  void add(exprt index, exprt value)
+  {
+    add_to_operands(std::move(index), std::move(value));
+  }
 };
 
 template <>
@@ -1741,6 +1757,22 @@ inline void validate_expr(const array_list_exprt &value)
   PRECONDITION(value.operands().size() % 2 == 0);
 }
 
+inline const array_list_exprt &to_array_list_expr(const exprt &expr)
+{
+  PRECONDITION(can_cast_expr<array_list_exprt>(expr));
+  auto &ret = static_cast<const array_list_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+inline array_list_exprt &to_array_list_expr(exprt &expr)
+{
+  PRECONDITION(can_cast_expr<array_list_exprt>(expr));
+  auto &ret = static_cast<array_list_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
 /// \brief Vector constructor from list of elements
 class vector_exprt : public multi_ary_exprt
 {