Crate z3_sys

Enums

Struct__Z3_app
Struct__Z3_apply_result
Struct__Z3_ast
Struct__Z3_ast_map
Struct__Z3_ast_vector
Struct__Z3_config
Struct__Z3_constructor
Struct__Z3_constructor_list
Struct__Z3_context
Struct__Z3_fixedpoint
Struct__Z3_func_decl
Struct__Z3_func_entry
Struct__Z3_func_interp
Struct__Z3_goal
Struct__Z3_literals
Struct__Z3_model
Struct__Z3_optimize
Struct__Z3_param_descrs
Struct__Z3_params
Struct__Z3_pattern
Struct__Z3_probe
Struct__Z3_rcf_num
Struct__Z3_solver
Struct__Z3_sort
Struct__Z3_stats
Struct__Z3_symbol
Struct__Z3_tactic

Constants

Z3_APP_AST
Z3_ARRAY_SORT
Z3_BOOL_SORT
Z3_BV_SORT
Z3_DATATYPE_SORT
Z3_DEC_REF_ERROR
Z3_EXCEPTION
Z3_FALSE
Z3_FILE_ACCESS_ERROR
Z3_FINITE_DOMAIN_SORT
Z3_FLOATING_POINT_SORT
Z3_FUNC_DECL_AST
Z3_GOAL_OVER
Z3_GOAL_PRECISE
Z3_GOAL_UNDER
Z3_GOAL_UNDER_OVER
Z3_INTERNAL_FATAL
Z3_INT_SORT
Z3_INT_SYMBOL
Z3_INVALID_ARG
Z3_INVALID_PATTERN
Z3_INVALID_USAGE
Z3_IOB
Z3_L_FALSE
Z3_L_TRUE
Z3_L_UNDEF
Z3_MEMOUT_FAIL
Z3_NO_PARSER
Z3_NUMERAL_AST
Z3_OK
Z3_OP_ADD
Z3_OP_AGNUM
Z3_OP_AND
Z3_OP_ANUM
Z3_OP_ARRAY_DEFAULT
Z3_OP_ARRAY_EXT
Z3_OP_ARRAY_MAP
Z3_OP_AS_ARRAY
Z3_OP_BADD
Z3_OP_BAND
Z3_OP_BASHR
Z3_OP_BCOMP
Z3_OP_BIT0
Z3_OP_BIT1
Z3_OP_BLSHR
Z3_OP_BMUL
Z3_OP_BNAND
Z3_OP_BNEG
Z3_OP_BNOR
Z3_OP_BNOT
Z3_OP_BNUM
Z3_OP_BOR
Z3_OP_BREDAND
Z3_OP_BREDOR
Z3_OP_BSDIV
Z3_OP_BSDIV0
Z3_OP_BSHL
Z3_OP_BSMOD
Z3_OP_BSMOD0
Z3_OP_BSREM
Z3_OP_BSREM0
Z3_OP_BSUB
Z3_OP_BUDIV
Z3_OP_BUDIV0
Z3_OP_BUREM
Z3_OP_BUREM0
Z3_OP_BV2INT
Z3_OP_BXNOR
Z3_OP_BXOR
Z3_OP_CARRY
Z3_OP_CONCAT
Z3_OP_CONST_ARRAY
Z3_OP_DISTINCT
Z3_OP_DIV
Z3_OP_DT_ACCESSOR
Z3_OP_DT_CONSTRUCTOR
Z3_OP_DT_RECOGNISER
Z3_OP_DT_UPDATE_FIELD
Z3_OP_EQ
Z3_OP_EXTRACT
Z3_OP_EXT_ROTATE_LEFT
Z3_OP_EXT_ROTATE_RIGHT
Z3_OP_FALSE
Z3_OP_FD_CONSTANT
Z3_OP_FD_LT
Z3_OP_FPA_ABS
Z3_OP_FPA_ADD
Z3_OP_FPA_DIV
Z3_OP_FPA_EQ
Z3_OP_FPA_FMA
Z3_OP_FPA_FP
Z3_OP_FPA_GE
Z3_OP_FPA_GT
Z3_OP_FPA_IS_INF
Z3_OP_FPA_IS_NAN
Z3_OP_FPA_IS_NEGATIVE
Z3_OP_FPA_IS_NORMAL
Z3_OP_FPA_IS_POSITIVE
Z3_OP_FPA_IS_SUBNORMAL
Z3_OP_FPA_IS_ZERO
Z3_OP_FPA_LE
Z3_OP_FPA_LT
Z3_OP_FPA_MAX
Z3_OP_FPA_MIN
Z3_OP_FPA_MINUS_INF
Z3_OP_FPA_MINUS_ZERO
Z3_OP_FPA_MUL
Z3_OP_FPA_NAN
Z3_OP_FPA_NEG
Z3_OP_FPA_NUM
Z3_OP_FPA_PLUS_INF
Z3_OP_FPA_PLUS_ZERO
Z3_OP_FPA_REM
Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY
Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN
Z3_OP_FPA_RM_TOWARD_NEGATIVE
Z3_OP_FPA_RM_TOWARD_POSITIVE
Z3_OP_FPA_RM_TOWARD_ZERO
Z3_OP_FPA_ROUND_TO_INTEGRAL
Z3_OP_FPA_SQRT
Z3_OP_FPA_SUB
Z3_OP_FPA_TO_FP
Z3_OP_FPA_TO_FP_UNSIGNED
Z3_OP_FPA_TO_IEEE_BV
Z3_OP_FPA_TO_REAL
Z3_OP_FPA_TO_SBV
Z3_OP_FPA_TO_UBV
Z3_OP_GE
Z3_OP_GT
Z3_OP_IDIV
Z3_OP_IFF
Z3_OP_IMPLIES
Z3_OP_INT2BV
Z3_OP_INTERP
Z3_OP_IS_INT
Z3_OP_ITE
Z3_OP_LABEL
Z3_OP_LABEL_LIT
Z3_OP_LE
Z3_OP_LT
Z3_OP_MOD
Z3_OP_MUL
Z3_OP_NOT
Z3_OP_OEQ
Z3_OP_OR
Z3_OP_PB_AT_MOST
Z3_OP_PB_GE
Z3_OP_PB_LE
Z3_OP_POWER
Z3_OP_PR_AND_ELIM
Z3_OP_PR_APPLY_DEF
Z3_OP_PR_ASSERTED
Z3_OP_PR_CNF_STAR
Z3_OP_PR_COMMUTATIVITY
Z3_OP_PR_DEF_AXIOM
Z3_OP_PR_DEF_INTRO
Z3_OP_PR_DER
Z3_OP_PR_DISTRIBUTIVITY
Z3_OP_PR_ELIM_UNUSED_VARS
Z3_OP_PR_GOAL
Z3_OP_PR_HYPER_RESOLVE
Z3_OP_PR_HYPOTHESIS
Z3_OP_PR_IFF_FALSE
Z3_OP_PR_IFF_OEQ
Z3_OP_PR_IFF_TRUE
Z3_OP_PR_LEMMA
Z3_OP_PR_MODUS_PONENS
Z3_OP_PR_MODUS_PONENS_OEQ
Z3_OP_PR_MONOTONICITY
Z3_OP_PR_NNF_NEG
Z3_OP_PR_NNF_POS
Z3_OP_PR_NNF_STAR
Z3_OP_PR_NOT_OR_ELIM
Z3_OP_PR_PULL_QUANT
Z3_OP_PR_PULL_QUANT_STAR
Z3_OP_PR_PUSH_QUANT
Z3_OP_PR_QUANT_INST
Z3_OP_PR_QUANT_INTRO
Z3_OP_PR_REFLEXIVITY
Z3_OP_PR_REWRITE
Z3_OP_PR_REWRITE_STAR
Z3_OP_PR_SKOLEMIZE
Z3_OP_PR_SYMMETRY
Z3_OP_PR_TH_LEMMA
Z3_OP_PR_TRANSITIVITY
Z3_OP_PR_TRANSITIVITY_STAR
Z3_OP_PR_TRUE
Z3_OP_PR_UNDEF
Z3_OP_PR_UNIT_RESOLUTION
Z3_OP_RA_CLONE
Z3_OP_RA_COMPLEMENT
Z3_OP_RA_EMPTY
Z3_OP_RA_FILTER
Z3_OP_RA_IS_EMPTY
Z3_OP_RA_JOIN
Z3_OP_RA_NEGATION_FILTER
Z3_OP_RA_PROJECT
Z3_OP_RA_RENAME
Z3_OP_RA_SELECT
Z3_OP_RA_STORE
Z3_OP_RA_UNION
Z3_OP_RA_WIDEN
Z3_OP_REM
Z3_OP_REPEAT
Z3_OP_ROTATE_LEFT
Z3_OP_ROTATE_RIGHT
Z3_OP_SELECT
Z3_OP_SET_COMPLEMENT
Z3_OP_SET_DIFFERENCE
Z3_OP_SET_INTERSECT
Z3_OP_SET_SUBSET
Z3_OP_SET_UNION
Z3_OP_SGEQ
Z3_OP_SGT
Z3_OP_SIGN_EXT
Z3_OP_SLEQ
Z3_OP_SLT
Z3_OP_STORE
Z3_OP_SUB
Z3_OP_TO_INT
Z3_OP_TO_REAL
Z3_OP_TRUE
Z3_OP_UGEQ
Z3_OP_UGT
Z3_OP_ULEQ
Z3_OP_ULT
Z3_OP_UMINUS
Z3_OP_UNINTERPRETED
Z3_OP_XOR
Z3_OP_XOR3
Z3_OP_ZERO_EXT
Z3_PARAMETER_AST
Z3_PARAMETER_DOUBLE
Z3_PARAMETER_FUNC_DECL
Z3_PARAMETER_INT
Z3_PARAMETER_RATIONAL
Z3_PARAMETER_SORT
Z3_PARAMETER_SYMBOL
Z3_PARSER_ERROR
Z3_PK_BOOL
Z3_PK_DOUBLE
Z3_PK_INVALID
Z3_PK_OTHER
Z3_PK_STRING
Z3_PK_SYMBOL
Z3_PK_UINT
Z3_PRINT_LOW_LEVEL
Z3_PRINT_SMTLIB2_COMPLIANT
Z3_PRINT_SMTLIB_COMPLIANT
Z3_PRINT_SMTLIB_FULL
Z3_QUANTIFIER_AST
Z3_REAL_SORT
Z3_RELATION_SORT
Z3_ROUNDING_MODE_SORT
Z3_SORT_AST
Z3_SORT_ERROR
Z3_STRING_SYMBOL
Z3_TRUE
Z3_UNINTERPRETED_SORT
Z3_UNKNOWN_AST
Z3_UNKNOWN_SORT
Z3_VAR_AST

Statics

__stderrp
__stdinp
__stdoutp
sys_errlist
sys_nerr

Functions

Z3_algebraic_add⚠
Z3_algebraic_div⚠
Z3_algebraic_eq⚠
Z3_algebraic_eval⚠
Z3_algebraic_ge⚠
Z3_algebraic_gt⚠
Z3_algebraic_is_neg⚠
Z3_algebraic_is_pos⚠
Z3_algebraic_is_value⚠
Z3_algebraic_is_zero⚠
Z3_algebraic_le⚠
Z3_algebraic_lt⚠
Z3_algebraic_mul⚠
Z3_algebraic_neq⚠
Z3_algebraic_power⚠
Z3_algebraic_root⚠
Z3_algebraic_roots⚠
Z3_algebraic_sign⚠
Z3_algebraic_sub⚠
Z3_app_to_ast⚠
Z3_append_log⚠
Z3_apply_result_convert_model⚠
Z3_apply_result_dec_ref⚠
Z3_apply_result_get_num_subgoals⚠
Z3_apply_result_get_subgoal⚠
Z3_apply_result_inc_ref⚠
Z3_apply_result_to_string⚠
Z3_assert_cnstr⚠
Z3_ast_map_contains⚠
Z3_ast_map_dec_ref⚠
Z3_ast_map_erase⚠
Z3_ast_map_find⚠
Z3_ast_map_inc_ref⚠
Z3_ast_map_insert⚠
Z3_ast_map_keys⚠
Z3_ast_map_reset⚠
Z3_ast_map_size⚠
Z3_ast_map_to_string⚠
Z3_ast_to_string⚠
Z3_ast_vector_dec_ref⚠
Z3_ast_vector_get⚠
Z3_ast_vector_inc_ref⚠
Z3_ast_vector_push⚠
Z3_ast_vector_resize⚠
Z3_ast_vector_set⚠
Z3_ast_vector_size⚠
Z3_ast_vector_to_string⚠
Z3_ast_vector_translate⚠
Z3_benchmark_to_smtlib_string⚠
Z3_check_interpolant⚠
Z3_close_log⚠
Z3_compute_interpolant⚠
Z3_datatype_update_field⚠
Z3_dec_ref⚠
Z3_del_config⚠
Z3_del_constructor⚠
Z3_del_constructor_list⚠
Z3_del_context⚠
Z3_disable_trace⚠
Z3_enable_trace⚠
Z3_finalize_memory⚠
Z3_fixedpoint_add_cover⚠
Z3_fixedpoint_add_fact⚠
Z3_fixedpoint_add_rule⚠
Z3_fixedpoint_assert⚠
Z3_fixedpoint_dec_ref⚠
Z3_fixedpoint_from_file⚠
Z3_fixedpoint_from_string⚠
Z3_fixedpoint_get_answer⚠
Z3_fixedpoint_get_assertions⚠
Z3_fixedpoint_get_cover_delta⚠
Z3_fixedpoint_get_help⚠
Z3_fixedpoint_get_num_levels⚠
Z3_fixedpoint_get_param_descrs⚠
Z3_fixedpoint_get_reason_unknown⚠
Z3_fixedpoint_get_rules⚠
Z3_fixedpoint_get_statistics⚠
Z3_fixedpoint_inc_ref⚠
Z3_fixedpoint_init⚠
Z3_fixedpoint_pop⚠
Z3_fixedpoint_push⚠
Z3_fixedpoint_query⚠
Z3_fixedpoint_query_relations⚠
Z3_fixedpoint_register_relation⚠
Z3_fixedpoint_set_params⚠
Z3_fixedpoint_set_predicate_representation⚠
Z3_fixedpoint_set_reduce_app_callback⚠
Z3_fixedpoint_set_reduce_assign_callback⚠
Z3_fixedpoint_to_string⚠
Z3_fixedpoint_update_rule⚠
Z3_fpa_get_ebits⚠
Z3_fpa_get_numeral_exponent_int64⚠
Z3_fpa_get_numeral_exponent_string⚠
Z3_fpa_get_numeral_sign⚠
Z3_fpa_get_numeral_significand_string⚠
Z3_fpa_get_numeral_significand_uint64⚠
Z3_fpa_get_sbits⚠
Z3_func_decl_to_ast⚠
Z3_func_decl_to_string⚠
Z3_func_entry_dec_ref⚠
Z3_func_entry_get_arg⚠
Z3_func_entry_get_num_args⚠
Z3_func_entry_get_value⚠
Z3_func_entry_inc_ref⚠
Z3_func_interp_dec_ref⚠
Z3_func_interp_get_arity⚠
Z3_func_interp_get_else⚠
Z3_func_interp_get_entry⚠
Z3_func_interp_get_num_entries⚠
Z3_func_interp_inc_ref⚠
Z3_get_algebraic_number_lower⚠
Z3_get_algebraic_number_upper⚠
Z3_get_app_arg⚠
Z3_get_app_decl⚠
Z3_get_app_num_args⚠
Z3_get_arity⚠
Z3_get_array_sort_domain⚠
Z3_get_array_sort_range⚠
Z3_get_as_array_func_decl⚠
Z3_get_ast_hash⚠
Z3_get_ast_id⚠
Z3_get_ast_kind⚠
Z3_get_bool_value⚠
Z3_get_bv_sort_size⚠
Z3_get_datatype_sort_constructor⚠
Z3_get_datatype_sort_constructor_accessor⚠
Z3_get_datatype_sort_num_constructors⚠
Z3_get_datatype_sort_recognizer⚠
Z3_get_decl_ast_parameter⚠
Z3_get_decl_double_parameter⚠
Z3_get_decl_func_decl_parameter⚠
Z3_get_decl_int_parameter⚠
Z3_get_decl_kind⚠
Z3_get_decl_name⚠
Z3_get_decl_num_parameters⚠
Z3_get_decl_parameter_kind⚠
Z3_get_decl_rational_parameter⚠
Z3_get_decl_sort_parameter⚠
Z3_get_decl_symbol_parameter⚠
Z3_get_denominator⚠
Z3_get_domain⚠
Z3_get_domain_size⚠
Z3_get_error_code⚠
Z3_get_error_msg⚠
Z3_get_finite_domain_sort_size⚠
Z3_get_func_decl_id⚠
Z3_get_implied_equalities⚠
Z3_get_index_value⚠
Z3_get_interpolant⚠
Z3_get_num_probes⚠
Z3_get_num_tactics⚠
Z3_get_numeral_decimal_string⚠
Z3_get_numeral_int⚠
Z3_get_numeral_int64⚠
Z3_get_numeral_rational_int64⚠
Z3_get_numeral_small⚠
Z3_get_numeral_string⚠
Z3_get_numeral_uint⚠
Z3_get_numeral_uint64⚠
Z3_get_numerator⚠
Z3_get_pattern⚠
Z3_get_pattern_num_terms⚠
Z3_get_probe_name⚠
Z3_get_quantifier_body⚠
Z3_get_quantifier_bound_name⚠
Z3_get_quantifier_bound_sort⚠
Z3_get_quantifier_no_pattern_ast⚠
Z3_get_quantifier_num_bound⚠
Z3_get_quantifier_num_no_patterns⚠
Z3_get_quantifier_num_patterns⚠
Z3_get_quantifier_pattern_ast⚠
Z3_get_quantifier_weight⚠
Z3_get_range⚠
Z3_get_relation_arity⚠
Z3_get_relation_column⚠
Z3_get_smtlib_assumption⚠
Z3_get_smtlib_decl⚠
Z3_get_smtlib_error⚠
Z3_get_smtlib_formula⚠
Z3_get_smtlib_num_assumptions⚠
Z3_get_smtlib_num_decls⚠
Z3_get_smtlib_num_formulas⚠
Z3_get_smtlib_num_sorts⚠
Z3_get_smtlib_sort⚠
Z3_get_sort⚠
Z3_get_sort_id⚠
Z3_get_sort_kind⚠
Z3_get_sort_name⚠
Z3_get_symbol_int⚠
Z3_get_symbol_kind⚠
Z3_get_symbol_string⚠
Z3_get_tactic_name⚠
Z3_get_tuple_sort_field_decl⚠
Z3_get_tuple_sort_mk_decl⚠
Z3_get_tuple_sort_num_fields⚠
Z3_get_version⚠
Z3_global_param_get⚠
Z3_global_param_reset_all⚠
Z3_global_param_set⚠
Z3_goal_assert⚠
Z3_goal_dec_ref⚠
Z3_goal_depth⚠
Z3_goal_formula⚠
Z3_goal_inc_ref⚠
Z3_goal_inconsistent⚠
Z3_goal_is_decided_sat⚠
Z3_goal_is_decided_unsat⚠
Z3_goal_num_exprs⚠
Z3_goal_precision⚠
Z3_goal_reset⚠
Z3_goal_size⚠
Z3_goal_to_string⚠
Z3_goal_translate⚠
Z3_inc_ref⚠
Z3_interpolation_profile⚠
Z3_interrupt⚠
Z3_is_algebraic_number⚠
Z3_is_app⚠
Z3_is_as_array⚠
Z3_is_eq_ast⚠
Z3_is_eq_func_decl⚠
Z3_is_eq_sort⚠
Z3_is_numeral_ast⚠
Z3_is_quantifier_forall⚠
Z3_is_well_sorted⚠
Z3_mk_add⚠
Z3_mk_and⚠
Z3_mk_app⚠
Z3_mk_array_default⚠
Z3_mk_array_ext⚠
Z3_mk_array_sort⚠
Z3_mk_ast_map⚠
Z3_mk_ast_vector⚠
Z3_mk_atmost⚠
Z3_mk_bool_sort⚠
Z3_mk_bound⚠
Z3_mk_bv2int⚠
Z3_mk_bv_sort⚠
Z3_mk_bvadd⚠
Z3_mk_bvadd_no_overflow⚠
Z3_mk_bvadd_no_underflow⚠
Z3_mk_bvand⚠
Z3_mk_bvashr⚠
Z3_mk_bvlshr⚠
Z3_mk_bvmul⚠
Z3_mk_bvmul_no_overflow⚠
Z3_mk_bvmul_no_underflow⚠
Z3_mk_bvnand⚠
Z3_mk_bvneg⚠
Z3_mk_bvneg_no_overflow⚠
Z3_mk_bvnor⚠
Z3_mk_bvnot⚠
Z3_mk_bvor⚠
Z3_mk_bvredand⚠
Z3_mk_bvredor⚠
Z3_mk_bvsdiv⚠
Z3_mk_bvsdiv_no_overflow⚠
Z3_mk_bvsge⚠
Z3_mk_bvsgt⚠
Z3_mk_bvshl⚠
Z3_mk_bvsle⚠
Z3_mk_bvslt⚠
Z3_mk_bvsmod⚠
Z3_mk_bvsrem⚠
Z3_mk_bvsub⚠
Z3_mk_bvsub_no_overflow⚠
Z3_mk_bvsub_no_underflow⚠
Z3_mk_bvudiv⚠
Z3_mk_bvuge⚠
Z3_mk_bvugt⚠
Z3_mk_bvule⚠
Z3_mk_bvult⚠
Z3_mk_bvurem⚠
Z3_mk_bvxnor⚠
Z3_mk_bvxor⚠
Z3_mk_concat⚠
Z3_mk_config⚠
Z3_mk_const⚠
Z3_mk_const_array⚠
Z3_mk_constructor⚠
Z3_mk_constructor_list⚠
Z3_mk_context⚠
Z3_mk_context_rc⚠
Z3_mk_datatype⚠
Z3_mk_datatypes⚠
Z3_mk_distinct⚠
Z3_mk_div⚠
Z3_mk_empty_set⚠
Z3_mk_enumeration_sort⚠
Z3_mk_eq⚠
Z3_mk_exists⚠
Z3_mk_exists_const⚠
Z3_mk_ext_rotate_left⚠
Z3_mk_ext_rotate_right⚠
Z3_mk_extract⚠
Z3_mk_false⚠
Z3_mk_finite_domain_sort⚠
Z3_mk_fixedpoint⚠
Z3_mk_forall⚠
Z3_mk_forall_const⚠
Z3_mk_fpa_abs⚠
Z3_mk_fpa_add⚠
Z3_mk_fpa_div⚠
Z3_mk_fpa_eq⚠
Z3_mk_fpa_fma⚠
Z3_mk_fpa_fp⚠
Z3_mk_fpa_geq⚠
Z3_mk_fpa_gt⚠
Z3_mk_fpa_inf⚠
Z3_mk_fpa_is_infinite⚠
Z3_mk_fpa_is_nan⚠
Z3_mk_fpa_is_negative⚠
Z3_mk_fpa_is_normal⚠
Z3_mk_fpa_is_positive⚠
Z3_mk_fpa_is_subnormal⚠
Z3_mk_fpa_is_zero⚠
Z3_mk_fpa_leq⚠
Z3_mk_fpa_lt⚠
Z3_mk_fpa_max⚠
Z3_mk_fpa_min⚠
Z3_mk_fpa_mul⚠
Z3_mk_fpa_nan⚠
Z3_mk_fpa_neg⚠
Z3_mk_fpa_numeral_double⚠
Z3_mk_fpa_numeral_float⚠
Z3_mk_fpa_numeral_int⚠
Z3_mk_fpa_numeral_int64_uint64⚠
Z3_mk_fpa_numeral_int_uint⚠
Z3_mk_fpa_rem⚠
Z3_mk_fpa_rna⚠
Z3_mk_fpa_rne⚠
Z3_mk_fpa_round_nearest_ties_to_away⚠
Z3_mk_fpa_round_nearest_ties_to_even⚠
Z3_mk_fpa_round_to_integral⚠
Z3_mk_fpa_round_toward_negative⚠
Z3_mk_fpa_round_toward_positive⚠
Z3_mk_fpa_round_toward_zero⚠
Z3_mk_fpa_rounding_mode_sort⚠
Z3_mk_fpa_rtn⚠
Z3_mk_fpa_rtp⚠
Z3_mk_fpa_rtz⚠
Z3_mk_fpa_sort⚠
Z3_mk_fpa_sort_16⚠
Z3_mk_fpa_sort_32⚠
Z3_mk_fpa_sort_64⚠
Z3_mk_fpa_sort_128⚠
Z3_mk_fpa_sort_double⚠
Z3_mk_fpa_sort_half⚠
Z3_mk_fpa_sort_quadruple⚠
Z3_mk_fpa_sort_single⚠
Z3_mk_fpa_sqrt⚠
Z3_mk_fpa_sub⚠
Z3_mk_fpa_to_fp_bv⚠
Z3_mk_fpa_to_fp_float⚠
Z3_mk_fpa_to_fp_int_real⚠
Z3_mk_fpa_to_fp_real⚠
Z3_mk_fpa_to_fp_signed⚠
Z3_mk_fpa_to_fp_unsigned⚠
Z3_mk_fpa_to_ieee_bv⚠
Z3_mk_fpa_to_real⚠
Z3_mk_fpa_to_sbv⚠
Z3_mk_fpa_to_ubv⚠
Z3_mk_fpa_zero⚠
Z3_mk_fresh_const⚠
Z3_mk_fresh_func_decl⚠
Z3_mk_full_set⚠
Z3_mk_func_decl⚠
Z3_mk_ge⚠
Z3_mk_goal⚠
Z3_mk_gt⚠
Z3_mk_iff⚠
Z3_mk_implies⚠
Z3_mk_int⚠
Z3_mk_int64⚠
Z3_mk_int2bv⚠
Z3_mk_int2real⚠
Z3_mk_int_sort⚠
Z3_mk_int_symbol⚠
Z3_mk_interpolant⚠
Z3_mk_interpolation_context⚠
Z3_mk_is_int⚠
Z3_mk_ite⚠
Z3_mk_le⚠
Z3_mk_list_sort⚠
Z3_mk_lt⚠
Z3_mk_map⚠
Z3_mk_mod⚠
Z3_mk_mul⚠
Z3_mk_not⚠
Z3_mk_numeral⚠
Z3_mk_optimize⚠
Z3_mk_or⚠
Z3_mk_params⚠
Z3_mk_pattern⚠
Z3_mk_pble⚠
Z3_mk_power⚠
Z3_mk_probe⚠
Z3_mk_quantifier⚠
Z3_mk_quantifier_const⚠
Z3_mk_quantifier_const_ex⚠
Z3_mk_quantifier_ex⚠
Z3_mk_real⚠
Z3_mk_real2int⚠
Z3_mk_real_sort⚠
Z3_mk_rem⚠
Z3_mk_repeat⚠
Z3_mk_rotate_left⚠
Z3_mk_rotate_right⚠
Z3_mk_select⚠
Z3_mk_set_add⚠
Z3_mk_set_complement⚠
Z3_mk_set_del⚠
Z3_mk_set_difference⚠
Z3_mk_set_intersect⚠
Z3_mk_set_member⚠
Z3_mk_set_sort⚠
Z3_mk_set_subset⚠
Z3_mk_set_union⚠
Z3_mk_sign_ext⚠
Z3_mk_simple_solver⚠
Z3_mk_solver⚠
Z3_mk_solver_for_logic⚠
Z3_mk_solver_from_tactic⚠
Z3_mk_store⚠
Z3_mk_string_symbol⚠
Z3_mk_sub⚠
Z3_mk_tactic⚠
Z3_mk_true⚠
Z3_mk_tuple_sort⚠
Z3_mk_unary_minus⚠
Z3_mk_uninterpreted_sort⚠
Z3_mk_unsigned_int⚠
Z3_mk_unsigned_int64⚠
Z3_mk_xor⚠
Z3_mk_zero_ext⚠
Z3_model_dec_ref⚠
Z3_model_eval⚠
Z3_model_get_const_decl⚠
Z3_model_get_const_interp⚠
Z3_model_get_func_decl⚠
Z3_model_get_func_interp⚠
Z3_model_get_num_consts⚠
Z3_model_get_num_funcs⚠
Z3_model_get_num_sorts⚠
Z3_model_get_sort⚠
Z3_model_get_sort_universe⚠
Z3_model_has_interp⚠
Z3_model_inc_ref⚠
Z3_model_to_string⚠
Z3_open_log⚠
Z3_optimize_assert⚠
Z3_optimize_assert_soft⚠
Z3_optimize_check⚠
Z3_optimize_dec_ref⚠
Z3_optimize_get_help⚠
Z3_optimize_get_lower⚠
Z3_optimize_get_model⚠
Z3_optimize_get_param_descrs⚠
Z3_optimize_get_reason_unknown⚠
Z3_optimize_get_statistics⚠
Z3_optimize_get_upper⚠
Z3_optimize_inc_ref⚠
Z3_optimize_maximize⚠
Z3_optimize_minimize⚠
Z3_optimize_pop⚠
Z3_optimize_push⚠
Z3_optimize_set_params⚠
Z3_optimize_to_string⚠
Z3_param_descrs_dec_ref⚠
Z3_param_descrs_get_kind⚠
Z3_param_descrs_get_name⚠
Z3_param_descrs_inc_ref⚠
Z3_param_descrs_size⚠
Z3_param_descrs_to_string⚠
Z3_params_dec_ref⚠
Z3_params_inc_ref⚠
Z3_params_set_bool⚠
Z3_params_set_double⚠
Z3_params_set_symbol⚠
Z3_params_set_uint⚠
Z3_params_to_string⚠
Z3_params_validate⚠
Z3_parse_smtlib2_file⚠
Z3_parse_smtlib2_string⚠
Z3_parse_smtlib_file⚠
Z3_parse_smtlib_string⚠
Z3_pattern_to_ast⚠
Z3_pattern_to_string⚠
Z3_polynomial_subresultants⚠
Z3_probe_and⚠
Z3_probe_apply⚠
Z3_probe_const⚠
Z3_probe_dec_ref⚠
Z3_probe_eq⚠
Z3_probe_ge⚠
Z3_probe_get_descr⚠
Z3_probe_gt⚠
Z3_probe_inc_ref⚠
Z3_probe_le⚠
Z3_probe_lt⚠
Z3_probe_not⚠
Z3_probe_or⚠
Z3_query_constructor⚠
Z3_rcf_add⚠
Z3_rcf_del⚠
Z3_rcf_div⚠
Z3_rcf_eq⚠
Z3_rcf_ge⚠
Z3_rcf_get_numerator_denominator⚠
Z3_rcf_gt⚠
Z3_rcf_inv⚠
Z3_rcf_le⚠
Z3_rcf_lt⚠
Z3_rcf_mk_e⚠
Z3_rcf_mk_infinitesimal⚠
Z3_rcf_mk_pi⚠
Z3_rcf_mk_rational⚠
Z3_rcf_mk_roots⚠
Z3_rcf_mk_small_int⚠
Z3_rcf_mul⚠
Z3_rcf_neg⚠
Z3_rcf_neq⚠
Z3_rcf_num_to_decimal_string⚠
Z3_rcf_num_to_string⚠
Z3_rcf_power⚠
Z3_rcf_sub⚠
Z3_read_interpolation_problem⚠
Z3_reset_memory⚠
Z3_set_ast_print_mode⚠
Z3_set_error⚠
Z3_set_error_handler⚠
Z3_set_param_value⚠
Z3_simplify⚠
Z3_simplify_ex⚠
Z3_simplify_get_help⚠
Z3_simplify_get_param_descrs⚠
Z3_solver_assert⚠
Z3_solver_assert_and_track⚠
Z3_solver_check⚠
Z3_solver_check_assumptions⚠
Z3_solver_dec_ref⚠
Z3_solver_get_assertions⚠
Z3_solver_get_help⚠
Z3_solver_get_model⚠
Z3_solver_get_num_scopes⚠
Z3_solver_get_param_descrs⚠
Z3_solver_get_proof⚠
Z3_solver_get_reason_unknown⚠
Z3_solver_get_statistics⚠
Z3_solver_get_unsat_core⚠
Z3_solver_inc_ref⚠
Z3_solver_pop⚠
Z3_solver_push⚠
Z3_solver_reset⚠
Z3_solver_set_params⚠
Z3_solver_to_string⚠
Z3_solver_translate⚠
Z3_sort_to_ast⚠
Z3_sort_to_string⚠
Z3_stats_dec_ref⚠
Z3_stats_get_double_value⚠
Z3_stats_get_key⚠
Z3_stats_get_uint_value⚠
Z3_stats_inc_ref⚠
Z3_stats_is_double⚠
Z3_stats_is_uint⚠
Z3_stats_size⚠
Z3_stats_to_string⚠
Z3_substitute⚠
Z3_substitute_vars⚠
Z3_tactic_and_then⚠
Z3_tactic_apply⚠
Z3_tactic_apply_ex⚠
Z3_tactic_cond⚠
Z3_tactic_dec_ref⚠
Z3_tactic_fail⚠
Z3_tactic_fail_if⚠
Z3_tactic_fail_if_not_decided⚠
Z3_tactic_get_descr⚠
Z3_tactic_get_help⚠
Z3_tactic_get_param_descrs⚠
Z3_tactic_inc_ref⚠
Z3_tactic_or_else⚠
Z3_tactic_par_and_then⚠
Z3_tactic_par_or⚠
Z3_tactic_repeat⚠
Z3_tactic_skip⚠
Z3_tactic_try_for⚠
Z3_tactic_using_params⚠
Z3_tactic_when⚠
Z3_to_app⚠
Z3_to_func_decl⚠
Z3_toggle_warning_messages⚠
Z3_translate⚠
Z3_update_param_value⚠
Z3_update_term⚠
Z3_write_interpolation_problem⚠
__snprintf_chk⚠
__sprintf_chk⚠
__sputc⚠
__srget⚠
__svfscanf⚠
__swbuf⚠
__vsnprintf_chk⚠
__vsprintf_chk⚠
asprintf⚠
clearerr⚠
ctermid⚠
ctermid_r⚠
dprintf⚠
fclose⚠
fdopen⚠
feof⚠
ferror⚠
fflush⚠
fgetc⚠
fgetln⚠
fgetpos⚠
fgets⚠
fileno⚠
flockfile⚠
fmtcheck⚠
fopen⚠
fprintf⚠
fpurge⚠
fputc⚠
fputs⚠
fread⚠
freopen⚠
fscanf⚠
fseek⚠
fseeko⚠
fsetpos⚠
ftell⚠
ftello⚠
ftrylockfile⚠
funlockfile⚠
funopen⚠
fwrite⚠
getc⚠
getc_unlocked⚠
getchar⚠
getchar_unlocked⚠
getdelim⚠
getline⚠
gets⚠
getw⚠
pclose⚠
perror⚠
popen⚠
printf⚠
putc⚠
putc_unlocked⚠
putchar⚠
putchar_unlocked⚠
puts⚠
putw⚠
remove⚠
rename⚠
rewind⚠
scanf⚠
setbuf⚠
setbuffer⚠
setlinebuf⚠
setvbuf⚠
snprintf⚠
sprintf⚠
sscanf⚠
tempnam⚠
tmpfile⚠
tmpnam⚠
ungetc⚠
vasprintf⚠
vdprintf⚠
vfprintf⚠
vfscanf⚠
vprintf⚠
vscanf⚠
vsnprintf⚠
vsprintf⚠
vsscanf⚠
zopen⚠

Type Definitions

Enum_Unnamed2
Enum_Unnamed3
Enum_Unnamed4
Enum_Unnamed5
Enum_Unnamed6
Enum_Unnamed7
Enum_Unnamed8
Enum_Unnamed9
Enum_Unnamed10
Enum_Unnamed11
Z3_app
Z3_apply_result
Z3_ast
Z3_ast_kind
Z3_ast_map
Z3_ast_print_mode
Z3_ast_vector
Z3_bool
Z3_config
Z3_constructor
Z3_constructor_list
Z3_context
Z3_decl_kind
Z3_error_code
Z3_error_handler
Z3_fixedpoint
Z3_fixedpoint_reduce_app_callback_fptr
Z3_fixedpoint_reduce_assign_callback_fptr
Z3_func_decl
Z3_func_entry
Z3_func_interp
Z3_goal
Z3_goal_prec
Z3_lbool
Z3_literals
Z3_model
Z3_optimize
Z3_param_descrs
Z3_param_kind
Z3_parameter_kind
Z3_params
Z3_pattern
Z3_probe
Z3_rcf_num
Z3_solver
Z3_sort
Z3_sort_kind
Z3_stats
Z3_string
Z3_string_ptr
Z3_symbol
Z3_symbol_kind
Z3_tactic
__int16_t
__int32_t
__int64_t
__int8_t
__uint16_t
__uint32_t
__uint64_t
__uint8_t