Java bindings: Force cleaning the queue on context closing.

src/api/java/Context.java

@@ -4017,21 +4017,21 @@ public class Context implements AutoCloseable {
     @Override
     public void close()
     {
-        m_AST_DRQ.clear(this);
+        m_AST_DRQ.forceClear(this);
-        m_ASTMap_DRQ.clear(this);
+        m_ASTMap_DRQ.forceClear(this);
-        m_ASTVector_DRQ.clear(this);
+        m_ASTVector_DRQ.forceClear(this);
-        m_ApplyResult_DRQ.clear(this);
+        m_ApplyResult_DRQ.forceClear(this);
-        m_FuncEntry_DRQ.clear(this);
+        m_FuncEntry_DRQ.forceClear(this);
-        m_FuncInterp_DRQ.clear(this);
+        m_FuncInterp_DRQ.forceClear(this);
-        m_Goal_DRQ.clear(this);
+        m_Goal_DRQ.forceClear(this);
-        m_Model_DRQ.clear(this);
+        m_Model_DRQ.forceClear(this);
-        m_Params_DRQ.clear(this);
+        m_Params_DRQ.forceClear(this);
-        m_Probe_DRQ.clear(this);
+        m_Probe_DRQ.forceClear(this);
-        m_Solver_DRQ.clear(this);
+        m_Solver_DRQ.forceClear(this);
-        m_Optimize_DRQ.clear(this);
+        m_Optimize_DRQ.forceClear(this);
-        m_Statistics_DRQ.clear(this);
+        m_Statistics_DRQ.forceClear(this);
-        m_Tactic_DRQ.clear(this);
+        m_Tactic_DRQ.forceClear(this);
-        m_Fixedpoint_DRQ.clear(this);
+        m_Fixedpoint_DRQ.forceClear(this);
 
         m_boolSort = null;
         m_intSort = null;

src/api/java/Fixedpoint.java

@@ -87,12 +87,11 @@ public class Fixedpoint extends Z3Object
 
     /**
      * Add rule into the fixedpoint solver.
-     * 
+     *
+     * @param name Nullable rule name.
      * @throws Z3Exception
      **/
-    public void addRule(BoolExpr rule, Symbol name)
+    public void addRule(BoolExpr rule, Symbol name) {
-    {
-
         getContext().checkContextMatch(rule);
         Native.fixedpointAddRule(getContext().nCtx(), getNativeObject(),
                 rule.getNativeObject(), AST.getNativeObject(name));
@@ -103,11 +102,10 @@ public class Fixedpoint extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public void addFact(FuncDecl pred, int ... args)
+    public void addFact(FuncDecl pred, int ... args) {
-    {
         getContext().checkContextMatch(pred);
         Native.fixedpointAddFact(getContext().nCtx(), getNativeObject(),
-                pred.getNativeObject(), (int) args.length, args);
+                pred.getNativeObject(), args.length, args);
     }
 
     /**
@@ -119,9 +117,7 @@ public class Fixedpoint extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public Status query(BoolExpr query)
+    public Status query(BoolExpr query) {
-    {
-
         getContext().checkContextMatch(query);
         Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQuery(getContext().nCtx(),
                 getNativeObject(), query.getNativeObject()));
@@ -144,9 +140,7 @@ public class Fixedpoint extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public Status query(FuncDecl[] relations)
+    public Status query(FuncDecl[] relations) {
-    {
-
         getContext().checkContextMatch(relations);
         Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQueryRelations(getContext()
                 .nCtx(), getNativeObject(), AST.arrayLength(relations), AST
@@ -166,8 +160,7 @@ public class Fixedpoint extends Z3Object
      * Creates a backtracking point. 
      * @see #pop
      **/
-    public void push()
+    public void push() {
-    {
         Native.fixedpointPush(getContext().nCtx(), getNativeObject());
     }
 
@@ -178,19 +171,17 @@ public class Fixedpoint extends Z3Object
      *  
      * @see #push
      **/
-    public void pop()
+    public void pop() {
-    {
         Native.fixedpointPop(getContext().nCtx(), getNativeObject());
     }
 
     /**
      * Update named rule into in the fixedpoint solver.
-     * 
+     *
+     * @param name Nullable rule name.
      * @throws Z3Exception
      **/
-    public void updateRule(BoolExpr rule, Symbol name)
+    public void updateRule(BoolExpr rule, Symbol name) {
-    {
-
         getContext().checkContextMatch(rule);
         Native.fixedpointUpdateRule(getContext().nCtx(), getNativeObject(),
                 rule.getNativeObject(), AST.getNativeObject(name));

src/api/java/IDecRefQueue.java

@@ -59,6 +59,9 @@ public abstract class IDecRefQueue<T extends Z3Object> {
         clear(ctx);
     }
 
+    /**
+     * Clean all references currently in {@code referenceQueue}.
+     */
     protected void clear(Context ctx)
     {
         Reference<? extends T> ref;
@@ -67,4 +70,14 @@ public abstract class IDecRefQueue<T extends Z3Object> {
             decRef(ctx, z3ast);
         }
     }
+
+    /**
+     * Clean all references stored in {@code referenceMap},
+     * <b>regardless</b> of whether they are in {@code referenceMap} or not.
+     */
+    public void forceClear(Context ctx) {
+        for (long ref : referenceMap.values()) {
+            decRef(ctx, ref);
+        }
+    }
 }

src/api/java/Quantifier.java

@@ -145,20 +145,28 @@ public class Quantifier extends BoolExpr
                 .nCtx(), getNativeObject()));
     }
 
+    /**
+     * Create a quantified expression.
+     *
+     * @param patterns Nullable patterns
+     * @param noPatterns Nullable noPatterns
+     * @param quantifierID Nullable quantifierID
+     * @param skolemID Nullable skolemID
+     */
     public static Quantifier of(
             Context ctx, boolean isForall, Sort[] sorts, Symbol[] names,
             Expr body, int weight, Pattern[] patterns, Expr[] noPatterns,
-            Symbol quantifierID, Symbol skolemID
+            Symbol quantifierID, Symbol skolemID) {
-    ) {
         ctx.checkContextMatch(patterns);
         ctx.checkContextMatch(noPatterns);
         ctx.checkContextMatch(sorts);
         ctx.checkContextMatch(names);
         ctx.checkContextMatch(body);
 
-        if (sorts.length != names.length)
+        if (sorts.length != names.length) {
             throw new Z3Exception(
                     "Number of sorts does not match number of names");
+        }
 
         long nativeObj;
         if (noPatterns == null && quantifierID == null && skolemID == null) {
@@ -180,18 +188,26 @@ public class Quantifier extends BoolExpr
     }
 
 
+    /**
+     * @param ctx Context to create the quantifier on.
+     * @param isForall Quantifier type.
+     * @param bound Bound variables.
+     * @param body Body of the quantifier.
+     * @param weight Weight.
+     * @param patterns Nullable array of patterns.
+     * @param noPatterns Nullable array of noPatterns.
+     * @param quantifierID Nullable quantifier identifier.
+     * @param skolemID Nullable skolem identifier.
+     */
     public static Quantifier of(Context ctx, boolean isForall, Expr[] bound, Expr body,
             int weight, Pattern[] patterns, Expr[] noPatterns,
-            Symbol quantifierID, Symbol skolemID)
+            Symbol quantifierID, Symbol skolemID) {
-    {
         ctx.checkContextMatch(noPatterns);
         ctx.checkContextMatch(patterns);
-        // ctx.CheckContextMatch(bound);
         ctx.checkContextMatch(body);
 
         long nativeObj;
-        if (noPatterns == null && quantifierID == null && skolemID == null)
+        if (noPatterns == null && quantifierID == null && skolemID == null) {
-        {
             nativeObj = Native.mkQuantifierConst(ctx.nCtx(),
                 isForall, weight, AST.arrayLength(bound),
                     AST.arrayToNative(bound), AST.arrayLength(patterns),
@@ -214,11 +230,11 @@ public class Quantifier extends BoolExpr
     }
 
     @Override
-    void checkNativeObject(long obj)
+    void checkNativeObject(long obj) {
-    {
         if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST
-                .toInt())
+                .toInt()) {
             throw new Z3Exception("Underlying object is not a quantifier");
+        }
         super.checkNativeObject(obj);
     }
 }