JavaAPI: DecRefQueue -- do not use move_limit for now.

src/api/java/ASTDecRefQueue.java

@@ -24,11 +24,6 @@ class ASTDecRefQueue extends IDecRefQueue<AST>
         super();
     }
 
-    public ASTDecRefQueue(int move_limit) 
-    {
-        super(move_limit);
-    }
-
     @Override
     protected void decRef(Context ctx, long obj) {
         Native.decRef(ctx.nCtx(), obj);

src/api/java/ApplyResultDecRefQueue.java

@@ -24,11 +24,6 @@ class ApplyResultDecRefQueue extends IDecRefQueue<ApplyResult>
         super();
     }
 
-    public ApplyResultDecRefQueue(int move_limit) 
-    {
-        super(move_limit);
-    }
-
     @Override
     protected void decRef(Context ctx, long obj) {
         Native.applyResultDecRef(ctx.nCtx(), obj);

src/api/java/AstMapDecRefQueue.java

@@ -17,20 +17,14 @@ Notes:
 
 package com.microsoft.z3;
 
-class ASTMapDecRefQueue extends IDecRefQueue<ASTMap>
+class ASTMapDecRefQueue extends IDecRefQueue<ASTMap> {
-{
     public ASTMapDecRefQueue() 
     {
         super();
     }
 
-    public ASTMapDecRefQueue(int move_limit) 
-    {
-        super(move_limit);
-    }
-
     @Override
     protected void decRef(Context ctx, long obj) {
         Native.astMapDecRef(ctx.nCtx(), obj);
     }
-};
+}

src/api/java/AstVectorDecRefQueue.java

@@ -17,20 +17,14 @@ Notes:
 
 package com.microsoft.z3;
 
-class ASTVectorDecRefQueue extends IDecRefQueue<ASTVector>
+class ASTVectorDecRefQueue extends IDecRefQueue<ASTVector> {
-{
     public ASTVectorDecRefQueue() 
     {
         super();
     }
 
-    public ASTVectorDecRefQueue(int move_limit) 
-    {
-        super(move_limit);
-    }
-
     @Override
     protected void decRef(Context ctx, long obj) {
         Native.astVectorDecRef(ctx.nCtx(), obj);
     }
-};
+}

src/api/java/ConstructorDecRefQueue.java

@@ -0,0 +1,12 @@
+package com.microsoft.z3;
+
+public class ConstructorDecRefQueue extends IDecRefQueue<Constructor> {
+    public ConstructorDecRefQueue() {
+        super();
+    }
+
+    @Override
+    protected void decRef(Context ctx, long obj) {
+        Native.delConstructor(ctx.nCtx(), obj);
+    }
+}

src/api/java/ConstructorListDecRefQueue.java

@@ -0,0 +1,12 @@
+package com.microsoft.z3;
+
+public class ConstructorListDecRefQueue extends IDecRefQueue<ConstructorList> {
+    public ConstructorListDecRefQueue() {
+        super();
+    }
+
+    @Override
+    protected void decRef(Context ctx, long obj) {
+        Native.delConstructorList(ctx.nCtx(), obj);
+    }
+}

src/api/java/Context.java

@@ -3905,24 +3905,24 @@ public class Context implements AutoCloseable {
     }
 
     private ASTDecRefQueue m_AST_DRQ = new ASTDecRefQueue();
-    private ASTMapDecRefQueue m_ASTMap_DRQ = new ASTMapDecRefQueue(10);
+    private ASTMapDecRefQueue m_ASTMap_DRQ = new ASTMapDecRefQueue();
-    private ASTVectorDecRefQueue m_ASTVector_DRQ = new ASTVectorDecRefQueue(10);
+    private ASTVectorDecRefQueue m_ASTVector_DRQ = new ASTVectorDecRefQueue();
-    private ApplyResultDecRefQueue m_ApplyResult_DRQ = new ApplyResultDecRefQueue(10);
+    private ApplyResultDecRefQueue m_ApplyResult_DRQ = new ApplyResultDecRefQueue();
-    private FuncInterpEntryDecRefQueue m_FuncEntry_DRQ = new FuncInterpEntryDecRefQueue(10);
+    private FuncInterpEntryDecRefQueue m_FuncEntry_DRQ = new FuncInterpEntryDecRefQueue();
-    private FuncInterpDecRefQueue m_FuncInterp_DRQ = new FuncInterpDecRefQueue(10);
+    private FuncInterpDecRefQueue m_FuncInterp_DRQ = new FuncInterpDecRefQueue();
-    private GoalDecRefQueue m_Goal_DRQ = new GoalDecRefQueue(10);
+    private GoalDecRefQueue m_Goal_DRQ = new GoalDecRefQueue();
-    private ModelDecRefQueue m_Model_DRQ = new ModelDecRefQueue(10);
+    private ModelDecRefQueue m_Model_DRQ = new ModelDecRefQueue();
-    private ParamsDecRefQueue m_Params_DRQ = new ParamsDecRefQueue(10);
+    private ParamsDecRefQueue m_Params_DRQ = new ParamsDecRefQueue();
-    private ParamDescrsDecRefQueue m_ParamDescrs_DRQ = new ParamDescrsDecRefQueue(10);
+    private ParamDescrsDecRefQueue m_ParamDescrs_DRQ = new ParamDescrsDecRefQueue();
-    private ProbeDecRefQueue m_Probe_DRQ = new ProbeDecRefQueue(10);
+    private ProbeDecRefQueue m_Probe_DRQ = new ProbeDecRefQueue();
-    private SolverDecRefQueue m_Solver_DRQ = new SolverDecRefQueue(10);
+    private SolverDecRefQueue m_Solver_DRQ = new SolverDecRefQueue();
-    private StatisticsDecRefQueue m_Statistics_DRQ = new StatisticsDecRefQueue(10);
+    private StatisticsDecRefQueue m_Statistics_DRQ = new StatisticsDecRefQueue();
-    private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue(10);
+    private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue();
-    private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue(10);
+    private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue();
-    private OptimizeDecRefQueue m_Optimize_DRQ = new OptimizeDecRefQueue(10);
+    private OptimizeDecRefQueue m_Optimize_DRQ = new OptimizeDecRefQueue();
-    private ConstructorDecRefQueue m_Constructor_DRQ = new ConstructorDecRefQueue(10);
+    private ConstructorDecRefQueue m_Constructor_DRQ = new ConstructorDecRefQueue();
     private ConstructorListDecRefQueue m_ConstructorList_DRQ =
-            new ConstructorListDecRefQueue(10);
+            new ConstructorListDecRefQueue();
 
     public IDecRefQueue<Constructor> getConstructorDRQ() {
         return m_Constructor_DRQ;

src/api/java/FixedpointDecRefQueue.java

@@ -23,11 +23,6 @@ class FixedpointDecRefQueue extends IDecRefQueue<Fixedpoint> {
         super();
     }
 
-    public FixedpointDecRefQueue(int move_limit) 
-    {
-        super(move_limit);
-    }
-
     @Override
     protected void decRef(Context ctx, long obj)
     {

src/api/java/FuncInterpDecRefQueue.java

@@ -24,11 +24,6 @@ class FuncInterpDecRefQueue extends IDecRefQueue<FuncInterp>
         super();
     }
 
-    public FuncInterpDecRefQueue(int move_limit) 
-    {
-        super(move_limit);
-    }
-
     @Override
     protected void decRef(Context ctx, long obj) {
         Native.funcInterpDecRef(ctx.nCtx(), obj);

src/api/java/FuncInterpEntryDecRefQueue.java

@@ -17,20 +17,14 @@ Notes:
 
 package com.microsoft.z3;
 
-class FuncInterpEntryDecRefQueue extends IDecRefQueue<FuncInterp.Entry>
+class FuncInterpEntryDecRefQueue extends IDecRefQueue<FuncInterp.Entry> {
-{
     public FuncInterpEntryDecRefQueue() 
     {
         super();
     }
 
-    public FuncInterpEntryDecRefQueue(int move_limit) 
-    {
-        super(move_limit);
-    }
-
     @Override
     protected void decRef(Context ctx, long obj) {
         Native.funcEntryDecRef(ctx.nCtx(), obj);
     }
-};
+}

src/api/java/GoalDecRefQueue.java

@@ -17,20 +17,14 @@ Notes:
 
 package com.microsoft.z3;
 
-class GoalDecRefQueue extends IDecRefQueue<Goal>
+class GoalDecRefQueue extends IDecRefQueue<Goal> {
-{
     public GoalDecRefQueue() 
     {
         super();
     }
 
-    public GoalDecRefQueue(int move_limit) 
-    {
-        super(move_limit);
-    }
-
     @Override
     protected void decRef(Context ctx, long obj) {
             Native.goalDecRef(ctx.nCtx(), obj);
     }
-};
+}

src/api/java/IDecRefQueue.java

@@ -23,25 +23,16 @@ import java.lang.ref.ReferenceQueue;
 import java.util.IdentityHashMap;
 import java.util.Map;
 
-public abstract class IDecRefQueue<T extends Z3Object>
+/**
-{
+ *
-    private final int m_move_limit;
+ * @param <T>
-
+ */
-    // TODO: problem: ReferenceQueue has no API to return length.
+public abstract class IDecRefQueue<T extends Z3Object> {
     private final ReferenceQueue<T> referenceQueue = new ReferenceQueue<>();
-    private int queueSize = 0;
     private final Map<PhantomReference<T>, Long> referenceMap =
             new IdentityHashMap<>();
 
-    protected IDecRefQueue() 
+    protected IDecRefQueue() {}
-	{
-    	m_move_limit = 1024;
-    }
-
-    protected IDecRefQueue(int move_limit) 
-    {
-    	m_move_limit = move_limit;
-    }
 
     /**
      * An implementation of this method should decrement the reference on a
@@ -56,8 +47,6 @@ public abstract class IDecRefQueue<T extends Z3Object>
     public void storeReference(Context ctx, T obj) {
         PhantomReference<T> ref = new PhantomReference<>(obj, referenceQueue);
         referenceMap.put(ref, obj.getNativeObject());
-
-        // TODO: use move_limit, somehow get the size of referenceQueue.
         clear(ctx);
     }
 

src/api/java/ModelDecRefQueue.java

@@ -17,20 +17,14 @@ Notes:
 
 package com.microsoft.z3;
 
-class ModelDecRefQueue extends IDecRefQueue<Model>
+class ModelDecRefQueue extends IDecRefQueue<Model> {
-{
     public ModelDecRefQueue() 
     {
         super();
     }
 
-    public ModelDecRefQueue(int move_limit) 
-    {
-        super(move_limit);
-    }
-
     @Override
     protected void decRef(Context ctx, long obj) {
         Native.modelDecRef(ctx.nCtx(), obj);
     }
-};
+}

src/api/java/OptimizeDecRefQueue.java

@@ -23,11 +23,6 @@ class OptimizeDecRefQueue extends IDecRefQueue<Optimize> {
         super();
     }
 
-    public OptimizeDecRefQueue(int move_limit) 
-    {
-        super(move_limit);
-    }
-
     @Override
     protected void decRef(Context ctx, long obj) {
         Native.optimizeDecRef(ctx.nCtx(), obj);

src/api/java/ParamDescrsDecRefQueue.java

@@ -17,20 +17,15 @@ Notes:
 
 package com.microsoft.z3;
 
-class ParamDescrsDecRefQueue extends IDecRefQueue<ParamDescrs>
+class ParamDescrsDecRefQueue extends IDecRefQueue<ParamDescrs> {
-{
     public ParamDescrsDecRefQueue() 
     {
         super();
     }
 
-    public ParamDescrsDecRefQueue(int move_limit) {
-        super(move_limit);
-    }
-
     @Override
     protected void decRef(Context ctx, long obj)
     {
         Native.paramDescrsDecRef(ctx.nCtx(), obj);
     }
-};
+}

src/api/java/ParamsDecRefQueue.java

@@ -17,20 +17,14 @@ Notes:
 
 package com.microsoft.z3;
 
-class ParamsDecRefQueue extends IDecRefQueue<Params>
+class ParamsDecRefQueue extends IDecRefQueue<Params> {
-{
     public ParamsDecRefQueue() 
     {
         super();
     }
 
-    public ParamsDecRefQueue(int move_limit) 
-    {
-        super(move_limit);
-    }
-
     @Override
     protected void decRef(Context ctx, long obj) {
         Native.paramsDecRef(ctx.nCtx(), obj);
     }
-};
+}

src/api/java/ProbeDecRefQueue.java

@@ -24,11 +24,6 @@ class ProbeDecRefQueue extends IDecRefQueue<Probe>
         super();
     }
 
-    public ProbeDecRefQueue(int move_limit) 
-    {
-        super(move_limit);
-    }
-
     @Override
     protected void decRef(Context ctx, long obj)
     {

src/api/java/SolverDecRefQueue.java

@@ -17,17 +17,11 @@ Notes:
 
 package com.microsoft.z3;
 
-class SolverDecRefQueue extends IDecRefQueue<Solver>
+class SolverDecRefQueue extends IDecRefQueue<Solver> {
-{
     public SolverDecRefQueue() { super(); }
     
-    public SolverDecRefQueue(int move_limit) 
-    {
-        super(move_limit);
-    }
-
     @Override
     protected void decRef(Context ctx, long obj) {
         Native.solverDecRef(ctx.nCtx(), obj);
     }
-};
+}

src/api/java/StatisticsDecRefQueue.java

@@ -17,20 +17,14 @@ Notes:
 
 package com.microsoft.z3;
 
-class StatisticsDecRefQueue extends IDecRefQueue<Statistics>
+class StatisticsDecRefQueue extends IDecRefQueue<Statistics> {
-{
     public StatisticsDecRefQueue() 
     {
         super();
     }
 
-    public StatisticsDecRefQueue(int move_limit) 
-    {
-        super(move_limit);
-    }
-
     @Override
     protected void decRef(Context ctx, long obj) {
         Native.statsDecRef(ctx.nCtx(), obj);
     }
-};
+}

src/api/java/TacticDecRefQueue.java

@@ -23,11 +23,6 @@ class TacticDecRefQueue extends IDecRefQueue<Tactic> {
         super();
     }
 
-    public TacticDecRefQueue(int move_limit) 
-    {
-        super(move_limit);
-    }
-
     @Override
     protected void decRef(Context ctx, long obj)
     {