From 121f66c19ce0dbe131b64db2f6d03ab827cecb3e Mon Sep 17 00:00:00 2001 From: Ruijie Fang <57693513+ruijiefang@users.noreply.github.com> Date: Mon, 29 Sep 2025 21:47:11 -0500 Subject: [PATCH 1/4] Distinguish between Quantifier and Lambda in AST.java --- src/api/java/AST.java | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/api/java/AST.java b/src/api/java/AST.java index 99cdde948..c2e4208c9 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -208,7 +208,13 @@ public class AST extends Z3Object implements Comparable case Z3_FUNC_DECL_AST: return new FuncDecl<>(ctx, obj); case Z3_QUANTIFIER_AST: - return new Quantifier(ctx, obj); + // a quantifier AST is a lambda iff it is neither a forall nor an exists. + boolean isLambda = !Native.isQuantifierExists(ctx, obj) && !Native.isQuantifierForall(ctx, obj); + if (isLambda) { + return new Lambda(ctx, obj); + } else { + return new Quantifier(ctx, obj); + } case Z3_SORT_AST: return Sort.create(ctx, obj); case Z3_APP_AST: From c791694af8947a0ca817180287c6288486e52e53 Mon Sep 17 00:00:00 2001 From: Ruijie Fang <57693513+ruijiefang@users.noreply.github.com> Date: Mon, 29 Sep 2025 21:48:33 -0500 Subject: [PATCH 2/4] Distinguish betwee Lambda and Quantifier in Expr.java --- src/api/java/Expr.java | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index 60826665d..96e2e2c38 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -2148,8 +2148,15 @@ public class Expr extends AST static Expr create(Context ctx, long obj) { Z3_ast_kind k = Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj)); - if (k == Z3_ast_kind.Z3_QUANTIFIER_AST) - return new Quantifier(ctx, obj); + if (k == Z3_ast_kind.Z3_QUANTIFIER_AST) { + // a quantifier AST is a lambda iff it is neither a forall nor an exists. + boolean isLambda = !Native.isQuantifierExists(ctx, obj) && !Native.isQuantifierForall(ctx, obj); + if (isLambda) { + return new Lambda(ctx, obj); + } else { + return new Quantifier(ctx, obj); + } + } long s = Native.getSort(ctx.nCtx(), obj); Z3_sort_kind sk = Z3_sort_kind .fromInt(Native.getSortKind(ctx.nCtx(), s)); From d86c049df25df9b8ca37cc67d245c9da9e929dc7 Mon Sep 17 00:00:00 2001 From: Ruijie Fang Date: Mon, 29 Sep 2025 21:52:54 -0500 Subject: [PATCH 3/4] Make things compile --- src/api/java/AST.java | 2 +- src/api/java/Expr.java | 2 +- src/api/java/Lambda.java | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/api/java/AST.java b/src/api/java/AST.java index c2e4208c9..0257f5294 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -209,7 +209,7 @@ public class AST extends Z3Object implements Comparable return new FuncDecl<>(ctx, obj); case Z3_QUANTIFIER_AST: // a quantifier AST is a lambda iff it is neither a forall nor an exists. - boolean isLambda = !Native.isQuantifierExists(ctx, obj) && !Native.isQuantifierForall(ctx, obj); + boolean isLambda = !Native.isQuantifierExists(ctx.nCtx(), obj) && !Native.isQuantifierForall(ctx.nCtx(), obj); if (isLambda) { return new Lambda(ctx, obj); } else { diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index 96e2e2c38..910869bcd 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -2150,7 +2150,7 @@ public class Expr extends AST Z3_ast_kind k = Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj)); if (k == Z3_ast_kind.Z3_QUANTIFIER_AST) { // a quantifier AST is a lambda iff it is neither a forall nor an exists. - boolean isLambda = !Native.isQuantifierExists(ctx, obj) && !Native.isQuantifierForall(ctx, obj); + boolean isLambda = !Native.isQuantifierExists(ctx.nCtx(), obj) && !Native.isQuantifierForall(ctx.nCtx(), obj); if (isLambda) { return new Lambda(ctx, obj); } else { diff --git a/src/api/java/Lambda.java b/src/api/java/Lambda.java index 780e543c8..a42dfbf45 100644 --- a/src/api/java/Lambda.java +++ b/src/api/java/Lambda.java @@ -126,7 +126,7 @@ public class Lambda extends ArrayExpr } - private Lambda(Context ctx, long obj) + Lambda(Context ctx, long obj) { super(ctx, obj); } From 6b79297252a8872be6f927562dda4e07a5a32677 Mon Sep 17 00:00:00 2001 From: Ruijie Fang Date: Tue, 24 Feb 2026 13:55:39 -0600 Subject: [PATCH 4/4] 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 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. **/