* feat(api/ml): use custom block hints to guide the GC
this forces the GC to collect garbage when a few _large_ objects
(solver, etc.) are dead. The current code would let arbitrarily many
such objects die and not trigger a GC (which would have to come from
OCaml code instead)
* tuning
* try to use caml_alloc_custom_mem with fake sizes
* try to fix leak by explicitly finalizing OCaml context
* chore: use more recent ubuntu for azure CI
* remove finalizer causing segfault in example
This patch ensures that the C code generated for the OCaml stubs complies with C89. It is needed to compile Z3 with OCaml support with Visual Studio versions older than VS2013.
This patch refactors the update_api script and the z3.ml implementation
to properly translate between OCaml options and NULL pointers. Some
unifications and simplifications (avoidance of unnecessary value allocation)
in the script that creates the native bindings.
The Z3 context and its reference counters are stored in a structure which is allocated
by the C layer outside the OCaml heap, whenever a Z3 context is created. The structure
and its Z3 context are disposed, once the last reference counter reaches zero. Reference
counters are decremented by C-level finalizers.
The OCaml representations for a Z3 context wrap only a pointer to the corresponding structure.