Define ID_array_list

Replaces the string literal "array-list".

Author: romainbrenguier

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 = exprt(ID_array_list, 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

@@ -189,7 +189,7 @@ 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")
+  if(expr.id() == ID_array_list)
     return of_array_list(expr, extra_value);
   return {};
 }

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);
+      exprt array_list(ID_array_list, 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++)