From 6b79297252a8872be6f927562dda4e07a5a32677 Mon Sep 17 00:00:00 2001
From: Ruijie Fang <ruijief@princeton.edu>
Date: Tue, 24 Feb 2026 13:55:39 -0600
Subject: [PATCH] Add missing Java API method for as-array

---
 src/api/java/Context.java | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index b67463431..23f3a68d0 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -1999,6 +1999,19 @@ public class Context implements AutoCloseable {
                 Native.mkArrayDefault(nCtx(), array.getNativeObject()));
     }
 
+    /**                                                                                                                                                                                                          * Create an as-array expression from a function declaration.
+     * @param f the function declaration to lift into an array.
+     *          Must have exactly one domain sort.
+     * @see #mkTermArray(Expr)
+     * @see #mkMap(FuncDecl, Expr[])
+     **/
+    public final <D extends Sort, R extends Sort> ArrayExpr<D, R> mkAsArray(FuncDecl<R> f)
+    {
+        checkContextMatch(f);
+        return (ArrayExpr<D, R>) Expr.create(this, Native.mkAsArray(nCtx(), f.getNativeObject()));
+    }
+
+
     /**
      * Create Extentionality index. Two arrays are equal if and only if they are equal on the index returned by MkArrayExt.
      **/