Add array eta-reduction rewrite: (lambda (x*) (select a x*)) -> a

Sound by array extensionality when a is independent of the bound
variables. Implemented as array_rewriter::mk_lambda_core and wired into
th_rewriter::reduce_quantifier alongside the ground-lambda case.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

src/ast/rewriter/array_rewriter.cpp

@@ -399,6 +399,40 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args,
     return BR_FAILED;
 }
 
+br_status array_rewriter::mk_lambda_core(quantifier * q, expr * body, expr_ref & result) {
+    // Array eta-reduction:
+    //   (lambda (x_0 ... x_{k-1}) (select a x_0 ... x_{k-1}))  -->  a
+    // sound by array extensionality, provided 'a' is independent of the bound
+    // variables x_0..x_{k-1}.
+    if (!m_util.is_select(body))
+        return BR_FAILED;
+    app * sel = to_app(body);
+    unsigned k = q->get_num_decls();
+    // select over a k-dimensional array takes the array plus k indices.
+    if (sel->get_num_args() != k + 1)
+        return BR_FAILED;
+    // The j-th index argument must be exactly the bound variable of the j-th
+    // declaration. With de Bruijn indexing the j-th declaration is var(k-1-j).
+    for (unsigned j = 0; j < k; ++j) {
+        expr * idx = sel->get_arg(j + 1);
+        if (!is_var(idx) || to_var(idx)->get_idx() != k - 1 - j)
+            return BR_FAILED;
+    }
+    expr * a = sel->get_arg(0);
+    // 'a' must not reference any of the bound variables 0..k-1.
+    if (!is_ground(a)) {
+        expr_free_vars fv(a);
+        for (unsigned j = 0; j < k; ++j)
+            if (fv.contains(j))
+                return BR_FAILED;
+    }
+    // Shift the remaining free variables of 'a' down by k, since they are no
+    // longer under the eliminated lambda binder.
+    inv_var_shifter sh(m());
+    sh(a, k, result);
+    return BR_DONE;
+}
+
 sort_ref array_rewriter::get_map_array_sort(func_decl* f, unsigned num_args, expr* const* args) {
     sort* s0 = args[0]->get_sort();
     unsigned sz = get_array_arity(s0);

src/ast/rewriter/array_rewriter.h

@@ -72,6 +72,13 @@ public:
     void mk_select(unsigned num_args, expr * const * args, expr_ref & result);
     void mk_map(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
 
+    // Array eta-reduction:
+    //   (lambda (x_0 ... x_{k-1}) (select a x_0 ... x_{k-1}))  -->  a
+    // when 'a' does not depend on the bound variables x_0..x_{k-1}.
+    // 'q' supplies the lambda binder, 'body' its (already rewritten) body.
+    // Returns BR_DONE with 'result' set to the eta-reduced array, or BR_FAILED.
+    br_status mk_lambda_core(quantifier * q, expr * body, expr_ref & result);
+
     bool has_index_set(expr* e, expr_ref& e0, vector<expr_ref_vector>& indices);
 
 

src/ast/rewriter/th_rewriter.cpp

@@ -814,6 +814,14 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
             }
             return true;
         }
+        else if (old_q->get_kind() == lambda_k &&
+                 BR_DONE == m_ar_rw.mk_lambda_core(old_q, new_body, result)) {
+            // array eta-reduction: (lambda (x*) (select a x*)) --> a
+            if (m().proofs_enabled()) {
+                result_pr = m().mk_rewrite(old_q, result);
+            }
+            return true;
+        }
         else {
             ptr_buffer<expr> new_patterns_buf;
             ptr_buffer<expr> new_no_patterns_buf;