mirror of
https://github.com/Z3Prover/z3
synced 2026-06-13 12:25:37 +00:00
42 lines
930 B
Text
42 lines
930 B
Text
(** The native (raw) interface to the dynamic Z3 library. *)
|
|
|
|
open Z3enums
|
|
|
|
(**/**)
|
|
type ptr
|
|
type symbol = ptr
|
|
type config = ptr
|
|
type context = ptr
|
|
type ast = ptr
|
|
type app = ast
|
|
type sort = ast
|
|
type func_decl = ast
|
|
type pattern = ast
|
|
type model = ptr
|
|
type literals = ptr
|
|
type constructor = ptr
|
|
type constructor_list = ptr
|
|
type solver = ptr
|
|
type solver_callback = ptr
|
|
type goal = ptr
|
|
type tactic = ptr
|
|
type simplifier = ptr
|
|
type params = ptr
|
|
type parser_context = ptr
|
|
type probe = ptr
|
|
type stats = ptr
|
|
type ast_vector = ptr
|
|
type ast_map = ptr
|
|
type apply_result = ptr
|
|
type func_interp = ptr
|
|
type func_entry = ptr
|
|
type fixedpoint = ptr
|
|
type optimize = ptr
|
|
type param_descrs = ptr
|
|
type rcf_num = ptr
|
|
|
|
external set_internal_error_handler : ptr -> unit
|
|
= "n_set_internal_error_handler"
|
|
|
|
external solver_register_on_clause : context -> solver -> (ast option -> int list -> ast_vector -> unit) -> unit
|
|
= "n_solver_register_on_clause"
|