mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 05:18:44 +00:00
f133f478c8
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.
37 lines
680 B
Plaintext
37 lines
680 B
Plaintext
(** The native (raw) interface to the dynamic Z3 library. *)
|
|
|
|
open Z3enums
|
|
|
|
(**/**)
|
|
type ptr
|
|
and symbol = ptr
|
|
and config = ptr
|
|
and context = ptr
|
|
and ast = ptr
|
|
and app = ast
|
|
and sort = ast
|
|
and func_decl = ast
|
|
and pattern = ast
|
|
and model = ptr
|
|
and literals = ptr
|
|
and constructor = ptr
|
|
and constructor_list = ptr
|
|
and solver = ptr
|
|
and goal = ptr
|
|
and tactic = ptr
|
|
and params = ptr
|
|
and probe = ptr
|
|
and stats = ptr
|
|
and ast_vector = ptr
|
|
and ast_map = ptr
|
|
and apply_result = ptr
|
|
and func_interp = ptr
|
|
and func_entry = ptr
|
|
and fixedpoint = ptr
|
|
and optimize = ptr
|
|
and param_descrs = ptr
|
|
and rcf_num = ptr
|
|
|
|
external set_internal_error_handler : ptr -> unit
|
|
= "n_set_internal_error_handler"
|