Declare an array_list_exprt class

Author: romainbrenguier

src/solvers/flattening/boolbv_get.cpp

@@ -375,7 +375,7 @@ exprt boolbvt::bv_get_unbounded_array(const exprt &expr) const
 
   if(size_mpint>100 || size.id()==ID_infinity)
   {
-    result = exprt(ID_array_list, type);
+    result = array_list_exprt(to_array_type(type));
     result.type().set(ID_size, integer2string(size_mpint));
 
     result.operands().reserve(values.size()*2);

src/solvers/smt1/smt1_conv.cpp

@@ -219,7 +219,7 @@ exprt smt1_convt::ce_value(
       if(index_expr.is_nil())
         return nil_exprt();
 
-      exprt array_list(ID_array_list, type);
+      array_list_exprt array_list(array_type);
       array_list.copy_to_operands(index_expr, value_expr);
 
       return array_list;

src/util/std_expr.h

@@ -1649,6 +1649,27 @@ template<> inline bool can_cast_expr<array_exprt>(const exprt &base)
   return base.id()==ID_array;
 }
 
+/// Array constructor from a list of index-element pairs
+/// Operands are index/value pairs, alternating.
+class array_list_exprt : public exprt
+{
+public:
+  explicit array_list_exprt(const array_typet &_type)
+    : exprt(ID_array_list, _type)
+  {
+  }
+};
+
+template <>
+inline bool can_cast_expr<array_list_exprt>(const exprt &base)
+{
+  return base.id() == ID_array_list;
+}
+
+inline void validate_expr(const array_list_exprt &value)
+{
+  PRECONDITION(value.operands().size() % 2 == 0);
+}
 
 /*! \brief vector constructor from list of elements
 */

unit/solvers/refinement/string_refinement/substitute_array_list.cpp

@@ -20,7 +20,8 @@ SCENARIO("substitute_array_list",
 {
   const typet char_type=unsignedbv_typet(16);
   const typet int_type=signedbv_typet(32);
-  exprt arr(ID_array_list);
+  const array_typet array_type(char_type, infinity_exprt(int_type));
+  array_list_exprt arr(array_type);
   const exprt index0=from_integer(0, int_type);
   const exprt charx=from_integer('x', char_type);
   const exprt index1=from_integer(1, int_type);