Replace finalizers with PhantomReferences in Java API

src/api/java/AST.java

@@ -175,15 +175,8 @@ public boolean isFuncDecl()
      * A string representation of the AST.
      **/
     @Override
-    public String toString()
-    {
-        try
-        {
-            return Native.astToString(getContext().nCtx(), getNativeObject());
-        } catch (Z3Exception e)
-        {
-            return "Z3Exception: " + e.getMessage();
-        }
+    public String toString() {
+        return Native.astToString(getContext().nCtx(), getNativeObject());
     }
 
     /**
@@ -194,34 +187,18 @@ public String getSExpr()
         return Native.astToString(getContext().nCtx(), getNativeObject());
     }
 
-    AST(Context ctx)
-    {
-        super(ctx);
-    }
-
-    AST(Context ctx, long obj)
-    {
+    AST(Context ctx, long obj) {
         super(ctx, obj);
     }
 
     @Override
-    void incRef(long o)
-    {
-        // Console.WriteLine("AST IncRef()");
-        if (getContext() == null || o == 0)
-            return;
-        getContext().getASTDRQ().incAndClear(getContext(), o);
-        super.incRef(o);
+    void incRef() {
+        Native.incRef(getContext().nCtx(), getNativeObject());
     }
 
     @Override
-    void decRef(long o)
-    {
-        // Console.WriteLine("AST DecRef()");
-        if (getContext() == null || o == 0)
-            return;
-        getContext().getASTDRQ().add(o);
-        super.decRef(o);
+    void addToReferenceQueue() {
+        getContext().getASTDRQ().storeReference(getContext(), this);
     }
 
     static AST create(Context ctx, long obj)

src/api/java/ASTDecRefQueue.java

@@ -17,7 +17,7 @@
 
 package com.microsoft.z3;
 
-class ASTDecRefQueue extends IDecRefQueue
+class ASTDecRefQueue extends IDecRefQueue<AST>
 {
     public ASTDecRefQueue() 
     {
@@ -30,26 +30,7 @@ public ASTDecRefQueue(int move_limit)
     }
 
     @Override
-    protected void incRef(Context ctx, long obj)
-    {
-        try
-        {
-            Native.incRef(ctx.nCtx(), obj);
-        } catch (Z3Exception e)
-        {
-            // OK.
-        }
-    }
-
-    @Override
-    protected void decRef(Context ctx, long obj)
-    {
-        try
-        {
-            Native.decRef(ctx.nCtx(), obj);
-        } catch (Z3Exception e)
-        {
-            // OK.
-        }
+    protected void decRef(Context ctx, long obj) {
+        Native.decRef(ctx.nCtx(), obj);
     }
 };

src/api/java/ASTMap.java

@@ -20,8 +20,7 @@
 /**
  * Map from AST to AST
  **/
-class ASTMap extends Z3Object
-{
+class ASTMap extends Z3Object {
     /**
      * Checks whether the map contains the key {@code k}. 
      * @param k An AST
@@ -104,13 +103,7 @@ public AST[] getKeys()
     @Override
     public String toString()
     {
-        try
-        {
-            return Native.astMapToString(getContext().nCtx(), getNativeObject());
-        } catch (Z3Exception e)
-        {
-            return "Z3Exception: " + e.getMessage();
-        }
+        return Native.astMapToString(getContext().nCtx(), getNativeObject());
     }
 
     ASTMap(Context ctx, long obj)
@@ -124,16 +117,12 @@ public String toString()
     }
 
     @Override
-    void incRef(long o)
-    {
-        getContext().getASTMapDRQ().incAndClear(getContext(), o);
-        super.incRef(o);
+    void incRef() {
+        Native.astMapIncRef(getContext().nCtx(), getNativeObject());
     }
 
     @Override
-    void decRef(long o)
-    {
-        getContext().getASTMapDRQ().add(o);
-        super.decRef(o);
+    void addToReferenceQueue() {
+        getContext().getASTMapDRQ().storeReference(getContext(), this);
     }
 }

src/api/java/ASTVector.java

@@ -20,8 +20,7 @@
 /**
  * Vectors of ASTs.
  **/
-public class ASTVector extends Z3Object
-{
+public class ASTVector extends Z3Object {
     /**
      * The size of the vector
      **/
@@ -88,15 +87,8 @@ public ASTVector translate(Context ctx)
      * Retrieves a string representation of the vector.
      **/
     @Override
-    public String toString()
-    {
-        try
-        {
-            return Native.astVectorToString(getContext().nCtx(), getNativeObject());
-        } catch (Z3Exception e)
-        {
-            return "Z3Exception: " + e.getMessage();
-        }
+    public String toString() {
+        return Native.astVectorToString(getContext().nCtx(), getNativeObject());
     }
 
     ASTVector(Context ctx, long obj)
@@ -110,19 +102,15 @@ public String toString()
     }
 
     @Override
-    void incRef(long o)
-    {
-        getContext().getASTVectorDRQ().incAndClear(getContext(), o);
-        super.incRef(o);
+    void incRef() {
+        Native.astVectorIncRef(getContext().nCtx(), getNativeObject());
     }
 
     @Override
-    void decRef(long o)
-    {
-        getContext().getASTVectorDRQ().add(o);
-        super.decRef(o);
+    void addToReferenceQueue() {
+        getContext().getASTVectorDRQ().storeReference(getContext(), this);
     }
-    
+
     /**
      * Translates the AST vector into an AST[]
      * */

src/api/java/ApplyResult.java

@@ -21,8 +21,7 @@
  * ApplyResult objects represent the result of an application of a tactic to a
  * goal. It contains the subgoals that were produced.
  **/
-public class ApplyResult extends Z3Object
-{
+public class ApplyResult extends Z3Object {
     /**
      * The number of Subgoals.
      **/
@@ -64,15 +63,8 @@ public Model convertModel(int i, Model m)
      * A string representation of the ApplyResult.
      **/
     @Override
-    public String toString()
-    {
-        try
-        {
-            return Native.applyResultToString(getContext().nCtx(), getNativeObject());
-        } catch (Z3Exception e)
-        {
-            return "Z3Exception: " + e.getMessage();
-        }
+    public String toString() {
+        return Native.applyResultToString(getContext().nCtx(), getNativeObject());
     }
 
     ApplyResult(Context ctx, long obj)
@@ -81,16 +73,12 @@ public String toString()
     }
 
     @Override
-    void incRef(long o)
-    {
-        getContext().getApplyResultDRQ().incAndClear(getContext(), o);
-        super.incRef(o);
+    void incRef() {
+        Native.applyResultIncRef(getContext().nCtx(), getNativeObject());
     }
 
     @Override
-    void decRef(long o)
-    {
-        getContext().getApplyResultDRQ().add(o);
-        super.decRef(o);
+    void addToReferenceQueue() {
+        getContext().getApplyResultDRQ().storeReference(getContext(), this);
     }
 }

src/api/java/ApplyResultDecRefQueue.java

@@ -17,7 +17,7 @@
 
 package com.microsoft.z3;
 
-class ApplyResultDecRefQueue extends IDecRefQueue
+class ApplyResultDecRefQueue extends IDecRefQueue<ApplyResult>
 {
     public ApplyResultDecRefQueue() 
     {
@@ -30,26 +30,7 @@ public ApplyResultDecRefQueue(int move_limit)
     }
 
     @Override
-    protected void incRef(Context ctx, long obj)
-    {
-        try
-        {
-            Native.applyResultIncRef(ctx.nCtx(), obj);
-        } catch (Z3Exception e)
-        {
-            // OK.
-        }
-    }
-
-    @Override
-    protected void decRef(Context ctx, long obj)
-    {
-        try
-        {
-            Native.applyResultDecRef(ctx.nCtx(), obj);
-        } catch (Z3Exception e)
-        {
-            // OK.
-        }
+    protected void decRef(Context ctx, long obj) {
+        Native.applyResultDecRef(ctx.nCtx(), obj);
     }
 };

src/api/java/AstMapDecRefQueue.java

@@ -17,7 +17,7 @@
 
 package com.microsoft.z3;
 
-class ASTMapDecRefQueue extends IDecRefQueue
+class ASTMapDecRefQueue extends IDecRefQueue<ASTMap>
 {
     public ASTMapDecRefQueue() 
     {
@@ -30,26 +30,7 @@ public ASTMapDecRefQueue(int move_limit)
     }
 
     @Override
-    protected void incRef(Context ctx, long obj)
-    {
-        try
-        {
-            Native.astMapIncRef(ctx.nCtx(), obj);
-        } catch (Z3Exception e)
-        {
-            // OK.
-        }
-    }
-
-    @Override
-    protected void decRef(Context ctx, long obj)
-    {
-        try
-        {
-            Native.astMapDecRef(ctx.nCtx(), obj);
-        } catch (Z3Exception e)
-        {
-            // OK.
-        }
+    protected void decRef(Context ctx, long obj) {
+        Native.astMapDecRef(ctx.nCtx(), obj);
     }
 };

src/api/java/AstVectorDecRefQueue.java

@@ -17,7 +17,7 @@
 
 package com.microsoft.z3;
 
-class ASTVectorDecRefQueue extends IDecRefQueue
+class ASTVectorDecRefQueue extends IDecRefQueue<ASTVector>
 {
     public ASTVectorDecRefQueue() 
     {
@@ -30,26 +30,7 @@ public ASTVectorDecRefQueue(int move_limit)
     }
 
     @Override
-    protected void incRef(Context ctx, long obj)
-    {
-        try
-        {
-            Native.astVectorIncRef(ctx.nCtx(), obj);
-        } catch (Z3Exception e)
-        {
-            // OK.
-        }
-    }
-
-    @Override
-    protected void decRef(Context ctx, long obj)
-    {
-        try
-        {
-            Native.astVectorDecRef(ctx.nCtx(), obj);
-        } catch (Z3Exception e)
-        {
-            // OK.
-        }
+    protected void decRef(Context ctx, long obj) {
+        Native.astVectorDecRef(ctx.nCtx(), obj);
     }
 };

src/api/java/BitVecNum.java

@@ -66,13 +66,7 @@ public BigInteger getBigInteger()
     @Override
     public String toString()
     {
-        try
-        {
-            return Native.getNumeralString(getContext().nCtx(), getNativeObject());
-        } catch (Z3Exception e)
-        {
-            return "Z3Exception: " + e.getMessage();
-        }
+        return Native.getNumeralString(getContext().nCtx(), getNativeObject());
     }
 
     BitVecNum(Context ctx, long obj)

src/api/java/BoolExpr.java

@@ -20,15 +20,7 @@
 /**
  * Boolean expressions
  **/
-public class BoolExpr extends Expr
-{
-    /**
-     * Constructor for BoolExpr
-     **/
-    protected BoolExpr(Context ctx)
-    {
-        super(ctx);
-    }
+public class BoolExpr extends Expr {
 
     /**
      * Constructor for BoolExpr