From cb87991d5fd70efb257f9ade0a22ecb085025d9e Mon Sep 17 00:00:00 2001 From: George Karpenkov 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 { clear(ctx); } + /** + * Clean all references currently in {@code referenceQueue}. + */ protected void clear(Context ctx) { Reference ref; @@ -67,4 +70,14 @@ public abstract class IDecRefQueue { decRef(ctx, z3ast); } } + + /** + * Clean all references stored in {@code referenceMap}, + * regardless 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); } }