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 ArrayExpr mkAsArray(FuncDecl f) + { + checkContextMatch(f); + return (ArrayExpr) 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. **/