|
static void | Z3_set_error_handler (Z3_context a0, Z3_error_handler a1) |
|
static void | Z3_global_param_set (string a0, string a1) |
|
static void | Z3_global_param_reset_all () |
|
static int | Z3_global_param_get (string a0, out IntPtr a1) |
|
static Z3_config | Z3_mk_config () |
|
static void | Z3_del_config (Z3_config a0) |
|
static void | Z3_set_param_value (Z3_config a0, string a1, string a2) |
|
static Z3_context | Z3_mk_context (Z3_config a0) |
|
static Z3_context | Z3_mk_context_rc (Z3_config a0) |
|
static void | Z3_del_context (Z3_context a0) |
|
static void | Z3_inc_ref (Z3_context a0, Z3_ast a1) |
|
static void | Z3_dec_ref (Z3_context a0, Z3_ast a1) |
|
static void | Z3_update_param_value (Z3_context a0, string a1, string a2) |
|
static void | Z3_interrupt (Z3_context a0) |
|
static Z3_params | Z3_mk_params (Z3_context a0) |
|
static void | Z3_params_inc_ref (Z3_context a0, Z3_params a1) |
|
static void | Z3_params_dec_ref (Z3_context a0, Z3_params a1) |
|
static void | Z3_params_set_bool (Z3_context a0, Z3_params a1, IntPtr a2, int a3) |
|
static void | Z3_params_set_uint (Z3_context a0, Z3_params a1, IntPtr a2, uint a3) |
|
static void | Z3_params_set_double (Z3_context a0, Z3_params a1, IntPtr a2, double a3) |
|
static void | Z3_params_set_symbol (Z3_context a0, Z3_params a1, IntPtr a2, IntPtr a3) |
|
static IntPtr | Z3_params_to_string (Z3_context a0, Z3_params a1) |
|
static void | Z3_params_validate (Z3_context a0, Z3_params a1, Z3_param_descrs a2) |
|
static void | Z3_param_descrs_inc_ref (Z3_context a0, Z3_param_descrs a1) |
|
static void | Z3_param_descrs_dec_ref (Z3_context a0, Z3_param_descrs a1) |
|
static uint | Z3_param_descrs_get_kind (Z3_context a0, Z3_param_descrs a1, IntPtr a2) |
|
static uint | Z3_param_descrs_size (Z3_context a0, Z3_param_descrs a1) |
|
static IntPtr | Z3_param_descrs_get_name (Z3_context a0, Z3_param_descrs a1, uint a2) |
|
static IntPtr | Z3_param_descrs_to_string (Z3_context a0, Z3_param_descrs a1) |
|
static IntPtr | Z3_mk_int_symbol (Z3_context a0, int a1) |
|
static IntPtr | Z3_mk_string_symbol (Z3_context a0, string a1) |
|
static Z3_sort | Z3_mk_uninterpreted_sort (Z3_context a0, IntPtr a1) |
|
static Z3_sort | Z3_mk_bool_sort (Z3_context a0) |
|
static Z3_sort | Z3_mk_int_sort (Z3_context a0) |
|
static Z3_sort | Z3_mk_real_sort (Z3_context a0) |
|
static Z3_sort | Z3_mk_bv_sort (Z3_context a0, uint a1) |
|
static Z3_sort | Z3_mk_finite_domain_sort (Z3_context a0, IntPtr a1, UInt64 a2) |
|
static Z3_sort | Z3_mk_array_sort (Z3_context a0, Z3_sort a1, Z3_sort a2) |
|
static Z3_sort | Z3_mk_tuple_sort (Z3_context a0, IntPtr a1, uint a2, [In] IntPtr[] a3, [In] Z3_sort[] a4, [In, Out] ref Z3_func_decl a5, [Out] Z3_func_decl[] a6) |
|
static Z3_sort | Z3_mk_enumeration_sort (Z3_context a0, IntPtr a1, uint a2, [In] IntPtr[] a3, [Out] Z3_func_decl[] a4, [Out] Z3_func_decl[] a5) |
|
static Z3_sort | Z3_mk_list_sort (Z3_context a0, IntPtr a1, Z3_sort a2, [In, Out] ref Z3_func_decl a3, [In, Out] ref Z3_func_decl a4, [In, Out] ref Z3_func_decl a5, [In, Out] ref Z3_func_decl a6, [In, Out] ref Z3_func_decl a7, [In, Out] ref Z3_func_decl a8) |
|
static Z3_constructor | Z3_mk_constructor (Z3_context a0, IntPtr a1, IntPtr a2, uint a3, [In] IntPtr[] a4, [In] Z3_sort[] a5, [In] uint[] a6) |
|
static void | Z3_del_constructor (Z3_context a0, Z3_constructor a1) |
|
static Z3_sort | Z3_mk_datatype (Z3_context a0, IntPtr a1, uint a2, [In, Out] Z3_constructor[] a3) |
|
static Z3_constructor_list | Z3_mk_constructor_list (Z3_context a0, uint a1, [In] Z3_constructor[] a2) |
|
static void | Z3_del_constructor_list (Z3_context a0, Z3_constructor_list a1) |
|
static void | Z3_mk_datatypes (Z3_context a0, uint a1, [In] IntPtr[] a2, [Out] Z3_sort[] a3, [In, Out] Z3_constructor_list[] a4) |
|
static void | Z3_query_constructor (Z3_context a0, Z3_constructor a1, uint a2, [In, Out] ref Z3_func_decl a3, [In, Out] ref Z3_func_decl a4, [Out] Z3_func_decl[] a5) |
|
static Z3_func_decl | Z3_mk_func_decl (Z3_context a0, IntPtr a1, uint a2, [In] Z3_sort[] a3, Z3_sort a4) |
|
static Z3_ast | Z3_mk_app (Z3_context a0, Z3_func_decl a1, uint a2, [In] Z3_ast[] a3) |
|
static Z3_ast | Z3_mk_const (Z3_context a0, IntPtr a1, Z3_sort a2) |
|
static Z3_func_decl | Z3_mk_fresh_func_decl (Z3_context a0, string a1, uint a2, [In] Z3_sort[] a3, Z3_sort a4) |
|
static Z3_ast | Z3_mk_fresh_const (Z3_context a0, string a1, Z3_sort a2) |
|
static Z3_ast | Z3_mk_true (Z3_context a0) |
|
static Z3_ast | Z3_mk_false (Z3_context a0) |
|
static Z3_ast | Z3_mk_eq (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_distinct (Z3_context a0, uint a1, [In] Z3_ast[] a2) |
|
static Z3_ast | Z3_mk_not (Z3_context a0, Z3_ast a1) |
|
static Z3_ast | Z3_mk_ite (Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3) |
|
static Z3_ast | Z3_mk_iff (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_implies (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_xor (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_and (Z3_context a0, uint a1, [In] Z3_ast[] a2) |
|
static Z3_ast | Z3_mk_or (Z3_context a0, uint a1, [In] Z3_ast[] a2) |
|
static Z3_ast | Z3_mk_add (Z3_context a0, uint a1, [In] Z3_ast[] a2) |
|
static Z3_ast | Z3_mk_mul (Z3_context a0, uint a1, [In] Z3_ast[] a2) |
|
static Z3_ast | Z3_mk_sub (Z3_context a0, uint a1, [In] Z3_ast[] a2) |
|
static Z3_ast | Z3_mk_unary_minus (Z3_context a0, Z3_ast a1) |
|
static Z3_ast | Z3_mk_div (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_mod (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_rem (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_power (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_lt (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_le (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_gt (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_ge (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_int2real (Z3_context a0, Z3_ast a1) |
|
static Z3_ast | Z3_mk_real2int (Z3_context a0, Z3_ast a1) |
|
static Z3_ast | Z3_mk_is_int (Z3_context a0, Z3_ast a1) |
|
static Z3_ast | Z3_mk_bvnot (Z3_context a0, Z3_ast a1) |
|
static Z3_ast | Z3_mk_bvredand (Z3_context a0, Z3_ast a1) |
|
static Z3_ast | Z3_mk_bvredor (Z3_context a0, Z3_ast a1) |
|
static Z3_ast | Z3_mk_bvand (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_bvor (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_bvxor (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_bvnand (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_bvnor (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_bvxnor (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_bvneg (Z3_context a0, Z3_ast a1) |
|
static Z3_ast | Z3_mk_bvadd (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_bvsub (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_bvmul (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_bvudiv (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_bvsdiv (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_bvurem (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_bvsrem (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_bvsmod (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_bvult (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_bvslt (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_bvule (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_bvsle (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_bvuge (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_bvsge (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_bvugt (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_bvsgt (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_concat (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_extract (Z3_context a0, uint a1, uint a2, Z3_ast a3) |
|
static Z3_ast | Z3_mk_sign_ext (Z3_context a0, uint a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_zero_ext (Z3_context a0, uint a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_repeat (Z3_context a0, uint a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_bvshl (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_bvlshr (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_bvashr (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_rotate_left (Z3_context a0, uint a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_rotate_right (Z3_context a0, uint a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_ext_rotate_left (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_ext_rotate_right (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_int2bv (Z3_context a0, uint a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_bv2int (Z3_context a0, Z3_ast a1, int a2) |
|
static Z3_ast | Z3_mk_bvadd_no_overflow (Z3_context a0, Z3_ast a1, Z3_ast a2, int a3) |
|
static Z3_ast | Z3_mk_bvadd_no_underflow (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_bvsub_no_overflow (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_bvsub_no_underflow (Z3_context a0, Z3_ast a1, Z3_ast a2, int a3) |
|
static Z3_ast | Z3_mk_bvsdiv_no_overflow (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_bvneg_no_overflow (Z3_context a0, Z3_ast a1) |
|
static Z3_ast | Z3_mk_bvmul_no_overflow (Z3_context a0, Z3_ast a1, Z3_ast a2, int a3) |
|
static Z3_ast | Z3_mk_bvmul_no_underflow (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_select (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_store (Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3) |
|
static Z3_ast | Z3_mk_const_array (Z3_context a0, Z3_sort a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_map (Z3_context a0, Z3_func_decl a1, uint a2, [In] Z3_ast[] a3) |
|
static Z3_ast | Z3_mk_array_default (Z3_context a0, Z3_ast a1) |
|
static Z3_sort | Z3_mk_set_sort (Z3_context a0, Z3_sort a1) |
|
static Z3_ast | Z3_mk_empty_set (Z3_context a0, Z3_sort a1) |
|
static Z3_ast | Z3_mk_full_set (Z3_context a0, Z3_sort a1) |
|
static Z3_ast | Z3_mk_set_add (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_set_del (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_set_union (Z3_context a0, uint a1, [In] Z3_ast[] a2) |
|
static Z3_ast | Z3_mk_set_intersect (Z3_context a0, uint a1, [In] Z3_ast[] a2) |
|
static Z3_ast | Z3_mk_set_difference (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_set_complement (Z3_context a0, Z3_ast a1) |
|
static Z3_ast | Z3_mk_set_member (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_set_subset (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_numeral (Z3_context a0, string a1, Z3_sort a2) |
|
static Z3_ast | Z3_mk_real (Z3_context a0, int a1, int a2) |
|
static Z3_ast | Z3_mk_int (Z3_context a0, int a1, Z3_sort a2) |
|
static Z3_ast | Z3_mk_unsigned_int (Z3_context a0, uint a1, Z3_sort a2) |
|
static Z3_ast | Z3_mk_int64 (Z3_context a0, Int64 a1, Z3_sort a2) |
|
static Z3_ast | Z3_mk_unsigned_int64 (Z3_context a0, UInt64 a1, Z3_sort a2) |
|
static Z3_pattern | Z3_mk_pattern (Z3_context a0, uint a1, [In] Z3_ast[] a2) |
|
static Z3_ast | Z3_mk_bound (Z3_context a0, uint a1, Z3_sort a2) |
|
static Z3_ast | Z3_mk_forall (Z3_context a0, uint a1, uint a2, [In] Z3_pattern[] a3, uint a4, [In] Z3_sort[] a5, [In] IntPtr[] a6, Z3_ast a7) |
|
static Z3_ast | Z3_mk_exists (Z3_context a0, uint a1, uint a2, [In] Z3_pattern[] a3, uint a4, [In] Z3_sort[] a5, [In] IntPtr[] a6, Z3_ast a7) |
|
static Z3_ast | Z3_mk_quantifier (Z3_context a0, int a1, uint a2, uint a3, [In] Z3_pattern[] a4, uint a5, [In] Z3_sort[] a6, [In] IntPtr[] a7, Z3_ast a8) |
|
static Z3_ast | Z3_mk_quantifier_ex (Z3_context a0, int a1, uint a2, IntPtr a3, IntPtr a4, uint a5, [In] Z3_pattern[] a6, uint a7, [In] Z3_ast[] a8, uint a9, [In] Z3_sort[] a10, [In] IntPtr[] a11, Z3_ast a12) |
|
static Z3_ast | Z3_mk_forall_const (Z3_context a0, uint a1, uint a2, [In] Z3_app[] a3, uint a4, [In] Z3_pattern[] a5, Z3_ast a6) |
|
static Z3_ast | Z3_mk_exists_const (Z3_context a0, uint a1, uint a2, [In] Z3_app[] a3, uint a4, [In] Z3_pattern[] a5, Z3_ast a6) |
|
static Z3_ast | Z3_mk_quantifier_const (Z3_context a0, int a1, uint a2, uint a3, [In] Z3_app[] a4, uint a5, [In] Z3_pattern[] a6, Z3_ast a7) |
|
static Z3_ast | Z3_mk_quantifier_const_ex (Z3_context a0, int a1, uint a2, IntPtr a3, IntPtr a4, uint a5, [In] Z3_app[] a6, uint a7, [In] Z3_pattern[] a8, uint a9, [In] Z3_ast[] a10, Z3_ast a11) |
|
static uint | Z3_get_symbol_kind (Z3_context a0, IntPtr a1) |
|
static int | Z3_get_symbol_int (Z3_context a0, IntPtr a1) |
|
static IntPtr | Z3_get_symbol_string (Z3_context a0, IntPtr a1) |
|
static IntPtr | Z3_get_sort_name (Z3_context a0, Z3_sort a1) |
|
static uint | Z3_get_sort_id (Z3_context a0, Z3_sort a1) |
|
static Z3_ast | Z3_sort_to_ast (Z3_context a0, Z3_sort a1) |
|
static int | Z3_is_eq_sort (Z3_context a0, Z3_sort a1, Z3_sort a2) |
|
static uint | Z3_get_sort_kind (Z3_context a0, Z3_sort a1) |
|
static uint | Z3_get_bv_sort_size (Z3_context a0, Z3_sort a1) |
|
static int | Z3_get_finite_domain_sort_size (Z3_context a0, Z3_sort a1, [In, Out] ref UInt64 a2) |
|
static Z3_sort | Z3_get_array_sort_domain (Z3_context a0, Z3_sort a1) |
|
static Z3_sort | Z3_get_array_sort_range (Z3_context a0, Z3_sort a1) |
|
static Z3_func_decl | Z3_get_tuple_sort_mk_decl (Z3_context a0, Z3_sort a1) |
|
static uint | Z3_get_tuple_sort_num_fields (Z3_context a0, Z3_sort a1) |
|
static Z3_func_decl | Z3_get_tuple_sort_field_decl (Z3_context a0, Z3_sort a1, uint a2) |
|
static uint | Z3_get_datatype_sort_num_constructors (Z3_context a0, Z3_sort a1) |
|
static Z3_func_decl | Z3_get_datatype_sort_constructor (Z3_context a0, Z3_sort a1, uint a2) |
|
static Z3_func_decl | Z3_get_datatype_sort_recognizer (Z3_context a0, Z3_sort a1, uint a2) |
|
static Z3_func_decl | Z3_get_datatype_sort_constructor_accessor (Z3_context a0, Z3_sort a1, uint a2, uint a3) |
|
static Z3_ast | Z3_datatype_update_field (Z3_context a0, Z3_func_decl a1, Z3_ast a2, Z3_ast a3) |
|
static uint | Z3_get_relation_arity (Z3_context a0, Z3_sort a1) |
|
static Z3_sort | Z3_get_relation_column (Z3_context a0, Z3_sort a1, uint a2) |
|
static Z3_ast | Z3_mk_atmost (Z3_context a0, uint a1, [In] Z3_ast[] a2, uint a3) |
|
static Z3_ast | Z3_mk_pble (Z3_context a0, uint a1, [In] Z3_ast[] a2, [In] int[] a3, int a4) |
|
static Z3_ast | Z3_func_decl_to_ast (Z3_context a0, Z3_func_decl a1) |
|
static int | Z3_is_eq_func_decl (Z3_context a0, Z3_func_decl a1, Z3_func_decl a2) |
|
static uint | Z3_get_func_decl_id (Z3_context a0, Z3_func_decl a1) |
|
static IntPtr | Z3_get_decl_name (Z3_context a0, Z3_func_decl a1) |
|
static uint | Z3_get_decl_kind (Z3_context a0, Z3_func_decl a1) |
|
static uint | Z3_get_domain_size (Z3_context a0, Z3_func_decl a1) |
|
static uint | Z3_get_arity (Z3_context a0, Z3_func_decl a1) |
|
static Z3_sort | Z3_get_domain (Z3_context a0, Z3_func_decl a1, uint a2) |
|
static Z3_sort | Z3_get_range (Z3_context a0, Z3_func_decl a1) |
|
static uint | Z3_get_decl_num_parameters (Z3_context a0, Z3_func_decl a1) |
|
static uint | Z3_get_decl_parameter_kind (Z3_context a0, Z3_func_decl a1, uint a2) |
|
static int | Z3_get_decl_int_parameter (Z3_context a0, Z3_func_decl a1, uint a2) |
|
static double | Z3_get_decl_double_parameter (Z3_context a0, Z3_func_decl a1, uint a2) |
|
static IntPtr | Z3_get_decl_symbol_parameter (Z3_context a0, Z3_func_decl a1, uint a2) |
|
static Z3_sort | Z3_get_decl_sort_parameter (Z3_context a0, Z3_func_decl a1, uint a2) |
|
static Z3_ast | Z3_get_decl_ast_parameter (Z3_context a0, Z3_func_decl a1, uint a2) |
|
static Z3_func_decl | Z3_get_decl_func_decl_parameter (Z3_context a0, Z3_func_decl a1, uint a2) |
|
static IntPtr | Z3_get_decl_rational_parameter (Z3_context a0, Z3_func_decl a1, uint a2) |
|
static Z3_ast | Z3_app_to_ast (Z3_context a0, Z3_app a1) |
|
static Z3_func_decl | Z3_get_app_decl (Z3_context a0, Z3_app a1) |
|
static uint | Z3_get_app_num_args (Z3_context a0, Z3_app a1) |
|
static Z3_ast | Z3_get_app_arg (Z3_context a0, Z3_app a1, uint a2) |
|
static int | Z3_is_eq_ast (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static uint | Z3_get_ast_id (Z3_context a0, Z3_ast a1) |
|
static uint | Z3_get_ast_hash (Z3_context a0, Z3_ast a1) |
|
static Z3_sort | Z3_get_sort (Z3_context a0, Z3_ast a1) |
|
static int | Z3_is_well_sorted (Z3_context a0, Z3_ast a1) |
|
static uint | Z3_get_bool_value (Z3_context a0, Z3_ast a1) |
|
static uint | Z3_get_ast_kind (Z3_context a0, Z3_ast a1) |
|
static int | Z3_is_app (Z3_context a0, Z3_ast a1) |
|
static int | Z3_is_numeral_ast (Z3_context a0, Z3_ast a1) |
|
static int | Z3_is_algebraic_number (Z3_context a0, Z3_ast a1) |
|
static Z3_app | Z3_to_app (Z3_context a0, Z3_ast a1) |
|
static Z3_func_decl | Z3_to_func_decl (Z3_context a0, Z3_ast a1) |
|
static IntPtr | Z3_get_numeral_string (Z3_context a0, Z3_ast a1) |
|
static IntPtr | Z3_get_numeral_decimal_string (Z3_context a0, Z3_ast a1, uint a2) |
|
static Z3_ast | Z3_get_numerator (Z3_context a0, Z3_ast a1) |
|
static Z3_ast | Z3_get_denominator (Z3_context a0, Z3_ast a1) |
|
static int | Z3_get_numeral_small (Z3_context a0, Z3_ast a1, [In, Out] ref Int64 a2, [In, Out] ref Int64 a3) |
|
static int | Z3_get_numeral_int (Z3_context a0, Z3_ast a1, [In, Out] ref int a2) |
|
static int | Z3_get_numeral_uint (Z3_context a0, Z3_ast a1, [In, Out] ref uint a2) |
|
static int | Z3_get_numeral_uint64 (Z3_context a0, Z3_ast a1, [In, Out] ref UInt64 a2) |
|
static int | Z3_get_numeral_int64 (Z3_context a0, Z3_ast a1, [In, Out] ref Int64 a2) |
|
static int | Z3_get_numeral_rational_int64 (Z3_context a0, Z3_ast a1, [In, Out] ref Int64 a2, [In, Out] ref Int64 a3) |
|
static Z3_ast | Z3_get_algebraic_number_lower (Z3_context a0, Z3_ast a1, uint a2) |
|
static Z3_ast | Z3_get_algebraic_number_upper (Z3_context a0, Z3_ast a1, uint a2) |
|
static Z3_ast | Z3_pattern_to_ast (Z3_context a0, Z3_pattern a1) |
|
static uint | Z3_get_pattern_num_terms (Z3_context a0, Z3_pattern a1) |
|
static Z3_ast | Z3_get_pattern (Z3_context a0, Z3_pattern a1, uint a2) |
|
static uint | Z3_get_index_value (Z3_context a0, Z3_ast a1) |
|
static int | Z3_is_quantifier_forall (Z3_context a0, Z3_ast a1) |
|
static uint | Z3_get_quantifier_weight (Z3_context a0, Z3_ast a1) |
|
static uint | Z3_get_quantifier_num_patterns (Z3_context a0, Z3_ast a1) |
|
static Z3_pattern | Z3_get_quantifier_pattern_ast (Z3_context a0, Z3_ast a1, uint a2) |
|
static uint | Z3_get_quantifier_num_no_patterns (Z3_context a0, Z3_ast a1) |
|
static Z3_ast | Z3_get_quantifier_no_pattern_ast (Z3_context a0, Z3_ast a1, uint a2) |
|
static uint | Z3_get_quantifier_num_bound (Z3_context a0, Z3_ast a1) |
|
static IntPtr | Z3_get_quantifier_bound_name (Z3_context a0, Z3_ast a1, uint a2) |
|
static Z3_sort | Z3_get_quantifier_bound_sort (Z3_context a0, Z3_ast a1, uint a2) |
|
static Z3_ast | Z3_get_quantifier_body (Z3_context a0, Z3_ast a1) |
|
static Z3_ast | Z3_simplify (Z3_context a0, Z3_ast a1) |
|
static Z3_ast | Z3_simplify_ex (Z3_context a0, Z3_ast a1, Z3_params a2) |
|
static IntPtr | Z3_simplify_get_help (Z3_context a0) |
|
static Z3_param_descrs | Z3_simplify_get_param_descrs (Z3_context a0) |
|
static Z3_ast | Z3_update_term (Z3_context a0, Z3_ast a1, uint a2, [In] Z3_ast[] a3) |
|
static Z3_ast | Z3_substitute (Z3_context a0, Z3_ast a1, uint a2, [In] Z3_ast[] a3, [In] Z3_ast[] a4) |
|
static Z3_ast | Z3_substitute_vars (Z3_context a0, Z3_ast a1, uint a2, [In] Z3_ast[] a3) |
|
static Z3_ast | Z3_translate (Z3_context a0, Z3_ast a1, Z3_context a2) |
|
static void | Z3_model_inc_ref (Z3_context a0, Z3_model a1) |
|
static void | Z3_model_dec_ref (Z3_context a0, Z3_model a1) |
|
static int | Z3_model_eval (Z3_context a0, Z3_model a1, Z3_ast a2, int a3, [In, Out] ref Z3_ast a4) |
|
static Z3_ast | Z3_model_get_const_interp (Z3_context a0, Z3_model a1, Z3_func_decl a2) |
|
static int | Z3_model_has_interp (Z3_context a0, Z3_model a1, Z3_func_decl a2) |
|
static Z3_func_interp | Z3_model_get_func_interp (Z3_context a0, Z3_model a1, Z3_func_decl a2) |
|
static uint | Z3_model_get_num_consts (Z3_context a0, Z3_model a1) |
|
static Z3_func_decl | Z3_model_get_const_decl (Z3_context a0, Z3_model a1, uint a2) |
|
static uint | Z3_model_get_num_funcs (Z3_context a0, Z3_model a1) |
|
static Z3_func_decl | Z3_model_get_func_decl (Z3_context a0, Z3_model a1, uint a2) |
|
static uint | Z3_model_get_num_sorts (Z3_context a0, Z3_model a1) |
|
static Z3_sort | Z3_model_get_sort (Z3_context a0, Z3_model a1, uint a2) |
|
static Z3_ast_vector | Z3_model_get_sort_universe (Z3_context a0, Z3_model a1, Z3_sort a2) |
|
static int | Z3_is_as_array (Z3_context a0, Z3_ast a1) |
|
static Z3_func_decl | Z3_get_as_array_func_decl (Z3_context a0, Z3_ast a1) |
|
static void | Z3_func_interp_inc_ref (Z3_context a0, Z3_func_interp a1) |
|
static void | Z3_func_interp_dec_ref (Z3_context a0, Z3_func_interp a1) |
|
static uint | Z3_func_interp_get_num_entries (Z3_context a0, Z3_func_interp a1) |
|
static Z3_func_entry | Z3_func_interp_get_entry (Z3_context a0, Z3_func_interp a1, uint a2) |
|
static Z3_ast | Z3_func_interp_get_else (Z3_context a0, Z3_func_interp a1) |
|
static uint | Z3_func_interp_get_arity (Z3_context a0, Z3_func_interp a1) |
|
static void | Z3_func_entry_inc_ref (Z3_context a0, Z3_func_entry a1) |
|
static void | Z3_func_entry_dec_ref (Z3_context a0, Z3_func_entry a1) |
|
static Z3_ast | Z3_func_entry_get_value (Z3_context a0, Z3_func_entry a1) |
|
static uint | Z3_func_entry_get_num_args (Z3_context a0, Z3_func_entry a1) |
|
static Z3_ast | Z3_func_entry_get_arg (Z3_context a0, Z3_func_entry a1, uint a2) |
|
static int | Z3_open_log (string a0) |
|
static void | Z3_append_log (string a0) |
|
static void | Z3_close_log () |
|
static void | Z3_toggle_warning_messages (int a0) |
|
static void | Z3_set_ast_print_mode (Z3_context a0, uint a1) |
|
static IntPtr | Z3_ast_to_string (Z3_context a0, Z3_ast a1) |
|
static IntPtr | Z3_pattern_to_string (Z3_context a0, Z3_pattern a1) |
|
static IntPtr | Z3_sort_to_string (Z3_context a0, Z3_sort a1) |
|
static IntPtr | Z3_func_decl_to_string (Z3_context a0, Z3_func_decl a1) |
|
static IntPtr | Z3_model_to_string (Z3_context a0, Z3_model a1) |
|
static IntPtr | Z3_benchmark_to_smtlib_string (Z3_context a0, string a1, string a2, string a3, string a4, uint a5, [In] Z3_ast[] a6, Z3_ast a7) |
|
static Z3_ast | Z3_parse_smtlib2_string (Z3_context a0, string a1, uint a2, [In] IntPtr[] a3, [In] Z3_sort[] a4, uint a5, [In] IntPtr[] a6, [In] Z3_func_decl[] a7) |
|
static Z3_ast | Z3_parse_smtlib2_file (Z3_context a0, string a1, uint a2, [In] IntPtr[] a3, [In] Z3_sort[] a4, uint a5, [In] IntPtr[] a6, [In] Z3_func_decl[] a7) |
|
static void | Z3_parse_smtlib_string (Z3_context a0, string a1, uint a2, [In] IntPtr[] a3, [In] Z3_sort[] a4, uint a5, [In] IntPtr[] a6, [In] Z3_func_decl[] a7) |
|
static void | Z3_parse_smtlib_file (Z3_context a0, string a1, uint a2, [In] IntPtr[] a3, [In] Z3_sort[] a4, uint a5, [In] IntPtr[] a6, [In] Z3_func_decl[] a7) |
|
static uint | Z3_get_smtlib_num_formulas (Z3_context a0) |
|
static Z3_ast | Z3_get_smtlib_formula (Z3_context a0, uint a1) |
|
static uint | Z3_get_smtlib_num_assumptions (Z3_context a0) |
|
static Z3_ast | Z3_get_smtlib_assumption (Z3_context a0, uint a1) |
|
static uint | Z3_get_smtlib_num_decls (Z3_context a0) |
|
static Z3_func_decl | Z3_get_smtlib_decl (Z3_context a0, uint a1) |
|
static uint | Z3_get_smtlib_num_sorts (Z3_context a0) |
|
static Z3_sort | Z3_get_smtlib_sort (Z3_context a0, uint a1) |
|
static IntPtr | Z3_get_smtlib_error (Z3_context a0) |
|
static uint | Z3_get_error_code (Z3_context a0) |
|
static void | Z3_set_error (Z3_context a0, uint a1) |
|
static IntPtr | Z3_get_error_msg (uint a0) |
|
static IntPtr | Z3_get_error_msg_ex (Z3_context a0, uint a1) |
|
static void | Z3_get_version ([In, Out] ref uint a0, [In, Out] ref uint a1, [In, Out] ref uint a2, [In, Out] ref uint a3) |
|
static void | Z3_enable_trace (string a0) |
|
static void | Z3_disable_trace (string a0) |
|
static void | Z3_reset_memory () |
|
static void | Z3_finalize_memory () |
|
static Z3_fixedpoint | Z3_mk_fixedpoint (Z3_context a0) |
|
static void | Z3_fixedpoint_inc_ref (Z3_context a0, Z3_fixedpoint a1) |
|
static void | Z3_fixedpoint_dec_ref (Z3_context a0, Z3_fixedpoint a1) |
|
static void | Z3_fixedpoint_add_rule (Z3_context a0, Z3_fixedpoint a1, Z3_ast a2, IntPtr a3) |
|
static void | Z3_fixedpoint_add_fact (Z3_context a0, Z3_fixedpoint a1, Z3_func_decl a2, uint a3, [In] uint[] a4) |
|
static void | Z3_fixedpoint_assert (Z3_context a0, Z3_fixedpoint a1, Z3_ast a2) |
|
static int | Z3_fixedpoint_query (Z3_context a0, Z3_fixedpoint a1, Z3_ast a2) |
|
static int | Z3_fixedpoint_query_relations (Z3_context a0, Z3_fixedpoint a1, uint a2, [In] Z3_func_decl[] a3) |
|
static Z3_ast | Z3_fixedpoint_get_answer (Z3_context a0, Z3_fixedpoint a1) |
|
static IntPtr | Z3_fixedpoint_get_reason_unknown (Z3_context a0, Z3_fixedpoint a1) |
|
static void | Z3_fixedpoint_update_rule (Z3_context a0, Z3_fixedpoint a1, Z3_ast a2, IntPtr a3) |
|
static uint | Z3_fixedpoint_get_num_levels (Z3_context a0, Z3_fixedpoint a1, Z3_func_decl a2) |
|
static Z3_ast | Z3_fixedpoint_get_cover_delta (Z3_context a0, Z3_fixedpoint a1, int a2, Z3_func_decl a3) |
|
static void | Z3_fixedpoint_add_cover (Z3_context a0, Z3_fixedpoint a1, int a2, Z3_func_decl a3, Z3_ast a4) |
|
static Z3_stats | Z3_fixedpoint_get_statistics (Z3_context a0, Z3_fixedpoint a1) |
|
static void | Z3_fixedpoint_register_relation (Z3_context a0, Z3_fixedpoint a1, Z3_func_decl a2) |
|
static void | Z3_fixedpoint_set_predicate_representation (Z3_context a0, Z3_fixedpoint a1, Z3_func_decl a2, uint a3, [In] IntPtr[] a4) |
|
static Z3_ast_vector | Z3_fixedpoint_get_rules (Z3_context a0, Z3_fixedpoint a1) |
|
static Z3_ast_vector | Z3_fixedpoint_get_assertions (Z3_context a0, Z3_fixedpoint a1) |
|
static void | Z3_fixedpoint_set_params (Z3_context a0, Z3_fixedpoint a1, Z3_params a2) |
|
static IntPtr | Z3_fixedpoint_get_help (Z3_context a0, Z3_fixedpoint a1) |
|
static Z3_param_descrs | Z3_fixedpoint_get_param_descrs (Z3_context a0, Z3_fixedpoint a1) |
|
static IntPtr | Z3_fixedpoint_to_string (Z3_context a0, Z3_fixedpoint a1, uint a2, [In] Z3_ast[] a3) |
|
static Z3_ast_vector | Z3_fixedpoint_from_string (Z3_context a0, Z3_fixedpoint a1, string a2) |
|
static Z3_ast_vector | Z3_fixedpoint_from_file (Z3_context a0, Z3_fixedpoint a1, string a2) |
|
static void | Z3_fixedpoint_push (Z3_context a0, Z3_fixedpoint a1) |
|
static void | Z3_fixedpoint_pop (Z3_context a0, Z3_fixedpoint a1) |
|
static Z3_optimize | Z3_mk_optimize (Z3_context a0) |
|
static void | Z3_optimize_inc_ref (Z3_context a0, Z3_optimize a1) |
|
static void | Z3_optimize_dec_ref (Z3_context a0, Z3_optimize a1) |
|
static void | Z3_optimize_assert (Z3_context a0, Z3_optimize a1, Z3_ast a2) |
|
static uint | Z3_optimize_assert_soft (Z3_context a0, Z3_optimize a1, Z3_ast a2, string a3, IntPtr a4) |
|
static uint | Z3_optimize_maximize (Z3_context a0, Z3_optimize a1, Z3_ast a2) |
|
static uint | Z3_optimize_minimize (Z3_context a0, Z3_optimize a1, Z3_ast a2) |
|
static void | Z3_optimize_push (Z3_context a0, Z3_optimize a1) |
|
static void | Z3_optimize_pop (Z3_context a0, Z3_optimize a1) |
|
static int | Z3_optimize_check (Z3_context a0, Z3_optimize a1) |
|
static IntPtr | Z3_optimize_get_reason_unknown (Z3_context a0, Z3_optimize a1) |
|
static Z3_model | Z3_optimize_get_model (Z3_context a0, Z3_optimize a1) |
|
static void | Z3_optimize_set_params (Z3_context a0, Z3_optimize a1, Z3_params a2) |
|
static Z3_param_descrs | Z3_optimize_get_param_descrs (Z3_context a0, Z3_optimize a1) |
|
static Z3_ast | Z3_optimize_get_lower (Z3_context a0, Z3_optimize a1, uint a2) |
|
static Z3_ast | Z3_optimize_get_upper (Z3_context a0, Z3_optimize a1, uint a2) |
|
static IntPtr | Z3_optimize_to_string (Z3_context a0, Z3_optimize a1) |
|
static IntPtr | Z3_optimize_get_help (Z3_context a0, Z3_optimize a1) |
|
static Z3_stats | Z3_optimize_get_statistics (Z3_context a0, Z3_optimize a1) |
|
static Z3_ast_vector | Z3_mk_ast_vector (Z3_context a0) |
|
static void | Z3_ast_vector_inc_ref (Z3_context a0, Z3_ast_vector a1) |
|
static void | Z3_ast_vector_dec_ref (Z3_context a0, Z3_ast_vector a1) |
|
static uint | Z3_ast_vector_size (Z3_context a0, Z3_ast_vector a1) |
|
static Z3_ast | Z3_ast_vector_get (Z3_context a0, Z3_ast_vector a1, uint a2) |
|
static void | Z3_ast_vector_set (Z3_context a0, Z3_ast_vector a1, uint a2, Z3_ast a3) |
|
static void | Z3_ast_vector_resize (Z3_context a0, Z3_ast_vector a1, uint a2) |
|
static void | Z3_ast_vector_push (Z3_context a0, Z3_ast_vector a1, Z3_ast a2) |
|
static Z3_ast_vector | Z3_ast_vector_translate (Z3_context a0, Z3_ast_vector a1, Z3_context a2) |
|
static IntPtr | Z3_ast_vector_to_string (Z3_context a0, Z3_ast_vector a1) |
|
static Z3_ast_map | Z3_mk_ast_map (Z3_context a0) |
|
static void | Z3_ast_map_inc_ref (Z3_context a0, Z3_ast_map a1) |
|
static void | Z3_ast_map_dec_ref (Z3_context a0, Z3_ast_map a1) |
|
static int | Z3_ast_map_contains (Z3_context a0, Z3_ast_map a1, Z3_ast a2) |
|
static Z3_ast | Z3_ast_map_find (Z3_context a0, Z3_ast_map a1, Z3_ast a2) |
|
static void | Z3_ast_map_insert (Z3_context a0, Z3_ast_map a1, Z3_ast a2, Z3_ast a3) |
|
static void | Z3_ast_map_erase (Z3_context a0, Z3_ast_map a1, Z3_ast a2) |
|
static void | Z3_ast_map_reset (Z3_context a0, Z3_ast_map a1) |
|
static uint | Z3_ast_map_size (Z3_context a0, Z3_ast_map a1) |
|
static Z3_ast_vector | Z3_ast_map_keys (Z3_context a0, Z3_ast_map a1) |
|
static IntPtr | Z3_ast_map_to_string (Z3_context a0, Z3_ast_map a1) |
|
static Z3_goal | Z3_mk_goal (Z3_context a0, int a1, int a2, int a3) |
|
static void | Z3_goal_inc_ref (Z3_context a0, Z3_goal a1) |
|
static void | Z3_goal_dec_ref (Z3_context a0, Z3_goal a1) |
|
static uint | Z3_goal_precision (Z3_context a0, Z3_goal a1) |
|
static void | Z3_goal_assert (Z3_context a0, Z3_goal a1, Z3_ast a2) |
|
static int | Z3_goal_inconsistent (Z3_context a0, Z3_goal a1) |
|
static uint | Z3_goal_depth (Z3_context a0, Z3_goal a1) |
|
static void | Z3_goal_reset (Z3_context a0, Z3_goal a1) |
|
static uint | Z3_goal_size (Z3_context a0, Z3_goal a1) |
|
static Z3_ast | Z3_goal_formula (Z3_context a0, Z3_goal a1, uint a2) |
|
static uint | Z3_goal_num_exprs (Z3_context a0, Z3_goal a1) |
|
static int | Z3_goal_is_decided_sat (Z3_context a0, Z3_goal a1) |
|
static int | Z3_goal_is_decided_unsat (Z3_context a0, Z3_goal a1) |
|
static Z3_goal | Z3_goal_translate (Z3_context a0, Z3_goal a1, Z3_context a2) |
|
static IntPtr | Z3_goal_to_string (Z3_context a0, Z3_goal a1) |
|
static Z3_tactic | Z3_mk_tactic (Z3_context a0, string a1) |
|
static void | Z3_tactic_inc_ref (Z3_context a0, Z3_tactic a1) |
|
static void | Z3_tactic_dec_ref (Z3_context a0, Z3_tactic a1) |
|
static Z3_probe | Z3_mk_probe (Z3_context a0, string a1) |
|
static void | Z3_probe_inc_ref (Z3_context a0, Z3_probe a1) |
|
static void | Z3_probe_dec_ref (Z3_context a0, Z3_probe a1) |
|
static Z3_tactic | Z3_tactic_and_then (Z3_context a0, Z3_tactic a1, Z3_tactic a2) |
|
static Z3_tactic | Z3_tactic_or_else (Z3_context a0, Z3_tactic a1, Z3_tactic a2) |
|
static Z3_tactic | Z3_tactic_par_or (Z3_context a0, uint a1, [In] Z3_tactic[] a2) |
|
static Z3_tactic | Z3_tactic_par_and_then (Z3_context a0, Z3_tactic a1, Z3_tactic a2) |
|
static Z3_tactic | Z3_tactic_try_for (Z3_context a0, Z3_tactic a1, uint a2) |
|
static Z3_tactic | Z3_tactic_when (Z3_context a0, Z3_probe a1, Z3_tactic a2) |
|
static Z3_tactic | Z3_tactic_cond (Z3_context a0, Z3_probe a1, Z3_tactic a2, Z3_tactic a3) |
|
static Z3_tactic | Z3_tactic_repeat (Z3_context a0, Z3_tactic a1, uint a2) |
|
static Z3_tactic | Z3_tactic_skip (Z3_context a0) |
|
static Z3_tactic | Z3_tactic_fail (Z3_context a0) |
|
static Z3_tactic | Z3_tactic_fail_if (Z3_context a0, Z3_probe a1) |
|
static Z3_tactic | Z3_tactic_fail_if_not_decided (Z3_context a0) |
|
static Z3_tactic | Z3_tactic_using_params (Z3_context a0, Z3_tactic a1, Z3_params a2) |
|
static Z3_probe | Z3_probe_const (Z3_context a0, double a1) |
|
static Z3_probe | Z3_probe_lt (Z3_context a0, Z3_probe a1, Z3_probe a2) |
|
static Z3_probe | Z3_probe_gt (Z3_context a0, Z3_probe a1, Z3_probe a2) |
|
static Z3_probe | Z3_probe_le (Z3_context a0, Z3_probe a1, Z3_probe a2) |
|
static Z3_probe | Z3_probe_ge (Z3_context a0, Z3_probe a1, Z3_probe a2) |
|
static Z3_probe | Z3_probe_eq (Z3_context a0, Z3_probe a1, Z3_probe a2) |
|
static Z3_probe | Z3_probe_and (Z3_context a0, Z3_probe a1, Z3_probe a2) |
|
static Z3_probe | Z3_probe_or (Z3_context a0, Z3_probe a1, Z3_probe a2) |
|
static Z3_probe | Z3_probe_not (Z3_context a0, Z3_probe a1) |
|
static uint | Z3_get_num_tactics (Z3_context a0) |
|
static IntPtr | Z3_get_tactic_name (Z3_context a0, uint a1) |
|
static uint | Z3_get_num_probes (Z3_context a0) |
|
static IntPtr | Z3_get_probe_name (Z3_context a0, uint a1) |
|
static IntPtr | Z3_tactic_get_help (Z3_context a0, Z3_tactic a1) |
|
static Z3_param_descrs | Z3_tactic_get_param_descrs (Z3_context a0, Z3_tactic a1) |
|
static IntPtr | Z3_tactic_get_descr (Z3_context a0, string a1) |
|
static IntPtr | Z3_probe_get_descr (Z3_context a0, string a1) |
|
static double | Z3_probe_apply (Z3_context a0, Z3_probe a1, Z3_goal a2) |
|
static Z3_apply_result | Z3_tactic_apply (Z3_context a0, Z3_tactic a1, Z3_goal a2) |
|
static Z3_apply_result | Z3_tactic_apply_ex (Z3_context a0, Z3_tactic a1, Z3_goal a2, Z3_params a3) |
|
static void | Z3_apply_result_inc_ref (Z3_context a0, Z3_apply_result a1) |
|
static void | Z3_apply_result_dec_ref (Z3_context a0, Z3_apply_result a1) |
|
static IntPtr | Z3_apply_result_to_string (Z3_context a0, Z3_apply_result a1) |
|
static uint | Z3_apply_result_get_num_subgoals (Z3_context a0, Z3_apply_result a1) |
|
static Z3_goal | Z3_apply_result_get_subgoal (Z3_context a0, Z3_apply_result a1, uint a2) |
|
static Z3_model | Z3_apply_result_convert_model (Z3_context a0, Z3_apply_result a1, uint a2, Z3_model a3) |
|
static Z3_solver | Z3_mk_solver (Z3_context a0) |
|
static Z3_solver | Z3_mk_simple_solver (Z3_context a0) |
|
static Z3_solver | Z3_mk_solver_for_logic (Z3_context a0, IntPtr a1) |
|
static Z3_solver | Z3_mk_solver_from_tactic (Z3_context a0, Z3_tactic a1) |
|
static IntPtr | Z3_solver_get_help (Z3_context a0, Z3_solver a1) |
|
static Z3_param_descrs | Z3_solver_get_param_descrs (Z3_context a0, Z3_solver a1) |
|
static void | Z3_solver_set_params (Z3_context a0, Z3_solver a1, Z3_params a2) |
|
static void | Z3_solver_inc_ref (Z3_context a0, Z3_solver a1) |
|
static void | Z3_solver_dec_ref (Z3_context a0, Z3_solver a1) |
|
static void | Z3_solver_push (Z3_context a0, Z3_solver a1) |
|
static void | Z3_solver_pop (Z3_context a0, Z3_solver a1, uint a2) |
|
static void | Z3_solver_reset (Z3_context a0, Z3_solver a1) |
|
static uint | Z3_solver_get_num_scopes (Z3_context a0, Z3_solver a1) |
|
static void | Z3_solver_assert (Z3_context a0, Z3_solver a1, Z3_ast a2) |
|
static void | Z3_solver_assert_and_track (Z3_context a0, Z3_solver a1, Z3_ast a2, Z3_ast a3) |
|
static Z3_ast_vector | Z3_solver_get_assertions (Z3_context a0, Z3_solver a1) |
|
static int | Z3_solver_check (Z3_context a0, Z3_solver a1) |
|
static int | Z3_solver_check_assumptions (Z3_context a0, Z3_solver a1, uint a2, [In] Z3_ast[] a3) |
|
static Z3_model | Z3_solver_get_model (Z3_context a0, Z3_solver a1) |
|
static Z3_ast | Z3_solver_get_proof (Z3_context a0, Z3_solver a1) |
|
static Z3_ast_vector | Z3_solver_get_unsat_core (Z3_context a0, Z3_solver a1) |
|
static IntPtr | Z3_solver_get_reason_unknown (Z3_context a0, Z3_solver a1) |
|
static Z3_stats | Z3_solver_get_statistics (Z3_context a0, Z3_solver a1) |
|
static IntPtr | Z3_solver_to_string (Z3_context a0, Z3_solver a1) |
|
static IntPtr | Z3_stats_to_string (Z3_context a0, Z3_stats a1) |
|
static void | Z3_stats_inc_ref (Z3_context a0, Z3_stats a1) |
|
static void | Z3_stats_dec_ref (Z3_context a0, Z3_stats a1) |
|
static uint | Z3_stats_size (Z3_context a0, Z3_stats a1) |
|
static IntPtr | Z3_stats_get_key (Z3_context a0, Z3_stats a1, uint a2) |
|
static int | Z3_stats_is_uint (Z3_context a0, Z3_stats a1, uint a2) |
|
static int | Z3_stats_is_double (Z3_context a0, Z3_stats a1, uint a2) |
|
static uint | Z3_stats_get_uint_value (Z3_context a0, Z3_stats a1, uint a2) |
|
static double | Z3_stats_get_double_value (Z3_context a0, Z3_stats a1, uint a2) |
|
static Z3_func_decl | Z3_mk_injective_function (Z3_context a0, IntPtr a1, uint a2, [In] Z3_sort[] a3, Z3_sort a4) |
|
static void | Z3_set_logic (Z3_context a0, string a1) |
|
static void | Z3_push (Z3_context a0) |
|
static void | Z3_pop (Z3_context a0, uint a1) |
|
static uint | Z3_get_num_scopes (Z3_context a0) |
|
static void | Z3_persist_ast (Z3_context a0, Z3_ast a1, uint a2) |
|
static void | Z3_assert_cnstr (Z3_context a0, Z3_ast a1) |
|
static int | Z3_check_and_get_model (Z3_context a0, [In, Out] ref Z3_model a1) |
|
static int | Z3_check (Z3_context a0) |
|
static int | Z3_check_assumptions (Z3_context a0, uint a1, [In] Z3_ast[] a2, [In, Out] ref Z3_model a3, [In, Out] ref Z3_ast a4, [In, Out] ref uint a5, [Out] Z3_ast[] a6) |
|
static uint | Z3_get_implied_equalities (Z3_context a0, Z3_solver a1, uint a2, [In] Z3_ast[] a3, [Out] uint[] a4) |
|
static void | Z3_del_model (Z3_context a0, Z3_model a1) |
|
static void | Z3_soft_check_cancel (Z3_context a0) |
|
static uint | Z3_get_search_failure (Z3_context a0) |
|
static Z3_ast | Z3_mk_label (Z3_context a0, IntPtr a1, int a2, Z3_ast a3) |
|
static Z3_literals | Z3_get_relevant_labels (Z3_context a0) |
|
static Z3_literals | Z3_get_relevant_literals (Z3_context a0) |
|
static Z3_literals | Z3_get_guessed_literals (Z3_context a0) |
|
static void | Z3_del_literals (Z3_context a0, Z3_literals a1) |
|
static uint | Z3_get_num_literals (Z3_context a0, Z3_literals a1) |
|
static IntPtr | Z3_get_label_symbol (Z3_context a0, Z3_literals a1, uint a2) |
|
static Z3_ast | Z3_get_literal (Z3_context a0, Z3_literals a1, uint a2) |
|
static void | Z3_disable_literal (Z3_context a0, Z3_literals a1, uint a2) |
|
static void | Z3_block_literals (Z3_context a0, Z3_literals a1) |
|
static uint | Z3_get_model_num_constants (Z3_context a0, Z3_model a1) |
|
static Z3_func_decl | Z3_get_model_constant (Z3_context a0, Z3_model a1, uint a2) |
|
static uint | Z3_get_model_num_funcs (Z3_context a0, Z3_model a1) |
|
static Z3_func_decl | Z3_get_model_func_decl (Z3_context a0, Z3_model a1, uint a2) |
|
static int | Z3_eval_func_decl (Z3_context a0, Z3_model a1, Z3_func_decl a2, [In, Out] ref Z3_ast a3) |
|
static int | Z3_is_array_value (Z3_context a0, Z3_model a1, Z3_ast a2, [In, Out] ref uint a3) |
|
static void | Z3_get_array_value (Z3_context a0, Z3_model a1, Z3_ast a2, uint a3, [Out] Z3_ast[] a4, [Out] Z3_ast[] a5, [In, Out] ref Z3_ast a6) |
|
static Z3_ast | Z3_get_model_func_else (Z3_context a0, Z3_model a1, uint a2) |
|
static uint | Z3_get_model_func_num_entries (Z3_context a0, Z3_model a1, uint a2) |
|
static uint | Z3_get_model_func_entry_num_args (Z3_context a0, Z3_model a1, uint a2, uint a3) |
|
static Z3_ast | Z3_get_model_func_entry_arg (Z3_context a0, Z3_model a1, uint a2, uint a3, uint a4) |
|
static Z3_ast | Z3_get_model_func_entry_value (Z3_context a0, Z3_model a1, uint a2, uint a3) |
|
static int | Z3_eval (Z3_context a0, Z3_model a1, Z3_ast a2, [In, Out] ref Z3_ast a3) |
|
static int | Z3_eval_decl (Z3_context a0, Z3_model a1, Z3_func_decl a2, uint a3, [In] Z3_ast[] a4, [In, Out] ref Z3_ast a5) |
|
static IntPtr | Z3_context_to_string (Z3_context a0) |
|
static IntPtr | Z3_statistics_to_string (Z3_context a0) |
|
static Z3_ast | Z3_get_context_assignment (Z3_context a0) |
|
static int | Z3_algebraic_is_value (Z3_context a0, Z3_ast a1) |
|
static int | Z3_algebraic_is_pos (Z3_context a0, Z3_ast a1) |
|
static int | Z3_algebraic_is_neg (Z3_context a0, Z3_ast a1) |
|
static int | Z3_algebraic_is_zero (Z3_context a0, Z3_ast a1) |
|
static int | Z3_algebraic_sign (Z3_context a0, Z3_ast a1) |
|
static Z3_ast | Z3_algebraic_add (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_algebraic_sub (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_algebraic_mul (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_algebraic_div (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_algebraic_root (Z3_context a0, Z3_ast a1, uint a2) |
|
static Z3_ast | Z3_algebraic_power (Z3_context a0, Z3_ast a1, uint a2) |
|
static int | Z3_algebraic_lt (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static int | Z3_algebraic_gt (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static int | Z3_algebraic_le (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static int | Z3_algebraic_ge (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static int | Z3_algebraic_eq (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static int | Z3_algebraic_neq (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast_vector | Z3_algebraic_roots (Z3_context a0, Z3_ast a1, uint a2, [In] Z3_ast[] a3) |
|
static int | Z3_algebraic_eval (Z3_context a0, Z3_ast a1, uint a2, [In] Z3_ast[] a3) |
|
static Z3_ast_vector | Z3_polynomial_subresultants (Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3) |
|
static void | Z3_rcf_del (Z3_context a0, Z3_rcf_num a1) |
|
static Z3_rcf_num | Z3_rcf_mk_rational (Z3_context a0, string a1) |
|
static Z3_rcf_num | Z3_rcf_mk_small_int (Z3_context a0, int a1) |
|
static Z3_rcf_num | Z3_rcf_mk_pi (Z3_context a0) |
|
static Z3_rcf_num | Z3_rcf_mk_e (Z3_context a0) |
|
static Z3_rcf_num | Z3_rcf_mk_infinitesimal (Z3_context a0) |
|
static uint | Z3_rcf_mk_roots (Z3_context a0, uint a1, [In] Z3_rcf_num[] a2, [Out] Z3_rcf_num[] a3) |
|
static Z3_rcf_num | Z3_rcf_add (Z3_context a0, Z3_rcf_num a1, Z3_rcf_num a2) |
|
static Z3_rcf_num | Z3_rcf_sub (Z3_context a0, Z3_rcf_num a1, Z3_rcf_num a2) |
|
static Z3_rcf_num | Z3_rcf_mul (Z3_context a0, Z3_rcf_num a1, Z3_rcf_num a2) |
|
static Z3_rcf_num | Z3_rcf_div (Z3_context a0, Z3_rcf_num a1, Z3_rcf_num a2) |
|
static Z3_rcf_num | Z3_rcf_neg (Z3_context a0, Z3_rcf_num a1) |
|
static Z3_rcf_num | Z3_rcf_inv (Z3_context a0, Z3_rcf_num a1) |
|
static Z3_rcf_num | Z3_rcf_power (Z3_context a0, Z3_rcf_num a1, uint a2) |
|
static int | Z3_rcf_lt (Z3_context a0, Z3_rcf_num a1, Z3_rcf_num a2) |
|
static int | Z3_rcf_gt (Z3_context a0, Z3_rcf_num a1, Z3_rcf_num a2) |
|
static int | Z3_rcf_le (Z3_context a0, Z3_rcf_num a1, Z3_rcf_num a2) |
|
static int | Z3_rcf_ge (Z3_context a0, Z3_rcf_num a1, Z3_rcf_num a2) |
|
static int | Z3_rcf_eq (Z3_context a0, Z3_rcf_num a1, Z3_rcf_num a2) |
|
static int | Z3_rcf_neq (Z3_context a0, Z3_rcf_num a1, Z3_rcf_num a2) |
|
static IntPtr | Z3_rcf_num_to_string (Z3_context a0, Z3_rcf_num a1, int a2, int a3) |
|
static IntPtr | Z3_rcf_num_to_decimal_string (Z3_context a0, Z3_rcf_num a1, uint a2) |
|
static void | Z3_rcf_get_numerator_denominator (Z3_context a0, Z3_rcf_num a1, [In, Out] ref Z3_rcf_num a2, [In, Out] ref Z3_rcf_num a3) |
|
static Z3_ast | Z3_mk_interpolant (Z3_context a0, Z3_ast a1) |
|
static Z3_context | Z3_mk_interpolation_context (Z3_config a0) |
|
static Z3_ast_vector | Z3_get_interpolant (Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_params a3) |
|
static int | Z3_compute_interpolant (Z3_context a0, Z3_ast a1, Z3_params a2, [In, Out] ref Z3_ast_vector a3, [In, Out] ref Z3_model a4) |
|
static IntPtr | Z3_interpolation_profile (Z3_context a0) |
|
static int | Z3_read_interpolation_problem (Z3_context a0, [In, Out] ref uint a1, [Out] out Z3_ast[] a2, [Out] out uint[] a3, string a4, out IntPtr a5, [In, Out] ref uint a6, [Out] out Z3_ast[] a7) |
|
static int | Z3_check_interpolant (Z3_context a0, uint a1, [In] Z3_ast[] a2, [In] uint[] a3, [In] Z3_ast[] a4, out IntPtr a5, uint a6, [In] Z3_ast[] a7) |
|
static void | Z3_write_interpolation_problem (Z3_context a0, uint a1, [In] Z3_ast[] a2, [In] uint[] a3, string a4, uint a5, [In] Z3_ast[] a6) |
|
static Z3_sort | Z3_mk_fpa_rounding_mode_sort (Z3_context a0) |
|
static Z3_ast | Z3_mk_fpa_round_nearest_ties_to_even (Z3_context a0) |
|
static Z3_ast | Z3_mk_fpa_rne (Z3_context a0) |
|
static Z3_ast | Z3_mk_fpa_round_nearest_ties_to_away (Z3_context a0) |
|
static Z3_ast | Z3_mk_fpa_rna (Z3_context a0) |
|
static Z3_ast | Z3_mk_fpa_round_toward_positive (Z3_context a0) |
|
static Z3_ast | Z3_mk_fpa_rtp (Z3_context a0) |
|
static Z3_ast | Z3_mk_fpa_round_toward_negative (Z3_context a0) |
|
static Z3_ast | Z3_mk_fpa_rtn (Z3_context a0) |
|
static Z3_ast | Z3_mk_fpa_round_toward_zero (Z3_context a0) |
|
static Z3_ast | Z3_mk_fpa_rtz (Z3_context a0) |
|
static Z3_sort | Z3_mk_fpa_sort (Z3_context a0, uint a1, uint a2) |
|
static Z3_sort | Z3_mk_fpa_sort_half (Z3_context a0) |
|
static Z3_sort | Z3_mk_fpa_sort_16 (Z3_context a0) |
|
static Z3_sort | Z3_mk_fpa_sort_single (Z3_context a0) |
|
static Z3_sort | Z3_mk_fpa_sort_32 (Z3_context a0) |
|
static Z3_sort | Z3_mk_fpa_sort_double (Z3_context a0) |
|
static Z3_sort | Z3_mk_fpa_sort_64 (Z3_context a0) |
|
static Z3_sort | Z3_mk_fpa_sort_quadruple (Z3_context a0) |
|
static Z3_sort | Z3_mk_fpa_sort_128 (Z3_context a0) |
|
static Z3_ast | Z3_mk_fpa_nan (Z3_context a0, Z3_sort a1) |
|
static Z3_ast | Z3_mk_fpa_inf (Z3_context a0, Z3_sort a1, int a2) |
|
static Z3_ast | Z3_mk_fpa_zero (Z3_context a0, Z3_sort a1, int a2) |
|
static Z3_ast | Z3_mk_fpa_fp (Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3) |
|
static Z3_ast | Z3_mk_fpa_numeral_float (Z3_context a0, float a1, Z3_sort a2) |
|
static Z3_ast | Z3_mk_fpa_numeral_double (Z3_context a0, double a1, Z3_sort a2) |
|
static Z3_ast | Z3_mk_fpa_numeral_int (Z3_context a0, int a1, Z3_sort a2) |
|
static Z3_ast | Z3_mk_fpa_numeral_int_uint (Z3_context a0, int a1, int a2, uint a3, Z3_sort a4) |
|
static Z3_ast | Z3_mk_fpa_numeral_int64_uint64 (Z3_context a0, int a1, Int64 a2, UInt64 a3, Z3_sort a4) |
|
static Z3_ast | Z3_mk_fpa_abs (Z3_context a0, Z3_ast a1) |
|
static Z3_ast | Z3_mk_fpa_neg (Z3_context a0, Z3_ast a1) |
|
static Z3_ast | Z3_mk_fpa_add (Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3) |
|
static Z3_ast | Z3_mk_fpa_sub (Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3) |
|
static Z3_ast | Z3_mk_fpa_mul (Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3) |
|
static Z3_ast | Z3_mk_fpa_div (Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3) |
|
static Z3_ast | Z3_mk_fpa_fma (Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3, Z3_ast a4) |
|
static Z3_ast | Z3_mk_fpa_sqrt (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_fpa_rem (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_fpa_round_to_integral (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_fpa_min (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_fpa_max (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_fpa_leq (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_fpa_lt (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_fpa_geq (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_fpa_gt (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_fpa_eq (Z3_context a0, Z3_ast a1, Z3_ast a2) |
|
static Z3_ast | Z3_mk_fpa_is_normal (Z3_context a0, Z3_ast a1) |
|
static Z3_ast | Z3_mk_fpa_is_subnormal (Z3_context a0, Z3_ast a1) |
|
static Z3_ast | Z3_mk_fpa_is_zero (Z3_context a0, Z3_ast a1) |
|
static Z3_ast | Z3_mk_fpa_is_infinite (Z3_context a0, Z3_ast a1) |
|
static Z3_ast | Z3_mk_fpa_is_nan (Z3_context a0, Z3_ast a1) |
|
static Z3_ast | Z3_mk_fpa_is_negative (Z3_context a0, Z3_ast a1) |
|
static Z3_ast | Z3_mk_fpa_is_positive (Z3_context a0, Z3_ast a1) |
|
static Z3_ast | Z3_mk_fpa_to_fp_bv (Z3_context a0, Z3_ast a1, Z3_sort a2) |
|
static Z3_ast | Z3_mk_fpa_to_fp_float (Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_sort a3) |
|
static Z3_ast | Z3_mk_fpa_to_fp_real (Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_sort a3) |
|
static Z3_ast | Z3_mk_fpa_to_fp_signed (Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_sort a3) |
|
static Z3_ast | Z3_mk_fpa_to_fp_unsigned (Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_sort a3) |
|
static Z3_ast | Z3_mk_fpa_to_ubv (Z3_context a0, Z3_ast a1, Z3_ast a2, uint a3) |
|
static Z3_ast | Z3_mk_fpa_to_sbv (Z3_context a0, Z3_ast a1, Z3_ast a2, uint a3) |
|
static Z3_ast | Z3_mk_fpa_to_real (Z3_context a0, Z3_ast a1) |
|
static uint | Z3_fpa_get_ebits (Z3_context a0, Z3_sort a1) |
|
static uint | Z3_fpa_get_sbits (Z3_context a0, Z3_sort a1) |
|
static int | Z3_fpa_get_numeral_sign (Z3_context a0, Z3_ast a1, [In, Out] ref int a2) |
|
static IntPtr | Z3_fpa_get_numeral_significand_string (Z3_context a0, Z3_ast a1) |
|
static int | Z3_fpa_get_numeral_significand_uint64 (Z3_context a0, Z3_ast a1, [In, Out] ref UInt64 a2) |
|
static IntPtr | Z3_fpa_get_numeral_exponent_string (Z3_context a0, Z3_ast a1) |
|
static int | Z3_fpa_get_numeral_exponent_int64 (Z3_context a0, Z3_ast a1, [In, Out] ref Int64 a2) |
|
static Z3_ast | Z3_mk_fpa_to_ieee_bv (Z3_context a0, Z3_ast a1) |
|
static Z3_ast | Z3_mk_fpa_to_fp_int_real (Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3, Z3_sort a4) |
|