Copyright | (c) Iago Abal 2012-2014 (c) David Castro 2012-2013 |
---|---|
License | BSD3 |
Maintainer | Iago Abal <mail@iagoabal.eu>, David Castro <david.castro.dcp@gmail.com> |
Safe Haskell | Safe |
Language | Haskell98 |
- Types
- 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
Z3 API foreign imports.
- 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
- newtype Z3_lbool = Z3_lbool CInt
- z3_l_true :: Z3_lbool
- z3_l_false :: Z3_lbool
- z3_l_undef :: Z3_lbool
- newtype Z3_bool = Z3_bool CInt
- type Z3_error_handler = Ptr Z3_context -> Z3_error_code -> IO ()
- z3_true :: Z3_bool
- z3_false :: Z3_bool
- type Z3_string = CString
- type Z3_ast_print_mode = CInt
- z3_print_smtlib_full :: Z3_ast_print_mode
- z3_print_low_level :: Z3_ast_print_mode
- z3_print_smtlib2_compliant :: Z3_ast_print_mode
- type Z3_error_code = CInt
- z3_ok :: Z3_error_code
- z3_sort_error :: Z3_error_code
- z3_iob :: Z3_error_code
- z3_invalid_arg :: Z3_error_code
- z3_parser_error :: Z3_error_code
- z3_no_parser :: Z3_error_code
- z3_invalid_pattern :: Z3_error_code
- z3_memout_fail :: Z3_error_code
- z3_file_access_error :: Z3_error_code
- type Z3_sort_kind = CInt
- z3_uninterpreted_sort :: Z3_sort_kind
- z3_internal_fatal :: Z3_error_code
- z3_bool_sort :: Z3_sort_kind
- z3_invalid_usage :: Z3_error_code
- z3_int_sort :: Z3_sort_kind
- z3_dec_ref_error :: Z3_error_code
- z3_real_sort :: Z3_sort_kind
- z3_exception :: Z3_error_code
- z3_bv_sort :: Z3_sort_kind
- z3_array_sort :: Z3_sort_kind
- z3_datatype_sort :: Z3_sort_kind
- z3_relation_sort :: Z3_sort_kind
- z3_finite_domain_sort :: Z3_sort_kind
- z3_floating_point_sort :: Z3_sort_kind
- z3_rounding_mode_sort :: Z3_sort_kind
- z3_unknown_sort :: Z3_sort_kind
- type Z3_ast_kind = CInt
- z3_numeral_ast :: Z3_ast_kind
- z3_app_ast :: Z3_ast_kind
- z3_var_ast :: Z3_ast_kind
- z3_quantifier_ast :: Z3_ast_kind
- z3_sort_ast :: Z3_ast_kind
- z3_func_decl_ast :: Z3_ast_kind
- z3_unknown_ast :: Z3_ast_kind
- z3_mk_config :: IO (Ptr Z3_config)
- z3_del_config :: Ptr Z3_config -> IO ()
- z3_set_param_value :: Ptr Z3_config -> Z3_string -> Z3_string -> IO ()
- z3_mk_context_rc :: Ptr Z3_config -> IO (Ptr Z3_context)
- z3_del_context :: Ptr Z3_context -> IO ()
- z3_inc_ref :: Ptr Z3_context -> Ptr Z3_ast -> IO ()
- z3_dec_ref :: Ptr Z3_context -> Ptr Z3_ast -> IO ()
- z3_mk_int_symbol :: Ptr Z3_context -> CInt -> IO (Ptr Z3_symbol)
- z3_mk_string_symbol :: Ptr Z3_context -> Z3_string -> IO (Ptr Z3_symbol)
- z3_sort_to_ast :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast)
- z3_mk_uninterpreted_sort :: Ptr Z3_context -> Ptr Z3_symbol -> IO (Ptr Z3_sort)
- z3_mk_bool_sort :: Ptr Z3_context -> IO (Ptr Z3_sort)
- z3_mk_int_sort :: Ptr Z3_context -> IO (Ptr Z3_sort)
- z3_mk_real_sort :: Ptr Z3_context -> IO (Ptr Z3_sort)
- z3_mk_bv_sort :: Ptr Z3_context -> CUInt -> IO (Ptr Z3_sort)
- z3_mk_array_sort :: Ptr Z3_context -> Ptr Z3_sort -> Ptr Z3_sort -> IO (Ptr Z3_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)
- 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)
- z3_del_constructor :: Ptr Z3_context -> Ptr Z3_constructor -> IO ()
- z3_mk_datatype :: Ptr Z3_context -> Ptr Z3_symbol -> CUInt -> Ptr (Ptr Z3_constructor) -> IO (Ptr Z3_sort)
- z3_mk_constructor_list :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_constructor) -> IO (Ptr Z3_constructor_list)
- z3_del_constructor_list :: Ptr Z3_context -> Ptr Z3_constructor_list -> IO ()
- z3_mk_datatypes :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_symbol) -> Ptr (Ptr Z3_sort) -> Ptr (Ptr Z3_constructor_list) -> IO ()
- z3_mk_set_sort :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_sort)
- z3_mk_func_decl :: Ptr Z3_context -> Ptr Z3_symbol -> CUInt -> Ptr (Ptr Z3_sort) -> Ptr Z3_sort -> IO (Ptr Z3_func_decl)
- z3_mk_app :: Ptr Z3_context -> Ptr Z3_func_decl -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
- z3_mk_const :: Ptr Z3_context -> Ptr Z3_symbol -> Ptr Z3_sort -> IO (Ptr Z3_ast)
- z3_mk_fresh_const :: Ptr Z3_context -> Z3_string -> Ptr Z3_sort -> IO (Ptr Z3_ast)
- z3_mk_fresh_func_decl :: Ptr z3_context -> Z3_string -> CUInt -> Ptr (Ptr Z3_sort) -> Ptr Z3_sort -> IO (Ptr Z3_func_decl)
- z3_mk_true :: Ptr Z3_context -> IO (Ptr Z3_ast)
- z3_mk_false :: Ptr Z3_context -> IO (Ptr Z3_ast)
- z3_mk_eq :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_distinct :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
- z3_mk_not :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_ite :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_iff :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_implies :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_xor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_and :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
- z3_mk_or :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
- z3_mk_add :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
- z3_mk_mul :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
- z3_mk_sub :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
- z3_mk_unary_minus :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_div :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_mod :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_rem :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_lt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_le :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_gt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_ge :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_int2real :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_real2int :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_is_int :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvnot :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvredand :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvredor :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvand :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvxor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvnand :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvnor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvxnor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvneg :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvadd :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvsub :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvmul :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvudiv :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvsdiv :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvurem :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvsrem :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvsmod :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvult :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvslt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvule :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvsle :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvuge :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvsge :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvugt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvsgt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_concat :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_extract :: Ptr Z3_context -> CUInt -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_sign_ext :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_zero_ext :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_repeat :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvshl :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvlshr :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvashr :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_rotate_left :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_rotate_right :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_ext_rotate_left :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_ext_rotate_right :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_int2bv :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bv2int :: Ptr Z3_context -> Ptr Z3_ast -> Z3_bool -> IO (Ptr Z3_ast)
- z3_mk_bvadd_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Z3_bool -> IO (Ptr Z3_ast)
- z3_mk_bvadd_no_underflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvsub_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvsub_no_underflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvsdiv_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvneg_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_bvmul_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Z3_bool -> IO (Ptr Z3_ast)
- z3_mk_bvmul_no_underflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_select :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_store :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_const_array :: Ptr Z3_context -> Ptr Z3_sort -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_map :: Ptr Z3_context -> Ptr Z3_func_decl -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
- z3_mk_array_default :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_empty_set :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast)
- z3_mk_full_set :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast)
- z3_mk_set_add :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_set_del :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_set_union :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
- z3_mk_set_intersect :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
- z3_mk_set_difference :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_set_complement :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_set_member :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_set_subset :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_numeral :: Ptr Z3_context -> Z3_string -> Ptr Z3_sort -> IO (Ptr Z3_ast)
- z3_mk_real :: Ptr Z3_context -> CInt -> CInt -> IO (Ptr Z3_ast)
- z3_mk_int :: Ptr Z3_context -> CInt -> Ptr Z3_sort -> IO (Ptr Z3_ast)
- z3_mk_unsigned_int :: Ptr Z3_context -> CUInt -> Ptr Z3_sort -> IO (Ptr Z3_ast)
- z3_mk_int64 :: Ptr Z3_context -> CLLong -> Ptr Z3_sort -> IO (Ptr Z3_ast)
- z3_mk_unsigned_int64 :: Ptr Z3_context -> CULLong -> Ptr Z3_sort -> IO (Ptr Z3_ast)
- z3_mk_pattern :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_pattern)
- z3_mk_bound :: Ptr Z3_context -> CUInt -> Ptr Z3_sort -> IO (Ptr Z3_ast)
- 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)
- 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)
- 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)
- 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)
- z3_func_decl_to_ast :: Ptr Z3_context -> Ptr Z3_func_decl -> IO (Ptr Z3_ast)
- z3_get_ast_kind :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_ast_kind
- z3_is_app :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_bool
- z3_get_app_num_args :: Ptr Z3_context -> Ptr Z3_app -> IO CUInt
- z3_get_app_arg :: Ptr Z3_context -> Ptr Z3_app -> CUInt -> IO (Ptr Z3_ast)
- z3_get_app_decl :: Ptr Z3_context -> Ptr Z3_app -> IO (Ptr Z3_func_decl)
- z3_get_datatype_sort_num_constructors :: Ptr Z3_context -> Ptr Z3_sort -> IO CUInt
- z3_get_datatype_sort_constructor :: Ptr Z3_context -> Ptr Z3_sort -> CUInt -> IO (Ptr Z3_func_decl)
- z3_get_datatype_sort_recognizer :: Ptr Z3_context -> Ptr Z3_sort -> CUInt -> IO (Ptr Z3_func_decl)
- z3_get_datatype_sort_constructor_accessor :: Ptr Z3_context -> Ptr Z3_sort -> CUInt -> CUInt -> IO (Ptr Z3_func_decl)
- z3_get_decl_name :: Ptr Z3_context -> Ptr Z3_func_decl -> IO (Ptr Z3_symbol)
- z3_get_symbol_string :: Ptr Z3_context -> Ptr Z3_symbol -> IO Z3_string
- z3_get_sort_kind :: Ptr Z3_context -> Ptr Z3_sort -> IO Z3_sort_kind
- z3_get_bv_sort_size :: Ptr Z3_context -> Ptr Z3_sort -> IO CUInt
- z3_app_to_ast :: Ptr Z3_context -> Ptr Z3_app -> IO (Ptr Z3_ast)
- z3_get_sort :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_sort)
- z3_get_array_sort_domain :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_sort)
- z3_get_array_sort_range :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_sort)
- z3_get_bool_value :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_lbool
- z3_get_numeral_string :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_string
- z3_get_arity :: Ptr Z3_context -> Ptr Z3_func_decl -> IO CUInt
- z3_get_domain :: Ptr Z3_context -> Ptr Z3_func_decl -> CUInt -> IO (Ptr Z3_sort)
- z3_get_range :: Ptr Z3_context -> Ptr Z3_func_decl -> IO (Ptr Z3_sort)
- z3_to_app :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_app)
- z3_pattern_to_ast :: Ptr Z3_context -> Ptr Z3_pattern -> IO (Ptr Z3_ast)
- z3_simplify :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_simplify_ex :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_params -> IO (Ptr Z3_ast)
- z3_is_quantifier_forall :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_bool
- z3_get_quantifier_weight :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt
- z3_get_quantifier_num_patterns :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt
- z3_get_quantifier_pattern_ast :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> IO (Ptr Z3_ast)
- z3_get_quantifier_num_no_patterns :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt
- z3_get_quantifier_no_pattern_ast :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> IO (Ptr Z3_ast)
- z3_get_quantifier_num_bound :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt
- z3_get_quantifier_bound_name :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> IO (Ptr Z3_symbol)
- z3_get_quantifier_bound_sort :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> IO (Ptr Z3_sort)
- z3_get_quantifier_body :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_substitute_vars :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
- z3_ast_vector_size :: Ptr Z3_context -> Ptr Z3_ast_vector -> IO CUInt
- z3_ast_vector_get :: Ptr Z3_context -> Ptr Z3_ast_vector -> CUInt -> IO (Ptr Z3_ast)
- z3_ast_vector_inc_ref :: Ptr Z3_context -> Ptr Z3_ast_vector -> IO ()
- z3_ast_vector_dec_ref :: Ptr Z3_context -> Ptr Z3_ast_vector -> IO ()
- z3_model_inc_ref :: Ptr Z3_context -> Ptr Z3_model -> IO ()
- z3_model_dec_ref :: Ptr Z3_context -> Ptr Z3_model -> IO ()
- z3_model_eval :: Ptr Z3_context -> Ptr Z3_model -> Ptr Z3_ast -> Z3_bool -> Ptr (Ptr Z3_ast) -> IO Z3_bool
- z3_model_get_const_interp :: Ptr Z3_context -> Ptr Z3_model -> Ptr Z3_func_decl -> IO (Ptr Z3_ast)
- z3_model_get_func_interp :: Ptr Z3_context -> Ptr Z3_model -> Ptr Z3_func_decl -> IO (Ptr Z3_func_interp)
- z3_model_has_interp :: Ptr Z3_context -> Ptr Z3_model -> Ptr Z3_func_decl -> IO Z3_bool
- z3_model_get_num_consts :: Ptr Z3_context -> Ptr Z3_model -> IO CUInt
- z3_model_get_num_funcs :: Ptr Z3_context -> Ptr Z3_model -> IO CUInt
- z3_model_get_const_decl :: Ptr Z3_context -> Ptr Z3_model -> CUInt -> IO (Ptr Z3_func_decl)
- z3_model_get_func_decl :: Ptr Z3_context -> Ptr Z3_model -> CUInt -> IO (Ptr Z3_func_decl)
- z3_is_as_array :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_bool
- z3_get_as_array_func_decl :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_func_decl)
- z3_add_func_interp :: Ptr Z3_context -> Ptr Z3_model -> Ptr Z3_func_decl -> Ptr Z3_ast -> IO (Ptr Z3_func_interp)
- z3_add_const_interp :: Ptr Z3_context -> Ptr Z3_model -> Ptr Z3_func_decl -> Ptr Z3_ast -> IO ()
- z3_func_interp_inc_ref :: Ptr Z3_context -> Ptr Z3_func_interp -> IO ()
- z3_func_interp_dec_ref :: Ptr Z3_context -> Ptr Z3_func_interp -> IO ()
- z3_func_interp_get_num_entries :: Ptr Z3_context -> Ptr Z3_func_interp -> IO CUInt
- z3_func_interp_get_entry :: Ptr Z3_context -> Ptr Z3_func_interp -> CUInt -> IO (Ptr Z3_func_entry)
- z3_func_interp_get_else :: Ptr Z3_context -> Ptr Z3_func_interp -> IO (Ptr Z3_ast)
- z3_func_interp_get_arity :: Ptr Z3_context -> Ptr Z3_func_interp -> IO CUInt
- z3_func_entry_inc_ref :: Ptr Z3_context -> Ptr Z3_func_entry -> IO ()
- z3_func_entry_dec_ref :: Ptr Z3_context -> Ptr Z3_func_entry -> IO ()
- z3_func_entry_get_value :: Ptr Z3_context -> Ptr Z3_func_entry -> IO (Ptr Z3_ast)
- z3_func_entry_get_num_args :: Ptr Z3_context -> Ptr Z3_func_entry -> IO CUInt
- z3_func_entry_get_arg :: Ptr Z3_context -> Ptr Z3_func_entry -> CUInt -> IO (Ptr Z3_ast)
- z3_get_index_value :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt
- z3_model_to_string :: Ptr Z3_context -> Ptr Z3_model -> IO Z3_string
- z3_mk_params :: Ptr Z3_context -> IO (Ptr Z3_params)
- z3_params_inc_ref :: Ptr Z3_context -> Ptr Z3_params -> IO ()
- z3_params_dec_ref :: Ptr Z3_context -> Ptr Z3_params -> IO ()
- z3_params_set_bool :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol -> Z3_bool -> IO ()
- z3_params_set_uint :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol -> CUInt -> IO ()
- z3_params_set_double :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol -> CDouble -> IO ()
- z3_params_set_symbol :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol -> Ptr Z3_symbol -> IO ()
- z3_params_to_string :: Ptr Z3_context -> Ptr Z3_params -> IO Z3_string
- z3_mk_interpolant :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
- z3_mk_interpolation_context :: Ptr Z3_config -> IO (Ptr Z3_context)
- z3_get_interpolant :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Ptr Z3_params -> IO (Ptr Z3_ast_vector)
- z3_compute_interpolant :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_params -> Ptr (Ptr Z3_ast_vector) -> Ptr (Ptr Z3_model) -> IO Z3_lbool
- 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
- 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
- z3_interpolation_profile :: Ptr Z3_context -> IO Z3_string
- z3_write_interpolation_problem :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> Ptr CUInt -> Ptr CChar -> CUInt -> Ptr (Ptr Z3_ast) -> IO ()
- z3_mk_tactic :: Ptr Z3_context -> Ptr CChar -> IO (Ptr Z3_tactic)
- z3_tactic_and_then :: Ptr Z3_context -> Ptr Z3_tactic -> Ptr Z3_tactic -> IO (Ptr Z3_tactic)
- z3_tactic_or_else :: Ptr Z3_context -> Ptr Z3_tactic -> Ptr Z3_tactic -> IO (Ptr Z3_tactic)
- z3_tactic_skip :: Ptr Z3_context -> IO (Ptr Z3_tactic)
- z3_tactic_try_for :: Ptr Z3_context -> Ptr Z3_tactic -> CUInt -> IO (Ptr Z3_tactic)
- z3_tactic_inc_ref :: Ptr Z3_context -> Ptr Z3_tactic -> IO ()
- z3_tactic_dec_ref :: Ptr Z3_context -> Ptr Z3_tactic -> IO ()
- z3_tactic_apply :: Ptr Z3_context -> Ptr Z3_tactic -> Ptr Z3_goal -> IO (Ptr Z3_apply_result)
- z3_apply_result_inc_ref :: Ptr Z3_context -> Ptr Z3_apply_result -> IO ()
- z3_apply_result_dec_ref :: Ptr Z3_context -> Ptr Z3_apply_result -> IO ()
- z3_apply_result_get_num_subgoals :: Ptr Z3_context -> Ptr Z3_apply_result -> IO CUInt
- z3_apply_result_get_subgoal :: Ptr Z3_context -> Ptr Z3_apply_result -> CUInt -> IO (Ptr Z3_goal)
- z3_mk_goal :: Ptr Z3_context -> Z3_bool -> Z3_bool -> Z3_bool -> IO (Ptr Z3_goal)
- z3_goal_inc_ref :: Ptr Z3_context -> Ptr Z3_goal -> IO ()
- z3_goal_dec_ref :: Ptr Z3_context -> Ptr Z3_goal -> IO ()
- z3_goal_assert :: Ptr Z3_context -> Ptr Z3_goal -> Ptr Z3_ast -> IO ()
- z3_goal_size :: Ptr Z3_context -> Ptr Z3_goal -> IO CUInt
- z3_goal_formula :: Ptr Z3_context -> Ptr Z3_goal -> CUInt -> IO (Ptr Z3_ast)
- z3_mk_solver :: Ptr Z3_context -> IO (Ptr Z3_solver)
- z3_mk_simple_solver :: Ptr Z3_context -> IO (Ptr Z3_solver)
- z3_mk_solver_for_logic :: Ptr Z3_context -> Ptr Z3_symbol -> IO (Ptr Z3_solver)
- z3_solver_get_help :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_string
- z3_solver_set_params :: Ptr Z3_context -> Ptr Z3_solver -> Ptr Z3_params -> IO ()
- z3_solver_inc_ref :: Ptr Z3_context -> Ptr Z3_solver -> IO ()
- z3_solver_dec_ref :: Ptr Z3_context -> Ptr Z3_solver -> IO ()
- z3_solver_push :: Ptr Z3_context -> Ptr Z3_solver -> IO ()
- z3_solver_pop :: Ptr Z3_context -> Ptr Z3_solver -> CUInt -> IO ()
- z3_solver_get_num_scopes :: Ptr Z3_context -> Ptr Z3_solver -> IO CUInt
- z3_solver_reset :: Ptr Z3_context -> Ptr Z3_solver -> IO ()
- z3_solver_assert :: Ptr Z3_context -> Ptr Z3_solver -> Ptr Z3_ast -> IO ()
- z3_solver_assert_and_track :: Ptr Z3_context -> Ptr Z3_solver -> Ptr Z3_ast -> Ptr Z3_ast -> IO ()
- z3_solver_check :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_lbool
- z3_solver_check_assumptions :: Ptr Z3_context -> Ptr Z3_solver -> CUInt -> Ptr (Ptr Z3_ast) -> IO Z3_lbool
- z3_solver_get_model :: Ptr Z3_context -> Ptr Z3_solver -> IO (Ptr Z3_model)
- z3_solver_get_unsat_core :: Ptr Z3_context -> Ptr Z3_solver -> IO (Ptr Z3_ast_vector)
- z3_solver_get_reason_unknown :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_string
- z3_solver_to_string :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_string
- z3_set_ast_print_mode :: Ptr Z3_context -> Z3_ast_print_mode -> IO ()
- z3_ast_to_string :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_string
- z3_pattern_to_string :: Ptr Z3_context -> Ptr Z3_pattern -> IO Z3_string
- z3_sort_to_string :: Ptr Z3_context -> Ptr Z3_sort -> IO Z3_string
- z3_func_decl_to_string :: Ptr Z3_context -> Ptr Z3_func_decl -> IO Z3_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
- 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)
- 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)
- z3_get_parser_error :: Ptr Z3_context -> IO Z3_string
- z3_get_error_code :: Ptr Z3_context -> IO Z3_error_code
- z3_set_error_handler :: Ptr Z3_context -> FunPtr Z3_error_handler -> IO ()
- z3_set_error :: Ptr Z3_context -> Z3_error_code -> IO ()
- z3_get_error_msg :: Z3_error_code -> IO Z3_string
- z3_get_error_msg_ex :: Ptr Z3_context -> Z3_error_code -> IO Z3_string
- z3_get_version :: Ptr CUInt -> Ptr CUInt -> Ptr CUInt -> Ptr CUInt -> IO ()
- z3_mk_fixedpoint :: Ptr Z3_context -> IO (Ptr Z3_fixedpoint)
- z3_fixedpoint_push :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO ()
- z3_fixedpoint_pop :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO ()
- z3_fixedpoint_inc_ref :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO ()
- z3_fixedpoint_dec_ref :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO ()
- z3_fixedpoint_set_params :: Ptr Z3_context -> Ptr Z3_fixedpoint -> Ptr Z3_params -> IO ()
- z3_fixedpoint_add_rule :: Ptr Z3_context -> Ptr Z3_fixedpoint -> Ptr Z3_ast -> Ptr Z3_symbol -> IO ()
- z3_fixedpoint_register_relation :: Ptr Z3_context -> Ptr Z3_fixedpoint -> Ptr Z3_func_decl -> IO ()
- z3_fixedpoint_get_answer :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO (Ptr Z3_ast)
- z3_fixedpoint_get_assertions :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO (Ptr Z3_ast_vector)
- z3_fixedpoint_query_relations :: Ptr Z3_context -> Ptr Z3_fixedpoint -> CUInt -> Ptr (Ptr Z3_func_decl) -> IO Z3_lbool
Types
data Z3_context Source #
data Z3_func_decl Source #
data Z3_pattern Source #
data Z3_constructor Source #
data Z3_constructor_list Source #
data Z3_apply_result Source #
data Z3_func_interp Source #
data Z3_func_entry Source #
data Z3_fixedpoint Source #
data Z3_ast_vector Source #
Z3_lbool CInt |
Z3_bool CInt |
type Z3_error_handler = Ptr Z3_context -> Z3_error_code -> IO () Source #
type Z3_ast_print_mode = CInt Source #
type Z3_error_code = CInt Source #
type Z3_sort_kind = CInt Source #
type Z3_ast_kind = CInt Source #
Create configuration
z3_mk_config :: IO (Ptr Z3_config) Source #
z3_del_config :: Ptr Z3_config -> IO () Source #
Create context
z3_mk_context_rc :: Ptr Z3_config -> IO (Ptr Z3_context) Source #
z3_del_context :: Ptr Z3_context -> IO () Source #
z3_inc_ref :: Ptr Z3_context -> Ptr Z3_ast -> IO () Source #
z3_dec_ref :: Ptr Z3_context -> Ptr Z3_ast -> IO () Source #
Symbols
z3_mk_int_symbol :: Ptr Z3_context -> CInt -> IO (Ptr Z3_symbol) Source #
z3_mk_string_symbol :: Ptr Z3_context -> Z3_string -> IO (Ptr Z3_symbol) Source #
Sorts
z3_sort_to_ast :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast) Source #
z3_mk_uninterpreted_sort :: Ptr Z3_context -> Ptr Z3_symbol -> IO (Ptr Z3_sort) Source #
z3_mk_bool_sort :: Ptr Z3_context -> IO (Ptr Z3_sort) Source #
z3_mk_int_sort :: Ptr Z3_context -> IO (Ptr Z3_sort) Source #
z3_mk_real_sort :: Ptr Z3_context -> IO (Ptr Z3_sort) Source #
z3_mk_bv_sort :: Ptr Z3_context -> CUInt -> IO (Ptr Z3_sort) Source #
:: Ptr Z3_context | |
-> Ptr Z3_sort | domain |
-> Ptr Z3_sort | range |
-> IO (Ptr Z3_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) Source #
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) Source #
z3_del_constructor :: Ptr Z3_context -> Ptr Z3_constructor -> IO () Source #
z3_mk_datatype :: Ptr Z3_context -> Ptr Z3_symbol -> CUInt -> Ptr (Ptr Z3_constructor) -> IO (Ptr Z3_sort) Source #
z3_mk_constructor_list :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_constructor) -> IO (Ptr Z3_constructor_list) Source #
z3_del_constructor_list :: Ptr Z3_context -> Ptr Z3_constructor_list -> IO () Source #
z3_mk_datatypes :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_symbol) -> Ptr (Ptr Z3_sort) -> Ptr (Ptr Z3_constructor_list) -> IO () Source #
z3_mk_set_sort :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_sort) Source #
Constants and Applications
z3_mk_func_decl :: Ptr Z3_context -> Ptr Z3_symbol -> CUInt -> Ptr (Ptr Z3_sort) -> Ptr Z3_sort -> IO (Ptr Z3_func_decl) Source #
z3_mk_app :: Ptr Z3_context -> Ptr Z3_func_decl -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) Source #
z3_mk_const :: Ptr Z3_context -> Ptr Z3_symbol -> Ptr Z3_sort -> IO (Ptr Z3_ast) Source #
z3_mk_fresh_const :: Ptr Z3_context -> Z3_string -> Ptr Z3_sort -> IO (Ptr Z3_ast) Source #
z3_mk_fresh_func_decl :: Ptr z3_context -> Z3_string -> CUInt -> Ptr (Ptr Z3_sort) -> Ptr Z3_sort -> IO (Ptr Z3_func_decl) Source #
Propositional Logic and Equality
z3_mk_true :: Ptr Z3_context -> IO (Ptr Z3_ast) Source #
z3_mk_false :: Ptr Z3_context -> IO (Ptr Z3_ast) Source #
z3_mk_distinct :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) Source #
z3_mk_implies :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
Arithmetic: Integers and Reals
z3_mk_unary_minus :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_int2real :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_real2int :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_is_int :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
Bit-vectors
z3_mk_bvnot :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvredand :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvredor :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvand :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvxor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvnand :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvnor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvxnor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvneg :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvadd :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvsub :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvmul :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvudiv :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvsdiv :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvurem :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvsrem :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvsmod :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvult :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvslt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvule :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvsle :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvuge :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvsge :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvugt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvsgt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_concat :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_extract :: Ptr Z3_context -> CUInt -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_sign_ext :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_zero_ext :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_repeat :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvshl :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvlshr :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvashr :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_rotate_left :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_rotate_right :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_ext_rotate_left :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_ext_rotate_right :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_int2bv :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bv2int :: Ptr Z3_context -> Ptr Z3_ast -> Z3_bool -> IO (Ptr Z3_ast) Source #
z3_mk_bvadd_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Z3_bool -> IO (Ptr Z3_ast) Source #
z3_mk_bvadd_no_underflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvsub_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvsub_no_underflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvsdiv_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvneg_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_bvmul_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Z3_bool -> IO (Ptr Z3_ast) Source #
z3_mk_bvmul_no_underflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
Arrays
:: Ptr Z3_context | |
-> Ptr Z3_ast | aray |
-> Ptr Z3_ast | index |
-> IO (Ptr Z3_ast) |
:: Ptr Z3_context | |
-> Ptr Z3_ast | array |
-> Ptr Z3_ast | index |
-> Ptr Z3_ast | value to store at array[index] |
-> IO (Ptr Z3_ast) |
z3_mk_const_array :: Ptr Z3_context -> Ptr Z3_sort -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_map :: Ptr Z3_context -> Ptr Z3_func_decl -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) Source #
z3_mk_array_default :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
Sets
z3_mk_empty_set :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast) Source #
z3_mk_full_set :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast) Source #
z3_mk_set_add :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_set_del :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_set_union :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) Source #
z3_mk_set_intersect :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) Source #
z3_mk_set_difference :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_set_complement :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_set_member :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_set_subset :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
Numerals
z3_mk_numeral :: Ptr Z3_context -> Z3_string -> Ptr Z3_sort -> IO (Ptr Z3_ast) Source #
z3_mk_real :: Ptr Z3_context -> CInt -> CInt -> IO (Ptr Z3_ast) Source #
z3_mk_unsigned_int :: Ptr Z3_context -> CUInt -> Ptr Z3_sort -> IO (Ptr Z3_ast) Source #
z3_mk_int64 :: Ptr Z3_context -> CLLong -> Ptr Z3_sort -> IO (Ptr Z3_ast) Source #
z3_mk_unsigned_int64 :: Ptr Z3_context -> CULLong -> Ptr Z3_sort -> IO (Ptr Z3_ast) Source #
Quantifiers
z3_mk_pattern :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_pattern) Source #
z3_mk_bound :: Ptr Z3_context -> CUInt -> Ptr Z3_sort -> IO (Ptr Z3_ast) Source #
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) Source #
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) Source #
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) Source #
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) Source #
Accessors
z3_func_decl_to_ast :: Ptr Z3_context -> Ptr Z3_func_decl -> IO (Ptr Z3_ast) Source #
z3_get_ast_kind :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_ast_kind Source #
z3_get_app_num_args :: Ptr Z3_context -> Ptr Z3_app -> IO CUInt Source #
z3_get_app_arg :: Ptr Z3_context -> Ptr Z3_app -> CUInt -> IO (Ptr Z3_ast) Source #
z3_get_app_decl :: Ptr Z3_context -> Ptr Z3_app -> IO (Ptr Z3_func_decl) Source #
z3_get_datatype_sort_num_constructors :: Ptr Z3_context -> Ptr Z3_sort -> IO CUInt Source #
z3_get_datatype_sort_constructor :: Ptr Z3_context -> Ptr Z3_sort -> CUInt -> IO (Ptr Z3_func_decl) Source #
z3_get_datatype_sort_recognizer :: Ptr Z3_context -> Ptr Z3_sort -> CUInt -> IO (Ptr Z3_func_decl) Source #
z3_get_datatype_sort_constructor_accessor :: Ptr Z3_context -> Ptr Z3_sort -> CUInt -> CUInt -> IO (Ptr Z3_func_decl) Source #
z3_get_decl_name :: Ptr Z3_context -> Ptr Z3_func_decl -> IO (Ptr Z3_symbol) Source #
z3_get_symbol_string :: Ptr Z3_context -> Ptr Z3_symbol -> IO Z3_string Source #
z3_get_sort_kind :: Ptr Z3_context -> Ptr Z3_sort -> IO Z3_sort_kind Source #
z3_get_bv_sort_size :: Ptr Z3_context -> Ptr Z3_sort -> IO CUInt Source #
z3_app_to_ast :: Ptr Z3_context -> Ptr Z3_app -> IO (Ptr Z3_ast) Source #
z3_get_sort :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_sort) Source #
z3_get_array_sort_domain :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_sort) Source #
z3_get_array_sort_range :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_sort) Source #
z3_get_bool_value :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_lbool Source #
z3_get_numeral_string :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_string Source #
z3_get_arity :: Ptr Z3_context -> Ptr Z3_func_decl -> IO CUInt Source #
z3_get_domain :: Ptr Z3_context -> Ptr Z3_func_decl -> CUInt -> IO (Ptr Z3_sort) Source #
z3_get_range :: Ptr Z3_context -> Ptr Z3_func_decl -> IO (Ptr Z3_sort) Source #
z3_pattern_to_ast :: Ptr Z3_context -> Ptr Z3_pattern -> IO (Ptr Z3_ast) Source #
z3_simplify :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_simplify_ex :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_params -> IO (Ptr Z3_ast) Source #
z3_is_quantifier_forall :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_bool Source #
z3_get_quantifier_weight :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt Source #
z3_get_quantifier_num_patterns :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt Source #
z3_get_quantifier_pattern_ast :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> IO (Ptr Z3_ast) Source #
z3_get_quantifier_num_no_patterns :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt Source #
z3_get_quantifier_no_pattern_ast :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> IO (Ptr Z3_ast) Source #
z3_get_quantifier_num_bound :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt Source #
z3_get_quantifier_bound_name :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> IO (Ptr Z3_symbol) Source #
z3_get_quantifier_bound_sort :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> IO (Ptr Z3_sort) Source #
z3_get_quantifier_body :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
Modifiers
z3_substitute_vars :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) Source #
AST vectors
z3_ast_vector_size :: Ptr Z3_context -> Ptr Z3_ast_vector -> IO CUInt Source #
z3_ast_vector_get :: Ptr Z3_context -> Ptr Z3_ast_vector -> CUInt -> IO (Ptr Z3_ast) Source #
z3_ast_vector_inc_ref :: Ptr Z3_context -> Ptr Z3_ast_vector -> IO () Source #
z3_ast_vector_dec_ref :: Ptr Z3_context -> Ptr Z3_ast_vector -> IO () Source #
Models
z3_model_inc_ref :: Ptr Z3_context -> Ptr Z3_model -> IO () Source #
z3_model_dec_ref :: Ptr Z3_context -> Ptr Z3_model -> IO () Source #
z3_model_eval :: Ptr Z3_context -> Ptr Z3_model -> Ptr Z3_ast -> Z3_bool -> Ptr (Ptr Z3_ast) -> IO Z3_bool Source #
z3_model_get_const_interp :: Ptr Z3_context -> Ptr Z3_model -> Ptr Z3_func_decl -> IO (Ptr Z3_ast) Source #
z3_model_get_func_interp :: Ptr Z3_context -> Ptr Z3_model -> Ptr Z3_func_decl -> IO (Ptr Z3_func_interp) Source #
z3_model_has_interp :: Ptr Z3_context -> Ptr Z3_model -> Ptr Z3_func_decl -> IO Z3_bool Source #
z3_model_get_num_consts :: Ptr Z3_context -> Ptr Z3_model -> IO CUInt Source #
z3_model_get_num_funcs :: Ptr Z3_context -> Ptr Z3_model -> IO CUInt Source #
z3_model_get_const_decl :: Ptr Z3_context -> Ptr Z3_model -> CUInt -> IO (Ptr Z3_func_decl) Source #
z3_model_get_func_decl :: Ptr Z3_context -> Ptr Z3_model -> CUInt -> IO (Ptr Z3_func_decl) Source #
z3_is_as_array :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_bool Source #
z3_get_as_array_func_decl :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_func_decl) Source #
z3_add_func_interp :: Ptr Z3_context -> Ptr Z3_model -> Ptr Z3_func_decl -> Ptr Z3_ast -> IO (Ptr Z3_func_interp) Source #
z3_add_const_interp :: Ptr Z3_context -> Ptr Z3_model -> Ptr Z3_func_decl -> Ptr Z3_ast -> IO () Source #
z3_func_interp_inc_ref :: Ptr Z3_context -> Ptr Z3_func_interp -> IO () Source #
z3_func_interp_dec_ref :: Ptr Z3_context -> Ptr Z3_func_interp -> IO () Source #
z3_func_interp_get_num_entries :: Ptr Z3_context -> Ptr Z3_func_interp -> IO CUInt Source #
z3_func_interp_get_entry :: Ptr Z3_context -> Ptr Z3_func_interp -> CUInt -> IO (Ptr Z3_func_entry) Source #
z3_func_interp_get_else :: Ptr Z3_context -> Ptr Z3_func_interp -> IO (Ptr Z3_ast) Source #
z3_func_interp_get_arity :: Ptr Z3_context -> Ptr Z3_func_interp -> IO CUInt Source #
z3_func_entry_inc_ref :: Ptr Z3_context -> Ptr Z3_func_entry -> IO () Source #
z3_func_entry_dec_ref :: Ptr Z3_context -> Ptr Z3_func_entry -> IO () Source #
z3_func_entry_get_value :: Ptr Z3_context -> Ptr Z3_func_entry -> IO (Ptr Z3_ast) Source #
z3_func_entry_get_num_args :: Ptr Z3_context -> Ptr Z3_func_entry -> IO CUInt Source #
z3_func_entry_get_arg :: Ptr Z3_context -> Ptr Z3_func_entry -> CUInt -> IO (Ptr Z3_ast) Source #
Constraints
z3_get_index_value :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt Source #
z3_model_to_string :: Ptr Z3_context -> Ptr Z3_model -> IO Z3_string Source #
Parameters
z3_mk_params :: Ptr Z3_context -> IO (Ptr Z3_params) Source #
z3_params_inc_ref :: Ptr Z3_context -> Ptr Z3_params -> IO () Source #
z3_params_dec_ref :: Ptr Z3_context -> Ptr Z3_params -> IO () Source #
z3_params_set_bool :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol -> Z3_bool -> IO () Source #
z3_params_set_uint :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol -> CUInt -> IO () Source #
z3_params_set_double :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol -> CDouble -> IO () Source #
z3_params_set_symbol :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol -> Ptr Z3_symbol -> IO () Source #
z3_params_to_string :: Ptr Z3_context -> Ptr Z3_params -> IO Z3_string Source #
Interpolation
z3_mk_interpolant :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #
z3_mk_interpolation_context :: Ptr Z3_config -> IO (Ptr Z3_context) Source #
z3_get_interpolant :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Ptr Z3_params -> IO (Ptr Z3_ast_vector) Source #
z3_compute_interpolant :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_params -> Ptr (Ptr Z3_ast_vector) -> Ptr (Ptr Z3_model) -> IO Z3_lbool Source #
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 Source #
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 Source #
z3_interpolation_profile :: Ptr Z3_context -> IO Z3_string Source #
z3_write_interpolation_problem :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> Ptr CUInt -> Ptr CChar -> CUInt -> Ptr (Ptr Z3_ast) -> IO () Source #
Tactics
z3_mk_tactic :: Ptr Z3_context -> Ptr CChar -> IO (Ptr Z3_tactic) Source #
z3_tactic_and_then :: Ptr Z3_context -> Ptr Z3_tactic -> Ptr Z3_tactic -> IO (Ptr Z3_tactic) Source #
z3_tactic_or_else :: Ptr Z3_context -> Ptr Z3_tactic -> Ptr Z3_tactic -> IO (Ptr Z3_tactic) Source #
z3_tactic_skip :: Ptr Z3_context -> IO (Ptr Z3_tactic) Source #
z3_tactic_try_for :: Ptr Z3_context -> Ptr Z3_tactic -> CUInt -> IO (Ptr Z3_tactic) Source #
z3_tactic_inc_ref :: Ptr Z3_context -> Ptr Z3_tactic -> IO () Source #
z3_tactic_dec_ref :: Ptr Z3_context -> Ptr Z3_tactic -> IO () Source #
z3_tactic_apply :: Ptr Z3_context -> Ptr Z3_tactic -> Ptr Z3_goal -> IO (Ptr Z3_apply_result) Source #
z3_apply_result_inc_ref :: Ptr Z3_context -> Ptr Z3_apply_result -> IO () Source #
z3_apply_result_dec_ref :: Ptr Z3_context -> Ptr Z3_apply_result -> IO () Source #
z3_apply_result_get_num_subgoals :: Ptr Z3_context -> Ptr Z3_apply_result -> IO CUInt Source #
z3_apply_result_get_subgoal :: Ptr Z3_context -> Ptr Z3_apply_result -> CUInt -> IO (Ptr Z3_goal) Source #
z3_mk_goal :: Ptr Z3_context -> Z3_bool -> Z3_bool -> Z3_bool -> IO (Ptr Z3_goal) Source #
z3_goal_inc_ref :: Ptr Z3_context -> Ptr Z3_goal -> IO () Source #
z3_goal_dec_ref :: Ptr Z3_context -> Ptr Z3_goal -> IO () Source #
z3_goal_assert :: Ptr Z3_context -> Ptr Z3_goal -> Ptr Z3_ast -> IO () Source #
z3_goal_size :: Ptr Z3_context -> Ptr Z3_goal -> IO CUInt Source #
z3_goal_formula :: Ptr Z3_context -> Ptr Z3_goal -> CUInt -> IO (Ptr Z3_ast) Source #
Solvers
z3_mk_solver :: Ptr Z3_context -> IO (Ptr Z3_solver) Source #
z3_mk_simple_solver :: Ptr Z3_context -> IO (Ptr Z3_solver) Source #
z3_mk_solver_for_logic :: Ptr Z3_context -> Ptr Z3_symbol -> IO (Ptr Z3_solver) Source #
z3_solver_get_help :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_string Source #
z3_solver_set_params :: Ptr Z3_context -> Ptr Z3_solver -> Ptr Z3_params -> IO () Source #
z3_solver_inc_ref :: Ptr Z3_context -> Ptr Z3_solver -> IO () Source #
z3_solver_dec_ref :: Ptr Z3_context -> Ptr Z3_solver -> IO () Source #
z3_solver_push :: Ptr Z3_context -> Ptr Z3_solver -> IO () Source #
z3_solver_pop :: Ptr Z3_context -> Ptr Z3_solver -> CUInt -> IO () Source #
z3_solver_get_num_scopes :: Ptr Z3_context -> Ptr Z3_solver -> IO CUInt Source #
z3_solver_reset :: Ptr Z3_context -> Ptr Z3_solver -> IO () Source #
z3_solver_assert :: Ptr Z3_context -> Ptr Z3_solver -> Ptr Z3_ast -> IO () Source #
z3_solver_assert_and_track :: Ptr Z3_context -> Ptr Z3_solver -> Ptr Z3_ast -> Ptr Z3_ast -> IO () Source #
z3_solver_check :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_lbool Source #
z3_solver_check_assumptions :: Ptr Z3_context -> Ptr Z3_solver -> CUInt -> Ptr (Ptr Z3_ast) -> IO Z3_lbool Source #
z3_solver_get_model :: Ptr Z3_context -> Ptr Z3_solver -> IO (Ptr Z3_model) Source #
z3_solver_get_unsat_core :: Ptr Z3_context -> Ptr Z3_solver -> IO (Ptr Z3_ast_vector) Source #
z3_solver_get_reason_unknown :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_string Source #
z3_solver_to_string :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_string Source #
String Conversion
z3_set_ast_print_mode :: Ptr Z3_context -> Z3_ast_print_mode -> IO () Source #
z3_ast_to_string :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_string Source #
z3_pattern_to_string :: Ptr Z3_context -> Ptr Z3_pattern -> IO Z3_string Source #
z3_sort_to_string :: Ptr Z3_context -> Ptr Z3_sort -> IO Z3_string Source #
z3_func_decl_to_string :: Ptr Z3_context -> Ptr Z3_func_decl -> IO Z3_string Source #
Parser Interface
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) Source #
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) Source #
z3_get_parser_error :: Ptr Z3_context -> IO Z3_string Source #
Error Handling
z3_get_error_code :: Ptr Z3_context -> IO Z3_error_code Source #
z3_set_error_handler :: Ptr Z3_context -> FunPtr Z3_error_handler -> IO () Source #
z3_set_error :: Ptr Z3_context -> Z3_error_code -> IO () Source #
z3_get_error_msg :: Z3_error_code -> IO Z3_string Source #
z3_get_error_msg_ex :: Ptr Z3_context -> Z3_error_code -> IO Z3_string Source #
Miscellaneous
z3_get_version :: Ptr CUInt -> Ptr CUInt -> Ptr CUInt -> Ptr CUInt -> IO () Source #
Fixedpoint facilities
z3_mk_fixedpoint :: Ptr Z3_context -> IO (Ptr Z3_fixedpoint) Source #
z3_fixedpoint_push :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO () Source #
z3_fixedpoint_pop :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO () Source #
z3_fixedpoint_inc_ref :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO () Source #
z3_fixedpoint_dec_ref :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO () Source #
z3_fixedpoint_set_params :: Ptr Z3_context -> Ptr Z3_fixedpoint -> Ptr Z3_params -> IO () Source #
z3_fixedpoint_add_rule :: Ptr Z3_context -> Ptr Z3_fixedpoint -> Ptr Z3_ast -> Ptr Z3_symbol -> IO () Source #
z3_fixedpoint_register_relation :: Ptr Z3_context -> Ptr Z3_fixedpoint -> Ptr Z3_func_decl -> IO () Source #
z3_fixedpoint_get_answer :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO (Ptr Z3_ast) Source #
z3_fixedpoint_get_assertions :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO (Ptr Z3_ast_vector) Source #
z3_fixedpoint_query_relations :: Ptr Z3_context -> Ptr Z3_fixedpoint -> CUInt -> Ptr (Ptr Z3_func_decl) -> IO Z3_lbool Source #