Package io.github.cvc5

Class Context

java.lang.Object
io.github.cvc5.Context
public class Context extends Object
The Context class is responsible for tracking and deleting pointers to native C++ cvc5 objects associated with their corresponding Java counterparts.

This class maintains a centralized registry of AbstractPointer instances, such as those used for term managers, solvers, terms, sorts, etc and ensures that all native memory is properly released when no longer needed.

  • Method Details

    • deletePointers

      public static void deletePointers()
      Delete all registered native pointers in reverse order of their registration.

      This method should be called by a single thread once all term managers and solver instances are no longer needed. It ensures that all native memory associated with registered AbstractPointers is released to prevent memory leaks.

      For more fine-grained control over memory release, consider using the AbstractPointer.deletePointer() method individually on each Java object instead of calling this method.