mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
Improved Java phantom references (#7131)
* Reworked phantom reference handling. - Replaced IDecRefQueue with a new Z3ReferenceQueue class - Z3ReferenceQueue manages custom subclasses of phantom references in a doubly-linked list - Replaced all subclasses of IDecRefQueue with subclasses of Z3ReferenceQueue.Reference. These custom reference classes are embedded in the class they reference count. - Context now owns a single Z3ReferenceQueue for all types of references. * Made Statistics.Entry a static subclass * Made Context.close idempotent (as recommended) * Update CMakeLists.txt for building the Java API. * Updated CMakeLists.txt again. * Use correct SuppressWarning annotation to silence the compiler * Formatting
This commit is contained in:
Thomas Haas
GitHub
parent
f7691d34fd
commit
a3d00ce356
|
|
@ -19,6 +19,8 @@ package com.microsoft.z3;
|
|||
|
||||
import com.microsoft.z3.enumerations.Z3_ast_kind;
|
||||
|
||||
import java.lang.ref.ReferenceQueue;
|
||||
|
||||
/**
|
||||
* The abstract syntax tree (AST) class.
|
||||
**/
|
||||
|
|
@ -196,7 +198,7 @@ public class AST extends Z3Object implements Comparable<AST>
|
|||
|
||||
@Override
|
||||
void addToReferenceQueue() {
|
||||
getContext().getASTDRQ().storeReference(getContext(), this);
|
||||
getContext().getReferenceQueue().storeReference(this, ASTRef::new);
|
||||
}
|
||||
|
||||
static AST create(Context ctx, long obj)
|
||||
|
|
@ -217,4 +219,16 @@ public class AST extends Z3Object implements Comparable<AST>
|
|||
throw new Z3Exception("Unknown AST kind");
|
||||
}
|
||||
}
|
||||
|
||||
private static class ASTRef extends Z3ReferenceQueue.Reference<AST> {
|
||||
|
||||
private ASTRef(AST referent, ReferenceQueue<Z3Object> q) {
|
||||
super(referent, q);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(Context ctx, long z3Obj) {
|
||||
Native.decRef(ctx.nCtx(), z3Obj);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,31 +0,0 @@
|
|||
/**
|
||||
Copyright (c) 2012-2014 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
ASTDecRefQueue.java
|
||||
|
||||
Abstract:
|
||||
|
||||
Author:
|
||||
|
||||
@author Christoph Wintersteiger (cwinter) 2012-03-15
|
||||
|
||||
Notes:
|
||||
|
||||
**/
|
||||
|
||||
package com.microsoft.z3;
|
||||
|
||||
class ASTDecRefQueue extends IDecRefQueue<AST>
|
||||
{
|
||||
public ASTDecRefQueue()
|
||||
{
|
||||
super();
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj) {
|
||||
Native.decRef(ctx.nCtx(), obj);
|
||||
}
|
||||
};
|
||||
|
|
@ -17,6 +17,8 @@ Notes:
|
|||
|
||||
package com.microsoft.z3;
|
||||
|
||||
import java.lang.ref.ReferenceQueue;
|
||||
|
||||
/**
|
||||
* Map from AST to AST
|
||||
**/
|
||||
|
|
@ -123,6 +125,18 @@ class ASTMap extends Z3Object {
|
|||
|
||||
@Override
|
||||
void addToReferenceQueue() {
|
||||
getContext().getASTMapDRQ().storeReference(getContext(), this);
|
||||
getContext().getReferenceQueue().storeReference(this, ASTMapRef::new);
|
||||
}
|
||||
|
||||
private static class ASTMapRef extends Z3ReferenceQueue.Reference<ASTMap> {
|
||||
|
||||
private ASTMapRef(ASTMap referent, ReferenceQueue<Z3Object> q) {
|
||||
super(referent, q);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(Context ctx, long z3Obj) {
|
||||
Native.astMapDecRef(ctx.nCtx(), z3Obj);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -17,6 +17,8 @@ Notes:
|
|||
|
||||
package com.microsoft.z3;
|
||||
|
||||
import java.lang.ref.ReferenceQueue;
|
||||
|
||||
/**
|
||||
* Vectors of ASTs.
|
||||
**/
|
||||
|
|
@ -101,16 +103,6 @@ public class ASTVector extends Z3Object {
|
|||
super(ctx, Native.mkAstVector(ctx.nCtx()));
|
||||
}
|
||||
|
||||
@Override
|
||||
void incRef() {
|
||||
Native.astVectorIncRef(getContext().nCtx(), getNativeObject());
|
||||
}
|
||||
|
||||
@Override
|
||||
void addToReferenceQueue() {
|
||||
getContext().getASTVectorDRQ().storeReference(getContext(), this);
|
||||
}
|
||||
|
||||
/**
|
||||
* Translates the AST vector into an AST[]
|
||||
* */
|
||||
|
|
@ -241,4 +233,26 @@ public class ASTVector extends Z3Object {
|
|||
res[i] = (RealExpr)Expr.create(getContext(), get(i).getNativeObject());
|
||||
return res;
|
||||
}
|
||||
|
||||
@Override
|
||||
void incRef() {
|
||||
Native.astVectorIncRef(getContext().nCtx(), getNativeObject());
|
||||
}
|
||||
|
||||
@Override
|
||||
void addToReferenceQueue() {
|
||||
getContext().getReferenceQueue().storeReference(this, ASTVectorRef::new);
|
||||
}
|
||||
|
||||
private static class ASTVectorRef extends Z3ReferenceQueue.Reference<ASTVector> {
|
||||
|
||||
private ASTVectorRef(ASTVector referent, ReferenceQueue<Z3Object> q) {
|
||||
super(referent, q);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(Context ctx, long z3Obj) {
|
||||
Native.astVectorDecRef(ctx.nCtx(), z3Obj);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -17,6 +17,8 @@ Notes:
|
|||
|
||||
package com.microsoft.z3;
|
||||
|
||||
import java.lang.ref.ReferenceQueue;
|
||||
|
||||
/**
|
||||
* ApplyResult objects represent the result of an application of a tactic to a
|
||||
* goal. It contains the subgoals that were produced.
|
||||
|
|
@ -66,6 +68,18 @@ public class ApplyResult extends Z3Object {
|
|||
|
||||
@Override
|
||||
void addToReferenceQueue() {
|
||||
getContext().getApplyResultDRQ().storeReference(getContext(), this);
|
||||
getContext().getReferenceQueue().storeReference(this, ApplyResultRef::new);
|
||||
}
|
||||
|
||||
private static class ApplyResultRef extends Z3ReferenceQueue.Reference<ApplyResult> {
|
||||
|
||||
private ApplyResultRef(ApplyResult referent, ReferenceQueue<Z3Object> q) {
|
||||
super(referent, q);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(Context ctx, long z3Obj) {
|
||||
Native.applyResultDecRef(ctx.nCtx(), z3Obj);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,31 +0,0 @@
|
|||
/**
|
||||
Copyright (c) 2012-2014 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
ApplyResultDecRefQueue.java
|
||||
|
||||
Abstract:
|
||||
|
||||
Author:
|
||||
|
||||
@author Christoph Wintersteiger (cwinter) 2012-03-15
|
||||
|
||||
Notes:
|
||||
|
||||
**/
|
||||
|
||||
package com.microsoft.z3;
|
||||
|
||||
class ApplyResultDecRefQueue extends IDecRefQueue<ApplyResult>
|
||||
{
|
||||
public ApplyResultDecRefQueue()
|
||||
{
|
||||
super();
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj) {
|
||||
Native.applyResultDecRef(ctx.nCtx(), obj);
|
||||
}
|
||||
};
|
||||
|
|
@ -1,30 +0,0 @@
|
|||
/**
|
||||
Copyright (c) 2012-2014 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
AstMapDecRefQueue.java
|
||||
|
||||
Abstract:
|
||||
|
||||
Author:
|
||||
|
||||
@author Christoph Wintersteiger (cwinter) 2012-03-15
|
||||
|
||||
Notes:
|
||||
|
||||
**/
|
||||
|
||||
package com.microsoft.z3;
|
||||
|
||||
class ASTMapDecRefQueue extends IDecRefQueue<ASTMap> {
|
||||
public ASTMapDecRefQueue()
|
||||
{
|
||||
super();
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj) {
|
||||
Native.astMapDecRef(ctx.nCtx(), obj);
|
||||
}
|
||||
}
|
||||
|
|
@ -1,30 +0,0 @@
|
|||
/**
|
||||
Copyright (c) 2012-2014 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
AstVectorDecRefQueue.java
|
||||
|
||||
Abstract:
|
||||
|
||||
Author:
|
||||
|
||||
@author Christoph Wintersteiger (cwinter) 2012-03-15
|
||||
|
||||
Notes:
|
||||
|
||||
**/
|
||||
|
||||
package com.microsoft.z3;
|
||||
|
||||
class ASTVectorDecRefQueue extends IDecRefQueue<ASTVector> {
|
||||
public ASTVectorDecRefQueue()
|
||||
{
|
||||
super();
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj) {
|
||||
Native.astVectorDecRef(ctx.nCtx(), obj);
|
||||
}
|
||||
}
|
||||
|
|
@ -91,17 +91,13 @@ add_custom_command(OUTPUT ${Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH}
|
|||
|
||||
set(Z3_JAVA_JAR_SOURCE_FILES
|
||||
AlgebraicNum.java
|
||||
ApplyResultDecRefQueue.java
|
||||
ApplyResult.java
|
||||
ArithExpr.java
|
||||
ArithSort.java
|
||||
ArrayExpr.java
|
||||
ArraySort.java
|
||||
ASTDecRefQueue.java
|
||||
AST.java
|
||||
AstMapDecRefQueue.java
|
||||
ASTMap.java
|
||||
AstVectorDecRefQueue.java
|
||||
ASTVector.java
|
||||
BitVecExpr.java
|
||||
BitVecNum.java
|
||||
|
|
@ -109,9 +105,7 @@ set(Z3_JAVA_JAR_SOURCE_FILES
|
|||
BoolExpr.java
|
||||
BoolSort.java
|
||||
CharSort.java
|
||||
ConstructorDecRefQueue.java
|
||||
Constructor.java
|
||||
ConstructorListDecRefQueue.java
|
||||
ConstructorList.java
|
||||
Context.java
|
||||
DatatypeExpr.java
|
||||
|
|
@ -121,7 +115,6 @@ set(Z3_JAVA_JAR_SOURCE_FILES
|
|||
FiniteDomainExpr.java
|
||||
FiniteDomainNum.java
|
||||
FiniteDomainSort.java
|
||||
FixedpointDecRefQueue.java
|
||||
Fixedpoint.java
|
||||
FPExpr.java
|
||||
FPNum.java
|
||||
|
|
@ -130,13 +123,9 @@ set(Z3_JAVA_JAR_SOURCE_FILES
|
|||
FPRMSort.java
|
||||
FPSort.java
|
||||
FuncDecl.java
|
||||
FuncInterpDecRefQueue.java
|
||||
FuncInterpEntryDecRefQueue.java
|
||||
FuncInterp.java
|
||||
Global.java
|
||||
GoalDecRefQueue.java
|
||||
Goal.java
|
||||
IDecRefQueue.java
|
||||
IntExpr.java
|
||||
IntNum.java
|
||||
IntSort.java
|
||||
|
|
@ -144,16 +133,11 @@ set(Z3_JAVA_JAR_SOURCE_FILES
|
|||
Lambda.java
|
||||
ListSort.java
|
||||
Log.java
|
||||
ModelDecRefQueue.java
|
||||
Model.java
|
||||
OptimizeDecRefQueue.java
|
||||
Optimize.java
|
||||
ParamDescrsDecRefQueue.java
|
||||
ParamDescrs.java
|
||||
ParamsDecRefQueue.java
|
||||
Params.java
|
||||
Pattern.java
|
||||
ProbeDecRefQueue.java
|
||||
Probe.java
|
||||
Quantifier.java
|
||||
RatNum.java
|
||||
|
|
@ -166,16 +150,12 @@ set(Z3_JAVA_JAR_SOURCE_FILES
|
|||
SeqSort.java
|
||||
SetSort.java
|
||||
Simplifier.java
|
||||
SimplifierDecRefQueue.java
|
||||
SolverDecRefQueue.java
|
||||
Solver.java
|
||||
Sort.java
|
||||
StatisticsDecRefQueue.java
|
||||
Statistics.java
|
||||
Status.java
|
||||
StringSymbol.java
|
||||
Symbol.java
|
||||
TacticDecRefQueue.java
|
||||
Tactic.java
|
||||
TupleSort.java
|
||||
UninterpretedSort.java
|
||||
|
|
@ -183,6 +163,7 @@ set(Z3_JAVA_JAR_SOURCE_FILES
|
|||
Version.java
|
||||
Z3Exception.java
|
||||
Z3Object.java
|
||||
Z3ReferenceQueue.java
|
||||
)
|
||||
set(Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH "")
|
||||
foreach (java_src_file ${Z3_JAVA_JAR_SOURCE_FILES})
|
||||
|
|
|
|||
|
|
@ -17,6 +17,8 @@ Notes:
|
|||
|
||||
package com.microsoft.z3;
|
||||
|
||||
import java.lang.ref.ReferenceQueue;
|
||||
|
||||
/**
|
||||
* Constructors are used for datatype sorts.
|
||||
**/
|
||||
|
|
@ -91,7 +93,7 @@ public class Constructor<R> extends Z3Object {
|
|||
|
||||
@Override
|
||||
void addToReferenceQueue() {
|
||||
getContext().getConstructorDRQ().storeReference(getContext(), this);
|
||||
getContext().getReferenceQueue().storeReference(this, ConstructorRef::new);
|
||||
}
|
||||
|
||||
static <R> Constructor<R> of(Context ctx, Symbol name, Symbol recognizer,
|
||||
|
|
@ -114,4 +116,16 @@ public class Constructor<R> extends Z3Object {
|
|||
return new Constructor<>(ctx, n, nativeObj);
|
||||
|
||||
}
|
||||
|
||||
private static class ConstructorRef extends Z3ReferenceQueue.Reference<Constructor<?>> {
|
||||
|
||||
private ConstructorRef(Constructor<?> referent, ReferenceQueue<Z3Object> q) {
|
||||
super(referent, q);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(Context ctx, long z3Obj) {
|
||||
Native.delConstructor(ctx.nCtx(), z3Obj);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,12 +0,0 @@
|
|||
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);
|
||||
}
|
||||
}
|
||||
|
|
@ -17,6 +17,8 @@ Notes:
|
|||
|
||||
package com.microsoft.z3;
|
||||
|
||||
import java.lang.ref.ReferenceQueue;
|
||||
|
||||
/**
|
||||
* Lists of constructors
|
||||
**/
|
||||
|
|
@ -34,7 +36,7 @@ public class ConstructorList<R> extends Z3Object {
|
|||
|
||||
@Override
|
||||
void addToReferenceQueue() {
|
||||
getContext().getConstructorListDRQ().storeReference(getContext(), this);
|
||||
getContext().getReferenceQueue().storeReference(this, ConstructorListRef::new);
|
||||
}
|
||||
|
||||
ConstructorList(Context ctx, Constructor<R>[] constructors)
|
||||
|
|
@ -43,4 +45,16 @@ public class ConstructorList<R> extends Z3Object {
|
|||
constructors.length,
|
||||
Constructor.arrayToNative(constructors)));
|
||||
}
|
||||
|
||||
private static class ConstructorListRef extends Z3ReferenceQueue.Reference<ConstructorList<?>> {
|
||||
|
||||
private ConstructorListRef(ConstructorList<?> referent, ReferenceQueue<Z3Object> q) {
|
||||
super(referent, q);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(Context ctx, long z3Obj) {
|
||||
Native.delConstructorList(ctx.nCtx(), z3Obj);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,12 +0,0 @@
|
|||
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);
|
||||
}
|
||||
}
|
||||
|
|
@ -4319,119 +4319,9 @@ public class Context implements AutoCloseable {
|
|||
checkContextMatch(a);
|
||||
}
|
||||
|
||||
private ASTDecRefQueue m_AST_DRQ = new ASTDecRefQueue();
|
||||
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 SimplifierDecRefQueue m_Simplifier_DRQ = new SimplifierDecRefQueue();
|
||||
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();
|
||||
private Z3ReferenceQueue m_RefQueue = new Z3ReferenceQueue(this);
|
||||
|
||||
public IDecRefQueue<Constructor<?>> getConstructorDRQ() {
|
||||
return m_Constructor_DRQ;
|
||||
}
|
||||
|
||||
public IDecRefQueue<ConstructorList<?>> getConstructorListDRQ() {
|
||||
return m_ConstructorList_DRQ;
|
||||
}
|
||||
|
||||
public IDecRefQueue<AST> getASTDRQ()
|
||||
{
|
||||
return m_AST_DRQ;
|
||||
}
|
||||
|
||||
public IDecRefQueue<ASTMap> getASTMapDRQ()
|
||||
{
|
||||
return m_ASTMap_DRQ;
|
||||
}
|
||||
|
||||
public IDecRefQueue<ASTVector> getASTVectorDRQ()
|
||||
{
|
||||
return m_ASTVector_DRQ;
|
||||
}
|
||||
|
||||
public IDecRefQueue<ApplyResult> getApplyResultDRQ()
|
||||
{
|
||||
return m_ApplyResult_DRQ;
|
||||
}
|
||||
|
||||
public IDecRefQueue<FuncInterp.Entry<?>> getFuncEntryDRQ()
|
||||
{
|
||||
return m_FuncEntry_DRQ;
|
||||
}
|
||||
|
||||
public IDecRefQueue<FuncInterp<?>> getFuncInterpDRQ()
|
||||
{
|
||||
return m_FuncInterp_DRQ;
|
||||
}
|
||||
|
||||
public IDecRefQueue<Goal> getGoalDRQ()
|
||||
{
|
||||
return m_Goal_DRQ;
|
||||
}
|
||||
|
||||
public IDecRefQueue<Model> getModelDRQ()
|
||||
{
|
||||
return m_Model_DRQ;
|
||||
}
|
||||
|
||||
public IDecRefQueue<Params> getParamsDRQ()
|
||||
{
|
||||
return m_Params_DRQ;
|
||||
}
|
||||
|
||||
public IDecRefQueue<ParamDescrs> getParamDescrsDRQ()
|
||||
{
|
||||
return m_ParamDescrs_DRQ;
|
||||
}
|
||||
|
||||
public IDecRefQueue<Probe> getProbeDRQ()
|
||||
{
|
||||
return m_Probe_DRQ;
|
||||
}
|
||||
|
||||
public IDecRefQueue<Solver> getSolverDRQ()
|
||||
{
|
||||
return m_Solver_DRQ;
|
||||
}
|
||||
|
||||
public IDecRefQueue<Statistics> getStatisticsDRQ()
|
||||
{
|
||||
return m_Statistics_DRQ;
|
||||
}
|
||||
|
||||
public IDecRefQueue<Tactic> getTacticDRQ()
|
||||
{
|
||||
return m_Tactic_DRQ;
|
||||
}
|
||||
|
||||
public IDecRefQueue<Simplifier> getSimplifierDRQ()
|
||||
{
|
||||
return m_Simplifier_DRQ;
|
||||
}
|
||||
|
||||
public IDecRefQueue<Fixedpoint> getFixedpointDRQ()
|
||||
{
|
||||
return m_Fixedpoint_DRQ;
|
||||
}
|
||||
|
||||
public IDecRefQueue<Optimize> getOptimizeDRQ()
|
||||
{
|
||||
return m_Optimize_DRQ;
|
||||
}
|
||||
Z3ReferenceQueue getReferenceQueue() { return m_RefQueue; }
|
||||
|
||||
/**
|
||||
* Disposes of the context.
|
||||
|
|
@ -4439,27 +4329,16 @@ public class Context implements AutoCloseable {
|
|||
@Override
|
||||
public void close()
|
||||
{
|
||||
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_Simplifier_DRQ.forceClear(this);
|
||||
m_Fixedpoint_DRQ.forceClear(this);
|
||||
if (m_ctx == 0)
|
||||
return;
|
||||
|
||||
m_RefQueue.forceClear();
|
||||
|
||||
m_boolSort = null;
|
||||
m_intSort = null;
|
||||
m_realSort = null;
|
||||
m_stringSort = null;
|
||||
m_RefQueue = null;
|
||||
|
||||
synchronized (creation_lock) {
|
||||
Native.delContext(m_ctx);
|
||||
|
|
|
|||
|
|
@ -19,6 +19,8 @@ package com.microsoft.z3;
|
|||
|
||||
import com.microsoft.z3.enumerations.Z3_lbool;
|
||||
|
||||
import java.lang.ref.ReferenceQueue;
|
||||
|
||||
/**
|
||||
* Object for managing fixedpoints
|
||||
**/
|
||||
|
|
@ -327,9 +329,18 @@ public class Fixedpoint extends Z3Object
|
|||
|
||||
@Override
|
||||
void addToReferenceQueue() {
|
||||
getContext().getFixedpointDRQ().storeReference(getContext(), this);
|
||||
getContext().getReferenceQueue().storeReference(this, FixedpointRef::new);
|
||||
}
|
||||
|
||||
@Override
|
||||
void checkNativeObject(long obj) { }
|
||||
private static class FixedpointRef extends Z3ReferenceQueue.Reference<Fixedpoint> {
|
||||
|
||||
private FixedpointRef(Fixedpoint referent, ReferenceQueue<Z3Object> q) {
|
||||
super(referent, q);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(Context ctx, long z3Obj) {
|
||||
Native.fixedpointDecRef(ctx.nCtx(), z3Obj);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,31 +0,0 @@
|
|||
/**
|
||||
Copyright (c) 2012-2014 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
FixedpointDecRefQueue.java
|
||||
|
||||
Abstract:
|
||||
|
||||
Author:
|
||||
|
||||
@author Christoph Wintersteiger (cwinter) 2012-03-15
|
||||
|
||||
Notes:
|
||||
|
||||
**/
|
||||
|
||||
package com.microsoft.z3;
|
||||
|
||||
class FixedpointDecRefQueue extends IDecRefQueue<Fixedpoint> {
|
||||
public FixedpointDecRefQueue()
|
||||
{
|
||||
super();
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
Native.fixedpointDecRef(ctx.nCtx(), obj);
|
||||
}
|
||||
};
|
||||
|
|
@ -17,6 +17,8 @@ Notes:
|
|||
|
||||
package com.microsoft.z3;
|
||||
|
||||
import java.lang.ref.ReferenceQueue;
|
||||
|
||||
/**
|
||||
* A function interpretation is represented as a finite map and an 'else' value.
|
||||
* Each entry in the finite map represents the value of a function given a set
|
||||
|
|
@ -93,7 +95,19 @@ public class FuncInterp<R extends Sort> extends Z3Object {
|
|||
|
||||
@Override
|
||||
void addToReferenceQueue() {
|
||||
getContext().getFuncEntryDRQ().storeReference(getContext(), this);
|
||||
getContext().getReferenceQueue().storeReference(this, FuncEntryRef::new);
|
||||
}
|
||||
|
||||
private static class FuncEntryRef extends Z3ReferenceQueue.Reference<Entry<?>> {
|
||||
|
||||
private FuncEntryRef(Entry<?> referent, ReferenceQueue<Z3Object> q) {
|
||||
super(referent, q);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(Context ctx, long z3Obj) {
|
||||
Native.funcEntryDecRef(ctx.nCtx(), z3Obj);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -186,6 +200,18 @@ public class FuncInterp<R extends Sort> extends Z3Object {
|
|||
|
||||
@Override
|
||||
void addToReferenceQueue() {
|
||||
getContext().getFuncInterpDRQ().storeReference(getContext(), this);
|
||||
getContext().getReferenceQueue().storeReference(this, FuncInterpRef::new);
|
||||
}
|
||||
|
||||
private static class FuncInterpRef extends Z3ReferenceQueue.Reference<FuncInterp<?>> {
|
||||
|
||||
private FuncInterpRef(FuncInterp<?> referent, ReferenceQueue<Z3Object> q) {
|
||||
super(referent, q);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(Context ctx, long z3Obj) {
|
||||
Native.funcInterpDecRef(ctx.nCtx(), z3Obj);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,31 +0,0 @@
|
|||
/**
|
||||
Copyright (c) 2012-2014 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
FuncInterpDecRefQueue.java
|
||||
|
||||
Abstract:
|
||||
|
||||
Author:
|
||||
|
||||
@author Christoph Wintersteiger (cwinter) 2012-03-15
|
||||
|
||||
Notes:
|
||||
|
||||
**/
|
||||
|
||||
package com.microsoft.z3;
|
||||
|
||||
class FuncInterpDecRefQueue extends IDecRefQueue<FuncInterp<?>>
|
||||
{
|
||||
public FuncInterpDecRefQueue()
|
||||
{
|
||||
super();
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj) {
|
||||
Native.funcInterpDecRef(ctx.nCtx(), obj);
|
||||
}
|
||||
};
|
||||
|
|
@ -1,30 +0,0 @@
|
|||
/**
|
||||
Copyright (c) 2012-2014 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
FuncInterpEntryDecRefQueue.java
|
||||
|
||||
Abstract:
|
||||
|
||||
Author:
|
||||
|
||||
@author Christoph Wintersteiger (cwinter) 2012-03-15
|
||||
|
||||
Notes:
|
||||
|
||||
**/
|
||||
|
||||
package com.microsoft.z3;
|
||||
|
||||
class FuncInterpEntryDecRefQueue extends IDecRefQueue<FuncInterp.Entry<?>> {
|
||||
public FuncInterpEntryDecRefQueue()
|
||||
{
|
||||
super();
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj) {
|
||||
Native.funcEntryDecRef(ctx.nCtx(), obj);
|
||||
}
|
||||
}
|
||||
|
|
@ -19,6 +19,8 @@ package com.microsoft.z3;
|
|||
|
||||
import com.microsoft.z3.enumerations.Z3_goal_prec;
|
||||
|
||||
import java.lang.ref.ReferenceQueue;
|
||||
|
||||
/**
|
||||
* A goal (aka problem). A goal is essentially a set of formulas, that can be
|
||||
* solved and/or transformed using tactics and solvers.
|
||||
|
|
@ -262,6 +264,18 @@ public class Goal extends Z3Object {
|
|||
|
||||
@Override
|
||||
void addToReferenceQueue() {
|
||||
getContext().getGoalDRQ().storeReference(getContext(), this);
|
||||
getContext().getReferenceQueue().storeReference(this, GoalRef::new);
|
||||
}
|
||||
|
||||
private static class GoalRef extends Z3ReferenceQueue.Reference<Goal> {
|
||||
|
||||
private GoalRef(Goal referent, ReferenceQueue<Z3Object> q) {
|
||||
super(referent, q);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(Context ctx, long z3Obj) {
|
||||
Native.goalDecRef(ctx.nCtx(), z3Obj);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,30 +0,0 @@
|
|||
/**
|
||||
Copyright (c) 2012-2014 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
GoalDecRefQueue.java
|
||||
|
||||
Abstract:
|
||||
|
||||
Author:
|
||||
|
||||
@author Christoph Wintersteiger (cwinter) 2012-03-15
|
||||
|
||||
Notes:
|
||||
|
||||
**/
|
||||
|
||||
package com.microsoft.z3;
|
||||
|
||||
class GoalDecRefQueue extends IDecRefQueue<Goal> {
|
||||
public GoalDecRefQueue()
|
||||
{
|
||||
super();
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj) {
|
||||
Native.goalDecRef(ctx.nCtx(), obj);
|
||||
}
|
||||
}
|
||||
|
|
@ -1,83 +0,0 @@
|
|||
/**
|
||||
Copyright (c) 2012-2014 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
IDecRefQueue.java
|
||||
|
||||
Abstract:
|
||||
|
||||
Author:
|
||||
|
||||
@author Christoph Wintersteiger (cwinter) 2012-03-15
|
||||
|
||||
Notes:
|
||||
|
||||
**/
|
||||
|
||||
package com.microsoft.z3;
|
||||
|
||||
import java.lang.ref.PhantomReference;
|
||||
import java.lang.ref.Reference;
|
||||
import java.lang.ref.ReferenceQueue;
|
||||
import java.util.IdentityHashMap;
|
||||
import java.util.Map;
|
||||
|
||||
/**
|
||||
* A queue to handle management of native memory.
|
||||
*
|
||||
* <p><b>Mechanics: </b>once an object is created, a metadata is stored for it in
|
||||
* {@code referenceMap}, and a {@link PhantomReference} is created with a
|
||||
* reference to {@code referenceQueue}.
|
||||
* Once the object becomes strongly unreachable, the phantom reference gets
|
||||
* added by JVM to the {@code referenceQueue}.
|
||||
* After each object creation, we iterate through the available objects in
|
||||
* {@code referenceQueue} and decrement references for them.
|
||||
*
|
||||
* @param <T> Type of object stored in queue.
|
||||
*/
|
||||
public abstract class IDecRefQueue<T extends Z3Object> {
|
||||
private final ReferenceQueue<T> referenceQueue = new ReferenceQueue<>();
|
||||
private final Map<PhantomReference<T>, Long> referenceMap =
|
||||
new IdentityHashMap<>();
|
||||
|
||||
protected IDecRefQueue() {}
|
||||
|
||||
/**
|
||||
* An implementation of this method should decrement the reference on a
|
||||
* given native object.
|
||||
* This function should always be called on the {@code ctx} thread.
|
||||
*
|
||||
* @param ctx Z3 context.
|
||||
* @param obj Pointer to a Z3 object.
|
||||
*/
|
||||
protected abstract void decRef(Context ctx, long obj);
|
||||
|
||||
public void storeReference(Context ctx, T obj) {
|
||||
PhantomReference<T> ref = new PhantomReference<>(obj, referenceQueue);
|
||||
referenceMap.put(ref, obj.getNativeObject());
|
||||
clear(ctx);
|
||||
}
|
||||
|
||||
/**
|
||||
* Clean all references currently in {@code referenceQueue}.
|
||||
*/
|
||||
protected void clear(Context ctx)
|
||||
{
|
||||
Reference<? extends T> ref;
|
||||
while ((ref = referenceQueue.poll()) != null) {
|
||||
long z3ast = referenceMap.remove(ref);
|
||||
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);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -19,6 +19,8 @@ package com.microsoft.z3;
|
|||
|
||||
import com.microsoft.z3.enumerations.Z3_sort_kind;
|
||||
|
||||
import java.lang.ref.ReferenceQueue;
|
||||
|
||||
/**
|
||||
* A Model contains interpretations (assignments) of constants and functions.
|
||||
**/
|
||||
|
|
@ -296,6 +298,18 @@ public class Model extends Z3Object {
|
|||
|
||||
@Override
|
||||
void addToReferenceQueue() {
|
||||
getContext().getModelDRQ().storeReference(getContext(), this);
|
||||
getContext().getReferenceQueue().storeReference(this, ModelRef::new);
|
||||
}
|
||||
|
||||
private static class ModelRef extends Z3ReferenceQueue.Reference<Model> {
|
||||
|
||||
private ModelRef(Model referent, ReferenceQueue<Z3Object> q) {
|
||||
super(referent, q);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(Context ctx, long z3Obj) {
|
||||
Native.modelDecRef(ctx.nCtx(), z3Obj);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,30 +0,0 @@
|
|||
/**
|
||||
Copyright (c) 2012-2014 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
ModelDecRefQueue.java
|
||||
|
||||
Abstract:
|
||||
|
||||
Author:
|
||||
|
||||
@author Christoph Wintersteiger (cwinter) 2012-03-15
|
||||
|
||||
Notes:
|
||||
|
||||
**/
|
||||
|
||||
package com.microsoft.z3;
|
||||
|
||||
class ModelDecRefQueue extends IDecRefQueue<Model> {
|
||||
public ModelDecRefQueue()
|
||||
{
|
||||
super();
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj) {
|
||||
Native.modelDecRef(ctx.nCtx(), obj);
|
||||
}
|
||||
}
|
||||
|
|
@ -20,6 +20,8 @@ package com.microsoft.z3;
|
|||
|
||||
import com.microsoft.z3.enumerations.Z3_lbool;
|
||||
|
||||
import java.lang.ref.ReferenceQueue;
|
||||
|
||||
|
||||
/**
|
||||
* Object for managing optimization context
|
||||
|
|
@ -421,6 +423,18 @@ public class Optimize extends Z3Object {
|
|||
|
||||
@Override
|
||||
void addToReferenceQueue() {
|
||||
getContext().getOptimizeDRQ().storeReference(getContext(), this);
|
||||
getContext().getReferenceQueue().storeReference(this, OptimizeRef::new);
|
||||
}
|
||||
|
||||
private static class OptimizeRef extends Z3ReferenceQueue.Reference<Optimize> {
|
||||
|
||||
private OptimizeRef(Optimize referent, ReferenceQueue<Z3Object> q) {
|
||||
super(referent, q);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(Context ctx, long z3Obj) {
|
||||
Native.optimizeDecRef(ctx.nCtx(), z3Obj);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,30 +0,0 @@
|
|||
/**
|
||||
Copyright (c) 2012-2015 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
OptimizeDecRefQueue.java
|
||||
|
||||
Abstract:
|
||||
|
||||
Author:
|
||||
|
||||
@author Christoph Wintersteiger (cwinter) 2012-03-15
|
||||
|
||||
Notes:
|
||||
|
||||
**/
|
||||
|
||||
package com.microsoft.z3;
|
||||
|
||||
class OptimizeDecRefQueue extends IDecRefQueue<Optimize> {
|
||||
public OptimizeDecRefQueue()
|
||||
{
|
||||
super();
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj) {
|
||||
Native.optimizeDecRef(ctx.nCtx(), obj);
|
||||
}
|
||||
};
|
||||
|
|
@ -19,6 +19,8 @@ package com.microsoft.z3;
|
|||
|
||||
import com.microsoft.z3.enumerations.Z3_param_kind;
|
||||
|
||||
import java.lang.ref.ReferenceQueue;
|
||||
|
||||
/**
|
||||
* A ParamDescrs describes a set of parameters.
|
||||
**/
|
||||
|
|
@ -97,6 +99,18 @@ public class ParamDescrs extends Z3Object {
|
|||
|
||||
@Override
|
||||
void addToReferenceQueue() {
|
||||
getContext().getParamDescrsDRQ().storeReference(getContext(), this);
|
||||
getContext().getReferenceQueue().storeReference(this, ParamDescrsRef::new);
|
||||
}
|
||||
|
||||
private static class ParamDescrsRef extends Z3ReferenceQueue.Reference<ParamDescrs> {
|
||||
|
||||
private ParamDescrsRef(ParamDescrs referent, ReferenceQueue<Z3Object> q) {
|
||||
super(referent, q);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(Context ctx, long z3Obj) {
|
||||
Native.paramDescrsDecRef(ctx.nCtx(), z3Obj);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,31 +0,0 @@
|
|||
/**
|
||||
Copyright (c) 2012-2014 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
ParamDescrsDecRefQueue.java
|
||||
|
||||
Abstract:
|
||||
|
||||
Author:
|
||||
|
||||
@author Christoph Wintersteiger (cwinter) 2012-03-15
|
||||
|
||||
Notes:
|
||||
|
||||
**/
|
||||
|
||||
package com.microsoft.z3;
|
||||
|
||||
class ParamDescrsDecRefQueue extends IDecRefQueue<ParamDescrs> {
|
||||
public ParamDescrsDecRefQueue()
|
||||
{
|
||||
super();
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
Native.paramDescrsDecRef(ctx.nCtx(), obj);
|
||||
}
|
||||
}
|
||||
|
|
@ -18,6 +18,8 @@ Notes:
|
|||
|
||||
package com.microsoft.z3;
|
||||
|
||||
import java.lang.ref.ReferenceQueue;
|
||||
|
||||
/**
|
||||
* A ParameterSet represents a configuration in the form of Symbol/value pairs.
|
||||
**/
|
||||
|
|
@ -130,6 +132,18 @@ public class Params extends Z3Object {
|
|||
|
||||
@Override
|
||||
void addToReferenceQueue() {
|
||||
getContext().getParamsDRQ().storeReference(getContext(), this);
|
||||
getContext().getReferenceQueue().storeReference(this, ParamsRef::new);
|
||||
}
|
||||
|
||||
private static class ParamsRef extends Z3ReferenceQueue.Reference<Params> {
|
||||
|
||||
private ParamsRef(Params referent, ReferenceQueue<Z3Object> q) {
|
||||
super(referent, q);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(Context ctx, long z3Obj) {
|
||||
Native.paramsDecRef(ctx.nCtx(), z3Obj);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,30 +0,0 @@
|
|||
/**
|
||||
Copyright (c) 2012-2014 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
ParamDecRefQueue.java
|
||||
|
||||
Abstract:
|
||||
|
||||
Author:
|
||||
|
||||
@author Christoph Wintersteiger (cwinter) 2012-03-15
|
||||
|
||||
Notes:
|
||||
|
||||
**/
|
||||
|
||||
package com.microsoft.z3;
|
||||
|
||||
class ParamsDecRefQueue extends IDecRefQueue<Params> {
|
||||
public ParamsDecRefQueue()
|
||||
{
|
||||
super();
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj) {
|
||||
Native.paramsDecRef(ctx.nCtx(), obj);
|
||||
}
|
||||
}
|
||||
|
|
@ -17,6 +17,8 @@ Notes:
|
|||
|
||||
package com.microsoft.z3;
|
||||
|
||||
import java.lang.ref.ReferenceQueue;
|
||||
|
||||
/**
|
||||
* Probes are used to inspect a goal (aka problem) and collect information that
|
||||
* may be used to decide which solver and/or preprocessing step will be used.
|
||||
|
|
@ -56,6 +58,18 @@ public class Probe extends Z3Object {
|
|||
|
||||
@Override
|
||||
void addToReferenceQueue() {
|
||||
getContext().getProbeDRQ().storeReference(getContext(), this);
|
||||
getContext().getReferenceQueue().storeReference(this, ProbeRef::new);
|
||||
}
|
||||
|
||||
private static class ProbeRef extends Z3ReferenceQueue.Reference<Probe> {
|
||||
|
||||
private ProbeRef(Probe referent, ReferenceQueue<Z3Object> q) {
|
||||
super(referent, q);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(Context ctx, long z3Obj) {
|
||||
Native.probeDecRef(ctx.nCtx(), z3Obj);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,32 +0,0 @@
|
|||
/**
|
||||
Copyright (c) 2012-2014 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
ProbeDecRefQueue.java
|
||||
|
||||
Abstract:
|
||||
|
||||
Author:
|
||||
|
||||
@author Christoph Wintersteiger (cwinter) 2012-03-15
|
||||
|
||||
Notes:
|
||||
|
||||
**/
|
||||
|
||||
package com.microsoft.z3;
|
||||
|
||||
class ProbeDecRefQueue extends IDecRefQueue<Probe>
|
||||
{
|
||||
public ProbeDecRefQueue()
|
||||
{
|
||||
super();
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
Native.probeDecRef(ctx.nCtx(), obj);
|
||||
}
|
||||
};
|
||||
|
|
@ -18,6 +18,8 @@ Author:
|
|||
package com.microsoft.z3;
|
||||
|
||||
|
||||
import java.lang.ref.ReferenceQueue;
|
||||
|
||||
public class Simplifier extends Z3Object {
|
||||
/*
|
||||
* A string containing a description of parameters accepted by the simplifier.
|
||||
|
|
@ -32,7 +34,7 @@ public class Simplifier extends Z3Object {
|
|||
* Retrieves parameter descriptions for Simplifiers.
|
||||
*/
|
||||
public ParamDescrs getParameterDescriptions() {
|
||||
return new ParamDescrs(getContext(), Native.simplifierGetParamDescrs(getContext().nCtx(), getNativeObject()));
|
||||
return new ParamDescrs(getContext(), Native.simplifierGetParamDescrs(getContext().nCtx(), getNativeObject()));
|
||||
}
|
||||
|
||||
Simplifier(Context ctx, long obj)
|
||||
|
|
@ -53,6 +55,18 @@ public class Simplifier extends Z3Object {
|
|||
|
||||
@Override
|
||||
void addToReferenceQueue() {
|
||||
getContext().getSimplifierDRQ().storeReference(getContext(), this);
|
||||
getContext().getReferenceQueue().storeReference(this, SimplifierRef::new);
|
||||
}
|
||||
}
|
||||
|
||||
private static class SimplifierRef extends Z3ReferenceQueue.Reference<Simplifier> {
|
||||
|
||||
private SimplifierRef(Simplifier referent, ReferenceQueue<Z3Object> q) {
|
||||
super(referent, q);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(Context ctx, long z3Obj) {
|
||||
Native.simplifierDecRef(ctx.nCtx(), z3Obj);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -1,31 +0,0 @@
|
|||
/**
|
||||
Copyright (c) 2012-2014 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
SimplifierDecRefQueue.java
|
||||
|
||||
Abstract:
|
||||
|
||||
Author:
|
||||
|
||||
@author Christoph Wintersteiger (cwinter) 2012-03-15
|
||||
|
||||
Notes:
|
||||
|
||||
**/
|
||||
|
||||
package com.microsoft.z3;
|
||||
|
||||
class SimplifierDecRefQueue extends IDecRefQueue<Simplifier> {
|
||||
public SimplifierDecRefQueue()
|
||||
{
|
||||
super();
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
Native.simplifierDecRef(ctx.nCtx(), obj);
|
||||
}
|
||||
}
|
||||
|
|
@ -19,6 +19,8 @@ Notes:
|
|||
package com.microsoft.z3;
|
||||
|
||||
import com.microsoft.z3.enumerations.Z3_lbool;
|
||||
|
||||
import java.lang.ref.ReferenceQueue;
|
||||
import java.util.*;
|
||||
|
||||
/**
|
||||
|
|
@ -403,6 +405,18 @@ public class Solver extends Z3Object {
|
|||
|
||||
@Override
|
||||
void addToReferenceQueue() {
|
||||
getContext().getSolverDRQ().storeReference(getContext(), this);
|
||||
getContext().getReferenceQueue().storeReference(this, SolverRef::new);
|
||||
}
|
||||
|
||||
private static class SolverRef extends Z3ReferenceQueue.Reference<Solver> {
|
||||
|
||||
private SolverRef(Solver referent, ReferenceQueue<Z3Object> q) {
|
||||
super(referent, q);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(Context ctx, long z3Obj) {
|
||||
Native.solverDecRef(ctx.nCtx(), z3Obj);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,27 +0,0 @@
|
|||
/**
|
||||
Copyright (c) 2012-2014 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
SolverDecRefQueue.java
|
||||
|
||||
Abstract:
|
||||
|
||||
Author:
|
||||
|
||||
@author Christoph Wintersteiger (cwinter) 2012-03-15
|
||||
|
||||
Notes:
|
||||
|
||||
**/
|
||||
|
||||
package com.microsoft.z3;
|
||||
|
||||
class SolverDecRefQueue extends IDecRefQueue<Solver> {
|
||||
public SolverDecRefQueue() { super(); }
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj) {
|
||||
Native.solverDecRef(ctx.nCtx(), obj);
|
||||
}
|
||||
}
|
||||
|
|
@ -17,6 +17,8 @@ Notes:
|
|||
|
||||
package com.microsoft.z3;
|
||||
|
||||
import java.lang.ref.ReferenceQueue;
|
||||
|
||||
/**
|
||||
* Objects of this class track statistical information about solvers.
|
||||
**/
|
||||
|
|
@ -25,7 +27,7 @@ public class Statistics extends Z3Object {
|
|||
* Statistical data is organized into pairs of [Key, Entry], where every
|
||||
* Entry is either a {@code DoubleEntry} or a {@code UIntEntry}
|
||||
**/
|
||||
public class Entry
|
||||
public static class Entry
|
||||
{
|
||||
/**
|
||||
* The key of the entry.
|
||||
|
|
@ -191,11 +193,23 @@ public class Statistics extends Z3Object {
|
|||
|
||||
@Override
|
||||
void incRef() {
|
||||
getContext().getStatisticsDRQ().storeReference(getContext(), this);
|
||||
Native.statsIncRef(getContext().nCtx(), getNativeObject());
|
||||
}
|
||||
|
||||
@Override
|
||||
void addToReferenceQueue() {
|
||||
Native.statsIncRef(getContext().nCtx(), getNativeObject());
|
||||
getContext().getReferenceQueue().storeReference(this, StatisticsRef::new);
|
||||
}
|
||||
|
||||
private static class StatisticsRef extends Z3ReferenceQueue.Reference<Statistics> {
|
||||
|
||||
private StatisticsRef(Statistics referent, ReferenceQueue<Z3Object> q) {
|
||||
super(referent, q);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(Context ctx, long z3Obj) {
|
||||
Native.statsDecRef(ctx.nCtx(), z3Obj);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,30 +0,0 @@
|
|||
/**
|
||||
Copyright (c) 2012-2014 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
StatisticsDecRefQueue.java
|
||||
|
||||
Abstract:
|
||||
|
||||
Author:
|
||||
|
||||
@author Christoph Wintersteiger (cwinter) 2012-03-15
|
||||
|
||||
Notes:
|
||||
|
||||
**/
|
||||
|
||||
package com.microsoft.z3;
|
||||
|
||||
class StatisticsDecRefQueue extends IDecRefQueue<Statistics> {
|
||||
public StatisticsDecRefQueue()
|
||||
{
|
||||
super();
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj) {
|
||||
Native.statsDecRef(ctx.nCtx(), obj);
|
||||
}
|
||||
}
|
||||
|
|
@ -17,6 +17,8 @@ Notes:
|
|||
|
||||
package com.microsoft.z3;
|
||||
|
||||
import java.lang.ref.ReferenceQueue;
|
||||
|
||||
/**
|
||||
* Tactics are the basic building block for creating custom solvers for specific
|
||||
* problem domains. The complete list of tactics may be obtained using
|
||||
|
|
@ -98,6 +100,19 @@ public class Tactic extends Z3Object {
|
|||
|
||||
@Override
|
||||
void addToReferenceQueue() {
|
||||
getContext().getTacticDRQ().storeReference(getContext(), this);
|
||||
//getContext().getTacticDRQ().storeReference(getContext(), this);
|
||||
getContext().getReferenceQueue().storeReference(this, TacticRef::new);
|
||||
}
|
||||
|
||||
private static class TacticRef extends Z3ReferenceQueue.Reference<Tactic> {
|
||||
|
||||
private TacticRef(Tactic referent, ReferenceQueue<Z3Object> q) {
|
||||
super(referent, q);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(Context ctx, long z3Obj) {
|
||||
Native.tacticDecRef(ctx.nCtx(), z3Obj);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,31 +0,0 @@
|
|||
/**
|
||||
Copyright (c) 2012-2014 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
TacticDecRefQueue.java
|
||||
|
||||
Abstract:
|
||||
|
||||
Author:
|
||||
|
||||
@author Christoph Wintersteiger (cwinter) 2012-03-15
|
||||
|
||||
Notes:
|
||||
|
||||
**/
|
||||
|
||||
package com.microsoft.z3;
|
||||
|
||||
class TacticDecRefQueue extends IDecRefQueue<Tactic> {
|
||||
public TacticDecRefQueue()
|
||||
{
|
||||
super();
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
Native.tacticDecRef(ctx.nCtx(), obj);
|
||||
}
|
||||
}
|
||||
144
src/api/java/Z3ReferenceQueue.java
Normal file
144
src/api/java/Z3ReferenceQueue.java
Normal file
|
|
@ -0,0 +1,144 @@
|
|||
/**
|
||||
Copyright (c) 2012-2014 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
IDecRefQueue.java
|
||||
|
||||
Abstract:
|
||||
|
||||
Author:
|
||||
|
||||
@author Christoph Wintersteiger (cwinter) 2012-03-15
|
||||
|
||||
Notes:
|
||||
|
||||
**/
|
||||
|
||||
package com.microsoft.z3;
|
||||
|
||||
import java.lang.ref.PhantomReference;
|
||||
import java.lang.ref.ReferenceQueue;
|
||||
|
||||
/**
|
||||
* A queue to handle management of native memory.
|
||||
*
|
||||
* <p><b>Mechanics: </b>When an object is created, a so-called {@link PhantomReference}
|
||||
* is constructed that is associated with the created object and the reference queue {@code referenceQueue}.
|
||||
* Once the object becomes strongly unreachable, the phantom reference gets
|
||||
* added by JVM to the {@code referenceQueue}.
|
||||
* After each object creation, we iterate through the available objects in
|
||||
* {@code referenceQueue} and decrement references for them.
|
||||
* <p>
|
||||
* In order for this to work, we need to (i) associate to each phantom reference the underlying
|
||||
* native object (and its type) that it references and (ii) keep the phantom references themselves alive, so they are not
|
||||
* garbage collected before the object they reference.
|
||||
* We use a doubly-linked list of custom phantom references, subclasses of {@link Reference}, to achieve this.
|
||||
*
|
||||
*/
|
||||
class Z3ReferenceQueue {
|
||||
private final Context ctx;
|
||||
private final ReferenceQueue<Z3Object> referenceQueue = new ReferenceQueue<>();
|
||||
private final Reference<?> referenceList = emptyList();
|
||||
|
||||
Z3ReferenceQueue(Context ctx) {
|
||||
this.ctx = ctx;
|
||||
}
|
||||
|
||||
/**
|
||||
* Create and store a new phantom reference.
|
||||
*/
|
||||
<T extends Z3Object> void storeReference(T z3Object, ReferenceConstructor<T> refConstructor) {
|
||||
referenceList.insert(refConstructor.construct(z3Object, referenceQueue));
|
||||
clear();
|
||||
}
|
||||
|
||||
/**
|
||||
* Clean all references currently in {@code referenceQueue}.
|
||||
*/
|
||||
private void clear() {
|
||||
Reference<?> ref;
|
||||
while ((ref = (Reference<?>)referenceQueue.poll()) != null) {
|
||||
ref.cleanup(ctx);
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Clean all references stored in {@code referenceList},
|
||||
* <b>regardless</b> of whether they are in {@code referenceQueue} or not.
|
||||
*/
|
||||
@SuppressWarnings("StatementWithEmptyBody")
|
||||
public void forceClear() {
|
||||
// Decrement all reference counters
|
||||
Reference<?> cur = referenceList.next;
|
||||
while (cur.next != null) {
|
||||
cur.decRef(ctx, cur.nativePtr);
|
||||
cur = cur.next;
|
||||
}
|
||||
|
||||
// Bulk-delete the reference list's entries
|
||||
referenceList.next = cur;
|
||||
cur.prev = referenceList;
|
||||
|
||||
// Empty the reference queue so that there are no living phantom references anymore.
|
||||
// This makes sure that all stored phantom references can be GC'd now.
|
||||
while (referenceQueue.poll() != null) {}
|
||||
}
|
||||
|
||||
private static Reference<?> emptyList() {
|
||||
Reference<?> head = new DummyReference();
|
||||
Reference<?> tail = new DummyReference();
|
||||
head.next = tail;
|
||||
tail.prev = head;
|
||||
return head;
|
||||
}
|
||||
|
||||
// ================================================================================================================
|
||||
|
||||
@FunctionalInterface
|
||||
interface ReferenceConstructor<T extends Z3Object> {
|
||||
Reference<T> construct(T reference, ReferenceQueue<Z3Object> queue);
|
||||
}
|
||||
|
||||
abstract static class Reference<T extends Z3Object> extends PhantomReference<T> {
|
||||
|
||||
private Reference<?> prev;
|
||||
private Reference<?> next;
|
||||
private final long nativePtr;
|
||||
|
||||
Reference(T referent, ReferenceQueue<Z3Object> q) {
|
||||
super(referent, q);
|
||||
this.nativePtr = referent != null ? referent.getNativeObject() : 0;
|
||||
}
|
||||
|
||||
private void cleanup(Context ctx) {
|
||||
decRef(ctx, nativePtr);
|
||||
assert (prev != null && next != null);
|
||||
prev.next = next;
|
||||
next.prev = prev;
|
||||
}
|
||||
|
||||
private void insert(Reference<?> ref) {
|
||||
assert next != null;
|
||||
ref.prev = this;
|
||||
ref.next = this.next;
|
||||
ref.next.prev = ref;
|
||||
next = ref;
|
||||
}
|
||||
|
||||
abstract void decRef(Context ctx, long z3Obj);
|
||||
}
|
||||
|
||||
private static class DummyReference extends Reference<Z3Object> {
|
||||
|
||||
public DummyReference() {
|
||||
super(null, null);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(Context ctx, long z3Obj) {
|
||||
// Should never be called.
|
||||
assert false;
|
||||
}
|
||||
}
|
||||
}
|
||||
Loading…
Reference in a new issue