Java type generics

examples/java/JavaExample.java

@@ -599,7 +599,7 @@ void quantifierExample1(Context ctx)
         System.out.println("QuantifierExample");
         Log.append("QuantifierExample");
 
-        Sort[] types = new Sort[3];
+        IntSort[] types = new IntSort[3];
         IntExpr[] xs = new IntExpr[3];
         Symbol[] names = new Symbol[3];
         IntExpr[] vars = new IntExpr[3];
@@ -1398,7 +1398,7 @@ public void bitvectorExample1(Context ctx) throws TestFailedException
         System.out.println("BitvectorExample1");
         Log.append("BitvectorExample1");
 
-        Sort bv_type = ctx.mkBitVecSort(32);
+        BitVecSort bv_type = ctx.mkBitVecSort(32);
         BitVecExpr x = (BitVecExpr) ctx.mkConst("x", bv_type);
         BitVecNum zero = (BitVecNum) ctx.mkNumeral("0", bv_type);
         BitVecNum ten = ctx.mkBV(10, 32);
@@ -1420,7 +1420,7 @@ public void bitvectorExample2(Context ctx) throws TestFailedException
         Log.append("BitvectorExample2");
 
         /* construct x ^ y - 103 == x * y */
-        Sort bv_type = ctx.mkBitVecSort(32);
+        BitVecSort bv_type = ctx.mkBitVecSort(32);
         BitVecExpr x = ctx.mkBVConst("x", 32);
         BitVecExpr y = ctx.mkBVConst("y", 32);
         BitVecExpr x_xor_y = ctx.mkBVXOR(x, y);

src/api/java/AST.java

@@ -204,7 +204,7 @@ static AST create(Context ctx, long obj)
         switch (Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj)))
         {
         case Z3_FUNC_DECL_AST:
-            return new FuncDecl(ctx, obj);
+            return new FuncDecl<>(ctx, obj);
         case Z3_QUANTIFIER_AST:
             return new Quantifier(ctx, obj);
         case Z3_SORT_AST:

src/api/java/ASTVector.java

@@ -126,9 +126,9 @@ public AST[] ToArray()
     /**
      * Translates the AST vector into an Expr[]
      * */
-    public Expr[] ToExprArray() {
+    public Expr<?>[] ToExprArray() {
         int n = size();
-        Expr[] res = new Expr[n];
+        Expr<?>[] res = new Expr[n];
         for (int i = 0; i < n; i++)
             res[i] = Expr.create(getContext(), get(i).getNativeObject());
         return res;    
@@ -161,36 +161,36 @@ public BitVecExpr[] ToBitVecExprArray()
     /**
      * Translates the AST vector into an ArithExpr[]
      * */   
-    public ArithExpr[] ToArithExprExprArray()
+    public ArithExpr<?>[] ToArithExprExprArray()
     {
         int n = size();
-        ArithExpr[] res = new ArithExpr[n];
+        ArithExpr<?>[] res = new ArithExpr[n];
         for (int i = 0; i < n; i++)
-            res[i] = (ArithExpr)Expr.create(getContext(), get(i).getNativeObject());
+            res[i] = (ArithExpr<?>)Expr.create(getContext(), get(i).getNativeObject());
         return res;
     }
 
     /**
      * Translates the AST vector into an ArrayExpr[]
      * */  
-    public ArrayExpr[] ToArrayExprArray()
+    public ArrayExpr<?, ?>[] ToArrayExprArray()
     {
         int n = size();
-        ArrayExpr[] res = new ArrayExpr[n];
+        ArrayExpr<?, ?>[] res = new ArrayExpr[n];
         for (int i = 0; i < n; i++)
-            res[i] = (ArrayExpr)Expr.create(getContext(), get(i).getNativeObject());
+            res[i] = (ArrayExpr<?, ?>)Expr.create(getContext(), get(i).getNativeObject());
         return res;
     }
 
     /**
      * Translates the AST vector into an DatatypeExpr[]
      * */ 
-    public DatatypeExpr[] ToDatatypeExprArray()
+    public DatatypeExpr<?>[] ToDatatypeExprArray()
     {
         int n = size();
-        DatatypeExpr[] res = new DatatypeExpr[n];
+        DatatypeExpr<?>[] res = new DatatypeExpr[n];
         for (int i = 0; i < n; i++)
-            res[i] = (DatatypeExpr)Expr.create(getContext(), get(i).getNativeObject());
+            res[i] = (DatatypeExpr<?>)Expr.create(getContext(), get(i).getNativeObject());
         return res;
     }
 

src/api/java/ArithExpr.java

@@ -20,7 +20,7 @@
 /**
  * Arithmetic expressions (int/real)
  **/
-public class ArithExpr extends Expr
+public class ArithExpr<R extends ArithSort> extends Expr<R>
 {
     /**
      * Constructor for ArithExpr

src/api/java/ArrayExpr.java

@@ -21,7 +21,7 @@
 /**
  * Array expressions
  **/
-public class ArrayExpr extends Expr
+public class ArrayExpr<D extends Sort, R extends Sort> extends Expr<ArraySort<D, R>>
 {
     /**
      * Constructor for ArrayExpr

src/api/java/ArraySort.java

@@ -20,17 +20,18 @@
 /**
  * Array sorts.
  **/
-public class ArraySort extends Sort
+@SuppressWarnings("unchecked")
+public class ArraySort<D extends Sort, R extends Sort> extends Sort
 {
     /**
      * The domain of the array sort.
      * @throws Z3Exception 
      * @throws Z3Exception on error
      * @return a sort
      **/
-    public Sort getDomain()
+    public D getDomain()
     {
-        return Sort.create(getContext(),
+        return (D) Sort.create(getContext(),
                 Native.getArraySortDomain(getContext().nCtx(), getNativeObject()));
     }
 
@@ -40,9 +41,9 @@ public Sort getDomain()
      * @throws Z3Exception on error
      * @return a sort
      **/
-    public Sort getRange()
+    public R getRange()
     {
-        return Sort.create(getContext(),
+        return (R) Sort.create(getContext(),
                 Native.getArraySortRange(getContext().nCtx(), getNativeObject()));
     }
 
@@ -51,13 +52,13 @@ public Sort getRange()
         super(ctx, obj);
     }
 
-    ArraySort(Context ctx, Sort domain, Sort range)
+    ArraySort(Context ctx, D domain, R range)
     {
         super(ctx, Native.mkArraySort(ctx.nCtx(), domain.getNativeObject(),
                 range.getNativeObject()));
     }
 
-    ArraySort(Context ctx, Sort[] domains, Sort range)
+    ArraySort(Context ctx, Sort[] domains, R range)
     {
         super(ctx, Native.mkArraySortN(ctx.nCtx(), domains.length, AST.arrayToNative(domains),
                 range.getNativeObject()));

src/api/java/BitVecExpr.java

@@ -20,7 +20,7 @@
 /**
  * Bit-vector expressions
  **/
-public class BitVecExpr extends Expr
+public class BitVecExpr extends Expr<BitVecSort>
 {
 
     /**

src/api/java/BoolExpr.java

@@ -20,7 +20,7 @@
 /**
  * Boolean expressions
  **/
-public class BoolExpr extends Expr {
+public class BoolExpr extends Expr<BoolSort> {
 
     /**
      * Constructor for BoolExpr

src/api/java/Constructor.java

@@ -44,43 +44,43 @@ public int getNumFields()
      * @throws Z3Exception 
      * @throws Z3Exception on error
      **/
-    public FuncDecl ConstructorDecl()
+    public FuncDecl<?> ConstructorDecl()
     {
         Native.LongPtr constructor = new Native.LongPtr();
         Native.LongPtr tester = new Native.LongPtr();
         long[] accessors = new long[n];
         Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
-        return new FuncDecl(getContext(), constructor.value);         
+        return new FuncDecl<>(getContext(), constructor.value);
     }
 
     /**
      * The function declaration of the tester.
      * @throws Z3Exception 
      * @throws Z3Exception on error
      **/
-    public FuncDecl getTesterDecl()
+    public FuncDecl<BoolSort> getTesterDecl()
     {
         Native.LongPtr constructor = new Native.LongPtr();
         Native.LongPtr tester = new Native.LongPtr();
         long[] accessors = new long[n];
         Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
-        return new FuncDecl(getContext(), tester.value);
+        return new FuncDecl<>(getContext(), tester.value);
     }
 
     /**
      * The function declarations of the accessors
      * @throws Z3Exception 
      * @throws Z3Exception on error
      **/
-    public FuncDecl[] getAccessorDecls()
+    public FuncDecl<?>[] getAccessorDecls()
     {
         Native.LongPtr constructor = new Native.LongPtr();
         Native.LongPtr tester = new Native.LongPtr();
         long[] accessors = new long[n];
         Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
-        FuncDecl[] t = new FuncDecl[n];
+        FuncDecl<?>[] t = new FuncDecl[n];
         for (int i = 0; i < n; i++)
-            t[i] = new FuncDecl(getContext(), accessors[i]); 
+            t[i] = new FuncDecl<>(getContext(), accessors[i]);
         return t;
     }