From b8e15f2121b97c7b51e1d4fd6cd145ab9af4d53d Mon Sep 17 00:00:00 2001 From: Angelica Moreira <48168649+angelica-moreira@users.noreply.github.com> Date: Sat, 14 Mar 2026 10:13:42 -0700 Subject: [PATCH] Add missing AST query methods to Java API (#8977) * add Expr.isGround() to Java API Expose Z3_is_ground as a public method on Expr. Returns true when the expression contains no free variables. * add Expr.isLambda() to Java API Expose Z3_is_lambda as a public method on Expr. Returns true when the expression is a lambda quantifier. * add AST.getDepth() to Java API Expose Z3_get_depth as a public method on AST. Returns the maximum number of nodes on any path from root to leaf. * add ArraySort.getArity() to Java API Expose Z3_get_array_arity as a public method on ArraySort. Returns the number of dimensions of a multi-dimensional array sort. * add DatatypeSort.isRecursive() to Java API Expose Z3_is_recursive_datatype_sort as a public method on DatatypeSort. Returns true when the datatype refers to itself. * add FPExpr.isNumeral() to Java API Expose Z3_fpa_is_numeral as a public method on FPExpr. Returns true when the expression is a concrete floating-point value. * add isGroundExample test to JavaExample Test Expr.isGround() on constants, variables, and compound expressions. * add astDepthExample test to JavaExample Test AST.getDepth() on leaf nodes and nested expressions to verify the depth computation. * add arrayArityExample test to JavaExample Test ArraySort.getArity() on single-domain and multi-domain array sorts. * add recursiveDatatypeExample test to JavaExample Test DatatypeSort.isRecursive() on a recursive list datatype and a non-recursive pair datatype. * add fpNumeralExample test to JavaExample Test FPExpr.isNumeral() on a floating point constant and a symbolic variable. * add isLambdaExample test to JavaExample Test Expr.isLambda() on a lambda expression and a plain variable. --- examples/java/JavaExample.java | 143 +++++++++++++++++++++++++++++++++ src/api/java/AST.java | 10 +++ src/api/java/ArraySort.java | 10 +++ src/api/java/DatatypeSort.java | 11 +++ src/api/java/Expr.java | 20 +++++ src/api/java/FPExpr.java | 12 ++- 6 files changed, 205 insertions(+), 1 deletion(-) diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index a27a60721..734f410dd 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -2277,6 +2277,143 @@ class JavaExample } + @SuppressWarnings("unchecked") + void isGroundExample(Context ctx) throws TestFailedException + { + System.out.println("IsGroundExample"); + Log.append("IsGroundExample"); + + // a constant integer is ground + IntExpr five = ctx.mkInt(5); + if (!five.isGround()) + throw new TestFailedException(); + + // a free variable is not ground + IntExpr x = ctx.mkIntConst("x"); + if (!x.isGround()) + throw new TestFailedException(); + + // an addition of constants is ground + Expr sum = ctx.mkAdd(ctx.mkInt(1), ctx.mkInt(2)); + if (!sum.isGround()) + throw new TestFailedException(); + + System.out.println("IsGroundExample passed."); + } + + @SuppressWarnings("unchecked") + void astDepthExample(Context ctx) throws TestFailedException + { + System.out.println("AstDepthExample"); + Log.append("AstDepthExample"); + + // a plain integer constant has depth 1 + IntExpr five = ctx.mkInt(5); + if (five.getDepth() != 1) + throw new TestFailedException(); + + // (x + 1) should have depth 2 + IntExpr x = ctx.mkIntConst("x"); + Expr sum = ctx.mkAdd(x, ctx.mkInt(1)); + if (sum.getDepth() != 2) + throw new TestFailedException(); + + // nested: (x + 1) * y should have depth 3 + IntExpr y = ctx.mkIntConst("y"); + Expr prod = ctx.mkMul(sum, y); + if (prod.getDepth() != 3) + throw new TestFailedException(); + + System.out.println("AstDepthExample passed."); + } + + void arrayArityExample(Context ctx) throws TestFailedException + { + System.out.println("ArrayArityExample"); + Log.append("ArrayArityExample"); + + // Array Int -> Int has arity 1 + ArraySort arr1 = ctx.mkArraySort(ctx.getIntSort(), ctx.getIntSort()); + if (arr1.getArity() != 1) + throw new TestFailedException(); + + // Array (Int, Bool) -> Int has arity 2 + ArraySort arr2 = ctx.mkArraySort(new Sort[]{ctx.getIntSort(), ctx.getBoolSort()}, ctx.getIntSort()); + if (arr2.getArity() != 2) + throw new TestFailedException(); + + System.out.println("ArrayArityExample passed."); + } + + void recursiveDatatypeExample(Context ctx) throws TestFailedException + { + System.out.println("RecursiveDatatypeExample"); + Log.append("RecursiveDatatypeExample"); + + // a list sort is recursive (cons refers back to the list) + Constructor nil = ctx.mkConstructor("nil", "is_nil", null, null, null); + Constructor cons = ctx.mkConstructor("cons", "is_cons", + new String[]{"head", "tail"}, + new Sort[]{ctx.getIntSort(), null}, + new int[]{0, 0}); + DatatypeSort intList = ctx.mkDatatypeSort("intlist", new Constructor[]{nil, cons}); + if (!intList.isRecursive()) + throw new TestFailedException(); + + // a simple pair sort is not recursive + Constructor mkPair = ctx.mkConstructor("mkpair", "is_pair", + new String[]{"fst", "snd"}, + new Sort[]{ctx.getIntSort(), ctx.getBoolSort()}, + null); + DatatypeSort pair = ctx.mkDatatypeSort("Pair", new Constructor[]{mkPair}); + if (pair.isRecursive()) + throw new TestFailedException(); + + System.out.println("RecursiveDatatypeExample passed."); + } + + void fpNumeralExample(Context ctx) throws TestFailedException + { + System.out.println("FpNumeralExample"); + Log.append("FpNumeralExample"); + + FPSort fpsort = ctx.mkFPSort32(); + + // a floating point numeral + FPExpr fpval = (FPExpr) ctx.mkFP(3.14, fpsort); + if (!fpval.isNumeral()) + throw new TestFailedException(); + + // a symbolic FP variable is not a numeral + FPExpr fpvar = (FPExpr) ctx.mkConst("fpx", fpsort); + if (fpvar.isNumeral()) + throw new TestFailedException(); + + System.out.println("FpNumeralExample passed."); + } + + @SuppressWarnings("unchecked") + void isLambdaExample(Context ctx) throws TestFailedException + { + System.out.println("IsLambdaExample"); + Log.append("IsLambdaExample"); + + // build lambda x : Int . x + 1 + IntExpr x = (IntExpr) ctx.mkBound(0, ctx.getIntSort()); + Expr body = ctx.mkAdd(x, ctx.mkInt(1)); + Expr lam = ctx.mkLambda(new Sort[]{ctx.getIntSort()}, + new Symbol[]{ctx.mkSymbol("x")}, body); + if (!lam.isLambda()) + throw new TestFailedException(); + + // a regular expression is not a lambda + IntExpr y = ctx.mkIntConst("y"); + if (y.isLambda()) + throw new TestFailedException(); + + System.out.println("IsLambdaExample passed."); + } + public static void main(String[] args) { JavaExample p = new JavaExample(); @@ -2328,6 +2465,12 @@ class JavaExample p.finiteDomainExample(ctx); p.floatingPointExample1(ctx); // core dumps: p.floatingPointExample2(ctx); + p.isGroundExample(ctx); + p.astDepthExample(ctx); + p.arrayArityExample(ctx); + p.recursiveDatatypeExample(ctx); + p.fpNumeralExample(ctx); + p.isLambdaExample(ctx); } { // These examples need proof generation turned on. diff --git a/src/api/java/AST.java b/src/api/java/AST.java index 0257f5294..a31e5ea3b 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -80,6 +80,16 @@ public class AST extends Z3Object implements Comparable return Native.getAstId(getContext().nCtx(), getNativeObject()); } + /** + * The depth of the AST (max nodes on any root-to-leaf path). + * @throws Z3Exception on error + * @return an int + **/ + public int getDepth() + { + return Native.getDepth(getContext().nCtx(), getNativeObject()); + } + /** * Translates (copies) the AST to the Context {@code ctx}. * @param ctx A context diff --git a/src/api/java/ArraySort.java b/src/api/java/ArraySort.java index 3d3ef3041..c52f17866 100644 --- a/src/api/java/ArraySort.java +++ b/src/api/java/ArraySort.java @@ -59,6 +59,16 @@ public class ArraySort extends Sort Native.getArraySortRange(getContext().nCtx(), getNativeObject())); } + /** + * The number of dimensions of the array sort. + * @throws Z3Exception on error + * @return an int + **/ + public int getArity() + { + return Native.getArrayArity(getContext().nCtx(), getNativeObject()); + } + ArraySort(Context ctx, long obj) { super(ctx, obj); diff --git a/src/api/java/DatatypeSort.java b/src/api/java/DatatypeSort.java index 8d7f53c24..92601a4f1 100644 --- a/src/api/java/DatatypeSort.java +++ b/src/api/java/DatatypeSort.java @@ -33,6 +33,17 @@ public class DatatypeSort extends Sort getNativeObject()); } + /** + * Indicates whether the datatype sort is recursive. + * @throws Z3Exception on error + * @return a boolean + **/ + public boolean isRecursive() + { + return Native.isRecursiveDatatypeSort(getContext().nCtx(), + getNativeObject()); + } + /** * The constructors. * diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index b15624871..acfebe5a9 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -306,6 +306,26 @@ public class Expr extends AST return Native.isAlgebraicNumber(getContext().nCtx(), getNativeObject()); } + /** + * Indicates whether the term is ground (contains no free variables). + * @throws Z3Exception on error + * @return a boolean + **/ + public boolean isGround() + { + return Native.isGround(getContext().nCtx(), getNativeObject()); + } + + /** + * Indicates whether the term is a lambda expression. + * @throws Z3Exception on error + * @return a boolean + **/ + public boolean isLambda() + { + return Native.isLambda(getContext().nCtx(), getNativeObject()); + } + /** * Indicates whether the term has Boolean sort. * @throws Z3Exception on error diff --git a/src/api/java/FPExpr.java b/src/api/java/FPExpr.java index c348e6420..660619ac2 100644 --- a/src/api/java/FPExpr.java +++ b/src/api/java/FPExpr.java @@ -32,7 +32,17 @@ public class FPExpr extends Expr * @throws Z3Exception */ public int getSBits() { return ((FPSort)getSort()).getSBits(); } - + + /** + * Indicates whether the floating-point expression is a numeral. + * @throws Z3Exception on error + * @return a boolean + **/ + public boolean isNumeral() + { + return Native.fpaIsNumeral(getContext().nCtx(), getNativeObject()); + } + public FPExpr(Context ctx, long obj) { super(ctx, obj);