z3_ffi library

Classes

Z3_ast_kind
\brief The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Z3_ast_print_mode
\brief Z3 pretty printing modes (See #Z3_set_ast_print_mode).
Z3_decl_kind
\brief The different kinds of interpreted function kinds.
Z3_error_code
\brief Z3 error codes (See #Z3_get_error_code).
Z3_goal_prec
\brief A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving and transforming Goals. Some of these transformations apply under/over approximations.
Z3_lbool
\brief Lifted Boolean type: \c false, \c undefined, \c true.
Z3_param_kind
\brief The different kinds of parameters that can be associated with parameter sets. (see #Z3_mk_params).
Z3_parameter_kind
\brief The different kinds of parameters that can be associated with function symbols. \sa Z3_get_decl_num_parameters \sa Z3_get_decl_parameter_kind
Z3_sort_kind
\brief The different kinds of Z3 types (See #Z3_get_sort_kind).
Z3_symbol_kind
\brief The different kinds of symbol. In Z3, a symbol can be represented using integers and strings (See #Z3_get_symbol_kind).
Z3Lib

Constants

BUFSIZ → const int
EOF → const int
false1 → const int
FILENAME_MAX → const int
FOPEN_MAX → const int
INT16_MAX → const int
INT16_MIN → const int
INT32_MAX → const int
INT32_MIN → const int
INT64_MAX → const int
INT64_MIN → const int
INT8_MAX → const int
INT8_MIN → const int
INT_FAST16_MAX → const int
INT_FAST16_MIN → const int
INT_FAST32_MAX → const int
INT_FAST32_MIN → const int
INT_FAST64_MAX → const int
INT_FAST64_MIN → const int
INT_FAST8_MAX → const int
INT_FAST8_MIN → const int
INT_LEAST16_MAX → const int
INT_LEAST16_MIN → const int
INT_LEAST32_MAX → const int
INT_LEAST32_MIN → const int
INT_LEAST64_MAX → const int
INT_LEAST64_MIN → const int
INT_LEAST8_MAX → const int
INT_LEAST8_MIN → const int
INTMAX_MAX → const int
INTMAX_MIN → const int
INTPTR_MAX → const int
INTPTR_MIN → const int
L_tmpnam → const int
L_tmpnam_s → const int
NULL → const int
PTRDIFF_MAX → const int
PTRDIFF_MIN → const int
SEEK_CUR → const int
SEEK_END → const int
SEEK_SET → const int
SIG_ATOMIC_MAX → const int
SIG_ATOMIC_MIN → const int
SIZE_MAX → const int
SYS_OPEN → const int
TMP_MAX → const int
TMP_MAX_S → const int
true1 → const int
UINT16_MAX → const int
UINT32_MAX → const int
UINT64_MAX → const int
UINT8_MAX → const int
UINT_FAST16_MAX → const int
UINT_FAST32_MAX → const int
UINT_FAST64_MAX → const int
UINT_FAST8_MAX → const int
UINT_LEAST16_MAX → const int
UINT_LEAST32_MAX → const int
UINT_LEAST64_MAX → const int
UINT_LEAST8_MAX → const int
UINTMAX_MAX → const int
UINTPTR_MAX → const int
WCHAR_MAX → const int
WCHAR_MIN → const int
WEOF → const int
WINT_MAX → const int
WINT_MIN → const int

Typedefs

errno_t = Int
FILE = _iobuf
fpos_t = LongLong
rsize_t = Size
va_list = Pointer<Char>
wint_t = UnsignedShort
Z3_app = Pointer<_Z3_app>
Z3_apply_result = Pointer<_Z3_apply_result>
Z3_ast = Pointer<_Z3_ast>
Z3_ast_map = Pointer<_Z3_ast_map>
Z3_ast_vector = Pointer<_Z3_ast_vector>
Z3_char_ptr = Pointer<Char>
Z3_config = Pointer<_Z3_config>
Z3_constructor = Pointer<_Z3_constructor>
Z3_constructor_list = Pointer<_Z3_constructor_list>
Z3_context = Pointer<_Z3_context>
Z3_created_eh = NativeFunction<Void Function(Pointer<Void> ctx, Z3_solver_callback cb, Z3_ast t)>
Z3_decide_eh = NativeFunction<Void Function(Pointer<Void> ctx, Z3_solver_callback cb, Z3_ast t, UnsignedInt idx, Bool phase)>
Z3_eq_eh = NativeFunction<Void Function(Pointer<Void> ctx, Z3_solver_callback cb, Z3_ast s, Z3_ast t)>
Z3_error_handler = NativeFunction<Void Function(Z3_context c, Int32 e)>
Z3_final_eh = NativeFunction<Void Function(Pointer<Void> ctx, Z3_solver_callback cb)>
Z3_fixed_eh = NativeFunction<Void Function(Pointer<Void> ctx, Z3_solver_callback cb, Z3_ast t, Z3_ast value)>
Z3_fixedpoint = Pointer<_Z3_fixedpoint>
Z3_fixedpoint_new_lemma_eh = Pointer<NativeFunction<Void Function(Pointer<Void> state, Z3_ast lemma, UnsignedInt level)>>
Z3_fixedpoint_predecessor_eh = Pointer<NativeFunction<Void Function(Pointer<Void> state)>>
Z3_fixedpoint_reduce_app_callback_fptr = NativeFunction<Void Function(Pointer<Void>, Z3_func_decl, UnsignedInt, Pointer<Z3_ast>, Pointer<Z3_ast>)>
Z3_fixedpoint_reduce_assign_callback_fptr = NativeFunction<Void Function(Pointer<Void>, Z3_func_decl, UnsignedInt, Pointer<Z3_ast>, UnsignedInt, Pointer<Z3_ast>)>
\brief The following utilities allows adding user-defined domains.
Z3_fixedpoint_unfold_eh = Pointer<NativeFunction<Void Function(Pointer<Void> state)>>
Z3_fresh_eh = NativeFunction<Pointer<Void> Function(Pointer<Void> ctx, Z3_context new_context)>
Z3_func_decl = Pointer<_Z3_func_decl>
Z3_func_entry = Pointer<_Z3_func_entry>
Z3_func_interp = Pointer<_Z3_func_interp>
Z3_goal = Pointer<_Z3_goal>
Z3_model = Pointer<_Z3_model>
Z3_model_eh = NativeFunction<Void Function(Pointer<Void> ctx)>
\brief callback functions for models.
Z3_on_clause_eh = NativeFunction<Void Function(Pointer<Void> ctx, Z3_ast proof_hint, UnsignedInt n, Pointer<UnsignedInt> deps, Z3_ast_vector literals)>
Z3_optimize = Pointer<_Z3_optimize>
Z3_param_descrs = Pointer<_Z3_param_descrs>
Z3_params = Pointer<_Z3_params>
Z3_parser_context = Pointer<_Z3_parser_context>
Z3_pattern = Pointer<_Z3_pattern>
Z3_pop_eh = NativeFunction<Void Function(Pointer<Void> ctx, Z3_solver_callback cb, UnsignedInt num_scopes)>
Z3_probe = Pointer<_Z3_probe>
Z3_push_eh = NativeFunction<Void Function(Pointer<Void> ctx, Z3_solver_callback cb)>
Z3_rcf_num = Pointer<_Z3_rcf_num>
Z3_simplifier = Pointer<_Z3_simplifier>
Z3_solver = Pointer<_Z3_solver>
Z3_solver_callback = Pointer<_Z3_solver_callback>
Z3_sort = Pointer<_Z3_sort>
Z3_stats = Pointer<_Z3_stats>
Z3_string = Pointer<Char>
\brief Z3 string type. It is just an alias for \ccode{const char *}.
Z3_string_ptr = Pointer<Z3_string>
Z3_symbol = Pointer<_Z3_symbol>
Z3_tactic = Pointer<_Z3_tactic>