General fixups

src/api/java/Constructor.java

@@ -20,7 +20,7 @@
 /**
  * Constructors are used for datatype sorts.
  **/
-public class Constructor<R extends DatatypeSort<?>> extends Z3Object {
+public class Constructor<R> extends Z3Object {
     private final int n;
 
     Constructor(Context ctx, int n, long nativeObj) {
@@ -44,7 +44,7 @@ public int getNumFields()
      * @throws Z3Exception 
      * @throws Z3Exception on error
      **/
-    public FuncDecl<R> ConstructorDecl()
+    public FuncDecl<DatatypeSort<R>> ConstructorDecl()
     {
         Native.LongPtr constructor = new Native.LongPtr();
         Native.LongPtr tester = new Native.LongPtr();
@@ -94,7 +94,7 @@ void addToReferenceQueue() {
         getContext().getConstructorDRQ().storeReference(getContext(), this);
     }
 
-    static Constructor<? extends DatatypeSort<?>> of(Context ctx, Symbol name, Symbol recognizer,
+    static <R> Constructor<R> of(Context ctx, Symbol name, Symbol recognizer,
             Symbol[] fieldNames, Sort[] sorts, int[] sortRefs) {
         int n = AST.arrayLength(fieldNames);
 

src/api/java/ConstructorList.java

@@ -20,7 +20,7 @@
 /**
  * Lists of constructors
  **/
-public class ConstructorList<R extends DatatypeSort<?>> extends Z3Object {
+public class ConstructorList<R> extends Z3Object {
 
     ConstructorList(Context ctx, long obj)
     {

src/api/java/Context.java

@@ -277,21 +277,21 @@ public TupleSort mkTupleSort(Symbol name, Symbol[] fieldNames,
     /**
      * Create a new enumeration sort.
      **/
-    public EnumSort mkEnumSort(Symbol name, Symbol... enumNames)
+    public <R> EnumSort<R> mkEnumSort(Symbol name, Symbol... enumNames)
 
     {
         checkContextMatch(name);
         checkContextMatch(enumNames);
-        return new EnumSort(this, name, enumNames);
+        return new EnumSort<>(this, name, enumNames);
     }
 
     /**
      * Create a new enumeration sort.
      **/
-    public EnumSort mkEnumSort(String name, String... enumNames)
+    public <R> EnumSort<R> mkEnumSort(String name, String... enumNames)
 
     {
-        return new EnumSort(this, mkSymbol(name), mkSymbols(enumNames));
+        return new EnumSort<>(this, mkSymbol(name), mkSymbols(enumNames));
     }
 
     /**
@@ -316,20 +316,20 @@ public <R extends Sort> ListSort<R> mkListSort(String name, R elemSort)
     /**
      * Create a new finite domain sort.
      **/
-    public FiniteDomainSort mkFiniteDomainSort(Symbol name, long size)
+    public <R> FiniteDomainSort<R> mkFiniteDomainSort(Symbol name, long size)
 
     {
         checkContextMatch(name);
-        return new FiniteDomainSort(this, name, size);
+        return new FiniteDomainSort<>(this, name, size);
     }
 
     /**
      * Create a new finite domain sort.
      **/
-    public FiniteDomainSort mkFiniteDomainSort(String name, long size)
+    public <R> FiniteDomainSort<R> mkFiniteDomainSort(String name, long size)
 
     {
-        return new FiniteDomainSort(this, mkSymbol(name), size);
+        return new FiniteDomainSort<>(this, mkSymbol(name), size);
     }
 
     /**
@@ -343,29 +343,26 @@ public FiniteDomainSort mkFiniteDomainSort(String name, long size)
      * an index referring to one of the recursive datatypes that is
      * declared.
      **/
-    public Constructor<?> mkConstructor(Symbol name, Symbol recognizer,
+    public <R> Constructor<R> mkConstructor(Symbol name, Symbol recognizer,
             Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
 
     {
-        return of(this, name, recognizer, fieldNames, sorts,
-                sortRefs);
+        return of(this, name, recognizer, fieldNames, sorts, sortRefs);
     }
 
     /**
      * Create a datatype constructor. 
      **/
-    public Constructor<?> mkConstructor(String name, String recognizer,
+    public <R> Constructor<R> mkConstructor(String name, String recognizer,
             String[] fieldNames, Sort[] sorts, int[] sortRefs)
     {
-        return of(this, mkSymbol(name), mkSymbol(recognizer),
-                mkSymbols(fieldNames), sorts, sortRefs);
+        return of(this, mkSymbol(name), mkSymbol(recognizer), mkSymbols(fieldNames), sorts, sortRefs);
     }
 
     /**
      * Create a new datatype sort.
      **/
-    public <R extends Sort> DatatypeSort<R> mkDatatypeSort(Symbol name, Constructor<DatatypeSort<R>>[] constructors)
-
+    public <R> DatatypeSort<R> mkDatatypeSort(Symbol name, Constructor<R>[] constructors)
     {
         checkContextMatch(name);
         checkContextMatch(constructors);
@@ -375,7 +372,7 @@ public <R extends Sort> DatatypeSort<R> mkDatatypeSort(Symbol name, Constructor<
     /**
      * Create a new datatype sort.
      **/
-    public <R extends Sort> DatatypeSort<R> mkDatatypeSort(String name, Constructor<DatatypeSort<R>>[] constructors)
+    public <R> DatatypeSort<R> mkDatatypeSort(String name, Constructor<R>[] constructors)
 
     {
         checkContextMatch(constructors);
@@ -387,16 +384,15 @@ public <R extends Sort> DatatypeSort<R> mkDatatypeSort(String name, Constructor<
      * @param names names of datatype sorts 
      * @param c list of constructors, one list per sort.
      **/
-    public DatatypeSort<Sort>[] mkDatatypeSorts(Symbol[] names, Constructor<DatatypeSort<Sort>>[][] c)
-
+    public DatatypeSort<Object>[] mkDatatypeSorts(Symbol[] names, Constructor<Object>[][] c)
     {
         checkContextMatch(names);
         int n = names.length;
-        ConstructorList<DatatypeSort<Sort>>[] cla = new ConstructorList[n];
+        ConstructorList<Object>[] cla = new ConstructorList[n];
         long[] n_constr = new long[n];
         for (int i = 0; i < n; i++)
         {
-            Constructor<DatatypeSort<Sort>>[] constructor = c[i];
+            Constructor<Object>[] constructor = c[i];
 
             checkContextMatch(constructor);
             cla[i] = new ConstructorList<>(this, constructor);
@@ -405,7 +401,7 @@ public DatatypeSort<Sort>[] mkDatatypeSorts(Symbol[] names, Constructor<Datatype
         long[] n_res = new long[n];
         Native.mkDatatypes(nCtx(), n, Symbol.arrayToNative(names), n_res,
                 n_constr);
-        DatatypeSort<Sort>[] res = new DatatypeSort[n];
+        DatatypeSort<Object>[] res = new DatatypeSort[n];
         for (int i = 0; i < n; i++)
             res[i] = new DatatypeSort<>(this, n_res[i]);
         return res;
@@ -414,7 +410,7 @@ public DatatypeSort<Sort>[] mkDatatypeSorts(Symbol[] names, Constructor<Datatype
     /**
      * Create mutually recursive data-types. 
      **/
-    public DatatypeSort<Sort>[] mkDatatypeSorts(String[] names, Constructor<DatatypeSort<Sort>>[][] c)
+    public DatatypeSort<Object>[] mkDatatypeSorts(String[] names, Constructor<Object>[][] c)
 
     {
         return mkDatatypeSorts(mkSymbols(names), c);

src/api/java/DatatypeSort.java

@@ -20,7 +20,7 @@
 /**
  * Datatype sorts.
  **/
-public class DatatypeSort<R extends Sort> extends Sort
+public class DatatypeSort<R> extends Sort
 {
     /**
      * The number of constructors of the datatype sort.
@@ -40,10 +40,10 @@ public int getNumConstructors()
      * @throws Z3Exception on error
      **/
     @SuppressWarnings("unchecked")
-    public FuncDecl<R>[] getConstructors()
+    public FuncDecl<DatatypeSort<R>>[] getConstructors()
     {
         int n = getNumConstructors();
-        FuncDecl<R>[] res = new FuncDecl[n];
+        FuncDecl<DatatypeSort<R>>[] res = new FuncDecl[n];
         for (int i = 0; i < n; i++)
             res[i] = new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(
                     getContext().nCtx(), getNativeObject(), i));
@@ -99,7 +99,7 @@ public FuncDecl<?>[][] getAccessors()
         super(ctx, obj);
     }
 
-    DatatypeSort(Context ctx, Symbol name, Constructor<DatatypeSort<R>>[] constructors)
+    DatatypeSort(Context ctx, Symbol name, Constructor<R>[] constructors)
 
     {
         super(ctx, Native.mkDatatype(ctx.nCtx(), name.getNativeObject(),

src/api/java/EnumSort.java

@@ -20,26 +20,27 @@
 /**
  * Enumeration sorts.
  **/
-public class EnumSort extends Sort
+@SuppressWarnings("unchecked")
+public class EnumSort<R> extends Sort
 {
     /**
      * The function declarations of the constants in the enumeration.
      * @throws Z3Exception on error
      **/
-    public FuncDecl<?>[] getConstDecls()
+    public FuncDecl<EnumSort<R>>[] getConstDecls()
     {
         int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
         FuncDecl<?>[] t = new FuncDecl[n];
         for (int i = 0; i < n; i++)
             t[i] = new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), i));
-        return t;
+        return (FuncDecl<EnumSort<R>>[]) t;
     }
 
     /**
      * Retrieves the inx'th constant declaration in the enumeration.
      * @throws Z3Exception on error
      **/
-    public FuncDecl<?> getConstDecl(int inx)
+    public FuncDecl<EnumSort<R>> getConstDecl(int inx)
     {
         return new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), inx));
     }
@@ -49,21 +50,21 @@ public FuncDecl<?> getConstDecl(int inx)
      * @throws Z3Exception on error
      * @return an Expr[]
      **/
-    public Expr<?>[] getConsts()
+    public Expr<EnumSort<R>>[] getConsts()
     {        
         FuncDecl<?>[] cds = getConstDecls();
         Expr<?>[] t = new Expr[cds.length];
         for (int i = 0; i < t.length; i++)
             t[i] = getContext().mkApp(cds[i]);
-        return t;
+        return (Expr<EnumSort<R>>[]) t;
     }
 
     /**
      * Retrieves the inx'th constant in the enumeration.
      * @throws Z3Exception on error
      * @return an Expr
      **/
-    public Expr<?> getConst(int inx)
+    public Expr<EnumSort<R>> getConst(int inx)
     {        
         return getContext().mkApp(getConstDecl(inx));
     }

src/api/java/FiniteDomainExpr.java

@@ -20,7 +20,7 @@
 /**
  * Finite-domain expressions
  **/
-public class FiniteDomainExpr extends Expr<FiniteDomainSort>
+public class FiniteDomainExpr<R> extends Expr<FiniteDomainSort<R>>
 {
     /**
      * Constructor for FiniteDomainExpr

src/api/java/FiniteDomainNum.java

@@ -22,7 +22,7 @@
 /**
  * Finite-domain Numerals
  **/
-public class FiniteDomainNum extends FiniteDomainExpr
+public class FiniteDomainNum<R> extends FiniteDomainExpr<R>
 {
 
     FiniteDomainNum(Context ctx, long obj)

src/api/java/FiniteDomainSort.java

@@ -20,7 +20,7 @@
 /**
  * Finite domain sorts.
  **/
-public class FiniteDomainSort extends Sort
+public class FiniteDomainSort<R> extends Sort
 {
     /**
      * The size of the finite domain sort.