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

@@ -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<IntSort, IntSort> 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<Sort> nil = ctx.mkConstructor("nil", "is_nil", null, null, null);
+        Constructor<Sort> cons = ctx.mkConstructor("cons", "is_cons",
+                new String[]{"head", "tail"},
+                new Sort[]{ctx.getIntSort(), null},
+                new int[]{0, 0});
+        DatatypeSort<Sort> intList = ctx.mkDatatypeSort("intlist", new Constructor[]{nil, cons});
+        if (!intList.isRecursive())
+            throw new TestFailedException();
+
+        // a simple pair sort is not recursive
+        Constructor<Sort> mkPair = ctx.mkConstructor("mkpair", "is_pair",
+                new String[]{"fst", "snd"},
+                new Sort[]{ctx.getIntSort(), ctx.getBoolSort()},
+                null);
+        DatatypeSort<Sort> 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.

src/api/java/AST.java

@@ -80,6 +80,16 @@ public class AST extends Z3Object implements Comparable<AST>
         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

src/api/java/ArraySort.java

@@ -59,6 +59,16 @@ public class ArraySort<D extends Sort, R extends Sort> 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);

src/api/java/DatatypeSort.java

@@ -33,6 +33,17 @@ public class DatatypeSort<R> 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.
      * 

src/api/java/Expr.java

@@ -306,6 +306,26 @@ public class Expr<R extends Sort> 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

src/api/java/FPExpr.java

@@ -32,7 +32,17 @@ public class FPExpr extends Expr<FPSort>
      * @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);