Package com.microsoft.z3

Class IDecRefQueue<T extends Z3Object>

java.lang.Object
com.microsoft.z3.IDecRefQueue<T>
Type Parameters:
T - Type of object stored in queue.
Direct Known Subclasses:
ConstructorDecRefQueue, ConstructorListDecRefQueue
public abstract class IDecRefQueue<T extends Z3Object> extends Object
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.

  • Constructor Details

    • IDecRefQueue

      protected IDecRefQueue()

  • Method Details

    • decRef

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

    • storeReference

      public void storeReference(Context ctx, T obj)

    • clear

      protected void clear(Context ctx)
      Clean all references currently in referenceQueue.

    • forceClear

      public void forceClear(Context ctx)
      Clean all references stored in referenceMap, regardless of whether they are in referenceMap or not.