Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups 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 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 int Z3_get_param_value (Z3_context a0, string a1, out IntPtr 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 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, uint a1,[In] Z3_ast[] a2,[Out] uint[] a3)
 
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)
 

Detailed Description

Definition at line 38 of file Native.cs.

Member Function Documentation

static Z3_ast Z3_app_to_ast ( Z3_context  a0,
Z3_app  a1 
)
inlinestatic

Definition at line 3034 of file Native.cs.

{
Z3_ast r = LIB.Z3_app_to_ast(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static void Z3_append_log ( string  a0)
inlinestatic

Definition at line 3633 of file Native.cs.

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

Definition at line 4670 of file Native.cs.

Referenced by ApplyResult.ConvertModel().

{
Z3_model r = LIB.Z3_apply_result_convert_model(a0, a1, a2, a3);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static void Z3_apply_result_dec_ref ( Z3_context  a0,
Z3_apply_result  a1 
)
inlinestatic

Definition at line 4639 of file Native.cs.

{
LIB.Z3_apply_result_dec_ref(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static uint Z3_apply_result_get_num_subgoals ( Z3_context  a0,
Z3_apply_result  a1 
)
inlinestatic

Definition at line 4654 of file Native.cs.

{
uint r = LIB.Z3_apply_result_get_num_subgoals(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_goal Z3_apply_result_get_subgoal ( Z3_context  a0,
Z3_apply_result  a1,
uint  a2 
)
inlinestatic

Definition at line 4662 of file Native.cs.

{
Z3_goal r = LIB.Z3_apply_result_get_subgoal(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static void Z3_apply_result_inc_ref ( Z3_context  a0,
Z3_apply_result  a1 
)
inlinestatic

Definition at line 4632 of file Native.cs.

{
LIB.Z3_apply_result_inc_ref(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static string Z3_apply_result_to_string ( Z3_context  a0,
Z3_apply_result  a1 
)
inlinestatic

Definition at line 4646 of file Native.cs.

Referenced by ApplyResult.ToString().

{
IntPtr r = LIB.Z3_apply_result_to_string(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return Marshal.PtrToStringAnsi(r);
}
static void Z3_assert_cnstr ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 4976 of file Native.cs.

{
LIB.Z3_assert_cnstr(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static int Z3_ast_map_contains ( Z3_context  a0,
Z3_ast_map  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 4147 of file Native.cs.

{
int r = LIB.Z3_ast_map_contains(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static void Z3_ast_map_dec_ref ( Z3_context  a0,
Z3_ast_map  a1 
)
inlinestatic

Definition at line 4140 of file Native.cs.

{
LIB.Z3_ast_map_dec_ref(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static void Z3_ast_map_erase ( Z3_context  a0,
Z3_ast_map  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 4170 of file Native.cs.

{
LIB.Z3_ast_map_erase(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static Z3_ast Z3_ast_map_find ( Z3_context  a0,
Z3_ast_map  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 4155 of file Native.cs.

{
Z3_ast r = LIB.Z3_ast_map_find(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static void Z3_ast_map_inc_ref ( Z3_context  a0,
Z3_ast_map  a1 
)
inlinestatic

Definition at line 4133 of file Native.cs.

{
LIB.Z3_ast_map_inc_ref(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static void Z3_ast_map_insert ( Z3_context  a0,
Z3_ast_map  a1,
Z3_ast  a2,
Z3_ast  a3 
)
inlinestatic

Definition at line 4163 of file Native.cs.

{
LIB.Z3_ast_map_insert(a0, a1, a2, a3);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static Z3_ast_vector Z3_ast_map_keys ( Z3_context  a0,
Z3_ast_map  a1 
)
inlinestatic

Definition at line 4192 of file Native.cs.

{
Z3_ast_vector r = LIB.Z3_ast_map_keys(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static void Z3_ast_map_reset ( Z3_context  a0,
Z3_ast_map  a1 
)
inlinestatic

Definition at line 4177 of file Native.cs.

{
LIB.Z3_ast_map_reset(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static uint Z3_ast_map_size ( Z3_context  a0,
Z3_ast_map  a1 
)
inlinestatic

Definition at line 4184 of file Native.cs.

{
uint r = LIB.Z3_ast_map_size(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static string Z3_ast_map_to_string ( Z3_context  a0,
Z3_ast_map  a1 
)
inlinestatic

Definition at line 4200 of file Native.cs.

{
IntPtr r = LIB.Z3_ast_map_to_string(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return Marshal.PtrToStringAnsi(r);
}
static string Z3_ast_to_string ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 3652 of file Native.cs.

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

{
IntPtr r = LIB.Z3_ast_to_string(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return Marshal.PtrToStringAnsi(r);
}
static void Z3_ast_vector_dec_ref ( Z3_context  a0,
Z3_ast_vector  a1 
)
inlinestatic

Definition at line 4065 of file Native.cs.

{
LIB.Z3_ast_vector_dec_ref(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static Z3_ast Z3_ast_vector_get ( Z3_context  a0,
Z3_ast_vector  a1,
uint  a2 
)
inlinestatic

Definition at line 4080 of file Native.cs.

{
Z3_ast r = LIB.Z3_ast_vector_get(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static void Z3_ast_vector_inc_ref ( Z3_context  a0,
Z3_ast_vector  a1 
)
inlinestatic

Definition at line 4058 of file Native.cs.

{
LIB.Z3_ast_vector_inc_ref(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static void Z3_ast_vector_push ( Z3_context  a0,
Z3_ast_vector  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 4102 of file Native.cs.

{
LIB.Z3_ast_vector_push(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static void Z3_ast_vector_resize ( Z3_context  a0,
Z3_ast_vector  a1,
uint  a2 
)
inlinestatic

Definition at line 4095 of file Native.cs.

{
LIB.Z3_ast_vector_resize(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static void Z3_ast_vector_set ( Z3_context  a0,
Z3_ast_vector  a1,
uint  a2,
Z3_ast  a3 
)
inlinestatic

Definition at line 4088 of file Native.cs.

{
LIB.Z3_ast_vector_set(a0, a1, a2, a3);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static uint Z3_ast_vector_size ( Z3_context  a0,
Z3_ast_vector  a1 
)
inlinestatic

Definition at line 4072 of file Native.cs.

{
uint r = LIB.Z3_ast_vector_size(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static string Z3_ast_vector_to_string ( Z3_context  a0,
Z3_ast_vector  a1 
)
inlinestatic

Definition at line 4117 of file Native.cs.

{
IntPtr r = LIB.Z3_ast_vector_to_string(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return Marshal.PtrToStringAnsi(r);
}
static Z3_ast_vector Z3_ast_vector_translate ( Z3_context  a0,
Z3_ast_vector  a1,
Z3_context  a2 
)
inlinestatic

Definition at line 4109 of file Native.cs.

{
Z3_ast_vector r = LIB.Z3_ast_vector_translate(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
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 3692 of file Native.cs.

Referenced by Context.BenchmarkToSMTString().

{
IntPtr r = LIB.Z3_benchmark_to_smtlib_string(a0, a1, a2, a3, a4, a5, a6, a7);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return Marshal.PtrToStringAnsi(r);
}
static void Z3_block_literals ( Z3_context  a0,
Z3_literals  a1 
)
inlinestatic

Definition at line 5107 of file Native.cs.

{
LIB.Z3_block_literals(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static int Z3_check ( Z3_context  a0)
inlinestatic

Definition at line 4991 of file Native.cs.

{
int r = LIB.Z3_check(a0);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static int Z3_check_and_get_model ( Z3_context  a0,
[In, Out] ref Z3_model  a1 
)
inlinestatic

Definition at line 4983 of file Native.cs.

{
int r = LIB.Z3_check_and_get_model(a0, ref a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
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 4999 of file Native.cs.

{
int r = LIB.Z3_check_assumptions(a0, a1, a2, ref a3, ref a4, ref a5, a6);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static void Z3_close_log ( )
inlinestatic

Definition at line 3637 of file Native.cs.

{
LIB.Z3_close_log();
}
static string Z3_context_to_string ( Z3_context  a0)
inlinestatic

Definition at line 5225 of file Native.cs.

{
IntPtr r = LIB.Z3_context_to_string(a0);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return Marshal.PtrToStringAnsi(r);
}
static void Z3_dec_ref ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 1546 of file Native.cs.

{
LIB.Z3_dec_ref(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static void Z3_del_config ( Z3_config  a0)
inlinestatic

Definition at line 1517 of file Native.cs.

Referenced by Context.Context().

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

Definition at line 1790 of file Native.cs.

{
LIB.Z3_del_constructor(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static void Z3_del_constructor_list ( Z3_context  a0,
Z3_constructor_list  a1 
)
inlinestatic

Definition at line 1813 of file Native.cs.

{
LIB.Z3_del_constructor_list(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static void Z3_del_context ( Z3_context  a0)
inlinestatic

Definition at line 1535 of file Native.cs.

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

Definition at line 5069 of file Native.cs.

{
LIB.Z3_del_literals(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static void Z3_del_model ( Z3_context  a0,
Z3_model  a1 
)
inlinestatic

Definition at line 5015 of file Native.cs.

{
LIB.Z3_del_model(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static void Z3_disable_literal ( Z3_context  a0,
Z3_literals  a1,
uint  a2 
)
inlinestatic

Definition at line 5100 of file Native.cs.

{
LIB.Z3_disable_literal(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static void Z3_disable_trace ( string  a0)
inlinestatic

Definition at line 3838 of file Native.cs.

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

Definition at line 3834 of file Native.cs.

{
LIB.Z3_enable_trace(a0);
}
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 5209 of file Native.cs.

{
int r = LIB.Z3_eval(a0, a1, a2, ref a3);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
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 5217 of file Native.cs.

{
int r = LIB.Z3_eval_decl(a0, a1, a2, a3, a4, ref a5);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
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 5146 of file Native.cs.

{
int r = LIB.Z3_eval_func_decl(a0, a1, a2, ref a3);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
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 3944 of file Native.cs.

{
LIB.Z3_fixedpoint_add_cover(a0, a1, a2, a3, a4);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
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 3875 of file Native.cs.

{
LIB.Z3_fixedpoint_add_fact(a0, a1, a2, a3, a4);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static void Z3_fixedpoint_add_rule ( Z3_context  a0,
Z3_fixedpoint  a1,
Z3_ast  a2,
IntPtr  a3 
)
inlinestatic

Definition at line 3868 of file Native.cs.

{
LIB.Z3_fixedpoint_add_rule(a0, a1, a2, a3);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static void Z3_fixedpoint_assert ( Z3_context  a0,
Z3_fixedpoint  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 3882 of file Native.cs.

{
LIB.Z3_fixedpoint_assert(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static void Z3_fixedpoint_dec_ref ( Z3_context  a0,
Z3_fixedpoint  a1 
)
inlinestatic

Definition at line 3861 of file Native.cs.

{
LIB.Z3_fixedpoint_dec_ref(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static Z3_ast_vector Z3_fixedpoint_from_file ( Z3_context  a0,
Z3_fixedpoint  a1,
string  a2 
)
inlinestatic

Definition at line 4028 of file Native.cs.

{
Z3_ast_vector r = LIB.Z3_fixedpoint_from_file(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast_vector Z3_fixedpoint_from_string ( Z3_context  a0,
Z3_fixedpoint  a1,
string  a2 
)
inlinestatic

Definition at line 4020 of file Native.cs.

{
Z3_ast_vector r = LIB.Z3_fixedpoint_from_string(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_fixedpoint_get_answer ( Z3_context  a0,
Z3_fixedpoint  a1 
)
inlinestatic

Definition at line 3905 of file Native.cs.

{
Z3_ast r = LIB.Z3_fixedpoint_get_answer(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast_vector Z3_fixedpoint_get_assertions ( Z3_context  a0,
Z3_fixedpoint  a1 
)
inlinestatic

Definition at line 3981 of file Native.cs.

{
Z3_ast_vector r = LIB.Z3_fixedpoint_get_assertions(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_fixedpoint_get_cover_delta ( Z3_context  a0,
Z3_fixedpoint  a1,
int  a2,
Z3_func_decl  a3 
)
inlinestatic

Definition at line 3936 of file Native.cs.

{
Z3_ast r = LIB.Z3_fixedpoint_get_cover_delta(a0, a1, a2, a3);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static string Z3_fixedpoint_get_help ( Z3_context  a0,
Z3_fixedpoint  a1 
)
inlinestatic

Definition at line 3996 of file Native.cs.

{
IntPtr r = LIB.Z3_fixedpoint_get_help(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return Marshal.PtrToStringAnsi(r);
}
static uint Z3_fixedpoint_get_num_levels ( Z3_context  a0,
Z3_fixedpoint  a1,
Z3_func_decl  a2 
)
inlinestatic

Definition at line 3928 of file Native.cs.

{
uint r = LIB.Z3_fixedpoint_get_num_levels(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_param_descrs Z3_fixedpoint_get_param_descrs ( Z3_context  a0,
Z3_fixedpoint  a1 
)
inlinestatic

Definition at line 4004 of file Native.cs.

{
Z3_param_descrs r = LIB.Z3_fixedpoint_get_param_descrs(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static string Z3_fixedpoint_get_reason_unknown ( Z3_context  a0,
Z3_fixedpoint  a1 
)
inlinestatic

Definition at line 3913 of file Native.cs.

{
IntPtr r = LIB.Z3_fixedpoint_get_reason_unknown(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return Marshal.PtrToStringAnsi(r);
}
static Z3_ast_vector Z3_fixedpoint_get_rules ( Z3_context  a0,
Z3_fixedpoint  a1 
)
inlinestatic

Definition at line 3973 of file Native.cs.

{
Z3_ast_vector r = LIB.Z3_fixedpoint_get_rules(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_stats Z3_fixedpoint_get_statistics ( Z3_context  a0,
Z3_fixedpoint  a1 
)
inlinestatic

Definition at line 3951 of file Native.cs.

{
Z3_stats r = LIB.Z3_fixedpoint_get_statistics(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static void Z3_fixedpoint_inc_ref ( Z3_context  a0,
Z3_fixedpoint  a1 
)
inlinestatic

Definition at line 3854 of file Native.cs.

{
LIB.Z3_fixedpoint_inc_ref(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static void Z3_fixedpoint_pop ( Z3_context  a0,
Z3_fixedpoint  a1 
)
inlinestatic

Definition at line 4043 of file Native.cs.

{
LIB.Z3_fixedpoint_pop(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static void Z3_fixedpoint_push ( Z3_context  a0,
Z3_fixedpoint  a1 
)
inlinestatic

Definition at line 4036 of file Native.cs.

{
LIB.Z3_fixedpoint_push(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static int Z3_fixedpoint_query ( Z3_context  a0,
Z3_fixedpoint  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 3889 of file Native.cs.

{
int r = LIB.Z3_fixedpoint_query(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static int Z3_fixedpoint_query_relations ( Z3_context  a0,
Z3_fixedpoint  a1,
uint  a2,
[In] Z3_func_decl[]  a3 
)
inlinestatic

Definition at line 3897 of file Native.cs.

{
int r = LIB.Z3_fixedpoint_query_relations(a0, a1, a2, a3);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static void Z3_fixedpoint_register_relation ( Z3_context  a0,
Z3_fixedpoint  a1,
Z3_func_decl  a2 
)
inlinestatic

Definition at line 3959 of file Native.cs.

{
LIB.Z3_fixedpoint_register_relation(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static void Z3_fixedpoint_set_params ( Z3_context  a0,
Z3_fixedpoint  a1,
Z3_params  a2 
)
inlinestatic

Definition at line 3989 of file Native.cs.

{
LIB.Z3_fixedpoint_set_params(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
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 3966 of file Native.cs.

{
LIB.Z3_fixedpoint_set_predicate_representation(a0, a1, a2, a3, a4);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static string Z3_fixedpoint_to_string ( Z3_context  a0,
Z3_fixedpoint  a1,
uint  a2,
[In] Z3_ast[]  a3 
)
inlinestatic

Definition at line 4012 of file Native.cs.

{
IntPtr r = LIB.Z3_fixedpoint_to_string(a0, a1, a2, a3);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return Marshal.PtrToStringAnsi(r);
}
static void Z3_fixedpoint_update_rule ( Z3_context  a0,
Z3_fixedpoint  a1,
Z3_ast  a2,
IntPtr  a3 
)
inlinestatic

Definition at line 3921 of file Native.cs.

{
LIB.Z3_fixedpoint_update_rule(a0, a1, a2, a3);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static Z3_ast Z3_func_decl_to_ast ( Z3_context  a0,
Z3_func_decl  a1 
)
inlinestatic

Definition at line 2890 of file Native.cs.

{
Z3_ast r = LIB.Z3_func_decl_to_ast(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static string Z3_func_decl_to_string ( Z3_context  a0,
Z3_func_decl  a1 
)
inlinestatic

Definition at line 3676 of file Native.cs.

Referenced by FuncDecl.ToString().

{
IntPtr r = LIB.Z3_func_decl_to_string(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return Marshal.PtrToStringAnsi(r);
}
static void Z3_func_entry_dec_ref ( Z3_context  a0,
Z3_func_entry  a1 
)
inlinestatic

Definition at line 3597 of file Native.cs.

{
LIB.Z3_func_entry_dec_ref(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static Z3_ast Z3_func_entry_get_arg ( Z3_context  a0,
Z3_func_entry  a1,
uint  a2 
)
inlinestatic

Definition at line 3620 of file Native.cs.

{
Z3_ast r = LIB.Z3_func_entry_get_arg(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_func_entry_get_num_args ( Z3_context  a0,
Z3_func_entry  a1 
)
inlinestatic

Definition at line 3612 of file Native.cs.

{
uint r = LIB.Z3_func_entry_get_num_args(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_func_entry_get_value ( Z3_context  a0,
Z3_func_entry  a1 
)
inlinestatic

Definition at line 3604 of file Native.cs.

{
Z3_ast r = LIB.Z3_func_entry_get_value(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static void Z3_func_entry_inc_ref ( Z3_context  a0,
Z3_func_entry  a1 
)
inlinestatic

Definition at line 3590 of file Native.cs.

{
LIB.Z3_func_entry_inc_ref(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static void Z3_func_interp_dec_ref ( Z3_context  a0,
Z3_func_interp  a1 
)
inlinestatic

Definition at line 3551 of file Native.cs.

{
LIB.Z3_func_interp_dec_ref(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static uint Z3_func_interp_get_arity ( Z3_context  a0,
Z3_func_interp  a1 
)
inlinestatic

Definition at line 3582 of file Native.cs.

{
uint r = LIB.Z3_func_interp_get_arity(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_func_interp_get_else ( Z3_context  a0,
Z3_func_interp  a1 
)
inlinestatic

Definition at line 3574 of file Native.cs.

{
Z3_ast r = LIB.Z3_func_interp_get_else(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_func_entry Z3_func_interp_get_entry ( Z3_context  a0,
Z3_func_interp  a1,
uint  a2 
)
inlinestatic

Definition at line 3566 of file Native.cs.

{
Z3_func_entry r = LIB.Z3_func_interp_get_entry(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_func_interp_get_num_entries ( Z3_context  a0,
Z3_func_interp  a1 
)
inlinestatic

Definition at line 3558 of file Native.cs.

{
uint r = LIB.Z3_func_interp_get_num_entries(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static void Z3_func_interp_inc_ref ( Z3_context  a0,
Z3_func_interp  a1 
)
inlinestatic

Definition at line 3544 of file Native.cs.

{
LIB.Z3_func_interp_inc_ref(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static Z3_ast Z3_get_algebraic_number_lower ( Z3_context  a0,
Z3_ast  a1,
uint  a2 
)
inlinestatic

Definition at line 3242 of file Native.cs.

Referenced by AlgebraicNum.ToLower().

{
Z3_ast r = LIB.Z3_get_algebraic_number_lower(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_get_algebraic_number_upper ( Z3_context  a0,
Z3_ast  a1,
uint  a2 
)
inlinestatic

Definition at line 3250 of file Native.cs.

Referenced by AlgebraicNum.ToUpper().

{
Z3_ast r = LIB.Z3_get_algebraic_number_upper(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_get_app_arg ( Z3_context  a0,
Z3_app  a1,
uint  a2 
)
inlinestatic

Definition at line 3058 of file Native.cs.

{
Z3_ast r = LIB.Z3_get_app_arg(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_func_decl Z3_get_app_decl ( Z3_context  a0,
Z3_app  a1 
)
inlinestatic

Definition at line 3042 of file Native.cs.

{
Z3_func_decl r = LIB.Z3_get_app_decl(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_app_num_args ( Z3_context  a0,
Z3_app  a1 
)
inlinestatic

Definition at line 3050 of file Native.cs.

{
uint r = LIB.Z3_get_app_num_args(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_arity ( Z3_context  a0,
Z3_func_decl  a1 
)
inlinestatic

Definition at line 2938 of file Native.cs.

{
uint r = LIB.Z3_get_arity(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_sort Z3_get_array_sort_domain ( Z3_context  a0,
Z3_sort  a1 
)
inlinestatic

Definition at line 2802 of file Native.cs.

{
Z3_sort r = LIB.Z3_get_array_sort_domain(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_sort Z3_get_array_sort_range ( Z3_context  a0,
Z3_sort  a1 
)
inlinestatic

Definition at line 2810 of file Native.cs.

{
Z3_sort r = LIB.Z3_get_array_sort_range(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
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 5162 of file Native.cs.

{
LIB.Z3_get_array_value(a0, a1, a2, a3, a4, a5, ref a6);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static Z3_func_decl Z3_get_as_array_func_decl ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 3536 of file Native.cs.

Referenced by Model.FuncInterp().

{
Z3_func_decl r = LIB.Z3_get_as_array_func_decl(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_ast_hash ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 3082 of file Native.cs.

Referenced by AST.GetHashCode().

{
uint r = LIB.Z3_get_ast_hash(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_ast_id ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 3074 of file Native.cs.

{
uint r = LIB.Z3_get_ast_id(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_ast_kind ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 3114 of file Native.cs.

{
uint r = LIB.Z3_get_ast_kind(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_bool_value ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 3106 of file Native.cs.

{
uint r = LIB.Z3_get_bool_value(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_bv_sort_size ( Z3_context  a0,
Z3_sort  a1 
)
inlinestatic

Definition at line 2786 of file Native.cs.

{
uint r = LIB.Z3_get_bv_sort_size(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_get_context_assignment ( Z3_context  a0)
inlinestatic

Definition at line 5241 of file Native.cs.

{
Z3_ast r = LIB.Z3_get_context_assignment(a0);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_func_decl Z3_get_datatype_sort_constructor ( Z3_context  a0,
Z3_sort  a1,
uint  a2 
)
inlinestatic

Definition at line 2850 of file Native.cs.

{
Z3_func_decl r = LIB.Z3_get_datatype_sort_constructor(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_func_decl Z3_get_datatype_sort_constructor_accessor ( Z3_context  a0,
Z3_sort  a1,
uint  a2,
uint  a3 
)
inlinestatic

Definition at line 2866 of file Native.cs.

{
Z3_func_decl r = LIB.Z3_get_datatype_sort_constructor_accessor(a0, a1, a2, a3);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_datatype_sort_num_constructors ( Z3_context  a0,
Z3_sort  a1 
)
inlinestatic

Definition at line 2842 of file Native.cs.

{
uint r = LIB.Z3_get_datatype_sort_num_constructors(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_func_decl Z3_get_datatype_sort_recognizer ( Z3_context  a0,
Z3_sort  a1,
uint  a2 
)
inlinestatic

Definition at line 2858 of file Native.cs.

{
Z3_func_decl r = LIB.Z3_get_datatype_sort_recognizer(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_get_decl_ast_parameter ( Z3_context  a0,
Z3_func_decl  a1,
uint  a2 
)
inlinestatic

Definition at line 3010 of file Native.cs.

{
Z3_ast r = LIB.Z3_get_decl_ast_parameter(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static double Z3_get_decl_double_parameter ( Z3_context  a0,
Z3_func_decl  a1,
uint  a2 
)
inlinestatic

Definition at line 2986 of file Native.cs.

{
double r = LIB.Z3_get_decl_double_parameter(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_func_decl Z3_get_decl_func_decl_parameter ( Z3_context  a0,
Z3_func_decl  a1,
uint  a2 
)
inlinestatic

Definition at line 3018 of file Native.cs.

{
Z3_func_decl r = LIB.Z3_get_decl_func_decl_parameter(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static int Z3_get_decl_int_parameter ( Z3_context  a0,
Z3_func_decl  a1,
uint  a2 
)
inlinestatic

Definition at line 2978 of file Native.cs.

{
int r = LIB.Z3_get_decl_int_parameter(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_decl_kind ( Z3_context  a0,
Z3_func_decl  a1 
)
inlinestatic

Definition at line 2922 of file Native.cs.

{
uint r = LIB.Z3_get_decl_kind(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static IntPtr Z3_get_decl_name ( Z3_context  a0,
Z3_func_decl  a1 
)
inlinestatic

Definition at line 2914 of file Native.cs.

{
IntPtr r = LIB.Z3_get_decl_name(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_decl_num_parameters ( Z3_context  a0,
Z3_func_decl  a1 
)
inlinestatic

Definition at line 2962 of file Native.cs.

{
uint r = LIB.Z3_get_decl_num_parameters(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_decl_parameter_kind ( Z3_context  a0,
Z3_func_decl  a1,
uint  a2 
)
inlinestatic

Definition at line 2970 of file Native.cs.

{
uint r = LIB.Z3_get_decl_parameter_kind(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static string Z3_get_decl_rational_parameter ( Z3_context  a0,
Z3_func_decl  a1,
uint  a2 
)
inlinestatic

Definition at line 3026 of file Native.cs.

{
IntPtr r = LIB.Z3_get_decl_rational_parameter(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return Marshal.PtrToStringAnsi(r);
}
static Z3_sort Z3_get_decl_sort_parameter ( Z3_context  a0,
Z3_func_decl  a1,
uint  a2 
)
inlinestatic

Definition at line 3002 of file Native.cs.

{
Z3_sort r = LIB.Z3_get_decl_sort_parameter(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static IntPtr Z3_get_decl_symbol_parameter ( Z3_context  a0,
Z3_func_decl  a1,
uint  a2 
)
inlinestatic

Definition at line 2994 of file Native.cs.

{
IntPtr r = LIB.Z3_get_decl_symbol_parameter(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_get_denominator ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 3186 of file Native.cs.

{
Z3_ast r = LIB.Z3_get_denominator(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_sort Z3_get_domain ( Z3_context  a0,
Z3_func_decl  a1,
uint  a2 
)
inlinestatic

Definition at line 2946 of file Native.cs.

{
Z3_sort r = LIB.Z3_get_domain(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_domain_size ( Z3_context  a0,
Z3_func_decl  a1 
)
inlinestatic

Definition at line 2930 of file Native.cs.

{
uint r = LIB.Z3_get_domain_size(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_error_code ( Z3_context  a0)
inlinestatic

Definition at line 3802 of file Native.cs.

{
uint r = LIB.Z3_get_error_code(a0);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static string Z3_get_error_msg ( uint  a0)
inlinestatic

Definition at line 3817 of file Native.cs.

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

Definition at line 3822 of file Native.cs.

{
IntPtr r = LIB.Z3_get_error_msg_ex(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return Marshal.PtrToStringAnsi(r);
}
static int Z3_get_finite_domain_sort_size ( Z3_context  a0,
Z3_sort  a1,
[In, Out] ref UInt64  a2 
)
inlinestatic

Definition at line 2794 of file Native.cs.

{
int r = LIB.Z3_get_finite_domain_sort_size(a0, a1, ref a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_func_decl_id ( Z3_context  a0,
Z3_func_decl  a1 
)
inlinestatic

Definition at line 2906 of file Native.cs.

{
uint r = LIB.Z3_get_func_decl_id(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_literals Z3_get_guessed_literals ( Z3_context  a0)
inlinestatic

Definition at line 5061 of file Native.cs.

{
Z3_literals r = LIB.Z3_get_guessed_literals(a0);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_implied_equalities ( Z3_context  a0,
uint  a1,
[In] Z3_ast[]  a2,
[Out] uint[]  a3 
)
inlinestatic

Definition at line 5007 of file Native.cs.

{
uint r = LIB.Z3_get_implied_equalities(a0, a1, a2, a3);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_index_value ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 3282 of file Native.cs.

{
uint r = LIB.Z3_get_index_value(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static IntPtr Z3_get_label_symbol ( Z3_context  a0,
Z3_literals  a1,
uint  a2 
)
inlinestatic

Definition at line 5084 of file Native.cs.

{
IntPtr r = LIB.Z3_get_label_symbol(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_get_literal ( Z3_context  a0,
Z3_literals  a1,
uint  a2 
)
inlinestatic

Definition at line 5092 of file Native.cs.

{
Z3_ast r = LIB.Z3_get_literal(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_func_decl Z3_get_model_constant ( Z3_context  a0,
Z3_model  a1,
uint  a2 
)
inlinestatic

Definition at line 5122 of file Native.cs.

{
Z3_func_decl r = LIB.Z3_get_model_constant(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_func_decl Z3_get_model_func_decl ( Z3_context  a0,
Z3_model  a1,
uint  a2 
)
inlinestatic

Definition at line 5138 of file Native.cs.

{
Z3_func_decl r = LIB.Z3_get_model_func_decl(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_get_model_func_else ( Z3_context  a0,
Z3_model  a1,
uint  a2 
)
inlinestatic

Definition at line 5169 of file Native.cs.

{
Z3_ast r = LIB.Z3_get_model_func_else(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_get_model_func_entry_arg ( Z3_context  a0,
Z3_model  a1,
uint  a2,
uint  a3,
uint  a4 
)
inlinestatic

Definition at line 5193 of file Native.cs.

{
Z3_ast r = LIB.Z3_get_model_func_entry_arg(a0, a1, a2, a3, a4);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_model_func_entry_num_args ( Z3_context  a0,
Z3_model  a1,
uint  a2,
uint  a3 
)
inlinestatic

Definition at line 5185 of file Native.cs.

{
uint r = LIB.Z3_get_model_func_entry_num_args(a0, a1, a2, a3);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_get_model_func_entry_value ( Z3_context  a0,
Z3_model  a1,
uint  a2,
uint  a3 
)
inlinestatic

Definition at line 5201 of file Native.cs.

{
Z3_ast r = LIB.Z3_get_model_func_entry_value(a0, a1, a2, a3);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_model_func_num_entries ( Z3_context  a0,
Z3_model  a1,
uint  a2 
)
inlinestatic

Definition at line 5177 of file Native.cs.

{
uint r = LIB.Z3_get_model_func_num_entries(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_model_num_constants ( Z3_context  a0,
Z3_model  a1 
)
inlinestatic

Definition at line 5114 of file Native.cs.

{
uint r = LIB.Z3_get_model_num_constants(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_model_num_funcs ( Z3_context  a0,
Z3_model  a1 
)
inlinestatic

Definition at line 5130 of file Native.cs.

{
uint r = LIB.Z3_get_model_num_funcs(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_num_literals ( Z3_context  a0,
Z3_literals  a1 
)
inlinestatic

Definition at line 5076 of file Native.cs.

{
uint r = LIB.Z3_get_num_literals(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_num_probes ( Z3_context  a0)
inlinestatic

Definition at line 4560 of file Native.cs.

{
uint r = LIB.Z3_get_num_probes(a0);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_num_scopes ( Z3_context  a0)
inlinestatic

Definition at line 4961 of file Native.cs.

{
uint r = LIB.Z3_get_num_scopes(a0);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_num_tactics ( Z3_context  a0)
inlinestatic

Definition at line 4544 of file Native.cs.

{
uint r = LIB.Z3_get_num_tactics(a0);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static string Z3_get_numeral_decimal_string ( Z3_context  a0,
Z3_ast  a1,
uint  a2 
)
inlinestatic

Definition at line 3170 of file Native.cs.

Referenced by AlgebraicNum.ToDecimal(), and RatNum.ToDecimalString().

{
IntPtr r = LIB.Z3_get_numeral_decimal_string(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return Marshal.PtrToStringAnsi(r);
}
static int Z3_get_numeral_int ( Z3_context  a0,
Z3_ast  a1,
[In, Out] ref int  a2 
)
inlinestatic

Definition at line 3202 of file Native.cs.

{
int r = LIB.Z3_get_numeral_int(a0, a1, ref a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static int Z3_get_numeral_int64 ( Z3_context  a0,
Z3_ast  a1,
[In, Out] ref Int64  a2 
)
inlinestatic

Definition at line 3226 of file Native.cs.

{
int r = LIB.Z3_get_numeral_int64(a0, a1, ref a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static int Z3_get_numeral_rational_int64 ( Z3_context  a0,
Z3_ast  a1,
[In, Out] ref Int64  a2,
[In, Out] ref Int64  a3 
)
inlinestatic

Definition at line 3234 of file Native.cs.

{
int r = LIB.Z3_get_numeral_rational_int64(a0, a1, ref a2, ref a3);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static int Z3_get_numeral_small ( Z3_context  a0,
Z3_ast  a1,
[In, Out] ref Int64  a2,
[In, Out] ref Int64  a3 
)
inlinestatic

Definition at line 3194 of file Native.cs.

{
int r = LIB.Z3_get_numeral_small(a0, a1, ref a2, ref a3);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static string Z3_get_numeral_string ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 3162 of file Native.cs.

Referenced by IntNum.ToString(), RatNum.ToString(), and BitVecNum.ToString().

{
IntPtr r = LIB.Z3_get_numeral_string(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return Marshal.PtrToStringAnsi(r);
}
static int Z3_get_numeral_uint ( Z3_context  a0,
Z3_ast  a1,
[In, Out] ref uint  a2 
)
inlinestatic

Definition at line 3210 of file Native.cs.

{
int r = LIB.Z3_get_numeral_uint(a0, a1, ref a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static int Z3_get_numeral_uint64 ( Z3_context  a0,
Z3_ast  a1,
[In, Out] ref UInt64  a2 
)
inlinestatic

Definition at line 3218 of file Native.cs.

{
int r = LIB.Z3_get_numeral_uint64(a0, a1, ref a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_get_numerator ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 3178 of file Native.cs.

{
Z3_ast r = LIB.Z3_get_numerator(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static int Z3_get_param_value ( Z3_context  a0,
string  a1,
out IntPtr  a2 
)
inlinestatic

Definition at line 1560 of file Native.cs.

Referenced by Context.GetParamValue().

{
int r = LIB.Z3_get_param_value(a0, a1, out a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_get_pattern ( Z3_context  a0,
Z3_pattern  a1,
uint  a2 
)
inlinestatic

Definition at line 3274 of file Native.cs.

{
Z3_ast r = LIB.Z3_get_pattern(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_pattern_num_terms ( Z3_context  a0,
Z3_pattern  a1 
)
inlinestatic

Definition at line 3266 of file Native.cs.

{
uint r = LIB.Z3_get_pattern_num_terms(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static string Z3_get_probe_name ( Z3_context  a0,
uint  a1 
)
inlinestatic

Definition at line 4568 of file Native.cs.

{
IntPtr r = LIB.Z3_get_probe_name(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return Marshal.PtrToStringAnsi(r);
}
static Z3_ast Z3_get_quantifier_body ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 3362 of file Native.cs.

{
Z3_ast r = LIB.Z3_get_quantifier_body(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static IntPtr Z3_get_quantifier_bound_name ( Z3_context  a0,
Z3_ast  a1,
uint  a2 
)
inlinestatic

Definition at line 3346 of file Native.cs.

{
IntPtr r = LIB.Z3_get_quantifier_bound_name(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_sort Z3_get_quantifier_bound_sort ( Z3_context  a0,
Z3_ast  a1,
uint  a2 
)
inlinestatic

Definition at line 3354 of file Native.cs.

{
Z3_sort r = LIB.Z3_get_quantifier_bound_sort(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_get_quantifier_no_pattern_ast ( Z3_context  a0,
Z3_ast  a1,
uint  a2 
)
inlinestatic

Definition at line 3330 of file Native.cs.

{
Z3_ast r = LIB.Z3_get_quantifier_no_pattern_ast(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_quantifier_num_bound ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 3338 of file Native.cs.

{
uint r = LIB.Z3_get_quantifier_num_bound(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_quantifier_num_no_patterns ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 3322 of file Native.cs.

{
uint r = LIB.Z3_get_quantifier_num_no_patterns(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_quantifier_num_patterns ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 3306 of file Native.cs.

{
uint r = LIB.Z3_get_quantifier_num_patterns(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_pattern Z3_get_quantifier_pattern_ast ( Z3_context  a0,
Z3_ast  a1,
uint  a2 
)
inlinestatic

Definition at line 3314 of file Native.cs.

{
Z3_pattern r = LIB.Z3_get_quantifier_pattern_ast(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_quantifier_weight ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 3298 of file Native.cs.

{
uint r = LIB.Z3_get_quantifier_weight(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_sort Z3_get_range ( Z3_context  a0,
Z3_func_decl  a1 
)
inlinestatic

Definition at line 2954 of file Native.cs.

Referenced by Model.ConstInterp(), and Model.FuncInterp().

{
Z3_sort r = LIB.Z3_get_range(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_relation_arity ( Z3_context  a0,
Z3_sort  a1 
)
inlinestatic

Definition at line 2874 of file Native.cs.

{
uint r = LIB.Z3_get_relation_arity(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_sort Z3_get_relation_column ( Z3_context  a0,
Z3_sort  a1,
uint  a2 
)
inlinestatic

Definition at line 2882 of file Native.cs.

{
Z3_sort r = LIB.Z3_get_relation_column(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_literals Z3_get_relevant_labels ( Z3_context  a0)
inlinestatic

Definition at line 5045 of file Native.cs.

{
Z3_literals r = LIB.Z3_get_relevant_labels(a0);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_literals Z3_get_relevant_literals ( Z3_context  a0)
inlinestatic

Definition at line 5053 of file Native.cs.

{
Z3_literals r = LIB.Z3_get_relevant_literals(a0);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_search_failure ( Z3_context  a0)
inlinestatic

Definition at line 5029 of file Native.cs.

{
uint r = LIB.Z3_get_search_failure(a0);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_get_smtlib_assumption ( Z3_context  a0,
uint  a1 
)
inlinestatic

Definition at line 3754 of file Native.cs.

{
Z3_ast r = LIB.Z3_get_smtlib_assumption(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_func_decl Z3_get_smtlib_decl ( Z3_context  a0,
uint  a1 
)
inlinestatic

Definition at line 3770 of file Native.cs.

{
Z3_func_decl r = LIB.Z3_get_smtlib_decl(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static string Z3_get_smtlib_error ( Z3_context  a0)
inlinestatic

Definition at line 3794 of file Native.cs.

{
IntPtr r = LIB.Z3_get_smtlib_error(a0);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return Marshal.PtrToStringAnsi(r);
}
static Z3_ast Z3_get_smtlib_formula ( Z3_context  a0,
uint  a1 
)
inlinestatic

Definition at line 3738 of file Native.cs.

{
Z3_ast r = LIB.Z3_get_smtlib_formula(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_smtlib_num_assumptions ( Z3_context  a0)
inlinestatic

Definition at line 3746 of file Native.cs.

{
uint r = LIB.Z3_get_smtlib_num_assumptions(a0);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_smtlib_num_decls ( Z3_context  a0)
inlinestatic

Definition at line 3762 of file Native.cs.

{
uint r = LIB.Z3_get_smtlib_num_decls(a0);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_smtlib_num_formulas ( Z3_context  a0)
inlinestatic

Definition at line 3730 of file Native.cs.

{
uint r = LIB.Z3_get_smtlib_num_formulas(a0);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_smtlib_num_sorts ( Z3_context  a0)
inlinestatic

Definition at line 3778 of file Native.cs.

{
uint r = LIB.Z3_get_smtlib_num_sorts(a0);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_sort Z3_get_smtlib_sort ( Z3_context  a0,
uint  a1 
)
inlinestatic

Definition at line 3786 of file Native.cs.

{
Z3_sort r = LIB.Z3_get_smtlib_sort(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_sort Z3_get_sort ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 3090 of file Native.cs.

{
Z3_sort r = LIB.Z3_get_sort(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_sort_id ( Z3_context  a0,
Z3_sort  a1 
)
inlinestatic

Definition at line 2754 of file Native.cs.

{
uint r = LIB.Z3_get_sort_id(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_sort_kind ( Z3_context  a0,
Z3_sort  a1 
)
inlinestatic

Definition at line 2778 of file Native.cs.

Referenced by Model.ConstInterp(), and Model.FuncInterp().

{
uint r = LIB.Z3_get_sort_kind(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static IntPtr Z3_get_sort_name ( Z3_context  a0,
Z3_sort  a1 
)
inlinestatic

Definition at line 2746 of file Native.cs.

{
IntPtr r = LIB.Z3_get_sort_name(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static int Z3_get_symbol_int ( Z3_context  a0,
IntPtr  a1 
)
inlinestatic

Definition at line 2730 of file Native.cs.

{
int r = LIB.Z3_get_symbol_int(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_symbol_kind ( Z3_context  a0,
IntPtr  a1 
)
inlinestatic

Definition at line 2722 of file Native.cs.

{
uint r = LIB.Z3_get_symbol_kind(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static string Z3_get_symbol_string ( Z3_context  a0,
IntPtr  a1 
)
inlinestatic

Definition at line 2738 of file Native.cs.

{
IntPtr r = LIB.Z3_get_symbol_string(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return Marshal.PtrToStringAnsi(r);
}
static string Z3_get_tactic_name ( Z3_context  a0,
uint  a1 
)
inlinestatic

Definition at line 4552 of file Native.cs.

{
IntPtr r = LIB.Z3_get_tactic_name(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return Marshal.PtrToStringAnsi(r);
}
static Z3_func_decl Z3_get_tuple_sort_field_decl ( Z3_context  a0,
Z3_sort  a1,
uint  a2 
)
inlinestatic

Definition at line 2834 of file Native.cs.

{
Z3_func_decl r = LIB.Z3_get_tuple_sort_field_decl(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_func_decl Z3_get_tuple_sort_mk_decl ( Z3_context  a0,
Z3_sort  a1 
)
inlinestatic

Definition at line 2818 of file Native.cs.

{
Z3_func_decl r = LIB.Z3_get_tuple_sort_mk_decl(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_get_tuple_sort_num_fields ( Z3_context  a0,
Z3_sort  a1 
)
inlinestatic

Definition at line 2826 of file Native.cs.

{
uint r = LIB.Z3_get_tuple_sort_num_fields(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
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 
)
inlinestatic

Definition at line 3830 of file Native.cs.

{
LIB.Z3_get_version(ref a0, ref a1, ref a2, ref a3);
}
static void Z3_goal_assert ( Z3_context  a0,
Z3_goal  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 4238 of file Native.cs.

Referenced by Goal.Assert().

{
LIB.Z3_goal_assert(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static void Z3_goal_dec_ref ( Z3_context  a0,
Z3_goal  a1 
)
inlinestatic

Definition at line 4223 of file Native.cs.

{
LIB.Z3_goal_dec_ref(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static uint Z3_goal_depth ( Z3_context  a0,
Z3_goal  a1 
)
inlinestatic

Definition at line 4253 of file Native.cs.

{
uint r = LIB.Z3_goal_depth(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_goal_formula ( Z3_context  a0,
Z3_goal  a1,
uint  a2 
)
inlinestatic

Definition at line 4276 of file Native.cs.

{
Z3_ast r = LIB.Z3_goal_formula(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static void Z3_goal_inc_ref ( Z3_context  a0,
Z3_goal  a1 
)
inlinestatic

Definition at line 4216 of file Native.cs.

{
LIB.Z3_goal_inc_ref(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static int Z3_goal_inconsistent ( Z3_context  a0,
Z3_goal  a1 
)
inlinestatic

Definition at line 4245 of file Native.cs.

{
int r = LIB.Z3_goal_inconsistent(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static int Z3_goal_is_decided_sat ( Z3_context  a0,
Z3_goal  a1 
)
inlinestatic

Definition at line 4292 of file Native.cs.

{
int r = LIB.Z3_goal_is_decided_sat(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static int Z3_goal_is_decided_unsat ( Z3_context  a0,
Z3_goal  a1 
)
inlinestatic

Definition at line 4300 of file Native.cs.

{
int r = LIB.Z3_goal_is_decided_unsat(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_goal_num_exprs ( Z3_context  a0,
Z3_goal  a1 
)
inlinestatic

Definition at line 4284 of file Native.cs.

{
uint r = LIB.Z3_goal_num_exprs(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static uint Z3_goal_precision ( Z3_context  a0,
Z3_goal  a1 
)
inlinestatic

Definition at line 4230 of file Native.cs.

{
uint r = LIB.Z3_goal_precision(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static void Z3_goal_reset ( Z3_context  a0,
Z3_goal  a1 
)
inlinestatic

Definition at line 4261 of file Native.cs.

Referenced by Goal.Reset().

{
LIB.Z3_goal_reset(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static uint Z3_goal_size ( Z3_context  a0,
Z3_goal  a1 
)
inlinestatic

Definition at line 4268 of file Native.cs.

{
uint r = LIB.Z3_goal_size(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static string Z3_goal_to_string ( Z3_context  a0,
Z3_goal  a1 
)
inlinestatic

Definition at line 4316 of file Native.cs.

Referenced by Goal.ToString().

{
IntPtr r = LIB.Z3_goal_to_string(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return Marshal.PtrToStringAnsi(r);
}
static Z3_goal Z3_goal_translate ( Z3_context  a0,
Z3_goal  a1,
Z3_context  a2 
)
inlinestatic

Definition at line 4308 of file Native.cs.

Referenced by Goal.Translate().

{
Z3_goal r = LIB.Z3_goal_translate(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static void Z3_inc_ref ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 1539 of file Native.cs.

{
LIB.Z3_inc_ref(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static void Z3_interrupt ( Z3_context  a0)
inlinestatic

Definition at line 1568 of file Native.cs.

Referenced by Context.Interrupt().

{
LIB.Z3_interrupt(a0);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
}
static int Z3_is_algebraic_number ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 3138 of file Native.cs.

{
int r = LIB.Z3_is_algebraic_number(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static int Z3_is_app ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 3122 of file Native.cs.

{
int r = LIB.Z3_is_app(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static int Z3_is_array_value ( Z3_context  a0,
Z3_model  a1,
Z3_ast  a2,
[In, Out] ref uint  a3 
)
inlinestatic

Definition at line 5154 of file Native.cs.

{
int r = LIB.Z3_is_array_value(a0, a1, a2, ref a3);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static int Z3_is_as_array ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 3528 of file Native.cs.

Referenced by Model.FuncInterp().

{
int r = LIB.Z3_is_as_array(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static int Z3_is_eq_ast ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 3066 of file Native.cs.

Referenced by AST.operator==().

{
int r = LIB.Z3_is_eq_ast(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static int Z3_is_eq_func_decl ( Z3_context  a0,
Z3_func_decl  a1,
Z3_func_decl  a2 
)
inlinestatic

Definition at line 2898 of file Native.cs.

Referenced by FuncDecl.operator==().

{
int r = LIB.Z3_is_eq_func_decl(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static int Z3_is_eq_sort ( Z3_context  a0,
Z3_sort  a1,
Z3_sort  a2 
)
inlinestatic

Definition at line 2770 of file Native.cs.

Referenced by Sort.operator==().

{
int r = LIB.Z3_is_eq_sort(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static int Z3_is_numeral_ast ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 3130 of file Native.cs.

{
int r = LIB.Z3_is_numeral_ast(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static int Z3_is_quantifier_forall ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 3290 of file Native.cs.

{
int r = LIB.Z3_is_quantifier_forall(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static int Z3_is_well_sorted ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 3098 of file Native.cs.

{
int r = LIB.Z3_is_well_sorted(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_mk_add ( Z3_context  a0,
uint  a1,
[In] Z3_ast[]  a2 
)
inlinestatic

Definition at line 1962 of file Native.cs.

Referenced by Context.MkAdd().

{
Z3_ast r = LIB.Z3_mk_add(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_mk_and ( Z3_context  a0,
uint  a1,
[In] Z3_ast[]  a2 
)
inlinestatic

Definition at line 1946 of file Native.cs.

Referenced by Context.MkAnd().

{
Z3_ast r = LIB.Z3_mk_and(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_mk_app ( Z3_context  a0,
Z3_func_decl  a1,
uint  a2,
[In] Z3_ast[]  a3 
)
inlinestatic

Definition at line 1842 of file Native.cs.

{
Z3_ast r = LIB.Z3_mk_app(a0, a1, a2, a3);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_mk_array_default ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 2498 of file Native.cs.

Referenced by Context.MkTermArray().

{
Z3_ast r = LIB.Z3_mk_array_default(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_sort Z3_mk_array_sort ( Z3_context  a0,
Z3_sort  a1,
Z3_sort  a2 
)
inlinestatic

Definition at line 1750 of file Native.cs.

{
Z3_sort r = LIB.Z3_mk_array_sort(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast_map Z3_mk_ast_map ( Z3_context  a0)
inlinestatic

Definition at line 4125 of file Native.cs.

{
Z3_ast_map r = LIB.Z3_mk_ast_map(a0);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast_vector Z3_mk_ast_vector ( Z3_context  a0)
inlinestatic

Definition at line 4050 of file Native.cs.

{
Z3_ast_vector r = LIB.Z3_mk_ast_vector(a0);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_sort Z3_mk_bool_sort ( Z3_context  a0)
inlinestatic

Definition at line 1710 of file Native.cs.

{
Z3_sort r = LIB.Z3_mk_bool_sort(a0);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_mk_bound ( Z3_context  a0,
uint  a1,
Z3_sort  a2 
)
inlinestatic

Definition at line 2650 of file Native.cs.

Referenced by Context.MkBound().

{
Z3_ast r = LIB.Z3_mk_bound(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_mk_bv2int ( Z3_context  a0,
Z3_ast  a1,
int  a2 
)
inlinestatic

Definition at line 2394 of file Native.cs.

Referenced by Context.MkBV2Int().

{
Z3_ast r = LIB.Z3_mk_bv2int(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_sort Z3_mk_bv_sort ( Z3_context  a0,
uint  a1 
)
inlinestatic

Definition at line 1734 of file Native.cs.

{
Z3_sort r = LIB.Z3_mk_bv_sort(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_mk_bvadd ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 2162 of file Native.cs.

Referenced by Context.MkBVAdd().

{
Z3_ast r = LIB.Z3_mk_bvadd(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_mk_bvadd_no_overflow ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2,
int  a3 
)
inlinestatic

Definition at line 2402 of file Native.cs.

Referenced by Context.MkBVAddNoOverflow().

{
Z3_ast r = LIB.Z3_mk_bvadd_no_overflow(a0, a1, a2, a3);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_mk_bvadd_no_underflow ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 2410 of file Native.cs.

Referenced by Context.MkBVAddNoUnderflow().

{
Z3_ast r = LIB.Z3_mk_bvadd_no_underflow(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_mk_bvand ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 2106 of file Native.cs.

Referenced by Context.MkBVAND().

{
Z3_ast r = LIB.Z3_mk_bvand(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_mk_bvashr ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 2346 of file Native.cs.

Referenced by Context.MkBVASHR().

{
Z3_ast r = LIB.Z3_mk_bvashr(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_mk_bvlshr ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 2338 of file Native.cs.

Referenced by Context.MkBVLSHR().

{
Z3_ast r = LIB.Z3_mk_bvlshr(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_mk_bvmul ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 2178 of file Native.cs.

Referenced by Context.MkBVMul().

{
Z3_ast r = LIB.Z3_mk_bvmul(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_mk_bvmul_no_overflow ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2,
int  a3 
)
inlinestatic

Definition at line 2450 of file Native.cs.

Referenced by Context.MkBVMulNoOverflow().

{
Z3_ast r = LIB.Z3_mk_bvmul_no_overflow(a0, a1, a2, a3);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_mk_bvmul_no_underflow ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 2458 of file Native.cs.

Referenced by Context.MkBVMulNoUnderflow().

{
Z3_ast r = LIB.Z3_mk_bvmul_no_underflow(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_mk_bvnand ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 2130 of file Native.cs.

Referenced by Context.MkBVNAND().

{
Z3_ast r = LIB.Z3_mk_bvnand(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_mk_bvneg ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 2154 of file Native.cs.

Referenced by Context.MkBVNeg().

{
Z3_ast r = LIB.Z3_mk_bvneg(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_mk_bvneg_no_overflow ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 2442 of file Native.cs.

Referenced by Context.MkBVNegNoOverflow().

{
Z3_ast r = LIB.Z3_mk_bvneg_no_overflow(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_mk_bvnor ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 2138 of file Native.cs.

Referenced by Context.MkBVNOR().

{
Z3_ast r = LIB.Z3_mk_bvnor(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_mk_bvnot ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 2082 of file Native.cs.

Referenced by Context.MkBVNot().

{
Z3_ast r = LIB.Z3_mk_bvnot(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_mk_bvor ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 2114 of file Native.cs.

Referenced by Context.MkBVOR().

{
Z3_ast r = LIB.Z3_mk_bvor(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_mk_bvredand ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 2090 of file Native.cs.

Referenced by Context.MkBVRedAND().

{
Z3_ast r = LIB.Z3_mk_bvredand(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_mk_bvredor ( Z3_context  a0,
Z3_ast  a1 
)
inlinestatic

Definition at line 2098 of file Native.cs.

Referenced by Context.MkBVRedOR().

{
Z3_ast r = LIB.Z3_mk_bvredor(a0, a1);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_mk_bvsdiv ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 2194 of file Native.cs.

Referenced by Context.MkBVSDiv().

{
Z3_ast r = LIB.Z3_mk_bvsdiv(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_mk_bvsdiv_no_overflow ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 2434 of file Native.cs.

Referenced by Context.MkBVSDivNoOverflow().

{
Z3_ast r = LIB.Z3_mk_bvsdiv_no_overflow(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_mk_bvsge ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 2266 of file Native.cs.

Referenced by Context.MkBVSGE().

{
Z3_ast r = LIB.Z3_mk_bvsge(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_mk_bvsgt ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 2282 of file Native.cs.

Referenced by Context.MkBVSGT().

{
Z3_ast r = LIB.Z3_mk_bvsgt(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_mk_bvshl ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 2330 of file Native.cs.

Referenced by Context.MkBVSHL().

{
Z3_ast r = LIB.Z3_mk_bvshl(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_mk_bvsle ( Z3_context  a0,
Z3_ast  a1,
Z3_ast  a2 
)
inlinestatic

Definition at line 2250 of file Native.cs.

Referenced by Context.MkBVSLE().

{
Z3_ast r = LIB.Z3_mk_bvsle(a0, a1, a2);
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
if (err != Z3_error_code.Z3_OK)
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
return r;
}
static Z3_ast Z3_mk_bvslt ( Z3_context  a0,