Use map-theory terminology: index→key, index_map→domain_map, remove 'array'

In a map theory the tracked expressions are 'keys' and their collection
per equivalence class is the 'domain'.  Rename identifiers, type
aliases, function names, and comments accordingly:

  index_sett          → key_sett
  index_mapt          → domain_mapt
  index_map           → domain_map
  update_indices      → update_keys
  collect_indices()   → collect_keys()
  update_index_map()  → update_domain_map()
  record_array_index()→ record_array_key()

Rename all map_theoryt members, methods, types, enum values, and
comments to use map-theory terminology instead of array-specific terms:

  Types:
    array_equalityt         → map_equalityt
    array_equalitiest       → map_equalitiest
    array_constraint_countt → map_constraint_countt

  Members:
    array_equalities        → map_equalities
    arrays (union-find)     → maps
    lazy_array_constraints  → lazy_constraints
    lazy_arrays             → lazy_dispatch
    get_array_constraints   → get_constraints
    array_constraint_count  → constraint_count

  Methods:
    record_array_equality   → record_equality
    record_array_let_binding→ record_let_binding
    record_array_key        → record_key
    collect_arrays          → collect_maps
    is_unbounded_array      → is_unbounded_map
    add_array_constraint    → add_map_constraint
    add_array_Ackermann_constraints → add_Ackermann_constraints
    add_array_constraints_equality  → add_map_equality_constraints
    display_array_constraint_count  → display_constraint_count
    finish_eager_conversion_arrays  → finish_eager_conversion_maps

  Enum values: ARRAY_* → MAP_*

C-level IR names (index_exprt, ID_index, etc.) are unchanged as they
refer to the array-indexing operation, not the map-theory concept.
Array-specific IR names (array_typet, index_exprt, ID_array,
array_comprehension_args, etc.) and arrayst-specific method names
(add_array_constraints, etc.) are unchanged.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Author: tautschnig

src/solvers/flattening/arrays.cpp

@@ -31,44 +31,44 @@ class arrayst : public map_theoryt
     const namespacet &_ns,
     propt &_prop,
     message_handlert &message_handler,
-    bool get_array_constraints = false);
+    bool get_constraints = false);
 
   // NOLINTNEXTLINE(readability/identifiers)
   typedef map_theoryt SUB;
 
-  literalt record_array_equality(const equal_exprt &expr) override;
+  literalt record_equality(const equal_exprt &expr) override;
 
   /// Record that \p symbol is equal to \p value for the purposes of the
   /// array theory. For unbounded-array-typed bindings this connects the
   /// two expressions in the union-find so that element-wise constraints
   /// propagate correctly.
-  void record_array_let_binding(const symbol_exprt &symbol, const exprt &value)
-    override;
+  void
+  record_let_binding(const symbol_exprt &symbol, const exprt &value) override;
 
 protected:
   message_handlert &message_handler;
 
-  void finish_eager_conversion_arrays() override
+  void finish_eager_conversion_maps() override
   {
     add_array_constraints();
   }
 
   void add_array_constraints();
-  void add_array_constraints(
-    const index_sett &index_set, const exprt &expr);
-  void add_array_constraints_if(
-    const index_sett &index_set, const if_exprt &exprt);
-  void add_array_constraints_with(
-    const index_sett &index_set, const with_exprt &expr);
+  void add_array_constraints(const key_sett &key_set, const exprt &expr);
+  void add_array_constraints_if(const key_sett &key_set, const if_exprt &exprt);
+  void
+  add_array_constraints_with(const key_sett &key_set, const with_exprt &expr);
   void add_array_constraints_update(
-    const index_sett &index_set, const update_exprt &expr);
+    const key_sett &key_set,
+    const update_exprt &expr);
   void add_array_constraints_array_of(
-    const index_sett &index_set, const array_of_exprt &exprt);
+    const key_sett &key_set,
+    const array_of_exprt &exprt);
   void add_array_constraints_array_constant(
-    const index_sett &index_set,
+    const key_sett &key_set,
     const array_exprt &exprt);
   void add_array_constraints_comprehension(
-    const index_sett &index_set,
+    const key_sett &key_set,
     const array_comprehension_exprt &expr);
 };
 

src/solvers/flattening/arrays.h

@@ -511,7 +511,7 @@ bool boolbvt::boolbv_set_equality_to_true(const equal_exprt &expr)
     type.id() != ID_bool)
   {
     // see if it is an unbounded array
-    if(is_unbounded_array(type))
+    if(is_unbounded_map(type))
       return true;
 
     const bvt &bv1=convert_bv(expr.rhs());
@@ -540,7 +540,7 @@ void boolbvt::set_to(const exprt &expr, bool value)
   SUB::set_to(expr, value);
 }
 
-bool boolbvt::is_unbounded_array(const typet &type) const
+bool boolbvt::is_unbounded_map(const typet &type) const
 {
   if(type.id()!=ID_array)
     return false;

src/solvers/flattening/boolbv.cpp

@@ -53,8 +53,8 @@ class boolbvt:public arrayst
     const namespacet &_ns,
     propt &_prop,
     message_handlert &message_handler,
-    bool get_array_constraints = false)
-    : arrayst(_ns, _prop, message_handler, get_array_constraints),
+    bool get_constraints = false)
+    : arrayst(_ns, _prop, message_handler, get_constraints),
       unbounded_array(unbounded_arrayt::U_NONE),
       bv_width(_ns),
       bv_utils(_prop),
@@ -267,7 +267,7 @@ class boolbvt:public arrayst
   exprt get_value(const exprt &expr) const;
 
   // unbounded arrays
-  bool is_unbounded_array(const typet &type) const override;
+  bool is_unbounded_map(const typet &type) const override;
 
   // quantifier instantiations
   class quantifiert

src/solvers/flattening/boolbv.h

@@ -20,7 +20,7 @@ bvt boolbvt::convert_array_of(const array_of_exprt &expr)
 
   const array_typet &array_type = expr.type();
 
-  if(is_unbounded_array(array_type))
+  if(is_unbounded_map(array_type))
     return conversion_failed(expr);
 
   std::size_t width=boolbv_width(array_type);

src/solvers/flattening/boolbv_array_of.cpp

@@ -34,7 +34,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
 {
   // array logic does not handle byte operators, thus lower when operating on
   // unbounded arrays
-  if(is_unbounded_array(expr.op().type()))
+  if(is_unbounded_map(expr.op().type()))
   {
     return convert_bv(lower_byte_extract(expr, ns));
   }

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -17,8 +17,7 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
   // if we update (from) an unbounded array, lower the expression as the array
   // logic does not handle byte operators
   if(
-    is_unbounded_array(expr.op().type()) ||
-    is_unbounded_array(expr.value().type()))
+    is_unbounded_map(expr.op().type()) || is_unbounded_map(expr.value().type()))
   {
     return convert_bv(lower_byte_update(expr, ns));
   }

src/solvers/flattening/boolbv_byte_update.cpp

@@ -22,17 +22,16 @@ literalt boolbvt::convert_equality(const equal_exprt &expr)
     irep_pretty_diagnosticst{expr.rhs()});
 
   // see if it is an unbounded array
-  if(is_unbounded_array(expr.lhs().type()))
+  if(is_unbounded_map(expr.lhs().type()))
   {
     // flatten byte_update/byte_extract operators if needed
 
     if(has_byte_operator(expr))
     {
-      return record_array_equality(
-        to_equal_expr(lower_byte_operators(expr, ns)));
+      return record_equality(to_equal_expr(lower_byte_operators(expr, ns)));
     }
 
-    return record_array_equality(expr);
+    return record_equality(expr);
   }
 
   const bvt &lhs_bv = convert_bv(expr.lhs());

src/solvers/flattening/boolbv_equality.cpp

@@ -108,7 +108,7 @@ exprt boolbvt::bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset)
     {
       const auto &array_type = to_array_type(type);
 
-      if(is_unbounded_array(type))
+      if(is_unbounded_map(type))
         return bv_get_unbounded_array(expr);
 
       const typet &subtype = array_type.element_type();
@@ -328,20 +328,18 @@ exprt boolbvt::bv_get_unbounded_array(const exprt &expr) const
   typedef std::map<mp_integer, exprt> valuest;
   valuest values;
 
-  const auto opt_num = arrays.get_number(expr);
+  const auto opt_num = maps.get_number(expr);
   if(opt_num.has_value())
   {
     // get root
-    const auto number = arrays.find_number(*opt_num);
+    const auto number = maps.find_number(*opt_num);
 
-    CHECK_RETURN(number < index_map.size());
-    index_mapt::const_iterator it=index_map.find(number);
-    CHECK_RETURN(it != index_map.end());
-    const index_sett &index_set=it->second;
+    CHECK_RETURN(number < domain_map.size());
+    domain_mapt::const_iterator it = domain_map.find(number);
+    CHECK_RETURN(it != domain_map.end());
+    const key_sett &key_set = it->second;
 
-    for(index_sett::const_iterator it1=
-        index_set.begin();
-        it1!=index_set.end();
+    for(key_sett::const_iterator it1 = key_set.begin(); it1 != key_set.end();
         it1++)
     {
       index_exprt index(expr, *it1);

src/solvers/flattening/boolbv_get.cpp

@@ -34,7 +34,7 @@ bvt boolbvt::convert_index(const index_exprt &expr)
 
     // see if the array size is constant
 
-    if(is_unbounded_array(array_type))
+    if(is_unbounded_map(array_type))
     {
       // use array decision procedure
 
@@ -65,7 +65,7 @@ bvt boolbvt::convert_index(const index_exprt &expr)
         // free variables
         bv = prop.new_variables(boolbv_width(expr.type()));
 
-        record_array_index(expr);
+        record_key(expr);
 
         // record type if array is a symbol
         if(array.id() == ID_symbol || array.id() == ID_nondet_symbol)