mirror of
https://github.com/Z3Prover/z3
synced 2026-02-23 00:37:36 +00:00
91886dafca
* do not use `and` for non mutually recursive types * use List.init, fix complexity of a few operations and make some code more readable * explicit some parameters to make working without LSP/Merlin easier * use fold_left instead of filteri because it is not available on old OCaml versions
39 lines
782 B
Text
39 lines
782 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"
|