Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules Pages
Data Structures | Public Member Functions | Static Public Member Functions
Native Class Reference

Data Structures

class  LIB
 

Public Member Functions

delegate void Z3_error_handler (Z3_context c, Z3_error_code e)
 

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 string 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 string 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 string 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 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_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 string 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 string Z3_get_numeral_string (Z3_context a0, Z3_ast a1)
 
static string 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 string 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 string Z3_ast_to_string (Z3_context a0, Z3_ast a1)
 
static string Z3_pattern_to_string (Z3_context a0, Z3_pattern a1)
 
static string Z3_sort_to_string (Z3_context a0, Z3_sort a1)
 
static string Z3_func_decl_to_string (Z3_context a0, Z3_func_decl a1)
 
static string Z3_model_to_string (Z3_context a0, Z3_model a1)
 
static string 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 string 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 string Z3_get_error_msg (uint a0)
 
static string 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 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 string 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 string 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 string 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_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 string 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 string 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 string 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 string Z3_get_tactic_name (Z3_context a0, uint a1)
 
static uint Z3_get_num_probes (Z3_context a0)
 
static string Z3_get_probe_name (Z3_context a0, uint a1)
 
static string 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 string Z3_tactic_get_descr (Z3_context a0, string a1)
 
static string 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 string 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 string 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 string 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 string Z3_solver_to_string (Z3_context a0, Z3_solver a1)
 
static string 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 string 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 string Z3_context_to_string (Z3_context a0)
 
static string 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 string Z3_rcf_num_to_string (Z3_context a0, Z3_rcf_num a1, int a2, int a3)
 
static string 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 string 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)
 

Detailed Description

Definition at line 39 of file Native.cs.

Member Function Documentation

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

Definition at line 5466 of file Native.cs.

5466  {
5467  Z3_ast r = LIB.Z3_algebraic_add(a0, a1, a2);
5468  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5469  if (err != Z3_error_code.Z3_OK)
5470  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5471  return r;
5472  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast Z3_algebraic_div ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 5490 of file Native.cs.

5490  {
5491  Z3_ast r = LIB.Z3_algebraic_div(a0, a1, a2);
5492  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5493  if (err != Z3_error_code.Z3_OK)
5494  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5495  return r;
5496  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static int Z3_algebraic_eq ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 5546 of file Native.cs.

5546  {
5547  int r = LIB.Z3_algebraic_eq(a0, a1, a2);
5548  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5549  if (err != Z3_error_code.Z3_OK)
5550  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5551  return r;
5552  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static int Z3_algebraic_eval ( Z3_context  a0,
Z3_ast  a1,
uint  a2,
[In] Z3_ast[]  a3 
)
inlinestatic

Definition at line 5570 of file Native.cs.

5570  {
5571  int r = LIB.Z3_algebraic_eval(a0, a1, a2, a3);
5572  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5573  if (err != Z3_error_code.Z3_OK)
5574  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5575  return r;
5576  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static int Z3_algebraic_ge ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 5538 of file Native.cs.

5538  {
5539  int r = LIB.Z3_algebraic_ge(a0, a1, a2);
5540  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5541  if (err != Z3_error_code.Z3_OK)
5542  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5543  return r;
5544  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static int Z3_algebraic_gt ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 5522 of file Native.cs.

5522  {
5523  int r = LIB.Z3_algebraic_gt(a0, a1, a2);
5524  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5525  if (err != Z3_error_code.Z3_OK)
5526  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5527  return r;
5528  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static int Z3_algebraic_is_neg ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 5442 of file Native.cs.

5442  {
5443  int r = LIB.Z3_algebraic_is_neg(a0, a1);
5444  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5445  if (err != Z3_error_code.Z3_OK)
5446  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5447  return r;
5448  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static int Z3_algebraic_is_pos ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 5434 of file Native.cs.

5434  {
5435  int r = LIB.Z3_algebraic_is_pos(a0, a1);
5436  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5437  if (err != Z3_error_code.Z3_OK)
5438  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5439  return r;
5440  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static int Z3_algebraic_is_value ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 5426 of file Native.cs.

5426  {
5427  int r = LIB.Z3_algebraic_is_value(a0, a1);
5428  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5429  if (err != Z3_error_code.Z3_OK)
5430  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5431  return r;
5432  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static int Z3_algebraic_is_zero ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 5450 of file Native.cs.

5450  {
5451  int r = LIB.Z3_algebraic_is_zero(a0, a1);
5452  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5453  if (err != Z3_error_code.Z3_OK)
5454  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5455  return r;
5456  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static int Z3_algebraic_le ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 5530 of file Native.cs.

5530  {
5531  int r = LIB.Z3_algebraic_le(a0, a1, a2);
5532  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5533  if (err != Z3_error_code.Z3_OK)
5534  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5535  return r;
5536  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static int Z3_algebraic_lt ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 5514 of file Native.cs.

5514  {
5515  int r = LIB.Z3_algebraic_lt(a0, a1, a2);
5516  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5517  if (err != Z3_error_code.Z3_OK)
5518  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5519  return r;
5520  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast Z3_algebraic_mul ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 5482 of file Native.cs.

5482  {
5483  Z3_ast r = LIB.Z3_algebraic_mul(a0, a1, a2);
5484  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5485  if (err != Z3_error_code.Z3_OK)
5486  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5487  return r;
5488  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static int Z3_algebraic_neq ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 5554 of file Native.cs.

5554  {
5555  int r = LIB.Z3_algebraic_neq(a0, a1, a2);
5556  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5557  if (err != Z3_error_code.Z3_OK)
5558  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5559  return r;
5560  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast Z3_algebraic_power ( Z3_context  a0,
Z3_ast  a1,
uint  a2 
)
inlinestatic

Definition at line 5506 of file Native.cs.

5506  {
5507  Z3_ast r = LIB.Z3_algebraic_power(a0, a1, a2);
5508  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5509  if (err != Z3_error_code.Z3_OK)
5510  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5511  return r;
5512  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast Z3_algebraic_root ( Z3_context  a0,
Z3_ast  a1,
uint  a2 
)
inlinestatic

Definition at line 5498 of file Native.cs.

5498  {
5499  Z3_ast r = LIB.Z3_algebraic_root(a0, a1, a2);
5500  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5501  if (err != Z3_error_code.Z3_OK)
5502  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5503  return r;
5504  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast_vector Z3_algebraic_roots ( Z3_context  a0,
Z3_ast  a1,
uint  a2,
[In] Z3_ast[]  a3 
)
inlinestatic

Definition at line 5562 of file Native.cs.

5562  {
5563  Z3_ast_vector r = LIB.Z3_algebraic_roots(a0, a1, a2, a3);
5564  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5565  if (err != Z3_error_code.Z3_OK)
5566  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5567  return r;
5568  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static int Z3_algebraic_sign ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 5458 of file Native.cs.

5458  {
5459  int r = LIB.Z3_algebraic_sign(a0, a1);
5460  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5461  if (err != Z3_error_code.Z3_OK)
5462  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5463  return r;
5464  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast Z3_algebraic_sub ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 5474 of file Native.cs.

5474  {
5475  Z3_ast r = LIB.Z3_algebraic_sub(a0, a1, a2);
5476  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5477  if (err != Z3_error_code.Z3_OK)
5478  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5479  return r;
5480  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast Z3_app_to_ast ( Z3_context  a0,
Z3_app  a1 
)
inlinestatic

Definition at line 3206 of file Native.cs.

3206  {
3207  Z3_ast r = LIB.Z3_app_to_ast(a0, a1);
3208  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3209  if (err != Z3_error_code.Z3_OK)
3210  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3211  return r;
3212  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_append_log ( string  a0)
inlinestatic

Definition at line 3813 of file Native.cs.

3813  {
3814  LIB.Z3_append_log(a0);
3815  }
static Z3_model Z3_apply_result_convert_model ( Z3_context  a0,
Z3_apply_result  a1,
uint  a2,
Z3_model  a3 
)
inlinestatic

Definition at line 4847 of file Native.cs.

Referenced by ApplyResult.ConvertModel().

4847  {
4848  Z3_model r = LIB.Z3_apply_result_convert_model(a0, a1, a2, a3);
4849  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4850  if (err != Z3_error_code.Z3_OK)
4851  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4852  return r;
4853  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_apply_result_dec_ref ( Z3_context  a0,
Z3_apply_result  a1 
)
inlinestatic

Definition at line 4816 of file Native.cs.

4816  {
4817  LIB.Z3_apply_result_dec_ref(a0, a1);
4818  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4819  if (err != Z3_error_code.Z3_OK)
4820  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4821  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static uint Z3_apply_result_get_num_subgoals ( Z3_context  a0,
Z3_apply_result  a1 
)
inlinestatic

Definition at line 4831 of file Native.cs.

4831  {
4832  uint r = LIB.Z3_apply_result_get_num_subgoals(a0, a1);
4833  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4834  if (err != Z3_error_code.Z3_OK)
4835  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4836  return r;
4837  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_goal Z3_apply_result_get_subgoal ( Z3_context  a0,
Z3_apply_result  a1,
uint  a2 
)
inlinestatic

Definition at line 4839 of file Native.cs.

4839  {
4840  Z3_goal r = LIB.Z3_apply_result_get_subgoal(a0, a1, a2);
4841  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4842  if (err != Z3_error_code.Z3_OK)
4843  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4844  return r;
4845  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_apply_result_inc_ref ( Z3_context  a0,
Z3_apply_result  a1 
)
inlinestatic

Definition at line 4809 of file Native.cs.

4809  {
4810  LIB.Z3_apply_result_inc_ref(a0, a1);
4811  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4812  if (err != Z3_error_code.Z3_OK)
4813  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4814  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static string Z3_apply_result_to_string ( Z3_context  a0,
Z3_apply_result  a1 
)
inlinestatic

Definition at line 4823 of file Native.cs.

Referenced by ApplyResult.ToString().

4823  {
4824  IntPtr r = LIB.Z3_apply_result_to_string(a0, a1);
4825  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4826  if (err != Z3_error_code.Z3_OK)
4827  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4828  return Marshal.PtrToStringAnsi(r);
4829  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_assert_cnstr ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 5153 of file Native.cs.

5153  {
5154  LIB.Z3_assert_cnstr(a0, a1);
5155  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5156  if (err != Z3_error_code.Z3_OK)
5157  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5158  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static int Z3_ast_map_contains ( Z3_context  a0,
Z3_ast_map  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 4324 of file Native.cs.

4324  {
4325  int r = LIB.Z3_ast_map_contains(a0, a1, a2);
4326  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4327  if (err != Z3_error_code.Z3_OK)
4328  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4329  return r;
4330  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_ast_map_dec_ref ( Z3_context  a0,
Z3_ast_map  a1 
)
inlinestatic

Definition at line 4317 of file Native.cs.

4317  {
4318  LIB.Z3_ast_map_dec_ref(a0, a1);
4319  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4320  if (err != Z3_error_code.Z3_OK)
4321  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4322  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_ast_map_erase ( Z3_context  a0,
Z3_ast_map  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 4347 of file Native.cs.

4347  {
4348  LIB.Z3_ast_map_erase(a0, a1, a2);
4349  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4350  if (err != Z3_error_code.Z3_OK)
4351  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4352  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast Z3_ast_map_find ( Z3_context  a0,
Z3_ast_map  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 4332 of file Native.cs.

4332  {
4333  Z3_ast r = LIB.Z3_ast_map_find(a0, a1, a2);
4334  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4335  if (err != Z3_error_code.Z3_OK)
4336  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4337  return r;
4338  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_ast_map_inc_ref ( Z3_context  a0,
Z3_ast_map  a1 
)
inlinestatic

Definition at line 4310 of file Native.cs.

4310  {
4311  LIB.Z3_ast_map_inc_ref(a0, a1);
4312  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4313  if (err != Z3_error_code.Z3_OK)
4314  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4315  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_ast_map_insert ( Z3_context  a0,
Z3_ast_map  a1,
Z3_ast  a2,
Z3_ast  a3 
)
inlinestatic

Definition at line 4340 of file Native.cs.

4340  {
4341  LIB.Z3_ast_map_insert(a0, a1, a2, a3);
4342  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4343  if (err != Z3_error_code.Z3_OK)
4344  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4345  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast_vector Z3_ast_map_keys ( Z3_context  a0,
Z3_ast_map  a1 
)
inlinestatic

Definition at line 4369 of file Native.cs.

4369  {
4370  Z3_ast_vector r = LIB.Z3_ast_map_keys(a0, a1);
4371  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4372  if (err != Z3_error_code.Z3_OK)
4373  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4374  return r;
4375  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_ast_map_reset ( Z3_context  a0,
Z3_ast_map  a1 
)
inlinestatic

Definition at line 4354 of file Native.cs.

4354  {
4355  LIB.Z3_ast_map_reset(a0, a1);
4356  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4357  if (err != Z3_error_code.Z3_OK)
4358  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4359  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static uint Z3_ast_map_size ( Z3_context  a0,
Z3_ast_map  a1 
)
inlinestatic

Definition at line 4361 of file Native.cs.

4361  {
4362  uint r = LIB.Z3_ast_map_size(a0, a1);
4363  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4364  if (err != Z3_error_code.Z3_OK)
4365  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4366  return r;
4367  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static string Z3_ast_map_to_string ( Z3_context  a0,
Z3_ast_map  a1 
)
inlinestatic

Definition at line 4377 of file Native.cs.

4377  {
4378  IntPtr r = LIB.Z3_ast_map_to_string(a0, a1);
4379  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4380  if (err != Z3_error_code.Z3_OK)
4381  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4382  return Marshal.PtrToStringAnsi(r);
4383  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static string Z3_ast_to_string ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 3832 of file Native.cs.

Referenced by AST.SExpr(), and AST.ToString().

3832  {
3833  IntPtr r = LIB.Z3_ast_to_string(a0, a1);
3834  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3835  if (err != Z3_error_code.Z3_OK)
3836  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3837  return Marshal.PtrToStringAnsi(r);
3838  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_ast_vector_dec_ref ( Z3_context  a0,
Z3_ast_vector  a1 
)
inlinestatic

Definition at line 4242 of file Native.cs.

4242  {
4243  LIB.Z3_ast_vector_dec_ref(a0, a1);
4244  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4245  if (err != Z3_error_code.Z3_OK)
4246  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4247  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast Z3_ast_vector_get ( Z3_context  a0,
Z3_ast_vector  a1,
uint  a2 
)
inlinestatic

Definition at line 4257 of file Native.cs.

4257  {
4258  Z3_ast r = LIB.Z3_ast_vector_get(a0, a1, a2);
4259  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4260  if (err != Z3_error_code.Z3_OK)
4261  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4262  return r;
4263  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_ast_vector_inc_ref ( Z3_context  a0,
Z3_ast_vector  a1 
)
inlinestatic

Definition at line 4235 of file Native.cs.

4235  {
4236  LIB.Z3_ast_vector_inc_ref(a0, a1);
4237  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4238  if (err != Z3_error_code.Z3_OK)
4239  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4240  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_ast_vector_push ( Z3_context  a0,
Z3_ast_vector  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 4279 of file Native.cs.

4279  {
4280  LIB.Z3_ast_vector_push(a0, a1, a2);
4281  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4282  if (err != Z3_error_code.Z3_OK)
4283  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4284  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_ast_vector_resize ( Z3_context  a0,
Z3_ast_vector  a1,
uint  a2 
)
inlinestatic

Definition at line 4272 of file Native.cs.

4272  {
4273  LIB.Z3_ast_vector_resize(a0, a1, a2);
4274  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4275  if (err != Z3_error_code.Z3_OK)
4276  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4277  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_ast_vector_set ( Z3_context  a0,
Z3_ast_vector  a1,
uint  a2,
Z3_ast  a3 
)
inlinestatic

Definition at line 4265 of file Native.cs.

4265  {
4266  LIB.Z3_ast_vector_set(a0, a1, a2, a3);
4267  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4268  if (err != Z3_error_code.Z3_OK)
4269  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4270  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static uint Z3_ast_vector_size ( Z3_context  a0,
Z3_ast_vector  a1 
)
inlinestatic

Definition at line 4249 of file Native.cs.

4249  {
4250  uint r = LIB.Z3_ast_vector_size(a0, a1);
4251  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4252  if (err != Z3_error_code.Z3_OK)
4253  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4254  return r;
4255  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static string Z3_ast_vector_to_string ( Z3_context  a0,
Z3_ast_vector  a1 
)
inlinestatic

Definition at line 4294 of file Native.cs.

4294  {
4295  IntPtr r = LIB.Z3_ast_vector_to_string(a0, a1);
4296  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4297  if (err != Z3_error_code.Z3_OK)
4298  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4299  return Marshal.PtrToStringAnsi(r);
4300  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast_vector Z3_ast_vector_translate ( Z3_context  a0,
Z3_ast_vector  a1,
Z3_context  a2 
)
inlinestatic

Definition at line 4286 of file Native.cs.

4286  {
4287  Z3_ast_vector r = LIB.Z3_ast_vector_translate(a0, a1, a2);
4288  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4289  if (err != Z3_error_code.Z3_OK)
4290  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4291  return r;
4292  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static string 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 
)
inlinestatic

Definition at line 3872 of file Native.cs.

3872  {
3873  IntPtr r = LIB.Z3_benchmark_to_smtlib_string(a0, a1, a2, a3, a4, a5, a6, a7);
3874  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3875  if (err != Z3_error_code.Z3_OK)
3876  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3877  return Marshal.PtrToStringAnsi(r);
3878  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_block_literals ( Z3_context  a0,
Z3_literals  a1 
)
inlinestatic

Definition at line 5284 of file Native.cs.

5284  {
5285  LIB.Z3_block_literals(a0, a1);
5286  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5287  if (err != Z3_error_code.Z3_OK)
5288  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5289  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static int Z3_check ( Z3_context  a0)
inlinestatic

Definition at line 5168 of file Native.cs.

5168  {
5169  int r = LIB.Z3_check(a0);
5170  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5171  if (err != Z3_error_code.Z3_OK)
5172  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5173  return r;
5174  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static int Z3_check_and_get_model ( Z3_context  a0,
[In, Out] ref Z3_model  a1 
)
inlinestatic

Definition at line 5160 of file Native.cs.

5160  {
5161  int r = LIB.Z3_check_and_get_model(a0, ref a1);
5162  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5163  if (err != Z3_error_code.Z3_OK)
5164  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5165  return r;
5166  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
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 
)
inlinestatic

Definition at line 5176 of file Native.cs.

5176  {
5177  int r = LIB.Z3_check_assumptions(a0, a1, a2, ref a3, ref a4, ref a5, a6);
5178  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5179  if (err != Z3_error_code.Z3_OK)
5180  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5181  return r;
5182  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
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 
)
inlinestatic

Definition at line 5813 of file Native.cs.

5813  {
5814  int r = LIB.Z3_check_interpolant(a0, a1, a2, a3, a4, out a5, a6, a7);
5815  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5816  if (err != Z3_error_code.Z3_OK)
5817  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5818  return r;
5819  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_close_log ( )
inlinestatic

Definition at line 3817 of file Native.cs.

3817  {
3818  LIB.Z3_close_log();
3819  }
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 
)
inlinestatic

Definition at line 5789 of file Native.cs.

5789  {
5790  int r = LIB.Z3_compute_interpolant(a0, a1, a2, ref a3, ref a4);
5791  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5792  if (err != Z3_error_code.Z3_OK)
5793  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5794  return r;
5795  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static string Z3_context_to_string ( Z3_context  a0)
inlinestatic

Definition at line 5402 of file Native.cs.

5402  {
5403  IntPtr r = LIB.Z3_context_to_string(a0);
5404  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5405  if (err != Z3_error_code.Z3_OK)
5406  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5407  return Marshal.PtrToStringAnsi(r);
5408  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_dec_ref ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 1726 of file Native.cs.

1726  {
1727  LIB.Z3_dec_ref(a0, a1);
1728  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1729  if (err != Z3_error_code.Z3_OK)
1730  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1731  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_del_config ( Z3_config  a0)
inlinestatic

Definition at line 1693 of file Native.cs.

Referenced by Context.Context().

1693  {
1694  LIB.Z3_del_config(a0);
1695  }
static void Z3_del_constructor ( Z3_context  a0,
Z3_constructor  a1 
)
inlinestatic

Definition at line 1962 of file Native.cs.

1962  {
1963  LIB.Z3_del_constructor(a0, a1);
1964  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1965  if (err != Z3_error_code.Z3_OK)
1966  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1967  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_del_constructor_list ( Z3_context  a0,
Z3_constructor_list  a1 
)
inlinestatic

Definition at line 1985 of file Native.cs.

1985  {
1986  LIB.Z3_del_constructor_list(a0, a1);
1987  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1988  if (err != Z3_error_code.Z3_OK)
1989  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1990  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_del_context ( Z3_context  a0)
inlinestatic

Definition at line 1715 of file Native.cs.

1715  {
1716  LIB.Z3_del_context(a0);
1717  }
static void Z3_del_literals ( Z3_context  a0,
Z3_literals  a1 
)
inlinestatic

Definition at line 5246 of file Native.cs.

5246  {
5247  LIB.Z3_del_literals(a0, a1);
5248  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5249  if (err != Z3_error_code.Z3_OK)
5250  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5251  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_del_model ( Z3_context  a0,
Z3_model  a1 
)
inlinestatic

Definition at line 5192 of file Native.cs.

5192  {
5193  LIB.Z3_del_model(a0, a1);
5194  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5195  if (err != Z3_error_code.Z3_OK)
5196  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5197  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_disable_literal ( Z3_context  a0,
Z3_literals  a1,
uint  a2 
)
inlinestatic

Definition at line 5277 of file Native.cs.

5277  {
5278  LIB.Z3_disable_literal(a0, a1, a2);
5279  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5280  if (err != Z3_error_code.Z3_OK)
5281  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5282  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_disable_trace ( string  a0)
inlinestatic

Definition at line 4015 of file Native.cs.

4015  {
4016  LIB.Z3_disable_trace(a0);
4017  }
static void Z3_enable_trace ( string  a0)
inlinestatic

Definition at line 4011 of file Native.cs.

4011  {
4012  LIB.Z3_enable_trace(a0);
4013  }
delegate void Z3_error_handler ( Z3_context  c,
Z3_error_code  e 
)
static int Z3_eval ( Z3_context  a0,
Z3_model  a1,
Z3_ast  a2,
[In, Out] ref Z3_ast  a3 
)
inlinestatic

Definition at line 5386 of file Native.cs.

5386  {
5387  int r = LIB.Z3_eval(a0, a1, a2, ref a3);
5388  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5389  if (err != Z3_error_code.Z3_OK)
5390  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5391  return r;
5392  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
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 
)
inlinestatic

Definition at line 5394 of file Native.cs.

5394  {
5395  int r = LIB.Z3_eval_decl(a0, a1, a2, a3, a4, ref a5);
5396  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5397  if (err != Z3_error_code.Z3_OK)
5398  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5399  return r;
5400  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static int Z3_eval_func_decl ( Z3_context  a0,
Z3_model  a1,
Z3_func_decl  a2,
[In, Out] ref Z3_ast  a3 
)
inlinestatic

Definition at line 5323 of file Native.cs.

5323  {
5324  int r = LIB.Z3_eval_func_decl(a0, a1, a2, ref a3);
5325  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5326  if (err != Z3_error_code.Z3_OK)
5327  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5328  return r;
5329  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_fixedpoint_add_cover ( Z3_context  a0,
Z3_fixedpoint  a1,
int  a2,
Z3_func_decl  a3,
Z3_ast  a4 
)
inlinestatic

Definition at line 4121 of file Native.cs.

4121  {
4122  LIB.Z3_fixedpoint_add_cover(a0, a1, a2, a3, a4);
4123  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4124  if (err != Z3_error_code.Z3_OK)
4125  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4126  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_fixedpoint_add_fact ( Z3_context  a0,
Z3_fixedpoint  a1,
Z3_func_decl  a2,
uint  a3,
[In] uint[]  a4 
)
inlinestatic

Definition at line 4052 of file Native.cs.

4052  {
4053  LIB.Z3_fixedpoint_add_fact(a0, a1, a2, a3, a4);
4054  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4055  if (err != Z3_error_code.Z3_OK)
4056  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4057  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_fixedpoint_add_rule ( Z3_context  a0,
Z3_fixedpoint  a1,
Z3_ast  a2,
IntPtr  a3 
)
inlinestatic

Definition at line 4045 of file Native.cs.

4045  {
4046  LIB.Z3_fixedpoint_add_rule(a0, a1, a2, a3);
4047  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4048  if (err != Z3_error_code.Z3_OK)
4049  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4050  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_fixedpoint_assert ( Z3_context  a0,
Z3_fixedpoint  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 4059 of file Native.cs.

4059  {
4060  LIB.Z3_fixedpoint_assert(a0, a1, a2);
4061  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4062  if (err != Z3_error_code.Z3_OK)
4063  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4064  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_fixedpoint_dec_ref ( Z3_context  a0,
Z3_fixedpoint  a1 
)
inlinestatic

Definition at line 4038 of file Native.cs.

4038  {
4039  LIB.Z3_fixedpoint_dec_ref(a0, a1);
4040  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4041  if (err != Z3_error_code.Z3_OK)
4042  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4043  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast_vector Z3_fixedpoint_from_file ( Z3_context  a0,
Z3_fixedpoint  a1,
string  a2 
)
inlinestatic

Definition at line 4205 of file Native.cs.

4205  {
4206  Z3_ast_vector r = LIB.Z3_fixedpoint_from_file(a0, a1, a2);
4207  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4208  if (err != Z3_error_code.Z3_OK)
4209  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4210  return r;
4211  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast_vector Z3_fixedpoint_from_string ( Z3_context  a0,
Z3_fixedpoint  a1,
string  a2 
)
inlinestatic

Definition at line 4197 of file Native.cs.

4197  {
4198  Z3_ast_vector r = LIB.Z3_fixedpoint_from_string(a0, a1, a2);
4199  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4200  if (err != Z3_error_code.Z3_OK)
4201  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4202  return r;
4203  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast Z3_fixedpoint_get_answer ( Z3_context  a0,
Z3_fixedpoint  a1 
)
inlinestatic

Definition at line 4082 of file Native.cs.

4082  {
4083  Z3_ast r = LIB.Z3_fixedpoint_get_answer(a0, a1);
4084  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4085  if (err != Z3_error_code.Z3_OK)
4086  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4087  return r;
4088  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast_vector Z3_fixedpoint_get_assertions ( Z3_context  a0,
Z3_fixedpoint  a1 
)
inlinestatic

Definition at line 4158 of file Native.cs.

4158  {
4159  Z3_ast_vector r = LIB.Z3_fixedpoint_get_assertions(a0, a1);
4160  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4161  if (err != Z3_error_code.Z3_OK)
4162  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4163  return r;
4164  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast Z3_fixedpoint_get_cover_delta ( Z3_context  a0,
Z3_fixedpoint  a1,
int  a2,
Z3_func_decl  a3 
)
inlinestatic

Definition at line 4113 of file Native.cs.

4113  {
4114  Z3_ast r = LIB.Z3_fixedpoint_get_cover_delta(a0, a1, a2, a3);
4115  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4116  if (err != Z3_error_code.Z3_OK)
4117  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4118  return r;
4119  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static string Z3_fixedpoint_get_help ( Z3_context  a0,
Z3_fixedpoint  a1 
)
inlinestatic

Definition at line 4173 of file Native.cs.

4173  {
4174  IntPtr r = LIB.Z3_fixedpoint_get_help(a0, a1);
4175  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4176  if (err != Z3_error_code.Z3_OK)
4177  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4178  return Marshal.PtrToStringAnsi(r);
4179  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static uint Z3_fixedpoint_get_num_levels ( Z3_context  a0,
Z3_fixedpoint  a1,
Z3_func_decl  a2 
)
inlinestatic

Definition at line 4105 of file Native.cs.

4105  {
4106  uint r = LIB.Z3_fixedpoint_get_num_levels(a0, a1, a2);
4107  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4108  if (err != Z3_error_code.Z3_OK)
4109  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4110  return r;
4111  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_param_descrs Z3_fixedpoint_get_param_descrs ( Z3_context  a0,
Z3_fixedpoint  a1 
)
inlinestatic

Definition at line 4181 of file Native.cs.

4181  {
4182  Z3_param_descrs r = LIB.Z3_fixedpoint_get_param_descrs(a0, a1);
4183  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4184  if (err != Z3_error_code.Z3_OK)
4185  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4186  return r;
4187  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static string Z3_fixedpoint_get_reason_unknown ( Z3_context  a0,
Z3_fixedpoint  a1 
)
inlinestatic

Definition at line 4090 of file Native.cs.

4090  {
4091  IntPtr r = LIB.Z3_fixedpoint_get_reason_unknown(a0, a1);
4092  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4093  if (err != Z3_error_code.Z3_OK)
4094  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4095  return Marshal.PtrToStringAnsi(r);
4096  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast_vector Z3_fixedpoint_get_rules ( Z3_context  a0,
Z3_fixedpoint  a1 
)
inlinestatic

Definition at line 4150 of file Native.cs.

4150  {
4151  Z3_ast_vector r = LIB.Z3_fixedpoint_get_rules(a0, a1);
4152  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4153  if (err != Z3_error_code.Z3_OK)
4154  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4155  return r;
4156  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_stats Z3_fixedpoint_get_statistics ( Z3_context  a0,
Z3_fixedpoint  a1 
)
inlinestatic

Definition at line 4128 of file Native.cs.

4128  {
4129  Z3_stats r = LIB.Z3_fixedpoint_get_statistics(a0, a1);
4130  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4131  if (err != Z3_error_code.Z3_OK)
4132  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4133  return r;
4134  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_fixedpoint_inc_ref ( Z3_context  a0,
Z3_fixedpoint  a1 
)
inlinestatic

Definition at line 4031 of file Native.cs.

4031  {
4032  LIB.Z3_fixedpoint_inc_ref(a0, a1);
4033  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4034  if (err != Z3_error_code.Z3_OK)
4035  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4036  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_fixedpoint_pop ( Z3_context  a0,
Z3_fixedpoint  a1 
)
inlinestatic

Definition at line 4220 of file Native.cs.

4220  {
4221  LIB.Z3_fixedpoint_pop(a0, a1);
4222  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4223  if (err != Z3_error_code.Z3_OK)
4224  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4225  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_fixedpoint_push ( Z3_context  a0,
Z3_fixedpoint  a1 
)
inlinestatic

Definition at line 4213 of file Native.cs.

4213  {
4214  LIB.Z3_fixedpoint_push(a0, a1);
4215  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4216  if (err != Z3_error_code.Z3_OK)
4217  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4218  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static int Z3_fixedpoint_query ( Z3_context  a0,
Z3_fixedpoint  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 4066 of file Native.cs.

4066  {
4067  int r = LIB.Z3_fixedpoint_query(a0, a1, a2);
4068  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4069  if (err != Z3_error_code.Z3_OK)
4070  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4071  return r;
4072  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static int Z3_fixedpoint_query_relations ( Z3_context  a0,
Z3_fixedpoint  a1,
uint  a2,
[In] Z3_func_decl[]  a3 
)
inlinestatic

Definition at line 4074 of file Native.cs.

4074  {
4075  int r = LIB.Z3_fixedpoint_query_relations(a0, a1, a2, a3);
4076  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4077  if (err != Z3_error_code.Z3_OK)
4078  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4079  return r;
4080  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_fixedpoint_register_relation ( Z3_context  a0,
Z3_fixedpoint  a1,
Z3_func_decl  a2 
)
inlinestatic

Definition at line 4136 of file Native.cs.

4136  {
4137  LIB.Z3_fixedpoint_register_relation(a0, a1, a2);
4138  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4139  if (err != Z3_error_code.Z3_OK)
4140  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4141  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_fixedpoint_set_params ( Z3_context  a0,
Z3_fixedpoint  a1,
Z3_params  a2 
)
inlinestatic

Definition at line 4166 of file Native.cs.

4166  {
4167  LIB.Z3_fixedpoint_set_params(a0, a1, a2);
4168  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4169  if (err != Z3_error_code.Z3_OK)
4170  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4171  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_fixedpoint_set_predicate_representation ( Z3_context  a0,
Z3_fixedpoint  a1,
Z3_func_decl  a2,
uint  a3,
[In] IntPtr[]  a4 
)
inlinestatic

Definition at line 4143 of file Native.cs.

4143  {
4144  LIB.Z3_fixedpoint_set_predicate_representation(a0, a1, a2, a3, a4);
4145  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4146  if (err != Z3_error_code.Z3_OK)
4147  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4148  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static string Z3_fixedpoint_to_string ( Z3_context  a0,
Z3_fixedpoint  a1,
uint  a2,
[In] Z3_ast[]  a3 
)
inlinestatic

Definition at line 4189 of file Native.cs.

4189  {
4190  IntPtr r = LIB.Z3_fixedpoint_to_string(a0, a1, a2, a3);
4191  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4192  if (err != Z3_error_code.Z3_OK)
4193  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4194  return Marshal.PtrToStringAnsi(r);
4195  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_fixedpoint_update_rule ( Z3_context  a0,
Z3_fixedpoint  a1,
Z3_ast  a2,
IntPtr  a3 
)
inlinestatic

Definition at line 4098 of file Native.cs.

4098  {
4099  LIB.Z3_fixedpoint_update_rule(a0, a1, a2, a3);
4100  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4101  if (err != Z3_error_code.Z3_OK)
4102  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4103  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast Z3_func_decl_to_ast ( Z3_context  a0,
Z3_func_decl  a1 
)
inlinestatic

Definition at line 3062 of file Native.cs.

3062  {
3063  Z3_ast r = LIB.Z3_func_decl_to_ast(a0, a1);
3064  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3065  if (err != Z3_error_code.Z3_OK)
3066  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3067  return r;
3068  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static string Z3_func_decl_to_string ( Z3_context  a0,
Z3_func_decl  a1 
)
inlinestatic

Definition at line 3856 of file Native.cs.

Referenced by FuncDecl.ToString().

3856  {
3857  IntPtr r = LIB.Z3_func_decl_to_string(a0, a1);
3858  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3859  if (err != Z3_error_code.Z3_OK)
3860  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3861  return Marshal.PtrToStringAnsi(r);
3862  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_func_entry_dec_ref ( Z3_context  a0,
Z3_func_entry  a1 
)
inlinestatic

Definition at line 3777 of file Native.cs.

3777  {
3778  LIB.Z3_func_entry_dec_ref(a0, a1);
3779  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3780  if (err != Z3_error_code.Z3_OK)
3781  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3782  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast Z3_func_entry_get_arg ( Z3_context  a0,
Z3_func_entry  a1,
uint  a2 
)
inlinestatic

Definition at line 3800 of file Native.cs.

3800  {
3801  Z3_ast r = LIB.Z3_func_entry_get_arg(a0, a1, a2);
3802  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3803  if (err != Z3_error_code.Z3_OK)
3804  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3805  return r;
3806  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static uint Z3_func_entry_get_num_args ( Z3_context  a0,
Z3_func_entry  a1 
)
inlinestatic

Definition at line 3792 of file Native.cs.

3792  {
3793  uint r = LIB.Z3_func_entry_get_num_args(a0, a1);
3794  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3795  if (err != Z3_error_code.Z3_OK)
3796  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3797  return r;
3798  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast Z3_func_entry_get_value ( Z3_context  a0,
Z3_func_entry  a1 
)
inlinestatic

Definition at line 3784 of file Native.cs.

3784  {
3785  Z3_ast r = LIB.Z3_func_entry_get_value(a0, a1);
3786  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3787  if (err != Z3_error_code.Z3_OK)
3788  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3789  return r;
3790  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_func_entry_inc_ref ( Z3_context  a0,
Z3_func_entry  a1 
)
inlinestatic

Definition at line 3770 of file Native.cs.

3770  {
3771  LIB.Z3_func_entry_inc_ref(a0, a1);
3772  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3773  if (err != Z3_error_code.Z3_OK)
3774  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3775  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_func_interp_dec_ref ( Z3_context  a0,
Z3_func_interp  a1 
)
inlinestatic

Definition at line 3731 of file Native.cs.

3731  {
3732  LIB.Z3_func_interp_dec_ref(a0, a1);
3733  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3734  if (err != Z3_error_code.Z3_OK)
3735  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3736  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static uint Z3_func_interp_get_arity ( Z3_context  a0,
Z3_func_interp  a1 
)
inlinestatic

Definition at line 3762 of file Native.cs.

3762  {
3763  uint r = LIB.Z3_func_interp_get_arity(a0, a1);
3764  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3765  if (err != Z3_error_code.Z3_OK)
3766  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3767  return r;
3768  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast Z3_func_interp_get_else ( Z3_context  a0,
Z3_func_interp  a1 
)
inlinestatic

Definition at line 3754 of file Native.cs.

3754  {
3755  Z3_ast r = LIB.Z3_func_interp_get_else(a0, a1);
3756  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3757  if (err != Z3_error_code.Z3_OK)
3758  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3759  return r;
3760  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_func_entry Z3_func_interp_get_entry ( Z3_context  a0,
Z3_func_interp  a1,
uint  a2 
)
inlinestatic

Definition at line 3746 of file Native.cs.

3746  {
3747  Z3_func_entry r = LIB.Z3_func_interp_get_entry(a0, a1, a2);
3748  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3749  if (err != Z3_error_code.Z3_OK)
3750  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3751  return r;
3752  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static uint Z3_func_interp_get_num_entries ( Z3_context  a0,
Z3_func_interp  a1 
)
inlinestatic

Definition at line 3738 of file Native.cs.

3738  {
3739  uint r = LIB.Z3_func_interp_get_num_entries(a0, a1);
3740  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3741  if (err != Z3_error_code.Z3_OK)
3742  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3743  return r;
3744  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static void Z3_func_interp_inc_ref ( Z3_context  a0,
Z3_func_interp  a1 
)
inlinestatic

Definition at line 3724 of file Native.cs.

3724  {
3725  LIB.Z3_func_interp_inc_ref(a0, a1);
3726  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3727  if (err != Z3_error_code.Z3_OK)
3728  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3729  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast Z3_get_algebraic_number_lower ( Z3_context  a0,
Z3_ast  a1,
uint  a2 
)
inlinestatic

Definition at line 3414 of file Native.cs.

3414  {
3415  Z3_ast r = LIB.Z3_get_algebraic_number_lower(a0, a1, a2);
3416  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3417  if (err != Z3_error_code.Z3_OK)
3418  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3419  return r;
3420  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast Z3_get_algebraic_number_upper ( Z3_context  a0,
Z3_ast  a1,
uint  a2 
)
inlinestatic

Definition at line 3422 of file Native.cs.

3422  {
3423  Z3_ast r = LIB.Z3_get_algebraic_number_upper(a0, a1, a2);
3424  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3425  if (err != Z3_error_code.Z3_OK)
3426  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3427  return r;
3428  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast Z3_get_app_arg ( Z3_context  a0,
Z3_app  a1,
uint  a2 
)
inlinestatic

Definition at line 3230 of file Native.cs.

3230  {
3231  Z3_ast r = LIB.Z3_get_app_arg(a0, a1, a2);
3232  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3233  if (err != Z3_error_code.Z3_OK)
3234  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3235  return r;
3236  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_func_decl Z3_get_app_decl ( Z3_context  a0,
Z3_app  a1 
)
inlinestatic

Definition at line 3214 of file Native.cs.

3214  {
3215  Z3_func_decl r = LIB.Z3_get_app_decl(a0, a1);
3216  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3217  if (err != Z3_error_code.Z3_OK)
3218  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3219  return r;
3220  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static uint Z3_get_app_num_args ( Z3_context  a0,
Z3_app  a1 
)
inlinestatic

Definition at line 3222 of file Native.cs.

3222  {
3223  uint r = LIB.Z3_get_app_num_args(a0, a1);
3224  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3225  if (err != Z3_error_code.Z3_OK)
3226  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3227  return r;
3228  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static uint Z3_get_arity ( Z3_context  a0,
Z3_func_decl  a1 
)
inlinestatic

Definition at line 3110 of file Native.cs.

3110  {
3111  uint r = LIB.Z3_get_arity(a0, a1);
3112  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3113  if (err != Z3_error_code.Z3_OK)
3114  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3115  return r;
3116  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_sort Z3_get_array_sort_domain ( Z3_context  a0,
Z3_sort  a1 
)
inlinestatic

Definition at line 2974 of file Native.cs.

2974  {
2975  Z3_sort r = LIB.Z3_get_array_sort_domain(a0, a1);
2976  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2977  if (err != Z3_error_code.Z3_OK)
2978  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2979  return r;
2980  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_sort Z3_get_array_sort_range ( Z3_context  a0,
Z3_sort  a1 
)
inlinestatic

Definition at line 2982 of file Native.cs.

2982  {
2983  Z3_sort r = LIB.Z3_get_array_sort_range(a0, a1);
2984  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2985  if (err != Z3_error_code.Z3_OK)
2986  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2987  return r;
2988  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
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 
)
inlinestatic

Definition at line 5339 of file Native.cs.

5339  {
5340  LIB.Z3_get_array_value(a0, a1, a2, a3, a4, a5, ref a6);
5341  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5342  if (err != Z3_error_code.Z3_OK)
5343  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5344  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_func_decl Z3_get_as_array_func_decl ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 3716 of file Native.cs.

Referenced by Model.FuncInterp().

3716  {
3717  Z3_func_decl r = LIB.Z3_get_as_array_func_decl(a0, a1);
3718  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3719  if (err != Z3_error_code.Z3_OK)
3720  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3721  return r;
3722  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static uint Z3_get_ast_hash ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 3254 of file Native.cs.

Referenced by AST.GetHashCode().

3254  {
3255  uint r = LIB.Z3_get_ast_hash(a0, a1);
3256  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3257  if (err != Z3_error_code.Z3_OK)
3258  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3259  return r;
3260  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static uint Z3_get_ast_id ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 3246 of file Native.cs.

3246  {
3247  uint r = LIB.Z3_get_ast_id(a0, a1);
3248  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3249  if (err != Z3_error_code.Z3_OK)
3250  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3251  return r;
3252  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static uint Z3_get_ast_kind ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 3286 of file Native.cs.

3286  {
3287  uint r = LIB.Z3_get_ast_kind(a0, a1);
3288  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3289  if (err != Z3_error_code.Z3_OK)
3290  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3291  return r;
3292  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static uint Z3_get_bool_value ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 3278 of file Native.cs.

3278  {
3279  uint r = LIB.Z3_get_bool_value(a0, a1);
3280  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3281  if (err != Z3_error_code.Z3_OK)
3282  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3283  return r;
3284  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static uint Z3_get_bv_sort_size ( Z3_context  a0,
Z3_sort  a1 
)
inlinestatic

Definition at line 2958 of file Native.cs.

2958  {
2959  uint r = LIB.Z3_get_bv_sort_size(a0, a1);
2960  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2961  if (err != Z3_error_code.Z3_OK)
2962  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2963  return r;
2964  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast Z3_get_context_assignment ( Z3_context  a0)
inlinestatic

Definition at line 5418 of file Native.cs.

5418  {
5419  Z3_ast r = LIB.Z3_get_context_assignment(a0);
5420  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5421  if (err != Z3_error_code.Z3_OK)
5422  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5423  return r;
5424  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_func_decl Z3_get_datatype_sort_constructor ( Z3_context  a0,
Z3_sort  a1,
uint  a2 
)
inlinestatic

Definition at line 3022 of file Native.cs.

3022  {
3023  Z3_func_decl r = LIB.Z3_get_datatype_sort_constructor(a0, a1, a2);
3024  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3025  if (err != Z3_error_code.Z3_OK)
3026  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3027  return r;
3028  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_func_decl Z3_get_datatype_sort_constructor_accessor ( Z3_context  a0,
Z3_sort  a1,
uint  a2,
uint  a3 
)
inlinestatic

Definition at line 3038 of file Native.cs.

3038  {
3039  Z3_func_decl r = LIB.Z3_get_datatype_sort_constructor_accessor(a0, a1, a2, a3);
3040  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3041  if (err != Z3_error_code.Z3_OK)
3042  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3043  return r;
3044  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static uint Z3_get_datatype_sort_num_constructors ( Z3_context  a0,
Z3_sort  a1 
)
inlinestatic

Definition at line 3014 of file Native.cs.

3014  {
3015  uint r = LIB.Z3_get_datatype_sort_num_constructors(a0, a1);
3016  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3017  if (err != Z3_error_code.Z3_OK)
3018  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3019  return r;
3020  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_func_decl Z3_get_datatype_sort_recognizer ( Z3_context  a0,
Z3_sort  a1,
uint  a2 
)
inlinestatic

Definition at line 3030 of file Native.cs.

3030  {
3031  Z3_func_decl r = LIB.Z3_get_datatype_sort_recognizer(a0, a1, a2);
3032  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3033  if (err != Z3_error_code.Z3_OK)
3034  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3035  return r;
3036  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast Z3_get_decl_ast_parameter ( Z3_context  a0,
Z3_func_decl  a1,
uint  a2 
)
inlinestatic

Definition at line 3182 of file Native.cs.

3182  {
3183  Z3_ast r = LIB.Z3_get_decl_ast_parameter(a0, a1, a2);
3184  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3185  if (err != Z3_error_code.Z3_OK)
3186  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3187  return r;
3188  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static double Z3_get_decl_double_parameter ( Z3_context  a0,
Z3_func_decl  a1,
uint  a2 
)
inlinestatic

Definition at line 3158 of file Native.cs.

3158  {
3159  double r = LIB.Z3_get_decl_double_parameter(a0, a1, a2);
3160  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3161  if (err != Z3_error_code.Z3_OK)
3162  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3163  return r;
3164  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_func_decl Z3_get_decl_func_decl_parameter ( Z3_context  a0,
Z3_func_decl  a1,
uint  a2 
)
inlinestatic

Definition at line 3190 of file Native.cs.

3190  {
3191  Z3_func_decl r = LIB.Z3_get_decl_func_decl_parameter(a0, a1, a2);
3192  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3193  if (err != Z3_error_code.Z3_OK)
3194  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3195  return r;
3196  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static int Z3_get_decl_int_parameter ( Z3_context  a0,
Z3_func_decl  a1,
uint  a2 
)
inlinestatic

Definition at line 3150 of file Native.cs.

3150  {
3151  int r = LIB.Z3_get_decl_int_parameter(a0, a1, a2);
3152  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3153  if (err != Z3_error_code.Z3_OK)
3154  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3155  return r;
3156  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static uint Z3_get_decl_kind ( Z3_context  a0,
Z3_func_decl  a1 
)
inlinestatic

Definition at line 3094 of file Native.cs.

3094  {
3095  uint r = LIB.Z3_get_decl_kind(a0, a1);
3096  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3097  if (err != Z3_error_code.Z3_OK)
3098  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3099  return r;
3100  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static IntPtr Z3_get_decl_name ( Z3_context  a0,
Z3_func_decl  a1 
)
inlinestatic

Definition at line 3086 of file Native.cs.

3086  {
3087  IntPtr r = LIB.Z3_get_decl_name(a0, a1);
3088  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3089  if (err != Z3_error_code.Z3_OK)
3090  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3091  return r;
3092  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static uint Z3_get_decl_num_parameters ( Z3_context  a0,
Z3_func_decl  a1 
)
inlinestatic

Definition at line 3134 of file Native.cs.

3134  {
3135  uint r = LIB.Z3_get_decl_num_parameters(a0, a1);
3136  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3137  if (err != Z3_error_code.Z3_OK)
3138  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3139  return r;
3140  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static uint Z3_get_decl_parameter_kind ( Z3_context  a0,
Z3_func_decl  a1,
uint  a2 
)
inlinestatic

Definition at line 3142 of file Native.cs.

3142  {
3143  uint r = LIB.Z3_get_decl_parameter_kind(a0, a1, a2);
3144  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3145  if (err != Z3_error_code.Z3_OK)
3146  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3147  return r;
3148  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static string Z3_get_decl_rational_parameter ( Z3_context  a0,
Z3_func_decl  a1,
uint  a2 
)
inlinestatic

Definition at line 3198 of file Native.cs.

3198  {
3199  IntPtr r = LIB.Z3_get_decl_rational_parameter(a0, a1, a2);
3200  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3201  if (err != Z3_error_code.Z3_OK)
3202  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3203  return Marshal.PtrToStringAnsi(r);
3204  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_sort Z3_get_decl_sort_parameter ( Z3_context  a0,
Z3_func_decl  a1,
uint  a2 
)
inlinestatic

Definition at line 3174 of file Native.cs.

3174  {
3175  Z3_sort r = LIB.Z3_get_decl_sort_parameter(a0, a1, a2);
3176  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3177  if (err != Z3_error_code.Z3_OK)
3178  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3179  return r;
3180  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static IntPtr Z3_get_decl_symbol_parameter ( Z3_context  a0,
Z3_func_decl  a1,
uint  a2 
)
inlinestatic

Definition at line 3166 of file Native.cs.

3166  {
3167  IntPtr r = LIB.Z3_get_decl_symbol_parameter(a0, a1, a2);
3168  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3169  if (err != Z3_error_code.Z3_OK)
3170  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3171  return r;
3172  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast Z3_get_denominator ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 3358 of file Native.cs.

3358  {
3359  Z3_ast r = LIB.Z3_get_denominator(a0, a1);
3360  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3361  if (err != Z3_error_code.Z3_OK)
3362  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3363  return r;
3364  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_sort Z3_get_domain ( Z3_context  a0,
Z3_func_decl  a1,
uint  a2 
)
inlinestatic

Definition at line 3118 of file Native.cs.

3118  {
3119  Z3_sort r = LIB.Z3_get_domain(a0, a1, a2);
3120  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3121  if (err != Z3_error_code.Z3_OK)
3122  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3123  return r;
3124  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static uint Z3_get_domain_size ( Z3_context  a0,
Z3_func_decl  a1 
)
inlinestatic

Definition at line 3102 of file Native.cs.

3102  {
3103  uint r = LIB.Z3_get_domain_size(a0, a1);
3104  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3105  if (err != Z3_error_code.Z3_OK)
3106  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3107  return r;
3108  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static uint Z3_get_error_code ( Z3_context  a0)
inlinestatic

Definition at line 3982 of file Native.cs.

3982  {
3983  uint r = LIB.Z3_get_error_code(a0);
3984  return r;
3985  }
static string Z3_get_error_msg ( uint  a0)
inlinestatic

Definition at line 3994 of file Native.cs.

3994  {
3995  IntPtr r = LIB.Z3_get_error_msg(a0);
3996  return Marshal.PtrToStringAnsi(r);
3997  }
static string Z3_get_error_msg_ex ( Z3_context  a0,
uint  a1 
)
inlinestatic

Definition at line 3999 of file Native.cs.

3999  {
4000  IntPtr r = LIB.Z3_get_error_msg_ex(a0, a1);
4001  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
4002  if (err != Z3_error_code.Z3_OK)
4003  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
4004  return Marshal.PtrToStringAnsi(r);
4005  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static int Z3_get_finite_domain_sort_size ( Z3_context  a0,
Z3_sort  a1,
[In, Out] ref UInt64  a2 
)
inlinestatic

Definition at line 2966 of file Native.cs.

2966  {
2967  int r = LIB.Z3_get_finite_domain_sort_size(a0, a1, ref a2);
2968  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2969  if (err != Z3_error_code.Z3_OK)
2970  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2971  return r;
2972  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static uint Z3_get_func_decl_id ( Z3_context  a0,
Z3_func_decl  a1 
)
inlinestatic

Definition at line 3078 of file Native.cs.

3078  {
3079  uint r = LIB.Z3_get_func_decl_id(a0, a1);
3080  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3081  if (err != Z3_error_code.Z3_OK)
3082  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3083  return r;
3084  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_literals Z3_get_guessed_literals ( Z3_context  a0)
inlinestatic

Definition at line 5238 of file Native.cs.

5238  {
5239  Z3_literals r = LIB.Z3_get_guessed_literals(a0);
5240  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5241  if (err != Z3_error_code.Z3_OK)
5242  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5243  return r;
5244  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static uint Z3_get_implied_equalities ( Z3_context  a0,
Z3_solver  a1,
uint  a2,
[In] Z3_ast[]  a3,
[Out] uint[]  a4 
)
inlinestatic

Definition at line 5184 of file Native.cs.

5184  {
5185  uint r = LIB.Z3_get_implied_equalities(a0, a1, a2, a3, a4);
5186  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5187  if (err != Z3_error_code.Z3_OK)
5188  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5189  return r;
5190  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static uint Z3_get_index_value ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 3454 of file Native.cs.

3454  {
3455  uint r = LIB.Z3_get_index_value(a0, a1);
3456  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
3457  if (err != Z3_error_code.Z3_OK)
3458  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
3459  return r;
3460  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast_vector Z3_get_interpolant ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2,
Z3_params  a3 
)
inlinestatic

Definition at line 5781 of file Native.cs.

5781  {
5782  Z3_ast_vector r = LIB.Z3_get_interpolant(a0, a1, a2, a3);
5783  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5784  if (err != Z3_error_code.Z3_OK)
5785  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5786  return r;
5787  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static IntPtr Z3_get_label_symbol ( Z3_context  a0,
Z3_literals  a1,
uint  a2 
)
inlinestatic

Definition at line 5261 of file Native.cs.

5261  {
5262  IntPtr r = LIB.Z3_get_label_symbol(a0, a1, a2);
5263  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5264  if (err != Z3_error_code.Z3_OK)
5265  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5266  return r;
5267  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast Z3_get_literal ( Z3_context  a0,
Z3_literals  a1,
uint  a2 
)
inlinestatic

Definition at line 5269 of file Native.cs.

5269  {
5270  Z3_ast r = LIB.Z3_get_literal(a0, a1, a2);
5271  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5272  if (err != Z3_error_code.Z3_OK)
5273  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5274  return r;
5275  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_func_decl Z3_get_model_constant ( Z3_context  a0,
Z3_model  a1,
uint  a2 
)
inlinestatic

Definition at line 5299 of file Native.cs.

5299  {
5300  Z3_func_decl r = LIB.Z3_get_model_constant(a0, a1, a2);
5301  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5302  if (err != Z3_error_code.Z3_OK)
5303  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5304  return r;
5305  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_func_decl Z3_get_model_func_decl ( Z3_context  a0,
Z3_model  a1,
uint  a2 
)
inlinestatic

Definition at line 5315 of file Native.cs.

5315  {
5316  Z3_func_decl r = LIB.Z3_get_model_func_decl(a0, a1, a2);
5317  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
5318  if (err != Z3_error_code.Z3_OK)
5319  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
5320  return r;
5321  }
Z3_error_code
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
static Z3_ast Z3_get_model_func_else ( Z3_context  a0,
Z3_model  a1,
uint  a2 
)