Z3
Static Public Member Functions
Native.LIB Class Reference

Static Public Member Functions

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)
 

Detailed Description

Definition at line 46 of file Native.cs.

Member Function Documentation

static Z3_ast Z3_algebraic_add ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_algebraic_add().

static Z3_ast Z3_algebraic_div ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_algebraic_div().

static int Z3_algebraic_eq ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_algebraic_eq().

static int Z3_algebraic_eval ( Z3_context  a0,
Z3_ast  a1,
uint  a2,
[In] Z3_ast[]  a3 
)
static
static int Z3_algebraic_ge ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_algebraic_ge().

static int Z3_algebraic_gt ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_algebraic_gt().

static int Z3_algebraic_is_neg ( Z3_context  a0,
Z3_ast  a1 
)
static
static int Z3_algebraic_is_pos ( Z3_context  a0,
Z3_ast  a1 
)
static
static int Z3_algebraic_is_value ( Z3_context  a0,
Z3_ast  a1 
)
static
static int Z3_algebraic_is_zero ( Z3_context  a0,
Z3_ast  a1 
)
static
static int Z3_algebraic_le ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_algebraic_le().

static int Z3_algebraic_lt ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_algebraic_lt().

static Z3_ast Z3_algebraic_mul ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_algebraic_mul().

static int Z3_algebraic_neq ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_algebraic_neq().

static Z3_ast Z3_algebraic_power ( Z3_context  a0,
Z3_ast  a1,
uint  a2 
)
static
static Z3_ast Z3_algebraic_root ( Z3_context  a0,
Z3_ast  a1,
uint  a2 
)
static
static Z3_ast_vector Z3_algebraic_roots ( Z3_context  a0,
Z3_ast  a1,
uint  a2,
[In] Z3_ast[]  a3 
)
static
static int Z3_algebraic_sign ( Z3_context  a0,
Z3_ast  a1 
)
static
static Z3_ast Z3_algebraic_sub ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_algebraic_sub().

static Z3_ast Z3_app_to_ast ( Z3_context  a0,
Z3_app  a1 
)
static

Referenced by Native.Z3_app_to_ast().

static void Z3_append_log ( string  a0)
static

Referenced by Native.Z3_append_log().

static Z3_model Z3_apply_result_convert_model ( Z3_context  a0,
Z3_apply_result  a1,
uint  a2,
Z3_model  a3 
)
static
static void Z3_apply_result_dec_ref ( Z3_context  a0,
Z3_apply_result  a1 
)
static
static uint Z3_apply_result_get_num_subgoals ( Z3_context  a0,
Z3_apply_result  a1 
)
static
static Z3_goal Z3_apply_result_get_subgoal ( Z3_context  a0,
Z3_apply_result  a1,
uint  a2 
)
static
static void Z3_apply_result_inc_ref ( Z3_context  a0,
Z3_apply_result  a1 
)
static
static IntPtr Z3_apply_result_to_string ( Z3_context  a0,
Z3_apply_result  a1 
)
static
static void Z3_assert_cnstr ( Z3_context  a0,
Z3_ast  a1 
)
static

Referenced by Native.Z3_assert_cnstr().

static int Z3_ast_map_contains ( Z3_context  a0,
Z3_ast_map  a1,
Z3_ast  a2 
)
static
static void Z3_ast_map_dec_ref ( Z3_context  a0,
Z3_ast_map  a1 
)
static
static void Z3_ast_map_erase ( Z3_context  a0,
Z3_ast_map  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_ast_map_erase().

static Z3_ast Z3_ast_map_find ( Z3_context  a0,
Z3_ast_map  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_ast_map_find().

static void Z3_ast_map_inc_ref ( Z3_context  a0,
Z3_ast_map  a1 
)
static
static void Z3_ast_map_insert ( Z3_context  a0,
Z3_ast_map  a1,
Z3_ast  a2,
Z3_ast  a3 
)
static
static Z3_ast_vector Z3_ast_map_keys ( Z3_context  a0,
Z3_ast_map  a1 
)
static

Referenced by Native.Z3_ast_map_keys().

static void Z3_ast_map_reset ( Z3_context  a0,
Z3_ast_map  a1 
)
static

Referenced by Native.Z3_ast_map_reset().

static uint Z3_ast_map_size ( Z3_context  a0,
Z3_ast_map  a1 
)
static

Referenced by Native.Z3_ast_map_size().

static IntPtr Z3_ast_map_to_string ( Z3_context  a0,
Z3_ast_map  a1 
)
static
static IntPtr Z3_ast_to_string ( Z3_context  a0,
Z3_ast  a1 
)
static

Referenced by Native.Z3_ast_to_string().

static void Z3_ast_vector_dec_ref ( Z3_context  a0,
Z3_ast_vector  a1 
)
static
static Z3_ast Z3_ast_vector_get ( Z3_context  a0,
Z3_ast_vector  a1,
uint  a2 
)
static
static void Z3_ast_vector_inc_ref ( Z3_context  a0,
Z3_ast_vector  a1 
)
static
static void Z3_ast_vector_push ( Z3_context  a0,
Z3_ast_vector  a1,
Z3_ast  a2 
)
static
static void Z3_ast_vector_resize ( Z3_context  a0,
Z3_ast_vector  a1,
uint  a2 
)
static
static void Z3_ast_vector_set ( Z3_context  a0,
Z3_ast_vector  a1,
uint  a2,
Z3_ast  a3 
)
static
static uint Z3_ast_vector_size ( Z3_context  a0,
Z3_ast_vector  a1 
)
static
static IntPtr Z3_ast_vector_to_string ( Z3_context  a0,
Z3_ast_vector  a1 
)
static
static Z3_ast_vector Z3_ast_vector_translate ( Z3_context  a0,
Z3_ast_vector  a1,
Z3_context  a2 
)
static
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
static void Z3_block_literals ( Z3_context  a0,
Z3_literals  a1 
)
static
static int Z3_check ( Z3_context  a0)
static

Referenced by Native.Z3_check().

static int Z3_check_and_get_model ( Z3_context  a0,
[In, Out] ref Z3_model  a1 
)
static
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
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
static void Z3_close_log ( )
static

Referenced by Native.Z3_close_log().

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
static IntPtr Z3_context_to_string ( Z3_context  a0)
static
static Z3_ast Z3_datatype_update_field ( Z3_context  a0,
Z3_func_decl  a1,
Z3_ast  a2,
Z3_ast  a3 
)
static
static void Z3_dec_ref ( Z3_context  a0,
Z3_ast  a1 
)
static

Referenced by Native.Z3_dec_ref().

static void Z3_del_config ( Z3_config  a0)
static

Referenced by Native.Z3_del_config().

static void Z3_del_constructor ( Z3_context  a0,
Z3_constructor  a1 
)
static
static void Z3_del_constructor_list ( Z3_context  a0,
Z3_constructor_list  a1 
)
static
static void Z3_del_context ( Z3_context  a0)
static

Referenced by Native.Z3_del_context().

static void Z3_del_literals ( Z3_context  a0,
Z3_literals  a1 
)
static

Referenced by Native.Z3_del_literals().

static void Z3_del_model ( Z3_context  a0,
Z3_model  a1 
)
static

Referenced by Native.Z3_del_model().

static void Z3_disable_literal ( Z3_context  a0,
Z3_literals  a1,
uint  a2 
)
static
static void Z3_disable_trace ( string  a0)
static

Referenced by Native.Z3_disable_trace().

static void Z3_enable_trace ( string  a0)
static

Referenced by Native.Z3_enable_trace().

static int Z3_eval ( Z3_context  a0,
Z3_model  a1,
Z3_ast  a2,
[In, Out] ref Z3_ast  a3 
)
static

Referenced by Native.Z3_eval().

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

Referenced by Native.Z3_eval_decl().

static int Z3_eval_func_decl ( Z3_context  a0,
Z3_model  a1,
Z3_func_decl  a2,
[In, Out] ref Z3_ast  a3 
)
static
static void Z3_finalize_memory ( )
static
static void Z3_fixedpoint_add_cover ( Z3_context  a0,
Z3_fixedpoint  a1,
int  a2,
Z3_func_decl  a3,
Z3_ast  a4 
)
static
static void Z3_fixedpoint_add_fact ( Z3_context  a0,
Z3_fixedpoint  a1,
Z3_func_decl  a2,
uint  a3,
[In] uint[]  a4 
)
static
static void Z3_fixedpoint_add_rule ( Z3_context  a0,
Z3_fixedpoint  a1,
Z3_ast  a2,
IntPtr  a3 
)
static
static void Z3_fixedpoint_assert ( Z3_context  a0,
Z3_fixedpoint  a1,
Z3_ast  a2 
)
static
static void Z3_fixedpoint_dec_ref ( Z3_context  a0,
Z3_fixedpoint  a1 
)
static
static Z3_ast_vector Z3_fixedpoint_from_file ( Z3_context  a0,
Z3_fixedpoint  a1,
string  a2 
)
static
static Z3_ast_vector Z3_fixedpoint_from_string ( Z3_context  a0,
Z3_fixedpoint  a1,
string  a2 
)
static
static Z3_ast Z3_fixedpoint_get_answer ( Z3_context  a0,
Z3_fixedpoint  a1 
)
static
static Z3_ast_vector Z3_fixedpoint_get_assertions ( Z3_context  a0,
Z3_fixedpoint  a1 
)
static
static Z3_ast Z3_fixedpoint_get_cover_delta ( Z3_context  a0,
Z3_fixedpoint  a1,
int  a2,
Z3_func_decl  a3 
)
static
static IntPtr Z3_fixedpoint_get_help ( Z3_context  a0,
Z3_fixedpoint  a1 
)
static
static uint Z3_fixedpoint_get_num_levels ( Z3_context  a0,
Z3_fixedpoint  a1,
Z3_func_decl  a2 
)
static
static Z3_param_descrs Z3_fixedpoint_get_param_descrs ( Z3_context  a0,
Z3_fixedpoint  a1 
)
static
static IntPtr Z3_fixedpoint_get_reason_unknown ( Z3_context  a0,
Z3_fixedpoint  a1 
)
static
static Z3_ast_vector Z3_fixedpoint_get_rules ( Z3_context  a0,
Z3_fixedpoint  a1 
)
static
static Z3_stats Z3_fixedpoint_get_statistics ( Z3_context  a0,
Z3_fixedpoint  a1 
)
static
static void Z3_fixedpoint_inc_ref ( Z3_context  a0,
Z3_fixedpoint  a1 
)
static
static void Z3_fixedpoint_pop ( Z3_context  a0,
Z3_fixedpoint  a1 
)
static
static void Z3_fixedpoint_push ( Z3_context  a0,
Z3_fixedpoint  a1 
)
static
static int Z3_fixedpoint_query ( Z3_context  a0,
Z3_fixedpoint  a1,
Z3_ast  a2 
)
static
static int Z3_fixedpoint_query_relations ( Z3_context  a0,
Z3_fixedpoint  a1,
uint  a2,
[In] Z3_func_decl[]  a3 
)
static
static void Z3_fixedpoint_register_relation ( Z3_context  a0,
Z3_fixedpoint  a1,
Z3_func_decl  a2 
)
static
static void Z3_fixedpoint_set_params ( Z3_context  a0,
Z3_fixedpoint  a1,
Z3_params  a2 
)
static
static void Z3_fixedpoint_set_predicate_representation ( Z3_context  a0,
Z3_fixedpoint  a1,
Z3_func_decl  a2,
uint  a3,
[In] IntPtr[]  a4 
)
static
static IntPtr Z3_fixedpoint_to_string ( Z3_context  a0,
Z3_fixedpoint  a1,
uint  a2,
[In] Z3_ast[]  a3 
)
static
static void Z3_fixedpoint_update_rule ( Z3_context  a0,
Z3_fixedpoint  a1,
Z3_ast  a2,
IntPtr  a3 
)
static
static uint Z3_fpa_get_ebits ( Z3_context  a0,
Z3_sort  a1 
)
static

Referenced by Native.Z3_fpa_get_ebits().

static int Z3_fpa_get_numeral_exponent_int64 ( Z3_context  a0,
Z3_ast  a1,
[In, Out] ref Int64  a2 
)
static
static IntPtr Z3_fpa_get_numeral_exponent_string ( Z3_context  a0,
Z3_ast  a1 
)
static
static int Z3_fpa_get_numeral_sign ( Z3_context  a0,
Z3_ast  a1,
[In, Out] ref int  a2 
)
static
static IntPtr Z3_fpa_get_numeral_significand_string ( Z3_context  a0,
Z3_ast  a1 
)
static
static int Z3_fpa_get_numeral_significand_uint64 ( Z3_context  a0,
Z3_ast  a1,
[In, Out] ref UInt64  a2 
)
static
static uint Z3_fpa_get_sbits ( Z3_context  a0,
Z3_sort  a1 
)
static

Referenced by Native.Z3_fpa_get_sbits().

static Z3_ast Z3_func_decl_to_ast ( Z3_context  a0,
Z3_func_decl  a1 
)
static
static IntPtr Z3_func_decl_to_string ( Z3_context  a0,
Z3_func_decl  a1 
)
static
static void Z3_func_entry_dec_ref ( Z3_context  a0,
Z3_func_entry  a1 
)
static
static Z3_ast Z3_func_entry_get_arg ( Z3_context  a0,
Z3_func_entry  a1,
uint  a2 
)
static
static uint Z3_func_entry_get_num_args ( Z3_context  a0,
Z3_func_entry  a1 
)
static
static Z3_ast Z3_func_entry_get_value ( Z3_context  a0,
Z3_func_entry  a1 
)
static
static void Z3_func_entry_inc_ref ( Z3_context  a0,
Z3_func_entry  a1 
)
static
static void Z3_func_interp_dec_ref ( Z3_context  a0,
Z3_func_interp  a1 
)
static
static uint Z3_func_interp_get_arity ( Z3_context  a0,
Z3_func_interp  a1 
)
static
static Z3_ast Z3_func_interp_get_else ( Z3_context  a0,
Z3_func_interp  a1 
)
static
static Z3_func_entry Z3_func_interp_get_entry ( Z3_context  a0,
Z3_func_interp  a1,
uint  a2 
)
static
static uint Z3_func_interp_get_num_entries ( Z3_context  a0,
Z3_func_interp  a1 
)
static
static void Z3_func_interp_inc_ref ( Z3_context  a0,
Z3_func_interp  a1 
)
static
static Z3_ast Z3_get_algebraic_number_lower ( Z3_context  a0,
Z3_ast  a1,
uint  a2 
)
static
static Z3_ast Z3_get_algebraic_number_upper ( Z3_context  a0,
Z3_ast  a1,
uint  a2 
)
static
static Z3_ast Z3_get_app_arg ( Z3_context  a0,
Z3_app  a1,
uint  a2 
)
static

Referenced by Native.Z3_get_app_arg().

static Z3_func_decl Z3_get_app_decl ( Z3_context  a0,
Z3_app  a1 
)
static

Referenced by Native.Z3_get_app_decl().

static uint Z3_get_app_num_args ( Z3_context  a0,
Z3_app  a1 
)
static
static uint Z3_get_arity ( Z3_context  a0,
Z3_func_decl  a1 
)
static

Referenced by Native.Z3_get_arity().

static Z3_sort Z3_get_array_sort_domain ( Z3_context  a0,
Z3_sort  a1 
)
static
static Z3_sort Z3_get_array_sort_range ( Z3_context  a0,
Z3_sort  a1 
)
static
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
static Z3_func_decl Z3_get_as_array_func_decl ( Z3_context  a0,
Z3_ast  a1 
)
static
static uint Z3_get_ast_hash ( Z3_context  a0,
Z3_ast  a1 
)
static

Referenced by Native.Z3_get_ast_hash().

static uint Z3_get_ast_id ( Z3_context  a0,
Z3_ast  a1 
)
static

Referenced by Native.Z3_get_ast_id().

static uint Z3_get_ast_kind ( Z3_context  a0,
Z3_ast  a1 
)
static

Referenced by Native.Z3_get_ast_kind().

static uint Z3_get_bool_value ( Z3_context  a0,
Z3_ast  a1 
)
static
static uint Z3_get_bv_sort_size ( Z3_context  a0,
Z3_sort  a1 
)
static
static Z3_ast Z3_get_context_assignment ( Z3_context  a0)
static
static Z3_func_decl Z3_get_datatype_sort_constructor ( Z3_context  a0,
Z3_sort  a1,
uint  a2 
)
static
static Z3_func_decl Z3_get_datatype_sort_constructor_accessor ( Z3_context  a0,
Z3_sort  a1,
uint  a2,
uint  a3 
)
static
static uint Z3_get_datatype_sort_num_constructors ( Z3_context  a0,
Z3_sort  a1 
)
static
static Z3_func_decl Z3_get_datatype_sort_recognizer ( Z3_context  a0,
Z3_sort  a1,
uint  a2 
)
static
static Z3_ast Z3_get_decl_ast_parameter ( Z3_context  a0,
Z3_func_decl  a1,
uint  a2 
)
static
static double Z3_get_decl_double_parameter ( Z3_context  a0,
Z3_func_decl  a1,
uint  a2 
)
static
static Z3_func_decl Z3_get_decl_func_decl_parameter ( Z3_context  a0,
Z3_func_decl  a1,
uint  a2 
)
static
static int Z3_get_decl_int_parameter ( Z3_context  a0,
Z3_func_decl  a1,
uint  a2 
)
static
static uint Z3_get_decl_kind ( Z3_context  a0,
Z3_func_decl  a1 
)
static

Referenced by Native.Z3_get_decl_kind().

static IntPtr Z3_get_decl_name ( Z3_context  a0,
Z3_func_decl  a1 
)
static

Referenced by Native.Z3_get_decl_name().

static uint Z3_get_decl_num_parameters ( Z3_context  a0,
Z3_func_decl  a1 
)
static
static uint Z3_get_decl_parameter_kind ( Z3_context  a0,
Z3_func_decl  a1,
uint  a2 
)
static
static IntPtr Z3_get_decl_rational_parameter ( Z3_context  a0,
Z3_func_decl  a1,
uint  a2 
)
static
static Z3_sort Z3_get_decl_sort_parameter ( Z3_context  a0,
Z3_func_decl  a1,
uint  a2 
)
static
static IntPtr Z3_get_decl_symbol_parameter ( Z3_context  a0,
Z3_func_decl  a1,
uint  a2 
)
static
static Z3_ast Z3_get_denominator ( Z3_context  a0,
Z3_ast  a1 
)
static
static Z3_sort Z3_get_domain ( Z3_context  a0,
Z3_func_decl  a1,
uint  a2 
)
static

Referenced by Native.Z3_get_domain().

static uint Z3_get_domain_size ( Z3_context  a0,
Z3_func_decl  a1 
)
static
static uint Z3_get_error_code ( Z3_context  a0)
static

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

static IntPtr Z3_get_error_msg ( uint  a0)
static

Referenced by Native.Z3_get_error_msg().

static IntPtr Z3_get_error_msg_ex ( Z3_context  a0,
uint  a1 
)
static

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

static int Z3_get_finite_domain_sort_size ( Z3_context  a0,
Z3_sort  a1,
[In, Out] ref UInt64  a2 
)
static
static uint Z3_get_func_decl_id ( Z3_context  a0,
Z3_func_decl  a1 
)
static
static Z3_literals Z3_get_guessed_literals ( Z3_context  a0)
static
static uint Z3_get_implied_equalities ( Z3_context  a0,
Z3_solver  a1,
uint  a2,
[In] Z3_ast[]  a3,
[Out] uint[]  a4 
)
static
static uint Z3_get_index_value ( Z3_context  a0,
Z3_ast  a1 
)
static
static Z3_ast_vector Z3_get_interpolant ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2,
Z3_params  a3 
)
static
static IntPtr Z3_get_label_symbol ( Z3_context  a0,
Z3_literals  a1,
uint  a2 
)
static
static Z3_ast Z3_get_literal ( Z3_context  a0,
Z3_literals  a1,
uint  a2 
)
static

Referenced by Native.Z3_get_literal().

static Z3_func_decl Z3_get_model_constant ( Z3_context  a0,
Z3_model  a1,
uint  a2 
)
static
static Z3_func_decl Z3_get_model_func_decl ( Z3_context  a0,
Z3_model  a1,
uint  a2 
)
static
static Z3_ast Z3_get_model_func_else ( Z3_context  a0,
Z3_model  a1,
uint  a2 
)
static
static Z3_ast Z3_get_model_func_entry_arg ( Z3_context  a0,
Z3_model  a1,
uint  a2,
uint  a3,
uint  a4 
)
static
static uint Z3_get_model_func_entry_num_args ( Z3_context  a0,
Z3_model  a1,
uint  a2,
uint  a3 
)
static
static Z3_ast Z3_get_model_func_entry_value ( Z3_context  a0,
Z3_model  a1,
uint  a2,
uint  a3 
)
static
static uint Z3_get_model_func_num_entries ( Z3_context  a0,
Z3_model  a1,
uint  a2 
)
static
static uint Z3_get_model_num_constants ( Z3_context  a0,
Z3_model  a1 
)
static
static uint Z3_get_model_num_funcs ( Z3_context  a0,
Z3_model  a1 
)
static
static uint Z3_get_num_literals ( Z3_context  a0,
Z3_literals  a1 
)
static
static uint Z3_get_num_probes ( Z3_context  a0)
static
static uint Z3_get_num_scopes ( Z3_context  a0)
static
static uint Z3_get_num_tactics ( Z3_context  a0)
static
static IntPtr Z3_get_numeral_decimal_string ( Z3_context  a0,
Z3_ast  a1,
uint  a2 
)
static
static int Z3_get_numeral_int ( Z3_context  a0,
Z3_ast  a1,
[In, Out] ref int  a2 
)
static
static int Z3_get_numeral_int64 ( Z3_context  a0,
Z3_ast  a1,
[In, Out] ref Int64  a2 
)
static
static int Z3_get_numeral_rational_int64 ( Z3_context  a0,
Z3_ast  a1,
[In, Out] ref Int64  a2,
[In, Out] ref Int64  a3 
)
static
static int Z3_get_numeral_small ( Z3_context  a0,
Z3_ast  a1,
[In, Out] ref Int64  a2,
[In, Out] ref Int64  a3 
)
static
static IntPtr Z3_get_numeral_string ( Z3_context  a0,
Z3_ast  a1 
)
static
static int Z3_get_numeral_uint ( Z3_context  a0,
Z3_ast  a1,
[In, Out] ref uint  a2 
)
static
static int Z3_get_numeral_uint64 ( Z3_context  a0,
Z3_ast  a1,
[In, Out] ref UInt64  a2 
)
static
static Z3_ast Z3_get_numerator ( Z3_context  a0,
Z3_ast  a1 
)
static

Referenced by Native.Z3_get_numerator().

static Z3_ast Z3_get_pattern ( Z3_context  a0,
Z3_pattern  a1,
uint  a2 
)
static

Referenced by Native.Z3_get_pattern().

static uint Z3_get_pattern_num_terms ( Z3_context  a0,
Z3_pattern  a1 
)
static
static IntPtr Z3_get_probe_name ( Z3_context  a0,
uint  a1 
)
static
static Z3_ast Z3_get_quantifier_body ( Z3_context  a0,
Z3_ast  a1 
)
static
static IntPtr Z3_get_quantifier_bound_name ( Z3_context  a0,
Z3_ast  a1,
uint  a2 
)
static
static Z3_sort Z3_get_quantifier_bound_sort ( Z3_context  a0,
Z3_ast  a1,
uint  a2 
)
static
static Z3_ast Z3_get_quantifier_no_pattern_ast ( Z3_context  a0,
Z3_ast  a1,
uint  a2 
)
static
static uint Z3_get_quantifier_num_bound ( Z3_context  a0,
Z3_ast  a1 
)
static
static uint Z3_get_quantifier_num_no_patterns ( Z3_context  a0,
Z3_ast  a1 
)
static
static uint Z3_get_quantifier_num_patterns ( Z3_context  a0,
Z3_ast  a1 
)
static
static Z3_pattern Z3_get_quantifier_pattern_ast ( Z3_context  a0,
Z3_ast  a1,
uint  a2 
)
static
static uint Z3_get_quantifier_weight ( Z3_context  a0,
Z3_ast  a1 
)
static
static Z3_sort Z3_get_range ( Z3_context  a0,
Z3_func_decl  a1 
)
static

Referenced by Native.Z3_get_range().

static uint Z3_get_relation_arity ( Z3_context  a0,
Z3_sort  a1 
)
static
static Z3_sort Z3_get_relation_column ( Z3_context  a0,
Z3_sort  a1,
uint  a2 
)
static
static Z3_literals Z3_get_relevant_labels ( Z3_context  a0)
static
static Z3_literals Z3_get_relevant_literals ( Z3_context  a0)
static
static uint Z3_get_search_failure ( Z3_context  a0)
static
static Z3_ast Z3_get_smtlib_assumption ( Z3_context  a0,
uint  a1 
)
static
static Z3_func_decl Z3_get_smtlib_decl ( Z3_context  a0,
uint  a1 
)
static
static IntPtr Z3_get_smtlib_error ( Z3_context  a0)
static
static Z3_ast Z3_get_smtlib_formula ( Z3_context  a0,
uint  a1 
)
static
static uint Z3_get_smtlib_num_assumptions ( Z3_context  a0)
static
static uint Z3_get_smtlib_num_decls ( Z3_context  a0)
static
static uint Z3_get_smtlib_num_formulas ( Z3_context  a0)
static
static uint Z3_get_smtlib_num_sorts ( Z3_context  a0)
static
static Z3_sort Z3_get_smtlib_sort ( Z3_context  a0,
uint  a1 
)
static
static Z3_sort Z3_get_sort ( Z3_context  a0,
Z3_ast  a1 
)
static

Referenced by Native.Z3_get_sort().

static uint Z3_get_sort_id ( Z3_context  a0,
Z3_sort  a1 
)
static

Referenced by Native.Z3_get_sort_id().

static uint Z3_get_sort_kind ( Z3_context  a0,
Z3_sort  a1 
)
static

Referenced by Native.Z3_get_sort_kind().

static IntPtr Z3_get_sort_name ( Z3_context  a0,
Z3_sort  a1 
)
static

Referenced by Native.Z3_get_sort_name().

static int Z3_get_symbol_int ( Z3_context  a0,
IntPtr  a1 
)
static
static uint Z3_get_symbol_kind ( Z3_context  a0,
IntPtr  a1 
)
static
static IntPtr Z3_get_symbol_string ( Z3_context  a0,
IntPtr  a1 
)
static
static IntPtr Z3_get_tactic_name ( Z3_context  a0,
uint  a1 
)
static
static Z3_func_decl Z3_get_tuple_sort_field_decl ( Z3_context  a0,
Z3_sort  a1,
uint  a2 
)
static
static Z3_func_decl Z3_get_tuple_sort_mk_decl ( Z3_context  a0,
Z3_sort  a1 
)
static
static uint Z3_get_tuple_sort_num_fields ( Z3_context  a0,
Z3_sort  a1 
)
static
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

Referenced by Native.Z3_get_version().

static int Z3_global_param_get ( string  a0,
out IntPtr  a1 
)
static
static void Z3_global_param_reset_all ( )
static
static void Z3_global_param_set ( string  a0,
string  a1 
)
static
static void Z3_goal_assert ( Z3_context  a0,
Z3_goal  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_goal_assert().

static void Z3_goal_dec_ref ( Z3_context  a0,
Z3_goal  a1 
)
static

Referenced by Native.Z3_goal_dec_ref().

static uint Z3_goal_depth ( Z3_context  a0,
Z3_goal  a1 
)
static

Referenced by Native.Z3_goal_depth().

static Z3_ast Z3_goal_formula ( Z3_context  a0,
Z3_goal  a1,
uint  a2 
)
static

Referenced by Native.Z3_goal_formula().

static void Z3_goal_inc_ref ( Z3_context  a0,
Z3_goal  a1 
)
static

Referenced by Native.Z3_goal_inc_ref().

static int Z3_goal_inconsistent ( Z3_context  a0,
Z3_goal  a1 
)
static
static int Z3_goal_is_decided_sat ( Z3_context  a0,
Z3_goal  a1 
)
static
static int Z3_goal_is_decided_unsat ( Z3_context  a0,
Z3_goal  a1 
)
static
static uint Z3_goal_num_exprs ( Z3_context  a0,
Z3_goal  a1 
)
static
static uint Z3_goal_precision ( Z3_context  a0,
Z3_goal  a1 
)
static
static void Z3_goal_reset ( Z3_context  a0,
Z3_goal  a1 
)
static

Referenced by Native.Z3_goal_reset().

static uint Z3_goal_size ( Z3_context  a0,
Z3_goal  a1 
)
static

Referenced by Native.Z3_goal_size().

static IntPtr Z3_goal_to_string ( Z3_context  a0,
Z3_goal  a1 
)
static
static Z3_goal Z3_goal_translate ( Z3_context  a0,
Z3_goal  a1,
Z3_context  a2 
)
static
static void Z3_inc_ref ( Z3_context  a0,
Z3_ast  a1 
)
static

Referenced by Native.Z3_inc_ref().

static IntPtr Z3_interpolation_profile ( Z3_context  a0)
static
static void Z3_interrupt ( Z3_context  a0)
static

Referenced by Native.Z3_interrupt().

static int Z3_is_algebraic_number ( Z3_context  a0,
Z3_ast  a1 
)
static
static int Z3_is_app ( Z3_context  a0,
Z3_ast  a1 
)
static

Referenced by Native.Z3_is_app().

static int Z3_is_array_value ( Z3_context  a0,
Z3_model  a1,
Z3_ast  a2,
[In, Out] ref uint  a3 
)
static
static int Z3_is_as_array ( Z3_context  a0,
Z3_ast  a1 
)
static

Referenced by Native.Z3_is_as_array().

static int Z3_is_eq_ast ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_is_eq_ast().

static int Z3_is_eq_func_decl ( Z3_context  a0,
Z3_func_decl  a1,
Z3_func_decl  a2 
)
static
static int Z3_is_eq_sort ( Z3_context  a0,
Z3_sort  a1,
Z3_sort  a2 
)
static

Referenced by Native.Z3_is_eq_sort().

static int Z3_is_numeral_ast ( Z3_context  a0,
Z3_ast  a1 
)
static
static int Z3_is_quantifier_forall ( Z3_context  a0,
Z3_ast  a1 
)
static
static int Z3_is_well_sorted ( Z3_context  a0,
Z3_ast  a1 
)
static
static Z3_ast Z3_mk_add ( Z3_context  a0,
uint  a1,
[In] Z3_ast[]  a2 
)
static

Referenced by Native.Z3_mk_add().

static Z3_ast Z3_mk_and ( Z3_context  a0,
uint  a1,
[In] Z3_ast[]  a2 
)
static

Referenced by Native.Z3_mk_and().

static Z3_ast Z3_mk_app ( Z3_context  a0,
Z3_func_decl  a1,
uint  a2,
[In] Z3_ast[]  a3 
)
static

Referenced by Native.Z3_mk_app().

static Z3_ast Z3_mk_array_default ( Z3_context  a0,
Z3_ast  a1 
)
static
static Z3_sort Z3_mk_array_sort ( Z3_context  a0,
Z3_sort  a1,
Z3_sort  a2 
)
static

Referenced by Native.Z3_mk_array_sort().

static Z3_ast_map Z3_mk_ast_map ( Z3_context  a0)
static

Referenced by Native.Z3_mk_ast_map().

static Z3_ast_vector Z3_mk_ast_vector ( Z3_context  a0)
static

Referenced by Native.Z3_mk_ast_vector().

static Z3_ast Z3_mk_atmost ( Z3_context  a0,
uint  a1,
[In] Z3_ast[]  a2,
uint  a3 
)
static

Referenced by Native.Z3_mk_atmost().

static Z3_sort Z3_mk_bool_sort ( Z3_context  a0)
static

Referenced by Native.Z3_mk_bool_sort().

static Z3_ast Z3_mk_bound ( Z3_context  a0,
uint  a1,
Z3_sort  a2 
)
static

Referenced by Native.Z3_mk_bound().

static Z3_ast Z3_mk_bv2int ( Z3_context  a0,
Z3_ast  a1,
int  a2 
)
static

Referenced by Native.Z3_mk_bv2int().

static Z3_sort Z3_mk_bv_sort ( Z3_context  a0,
uint  a1 
)
static

Referenced by Native.Z3_mk_bv_sort().

static Z3_ast Z3_mk_bvadd ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_bvadd().

static Z3_ast Z3_mk_bvadd_no_overflow ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2,
int  a3 
)
static
static Z3_ast Z3_mk_bvadd_no_underflow ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static
static Z3_ast Z3_mk_bvand ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_bvand().

static Z3_ast Z3_mk_bvashr ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_bvashr().

static Z3_ast Z3_mk_bvlshr ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_bvlshr().

static Z3_ast Z3_mk_bvmul ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_bvmul().

static Z3_ast Z3_mk_bvmul_no_overflow ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2,
int  a3 
)
static
static Z3_ast Z3_mk_bvmul_no_underflow ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static
static Z3_ast Z3_mk_bvnand ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_bvnand().

static Z3_ast Z3_mk_bvneg ( Z3_context  a0,
Z3_ast  a1 
)
static

Referenced by Native.Z3_mk_bvneg().

static Z3_ast Z3_mk_bvneg_no_overflow ( Z3_context  a0,
Z3_ast  a1 
)
static
static Z3_ast Z3_mk_bvnor ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_bvnor().

static Z3_ast Z3_mk_bvnot ( Z3_context  a0,
Z3_ast  a1 
)
static

Referenced by Native.Z3_mk_bvnot().

static Z3_ast Z3_mk_bvor ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_bvor().

static Z3_ast Z3_mk_bvredand ( Z3_context  a0,
Z3_ast  a1 
)
static

Referenced by Native.Z3_mk_bvredand().

static Z3_ast Z3_mk_bvredor ( Z3_context  a0,
Z3_ast  a1 
)
static

Referenced by Native.Z3_mk_bvredor().

static Z3_ast Z3_mk_bvsdiv ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_bvsdiv().

static Z3_ast Z3_mk_bvsdiv_no_overflow ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static
static Z3_ast Z3_mk_bvsge ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_bvsge().

static Z3_ast Z3_mk_bvsgt ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_bvsgt().

static Z3_ast Z3_mk_bvshl ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_bvshl().

static Z3_ast Z3_mk_bvsle ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_bvsle().

static Z3_ast Z3_mk_bvslt ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_bvslt().

static Z3_ast Z3_mk_bvsmod ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_bvsmod().

static Z3_ast Z3_mk_bvsrem ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_bvsrem().

static Z3_ast Z3_mk_bvsub ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_bvsub().

static Z3_ast Z3_mk_bvsub_no_overflow ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static
static Z3_ast Z3_mk_bvsub_no_underflow ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2,
int  a3 
)
static
static Z3_ast Z3_mk_bvudiv ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_bvudiv().

static Z3_ast Z3_mk_bvuge ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_bvuge().

static Z3_ast Z3_mk_bvugt ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_bvugt().

static Z3_ast Z3_mk_bvule ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_bvule().

static Z3_ast Z3_mk_bvult ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_bvult().

static Z3_ast Z3_mk_bvurem ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_bvurem().

static Z3_ast Z3_mk_bvxnor ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_bvxnor().

static Z3_ast Z3_mk_bvxor ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_bvxor().

static Z3_ast Z3_mk_concat ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_concat().

static Z3_config Z3_mk_config ( )
static

Referenced by Native.Z3_mk_config().

static Z3_ast Z3_mk_const ( Z3_context  a0,
IntPtr  a1,
Z3_sort  a2 
)
static

Referenced by Native.Z3_mk_const().

static Z3_ast Z3_mk_const_array ( Z3_context  a0,
Z3_sort  a1,
Z3_ast  a2 
)
static
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
static Z3_constructor_list Z3_mk_constructor_list ( Z3_context  a0,
uint  a1,
[In] Z3_constructor[]  a2 
)
static
static Z3_context Z3_mk_context ( Z3_config  a0)
static

Referenced by Native.Z3_mk_context().

static Z3_context Z3_mk_context_rc ( Z3_config  a0)
static

Referenced by Native.Z3_mk_context_rc().

static Z3_sort Z3_mk_datatype ( Z3_context  a0,
IntPtr  a1,
uint  a2,
[In, Out] Z3_constructor[]  a3 
)
static

Referenced by Native.Z3_mk_datatype().

static void Z3_mk_datatypes ( Z3_context  a0,
uint  a1,
[In] IntPtr[]  a2,
[Out] Z3_sort[]  a3,
[In, Out] Z3_constructor_list[]  a4 
)
static

Referenced by Native.Z3_mk_datatypes().

static Z3_ast Z3_mk_distinct ( Z3_context  a0,
uint  a1,
[In] Z3_ast[]  a2 
)
static

Referenced by Native.Z3_mk_distinct().

static Z3_ast Z3_mk_div ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_div().

static Z3_ast Z3_mk_empty_set ( Z3_context  a0,
Z3_sort  a1 
)
static

Referenced by Native.Z3_mk_empty_set().

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
static Z3_ast Z3_mk_eq ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_eq().

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

Referenced by Native.Z3_mk_exists().

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
static Z3_ast Z3_mk_ext_rotate_left ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static
static Z3_ast Z3_mk_ext_rotate_right ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static
static Z3_ast Z3_mk_extract ( Z3_context  a0,
uint  a1,
uint  a2,
Z3_ast  a3 
)
static

Referenced by Native.Z3_mk_extract().

static Z3_ast Z3_mk_false ( Z3_context  a0)
static

Referenced by Native.Z3_mk_false().

static Z3_sort Z3_mk_finite_domain_sort ( Z3_context  a0,
IntPtr  a1,
UInt64  a2 
)
static
static Z3_fixedpoint Z3_mk_fixedpoint ( Z3_context  a0)
static

Referenced by Native.Z3_mk_fixedpoint().

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

Referenced by Native.Z3_mk_forall().

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
static Z3_ast Z3_mk_fpa_abs ( Z3_context  a0,
Z3_ast  a1 
)
static

Referenced by Native.Z3_mk_fpa_abs().

static Z3_ast Z3_mk_fpa_add ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2,
Z3_ast  a3 
)
static

Referenced by Native.Z3_mk_fpa_add().

static Z3_ast Z3_mk_fpa_div ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2,
Z3_ast  a3 
)
static

Referenced by Native.Z3_mk_fpa_div().

static Z3_ast Z3_mk_fpa_eq ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_fpa_eq().

static Z3_ast Z3_mk_fpa_fma ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2,
Z3_ast  a3,
Z3_ast  a4 
)
static

Referenced by Native.Z3_mk_fpa_fma().

static Z3_ast Z3_mk_fpa_fp ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2,
Z3_ast  a3 
)
static

Referenced by Native.Z3_mk_fpa_fp().

static Z3_ast Z3_mk_fpa_geq ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_fpa_geq().

static Z3_ast Z3_mk_fpa_gt ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_fpa_gt().

static Z3_ast Z3_mk_fpa_inf ( Z3_context  a0,
Z3_sort  a1,
int  a2 
)
static

Referenced by Native.Z3_mk_fpa_inf().

static Z3_ast Z3_mk_fpa_is_infinite ( Z3_context  a0,
Z3_ast  a1 
)
static
static Z3_ast Z3_mk_fpa_is_nan ( Z3_context  a0,
Z3_ast  a1 
)
static

Referenced by Native.Z3_mk_fpa_is_nan().

static Z3_ast Z3_mk_fpa_is_negative ( Z3_context  a0,
Z3_ast  a1 
)
static
static Z3_ast Z3_mk_fpa_is_normal ( Z3_context  a0,
Z3_ast  a1 
)
static
static Z3_ast Z3_mk_fpa_is_positive ( Z3_context  a0,
Z3_ast  a1 
)
static
static Z3_ast Z3_mk_fpa_is_subnormal ( Z3_context  a0,
Z3_ast  a1 
)
static
static Z3_ast Z3_mk_fpa_is_zero ( Z3_context  a0,
Z3_ast  a1 
)
static
static Z3_ast Z3_mk_fpa_leq ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_fpa_leq().

static Z3_ast Z3_mk_fpa_lt ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_fpa_lt().

static Z3_ast Z3_mk_fpa_max ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_fpa_max().

static Z3_ast Z3_mk_fpa_min ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_fpa_min().

static Z3_ast Z3_mk_fpa_mul ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2,
Z3_ast  a3 
)
static

Referenced by Native.Z3_mk_fpa_mul().

static Z3_ast Z3_mk_fpa_nan ( Z3_context  a0,
Z3_sort  a1 
)
static

Referenced by Native.Z3_mk_fpa_nan().

static Z3_ast Z3_mk_fpa_neg ( Z3_context  a0,
Z3_ast  a1 
)
static

Referenced by Native.Z3_mk_fpa_neg().

static Z3_ast Z3_mk_fpa_numeral_double ( Z3_context  a0,
double  a1,
Z3_sort  a2 
)
static
static Z3_ast Z3_mk_fpa_numeral_float ( Z3_context  a0,
float  a1,
Z3_sort  a2 
)
static
static Z3_ast Z3_mk_fpa_numeral_int ( Z3_context  a0,
int  a1,
Z3_sort  a2 
)
static
static Z3_ast Z3_mk_fpa_numeral_int64_uint64 ( Z3_context  a0,
int  a1,
Int64  a2,
UInt64  a3,
Z3_sort  a4 
)
static
static Z3_ast Z3_mk_fpa_numeral_int_uint ( Z3_context  a0,
int  a1,
int  a2,
uint  a3,
Z3_sort  a4 
)
static
static Z3_ast Z3_mk_fpa_rem ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_fpa_rem().

static Z3_ast Z3_mk_fpa_rna ( Z3_context  a0)
static

Referenced by Native.Z3_mk_fpa_rna().

static Z3_ast Z3_mk_fpa_rne ( Z3_context  a0)
static

Referenced by Native.Z3_mk_fpa_rne().

static Z3_ast Z3_mk_fpa_round_nearest_ties_to_away ( Z3_context  a0)
static
static Z3_ast Z3_mk_fpa_round_nearest_ties_to_even ( Z3_context  a0)
static
static Z3_ast Z3_mk_fpa_round_to_integral ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static
static Z3_ast Z3_mk_fpa_round_toward_negative ( Z3_context  a0)
static
static Z3_ast Z3_mk_fpa_round_toward_positive ( Z3_context  a0)
static
static Z3_ast Z3_mk_fpa_round_toward_zero ( Z3_context  a0)
static
static Z3_sort Z3_mk_fpa_rounding_mode_sort ( Z3_context  a0)
static
static Z3_ast Z3_mk_fpa_rtn ( Z3_context  a0)
static

Referenced by Native.Z3_mk_fpa_rtn().

static Z3_ast Z3_mk_fpa_rtp ( Z3_context  a0)
static

Referenced by Native.Z3_mk_fpa_rtp().

static Z3_ast Z3_mk_fpa_rtz ( Z3_context  a0)
static

Referenced by Native.Z3_mk_fpa_rtz().

static Z3_sort Z3_mk_fpa_sort ( Z3_context  a0,
uint  a1,
uint  a2 
)
static

Referenced by Native.Z3_mk_fpa_sort().

static Z3_sort Z3_mk_fpa_sort_128 ( Z3_context  a0)
static
static Z3_sort Z3_mk_fpa_sort_16 ( Z3_context  a0)
static
static Z3_sort Z3_mk_fpa_sort_32 ( Z3_context  a0)
static
static Z3_sort Z3_mk_fpa_sort_64 ( Z3_context  a0)
static
static Z3_sort Z3_mk_fpa_sort_double ( Z3_context  a0)
static
static Z3_sort Z3_mk_fpa_sort_half ( Z3_context  a0)
static
static Z3_sort Z3_mk_fpa_sort_quadruple ( Z3_context  a0)
static
static Z3_sort Z3_mk_fpa_sort_single ( Z3_context  a0)
static
static Z3_ast Z3_mk_fpa_sqrt ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_fpa_sqrt().

static Z3_ast Z3_mk_fpa_sub ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2,
Z3_ast  a3 
)
static

Referenced by Native.Z3_mk_fpa_sub().

static Z3_ast Z3_mk_fpa_to_fp_bv ( Z3_context  a0,
Z3_ast  a1,
Z3_sort  a2 
)
static
static Z3_ast Z3_mk_fpa_to_fp_float ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2,
Z3_sort  a3 
)
static
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 
)
static
static Z3_ast Z3_mk_fpa_to_fp_real ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2,
Z3_sort  a3 
)
static
static Z3_ast Z3_mk_fpa_to_fp_signed ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2,
Z3_sort  a3 
)
static
static Z3_ast Z3_mk_fpa_to_fp_unsigned ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2,
Z3_sort  a3 
)
static
static Z3_ast Z3_mk_fpa_to_ieee_bv ( Z3_context  a0,
Z3_ast  a1 
)
static
static Z3_ast Z3_mk_fpa_to_real ( Z3_context  a0,
Z3_ast  a1 
)
static
static Z3_ast Z3_mk_fpa_to_sbv ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2,
uint  a3 
)
static

Referenced by Native.Z3_mk_fpa_to_sbv().

static Z3_ast Z3_mk_fpa_to_ubv ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2,
uint  a3 
)
static

Referenced by Native.Z3_mk_fpa_to_ubv().

static Z3_ast Z3_mk_fpa_zero ( Z3_context  a0,
Z3_sort  a1,
int  a2 
)
static

Referenced by Native.Z3_mk_fpa_zero().

static Z3_ast Z3_mk_fresh_const ( Z3_context  a0,
string  a1,
Z3_sort  a2 
)
static
static Z3_func_decl Z3_mk_fresh_func_decl ( Z3_context  a0,
string  a1,
uint  a2,
[In] Z3_sort[]  a3,
Z3_sort  a4 
)
static
static Z3_ast Z3_mk_full_set ( Z3_context  a0,
Z3_sort  a1 
)
static

Referenced by Native.Z3_mk_full_set().

static Z3_func_decl Z3_mk_func_decl ( Z3_context  a0,
IntPtr  a1,
uint  a2,
[In] Z3_sort[]  a3,
Z3_sort  a4 
)
static

Referenced by Native.Z3_mk_func_decl().

static Z3_ast Z3_mk_ge ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_ge().

static Z3_goal Z3_mk_goal ( Z3_context  a0,
int  a1,
int  a2,
int  a3 
)
static

Referenced by Native.Z3_mk_goal().

static Z3_ast Z3_mk_gt ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_gt().

static Z3_ast Z3_mk_iff ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_iff().

static Z3_ast Z3_mk_implies ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_implies().

static Z3_func_decl Z3_mk_injective_function ( Z3_context  a0,
IntPtr  a1,
uint  a2,
[In] Z3_sort[]  a3,
Z3_sort  a4 
)
static
static Z3_ast Z3_mk_int ( Z3_context  a0,
int  a1,
Z3_sort  a2 
)
static

Referenced by Native.Z3_mk_int().

static Z3_ast Z3_mk_int2bv ( Z3_context  a0,
uint  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_int2bv().

static Z3_ast Z3_mk_int2real ( Z3_context  a0,
Z3_ast  a1 
)
static

Referenced by Native.Z3_mk_int2real().

static Z3_ast Z3_mk_int64 ( Z3_context  a0,
Int64  a1,
Z3_sort  a2 
)
static

Referenced by Native.Z3_mk_int64().

static Z3_sort Z3_mk_int_sort ( Z3_context  a0)
static

Referenced by Native.Z3_mk_int_sort().

static IntPtr Z3_mk_int_symbol ( Z3_context  a0,
int  a1 
)
static

Referenced by Native.Z3_mk_int_symbol().

static Z3_ast Z3_mk_interpolant ( Z3_context  a0,
Z3_ast  a1 
)
static
static Z3_context Z3_mk_interpolation_context ( Z3_config  a0)
static
static Z3_ast Z3_mk_is_int ( Z3_context  a0,
Z3_ast  a1 
)
static

Referenced by Native.Z3_mk_is_int().

static Z3_ast Z3_mk_ite ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2,
Z3_ast  a3 
)
static

Referenced by Native.Z3_mk_ite().

static Z3_ast Z3_mk_label ( Z3_context  a0,
IntPtr  a1,
int  a2,
Z3_ast  a3 
)
static

Referenced by Native.Z3_mk_label().

static Z3_ast Z3_mk_le ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_le().

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

Referenced by Native.Z3_mk_list_sort().

static Z3_ast Z3_mk_lt ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_lt().

static Z3_ast Z3_mk_map ( Z3_context  a0,
Z3_func_decl  a1,
uint  a2,
[In] Z3_ast[]  a3 
)
static

Referenced by Native.Z3_mk_map().

static Z3_ast Z3_mk_mod ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_mod().

static Z3_ast Z3_mk_mul ( Z3_context  a0,
uint  a1,
[In] Z3_ast[]  a2 
)
static

Referenced by Native.Z3_mk_mul().

static Z3_ast Z3_mk_not ( Z3_context  a0,
Z3_ast  a1 
)
static

Referenced by Native.Z3_mk_not().

static Z3_ast Z3_mk_numeral ( Z3_context  a0,
string  a1,
Z3_sort  a2 
)
static

Referenced by Native.Z3_mk_numeral().

static Z3_optimize Z3_mk_optimize ( Z3_context  a0)
static

Referenced by Native.Z3_mk_optimize().

static Z3_ast Z3_mk_or ( Z3_context  a0,
uint  a1,
[In] Z3_ast[]  a2 
)
static

Referenced by Native.Z3_mk_or().

static Z3_params Z3_mk_params ( Z3_context  a0)
static

Referenced by Native.Z3_mk_params().

static Z3_pattern Z3_mk_pattern ( Z3_context  a0,
uint  a1,
[In] Z3_ast[]  a2 
)
static

Referenced by Native.Z3_mk_pattern().

static Z3_ast Z3_mk_pble ( Z3_context  a0,
uint  a1,
[In] Z3_ast[]  a2,
[In] int[]  a3,
int  a4 
)
static

Referenced by Native.Z3_mk_pble().

static Z3_ast Z3_mk_power ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_power().

static Z3_probe Z3_mk_probe ( Z3_context  a0,
string  a1 
)
static

Referenced by Native.Z3_mk_probe().

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

Referenced by Native.Z3_mk_quantifier().

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
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
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
static Z3_ast Z3_mk_real ( Z3_context  a0,
int  a1,
int  a2 
)
static

Referenced by Native.Z3_mk_real().

static Z3_ast Z3_mk_real2int ( Z3_context  a0,
Z3_ast  a1 
)
static

Referenced by Native.Z3_mk_real2int().

static Z3_sort Z3_mk_real_sort ( Z3_context  a0)
static

Referenced by Native.Z3_mk_real_sort().

static Z3_ast Z3_mk_rem ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_rem().

static Z3_ast Z3_mk_repeat ( Z3_context  a0,
uint  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_repeat().

static Z3_ast Z3_mk_rotate_left ( Z3_context  a0,
uint  a1,
Z3_ast  a2 
)
static
static Z3_ast Z3_mk_rotate_right ( Z3_context  a0,
uint  a1,
Z3_ast  a2 
)
static
static Z3_ast Z3_mk_select ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_select().

static Z3_ast Z3_mk_set_add ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_set_add().

static Z3_ast Z3_mk_set_complement ( Z3_context  a0,
Z3_ast  a1 
)
static
static Z3_ast Z3_mk_set_del ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_set_del().

static Z3_ast Z3_mk_set_difference ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static
static Z3_ast Z3_mk_set_intersect ( Z3_context  a0,
uint  a1,
[In] Z3_ast[]  a2 
)
static
static Z3_ast Z3_mk_set_member ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_set_member().

static Z3_sort Z3_mk_set_sort ( Z3_context  a0,
Z3_sort  a1 
)
static

Referenced by Native.Z3_mk_set_sort().

static Z3_ast Z3_mk_set_subset ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_set_subset().

static Z3_ast Z3_mk_set_union ( Z3_context  a0,
uint  a1,
[In] Z3_ast[]  a2 
)
static

Referenced by Native.Z3_mk_set_union().

static Z3_ast Z3_mk_sign_ext ( Z3_context  a0,
uint  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_sign_ext().

static Z3_solver Z3_mk_simple_solver ( Z3_context  a0)
static
static Z3_solver Z3_mk_solver ( Z3_context  a0)
static

Referenced by Native.Z3_mk_solver().

static Z3_solver Z3_mk_solver_for_logic ( Z3_context  a0,
IntPtr  a1 
)
static
static Z3_solver Z3_mk_solver_from_tactic ( Z3_context  a0,
Z3_tactic  a1 
)
static
static Z3_ast Z3_mk_store ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2,
Z3_ast  a3 
)
static

Referenced by Native.Z3_mk_store().

static IntPtr Z3_mk_string_symbol ( Z3_context  a0,
string  a1 
)
static
static Z3_ast Z3_mk_sub ( Z3_context  a0,
uint  a1,
[In] Z3_ast[]  a2 
)
static

Referenced by Native.Z3_mk_sub().

static Z3_tactic Z3_mk_tactic ( Z3_context  a0,
string  a1 
)
static

Referenced by Native.Z3_mk_tactic().

static Z3_ast Z3_mk_true ( Z3_context  a0)
static

Referenced by Native.Z3_mk_true().

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

Referenced by Native.Z3_mk_tuple_sort().

static Z3_ast Z3_mk_unary_minus ( Z3_context  a0,
Z3_ast  a1 
)
static
static Z3_sort Z3_mk_uninterpreted_sort ( Z3_context  a0,
IntPtr  a1 
)
static
static Z3_ast Z3_mk_unsigned_int ( Z3_context  a0,
uint  a1,
Z3_sort  a2 
)
static
static Z3_ast Z3_mk_unsigned_int64 ( Z3_context  a0,
UInt64  a1,
Z3_sort  a2 
)
static
static Z3_ast Z3_mk_xor ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_xor().

static Z3_ast Z3_mk_zero_ext ( Z3_context  a0,
uint  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_mk_zero_ext().

static void Z3_model_dec_ref ( Z3_context  a0,
Z3_model  a1 
)
static

Referenced by Native.Z3_model_dec_ref().

static int Z3_model_eval ( Z3_context  a0,
Z3_model  a1,
Z3_ast  a2,
int  a3,
[In, Out] ref Z3_ast  a4 
)
static

Referenced by Native.Z3_model_eval().

static Z3_func_decl Z3_model_get_const_decl ( Z3_context  a0,
Z3_model  a1,
uint  a2 
)
static
static Z3_ast Z3_model_get_const_interp ( Z3_context  a0,
Z3_model  a1,
Z3_func_decl  a2 
)
static
static Z3_func_decl Z3_model_get_func_decl ( Z3_context  a0,
Z3_model  a1,
uint  a2 
)
static
static Z3_func_interp Z3_model_get_func_interp ( Z3_context  a0,
Z3_model  a1,
Z3_func_decl  a2 
)
static
static uint Z3_model_get_num_consts ( Z3_context  a0,
Z3_model  a1 
)
static
static uint Z3_model_get_num_funcs ( Z3_context  a0,
Z3_model  a1 
)
static
static uint Z3_model_get_num_sorts ( Z3_context  a0,
Z3_model  a1 
)
static
static Z3_sort Z3_model_get_sort ( Z3_context  a0,
Z3_model  a1,
uint  a2 
)
static
static Z3_ast_vector Z3_model_get_sort_universe ( Z3_context  a0,
Z3_model  a1,
Z3_sort  a2 
)
static
static int Z3_model_has_interp ( Z3_context  a0,
Z3_model  a1,
Z3_func_decl  a2 
)
static
static void Z3_model_inc_ref ( Z3_context  a0,
Z3_model  a1 
)
static

Referenced by Native.Z3_model_inc_ref().

static IntPtr Z3_model_to_string ( Z3_context  a0,
Z3_model  a1 
)
static
static int Z3_open_log ( string  a0)
static

Referenced by Native.Z3_open_log().

static void Z3_optimize_assert ( Z3_context  a0,
Z3_optimize  a1,
Z3_ast  a2 
)
static
static uint Z3_optimize_assert_soft ( Z3_context  a0,
Z3_optimize  a1,
Z3_ast  a2,
string  a3,
IntPtr  a4 
)
static
static int Z3_optimize_check ( Z3_context  a0,
Z3_optimize  a1 
)
static
static void Z3_optimize_dec_ref ( Z3_context  a0,
Z3_optimize  a1 
)
static
static IntPtr Z3_optimize_get_help ( Z3_context  a0,
Z3_optimize  a1 
)
static
static Z3_ast Z3_optimize_get_lower ( Z3_context  a0,
Z3_optimize  a1,
uint  a2 
)
static
static Z3_model Z3_optimize_get_model ( Z3_context  a0,
Z3_optimize  a1 
)
static
static Z3_param_descrs Z3_optimize_get_param_descrs ( Z3_context  a0,
Z3_optimize  a1 
)
static
static IntPtr Z3_optimize_get_reason_unknown ( Z3_context  a0,
Z3_optimize  a1 
)
static
static Z3_stats Z3_optimize_get_statistics ( Z3_context  a0,
Z3_optimize  a1 
)
static
static Z3_ast Z3_optimize_get_upper ( Z3_context  a0,
Z3_optimize  a1,
uint  a2 
)
static
static void Z3_optimize_inc_ref ( Z3_context  a0,
Z3_optimize  a1 
)
static
static uint Z3_optimize_maximize ( Z3_context  a0,
Z3_optimize  a1,
Z3_ast  a2 
)
static
static uint Z3_optimize_minimize ( Z3_context  a0,
Z3_optimize  a1,
Z3_ast  a2 
)
static
static void Z3_optimize_pop ( Z3_context  a0,
Z3_optimize  a1 
)
static

Referenced by Native.Z3_optimize_pop().

static void Z3_optimize_push ( Z3_context  a0,
Z3_optimize  a1 
)
static

Referenced by Native.Z3_optimize_push().

static void Z3_optimize_set_params ( Z3_context  a0,
Z3_optimize  a1,
Z3_params  a2 
)
static
static IntPtr Z3_optimize_to_string ( Z3_context  a0,
Z3_optimize  a1 
)
static
static void Z3_param_descrs_dec_ref ( Z3_context  a0,
Z3_param_descrs  a1 
)
static
static uint Z3_param_descrs_get_kind ( Z3_context  a0,
Z3_param_descrs  a1,
IntPtr  a2 
)
static
static IntPtr Z3_param_descrs_get_name ( Z3_context  a0,
Z3_param_descrs  a1,
uint  a2 
)
static
static void Z3_param_descrs_inc_ref ( Z3_context  a0,
Z3_param_descrs  a1 
)
static
static uint Z3_param_descrs_size ( Z3_context  a0,
Z3_param_descrs  a1 
)
static
static IntPtr Z3_param_descrs_to_string ( Z3_context  a0,
Z3_param_descrs  a1 
)
static
static void Z3_params_dec_ref ( Z3_context  a0,
Z3_params  a1 
)
static
static void Z3_params_inc_ref ( Z3_context  a0,
Z3_params  a1 
)
static
static void Z3_params_set_bool ( Z3_context  a0,
Z3_params  a1,
IntPtr  a2,
int  a3 
)
static
static void Z3_params_set_double ( Z3_context  a0,
Z3_params  a1,
IntPtr  a2,
double  a3 
)
static
static void Z3_params_set_symbol ( Z3_context  a0,
Z3_params  a1,
IntPtr  a2,
IntPtr  a3 
)
static
static void Z3_params_set_uint ( Z3_context  a0,
Z3_params  a1,
IntPtr  a2,
uint  a3 
)
static
static IntPtr Z3_params_to_string ( Z3_context  a0,
Z3_params  a1 
)
static
static void Z3_params_validate ( Z3_context  a0,
Z3_params  a1,
Z3_param_descrs  a2 
)
static
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
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
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
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
static Z3_ast Z3_pattern_to_ast ( Z3_context  a0,
Z3_pattern  a1 
)
static
static IntPtr Z3_pattern_to_string ( Z3_context  a0,
Z3_pattern  a1 
)
static
static void Z3_persist_ast ( Z3_context  a0,
Z3_ast  a1,
uint  a2 
)
static

Referenced by Native.Z3_persist_ast().

static Z3_ast_vector Z3_polynomial_subresultants ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2,
Z3_ast  a3 
)
static
static void Z3_pop ( Z3_context  a0,
uint  a1 
)
static

Referenced by Native.Z3_pop().

static Z3_probe Z3_probe_and ( Z3_context  a0,
Z3_probe  a1,
Z3_probe  a2 
)
static

Referenced by Native.Z3_probe_and().

static double Z3_probe_apply ( Z3_context  a0,
Z3_probe  a1,
Z3_goal  a2 
)
static

Referenced by Native.Z3_probe_apply().

static Z3_probe Z3_probe_const ( Z3_context  a0,
double  a1 
)
static

Referenced by Native.Z3_probe_const().

static void Z3_probe_dec_ref ( Z3_context  a0,
Z3_probe  a1 
)
static

Referenced by Native.Z3_probe_dec_ref().

static Z3_probe Z3_probe_eq ( Z3_context  a0,
Z3_probe  a1,
Z3_probe  a2 
)
static

Referenced by Native.Z3_probe_eq().

static Z3_probe Z3_probe_ge ( Z3_context  a0,
Z3_probe  a1,
Z3_probe  a2 
)
static

Referenced by Native.Z3_probe_ge().

static IntPtr Z3_probe_get_descr ( Z3_context  a0,
string  a1 
)
static
static Z3_probe Z3_probe_gt ( Z3_context  a0,
Z3_probe  a1,
Z3_probe  a2 
)
static

Referenced by Native.Z3_probe_gt().

static void Z3_probe_inc_ref ( Z3_context  a0,
Z3_probe  a1 
)
static

Referenced by Native.Z3_probe_inc_ref().

static Z3_probe Z3_probe_le ( Z3_context  a0,
Z3_probe  a1,
Z3_probe  a2 
)
static

Referenced by Native.Z3_probe_le().

static Z3_probe Z3_probe_lt ( Z3_context  a0,
Z3_probe  a1,
Z3_probe  a2 
)
static

Referenced by Native.Z3_probe_lt().

static Z3_probe Z3_probe_not ( Z3_context  a0,
Z3_probe  a1 
)
static

Referenced by Native.Z3_probe_not().

static Z3_probe Z3_probe_or ( Z3_context  a0,
Z3_probe  a1,
Z3_probe  a2 
)
static

Referenced by Native.Z3_probe_or().

static void Z3_push ( Z3_context  a0)
static

Referenced by Native.Z3_push().

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
static Z3_rcf_num Z3_rcf_add ( Z3_context  a0,
Z3_rcf_num  a1,
Z3_rcf_num  a2 
)
static

Referenced by Native.Z3_rcf_add().

static void Z3_rcf_del ( Z3_context  a0,
Z3_rcf_num  a1 
)
static

Referenced by Native.Z3_rcf_del().

static Z3_rcf_num Z3_rcf_div ( Z3_context  a0,
Z3_rcf_num  a1,
Z3_rcf_num  a2 
)
static

Referenced by Native.Z3_rcf_div().

static int Z3_rcf_eq ( Z3_context  a0,
Z3_rcf_num  a1,
Z3_rcf_num  a2 
)
static

Referenced by Native.Z3_rcf_eq().

static int Z3_rcf_ge ( Z3_context  a0,
Z3_rcf_num  a1,
Z3_rcf_num  a2 
)
static

Referenced by Native.Z3_rcf_ge().

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
static int Z3_rcf_gt ( Z3_context  a0,
Z3_rcf_num  a1,
Z3_rcf_num  a2 
)
static

Referenced by Native.Z3_rcf_gt().

static Z3_rcf_num Z3_rcf_inv ( Z3_context  a0,
Z3_rcf_num  a1 
)
static

Referenced by Native.Z3_rcf_inv().

static int Z3_rcf_le ( Z3_context  a0,
Z3_rcf_num  a1,
Z3_rcf_num  a2 
)
static

Referenced by Native.Z3_rcf_le().

static int Z3_rcf_lt ( Z3_context  a0,
Z3_rcf_num  a1,
Z3_rcf_num  a2 
)
static

Referenced by Native.Z3_rcf_lt().

static Z3_rcf_num Z3_rcf_mk_e ( Z3_context  a0)
static

Referenced by Native.Z3_rcf_mk_e().

static Z3_rcf_num Z3_rcf_mk_infinitesimal ( Z3_context  a0)
static
static Z3_rcf_num Z3_rcf_mk_pi ( Z3_context  a0)
static

Referenced by Native.Z3_rcf_mk_pi().

static Z3_rcf_num Z3_rcf_mk_rational ( Z3_context  a0,
string  a1 
)
static
static uint Z3_rcf_mk_roots ( Z3_context  a0,
uint  a1,
[In] Z3_rcf_num[]  a2,
[Out] Z3_rcf_num[]  a3 
)
static

Referenced by Native.Z3_rcf_mk_roots().

static Z3_rcf_num Z3_rcf_mk_small_int ( Z3_context  a0,
int  a1 
)
static
static Z3_rcf_num Z3_rcf_mul ( Z3_context  a0,
Z3_rcf_num  a1,
Z3_rcf_num  a2 
)
static

Referenced by Native.Z3_rcf_mul().

static Z3_rcf_num Z3_rcf_neg ( Z3_context  a0,
Z3_rcf_num  a1 
)
static

Referenced by Native.Z3_rcf_neg().

static int Z3_rcf_neq ( Z3_context  a0,
Z3_rcf_num  a1,
Z3_rcf_num  a2 
)
static

Referenced by Native.Z3_rcf_neq().

static IntPtr Z3_rcf_num_to_decimal_string ( Z3_context  a0,
Z3_rcf_num  a1,
uint  a2 
)
static
static IntPtr Z3_rcf_num_to_string ( Z3_context  a0,
Z3_rcf_num  a1,
int  a2,
int  a3 
)
static
static Z3_rcf_num Z3_rcf_power ( Z3_context  a0,
Z3_rcf_num  a1,
uint  a2 
)
static

Referenced by Native.Z3_rcf_power().

static Z3_rcf_num Z3_rcf_sub ( Z3_context  a0,
Z3_rcf_num  a1,
Z3_rcf_num  a2 
)
static

Referenced by Native.Z3_rcf_sub().

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
static void Z3_reset_memory ( )
static

Referenced by Native.Z3_reset_memory().

static void Z3_set_ast_print_mode ( Z3_context  a0,
uint  a1 
)
static
static void Z3_set_error ( Z3_context  a0,
uint  a1 
)
static

Referenced by Native.Z3_set_error().

static void Z3_set_error_handler ( Z3_context  a0,
Z3_error_handler  a1 
)
static
static void Z3_set_logic ( Z3_context  a0,
string  a1 
)
static

Referenced by Native.Z3_set_logic().

static void Z3_set_param_value ( Z3_config  a0,
string  a1,
string  a2 
)
static
static Z3_ast Z3_simplify ( Z3_context  a0,
Z3_ast  a1 
)
static

Referenced by Native.Z3_simplify().

static Z3_ast Z3_simplify_ex ( Z3_context  a0,
Z3_ast  a1,
Z3_params  a2 
)
static

Referenced by Native.Z3_simplify_ex().

static IntPtr Z3_simplify_get_help ( Z3_context  a0)
static
static Z3_param_descrs Z3_simplify_get_param_descrs ( Z3_context  a0)
static
static void Z3_soft_check_cancel ( Z3_context  a0)
static
static void Z3_solver_assert ( Z3_context  a0,
Z3_solver  a1,
Z3_ast  a2 
)
static

Referenced by Native.Z3_solver_assert().

static void Z3_solver_assert_and_track ( Z3_context  a0,
Z3_solver  a1,
Z3_ast  a2,
Z3_ast  a3 
)
static
static int Z3_solver_check ( Z3_context  a0,
Z3_solver  a1 
)
static

Referenced by Native.Z3_solver_check().

static int Z3_solver_check_assumptions ( Z3_context  a0,
Z3_solver  a1,
uint  a2,
[In] Z3_ast[]  a3 
)
static
static void Z3_solver_dec_ref ( Z3_context  a0,
Z3_solver  a1 
)
static
static Z3_ast_vector Z3_solver_get_assertions ( Z3_context  a0,
Z3_solver  a1 
)
static
static IntPtr Z3_solver_get_help ( Z3_context  a0,
Z3_solver  a1 
)
static
static Z3_model Z3_solver_get_model ( Z3_context  a0,
Z3_solver  a1 
)
static
static uint Z3_solver_get_num_scopes ( Z3_context  a0,
Z3_solver  a1 
)
static
static Z3_param_descrs Z3_solver_get_param_descrs ( Z3_context  a0,
Z3_solver  a1 
)
static
static Z3_ast Z3_solver_get_proof ( Z3_context  a0,
Z3_solver  a1 
)
static
static IntPtr Z3_solver_get_reason_unknown ( Z3_context  a0,
Z3_solver  a1 
)
static
static Z3_stats Z3_solver_get_statistics ( Z3_context  a0,
Z3_solver  a1 
)
static
static Z3_ast_vector Z3_solver_get_unsat_core ( Z3_context  a0,
Z3_solver  a1 
)
static
static void Z3_solver_inc_ref ( Z3_context  a0,
Z3_solver  a1 
)
static
static void Z3_solver_pop ( Z3_context  a0,
Z3_solver  a1,
uint  a2 
)
static

Referenced by Native.Z3_solver_pop().

static void Z3_solver_push ( Z3_context  a0,
Z3_solver  a1 
)
static

Referenced by Native.Z3_solver_push().

static void Z3_solver_reset ( Z3_context  a0,
Z3_solver  a1 
)
static

Referenced by Native.Z3_solver_reset().

static void Z3_solver_set_params ( Z3_context  a0,
Z3_solver  a1,
Z3_params  a2 
)
static
static IntPtr Z3_solver_to_string ( Z3_context  a0,
Z3_solver  a1 
)
static
static Z3_ast Z3_sort_to_ast ( Z3_context  a0,
Z3_sort  a1 
)
static

Referenced by Native.Z3_sort_to_ast().

static IntPtr Z3_sort_to_string ( Z3_context  a0,
Z3_sort  a1 
)
static
static IntPtr Z3_statistics_to_string ( Z3_context  a0)
static
static void Z3_stats_dec_ref ( Z3_context  a0,
Z3_stats  a1 
)
static

Referenced by Native.Z3_stats_dec_ref().

static double Z3_stats_get_double_value ( Z3_context  a0,
Z3_stats  a1,
uint  a2 
)
static
static IntPtr Z3_stats_get_key ( Z3_context  a0,
Z3_stats  a1,
uint  a2 
)
static

Referenced by Native.Z3_stats_get_key().

static uint Z3_stats_get_uint_value ( Z3_context  a0,
Z3_stats  a1,
uint  a2 
)
static
static void Z3_stats_inc_ref ( Z3_context  a0,
Z3_stats  a1 
)
static

Referenced by Native.Z3_stats_inc_ref().

static int Z3_stats_is_double ( Z3_context  a0,
Z3_stats  a1,
uint  a2 
)
static
static int Z3_stats_is_uint ( Z3_context  a0,
Z3_stats  a1,
uint  a2 
)
static

Referenced by Native.Z3_stats_is_uint().

static uint Z3_stats_size ( Z3_context  a0,
Z3_stats  a1 
)
static

Referenced by Native.Z3_stats_size().

static IntPtr Z3_stats_to_string ( Z3_context  a0,
Z3_stats  a1 
)
static
static Z3_ast Z3_substitute ( Z3_context  a0,
Z3_ast  a1,
uint  a2,
[In] Z3_ast[]  a3,
[In] Z3_ast[]  a4 
)
static

Referenced by Native.Z3_substitute().

static Z3_ast Z3_substitute_vars ( Z3_context  a0,
Z3_ast  a1,
uint  a2,
[In] Z3_ast[]  a3 
)
static
static Z3_tactic Z3_tactic_and_then ( Z3_context  a0,
Z3_tactic  a1,
Z3_tactic  a2 
)
static
static Z3_apply_result Z3_tactic_apply ( Z3_context  a0,
Z3_tactic  a1,
Z3_goal  a2 
)
static

Referenced by Native.Z3_tactic_apply().

static Z3_apply_result Z3_tactic_apply_ex ( Z3_context  a0,
Z3_tactic  a1,
Z3_goal  a2,
Z3_params  a3 
)
static
static Z3_tactic Z3_tactic_cond ( Z3_context  a0,
Z3_probe  a1,
Z3_tactic  a2,
Z3_tactic  a3 
)
static

Referenced by Native.Z3_tactic_cond().

static void Z3_tactic_dec_ref ( Z3_context  a0,
Z3_tactic  a1 
)
static
static Z3_tactic Z3_tactic_fail ( Z3_context  a0)
static

Referenced by Native.Z3_tactic_fail().

static Z3_tactic Z3_tactic_fail_if ( Z3_context  a0,
Z3_probe  a1 
)
static
static Z3_tactic Z3_tactic_fail_if_not_decided ( Z3_context  a0)
static
static IntPtr Z3_tactic_get_descr ( Z3_context  a0,
string  a1 
)
static
static IntPtr Z3_tactic_get_help ( Z3_context  a0,
Z3_tactic  a1 
)
static
static Z3_param_descrs Z3_tactic_get_param_descrs ( Z3_context  a0,
Z3_tactic  a1 
)
static
static void Z3_tactic_inc_ref ( Z3_context  a0,
Z3_tactic  a1 
)
static
static Z3_tactic Z3_tactic_or_else ( Z3_context  a0,
Z3_tactic  a1,
Z3_tactic  a2 
)
static
static Z3_tactic Z3_tactic_par_and_then ( Z3_context  a0,
Z3_tactic  a1,
Z3_tactic  a2 
)
static
static Z3_tactic Z3_tactic_par_or ( Z3_context  a0,
uint  a1,
[In] Z3_tactic[]  a2 
)
static

Referenced by Native.Z3_tactic_par_or().

static Z3_tactic Z3_tactic_repeat ( Z3_context  a0,
Z3_tactic  a1,
uint  a2 
)
static

Referenced by Native.Z3_tactic_repeat().

static Z3_tactic Z3_tactic_skip ( Z3_context  a0)
static

Referenced by Native.Z3_tactic_skip().

static Z3_tactic Z3_tactic_try_for ( Z3_context  a0,
Z3_tactic  a1,
uint  a2 
)
static
static Z3_tactic Z3_tactic_using_params ( Z3_context  a0,
Z3_tactic  a1,
Z3_params  a2 
)
static
static Z3_tactic Z3_tactic_when ( Z3_context  a0,
Z3_probe  a1,
Z3_tactic  a2 
)
static

Referenced by Native.Z3_tactic_when().

static Z3_app Z3_to_app ( Z3_context  a0,
Z3_ast  a1 
)
static

Referenced by Native.Z3_to_app().

static Z3_func_decl Z3_to_func_decl ( Z3_context  a0,
Z3_ast  a1 
)
static

Referenced by Native.Z3_to_func_decl().

static void Z3_toggle_warning_messages ( int  a0)
static
static Z3_ast Z3_translate ( Z3_context  a0,
Z3_ast  a1,
Z3_context  a2 
)
static

Referenced by Native.Z3_translate().

static void Z3_update_param_value ( Z3_context  a0,
string  a1,
string  a2 
)
static
static Z3_ast Z3_update_term ( Z3_context  a0,
Z3_ast  a1,
uint  a2,
[In] Z3_ast[]  a3 
)
static

Referenced by Native.Z3_update_term().

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