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 | ( |  | ) |
| inline protected

Definition at line 44 of file IDecRefQueue.java.

44{}

## Member Function Documentation

## ◆ clear()

void clear | ( | Context | ctx | ) |
| inline protected

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 }
com.microsoft.z3.IDecRefQueue.decRef
abstract void decRef(Context ctx, long obj)

Referenced by IDecRefQueue< T extends Z3Object >.storeReference().

## ◆ decRef()

abstract void decRef | ( | Context | ctx,
|  | long | obj
| ) |  |
| abstract protected

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.

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

## ◆ storeReference()

void storeReference | ( | Context | ctx,
|  | T | 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