Java API: split incRef into incRef and addToReferenceQueue

One method should do one thing only, it's easy to mix things up
otherwise.

src/api/java/AST.java

@@ -192,9 +192,12 @@ public class AST extends Z3Object implements Comparable<AST>
     }
 
     @Override
-    void incRef(long o)
+    void incRef() {
-    {
+        Native.incRef(getContext().nCtx(), getNativeObject());
-        Native.incRef(getContext().nCtx(), o);
+    }
+
+    @Override
+    void addToReferenceQueue() {
         getContext().getASTDRQ().storeReference(getContext(), this);
     }
 

src/api/java/ASTMap.java

@@ -20,8 +20,7 @@ package com.microsoft.z3;
 /**
  * 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
@@ -118,9 +117,12 @@ class ASTMap extends Z3Object
     }
 
     @Override
-    void incRef(long o)
+    void incRef() {
-    {
+        Native.astMapIncRef(getContext().nCtx(), getNativeObject());
-        Native.astMapIncRef(getContext().nCtx(), o);
+    }
+
+    @Override
+    void addToReferenceQueue() {
         getContext().getASTMapDRQ().storeReference(getContext(), this);
     }
 }

src/api/java/ASTVector.java

@@ -20,8 +20,7 @@ package com.microsoft.z3;
 /**
  * Vectors of ASTs.
  **/
-public class ASTVector extends Z3Object
+public class ASTVector extends Z3Object {
-{
     /**
      * The size of the vector
      **/
@@ -103,9 +102,12 @@ public class ASTVector extends Z3Object
     }
 
     @Override
-    void incRef(long o)
+    void incRef() {
-    {
+        Native.astVectorIncRef(getContext().nCtx(), getNativeObject());
-        Native.astVectorIncRef(getContext().nCtx(), o);
+    }
+
+    @Override
+    void addToReferenceQueue() {
         getContext().getASTVectorDRQ().storeReference(getContext(), this);
     }
 

src/api/java/ApplyResult.java

@@ -21,8 +21,7 @@ package com.microsoft.z3;
  * 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.
      **/
@@ -74,8 +73,12 @@ public class ApplyResult extends Z3Object
     }
 
     @Override
-    void incRef(long o) {
+    void incRef() {
-        Native.applyResultIncRef(getContext().nCtx(), o);
+        Native.applyResultIncRef(getContext().nCtx(), getNativeObject());
+    }
+
+    @Override
+    void addToReferenceQueue() {
         getContext().getApplyResultDRQ().storeReference(getContext(), this);
     }
 }

src/api/java/Constructor.java

@@ -85,9 +85,12 @@ public class Constructor extends Z3Object {
     }
 
     @Override
-    void incRef(long o) {
+    void incRef() {
-
         // Datatype constructors are not reference counted.
+    }
+
+    @Override
+    void addToReferenceQueue() {
         getContext().getConstructorDRQ().storeReference(getContext(), this);
     }
 

src/api/java/ConstructorList.java

@@ -28,7 +28,12 @@ public class ConstructorList extends Z3Object {
     }
 
     @Override
-    void incRef(long o) {
+    void incRef() {
+        // Constructor lists are not reference counted.
+    }
+
+    @Override
+    void addToReferenceQueue() {
         getContext().getConstructorListDRQ().storeReference(getContext(), this);
     }
 

src/api/java/Fixedpoint.java

@@ -349,8 +349,12 @@ public class Fixedpoint extends Z3Object
     }
 
     @Override
-    void incRef(long o) {
+    void incRef() {
-        Native.fixedpointIncRef(getContext().nCtx(), o);
+        Native.fixedpointIncRef(getContext().nCtx(), getNativeObject());
+    }
+
+    @Override
+    void addToReferenceQueue() {
         getContext().getFixedpointDRQ().storeReference(getContext(), this);
     }
 

src/api/java/FixedpointDecRefQueue.java

@@ -17,8 +17,7 @@ Notes:
 
 package com.microsoft.z3;
 
-class FixedpointDecRefQueue extends IDecRefQueue<Fixedpoint>
+class FixedpointDecRefQueue extends IDecRefQueue<Fixedpoint> {
-{
     public FixedpointDecRefQueue() 
     {
         super();
@@ -29,7 +28,6 @@ class FixedpointDecRefQueue extends IDecRefQueue<Fixedpoint>
         super(move_limit);
     }
 
-
     @Override
     protected void decRef(Context ctx, long obj)
     {

src/api/java/FuncInterp.java

@@ -22,8 +22,8 @@ package com.microsoft.z3;
  * Each entry in the finite map represents the value of a function given a set
  * of arguments.
  **/
-public class FuncInterp extends Z3Object
+public class FuncInterp extends Z3Object {
-{
+
     /**
      * An Entry object represents an element in the finite map used to encode a
      * function interpretation.
@@ -32,10 +32,10 @@ public class FuncInterp extends Z3Object
 
         /**
          * Return the (symbolic) value of this entry.
-         * 
+         *
          * @throws Z3Exception
          * @throws Z3Exception on error
-     **/
+         **/
         public Expr getValue()
         {
             return Expr.create(getContext(),
@@ -45,7 +45,7 @@ public class FuncInterp extends Z3Object
         /**
          * The number of arguments of the entry.
          * @throws Z3Exception on error
-     **/
+         **/
         public int getNumArgs()
         {
             return Native.funcEntryGetNumArgs(getContext().nCtx(), getNativeObject());
@@ -53,10 +53,10 @@ public class FuncInterp extends Z3Object
 
         /**
          * The arguments of the function entry.
-         * 
+         *
          * @throws Z3Exception
          * @throws Z3Exception on error
-     **/
+         **/
         public Expr[] getArgs()
         {
             int n = getNumArgs();
@@ -81,14 +81,17 @@ public class FuncInterp extends Z3Object
             return res + getValue() + "]";
         }
 
-        Entry(Context ctx, long obj)
+        Entry(Context ctx, long obj) {
-        {
             super(ctx, obj);
         }
 
         @Override
-        void incRef(long o) {
+        void incRef() {
-            Native.funcEntryIncRef(getContext().nCtx(), o);;
+            Native.funcEntryIncRef(getContext().nCtx(), getNativeObject());
+        }
+
+        @Override
+        void addToReferenceQueue() {
             getContext().getFuncEntryDRQ().storeReference(getContext(), this);
         }
     }
@@ -176,8 +179,12 @@ public class FuncInterp extends Z3Object
     }
 
     @Override
-    void incRef(long o) {
+    void incRef() {
-        Native.funcInterpIncRef(getContext().nCtx(), o);
+        Native.funcInterpIncRef(getContext().nCtx(), getNativeObject());
+    }
+
+    @Override
+    void addToReferenceQueue() {
         getContext().getFuncInterpDRQ().storeReference(getContext(), this);
     }
 }

src/api/java/Goal.java

@@ -23,8 +23,7 @@ import com.microsoft.z3.enumerations.Z3_goal_prec;
  * A goal (aka problem). A goal is essentially a set of formulas, that can be
  * solved and/or transformed using tactics and solvers.
  **/
-public class Goal extends Z3Object
+public class Goal extends Z3Object {
-{
     /**
      * The precision of the goal.
      * Remarks:  Goals can be transformed using over
@@ -242,8 +241,12 @@ public class Goal extends Z3Object
     }
 
     @Override
-    void incRef(long o) {
+    void incRef() {
-        Native.goalIncRef(getContext().nCtx(), o);
+        Native.goalIncRef(getContext().nCtx(), getNativeObject());
+    }
+
+    @Override
+    void addToReferenceQueue() {
         getContext().getGoalDRQ().storeReference(getContext(), this);
     }
 }

src/api/java/Model.java

@@ -22,8 +22,7 @@ import com.microsoft.z3.enumerations.Z3_sort_kind;
 /**
  * A Model contains interpretations (assignments) of constants and functions.
  **/
-public class Model extends Z3Object
+public class Model extends Z3Object {
-{
     /**
      * Retrieves the interpretation (the assignment) of {@code a} in
      * the model. 
@@ -293,8 +292,12 @@ public class Model extends Z3Object
     }
 
     @Override
-    void incRef(long o) {
+    void incRef() {
-        Native.modelIncRef(getContext().nCtx(), o);
+        Native.modelIncRef(getContext().nCtx(), getNativeObject());
+    }
+
+    @Override
+    void addToReferenceQueue() {
         getContext().getModelDRQ().storeReference(getContext(), this);
     }
 }

src/api/java/Optimize.java

@@ -266,8 +266,12 @@ public class Optimize extends Z3Object
     }
 
     @Override
-    void incRef(long o) {
+    void incRef() {
-        Native.optimizeIncRef(getContext().nCtx(), o);
+        Native.optimizeIncRef(getContext().nCtx(), getNativeObject());
+    }
+
+    @Override
+    void addToReferenceQueue() {
         getContext().getOptimizeDRQ().storeReference(getContext(), this);
     }
 }

src/api/java/ParamDescrs.java

@@ -22,8 +22,7 @@ import com.microsoft.z3.enumerations.Z3_param_kind;
 /**
  * A ParamDescrs describes a set of parameters.
  **/
-public class ParamDescrs extends Z3Object
+public class ParamDescrs extends Z3Object {
-{
     /**
      * validate a set of parameters.
      **/
@@ -92,8 +91,12 @@ public class ParamDescrs extends Z3Object
     }
 
     @Override
-    void incRef(long o) {
+    void incRef() {
-        Native.paramDescrsIncRef(getContext().nCtx(), o);
+        Native.paramDescrsIncRef(getContext().nCtx(), getNativeObject());
+    }
+
+    @Override
+    void addToReferenceQueue() {
         getContext().getParamDescrsDRQ().storeReference(getContext(), this);
     }
 }

src/api/java/Params.java

@@ -21,8 +21,7 @@ package com.microsoft.z3;
 /**
  * A ParameterSet represents a configuration in the form of Symbol/value pairs.
  **/
-public class Params extends Z3Object
+public class Params extends Z3Object {
-{
     /**
      * Adds a parameter setting.
      **/
@@ -123,9 +122,14 @@ public class Params extends Z3Object
         super(ctx, Native.mkParams(ctx.nCtx()));
     }
 
+
     @Override
-    void incRef(long o) {
+    void incRef() {
-        Native.paramsIncRef(getContext().nCtx(), o);
+        Native.paramsIncRef(getContext().nCtx(), getNativeObject());
+    }
+
+    @Override
+    void addToReferenceQueue() {
         getContext().getParamsDRQ().storeReference(getContext(), this);
     }
 }

src/api/java/Probe.java

@@ -25,8 +25,7 @@ package com.microsoft.z3;
  * also be obtained using the command {@code (help-tactic)} in the SMT 2.0
  * front-end.
  **/
-public class Probe extends Z3Object
+public class Probe extends Z3Object {
-{
     /**
      * Execute the probe over the goal.
      * 
@@ -46,15 +45,17 @@ public class Probe extends Z3Object
         super(ctx, obj);
     }
 
-    Probe(Context ctx, String name)
+    Probe(Context ctx, String name) {
-    {
         super(ctx, Native.mkProbe(ctx.nCtx(), name));
     }
 
     @Override
-    void incRef(long o)
+    void incRef() {
-    {
+        Native.probeIncRef(getContext().nCtx(), getNativeObject());
-        Native.probeIncRef(getContext().nCtx(), o);
+    }
+
+    @Override
+    void addToReferenceQueue() {
         getContext().getProbeDRQ().storeReference(getContext(), this);
     }
 }

src/api/java/Solver.java

@@ -22,8 +22,7 @@ import com.microsoft.z3.enumerations.Z3_lbool;
 /**
  * Solvers.
  **/
-public class Solver extends Z3Object
+public class Solver extends Z3Object {
-{
     /**
      * A string that describes all available solver parameters.
      **/
@@ -154,13 +153,13 @@ public class Solver extends Z3Object
      * using the Boolean constant p.
      * 
      * Remarks: 
-     * This API is an alternative to {@link check} with assumptions for
+     * This API is an alternative to {@link #check} with assumptions for
      * extracting unsat cores.
      * Both APIs can be used in the same solver. The unsat core will contain a
      * combination
-     * of the Boolean variables provided using {@link assertAndTrack}
+     * of the Boolean variables provided using {@link #assertAndTrack}
      * and the Boolean literals
-     * provided using {@link check} with assumptions.
+     * provided using {@link #check} with assumptions.
      */ 
     public void assertAndTrack(BoolExpr constraint, BoolExpr p)
     {
@@ -333,8 +332,12 @@ public class Solver extends Z3Object
     }
 
     @Override
-    void incRef(long o) {
+    void incRef() {
-        Native.solverIncRef(getContext().nCtx(), o);
+        Native.solverIncRef(getContext().nCtx(), getNativeObject());
+    }
+
+    @Override
+    void addToReferenceQueue() {
         getContext().getSolverDRQ().storeReference(getContext(), this);
     }
 }

src/api/java/Statistics.java

@@ -20,8 +20,7 @@ package com.microsoft.z3;
 /**
  * Objects of this class track statistical information about solvers.
  **/
-public class Statistics extends Z3Object
+public class Statistics extends Z3Object {
-{
     /**
      * Statistical data is organized into pairs of [Key, Entry], where every
      * Entry is either a {@code DoubleEntry} or a {@code UIntEntry}
@@ -191,8 +190,12 @@ public class Statistics extends Z3Object
     }
 
     @Override
-    void incRef(long o) {
+    void incRef() {
-        Native.statsIncRef(getContext().nCtx(), o);
         getContext().getStatisticsDRQ().storeReference(getContext(), this);
     }
+
+    @Override
+    void addToReferenceQueue() {
+        Native.statsIncRef(getContext().nCtx(), getNativeObject());
+    }
 }

src/api/java/Symbol.java

@@ -22,8 +22,7 @@ import com.microsoft.z3.enumerations.Z3_symbol_kind;
 /**
  * Symbols are used to name several term and type constructors.
  **/
-public class Symbol extends Z3Object
+public class Symbol extends Z3Object {
-{
     /**
      * The kind of the symbol (int or string)
      **/
@@ -81,7 +80,13 @@ public class Symbol extends Z3Object
     }
 
     @Override
-    void incRef(long o) {
+    void incRef() {
+        // Symbol does not require tracking.
+    }
+
+    @Override
+    void addToReferenceQueue() {
+
         // Symbol does not require tracking.
     }
 

src/api/java/Tactic.java

@@ -24,8 +24,7 @@ package com.microsoft.z3;
  * also be obtained using the command {@code (help-tactic)} in the SMT 2.0
  * front-end.
  **/
-public class Tactic extends Z3Object
+public class Tactic extends Z3Object {
-{
     /**
      * A string containing a description of parameters accepted by the tactic.
      **/
@@ -93,9 +92,12 @@ public class Tactic extends Z3Object
     }
 
     @Override
-    void incRef(long o)
+    void incRef() {
-    {
+        Native.tacticIncRef(getContext().nCtx(), getNativeObject());
-        Native.tacticIncRef(getContext().nCtx(), o);
+    }
+
+    @Override
+    void addToReferenceQueue() {
         getContext().getTacticDRQ().storeReference(getContext(), this);
     }
 }

src/api/java/Z3Object.java

@@ -30,15 +30,20 @@ public abstract class Z3Object {
         m_ctx = ctx;
         checkNativeObject(obj);
         m_n_obj = obj;
-        incRef(obj);
+        incRef();
+        addToReferenceQueue();
     }
 
     /**
-     * Increment reference count on {@code o}.
+     * Add to ReferenceQueue for tracking reachability on the object and
-     *
+     * decreasing the reference count when the object is no longer reachable.
-     * @param o Z3 object.
      */
-    abstract void incRef(long o);
+    abstract void addToReferenceQueue();
+
+    /**
+     * Increment reference count on {@code this}.
+     */
+    abstract void incRef();
 
     /**
      * This function is provided for overriding, and a child class