IDecRefQueue< T extends Z3Object > Class Template Reference

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.

{}

Member Function Documentation

clear()

void clear ( Context  ctx )

inlineprotected

Clean all references currently in

referenceQueue 

.

Definition at line 65 of file IDecRefQueue.java.

    {
        Reference<? extends T> ref;
        while ((ref = referenceQueue.poll()) != null) {
            long z3ast = referenceMap.remove(ref);
            decRef(ctx, z3ast);
        }
    }

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

ctx	Z3 context.
obj	Pointer 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.

                                        {
        for (long ref : referenceMap.values()) {
            decRef(ctx, ref);
        }
    }

storeReference()

void storeReference ( Context  ctx, T  obj  )

inline

Definition at line 56 of file IDecRefQueue.java.

                                                   {
        PhantomReference<T> ref = new PhantomReference<>(obj, referenceQueue);
        referenceMap.put(ref, obj.getNativeObject());
        clear(ctx);
    }