{-# LANGUAGE EmptyDataDecls #-} -- | -- Module : Z3.Base.C -- Copyright : (c) Iago Abal, 2012-2014 -- (c) David Castro, 2012-2013 -- License : BSD3 -- Maintainer: Iago Abal , -- David Castro -- -- Z3 API foreign imports. {- HACKING Add here the foreign import to support a new API function: * Take a look to a few others foreign imports and follow the same coding style. * 2-space wide indentation, no tabs. * No trailing spaces, please. * ... * Place the foreign import in the right section, according to the Z3's API documentation. * Include a reference to the function's API documentation. -} module Z3.Base.C where import Foreign import Foreign.C.Types import Foreign.C.String #include --------------------------------------------------------------------- -- * 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_optimize data Z3_solver data Z3_params data Z3_ast_vector -- | Reference: newtype Z3_lbool = Z3_lbool CInt deriving Eq z3_l_true, z3_l_false, z3_l_undef :: Z3_lbool z3_l_true = Z3_lbool (#const Z3_L_TRUE) z3_l_false = Z3_lbool (#const Z3_L_FALSE) z3_l_undef = Z3_lbool (#const Z3_L_UNDEF) -- | Reference: newtype Z3_bool = Z3_bool CInt deriving Eq -- | Reference: type Z3_error_handler = Ptr Z3_context -> Z3_error_code -> IO () z3_true, z3_false :: Z3_bool -- | Reference: z3_true = Z3_bool(#const Z3_TRUE) -- | Reference: z3_false = Z3_bool(#const Z3_FALSE) -- | Reference: type Z3_string = CString -- | Reference: type Z3_ast_print_mode = CInt z3_print_smtlib_full :: Z3_ast_print_mode z3_print_smtlib_full = #const Z3_PRINT_SMTLIB_FULL z3_print_low_level :: Z3_ast_print_mode z3_print_low_level = #const Z3_PRINT_LOW_LEVEL z3_print_smtlib2_compliant :: Z3_ast_print_mode z3_print_smtlib2_compliant = #const Z3_PRINT_SMTLIB2_COMPLIANT -- | Reference: type Z3_error_code = CInt #{enum Z3_error_code, , z3_ok = Z3_OK , z3_sort_error = Z3_SORT_ERROR , z3_iob = Z3_IOB , z3_invalid_arg = Z3_INVALID_ARG , z3_parser_error = Z3_PARSER_ERROR , z3_no_parser = Z3_NO_PARSER , z3_invalid_pattern = Z3_INVALID_PATTERN , z3_memout_fail = Z3_MEMOUT_FAIL , z3_file_access_error = Z3_FILE_ACCESS_ERROR , z3_internal_fatal = Z3_INTERNAL_FATAL , z3_invalid_usage = Z3_INVALID_USAGE , z3_dec_ref_error = Z3_DEC_REF_ERROR , z3_exception = Z3_EXCEPTION } -- | Reference: type Z3_sort_kind = CInt z3_uninterpreted_sort :: Z3_sort_kind z3_uninterpreted_sort = #const Z3_UNINTERPRETED_SORT z3_bool_sort :: Z3_sort_kind z3_bool_sort = #const Z3_BOOL_SORT z3_int_sort :: Z3_sort_kind z3_int_sort = #const Z3_INT_SORT z3_real_sort :: Z3_sort_kind z3_real_sort = #const Z3_REAL_SORT z3_bv_sort :: Z3_sort_kind z3_bv_sort = #const Z3_BV_SORT z3_array_sort :: Z3_sort_kind z3_array_sort = #const Z3_ARRAY_SORT z3_datatype_sort :: Z3_sort_kind z3_datatype_sort = #const Z3_DATATYPE_SORT z3_relation_sort :: Z3_sort_kind z3_relation_sort = #const Z3_RELATION_SORT z3_finite_domain_sort :: Z3_sort_kind z3_finite_domain_sort = #const Z3_FINITE_DOMAIN_SORT z3_floating_point_sort :: Z3_sort_kind z3_floating_point_sort = #const Z3_FLOATING_POINT_SORT z3_rounding_mode_sort :: Z3_sort_kind z3_rounding_mode_sort = #const Z3_ROUNDING_MODE_SORT z3_unknown_sort :: Z3_sort_kind z3_unknown_sort = #const Z3_UNKNOWN_SORT -- | Reference: type Z3_ast_kind = CInt z3_numeral_ast :: Z3_ast_kind z3_numeral_ast = #const Z3_NUMERAL_AST z3_app_ast :: Z3_ast_kind z3_app_ast = #const Z3_APP_AST z3_var_ast :: Z3_ast_kind z3_var_ast = #const Z3_VAR_AST z3_quantifier_ast :: Z3_ast_kind z3_quantifier_ast = #const Z3_QUANTIFIER_AST z3_sort_ast :: Z3_ast_kind z3_sort_ast = #const Z3_SORT_AST z3_func_decl_ast :: Z3_ast_kind z3_func_decl_ast = #const Z3_FUNC_DECL_AST z3_unknown_ast :: Z3_ast_kind z3_unknown_ast = #const Z3_UNKNOWN_AST --------------------------------------------------------------------- -- * Create configuration -- | Reference: foreign import ccall unsafe "Z3_mk_config" z3_mk_config :: IO (Ptr Z3_config) -- | Reference: foreign import ccall unsafe "Z3_del_config" z3_del_config :: Ptr Z3_config -> IO () -- | Reference: foreign import ccall unsafe "Z3_set_param_value" z3_set_param_value :: Ptr Z3_config -> Z3_string -> Z3_string -> IO () --------------------------------------------------------------------- -- * Create context -- | Reference: foreign import ccall unsafe "Z3_mk_context_rc" z3_mk_context_rc :: Ptr Z3_config -> IO (Ptr Z3_context) -- | Reference: foreign import ccall unsafe "Z3_del_context" z3_del_context :: Ptr Z3_context -> IO () -- | Reference: foreign import ccall unsafe "Z3_inc_ref" z3_inc_ref :: Ptr Z3_context -> Ptr Z3_ast -> IO () -- | Reference: foreign import ccall unsafe "Z3_dec_ref" z3_dec_ref :: Ptr Z3_context -> Ptr Z3_ast -> IO () --------------------------------------------------------------------- -- * Symbols -- | Reference: foreign import ccall unsafe "Z3_mk_int_symbol" z3_mk_int_symbol :: Ptr Z3_context -> CInt -> IO (Ptr Z3_symbol) -- | Reference: foreign import ccall unsafe "Z3_mk_string_symbol" z3_mk_string_symbol :: Ptr Z3_context -> Z3_string -> IO (Ptr Z3_symbol) --------------------------------------------------------------------- -- * Sorts -- | Reference: foreign import ccall unsafe "Z3_sort_to_ast" z3_sort_to_ast :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast) -- TODO Sorts: Z3_is_eq_sort -- | Reference: foreign import ccall unsafe "Z3_mk_uninterpreted_sort" z3_mk_uninterpreted_sort :: Ptr Z3_context -> Ptr Z3_symbol -> IO (Ptr Z3_sort) -- | Reference: foreign import ccall unsafe "Z3_mk_bool_sort" z3_mk_bool_sort :: Ptr Z3_context -> IO (Ptr Z3_sort) -- | Reference: foreign import ccall unsafe "Z3_mk_int_sort" z3_mk_int_sort :: Ptr Z3_context -> IO (Ptr Z3_sort) -- | Reference: foreign import ccall unsafe "Z3_mk_real_sort" z3_mk_real_sort :: Ptr Z3_context -> IO (Ptr Z3_sort) -- | Reference: foreign import ccall unsafe "Z3_mk_finite_domain_sort" z3_mk_finite_domain_sort :: Ptr Z3_context -> Ptr Z3_symbol -> CULLong -> IO (Ptr Z3_sort) -- | Reference: foreign import ccall unsafe "Z3_mk_bv_sort" z3_mk_bv_sort :: Ptr Z3_context -> CUInt -> IO (Ptr Z3_sort) -- | Reference: foreign import ccall unsafe "Z3_mk_array_sort" z3_mk_array_sort :: Ptr Z3_context -> Ptr Z3_sort -- ^ domain -> Ptr Z3_sort -- ^ range -> IO (Ptr Z3_sort) -- | Reference: 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) -- | Reference 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) -- | Reference foreign import ccall unsafe "Z3_del_constructor" z3_del_constructor :: Ptr Z3_context -> Ptr Z3_constructor -> IO () -- | Reference: 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) -- | Reference 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) -- | Reference foreign import ccall unsafe "Z3_del_constructor_list" z3_del_constructor_list :: Ptr Z3_context -> Ptr (Z3_constructor_list) -> IO () -- | Reference: 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 () -- | Reference: foreign import ccall unsafe "Z3_mk_set_sort" z3_mk_set_sort :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_sort) -- TODO Sorts: from Z3_mk_array_sort on --------------------------------------------------------------------- -- * Constants and Applications -- | Reference: 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) -- | Reference: 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) -- | Reference: foreign import ccall unsafe "Z3_mk_const" z3_mk_const :: Ptr Z3_context -> Ptr Z3_symbol -> Ptr Z3_sort -> IO (Ptr Z3_ast) -- Reference: foreign import ccall unsafe "Z3_mk_fresh_const" z3_mk_fresh_const :: Ptr Z3_context -> Z3_string -> Ptr Z3_sort -> IO (Ptr Z3_ast) -- Reference: 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) --------------------------------------------------------------------- -- * Propositional Logic and Equality -- | Reference: foreign import ccall unsafe "Z3_mk_true" z3_mk_true :: Ptr Z3_context -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_false" z3_mk_false :: Ptr Z3_context -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_eq" z3_mk_eq :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_distinct" z3_mk_distinct :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_not" z3_mk_not :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: 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) -- | Reference: foreign import ccall unsafe "Z3_mk_iff" z3_mk_iff :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_implies" z3_mk_implies :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_xor" z3_mk_xor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_and" z3_mk_and :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_or" z3_mk_or :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) --------------------------------------------------------------------- -- * Arithmetic: Integers and Reals -- | Reference: foreign import ccall unsafe "Z3_mk_add" z3_mk_add :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_mul" z3_mk_mul :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_sub" z3_mk_sub :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_unary_minus" z3_mk_unary_minus :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_div" z3_mk_div :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_mod" z3_mk_mod :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_rem" z3_mk_rem :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_lt" z3_mk_lt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_le" z3_mk_le :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_gt" z3_mk_gt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_ge" z3_mk_ge :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_int2real" z3_mk_int2real :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_real2int" z3_mk_real2int :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_is_int" z3_mk_is_int :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --------------------------------------------------------------------- -- * Bit-vectors -- | Reference: foreign import ccall unsafe "Z3_mk_bvnot" z3_mk_bvnot :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_bvredand" z3_mk_bvredand :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_bvredor" z3_mk_bvredor :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_bvand" z3_mk_bvand :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_bvor" z3_mk_bvor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_bvxor" z3_mk_bvxor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_bvnand" z3_mk_bvnand :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_bvnor" z3_mk_bvnor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_bvxnor" z3_mk_bvxnor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_bvadd" z3_mk_bvadd :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_bvsub" z3_mk_bvsub :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_bvmul" z3_mk_bvmul :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_bvudiv" z3_mk_bvudiv :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_bvsdiv" z3_mk_bvsdiv :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_bvurem" z3_mk_bvurem :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_bvsrem" z3_mk_bvsrem :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_bvsmod" z3_mk_bvsmod :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_bvult" z3_mk_bvult :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_bvslt" z3_mk_bvslt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_bvule" z3_mk_bvule :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_bvsle" z3_mk_bvsle :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_bvuge" z3_mk_bvuge :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_bvsge" z3_mk_bvsge :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_bvugt" z3_mk_bvugt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_bvsgt" z3_mk_bvsgt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_concat" z3_mk_concat :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_extract" z3_mk_extract :: Ptr Z3_context -> CUInt -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_sign_ext" z3_mk_sign_ext :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_zero_ext" z3_mk_zero_ext :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_repeat" z3_mk_repeat :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_bvshl" z3_mk_bvshl :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_bvlshr" z3_mk_bvlshr :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_bvashr" z3_mk_bvashr :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_rotate_left" z3_mk_rotate_left :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_rotate_right" z3_mk_rotate_right :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: 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) -- | Reference: 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) -- | Reference: foreign import ccall unsafe "Z3_mk_int2bv" z3_mk_int2bv :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_bv2int" z3_mk_bv2int :: Ptr Z3_context -> Ptr Z3_ast -> Z3_bool -> IO (Ptr Z3_ast) -- | Reference: 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) -- | Reference: 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) -- | Reference: 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) -- | Reference: 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) -- | Reference: 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) -- | Reference: foreign import ccall unsafe "Z3_mk_bvneg_no_overflow" z3_mk_bvneg_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: 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) -- | Reference: 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) -------------------------------------------------------------------------------- -- * Arrays -- | Reference: foreign import ccall unsafe "Z3_mk_select" z3_mk_select :: Ptr Z3_context -> Ptr Z3_ast -- ^ aray -> Ptr Z3_ast -- ^ index -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_store" z3_mk_store :: Ptr Z3_context -> Ptr Z3_ast -- ^ array -> Ptr Z3_ast -- ^ index -> Ptr Z3_ast -- ^ value to store at array[index] -> IO (Ptr Z3_ast) -- | Reference: 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) -- | Reference: 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) -- | Reference: foreign import ccall unsafe "Z3_mk_array_default" z3_mk_array_default :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) -------------------------------------------------------------------------------- -- * Sets -- | Reference: foreign import ccall unsafe "Z3_mk_empty_set" z3_mk_empty_set :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_full_set" z3_mk_full_set :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast) -- | Reference: 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) -- | Reference: 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) -- | Reference: foreign import ccall unsafe "Z3_mk_set_union" z3_mk_set_union :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_set_intersect" z3_mk_set_intersect :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) -- | Reference: 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) -- | Reference: foreign import ccall unsafe "Z3_mk_set_complement" z3_mk_set_complement :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: 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) -- | Reference: 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) --------------------------------------------------------------------- -- * Numerals -- | Reference: foreign import ccall unsafe "Z3_mk_numeral" z3_mk_numeral :: Ptr Z3_context -> Z3_string -> Ptr Z3_sort -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_real" z3_mk_real :: Ptr Z3_context -> CInt -> CInt -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_int" z3_mk_int :: Ptr Z3_context -> CInt -> Ptr Z3_sort -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_unsigned_int" z3_mk_unsigned_int :: Ptr Z3_context -> CUInt -> Ptr Z3_sort -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_int64" z3_mk_int64 :: Ptr Z3_context -> CLLong -> Ptr Z3_sort -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_mk_unsigned_int64" z3_mk_unsigned_int64 :: Ptr Z3_context -> CULLong -> Ptr Z3_sort -> IO (Ptr Z3_ast) --------------------------------------------------------------------- -- * Sequences and regular expressions foreign import ccall unsafe "Z3_mk_seq_sort" z3_mk_seq_sort :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_sort) foreign import ccall unsafe "Z3_is_seq_sort" z3_is_seq_sort :: Ptr Z3_context -> Ptr Z3_sort -> IO Z3_bool foreign import ccall unsafe "Z3_mk_re_sort" z3_mk_re_sort :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_sort) foreign import ccall unsafe "Z3_is_re_sort" z3_is_re_sort :: Ptr Z3_context -> Ptr Z3_sort -> IO Z3_bool foreign import ccall unsafe "Z3_mk_string_sort" z3_mk_string_sort :: Ptr Z3_context -> IO (Ptr Z3_sort) foreign import ccall unsafe "Z3_is_string_sort" z3_is_string_sort :: Ptr Z3_context -> Ptr Z3_sort -> IO Z3_bool foreign import ccall unsafe "Z3_mk_string" z3_mk_string :: Ptr Z3_context -> Z3_string -> IO (Ptr Z3_ast) foreign import ccall unsafe "Z3_is_string" z3_is_string :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_bool foreign import ccall unsafe "Z3_get_string" z3_get_string :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_string foreign import ccall unsafe "Z3_mk_seq_empty" z3_mk_seq_empty :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast) foreign import ccall unsafe "Z3_mk_seq_unit" z3_mk_seq_unit :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) foreign import ccall unsafe "Z3_mk_seq_concat" z3_mk_seq_concat :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) foreign import ccall unsafe "Z3_mk_seq_prefix" z3_mk_seq_prefix :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) foreign import ccall unsafe "Z3_mk_seq_suffix" z3_mk_seq_suffix :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) foreign import ccall unsafe "Z3_mk_seq_contains" z3_mk_seq_contains :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) foreign import ccall unsafe "Z3_mk_seq_extract" z3_mk_seq_extract :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) foreign import ccall unsafe "Z3_mk_seq_replace" z3_mk_seq_replace :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) foreign import ccall unsafe "Z3_mk_seq_at" z3_mk_seq_at :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) foreign import ccall unsafe "Z3_mk_seq_length" z3_mk_seq_length :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) foreign import ccall unsafe "Z3_mk_seq_index" z3_mk_seq_index :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) foreign import ccall unsafe "Z3_mk_str_to_int" z3_mk_str_to_int :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) foreign import ccall unsafe "Z3_mk_int_to_str" z3_mk_int_to_str :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) foreign import ccall unsafe "Z3_mk_seq_to_re" z3_mk_seq_to_re :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) foreign import ccall unsafe "Z3_mk_seq_in_re" z3_mk_seq_in_re :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) foreign import ccall unsafe "Z3_mk_re_plus" z3_mk_re_plus :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) foreign import ccall unsafe "Z3_mk_re_star" z3_mk_re_star :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) foreign import ccall unsafe "Z3_mk_re_option" z3_mk_re_option :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) foreign import ccall unsafe "Z3_mk_re_union" z3_mk_re_union :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) foreign import ccall unsafe "Z3_mk_re_concat" z3_mk_re_concat :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) foreign import ccall unsafe "Z3_mk_re_range" z3_mk_re_range :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) foreign import ccall unsafe "Z3_mk_re_loop" z3_mk_re_loop :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> CUInt -> IO (Ptr Z3_ast) foreign import ccall unsafe "Z3_mk_re_intersect" z3_mk_re_intersect :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) foreign import ccall unsafe "Z3_mk_re_complement" z3_mk_re_complement :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) foreign import ccall unsafe "Z3_mk_re_empty" z3_mk_re_empty :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast) foreign import ccall unsafe "Z3_mk_re_full" z3_mk_re_full :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast) --------------------------------------------------------------------- -- * Quantifiers -- | Reference: foreign import ccall unsafe "Z3_mk_pattern" z3_mk_pattern :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_pattern) -- | Reference: foreign import ccall unsafe "Z3_mk_bound" z3_mk_bound :: Ptr Z3_context -> CUInt -> Ptr Z3_sort -> IO (Ptr Z3_ast) -- | Reference: 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) -- | Referece: 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) -- TODO: Z3_mk_quantifier, Z3_mk_quantifier_ex -- | Reference 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) -- | Reference: 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) -- TODO: Z3_mk_quantifier_const, Z3_mk_quantifier_const_ex --------------------------------------------------------------------- -- * Accessors -- | Reference: 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) -- | Reference: foreign import ccall unsafe "Z3_get_ast_kind" z3_get_ast_kind :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_ast_kind -- | Reference: foreign import ccall unsafe "Z3_is_app" z3_is_app :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_bool -- Reference: foreign import ccall unsafe "Z3_get_app_num_args" z3_get_app_num_args :: Ptr Z3_context -> Ptr Z3_app -> IO CUInt -- Reference: foreign import ccall unsafe "Z3_get_app_arg" z3_get_app_arg :: Ptr Z3_context -> Ptr Z3_app -> CUInt -> IO (Ptr Z3_ast) -- Reference: foreign import ccall unsafe "Z3_get_app_decl" z3_get_app_decl :: Ptr Z3_context -> Ptr Z3_app -> IO (Ptr Z3_func_decl) -- Reference: foreign import ccall unsafe "Z3_get_datatype_sort_num_constructors" z3_get_datatype_sort_num_constructors :: Ptr Z3_context -> Ptr Z3_sort -> IO CUInt -- Reference: 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) -- Reference: 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) -- Reference: 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) -- Reference: foreign import ccall unsafe "Z3_get_decl_name" z3_get_decl_name :: Ptr Z3_context -> Ptr Z3_func_decl -> IO (Ptr Z3_symbol) -- Reference: foreign import ccall unsafe "Z3_get_symbol_string" z3_get_symbol_string :: Ptr Z3_context -> Ptr Z3_symbol -> IO Z3_string -- Reference: foreign import ccall unsafe "Z3_get_sort_kind" z3_get_sort_kind :: Ptr Z3_context -> Ptr Z3_sort -> IO Z3_sort_kind -- | Reference: foreign import ccall unsafe "Z3_get_bv_sort_size" z3_get_bv_sort_size :: Ptr Z3_context -> Ptr Z3_sort -> IO CUInt -- | Reference: foreign import ccall unsafe "Z3_app_to_ast" z3_app_to_ast :: Ptr Z3_context -> Ptr Z3_app -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_get_sort" z3_get_sort :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_sort) -- | Reference: foreign import ccall unsafe "Z3_get_array_sort_domain" z3_get_array_sort_domain :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_sort) -- | Reference: foreign import ccall unsafe "Z3_get_array_sort_range" z3_get_array_sort_range :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_sort) -- | Reference: foreign import ccall unsafe "Z3_get_bool_value" z3_get_bool_value :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_lbool -- | Reference: foreign import ccall unsafe "Z3_get_numeral_string" z3_get_numeral_string :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_string -- | Reference: foreign import ccall unsafe "Z3_get_arity" z3_get_arity :: Ptr Z3_context -> Ptr Z3_func_decl -> IO CUInt -- | Reference: foreign import ccall unsafe "Z3_get_domain" z3_get_domain :: Ptr Z3_context -> Ptr Z3_func_decl -> CUInt -> IO (Ptr Z3_sort) -- | Reference: foreign import ccall unsafe "Z3_get_range" z3_get_range :: Ptr Z3_context -> Ptr Z3_func_decl -> IO (Ptr Z3_sort) -- | Reference: foreign import ccall unsafe "Z3_to_app" z3_to_app :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_app) -- | Reference: foreign import ccall unsafe "Z3_pattern_to_ast" z3_pattern_to_ast :: Ptr Z3_context -> Ptr Z3_pattern -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_simplify" z3_simplify :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_simplify_ex" z3_simplify_ex :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_params -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_is_quantifier_forall" z3_is_quantifier_forall :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_bool -- | Reference: foreign import ccall unsafe "Z3_get_quantifier_weight" z3_get_quantifier_weight :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt -- | Reference: foreign import ccall unsafe "Z3_get_quantifier_num_patterns" z3_get_quantifier_num_patterns :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt -- | Reference: 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) -- | Reference: foreign import ccall unsafe "Z3_get_quantifier_num_no_patterns" z3_get_quantifier_num_no_patterns :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt -- | Reference: 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) -- | Reference: foreign import ccall unsafe "Z3_get_quantifier_num_bound" z3_get_quantifier_num_bound :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt -- | Reference: 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) -- | Reference: 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) -- | Reference: foreign import ccall unsafe "Z3_get_quantifier_body" z3_get_quantifier_body :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --------------------------------------------------------------------- -- * Modifiers -- | Reference: 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) -- | Reference: foreign import ccall unsafe "Z3_substitute" z3_substitute :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> Ptr (Ptr Z3_ast) -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) --------------------------------------------------------------------- -- * AST vectors -- | Reference: foreign import ccall unsafe "Z3_ast_vector_size" z3_ast_vector_size :: Ptr Z3_context -> Ptr Z3_ast_vector -> IO CUInt -- | Reference: foreign import ccall unsafe "Z3_ast_vector_get" z3_ast_vector_get :: Ptr Z3_context -> Ptr Z3_ast_vector -> CUInt -> IO (Ptr Z3_ast) -- | Reference: foreign import ccall unsafe "Z3_ast_vector_inc_ref" z3_ast_vector_inc_ref :: Ptr Z3_context -> Ptr Z3_ast_vector -> IO () -- | Reference: foreign import ccall unsafe "Z3_ast_vector_dec_ref" z3_ast_vector_dec_ref :: Ptr Z3_context -> Ptr Z3_ast_vector -> IO () --------------------------------------------------------------------- -- * Models -- | Reference: foreign import ccall unsafe "Z3_model_inc_ref" z3_model_inc_ref :: Ptr Z3_context -> Ptr Z3_model -> IO () -- | Reference: foreign import ccall unsafe "Z3_model_dec_ref" z3_model_dec_ref :: Ptr Z3_context -> Ptr Z3_model -> IO () -- | Reference: 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 -- | Reference: https://z3prover.github.io/api/html/group__capi.html#ga01bc2993f3eb358f7bd3b2d2d4cf5e51 foreign import ccall unsafe "Z3_model_get_const_interp" z3_model_get_const_interp :: Ptr Z3_context -> Ptr Z3_model -> Ptr Z3_func_decl -> IO (Ptr Z3_ast) -- | Reference: https://z3prover.github.io/api/html/group__capi.html#gaf5e9adb229e98b29cbeb7cebf41433a3 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) -- | Reference: https://z3prover.github.io/api/html/group__capi.html#ga3c7f8f6ce7c9f30710d3b73fa091f6b3 foreign import ccall unsafe "Z3_model_has_interp" z3_model_has_interp :: Ptr Z3_context -> Ptr Z3_model -> Ptr Z3_func_decl -> IO Z3_bool -- | Reference: https://z3prover.github.io/api/html/group__capi.html#ga3ff26c1c0f55d17ebf2c152a74eac743 foreign import ccall unsafe "Z3_model_get_num_consts" z3_model_get_num_consts :: Ptr Z3_context -> Ptr Z3_model -> IO CUInt -- | Reference: https://z3prover.github.io/api/html/group__capi.html#gaab062a06c0789b432885f4813dd9633b foreign import ccall unsafe "Z3_model_get_num_funcs" z3_model_get_num_funcs :: Ptr Z3_context -> Ptr Z3_model -> IO CUInt -- | Reference: https://z3prover.github.io/api/html/group__capi.html#ga8e70ac56fe6748301b7776191395184a foreign import ccall unsafe "Z3_model_get_const_decl" z3_model_get_const_decl :: Ptr Z3_context -> Ptr Z3_model -> CUInt -> IO (Ptr Z3_func_decl) -- | Reference: https://z3prover.github.io/api/html/group__capi.html#ga2a1a4524289574ae34ce2eecdade84d7 foreign import ccall unsafe "Z3_model_get_func_decl" z3_model_get_func_decl :: Ptr Z3_context -> Ptr Z3_model -> CUInt -> IO (Ptr Z3_func_decl) -- | Reference: foreign import ccall unsafe "Z3_is_as_array" z3_is_as_array :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_bool -- | Reference: foreign import ccall unsafe "Z3_is_eq_ast" z3_is_eq_ast :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO Z3_bool -- | Reference: 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) -- | Reference: https://z3prover.github.io/api/html/group__capi.html#ga1f30176bce864257bebb1fb30a103779 foreign import ccall unsafe "Z3_add_func_interp" z3_add_func_interp :: Ptr Z3_context -> Ptr Z3_model -> Ptr Z3_func_decl -> Ptr Z3_ast -> IO (Ptr Z3_func_interp) -- | Reference: https://z3prover.github.io/api/html/group__capi.html#ga73b1de0ec17bb4f2e47d256a7628925c foreign import ccall unsafe "Z3_add_const_interp" z3_add_const_interp :: Ptr Z3_context -> Ptr Z3_model -> Ptr Z3_func_decl -> Ptr Z3_ast -> IO () -- | Reference: foreign import ccall unsafe "Z3_func_interp_inc_ref" z3_func_interp_inc_ref :: Ptr Z3_context -> Ptr Z3_func_interp -> IO () -- | Reference: foreign import ccall unsafe "Z3_func_interp_dec_ref" z3_func_interp_dec_ref :: Ptr Z3_context -> Ptr Z3_func_interp -> IO () -- | Reference: 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 -- | Reference: 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) -- | Reference: 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) -- | Reference: foreign import ccall unsafe "Z3_func_interp_get_arity" z3_func_interp_get_arity :: Ptr Z3_context -> Ptr Z3_func_interp -> IO CUInt -- | Reference: foreign import ccall unsafe "Z3_func_entry_inc_ref" z3_func_entry_inc_ref :: Ptr Z3_context -> Ptr Z3_func_entry -> IO () -- | Reference: foreign import ccall unsafe "Z3_func_entry_dec_ref" z3_func_entry_dec_ref :: Ptr Z3_context -> Ptr Z3_func_entry -> IO () -- | Reference: 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) -- | Reference: 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 -- | Reference: 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) --------------------------------------------------------------------- -- * Constraints -- TODO Constraints: Z3_get_num_scopes -- TODO Constraints: Z3_persist_ast -- TODO Constraints: Z3_check_assumptions -- TODO Constraints: Z3_get_implied_equalities -- | Reference: foreign import ccall unsafe "Z3_get_index_value" z3_get_index_value :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt -- | Reference: foreign import ccall unsafe "Z3_model_to_string" z3_model_to_string :: Ptr Z3_context -> Ptr Z3_model -> IO Z3_string -- TODO From section 'Constraints' on. --------------------------------------------------------------------- -- * Parameters -- | Reference: foreign import ccall unsafe "Z3_mk_params" z3_mk_params :: Ptr Z3_context -> IO (Ptr Z3_params) -- | Reference: foreign import ccall unsafe "Z3_params_inc_ref" z3_params_inc_ref :: Ptr Z3_context -> Ptr Z3_params -> IO () -- | Reference: foreign import ccall unsafe "Z3_params_dec_ref" z3_params_dec_ref :: Ptr Z3_context -> Ptr Z3_params -> IO () -- | Reference: foreign import ccall unsafe "Z3_params_set_bool" z3_params_set_bool :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol -> Z3_bool -> IO () -- | Reference: foreign import ccall unsafe "Z3_params_set_uint" z3_params_set_uint :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol -> CUInt -> IO () -- | Reference: foreign import ccall unsafe "Z3_params_set_double" z3_params_set_double :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol -> CDouble -> IO () -- | Reference: 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 () -- | Reference: foreign import ccall unsafe "Z3_params_to_string" z3_params_to_string :: Ptr Z3_context -> Ptr Z3_params -> IO Z3_string --------------------------------------------------------------------- -- * Tactics -- | Reference: foreign import ccall unsafe "Z3_mk_tactic" z3_mk_tactic :: Ptr Z3_context -> Ptr CChar -> IO (Ptr Z3_tactic) -- | Reference: 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) -- | Reference: 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) -- | Reference: foreign import ccall unsafe "Z3_tactic_skip" z3_tactic_skip :: Ptr Z3_context -> IO (Ptr Z3_tactic) -- | Reference: foreign import ccall unsafe "Z3_tactic_try_for" z3_tactic_try_for :: Ptr Z3_context -> Ptr Z3_tactic -> CUInt -> IO (Ptr Z3_tactic) -- | Reference: foreign import ccall unsafe "Z3_tactic_inc_ref" z3_tactic_inc_ref :: Ptr Z3_context -> Ptr Z3_tactic -> IO () -- | Reference: foreign import ccall unsafe "Z3_tactic_dec_ref" z3_tactic_dec_ref :: Ptr Z3_context -> Ptr Z3_tactic -> IO () -- | Reference: foreign import ccall unsafe "Z3_tactic_apply" z3_tactic_apply :: Ptr Z3_context -> Ptr Z3_tactic -> Ptr Z3_goal -> IO (Ptr Z3_apply_result) -- | Reference: foreign import ccall unsafe "Z3_apply_result_inc_ref" z3_apply_result_inc_ref :: Ptr Z3_context -> Ptr Z3_apply_result -> IO () -- | Reference: foreign import ccall unsafe "Z3_apply_result_dec_ref" z3_apply_result_dec_ref :: Ptr Z3_context -> Ptr Z3_apply_result -> IO () -- | Reference: 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 -- | Reference: 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) -- | Reference: foreign import ccall unsafe "Z3_mk_goal" z3_mk_goal :: Ptr Z3_context -> Z3_bool -> Z3_bool -> Z3_bool -> IO (Ptr Z3_goal) -- | Reference: foreign import ccall unsafe "Z3_goal_inc_ref" z3_goal_inc_ref :: Ptr Z3_context -> Ptr Z3_goal -> IO () -- | Reference: foreign import ccall unsafe "Z3_goal_dec_ref" z3_goal_dec_ref :: Ptr Z3_context -> Ptr Z3_goal -> IO () -- | Reference: foreign import ccall unsafe "Z3_goal_assert" z3_goal_assert :: Ptr Z3_context -> Ptr Z3_goal -> Ptr Z3_ast -> IO () -- | Reference: foreign import ccall unsafe "Z3_goal_size" z3_goal_size :: Ptr Z3_context -> Ptr Z3_goal -> IO CUInt -- | Reference: foreign import ccall unsafe "Z3_goal_formula" z3_goal_formula :: Ptr Z3_context -> Ptr Z3_goal -> CUInt -> IO (Ptr Z3_ast) --------------------------------------------------------------------- -- * Solvers -- | Reference: foreign import ccall unsafe "Z3_mk_solver" z3_mk_solver :: Ptr Z3_context -> IO (Ptr Z3_solver) -- | Reference: foreign import ccall unsafe "Z3_mk_simple_solver" z3_mk_simple_solver :: Ptr Z3_context -> IO (Ptr Z3_solver) -- | Reference: foreign import ccall unsafe "Z3_mk_solver_for_logic" z3_mk_solver_for_logic :: Ptr Z3_context -> Ptr Z3_symbol -> IO (Ptr Z3_solver) -- | Reference: foreign import ccall unsafe "Z3_solver_get_help" z3_solver_get_help :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_string -- | Reference: foreign import ccall unsafe "Z3_solver_set_params" z3_solver_set_params :: Ptr Z3_context -> Ptr Z3_solver -> Ptr Z3_params -> IO () -- | Reference: foreign import ccall unsafe "Z3_solver_inc_ref" z3_solver_inc_ref :: Ptr Z3_context -> Ptr Z3_solver -> IO () -- | Reference: foreign import ccall unsafe "Z3_solver_dec_ref" z3_solver_dec_ref :: Ptr Z3_context -> Ptr Z3_solver -> IO () -- | Reference: foreign import ccall unsafe "Z3_solver_push" z3_solver_push :: Ptr Z3_context -> Ptr Z3_solver -> IO () -- | Reference: foreign import ccall unsafe "Z3_solver_pop" z3_solver_pop :: Ptr Z3_context -> Ptr Z3_solver -> CUInt -> IO () -- | Reference: foreign import ccall unsafe "Z3_solver_get_num_scopes" z3_solver_get_num_scopes :: Ptr Z3_context -> Ptr Z3_solver -> IO CUInt -- | Reference: foreign import ccall unsafe "Z3_solver_reset" z3_solver_reset :: Ptr Z3_context -> Ptr Z3_solver -> IO () -- | Reference: foreign import ccall unsafe "Z3_solver_assert" z3_solver_assert :: Ptr Z3_context -> Ptr Z3_solver -> Ptr Z3_ast -> IO () -- | Reference: 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 () -- | Reference: foreign import ccall unsafe "Z3_solver_check" z3_solver_check :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_lbool -- | Reference: 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 -- | Reference: foreign import ccall unsafe "Z3_solver_get_model" z3_solver_get_model :: Ptr Z3_context -> Ptr Z3_solver -> IO (Ptr Z3_model) -- | Reference: foreign import ccall unsafe "Z3_solver_get_proof" z3_solver_get_proof :: Ptr Z3_context -> Ptr Z3_solver -> IO (Ptr Z3_ast) -- | Reference: 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) -- | Reference: foreign import ccall unsafe "Z3_solver_get_reason_unknown" z3_solver_get_reason_unknown :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_string -- | Reference: foreign import ccall unsafe "Z3_solver_to_string" z3_solver_to_string :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_string --------------------------------------------------------------------- -- * String Conversion -- | Reference: foreign import ccall unsafe "Z3_set_ast_print_mode" z3_set_ast_print_mode :: Ptr Z3_context -> Z3_ast_print_mode -> IO () -- | Reference: foreign import ccall unsafe "Z3_ast_to_string" z3_ast_to_string :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_string -- | Reference: foreign import ccall unsafe "Z3_pattern_to_string" z3_pattern_to_string :: Ptr Z3_context -> Ptr Z3_pattern -> IO Z3_string -- | Reference: foreign import ccall unsafe "Z3_sort_to_string" z3_sort_to_string :: Ptr Z3_context -> Ptr Z3_sort -> IO Z3_string -- | Reference: foreign import ccall unsafe "Z3_func_decl_to_string" z3_func_decl_to_string :: Ptr Z3_context -> Ptr Z3_func_decl -> IO Z3_string -- | Reference: foreign import ccall unsafe "Z3_benchmark_to_smtlib_string" z3_benchmark_to_smtlib_string :: Ptr Z3_context -> Z3_string -- ^ name -> Z3_string -- ^ logic -> Z3_string -- ^ status -> Z3_string -- ^ attributes -> CUInt -- ^ assumptions# -> Ptr (Ptr Z3_ast) -- ^ assumptions -> Ptr Z3_ast -- ^ formula -> IO Z3_string --------------------------------------------------------------------- -- * Parser Interface -- | Reference: foreign import ccall unsafe "Z3_parse_smtlib2_string" z3_parse_smtlib2_string :: Ptr Z3_context -> Z3_string -> CUInt -> Ptr (Ptr Z3_symbol) -> Ptr (Ptr Z3_sort) -> CUInt -> Ptr (Ptr Z3_symbol) -> Ptr (Ptr Z3_func_decl) -> IO (Ptr Z3_ast) -- | Referece foreign import ccall unsafe "Z3_parse_smtlib2_file" z3_parse_smtlib2_file :: Ptr Z3_context -> Z3_string -> CUInt -> Ptr (Ptr Z3_symbol) -> Ptr (Ptr Z3_sort) -> CUInt -> Ptr (Ptr Z3_symbol) -> Ptr (Ptr Z3_func_decl) -> IO (Ptr Z3_ast) --------------------------------------------------------------------- -- * Error Handling -- | Reference: foreign import ccall unsafe "Z3_get_error_code" z3_get_error_code :: Ptr Z3_context -> IO Z3_error_code -- | Reference: foreign import ccall unsafe "Z3_set_error_handler" z3_set_error_handler :: Ptr Z3_context -> FunPtr Z3_error_handler -> IO () -- | Reference: foreign import ccall unsafe "Z3_set_error" z3_set_error :: Ptr Z3_context -> Z3_error_code -> IO () -- | Reference: foreign import ccall unsafe "Z3_get_error_msg" z3_get_error_msg :: Ptr Z3_context -> Z3_error_code -> IO Z3_string --------------------------------------------------------------------- -- * Miscellaneous -- | Reference: foreign import ccall unsafe "Z3_get_version" z3_get_version :: Ptr CUInt -> Ptr CUInt -> Ptr CUInt -> Ptr CUInt -> IO () --------------------------------------------------------------------- -- * Fixedpoint facilities foreign import ccall unsafe "Z3_mk_fixedpoint" z3_mk_fixedpoint :: Ptr Z3_context -> IO (Ptr Z3_fixedpoint) foreign import ccall unsafe "Z3_fixedpoint_inc_ref" z3_fixedpoint_inc_ref :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO () foreign import ccall unsafe "Z3_fixedpoint_dec_ref" z3_fixedpoint_dec_ref :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO () foreign import ccall unsafe "Z3_fixedpoint_set_params" z3_fixedpoint_set_params :: Ptr Z3_context -> Ptr Z3_fixedpoint -> Ptr Z3_params -> IO () foreign import ccall unsafe "Z3_fixedpoint_add_rule" z3_fixedpoint_add_rule :: Ptr Z3_context -> Ptr Z3_fixedpoint -> Ptr Z3_ast -> Ptr Z3_symbol -> IO () foreign import ccall unsafe "Z3_fixedpoint_register_relation" z3_fixedpoint_register_relation :: Ptr Z3_context -> Ptr Z3_fixedpoint -> Ptr Z3_func_decl -> IO () foreign import ccall unsafe "Z3_fixedpoint_get_answer" z3_fixedpoint_get_answer :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO (Ptr Z3_ast) foreign import ccall unsafe "Z3_fixedpoint_get_assertions" z3_fixedpoint_get_assertions :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO (Ptr Z3_ast_vector) foreign import ccall unsafe "Z3_fixedpoint_query_relations" z3_fixedpoint_query_relations :: Ptr Z3_context -> Ptr Z3_fixedpoint -> CUInt -> Ptr (Ptr Z3_func_decl) -> IO Z3_lbool --------------------------------------------------------------------- -- * Optimization facilities foreign import ccall unsafe "Z3_mk_optimize" z3_mk_optimize :: Ptr Z3_context -> IO (Ptr Z3_optimize) foreign import ccall unsafe "Z3_optimize_inc_ref" z3_optimize_inc_ref :: Ptr Z3_context -> Ptr Z3_optimize -> IO () foreign import ccall unsafe "Z3_optimize_dec_ref" z3_optimize_dec_ref :: Ptr Z3_context -> Ptr Z3_optimize -> IO () foreign import ccall unsafe "Z3_optimize_assert" z3_optimize_assert :: Ptr Z3_context -> Ptr Z3_optimize -> Ptr Z3_ast -> IO () foreign import ccall unsafe "Z3_optimize_assert_and_track" z3_optimize_assert_and_track :: Ptr Z3_context -> Ptr Z3_optimize -> Ptr Z3_ast -> Ptr Z3_ast -> IO () foreign import ccall unsafe "Z3_optimize_assert_soft" z3_optimize_assert_soft :: Ptr Z3_context -> Ptr Z3_optimize -> Ptr Z3_ast -> Z3_string -> Ptr Z3_symbol -> IO CUInt foreign import ccall unsafe "Z3_optimize_maximize" z3_optimize_maximize :: Ptr Z3_context -> Ptr Z3_optimize -> Ptr Z3_ast -> IO CUInt foreign import ccall unsafe "Z3_optimize_minimize" z3_optimize_minimize :: Ptr Z3_context -> Ptr Z3_optimize -> Ptr Z3_ast -> IO CUInt foreign import ccall unsafe "Z3_optimize_push" z3_optimize_push :: Ptr Z3_context -> Ptr Z3_optimize -> IO () foreign import ccall unsafe "Z3_optimize_pop" z3_optimize_pop :: Ptr Z3_context -> Ptr Z3_optimize -> IO () foreign import ccall unsafe "Z3_optimize_check" z3_optimize_check :: Ptr Z3_context -> Ptr Z3_optimize -> CUInt -> Ptr (Ptr Z3_ast) -> IO Z3_lbool foreign import ccall unsafe "Z3_optimize_get_reason_unknown" z3_optimize_get_reason_unknown :: Ptr Z3_context -> Ptr Z3_optimize -> IO Z3_string foreign import ccall unsafe "Z3_optimize_get_model" z3_optimize_get_model :: Ptr Z3_context -> Ptr Z3_optimize -> IO (Ptr Z3_model) foreign import ccall unsafe "Z3_optimize_get_unsat_core" z3_optimize_get_unsat_core :: Ptr Z3_context -> Ptr Z3_optimize -> IO (Ptr Z3_ast_vector) foreign import ccall unsafe "Z3_optimize_set_params" z3_optimize_set_params :: Ptr Z3_context -> Ptr Z3_optimize -> Ptr Z3_params -> IO () foreign import ccall unsafe "Z3_optimize_get_lower" z3_optimize_get_lower :: Ptr Z3_context -> Ptr Z3_optimize -> CUInt -> IO (Ptr Z3_ast) foreign import ccall unsafe "Z3_optimize_get_upper" z3_optimize_get_upper :: Ptr Z3_context -> Ptr Z3_optimize -> CUInt -> IO (Ptr Z3_ast) foreign import ccall unsafe "Z3_optimize_get_lower_as_vector" z3_optimize_get_lower_as_vector :: Ptr Z3_context -> Ptr Z3_optimize -> CUInt -> IO (Ptr Z3_ast_vector) foreign import ccall unsafe "Z3_optimize_get_upper_as_vector" z3_optimize_get_upper_as_vector :: Ptr Z3_context -> Ptr Z3_optimize -> CUInt -> IO (Ptr Z3_ast_vector) foreign import ccall unsafe "Z3_optimize_to_string" z3_optimize_to_string :: Ptr Z3_context -> Ptr Z3_optimize -> IO Z3_string foreign import ccall unsafe "Z3_optimize_from_string" z3_optimize_from_string :: Ptr Z3_context -> Ptr Z3_optimize -> Z3_string -> IO () foreign import ccall unsafe "Z3_optimize_from_file" z3_optimize_from_file :: Ptr Z3_context -> Ptr Z3_optimize -> Z3_string -> IO () foreign import ccall unsafe "Z3_optimize_get_help" z3_optimize_get_help :: Ptr Z3_context -> Ptr Z3_optimize -> IO Z3_string foreign import ccall unsafe "Z3_optimize_get_assertions" z3_optimize_get_assertions :: Ptr Z3_context -> Ptr Z3_optimize -> IO (Ptr Z3_ast_vector) foreign import ccall unsafe "Z3_optimize_get_objectives" z3_optimize_get_objectives :: Ptr Z3_context -> Ptr Z3_optimize -> IO (Ptr Z3_ast_vector)