Nonstandard Z3 OCaml Bindings

Overview

These are OCaml bindings for the Z3 SMT solver that closely follow the Z3 C API. This differs from the official Z3 OCaml bindings which provide a more object-oriented wrapper interface.

Goals:

• The binding layer should be as thin as possible, avoiding surprises. The OCaml binding of a C function converts the arguments, calls the C function, and converts the results. Intermediate data structure conversions, hidden caches, etc. are avoided. OCaml functions that do more, e.g. mk_context and mk_datatypes, have OCaml API documentation.

• The OCaml interface should be close enough to the C interface that it is effective for users to read the Z3 C API documentation and follow the types of the OCaml functions. Function signatures are translated systematically with very few exceptions, so the friction should be low.

Installation

opam install nonstd-z3

Note this requires the conf-z3 opam package, which locates an already-built Z3 library and header files from system packages or a local build.

Design

Automatic reference counting

The bindings automatically manage Z3's reference counting. The inc_ref and dec_ref functions are not exposed in the OCaml API. Instead, inc_ref is called when Z3 values are returned to OCaml, and dec_ref is called by OCaml finalizers when the values are garbage collected.

Error handling

Z3 errors raise a Fatal exception. These exceptions are fatal: Z3 may be left in an inconsistent internal state, and it is unsafe to call any Z3 function after a Fatal exception has been raised.

This is a design trade-off for efficiency. The OCaml exception is raised from within Z3's C++ code, which means the C++ stack is not unwound correctly. An alternative design could propagate errors to the C/OCaml boundary and only raise an OCaml exception there.

Context lifetime

Z3 contexts are intentionally never freed. This is because OCaml finalizers for Z3 values may call dec_ref at any time, and calling dec_ref after del_context is unsafe. The memory management functions reset_memory and finalize_memory are also not exposed for the same reason.

This is a design trade-off for efficiency. Alternative designs could prevent contexts from being freed while live Z3 values exist.

Testing

The test/ directory contains a test suite demonstrating usage of various Z3 features including user propagators and parametric datatypes.

Operation

The Z3 bindings are generated through several stages involving opam package configuration, header file parsing, IDL generation, and CamlIDL processing.

Locating the Z3 installation

The conf-z3 opam package provides the location of the Z3 library installation. This can be either a system-installed package or a local build from source. The dune file queries opam for:

• opam var conf-z3:includedir - location of Z3 header files
• opam var conf-z3:cflags - compiler flags for C compilation
• opam var conf-z3:libs - linker flags for the Z3 library

IDL generation

The dune file passes the Z3 include directory to the gen_z3_idl.ml script, which reads the Z3 header files and generates IDL code. CamlIDL then processes this IDL code to produce the z3.ml, z3.mli, and z3_stubs.c files that form the bindings.

gen_z3_idl.ml

The gen_z3_idl.ml script performs several steps:

1. Type conversions: Defines custom conversions between C and OCaml types. These handle the interoperation between Z3's reference counting and OCaml's garbage collection. Reference-counted Z3 types are wrapped in OCaml custom blocks with finalizers that call the appropriate dec_ref functions. The inc_ref calls happen when values are returned from Z3 to OCaml. Some Z3 types (Z3_ast and its subtypes) also support polymorphic comparison and hashing.

2. Enum translation: Reads the Z3 header files to find typedef enum definitions and translates them to IDL enum declarations. This header file parsing is hacky.

3. API translation: Reads the Z3 header files to find def_API and extra_API comments that declare the exposed C API. These are parsed and translated into IDL function declarations with type annotations for input/output parameters, arrays with length parameters, nullable pointers, etc. The def_API annotations do not fully express the information that CamlIDL needs, so a few functions require hand-written IDL declarations.

4. Safe OCaml interfaces: Emits custom wrappers for Z3 features that need a different style of interface than the C API to be safe in OCaml:

   • Datatype creation (mk_datatype, mk_polymorphic_datatype, mk_datatypes) without exposing the Z3_constructor type, whose values cannot be freed safely
   • Context creation (mk_context) without exposing the Z3_config type

5. Function pointer callbacks: Emits custom bindings for Z3 features that rely on function pointers, such as the user propagator interface.