Z3
Public Member Functions | Protected Member Functions
IDecRefQueue< T extends Z3Object > Class Template Referenceabstract

Public Member Functions

void storeReference (Context ctx, T obj)
 
void forceClear (Context ctx)
 

Protected Member Functions

 IDecRefQueue ()
 
abstract void decRef (Context ctx, long obj)
 
void clear (Context ctx)
 

Detailed Description

A queue to handle management of native memory.

Mechanics: once an object is created, a metadata is stored for it in

referenceMap

, and a PhantomReference is created with a reference to

referenceQueue

. Once the object becomes strongly unreachable, the phantom reference gets added by JVM to the

referenceQueue

. After each object creation, we iterate through the available objects in

referenceQueue

and decrement references for them.

Parameters
<T>Type of object stored in queue.

Definition at line 39 of file IDecRefQueue.java.

Constructor & Destructor Documentation

◆ IDecRefQueue()

IDecRefQueue ( )
inlineprotected

Definition at line 44 of file IDecRefQueue.java.

44 {}

Member Function Documentation

◆ clear()

void clear ( Context  ctx)
inlineprotected

Clean all references currently in

referenceQueue

.

Definition at line 65 of file IDecRefQueue.java.

66  {
67  Reference<? extends T> ref;
68  while ((ref = referenceQueue.poll()) != null) {
69  long z3ast = referenceMap.remove(ref);
70  decRef(ctx, z3ast);
71  }
72  }

Referenced by IDecRefQueue< ParamDescrs >.storeReference().

◆ decRef()

abstract void decRef ( Context  ctx,
long  obj 
)
abstractprotected

An implementation of this method should decrement the reference on a given native object. This function should always be called on the

ctx

thread.

Parameters
ctxZ3 context.
objPointer to a Z3 object.

Referenced by IDecRefQueue< ParamDescrs >.clear(), and IDecRefQueue< ParamDescrs >.forceClear().

◆ forceClear()

void forceClear ( Context  ctx)
inline

Clean all references stored in

referenceMap

, regardless of whether they are in

referenceMap

or not.

Definition at line 78 of file IDecRefQueue.java.

78  {
79  for (long ref : referenceMap.values()) {
80  decRef(ctx, ref);
81  }
82  }

◆ storeReference()

void storeReference ( Context  ctx,
obj 
)
inline

Definition at line 56 of file IDecRefQueue.java.

56  {
57  PhantomReference<T> ref = new PhantomReference<>(obj, referenceQueue);
58  referenceMap.put(ref, obj.getNativeObject());
59  clear(ctx);
60  }
com.microsoft.z3.IDecRefQueue.clear
void clear(Context ctx)
Definition: IDecRefQueue.java:65
com.microsoft.z3.IDecRefQueue.decRef
abstract void decRef(Context ctx, long obj)