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 }
abstract void decRef(Context ctx, long obj)

Referenced by IDecRefQueue< T extends Z3Object >.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< T extends Z3Object >.clear(), and IDecRefQueue< T extends Z3Object >.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 }