module Z3.Base.C where
import Foreign
import Foreign.C.Types
import Foreign.C.String
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_solver
data Z3_params
data Z3_ast_vector
newtype Z3_lbool = Z3_lbool CInt
deriving Eq
z3_l_true, z3_l_false, z3_l_undef :: Z3_lbool
z3_l_true = Z3_lbool (1)
z3_l_false = Z3_lbool (1)
z3_l_undef = Z3_lbool (0)
newtype Z3_bool = Z3_bool CInt
deriving Eq
type Z3_error_handler = Ptr Z3_context -> Z3_error_code -> IO ()
z3_true, z3_false :: Z3_bool
z3_true = Z3_bool(1)
z3_false = Z3_bool(0)
type Z3_string = CString
type Z3_ast_print_mode = CInt
z3_print_smtlib_full :: Z3_ast_print_mode
z3_print_smtlib_full = 0
z3_print_low_level :: Z3_ast_print_mode
z3_print_low_level = 1
z3_print_smtlib2_compliant :: Z3_ast_print_mode
z3_print_smtlib2_compliant = 2
type Z3_error_code = CInt
z3_ok :: Z3_error_code
z3_ok = 0
z3_sort_error :: Z3_error_code
z3_sort_error = 1
z3_iob :: Z3_error_code
z3_iob = 2
z3_invalid_arg :: Z3_error_code
z3_invalid_arg = 3
z3_parser_error :: Z3_error_code
z3_parser_error = 4
z3_no_parser :: Z3_error_code
z3_no_parser = 5
z3_invalid_pattern :: Z3_error_code
z3_invalid_pattern = 6
z3_memout_fail :: Z3_error_code
z3_memout_fail = 7
z3_file_access_error :: Z3_error_code
z3_file_access_error = 8
z3_internal_fatal :: Z3_error_code
z3_internal_fatal = 9
z3_invalid_usage :: Z3_error_code
z3_invalid_usage = 10
z3_dec_ref_error :: Z3_error_code
z3_dec_ref_error = 11
z3_exception :: Z3_error_code
z3_exception = 12
type Z3_sort_kind = CInt
z3_uninterpreted_sort :: Z3_sort_kind
z3_uninterpreted_sort = 0
z3_bool_sort :: Z3_sort_kind
z3_bool_sort = 1
z3_int_sort :: Z3_sort_kind
z3_int_sort = 2
z3_real_sort :: Z3_sort_kind
z3_real_sort = 3
z3_bv_sort :: Z3_sort_kind
z3_bv_sort = 4
z3_array_sort :: Z3_sort_kind
z3_array_sort = 5
z3_datatype_sort :: Z3_sort_kind
z3_datatype_sort = 6
z3_relation_sort :: Z3_sort_kind
z3_relation_sort = 7
z3_finite_domain_sort :: Z3_sort_kind
z3_finite_domain_sort = 8
z3_floating_point_sort :: Z3_sort_kind
z3_floating_point_sort = 9
z3_rounding_mode_sort :: Z3_sort_kind
z3_rounding_mode_sort = 10
z3_unknown_sort :: Z3_sort_kind
z3_unknown_sort = 1000
type Z3_ast_kind = CInt
z3_numeral_ast :: Z3_ast_kind
z3_numeral_ast = 0
z3_app_ast :: Z3_ast_kind
z3_app_ast = 1
z3_var_ast :: Z3_ast_kind
z3_var_ast = 2
z3_quantifier_ast :: Z3_ast_kind
z3_quantifier_ast = 3
z3_sort_ast :: Z3_ast_kind
z3_sort_ast = 4
z3_func_decl_ast :: Z3_ast_kind
z3_func_decl_ast = 5
z3_unknown_ast :: Z3_ast_kind
z3_unknown_ast = 1000
foreign import ccall unsafe "Z3_mk_config"
z3_mk_config :: IO (Ptr Z3_config)
foreign import ccall unsafe "Z3_del_config"
z3_del_config :: Ptr Z3_config -> IO ()
foreign import ccall unsafe "Z3_set_param_value"
z3_set_param_value :: Ptr Z3_config -> Z3_string -> Z3_string -> IO ()
foreign import ccall unsafe "Z3_mk_context_rc"
z3_mk_context_rc :: Ptr Z3_config -> IO (Ptr Z3_context)
foreign import ccall unsafe "Z3_del_context"
z3_del_context :: Ptr Z3_context -> IO ()
foreign import ccall unsafe "Z3_inc_ref"
z3_inc_ref :: Ptr Z3_context -> Ptr Z3_ast -> IO ()
foreign import ccall unsafe "Z3_inc_ref"
z3_dec_ref :: Ptr Z3_context -> Ptr Z3_ast -> IO ()
foreign import ccall unsafe "Z3_mk_int_symbol"
z3_mk_int_symbol :: Ptr Z3_context -> CInt -> IO (Ptr Z3_symbol)
foreign import ccall unsafe "Z3_mk_string_symbol"
z3_mk_string_symbol :: Ptr Z3_context -> Z3_string -> IO (Ptr Z3_symbol)
foreign import ccall unsafe "Z3_sort_to_ast"
z3_sort_to_ast :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_uninterpreted_sort"
z3_mk_uninterpreted_sort :: Ptr Z3_context -> Ptr Z3_symbol -> IO (Ptr Z3_sort)
foreign import ccall unsafe "Z3_mk_bool_sort"
z3_mk_bool_sort :: Ptr Z3_context -> IO (Ptr Z3_sort)
foreign import ccall unsafe "Z3_mk_int_sort"
z3_mk_int_sort :: Ptr Z3_context -> IO (Ptr Z3_sort)
foreign import ccall unsafe "Z3_mk_real_sort"
z3_mk_real_sort :: Ptr Z3_context -> IO (Ptr Z3_sort)
foreign import ccall unsafe "Z3_mk_bv_sort"
z3_mk_bv_sort :: Ptr Z3_context -> CUInt -> IO (Ptr Z3_sort)
foreign import ccall unsafe "Z3_mk_array_sort"
z3_mk_array_sort :: Ptr Z3_context -> Ptr Z3_sort -> Ptr Z3_sort -> IO (Ptr Z3_sort)
foreign import ccall unsafe "Z3_mk_tuple_sort"
z3_mk_tuple_sort :: Ptr Z3_context
-> Ptr Z3_symbol
-> CUInt
-> Ptr (Ptr Z3_symbol)
-> Ptr (Ptr Z3_sort)
-> Ptr (Ptr Z3_func_decl)
-> Ptr (Ptr Z3_func_decl)
-> IO (Ptr Z3_sort)
foreign import ccall unsafe "Z3_mk_constructor"
z3_mk_constructor :: Ptr Z3_context
-> Ptr Z3_symbol
-> Ptr Z3_symbol
-> CUInt
-> Ptr (Ptr Z3_symbol)
-> Ptr (Ptr Z3_sort)
-> Ptr CUInt
-> IO (Ptr Z3_constructor)
foreign import ccall unsafe "Z3_del_constructor"
z3_del_constructor :: Ptr Z3_context -> Ptr Z3_constructor -> IO ()
foreign import ccall unsafe "Z3_mk_datatype"
z3_mk_datatype :: Ptr Z3_context
-> Ptr Z3_symbol
-> CUInt
-> Ptr (Ptr Z3_constructor)
-> IO (Ptr Z3_sort)
foreign import ccall unsafe "Z3_mk_constructor_list"
z3_mk_constructor_list :: Ptr Z3_context
-> CUInt
-> Ptr (Ptr Z3_constructor)
-> IO (Ptr Z3_constructor_list)
foreign import ccall unsafe "Z3_del_constructor_list"
z3_del_constructor_list :: Ptr Z3_context
-> Ptr (Z3_constructor_list)
-> IO ()
foreign import ccall unsafe "Z3_mk_datatypes"
z3_mk_datatypes :: Ptr Z3_context
-> CUInt
-> Ptr (Ptr Z3_symbol)
-> Ptr (Ptr Z3_sort)
-> Ptr (Ptr Z3_constructor_list)
-> IO ()
foreign import ccall unsafe "Z3_mk_set_sort"
z3_mk_set_sort :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_sort)
foreign import ccall unsafe "Z3_mk_func_decl"
z3_mk_func_decl :: Ptr Z3_context
-> Ptr Z3_symbol
-> CUInt
-> Ptr (Ptr Z3_sort)
-> Ptr Z3_sort
-> IO (Ptr Z3_func_decl)
foreign import ccall unsafe "Z3_mk_app"
z3_mk_app :: Ptr Z3_context
-> Ptr Z3_func_decl
-> CUInt
-> Ptr (Ptr Z3_ast)
-> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_const"
z3_mk_const :: Ptr Z3_context -> Ptr Z3_symbol -> Ptr Z3_sort -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_fresh_const"
z3_mk_fresh_const :: Ptr Z3_context -> Z3_string -> Ptr Z3_sort -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_fresh_func_decl"
z3_mk_fresh_func_decl :: Ptr z3_context
-> Z3_string
-> CUInt
-> Ptr (Ptr Z3_sort)
-> Ptr Z3_sort
-> IO (Ptr Z3_func_decl)
foreign import ccall unsafe "Z3_mk_true"
z3_mk_true :: Ptr Z3_context -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_false"
z3_mk_false :: Ptr Z3_context -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_eq"
z3_mk_eq :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_distinct"
z3_mk_distinct :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_not"
z3_mk_not :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_ite"
z3_mk_ite :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_iff"
z3_mk_iff :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_implies"
z3_mk_implies :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_xor"
z3_mk_xor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_and"
z3_mk_and :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_or"
z3_mk_or :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_add"
z3_mk_add :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_mul"
z3_mk_mul :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_sub"
z3_mk_sub :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_unary_minus"
z3_mk_unary_minus :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_div"
z3_mk_div :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_mod"
z3_mk_mod :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_rem"
z3_mk_rem :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_lt"
z3_mk_lt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_le"
z3_mk_le :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_gt"
z3_mk_gt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_ge"
z3_mk_ge :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_int2real"
z3_mk_int2real :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_real2int"
z3_mk_real2int :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_is_int"
z3_mk_is_int :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvnot"
z3_mk_bvnot :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvredand"
z3_mk_bvredand :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvredor"
z3_mk_bvredor :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvand"
z3_mk_bvand :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvor"
z3_mk_bvor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvxor"
z3_mk_bvxor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvnand"
z3_mk_bvnand :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvnor"
z3_mk_bvnor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvxnor"
z3_mk_bvxnor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvneg"
z3_mk_bvneg :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvadd"
z3_mk_bvadd :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvsub"
z3_mk_bvsub :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvmul"
z3_mk_bvmul :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvudiv"
z3_mk_bvudiv :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvsdiv"
z3_mk_bvsdiv :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvurem"
z3_mk_bvurem :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvsrem"
z3_mk_bvsrem :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvsmod"
z3_mk_bvsmod :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvult"
z3_mk_bvult :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvslt"
z3_mk_bvslt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvule"
z3_mk_bvule :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvsle"
z3_mk_bvsle :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvuge"
z3_mk_bvuge :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvsge"
z3_mk_bvsge :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvugt"
z3_mk_bvugt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvsgt"
z3_mk_bvsgt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_concat"
z3_mk_concat :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_extract"
z3_mk_extract :: Ptr Z3_context -> CUInt -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_sign_ext"
z3_mk_sign_ext :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_zero_ext"
z3_mk_zero_ext :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_repeat"
z3_mk_repeat :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvshl"
z3_mk_bvshl :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvlshr"
z3_mk_bvlshr :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvashr"
z3_mk_bvashr :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_rotate_left"
z3_mk_rotate_left :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_rotate_right"
z3_mk_rotate_right :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_ext_rotate_left"
z3_mk_ext_rotate_left :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_ext_rotate_right"
z3_mk_ext_rotate_right :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_int2bv"
z3_mk_int2bv :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bv2int"
z3_mk_bv2int :: Ptr Z3_context -> Ptr Z3_ast -> Z3_bool -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvadd_no_overflow"
z3_mk_bvadd_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Z3_bool -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvadd_no_underflow"
z3_mk_bvadd_no_underflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvsub_no_overflow"
z3_mk_bvsub_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvsub_no_underflow"
z3_mk_bvsub_no_underflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvsdiv_no_overflow"
z3_mk_bvsdiv_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvneg_no_overflow"
z3_mk_bvneg_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvmul_no_overflow"
z3_mk_bvmul_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Z3_bool -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_bvmul_no_underflow"
z3_mk_bvmul_no_underflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_select"
z3_mk_select :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_store"
z3_mk_store :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_const_array"
z3_mk_const_array :: Ptr Z3_context -> Ptr Z3_sort -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_map"
z3_mk_map :: Ptr Z3_context -> Ptr Z3_func_decl -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_array_default"
z3_mk_array_default :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_empty_set"
z3_mk_empty_set :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_full_set"
z3_mk_full_set :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_set_add"
z3_mk_set_add :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_set_del"
z3_mk_set_del :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_set_union"
z3_mk_set_union :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_set_intersect"
z3_mk_set_intersect :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_set_difference"
z3_mk_set_difference :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_set_complement"
z3_mk_set_complement :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_set_member"
z3_mk_set_member :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_set_subset"
z3_mk_set_subset :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_numeral"
z3_mk_numeral :: Ptr Z3_context -> Z3_string -> Ptr Z3_sort -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_real"
z3_mk_real :: Ptr Z3_context -> CInt -> CInt -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_int"
z3_mk_int :: Ptr Z3_context -> CInt -> Ptr Z3_sort -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_unsigned_int"
z3_mk_unsigned_int :: Ptr Z3_context -> CUInt -> Ptr Z3_sort -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_int64"
z3_mk_int64 :: Ptr Z3_context -> CLLong -> Ptr Z3_sort -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_unsigned_int64"
z3_mk_unsigned_int64 :: Ptr Z3_context -> CULLong -> Ptr Z3_sort -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_pattern"
z3_mk_pattern :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_pattern)
foreign import ccall unsafe "Z3_mk_bound"
z3_mk_bound :: Ptr Z3_context -> CUInt -> Ptr Z3_sort -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_forall"
z3_mk_forall :: Ptr Z3_context -> CUInt
-> CUInt -> Ptr (Ptr Z3_pattern)
-> CUInt -> Ptr (Ptr Z3_sort) -> Ptr (Ptr Z3_symbol)
-> Ptr Z3_ast
-> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_exists"
z3_mk_exists :: Ptr Z3_context -> CUInt
-> CUInt -> Ptr (Ptr Z3_pattern)
-> CUInt -> Ptr (Ptr Z3_sort) -> Ptr (Ptr Z3_symbol)
-> Ptr Z3_ast
-> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_forall_const"
z3_mk_forall_const :: Ptr Z3_context
-> CUInt
-> CUInt
-> Ptr (Ptr Z3_app)
-> CUInt
-> Ptr (Ptr Z3_pattern)
-> Ptr Z3_ast
-> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_exists_const"
z3_mk_exists_const :: Ptr Z3_context
-> CUInt
-> CUInt
-> Ptr (Ptr Z3_app)
-> CUInt
-> Ptr (Ptr Z3_pattern)
-> Ptr Z3_ast
-> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_func_decl_to_ast"
z3_func_decl_to_ast :: Ptr Z3_context -> Ptr Z3_func_decl -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_get_ast_kind"
z3_get_ast_kind :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_ast_kind
foreign import ccall unsafe "Z3_is_app"
z3_is_app :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_bool
foreign import ccall unsafe "Z3_get_app_num_args"
z3_get_app_num_args :: Ptr Z3_context -> Ptr Z3_app -> IO CUInt
foreign import ccall unsafe "Z3_get_app_arg"
z3_get_app_arg :: Ptr Z3_context -> Ptr Z3_app -> CUInt -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_get_app_decl"
z3_get_app_decl :: Ptr Z3_context -> Ptr Z3_app -> IO (Ptr Z3_func_decl)
foreign import ccall unsafe "Z3_get_datatype_sort_num_constructors"
z3_get_datatype_sort_num_constructors :: Ptr Z3_context -> Ptr Z3_sort -> IO CUInt
foreign import ccall unsafe "Z3_get_datatype_sort_constructor"
z3_get_datatype_sort_constructor :: Ptr Z3_context -> Ptr Z3_sort -> CUInt -> IO (Ptr Z3_func_decl)
foreign import ccall unsafe "Z3_get_datatype_sort_recognizer"
z3_get_datatype_sort_recognizer :: Ptr Z3_context -> Ptr Z3_sort -> CUInt -> IO (Ptr Z3_func_decl)
foreign import ccall unsafe "Z3_get_datatype_sort_constructor_accessor"
z3_get_datatype_sort_constructor_accessor :: Ptr Z3_context -> Ptr Z3_sort -> CUInt -> CUInt -> IO (Ptr Z3_func_decl)
foreign import ccall unsafe "Z3_get_decl_name"
z3_get_decl_name :: Ptr Z3_context -> Ptr Z3_func_decl -> IO (Ptr Z3_symbol)
foreign import ccall unsafe "Z3_get_symbol_string"
z3_get_symbol_string :: Ptr Z3_context -> Ptr Z3_symbol -> IO Z3_string
foreign import ccall unsafe "Z3_get_sort_kind"
z3_get_sort_kind :: Ptr Z3_context -> Ptr Z3_sort -> IO Z3_sort_kind
foreign import ccall unsafe "Z3_get_bv_sort_size"
z3_get_bv_sort_size :: Ptr Z3_context -> Ptr Z3_sort -> IO CUInt
foreign import ccall unsafe "Z3_app_to_ast"
z3_app_to_ast :: Ptr Z3_context -> Ptr Z3_app -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_get_sort"
z3_get_sort :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_sort)
foreign import ccall unsafe "Z3_get_array_sort_domain"
z3_get_array_sort_domain :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_sort)
foreign import ccall unsafe "Z3_get_array_sort_range"
z3_get_array_sort_range :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_sort)
foreign import ccall unsafe "Z3_get_bool_value"
z3_get_bool_value :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_lbool
foreign import ccall unsafe "Z3_get_numeral_string"
z3_get_numeral_string :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_string
foreign import ccall unsafe "Z3_get_arity"
z3_get_arity :: Ptr Z3_context -> Ptr Z3_func_decl -> IO CUInt
foreign import ccall unsafe "Z3_get_domain"
z3_get_domain :: Ptr Z3_context -> Ptr Z3_func_decl -> CUInt -> IO (Ptr Z3_sort)
foreign import ccall unsafe "Z3_get_range"
z3_get_range :: Ptr Z3_context -> Ptr Z3_func_decl -> IO (Ptr Z3_sort)
foreign import ccall unsafe "Z3_to_app"
z3_to_app :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_app)
foreign import ccall unsafe "Z3_pattern_to_ast"
z3_pattern_to_ast :: Ptr Z3_context -> Ptr Z3_pattern -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_simplify"
z3_simplify :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_simplify_ex"
z3_simplify_ex :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_params -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_is_quantifier_forall"
z3_is_quantifier_forall :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_bool
foreign import ccall unsafe "Z3_get_quantifier_weight"
z3_get_quantifier_weight :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt
foreign import ccall unsafe "Z3_get_quantifier_num_patterns"
z3_get_quantifier_num_patterns :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt
foreign import ccall unsafe "Z3_get_quantifier_pattern_ast"
z3_get_quantifier_pattern_ast :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_get_quantifier_num_no_patterns"
z3_get_quantifier_num_no_patterns :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt
foreign import ccall unsafe "Z3_get_quantifier_no_pattern_ast"
z3_get_quantifier_no_pattern_ast :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_get_quantifier_num_bound"
z3_get_quantifier_num_bound :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt
foreign import ccall unsafe "Z3_get_quantifier_bound_name"
z3_get_quantifier_bound_name :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> IO (Ptr Z3_symbol)
foreign import ccall unsafe "Z3_get_quantifier_bound_sort"
z3_get_quantifier_bound_sort :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> IO (Ptr Z3_sort)
foreign import ccall unsafe "Z3_get_quantifier_body"
z3_get_quantifier_body :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_substitute_vars"
z3_substitute_vars :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_ast_vector_size"
z3_ast_vector_size :: Ptr Z3_context -> Ptr Z3_ast_vector -> IO CUInt
foreign import ccall unsafe "Z3_ast_vector_get"
z3_ast_vector_get :: Ptr Z3_context -> Ptr Z3_ast_vector -> CUInt -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_ast_vector_inc_ref"
z3_ast_vector_inc_ref :: Ptr Z3_context -> Ptr Z3_ast_vector -> IO ()
foreign import ccall unsafe "Z3_ast_vector_dec_ref"
z3_ast_vector_dec_ref :: Ptr Z3_context -> Ptr Z3_ast_vector -> IO ()
foreign import ccall unsafe "Z3_model_inc_ref"
z3_model_inc_ref :: Ptr Z3_context
-> Ptr Z3_model
-> IO ()
foreign import ccall unsafe "Z3_model_dec_ref"
z3_model_dec_ref :: Ptr Z3_context
-> Ptr Z3_model
-> IO ()
foreign import ccall unsafe "Z3_model_eval"
z3_model_eval :: Ptr Z3_context
-> Ptr Z3_model
-> Ptr Z3_ast
-> Z3_bool
-> Ptr (Ptr Z3_ast)
-> IO Z3_bool
foreign import ccall unsafe "Z3_is_as_array"
z3_is_as_array :: Ptr Z3_context
-> Ptr Z3_ast
-> IO Z3_bool
foreign import ccall unsafe "Z3_get_as_array_func_decl"
z3_get_as_array_func_decl :: Ptr Z3_context
-> Ptr Z3_ast
-> IO (Ptr Z3_func_decl)
foreign import ccall unsafe "Z3_model_get_func_interp"
z3_model_get_func_interp :: Ptr Z3_context
-> Ptr Z3_model
-> Ptr Z3_func_decl
-> IO (Ptr Z3_func_interp)
foreign import ccall unsafe "Z3_func_interp_inc_ref"
z3_func_interp_inc_ref :: Ptr Z3_context
-> Ptr Z3_func_interp
-> IO ()
foreign import ccall unsafe "Z3_func_interp_dec_ref"
z3_func_interp_dec_ref :: Ptr Z3_context
-> Ptr Z3_func_interp
-> IO ()
foreign import ccall unsafe "Z3_func_interp_get_num_entries"
z3_func_interp_get_num_entries :: Ptr Z3_context
-> Ptr Z3_func_interp
-> IO CUInt
foreign import ccall unsafe "Z3_func_interp_get_entry"
z3_func_interp_get_entry :: Ptr Z3_context
-> Ptr Z3_func_interp
-> CUInt
-> IO (Ptr Z3_func_entry)
foreign import ccall unsafe "Z3_func_interp_get_else"
z3_func_interp_get_else :: Ptr Z3_context
-> Ptr Z3_func_interp
-> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_func_interp_get_arity"
z3_func_interp_get_arity :: Ptr Z3_context
-> Ptr Z3_func_interp
-> IO CUInt
foreign import ccall unsafe "Z3_func_entry_inc_ref"
z3_func_entry_inc_ref :: Ptr Z3_context
-> Ptr Z3_func_entry
-> IO ()
foreign import ccall unsafe "Z3_func_entry_dec_ref"
z3_func_entry_dec_ref :: Ptr Z3_context
-> Ptr Z3_func_entry
-> IO ()
foreign import ccall unsafe "Z3_func_entry_get_value"
z3_func_entry_get_value :: Ptr Z3_context
-> Ptr Z3_func_entry
-> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_func_entry_get_num_args"
z3_func_entry_get_num_args :: Ptr Z3_context
-> Ptr Z3_func_entry
-> IO CUInt
foreign import ccall unsafe "Z3_func_entry_get_arg"
z3_func_entry_get_arg :: Ptr Z3_context
-> Ptr Z3_func_entry
-> CUInt
-> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_get_index_value"
z3_get_index_value :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt
foreign import ccall unsafe "Z3_model_to_string"
z3_model_to_string :: Ptr Z3_context -> Ptr Z3_model -> IO Z3_string
foreign import ccall unsafe "Z3_mk_params"
z3_mk_params :: Ptr Z3_context -> IO (Ptr Z3_params)
foreign import ccall unsafe "Z3_params_inc_ref"
z3_params_inc_ref :: Ptr Z3_context -> Ptr Z3_params -> IO ()
foreign import ccall unsafe "Z3_params_dec_ref"
z3_params_dec_ref :: Ptr Z3_context -> Ptr Z3_params -> IO ()
foreign import ccall unsafe "Z3_params_set_bool"
z3_params_set_bool :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol ->
Z3_bool -> IO ()
foreign import ccall unsafe "Z3_params_set_uint"
z3_params_set_uint :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol ->
CUInt -> IO ()
foreign import ccall unsafe "Z3_params_set_double"
z3_params_set_double :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol ->
CDouble -> IO ()
foreign import ccall unsafe "Z3_params_set_symbol"
z3_params_set_symbol :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol ->
Ptr Z3_symbol -> IO ()
foreign import ccall unsafe "Z3_params_to_string"
z3_params_to_string :: Ptr Z3_context -> Ptr Z3_params -> IO Z3_string
foreign import ccall unsafe "Z3_mk_interpolant"
z3_mk_interpolant :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_interpolation_context"
z3_mk_interpolation_context :: Ptr Z3_config -> IO (Ptr Z3_context)
foreign import ccall unsafe "Z3_get_interpolant"
z3_get_interpolant :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast
-> Ptr Z3_params -> IO (Ptr Z3_ast_vector)
foreign import ccall unsafe "Z3_compute_interpolant"
z3_compute_interpolant :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_params
-> Ptr (Ptr Z3_ast_vector) -> Ptr (Ptr Z3_model)
-> IO Z3_lbool
foreign import ccall unsafe "Z3_read_interpolation_problem"
z3_read_interpolation_problem :: Ptr Z3_context -> Ptr CUInt -> Ptr (Ptr Z3_ast)
-> Ptr (Ptr CUInt) -> Ptr CChar -> Ptr Z3_string
-> Ptr CUInt -> Ptr (Ptr Z3_ast) -> IO Z3_bool
foreign import ccall unsafe "Z3_check_interpolant"
z3_check_interpolant :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> Ptr CUInt
-> Ptr (Ptr Z3_ast) -> Ptr Z3_string -> CUInt
-> Ptr (Ptr Z3_ast) -> IO Z3_lbool
foreign import ccall unsafe "Z3_interpolation_profile"
z3_interpolation_profile :: Ptr Z3_context -> IO Z3_string
foreign import ccall unsafe "Z3_write_interpolation_problem"
z3_write_interpolation_problem :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast)
-> Ptr CUInt -> Ptr CChar -> CUInt
-> Ptr (Ptr Z3_ast) -> IO ()
foreign import ccall unsafe "Z3_mk_tactic"
z3_mk_tactic :: Ptr Z3_context -> Ptr CChar -> IO (Ptr Z3_tactic)
foreign import ccall unsafe "Z3_tactic_and_then"
z3_tactic_and_then :: Ptr Z3_context -> Ptr Z3_tactic -> Ptr Z3_tactic -> IO (Ptr Z3_tactic)
foreign import ccall unsafe "Z3_tactic_or_else"
z3_tactic_or_else :: Ptr Z3_context -> Ptr Z3_tactic -> Ptr Z3_tactic -> IO (Ptr Z3_tactic)
foreign import ccall unsafe "Z3_tactic_skip"
z3_tactic_skip :: Ptr Z3_context -> IO (Ptr Z3_tactic)
foreign import ccall unsafe "Z3_tactic_try_for"
z3_tactic_try_for :: Ptr Z3_context -> Ptr Z3_tactic -> CUInt -> IO (Ptr Z3_tactic)
foreign import ccall unsafe "Z3_tactic_inc_ref"
z3_tactic_inc_ref :: Ptr Z3_context -> Ptr Z3_tactic -> IO ()
foreign import ccall unsafe "Z3_tactic_dec_ref"
z3_tactic_dec_ref :: Ptr Z3_context -> Ptr Z3_tactic -> IO ()
foreign import ccall unsafe "Z3_tactic_apply"
z3_tactic_apply :: Ptr Z3_context -> Ptr Z3_tactic -> Ptr Z3_goal -> IO (Ptr Z3_apply_result)
foreign import ccall unsafe "Z3_apply_result_inc_ref"
z3_apply_result_inc_ref :: Ptr Z3_context -> Ptr Z3_apply_result -> IO ()
foreign import ccall unsafe "Z3_apply_result_dec_ref"
z3_apply_result_dec_ref :: Ptr Z3_context -> Ptr Z3_apply_result -> IO ()
foreign import ccall unsafe "Z3_apply_result_get_num_subgoals"
z3_apply_result_get_num_subgoals :: Ptr Z3_context -> Ptr Z3_apply_result -> IO CUInt
foreign import ccall unsafe "Z3_apply_result_get_subgoal"
z3_apply_result_get_subgoal :: Ptr Z3_context -> Ptr Z3_apply_result -> CUInt -> IO (Ptr Z3_goal)
foreign import ccall unsafe "Z3_mk_goal"
z3_mk_goal :: Ptr Z3_context -> Z3_bool -> Z3_bool -> Z3_bool -> IO (Ptr Z3_goal)
foreign import ccall unsafe "Z3_goal_inc_ref"
z3_goal_inc_ref :: Ptr Z3_context -> Ptr Z3_goal -> IO ()
foreign import ccall unsafe "Z3_goal_dec_ref"
z3_goal_dec_ref :: Ptr Z3_context -> Ptr Z3_goal -> IO ()
foreign import ccall unsafe "Z3_goal_assert"
z3_goal_assert :: Ptr Z3_context -> Ptr Z3_goal -> Ptr Z3_ast -> IO ()
foreign import ccall unsafe "Z3_goal_size"
z3_goal_size :: Ptr Z3_context -> Ptr Z3_goal -> IO CUInt
foreign import ccall unsafe "Z3_goal_formula"
z3_goal_formula :: Ptr Z3_context -> Ptr Z3_goal -> CUInt -> IO (Ptr Z3_ast)
foreign import ccall unsafe "Z3_mk_solver"
z3_mk_solver :: Ptr Z3_context -> IO (Ptr Z3_solver)
foreign import ccall unsafe "Z3_mk_simple_solver"
z3_mk_simple_solver :: Ptr Z3_context -> IO (Ptr Z3_solver)
foreign import ccall unsafe "Z3_mk_solver_for_logic"
z3_mk_solver_for_logic :: Ptr Z3_context -> Ptr Z3_symbol -> IO (Ptr Z3_solver)
foreign import ccall unsafe "Z3_solver_get_help"
z3_solver_get_help :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_string
foreign import ccall unsafe "Z3_solver_set_params"
z3_solver_set_params :: Ptr Z3_context -> Ptr Z3_solver -> Ptr Z3_params ->
IO ()
foreign import ccall unsafe "Z3_solver_inc_ref"
z3_solver_inc_ref :: Ptr Z3_context -> Ptr Z3_solver -> IO ()
foreign import ccall unsafe "Z3_solver_dec_ref"
z3_solver_dec_ref :: Ptr Z3_context -> Ptr Z3_solver -> IO ()
foreign import ccall unsafe "Z3_solver_push"
z3_solver_push :: Ptr Z3_context -> Ptr Z3_solver -> IO ()
foreign import ccall unsafe "Z3_solver_pop"
z3_solver_pop :: Ptr Z3_context -> Ptr Z3_solver -> CUInt -> IO ()
foreign import ccall unsafe "Z3_solver_get_num_scopes"
z3_solver_get_num_scopes :: Ptr Z3_context -> Ptr Z3_solver -> IO CUInt
foreign import ccall unsafe "Z3_solver_reset"
z3_solver_reset :: Ptr Z3_context -> Ptr Z3_solver -> IO ()
foreign import ccall unsafe "Z3_solver_assert"
z3_solver_assert :: Ptr Z3_context -> Ptr Z3_solver -> Ptr Z3_ast -> IO ()
foreign import ccall unsafe "Z3_solver_assert_and_track"
z3_solver_assert_and_track :: Ptr Z3_context -> Ptr Z3_solver ->
Ptr Z3_ast -> Ptr Z3_ast -> IO ()
foreign import ccall unsafe "Z3_solver_check"
z3_solver_check :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_lbool
foreign import ccall unsafe "Z3_solver_check_assumptions"
z3_solver_check_assumptions :: Ptr Z3_context -> Ptr Z3_solver -> CUInt -> Ptr (Ptr Z3_ast) -> IO Z3_lbool
foreign import ccall unsafe "Z3_solver_get_model"
z3_solver_get_model :: Ptr Z3_context -> Ptr Z3_solver -> IO (Ptr Z3_model)
foreign import ccall unsafe "Z3_solver_get_unsat_core"
z3_solver_get_unsat_core :: Ptr Z3_context -> Ptr Z3_solver -> IO (Ptr Z3_ast_vector)
foreign import ccall unsafe "Z3_solver_get_reason_unknown"
z3_solver_get_reason_unknown :: Ptr Z3_context -> Ptr Z3_solver ->
IO Z3_string
foreign import ccall unsafe "Z3_solver_to_string"
z3_solver_to_string :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_string
foreign import ccall unsafe "Z3_set_ast_print_mode"
z3_set_ast_print_mode :: Ptr Z3_context -> Z3_ast_print_mode -> IO ()
foreign import ccall unsafe "Z3_ast_to_string"
z3_ast_to_string :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_string
foreign import ccall unsafe "Z3_pattern_to_string"
z3_pattern_to_string :: Ptr Z3_context -> Ptr Z3_pattern -> IO Z3_string
foreign import ccall unsafe "Z3_sort_to_string"
z3_sort_to_string :: Ptr Z3_context -> Ptr Z3_sort -> IO Z3_string
foreign import ccall unsafe "Z3_func_decl_to_string"
z3_func_decl_to_string :: Ptr Z3_context -> Ptr Z3_func_decl -> IO Z3_string
foreign import ccall unsafe "Z3_benchmark_to_smtlib_string"
z3_benchmark_to_smtlib_string :: Ptr Z3_context
-> Z3_string
-> Z3_string
-> Z3_string
-> Z3_string
-> CUInt
-> Ptr (Ptr Z3_ast)
-> Ptr Z3_ast
-> IO Z3_string
foreign import ccall unsafe "Z3_get_error_code"
z3_get_error_code :: Ptr Z3_context -> IO Z3_error_code
foreign import ccall unsafe "Z3_set_error_handler"
z3_set_error_handler :: Ptr Z3_context -> FunPtr Z3_error_handler -> IO ()
foreign import ccall unsafe "Z3_set_error"
z3_set_error :: Ptr Z3_context -> Z3_error_code -> IO ()
foreign import ccall unsafe "Z3_get_error_msg"
z3_get_error_msg :: Z3_error_code -> IO Z3_string
foreign import ccall unsafe "Z3_get_error_msg_ex"
z3_get_error_msg_ex :: Ptr Z3_context -> Z3_error_code -> IO Z3_string
foreign import ccall unsafe "Z3_get_version"
z3_get_version :: Ptr CUInt -> Ptr CUInt -> Ptr CUInt -> Ptr CUInt -> IO ()