From cb87991d5fd70efb257f9ade0a22ecb085025d9e Mon Sep 17 00:00:00 2001
From: George Karpenkov <george@metaworld.me>
Date: Wed, 29 Jun 2016 13:09:05 +0200
Subject: [PATCH] Java bindings: Force cleaning the queue on context closing.
---
src/api/java/Context.java | 30 +++++++++++++--------------
src/api/java/Fixedpoint.java | 33 +++++++++++------------------
src/api/java/IDecRefQueue.java | 13 ++++++++++++
src/api/java/Quantifier.java | 38 ++++++++++++++++++++++++----------
4 files changed, 67 insertions(+), 47 deletions(-)
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index da924026c..b7656c5da 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -4017,21 +4017,21 @@ public class Context implements AutoCloseable {
@Override
public void close()
{
- m_AST_DRQ.clear(this);
- m_ASTMap_DRQ.clear(this);
- m_ASTVector_DRQ.clear(this);
- m_ApplyResult_DRQ.clear(this);
- m_FuncEntry_DRQ.clear(this);
- m_FuncInterp_DRQ.clear(this);
- m_Goal_DRQ.clear(this);
- m_Model_DRQ.clear(this);
- m_Params_DRQ.clear(this);
- m_Probe_DRQ.clear(this);
- m_Solver_DRQ.clear(this);
- m_Optimize_DRQ.clear(this);
- m_Statistics_DRQ.clear(this);
- m_Tactic_DRQ.clear(this);
- m_Fixedpoint_DRQ.clear(this);
+ m_AST_DRQ.forceClear(this);
+ m_ASTMap_DRQ.forceClear(this);
+ m_ASTVector_DRQ.forceClear(this);
+ m_ApplyResult_DRQ.forceClear(this);
+ m_FuncEntry_DRQ.forceClear(this);
+ m_FuncInterp_DRQ.forceClear(this);
+ m_Goal_DRQ.forceClear(this);
+ m_Model_DRQ.forceClear(this);
+ m_Params_DRQ.forceClear(this);
+ m_Probe_DRQ.forceClear(this);
+ m_Solver_DRQ.forceClear(this);
+ m_Optimize_DRQ.forceClear(this);
+ m_Statistics_DRQ.forceClear(this);
+ m_Tactic_DRQ.forceClear(this);
+ m_Fixedpoint_DRQ.forceClear(this);
m_boolSort = null;
m_intSort = null;
diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java
index 876345f1e..ad6d5a658 100644
--- a/src/api/java/Fixedpoint.java
+++ b/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));
diff --git a/src/api/java/IDecRefQueue.java b/src/api/java/IDecRefQueue.java
index 2deb9c0f9..4b515a3b6 100644
--- a/src/api/java/IDecRefQueue.java
+++ b/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);
+ }
+ }
}
diff --git a/src/api/java/Quantifier.java b/src/api/java/Quantifier.java
index a78277839..bc2537107 100644
--- a/src/api/java/Quantifier.java
+++ b/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);
}
}