Z3.Base.C

Types

data Z3_config

data Z3_context

data Z3_symbol

data Z3_ast

data Z3_sort

data Z3_func_decl

data Z3_app

data Z3_pattern

data Z3_constructor

data Z3_constructor_list

data Z3_model

data Z3_goal

data Z3_tactic

data Z3_apply_result

data Z3_func_interp

data Z3_func_entry

data Z3_fixedpoint

data Z3_solver

data Z3_params

data Z3_ast_vector

data Z3_lbool

z3_l_true

z3_l_false

z3_l_undef

data Z3_bool

type Z3_error_handler

z3_true

z3_false

type Z3_string

type Z3_ast_print_mode

z3_print_smtlib_full

z3_print_low_level

z3_print_smtlib2_compliant

type Z3_error_code

z3_ok

z3_sort_error

z3_iob

z3_invalid_arg

z3_parser_error

z3_no_parser

z3_invalid_pattern

z3_memout_fail

z3_file_access_error

type Z3_sort_kind

z3_uninterpreted_sort

z3_internal_fatal

z3_bool_sort

z3_invalid_usage

z3_int_sort

z3_dec_ref_error

z3_real_sort

z3_exception

z3_bv_sort

z3_array_sort

z3_datatype_sort

z3_relation_sort

z3_finite_domain_sort

z3_floating_point_sort

z3_rounding_mode_sort

z3_unknown_sort

type Z3_ast_kind

z3_numeral_ast

z3_app_ast

z3_var_ast

z3_quantifier_ast

z3_sort_ast

z3_func_decl_ast

z3_unknown_ast

Create configuration

Create context

Symbols

Sorts

Constants and Applications

Propositional Logic and Equality

Arithmetic: Integers and Reals

Bit-vectors

Arrays

Sets

Numerals

Quantifiers

Accessors

Modifiers

AST vectors

Models

Constraints

Parameters

Interpolation

Tactics

Solvers

String Conversion

Parser Interface

Error Handling

Miscellaneous

Fixedpoint facilities