From a914822346179531cf36c79809e5f01842267c84 Mon Sep 17 00:00:00 2001
From: George Karpenkov <george@metaworld.me>
Date: Mon, 13 Jun 2016 12:18:31 +0200
Subject: [PATCH] JavaAPI: DecRefQueue -- do not use move_limit for now.

---
 src/api/java/ASTDecRefQueue.java             |  5 ---
 src/api/java/ApplyResultDecRefQueue.java     |  5 ---
 src/api/java/AstMapDecRefQueue.java          | 10 ++----
 src/api/java/AstVectorDecRefQueue.java       | 10 ++----
 src/api/java/ConstructorDecRefQueue.java     | 12 +++++++
 src/api/java/ConstructorListDecRefQueue.java | 12 +++++++
 src/api/java/Context.java                    | 34 ++++++++++----------
 src/api/java/FixedpointDecRefQueue.java      |  5 ---
 src/api/java/FuncInterpDecRefQueue.java      |  5 ---
 src/api/java/FuncInterpEntryDecRefQueue.java | 10 ++----
 src/api/java/GoalDecRefQueue.java            | 10 ++----
 src/api/java/IDecRefQueue.java               | 23 ++++---------
 src/api/java/ModelDecRefQueue.java           | 10 ++----
 src/api/java/OptimizeDecRefQueue.java        |  5 ---
 src/api/java/ParamDescrsDecRefQueue.java     |  9 ++----
 src/api/java/ParamsDecRefQueue.java          | 10 ++----
 src/api/java/ProbeDecRefQueue.java           |  5 ---
 src/api/java/SolverDecRefQueue.java          | 10 ++----
 src/api/java/StatisticsDecRefQueue.java      | 10 ++----
 src/api/java/TacticDecRefQueue.java          |  5 ---
 20 files changed, 65 insertions(+), 140 deletions(-)
 create mode 100644 src/api/java/ConstructorDecRefQueue.java
 create mode 100644 src/api/java/ConstructorListDecRefQueue.java

diff --git a/src/api/java/ASTDecRefQueue.java b/src/api/java/ASTDecRefQueue.java
index d462e16d5..b0a6fa217 100644
--- a/src/api/java/ASTDecRefQueue.java
+++ b/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);
diff --git a/src/api/java/ApplyResultDecRefQueue.java b/src/api/java/ApplyResultDecRefQueue.java
index d28ff755e..e1a660781 100644
--- a/src/api/java/ApplyResultDecRefQueue.java
+++ b/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);
diff --git a/src/api/java/AstMapDecRefQueue.java b/src/api/java/AstMapDecRefQueue.java
index 234b7eec4..6c96970b7 100644
--- a/src/api/java/AstMapDecRefQueue.java
+++ b/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);
     }
-};
+}
diff --git a/src/api/java/AstVectorDecRefQueue.java b/src/api/java/AstVectorDecRefQueue.java
index 3a486ee06..e7ce3e33e 100644
--- a/src/api/java/AstVectorDecRefQueue.java
+++ b/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);
     }
-};
+}
diff --git a/src/api/java/ConstructorDecRefQueue.java b/src/api/java/ConstructorDecRefQueue.java
new file mode 100644
index 000000000..5003dde5f
--- /dev/null
+++ b/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);
+    }
+}
diff --git a/src/api/java/ConstructorListDecRefQueue.java b/src/api/java/ConstructorListDecRefQueue.java
new file mode 100644
index 000000000..1a2460731
--- /dev/null
+++ b/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);
+    }
+}
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index e66920441..1e2b5d4fa 100644
--- a/src/api/java/Context.java
+++ b/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 ASTVectorDecRefQueue m_ASTVector_DRQ = new ASTVectorDecRefQueue(10);
-    private ApplyResultDecRefQueue m_ApplyResult_DRQ = new ApplyResultDecRefQueue(10);
-    private FuncInterpEntryDecRefQueue m_FuncEntry_DRQ = new FuncInterpEntryDecRefQueue(10);
-    private FuncInterpDecRefQueue m_FuncInterp_DRQ = new FuncInterpDecRefQueue(10);
-    private GoalDecRefQueue m_Goal_DRQ = new GoalDecRefQueue(10);
-    private ModelDecRefQueue m_Model_DRQ = new ModelDecRefQueue(10);
-    private ParamsDecRefQueue m_Params_DRQ = new ParamsDecRefQueue(10);
-    private ParamDescrsDecRefQueue m_ParamDescrs_DRQ = new ParamDescrsDecRefQueue(10);
-    private ProbeDecRefQueue m_Probe_DRQ = new ProbeDecRefQueue(10);
-    private SolverDecRefQueue m_Solver_DRQ = new SolverDecRefQueue(10);
-    private StatisticsDecRefQueue m_Statistics_DRQ = new StatisticsDecRefQueue(10);
-    private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue(10);
-    private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue(10);
-    private OptimizeDecRefQueue m_Optimize_DRQ = new OptimizeDecRefQueue(10);
-    private ConstructorDecRefQueue m_Constructor_DRQ = new ConstructorDecRefQueue(10);
+    private ASTMapDecRefQueue m_ASTMap_DRQ = new ASTMapDecRefQueue();
+    private ASTVectorDecRefQueue m_ASTVector_DRQ = new ASTVectorDecRefQueue();
+    private ApplyResultDecRefQueue m_ApplyResult_DRQ = new ApplyResultDecRefQueue();
+    private FuncInterpEntryDecRefQueue m_FuncEntry_DRQ = new FuncInterpEntryDecRefQueue();
+    private FuncInterpDecRefQueue m_FuncInterp_DRQ = new FuncInterpDecRefQueue();
+    private GoalDecRefQueue m_Goal_DRQ = new GoalDecRefQueue();
+    private ModelDecRefQueue m_Model_DRQ = new ModelDecRefQueue();
+    private ParamsDecRefQueue m_Params_DRQ = new ParamsDecRefQueue();
+    private ParamDescrsDecRefQueue m_ParamDescrs_DRQ = new ParamDescrsDecRefQueue();
+    private ProbeDecRefQueue m_Probe_DRQ = new ProbeDecRefQueue();
+    private SolverDecRefQueue m_Solver_DRQ = new SolverDecRefQueue();
+    private StatisticsDecRefQueue m_Statistics_DRQ = new StatisticsDecRefQueue();
+    private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue();
+    private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue();
+    private OptimizeDecRefQueue m_Optimize_DRQ = new OptimizeDecRefQueue();
+    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;
diff --git a/src/api/java/FixedpointDecRefQueue.java b/src/api/java/FixedpointDecRefQueue.java
index 3cba67ced..69ed82092 100644
--- a/src/api/java/FixedpointDecRefQueue.java
+++ b/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)
     {
diff --git a/src/api/java/FuncInterpDecRefQueue.java b/src/api/java/FuncInterpDecRefQueue.java
index 136c07b6a..d8715bd0e 100644
--- a/src/api/java/FuncInterpDecRefQueue.java
+++ b/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);
diff --git a/src/api/java/FuncInterpEntryDecRefQueue.java b/src/api/java/FuncInterpEntryDecRefQueue.java
index 8f6741ba0..a4d8a0690 100644
--- a/src/api/java/FuncInterpEntryDecRefQueue.java
+++ b/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);
     }
-};
+}
diff --git a/src/api/java/GoalDecRefQueue.java b/src/api/java/GoalDecRefQueue.java
index 724ec003f..90bad1fb1 100644
--- a/src/api/java/GoalDecRefQueue.java
+++ b/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);
     }
-};
+}
diff --git a/src/api/java/IDecRefQueue.java b/src/api/java/IDecRefQueue.java
index f3cea7249..5a80adf5f 100644
--- a/src/api/java/IDecRefQueue.java
+++ b/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;
-
-    // TODO: problem: ReferenceQueue has no API to return length.
+/**
+ *
+ * @param <T>
+ */
+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() 
-	{
-    	m_move_limit = 1024;
-    }
-
-    protected IDecRefQueue(int move_limit) 
-    {
-    	m_move_limit = move_limit;
-    }
+    protected IDecRefQueue() {}
 
     /**
      * 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);
     }
 
diff --git a/src/api/java/ModelDecRefQueue.java b/src/api/java/ModelDecRefQueue.java
index 6b141078e..f1b7c3fdd 100644
--- a/src/api/java/ModelDecRefQueue.java
+++ b/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);
     }
-};
+}
diff --git a/src/api/java/OptimizeDecRefQueue.java b/src/api/java/OptimizeDecRefQueue.java
index a06165f3e..0acf20068 100644
--- a/src/api/java/OptimizeDecRefQueue.java
+++ b/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);
diff --git a/src/api/java/ParamDescrsDecRefQueue.java b/src/api/java/ParamDescrsDecRefQueue.java
index ab7f4ddd6..ee3257db9 100644
--- a/src/api/java/ParamDescrsDecRefQueue.java
+++ b/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);
     }
-};
+}
diff --git a/src/api/java/ParamsDecRefQueue.java b/src/api/java/ParamsDecRefQueue.java
index b5281ecbc..349713f67 100644
--- a/src/api/java/ParamsDecRefQueue.java
+++ b/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);
     }
-};
+}
diff --git a/src/api/java/ProbeDecRefQueue.java b/src/api/java/ProbeDecRefQueue.java
index 3f78c6288..b25446c0c 100644
--- a/src/api/java/ProbeDecRefQueue.java
+++ b/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)
     {
diff --git a/src/api/java/SolverDecRefQueue.java b/src/api/java/SolverDecRefQueue.java
index 106892fec..efa15d939 100644
--- a/src/api/java/SolverDecRefQueue.java
+++ b/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);
     }
-};
+}
diff --git a/src/api/java/StatisticsDecRefQueue.java b/src/api/java/StatisticsDecRefQueue.java
index fecf52267..ed698e4ca 100644
--- a/src/api/java/StatisticsDecRefQueue.java
+++ b/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);
     }
-};
+}
diff --git a/src/api/java/TacticDecRefQueue.java b/src/api/java/TacticDecRefQueue.java
index 079904175..8f151f25c 100644
--- a/src/api/java/TacticDecRefQueue.java
+++ b/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)
     {