Define ID and exprt for array-list

src/ansi-c/expr2c.cpp

@@ -3913,7 +3913,7 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id()==ID_array)
     return convert_array(src, precedence);
 
-  else if(src.id()=="array-list")
+  else if(src.id() == ID_array_list)
     return convert_array_list(src, precedence);
 
   else if(src.id()==ID_typecast)

src/goto-programs/interpreter_evaluate.cpp

@@ -934,7 +934,7 @@ void interpretert::evaluate(
               return;
           }
         }
-        else if(expr.op0().id()=="array-list")
+        else if(expr.op0().id() == ID_array_list)
         {
           // This sort of construct comes from boolbv_get, but doesn't seem
           // to have an exprt yet. Its operands are a list of key-value pairs.

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("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/refinement/string_refinement.cpp

@@ -2050,7 +2050,7 @@ exprt substitute_array_lists(exprt expr, size_t string_max_length)
   for(auto &operand : expr.operands())
     operand = substitute_array_lists(operand, string_max_length);
 
-  if(expr.id()=="array-list")
+  if(expr.id() == ID_array_list)
   {
     DATA_INVARIANT(
       expr.operands().size()>=2,

src/solvers/refinement/string_refinement_util.cpp

@@ -164,22 +164,21 @@ interval_sparse_arrayt::interval_sparse_arrayt(
   }
 }
 
-interval_sparse_arrayt interval_sparse_arrayt::of_array_list(
-  const exprt &expr,
+interval_sparse_arrayt::interval_sparse_arrayt(
+  const array_list_exprt &expr,
   const exprt &extra_value)
+  : interval_sparse_arrayt(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];
+      entries[*index] = expr.operands()[i + 1];
   }
-  return sparse_array;
 }
 
 optionalt<interval_sparse_arrayt>
@@ -189,8 +188,8 @@ interval_sparse_arrayt::of_expr(const exprt &expr, const exprt &extra_value)
     return interval_sparse_arrayt(*array_expr, extra_value);
   if(const auto &with_expr = expr_try_dynamic_cast<with_exprt>(expr))
     return interval_sparse_arrayt(*with_expr);
-  if(expr.id() == "array-list")
-    return of_array_list(expr, extra_value);
+  if(const auto &array_list = expr_try_dynamic_cast<array_list_exprt>(expr))
+    return interval_sparse_arrayt(*array_list, extra_value);
   return {};
 }
 

src/solvers/refinement/string_refinement_util.h

@@ -131,8 +131,9 @@ class interval_sparse_arrayt final : public sparse_arrayt
   /// 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);
+  interval_sparse_arrayt(
+    const array_list_exprt &expr,
+    const exprt &extra_value);
 
   exprt to_if_expression(const exprt &index) const override;
 

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("array-list", type);
+      array_list_exprt array_list(array_type);
       array_list.copy_to_operands(index_expr, value_expr);
 
       return array_list;

src/solvers/smt1/smt1_conv.h

@@ -158,7 +158,7 @@ class smt1_convt:public prop_convt
     const std::string &value)
   {
     exprt tmp=ce_value(identifier.type, index, value, false);
-    if(tmp.id()=="array-list" && identifier.value.id()=="array-list")
+    if(tmp.id() == ID_array_list && identifier.value.id() == ID_array_list)
     {
       forall_operands(it, tmp)
         identifier.value.copy_to_operands(*it);

src/util/irep_ids.def

@@ -246,6 +246,7 @@ IREP_ID_ONE(array_of)
 IREP_ID_ONE(array_equal)
 IREP_ID_ONE(array_set)
 IREP_ID_ONE(array_copy)
+IREP_ID_ONE(array_list)
 IREP_ID_ONE(mod)
 IREP_ID_ONE(rem)
 IREP_ID_ONE(shr)

src/util/simplify_expr_array.cpp

@@ -167,7 +167,7 @@ bool simplify_exprt::simplify_index(exprt &expr)
       return false;
     }
   }
-  else if(array.id()=="array-list")
+  else if(array.id() == ID_array_list)
   {
     // These are index/value pairs, alternating.
     for(size_t i=0; i<array.operands().size()/2; i++)

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("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);