Java type generics

src/api/java/Optimize.java

@@ -24,6 +24,7 @@ Nikolaj Bjorner (nbjorner) 2015-07-16
 /**
  * Object for managing optimization context
  **/
+@SuppressWarnings("unchecked")
 public class Optimize extends Z3Object {
 
     /**
@@ -75,7 +76,7 @@ public void Add(BoolExpr ... constraints)
     /**
      * Handle to objectives returned by objective functions.
      **/
-    public static class Handle {
+    public static class Handle<R extends Sort> {
 
         private final Optimize opt;
         private final int handle;
@@ -89,15 +90,15 @@ public static class Handle {
         /**
          * Retrieve a lower bound for the objective handle.
          **/
-        public Expr getLower()
+        public Expr<R> getLower()
         {
             return opt.GetLower(handle);
         }
 
         /**
          * Retrieve an upper bound for the objective handle.
          **/
-        public Expr getUpper()
+        public Expr<R> getUpper()
         {
             return opt.GetUpper(handle);
         }
@@ -110,7 +111,7 @@ public Expr getUpper()
          * and otherwise is represented by the expression {@code value + eps * EPSILON},
          * where {@code EPSILON} is an arbitrarily small real number.
          */
-        public Expr[] getUpperAsVector()
+        public Expr<?>[] getUpperAsVector()
         {
             return opt.GetUpperAsVector(handle);
         }
@@ -120,15 +121,15 @@ public Expr[] getUpperAsVector()
          *
          * <p>See {@link #getUpperAsVector()} for triple semantics.
          */
-        public Expr[] getLowerAsVector()
+        public Expr<?>[] getLowerAsVector()
         {
             return opt.GetLowerAsVector(handle);
         }
 
         /**
          * Retrieve the value of an objective.
          **/
-        public Expr getValue()
+        public Expr<R> getValue()
         {
             return getLower();
         }
@@ -243,42 +244,42 @@ public BoolExpr[] getUnsatCore()
      *  Return a handle to the objective. The handle is used as
      *  to retrieve the values of objectives after calling Check.
      **/            
-    public Handle MkMaximize(Expr e)
+    public <R extends Sort> Handle<R> MkMaximize(Expr<R> e)
     {
-        return new Handle(this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
+        return new Handle<>(this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
     }
 
     /**
      *  Declare an arithmetical minimization objective. 
      *  Similar to MkMaximize.
      **/
-    public Handle MkMinimize(Expr e)
+    public <R extends Sort> Handle<R> MkMinimize(Expr<R> e)
     {
-        return new Handle(this, Native.optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
+        return new Handle<>(this, Native.optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
     }
 
     /**
      *  Retrieve a lower bound for the objective handle.
      **/
-    private Expr GetLower(int index)
+    private <R extends Sort> Expr<R> GetLower(int index)
     {
-        return Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index));
+        return (Expr<R>) Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index));
     }
 
     /**
      *  Retrieve an upper bound for the objective handle.
      **/
-    private Expr GetUpper(int index)
+    private <R extends Sort> Expr<R> GetUpper(int index)
     {
-        return Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index));
+        return (Expr<R>) Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index));
     }
 
     /**
      * @return Triple representing the upper bound for the objective handle.
      *
      * <p>See {@link Handle#getUpperAsVector}.
      */
-    private Expr[] GetUpperAsVector(int index) {
+    private Expr<?>[] GetUpperAsVector(int index) {
         return unpackObjectiveValueVector(
                 Native.optimizeGetUpperAsVector(
                         getContext().nCtx(), getNativeObject(), index
@@ -291,20 +292,20 @@ private Expr[] GetUpperAsVector(int index) {
      *
      * <p>See {@link Handle#getLowerAsVector}.
      */
-    private Expr[] GetLowerAsVector(int index) {
+    private Expr<?>[] GetLowerAsVector(int index) {
         return unpackObjectiveValueVector(
                 Native.optimizeGetLowerAsVector(
                         getContext().nCtx(), getNativeObject(), index
                 )
         );
     }
 
-    private Expr[] unpackObjectiveValueVector(long nativeVec) {
+    private Expr<?>[] unpackObjectiveValueVector(long nativeVec) {
         ASTVector vec = new ASTVector(
                 getContext(), nativeVec
         );
         return new Expr[] {
-                (Expr) vec.get(0), (Expr) vec.get(1), (Expr) vec.get(2)
+                (Expr<?>) vec.get(0), (Expr<?>) vec.get(1), (Expr<?>) vec.get(2)
         };
 
     }
@@ -355,7 +356,7 @@ public BoolExpr[] getAssertions()
     /**
      * The set of asserted formulas.
      */
-    public Expr[] getObjectives() 
+    public Expr<?>[] getObjectives()
     {
         ASTVector objectives = new ASTVector(getContext(), Native.optimizeGetObjectives(getContext().nCtx(), getNativeObject()));
         return objectives.ToExprArray();