List of all items
Enums
Functions
- Z3_add_const_interp
- Z3_add_func_interp
- Z3_add_rec_def
- 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_dec_ref
- Z3_apply_result_get_num_subgoals
- Z3_apply_result_get_subgoal
- Z3_apply_result_inc_ref
- Z3_apply_result_to_string
- 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_close_log
- 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_eval_smtlib2_string
- Z3_finalize_memory
- Z3_fixedpoint_add_callback
- Z3_fixedpoint_add_constraint
- Z3_fixedpoint_add_cover
- Z3_fixedpoint_add_fact
- Z3_fixedpoint_add_invariant
- 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_ground_sat_answer
- Z3_fixedpoint_get_help
- Z3_fixedpoint_get_num_levels
- Z3_fixedpoint_get_param_descrs
- Z3_fixedpoint_get_reachable
- Z3_fixedpoint_get_reason_unknown
- Z3_fixedpoint_get_rule_names_along_trace
- Z3_fixedpoint_get_rules
- Z3_fixedpoint_get_rules_along_trace
- Z3_fixedpoint_get_statistics
- Z3_fixedpoint_inc_ref
- Z3_fixedpoint_init
- Z3_fixedpoint_query
- Z3_fixedpoint_query_from_lvl
- 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_bv
- Z3_fpa_get_numeral_exponent_int64
- Z3_fpa_get_numeral_exponent_string
- Z3_fpa_get_numeral_sign
- Z3_fpa_get_numeral_sign_bv
- Z3_fpa_get_numeral_significand_bv
- Z3_fpa_get_numeral_significand_string
- Z3_fpa_get_numeral_significand_uint64
- Z3_fpa_get_sbits
- Z3_fpa_is_numeral_inf
- Z3_fpa_is_numeral_nan
- Z3_fpa_is_numeral_negative
- Z3_fpa_is_numeral_normal
- Z3_fpa_is_numeral_positive
- Z3_fpa_is_numeral_subnormal
- Z3_fpa_is_numeral_zero
- 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_add_entry
- 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_func_interp_set_else
- 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_estimated_alloc_size
- Z3_get_finite_domain_sort_size
- Z3_get_full_version
- Z3_get_func_decl_id
- Z3_get_implied_equalities
- Z3_get_index_value
- Z3_get_num_probes
- Z3_get_num_tactics
- Z3_get_numeral_decimal_string
- Z3_get_numeral_double
- 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_sort
- Z3_get_sort_id
- Z3_get_sort_kind
- Z3_get_sort_name
- Z3_get_string
- 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_convert_model
- 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_dimacs_string
- Z3_goal_to_string
- Z3_goal_translate
- Z3_inc_ref
- 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_lambda
- Z3_is_numeral_ast
- Z3_is_quantifier_exists
- Z3_is_quantifier_forall
- Z3_is_re_sort
- Z3_is_seq_sort
- Z3_is_string
- Z3_is_string_sort
- 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_array_sort_n
- Z3_mk_as_array
- Z3_mk_ast_map
- Z3_mk_ast_vector
- Z3_mk_atleast
- Z3_mk_atmost
- Z3_mk_bool_sort
- Z3_mk_bound
- Z3_mk_bv2int
- Z3_mk_bv_numeral
- 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_128
- Z3_mk_fpa_sort_16
- Z3_mk_fpa_sort_32
- Z3_mk_fpa_sort_64
- 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_int2bv
- Z3_mk_int2real
- Z3_mk_int64
- Z3_mk_int_sort
- Z3_mk_int_symbol
- Z3_mk_int_to_str
- Z3_mk_is_int
- Z3_mk_ite
- Z3_mk_lambda
- Z3_mk_lambda_const
- Z3_mk_le
- Z3_mk_list_sort
- Z3_mk_lt
- Z3_mk_map
- Z3_mk_mod
- Z3_mk_model
- Z3_mk_mul
- Z3_mk_not
- Z3_mk_numeral
- Z3_mk_optimize
- Z3_mk_or
- Z3_mk_params
- Z3_mk_pattern
- Z3_mk_pbeq
- Z3_mk_pbge
- 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_re_complement
- Z3_mk_re_concat
- Z3_mk_re_empty
- Z3_mk_re_full
- Z3_mk_re_intersect
- Z3_mk_re_loop
- Z3_mk_re_option
- Z3_mk_re_plus
- Z3_mk_re_range
- Z3_mk_re_sort
- Z3_mk_re_star
- Z3_mk_re_union
- Z3_mk_real
- Z3_mk_real2int
- Z3_mk_real_sort
- Z3_mk_rec_func_decl
- Z3_mk_rem
- Z3_mk_repeat
- Z3_mk_rotate_left
- Z3_mk_rotate_right
- Z3_mk_select
- Z3_mk_select_n
- Z3_mk_seq_at
- Z3_mk_seq_concat
- Z3_mk_seq_contains
- Z3_mk_seq_empty
- Z3_mk_seq_extract
- Z3_mk_seq_in_re
- Z3_mk_seq_index
- Z3_mk_seq_length
- Z3_mk_seq_prefix
- Z3_mk_seq_replace
- Z3_mk_seq_sort
- Z3_mk_seq_suffix
- Z3_mk_seq_to_re
- Z3_mk_seq_unit
- 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_store_n
- Z3_mk_str_to_int
- Z3_mk_string
- Z3_mk_string_sort
- 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_extrapolate
- 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_model_translate
- Z3_open_log
- Z3_optimize_assert
- Z3_optimize_assert_soft
- Z3_optimize_check
- Z3_optimize_dec_ref
- Z3_optimize_from_file
- Z3_optimize_from_string
- Z3_optimize_get_assertions
- Z3_optimize_get_help
- Z3_optimize_get_lower
- Z3_optimize_get_lower_as_vector
- Z3_optimize_get_model
- Z3_optimize_get_objectives
- Z3_optimize_get_param_descrs
- Z3_optimize_get_reason_unknown
- Z3_optimize_get_statistics
- Z3_optimize_get_unsat_core
- Z3_optimize_get_upper
- Z3_optimize_get_upper_as_vector
- 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_documentation
- 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_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_qe_lite
- Z3_qe_model_project
- Z3_qe_model_project_skolem
- 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_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_cube
- Z3_solver_dec_ref
- Z3_solver_from_file
- Z3_solver_from_string
- Z3_solver_get_assertions
- Z3_solver_get_consequences
- Z3_solver_get_help
- Z3_solver_get_model
- Z3_solver_get_non_units
- 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_units
- Z3_solver_get_unsat_core
- Z3_solver_import_model_converter
- 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
Type Definitions
- Z3_app
- Z3_apply_result
- Z3_ast
- Z3_ast_map
- Z3_ast_vector
- Z3_config
- Z3_constructor
- Z3_constructor_list
- Z3_context
- Z3_error_handler
- Z3_fixedpoint
- Z3_fixedpoint_new_lemma_eh
- Z3_fixedpoint_predecessor_eh
- Z3_fixedpoint_reduce_app_callback_fptr
- Z3_fixedpoint_reduce_assign_callback_fptr
- Z3_fixedpoint_unfold_eh
- Z3_func_decl
- Z3_func_entry
- Z3_func_interp
- Z3_goal
- Z3_lbool
- Z3_literals
- Z3_model
- Z3_optimize
- Z3_param_descrs
- Z3_params
- Z3_pattern
- Z3_probe
- Z3_rcf_num
- Z3_solver
- Z3_sort
- Z3_stats
- Z3_string
- Z3_string_ptr
- Z3_symbol
- Z3_tactic