Module: Z3::ReferenceCounted

Included in:
Goal, Model, Optimize, ParamDescrs, Params, Probe, Solver, Tactic
Defined in:
lib/z3/reference_counted.rb

Overview

Z3 objects other than ASTs are reference counted, even when the context is not (Z3_mk_context vs Z3_mk_context_rc only changes how ASTs are managed).

Every wrapper must claim the object it holds, and release it once the wrapper is garbage collected. Without the release the native object stays alive at a nonzero refcount until the process exits.

Class Method Summary collapse

Class Method Details

.finalizer(kind, pointer) ⇒ Object

Must not close over the wrapper, or the wrapper would never become unreachable, the finalizer would never run, and the object would leak anyway



11
12
13
 
# File 'lib/z3/reference_counted.rb', line 11

def self.finalizer(kind, pointer)
  proc { LowLevel.dec_ref_pointer(kind, pointer) }
end