Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Native.cs
Go to the documentation of this file.
1 // Automatically generated file
2 using System;
3 using System.Collections.Generic;
4 using System.Text;
5 using System.Runtime.InteropServices;
6 
7 #pragma warning disable 1591
8 
9 namespace Microsoft.Z3
10 {
11  using Z3_config = System.IntPtr;
12  using Z3_context = System.IntPtr;
13  using Z3_ast = System.IntPtr;
14  using Z3_app = System.IntPtr;
15  using Z3_sort = System.IntPtr;
16  using Z3_func_decl = System.IntPtr;
17  using Z3_pattern = System.IntPtr;
18  using Z3_model = System.IntPtr;
19  using Z3_literals = System.IntPtr;
20  using Z3_constructor = System.IntPtr;
21  using Z3_constructor_list = System.IntPtr;
22  using Z3_theory = System.IntPtr;
23  using Z3_theory_data = System.IntPtr;
24  using Z3_solver = System.IntPtr;
25  using Z3_goal = System.IntPtr;
26  using Z3_tactic = System.IntPtr;
27  using Z3_params = System.IntPtr;
28  using Z3_probe = System.IntPtr;
29  using Z3_stats = System.IntPtr;
30  using Z3_ast_vector = System.IntPtr;
31  using Z3_ast_map = System.IntPtr;
32  using Z3_apply_result = System.IntPtr;
33  using Z3_func_interp = System.IntPtr;
34  using Z3_func_entry = System.IntPtr;
35  using Z3_fixedpoint = System.IntPtr;
36  using Z3_param_descrs = System.IntPtr;
37 
38  public class Native
39  {
40 
41  [UnmanagedFunctionPointer(CallingConvention.Cdecl)]
42  public delegate void Z3_error_handler(Z3_context c, Z3_error_code e);
43 
44  public unsafe class LIB
45  {
46  const string Z3_DLL_NAME = "libz3.dll";
47 
48  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
49  public extern static void Z3_set_error_handler(Z3_context a0, Z3_error_handler a1);
50 
51  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
52  public extern static Z3_config Z3_mk_config();
53 
54  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
55  public extern static void Z3_del_config(Z3_config a0);
56 
57  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
58  public extern static void Z3_set_param_value(Z3_config a0, string a1, string a2);
59 
60  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
61  public extern static Z3_context Z3_mk_context(Z3_config a0);
62 
63  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
64  public extern static Z3_context Z3_mk_context_rc(Z3_config a0);
65 
66  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
67  public extern static void Z3_del_context(Z3_context a0);
68 
69  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
70  public extern static void Z3_inc_ref(Z3_context a0, Z3_ast a1);
71 
72  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
73  public extern static void Z3_dec_ref(Z3_context a0, Z3_ast a1);
74 
75  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
76  public extern static void Z3_update_param_value(Z3_context a0, string a1, string a2);
77 
78  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
79  public extern static int Z3_get_param_value(Z3_context a0, string a1, out IntPtr a2);
80 
81  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
82  public extern static void Z3_interrupt(Z3_context a0);
83 
84  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
85  public extern static Z3_params Z3_mk_params(Z3_context a0);
86 
87  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
88  public extern static void Z3_params_inc_ref(Z3_context a0, Z3_params a1);
89 
90  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
91  public extern static void Z3_params_dec_ref(Z3_context a0, Z3_params a1);
92 
93  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
94  public extern static void Z3_params_set_bool(Z3_context a0, Z3_params a1, IntPtr a2, int a3);
95 
96  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
97  public extern static void Z3_params_set_uint(Z3_context a0, Z3_params a1, IntPtr a2, uint a3);
98 
99  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
100  public extern static void Z3_params_set_double(Z3_context a0, Z3_params a1, IntPtr a2, double a3);
101 
102  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
103  public extern static void Z3_params_set_symbol(Z3_context a0, Z3_params a1, IntPtr a2, IntPtr a3);
104 
105  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
106  public extern static IntPtr Z3_params_to_string(Z3_context a0, Z3_params a1);
107 
108  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
109  public extern static void Z3_params_validate(Z3_context a0, Z3_params a1, Z3_param_descrs a2);
110 
111  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
112  public extern static void Z3_param_descrs_inc_ref(Z3_context a0, Z3_param_descrs a1);
113 
114  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
115  public extern static void Z3_param_descrs_dec_ref(Z3_context a0, Z3_param_descrs a1);
116 
117  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
118  public extern static uint Z3_param_descrs_get_kind(Z3_context a0, Z3_param_descrs a1, IntPtr a2);
119 
120  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
121  public extern static uint Z3_param_descrs_size(Z3_context a0, Z3_param_descrs a1);
122 
123  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
124  public extern static IntPtr Z3_param_descrs_get_name(Z3_context a0, Z3_param_descrs a1, uint a2);
125 
126  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
127  public extern static IntPtr Z3_param_descrs_to_string(Z3_context a0, Z3_param_descrs a1);
128 
129  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
130  public extern static IntPtr Z3_mk_int_symbol(Z3_context a0, int a1);
131 
132  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
133  public extern static IntPtr Z3_mk_string_symbol(Z3_context a0, string a1);
134 
135  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
136  public extern static Z3_sort Z3_mk_uninterpreted_sort(Z3_context a0, IntPtr a1);
137 
138  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
139  public extern static Z3_sort Z3_mk_bool_sort(Z3_context a0);
140 
141  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
142  public extern static Z3_sort Z3_mk_int_sort(Z3_context a0);
143 
144  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
145  public extern static Z3_sort Z3_mk_real_sort(Z3_context a0);
146 
147  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
148  public extern static Z3_sort Z3_mk_bv_sort(Z3_context a0, uint a1);
149 
150  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
151  public extern static Z3_sort Z3_mk_finite_domain_sort(Z3_context a0, IntPtr a1, UInt64 a2);
152 
153  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
154  public extern static Z3_sort Z3_mk_array_sort(Z3_context a0, Z3_sort a1, Z3_sort a2);
155 
156  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
157  public extern 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);
158 
159  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
160  public extern 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);
161 
162  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
163  public extern 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);
164 
165  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
166  public extern 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);
167 
168  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
169  public extern static void Z3_del_constructor(Z3_context a0, Z3_constructor a1);
170 
171  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
172  public extern static Z3_sort Z3_mk_datatype(Z3_context a0, IntPtr a1, uint a2, [In, Out] Z3_constructor[] a3);
173 
174  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
175  public extern static Z3_constructor_list Z3_mk_constructor_list(Z3_context a0, uint a1, [In] Z3_constructor[] a2);
176 
177  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
178  public extern static void Z3_del_constructor_list(Z3_context a0, Z3_constructor_list a1);
179 
180  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
181  public extern static void Z3_mk_datatypes(Z3_context a0, uint a1, [In] IntPtr[] a2, [Out] Z3_sort[] a3, [In, Out] Z3_constructor_list[] a4);
182 
183  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
184  public extern 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);
185 
186  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
187  public extern static Z3_func_decl Z3_mk_func_decl(Z3_context a0, IntPtr a1, uint a2, [In] Z3_sort[] a3, Z3_sort a4);
188 
189  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
190  public extern static Z3_ast Z3_mk_app(Z3_context a0, Z3_func_decl a1, uint a2, [In] Z3_ast[] a3);
191 
192  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
193  public extern static Z3_ast Z3_mk_const(Z3_context a0, IntPtr a1, Z3_sort a2);
194 
195  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
196  public extern static Z3_func_decl Z3_mk_fresh_func_decl(Z3_context a0, string a1, uint a2, [In] Z3_sort[] a3, Z3_sort a4);
197 
198  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
199  public extern static Z3_ast Z3_mk_fresh_const(Z3_context a0, string a1, Z3_sort a2);
200 
201  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
202  public extern static Z3_ast Z3_mk_true(Z3_context a0);
203 
204  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
205  public extern static Z3_ast Z3_mk_false(Z3_context a0);
206 
207  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
208  public extern static Z3_ast Z3_mk_eq(Z3_context a0, Z3_ast a1, Z3_ast a2);
209 
210  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
211  public extern static Z3_ast Z3_mk_distinct(Z3_context a0, uint a1, [In] Z3_ast[] a2);
212 
213  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
214  public extern static Z3_ast Z3_mk_not(Z3_context a0, Z3_ast a1);
215 
216  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
217  public extern static Z3_ast Z3_mk_ite(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3);
218 
219  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
220  public extern static Z3_ast Z3_mk_iff(Z3_context a0, Z3_ast a1, Z3_ast a2);
221 
222  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
223  public extern static Z3_ast Z3_mk_implies(Z3_context a0, Z3_ast a1, Z3_ast a2);
224 
225  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
226  public extern static Z3_ast Z3_mk_xor(Z3_context a0, Z3_ast a1, Z3_ast a2);
227 
228  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
229  public extern static Z3_ast Z3_mk_and(Z3_context a0, uint a1, [In] Z3_ast[] a2);
230 
231  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
232  public extern static Z3_ast Z3_mk_or(Z3_context a0, uint a1, [In] Z3_ast[] a2);
233 
234  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
235  public extern static Z3_ast Z3_mk_add(Z3_context a0, uint a1, [In] Z3_ast[] a2);
236 
237  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
238  public extern static Z3_ast Z3_mk_mul(Z3_context a0, uint a1, [In] Z3_ast[] a2);
239 
240  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
241  public extern static Z3_ast Z3_mk_sub(Z3_context a0, uint a1, [In] Z3_ast[] a2);
242 
243  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
244  public extern static Z3_ast Z3_mk_unary_minus(Z3_context a0, Z3_ast a1);
245 
246  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
247  public extern static Z3_ast Z3_mk_div(Z3_context a0, Z3_ast a1, Z3_ast a2);
248 
249  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
250  public extern static Z3_ast Z3_mk_mod(Z3_context a0, Z3_ast a1, Z3_ast a2);
251 
252  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
253  public extern static Z3_ast Z3_mk_rem(Z3_context a0, Z3_ast a1, Z3_ast a2);
254 
255  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
256  public extern static Z3_ast Z3_mk_power(Z3_context a0, Z3_ast a1, Z3_ast a2);
257 
258  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
259  public extern static Z3_ast Z3_mk_lt(Z3_context a0, Z3_ast a1, Z3_ast a2);
260 
261  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
262  public extern static Z3_ast Z3_mk_le(Z3_context a0, Z3_ast a1, Z3_ast a2);
263 
264  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
265  public extern static Z3_ast Z3_mk_gt(Z3_context a0, Z3_ast a1, Z3_ast a2);
266 
267  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
268  public extern static Z3_ast Z3_mk_ge(Z3_context a0, Z3_ast a1, Z3_ast a2);
269 
270  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
271  public extern static Z3_ast Z3_mk_int2real(Z3_context a0, Z3_ast a1);
272 
273  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
274  public extern static Z3_ast Z3_mk_real2int(Z3_context a0, Z3_ast a1);
275 
276  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
277  public extern static Z3_ast Z3_mk_is_int(Z3_context a0, Z3_ast a1);
278 
279  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
280  public extern static Z3_ast Z3_mk_bvnot(Z3_context a0, Z3_ast a1);
281 
282  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
283  public extern static Z3_ast Z3_mk_bvredand(Z3_context a0, Z3_ast a1);
284 
285  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
286  public extern static Z3_ast Z3_mk_bvredor(Z3_context a0, Z3_ast a1);
287 
288  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
289  public extern static Z3_ast Z3_mk_bvand(Z3_context a0, Z3_ast a1, Z3_ast a2);
290 
291  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
292  public extern static Z3_ast Z3_mk_bvor(Z3_context a0, Z3_ast a1, Z3_ast a2);
293 
294  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
295  public extern static Z3_ast Z3_mk_bvxor(Z3_context a0, Z3_ast a1, Z3_ast a2);
296 
297  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
298  public extern static Z3_ast Z3_mk_bvnand(Z3_context a0, Z3_ast a1, Z3_ast a2);
299 
300  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
301  public extern static Z3_ast Z3_mk_bvnor(Z3_context a0, Z3_ast a1, Z3_ast a2);
302 
303  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
304  public extern static Z3_ast Z3_mk_bvxnor(Z3_context a0, Z3_ast a1, Z3_ast a2);
305 
306  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
307  public extern static Z3_ast Z3_mk_bvneg(Z3_context a0, Z3_ast a1);
308 
309  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
310  public extern static Z3_ast Z3_mk_bvadd(Z3_context a0, Z3_ast a1, Z3_ast a2);
311 
312  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
313  public extern static Z3_ast Z3_mk_bvsub(Z3_context a0, Z3_ast a1, Z3_ast a2);
314 
315  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
316  public extern static Z3_ast Z3_mk_bvmul(Z3_context a0, Z3_ast a1, Z3_ast a2);
317 
318  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
319  public extern static Z3_ast Z3_mk_bvudiv(Z3_context a0, Z3_ast a1, Z3_ast a2);
320 
321  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
322  public extern static Z3_ast Z3_mk_bvsdiv(Z3_context a0, Z3_ast a1, Z3_ast a2);
323 
324  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
325  public extern static Z3_ast Z3_mk_bvurem(Z3_context a0, Z3_ast a1, Z3_ast a2);
326 
327  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
328  public extern static Z3_ast Z3_mk_bvsrem(Z3_context a0, Z3_ast a1, Z3_ast a2);
329 
330  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
331  public extern static Z3_ast Z3_mk_bvsmod(Z3_context a0, Z3_ast a1, Z3_ast a2);
332 
333  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
334  public extern static Z3_ast Z3_mk_bvult(Z3_context a0, Z3_ast a1, Z3_ast a2);
335 
336  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
337  public extern static Z3_ast Z3_mk_bvslt(Z3_context a0, Z3_ast a1, Z3_ast a2);
338 
339  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
340  public extern static Z3_ast Z3_mk_bvule(Z3_context a0, Z3_ast a1, Z3_ast a2);
341 
342  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
343  public extern static Z3_ast Z3_mk_bvsle(Z3_context a0, Z3_ast a1, Z3_ast a2);
344 
345  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
346  public extern static Z3_ast Z3_mk_bvuge(Z3_context a0, Z3_ast a1, Z3_ast a2);
347 
348  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
349  public extern static Z3_ast Z3_mk_bvsge(Z3_context a0, Z3_ast a1, Z3_ast a2);
350 
351  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
352  public extern static Z3_ast Z3_mk_bvugt(Z3_context a0, Z3_ast a1, Z3_ast a2);
353 
354  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
355  public extern static Z3_ast Z3_mk_bvsgt(Z3_context a0, Z3_ast a1, Z3_ast a2);
356 
357  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
358  public extern static Z3_ast Z3_mk_concat(Z3_context a0, Z3_ast a1, Z3_ast a2);
359 
360  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
361  public extern static Z3_ast Z3_mk_extract(Z3_context a0, uint a1, uint a2, Z3_ast a3);
362 
363  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
364  public extern static Z3_ast Z3_mk_sign_ext(Z3_context a0, uint a1, Z3_ast a2);
365 
366  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
367  public extern static Z3_ast Z3_mk_zero_ext(Z3_context a0, uint a1, Z3_ast a2);
368 
369  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
370  public extern static Z3_ast Z3_mk_repeat(Z3_context a0, uint a1, Z3_ast a2);
371 
372  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
373  public extern static Z3_ast Z3_mk_bvshl(Z3_context a0, Z3_ast a1, Z3_ast a2);
374 
375  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
376  public extern static Z3_ast Z3_mk_bvlshr(Z3_context a0, Z3_ast a1, Z3_ast a2);
377 
378  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
379  public extern static Z3_ast Z3_mk_bvashr(Z3_context a0, Z3_ast a1, Z3_ast a2);
380 
381  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
382  public extern static Z3_ast Z3_mk_rotate_left(Z3_context a0, uint a1, Z3_ast a2);
383 
384  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
385  public extern static Z3_ast Z3_mk_rotate_right(Z3_context a0, uint a1, Z3_ast a2);
386 
387  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
388  public extern static Z3_ast Z3_mk_ext_rotate_left(Z3_context a0, Z3_ast a1, Z3_ast a2);
389 
390  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
391  public extern static Z3_ast Z3_mk_ext_rotate_right(Z3_context a0, Z3_ast a1, Z3_ast a2);
392 
393  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
394  public extern static Z3_ast Z3_mk_int2bv(Z3_context a0, uint a1, Z3_ast a2);
395 
396  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
397  public extern static Z3_ast Z3_mk_bv2int(Z3_context a0, Z3_ast a1, int a2);
398 
399  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
400  public extern static Z3_ast Z3_mk_bvadd_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2, int a3);
401 
402  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
403  public extern static Z3_ast Z3_mk_bvadd_no_underflow(Z3_context a0, Z3_ast a1, Z3_ast a2);
404 
405  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
406  public extern static Z3_ast Z3_mk_bvsub_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2);
407 
408  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
409  public extern static Z3_ast Z3_mk_bvsub_no_underflow(Z3_context a0, Z3_ast a1, Z3_ast a2, int a3);
410 
411  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
412  public extern static Z3_ast Z3_mk_bvsdiv_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2);
413 
414  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
415  public extern static Z3_ast Z3_mk_bvneg_no_overflow(Z3_context a0, Z3_ast a1);
416 
417  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
418  public extern static Z3_ast Z3_mk_bvmul_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2, int a3);
419 
420  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
421  public extern static Z3_ast Z3_mk_bvmul_no_underflow(Z3_context a0, Z3_ast a1, Z3_ast a2);
422 
423  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
424  public extern static Z3_ast Z3_mk_select(Z3_context a0, Z3_ast a1, Z3_ast a2);
425 
426  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
427  public extern static Z3_ast Z3_mk_store(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3);
428 
429  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
430  public extern static Z3_ast Z3_mk_const_array(Z3_context a0, Z3_sort a1, Z3_ast a2);
431 
432  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
433  public extern static Z3_ast Z3_mk_map(Z3_context a0, Z3_func_decl a1, uint a2, [In] Z3_ast[] a3);
434 
435  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
436  public extern static Z3_ast Z3_mk_array_default(Z3_context a0, Z3_ast a1);
437 
438  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
439  public extern static Z3_sort Z3_mk_set_sort(Z3_context a0, Z3_sort a1);
440 
441  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
442  public extern static Z3_ast Z3_mk_empty_set(Z3_context a0, Z3_sort a1);
443 
444  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
445  public extern static Z3_ast Z3_mk_full_set(Z3_context a0, Z3_sort a1);
446 
447  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
448  public extern static Z3_ast Z3_mk_set_add(Z3_context a0, Z3_ast a1, Z3_ast a2);
449 
450  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
451  public extern static Z3_ast Z3_mk_set_del(Z3_context a0, Z3_ast a1, Z3_ast a2);
452 
453  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
454  public extern static Z3_ast Z3_mk_set_union(Z3_context a0, uint a1, [In] Z3_ast[] a2);
455 
456  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
457  public extern static Z3_ast Z3_mk_set_intersect(Z3_context a0, uint a1, [In] Z3_ast[] a2);
458 
459  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
460  public extern static Z3_ast Z3_mk_set_difference(Z3_context a0, Z3_ast a1, Z3_ast a2);
461 
462  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
463  public extern static Z3_ast Z3_mk_set_complement(Z3_context a0, Z3_ast a1);
464 
465  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
466  public extern static Z3_ast Z3_mk_set_member(Z3_context a0, Z3_ast a1, Z3_ast a2);
467 
468  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
469  public extern static Z3_ast Z3_mk_set_subset(Z3_context a0, Z3_ast a1, Z3_ast a2);
470 
471  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
472  public extern static Z3_ast Z3_mk_numeral(Z3_context a0, string a1, Z3_sort a2);
473 
474  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
475  public extern static Z3_ast Z3_mk_real(Z3_context a0, int a1, int a2);
476 
477  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
478  public extern static Z3_ast Z3_mk_int(Z3_context a0, int a1, Z3_sort a2);
479 
480  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
481  public extern static Z3_ast Z3_mk_unsigned_int(Z3_context a0, uint a1, Z3_sort a2);
482 
483  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
484  public extern static Z3_ast Z3_mk_int64(Z3_context a0, Int64 a1, Z3_sort a2);
485 
486  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
487  public extern static Z3_ast Z3_mk_unsigned_int64(Z3_context a0, UInt64 a1, Z3_sort a2);
488 
489  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
490  public extern static Z3_pattern Z3_mk_pattern(Z3_context a0, uint a1, [In] Z3_ast[] a2);
491 
492  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
493  public extern static Z3_ast Z3_mk_bound(Z3_context a0, uint a1, Z3_sort a2);
494 
495  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
496  public extern 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);
497 
498  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
499  public extern 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);
500 
501  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
502  public extern 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);
503 
504  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
505  public extern 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);
506 
507  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
508  public extern 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);
509 
510  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
511  public extern 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);
512 
513  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
514  public extern 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);
515 
516  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
517  public extern 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);
518 
519  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
520  public extern static uint Z3_get_symbol_kind(Z3_context a0, IntPtr a1);
521 
522  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
523  public extern static int Z3_get_symbol_int(Z3_context a0, IntPtr a1);
524 
525  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
526  public extern static IntPtr Z3_get_symbol_string(Z3_context a0, IntPtr a1);
527 
528  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
529  public extern static IntPtr Z3_get_sort_name(Z3_context a0, Z3_sort a1);
530 
531  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
532  public extern static uint Z3_get_sort_id(Z3_context a0, Z3_sort a1);
533 
534  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
535  public extern static Z3_ast Z3_sort_to_ast(Z3_context a0, Z3_sort a1);
536 
537  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
538  public extern static int Z3_is_eq_sort(Z3_context a0, Z3_sort a1, Z3_sort a2);
539 
540  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
541  public extern static uint Z3_get_sort_kind(Z3_context a0, Z3_sort a1);
542 
543  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
544  public extern static uint Z3_get_bv_sort_size(Z3_context a0, Z3_sort a1);
545 
546  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
547  public extern static int Z3_get_finite_domain_sort_size(Z3_context a0, Z3_sort a1, [In, Out] ref UInt64 a2);
548 
549  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
550  public extern static Z3_sort Z3_get_array_sort_domain(Z3_context a0, Z3_sort a1);
551 
552  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
553  public extern static Z3_sort Z3_get_array_sort_range(Z3_context a0, Z3_sort a1);
554 
555  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
556  public extern static Z3_func_decl Z3_get_tuple_sort_mk_decl(Z3_context a0, Z3_sort a1);
557 
558  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
559  public extern static uint Z3_get_tuple_sort_num_fields(Z3_context a0, Z3_sort a1);
560 
561  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
562  public extern static Z3_func_decl Z3_get_tuple_sort_field_decl(Z3_context a0, Z3_sort a1, uint a2);
563 
564  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
565  public extern static uint Z3_get_datatype_sort_num_constructors(Z3_context a0, Z3_sort a1);
566 
567  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
568  public extern static Z3_func_decl Z3_get_datatype_sort_constructor(Z3_context a0, Z3_sort a1, uint a2);
569 
570  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
571  public extern static Z3_func_decl Z3_get_datatype_sort_recognizer(Z3_context a0, Z3_sort a1, uint a2);
572 
573  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
574  public extern static Z3_func_decl Z3_get_datatype_sort_constructor_accessor(Z3_context a0, Z3_sort a1, uint a2, uint a3);
575 
576  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
577  public extern static uint Z3_get_relation_arity(Z3_context a0, Z3_sort a1);
578 
579  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
580  public extern static Z3_sort Z3_get_relation_column(Z3_context a0, Z3_sort a1, uint a2);
581 
582  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
583  public extern static Z3_ast Z3_func_decl_to_ast(Z3_context a0, Z3_func_decl a1);
584 
585  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
586  public extern static int Z3_is_eq_func_decl(Z3_context a0, Z3_func_decl a1, Z3_func_decl a2);
587 
588  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
589  public extern static uint Z3_get_func_decl_id(Z3_context a0, Z3_func_decl a1);
590 
591  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
592  public extern static IntPtr Z3_get_decl_name(Z3_context a0, Z3_func_decl a1);
593 
594  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
595  public extern static uint Z3_get_decl_kind(Z3_context a0, Z3_func_decl a1);
596 
597  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
598  public extern static uint Z3_get_domain_size(Z3_context a0, Z3_func_decl a1);
599 
600  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
601  public extern static uint Z3_get_arity(Z3_context a0, Z3_func_decl a1);
602 
603  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
604  public extern static Z3_sort Z3_get_domain(Z3_context a0, Z3_func_decl a1, uint a2);
605 
606  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
607  public extern static Z3_sort Z3_get_range(Z3_context a0, Z3_func_decl a1);
608 
609  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
610  public extern static uint Z3_get_decl_num_parameters(Z3_context a0, Z3_func_decl a1);
611 
612  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
613  public extern static uint Z3_get_decl_parameter_kind(Z3_context a0, Z3_func_decl a1, uint a2);
614 
615  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
616  public extern static int Z3_get_decl_int_parameter(Z3_context a0, Z3_func_decl a1, uint a2);
617 
618  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
619  public extern static double Z3_get_decl_double_parameter(Z3_context a0, Z3_func_decl a1, uint a2);
620 
621  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
622  public extern static IntPtr Z3_get_decl_symbol_parameter(Z3_context a0, Z3_func_decl a1, uint a2);
623 
624  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
625  public extern static Z3_sort Z3_get_decl_sort_parameter(Z3_context a0, Z3_func_decl a1, uint a2);
626 
627  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
628  public extern static Z3_ast Z3_get_decl_ast_parameter(Z3_context a0, Z3_func_decl a1, uint a2);
629 
630  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
631  public extern static Z3_func_decl Z3_get_decl_func_decl_parameter(Z3_context a0, Z3_func_decl a1, uint a2);
632 
633  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
634  public extern static IntPtr Z3_get_decl_rational_parameter(Z3_context a0, Z3_func_decl a1, uint a2);
635 
636  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
637  public extern static Z3_ast Z3_app_to_ast(Z3_context a0, Z3_app a1);
638 
639  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
640  public extern static Z3_func_decl Z3_get_app_decl(Z3_context a0, Z3_app a1);
641 
642  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
643  public extern static uint Z3_get_app_num_args(Z3_context a0, Z3_app a1);
644 
645  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
646  public extern static Z3_ast Z3_get_app_arg(Z3_context a0, Z3_app a1, uint a2);
647 
648  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
649  public extern static int Z3_is_eq_ast(Z3_context a0, Z3_ast a1, Z3_ast a2);
650 
651  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
652  public extern static uint Z3_get_ast_id(Z3_context a0, Z3_ast a1);
653 
654  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
655  public extern static uint Z3_get_ast_hash(Z3_context a0, Z3_ast a1);
656 
657  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
658  public extern static Z3_sort Z3_get_sort(Z3_context a0, Z3_ast a1);
659 
660  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
661  public extern static int Z3_is_well_sorted(Z3_context a0, Z3_ast a1);
662 
663  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
664  public extern static uint Z3_get_bool_value(Z3_context a0, Z3_ast a1);
665 
666  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
667  public extern static uint Z3_get_ast_kind(Z3_context a0, Z3_ast a1);
668 
669  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
670  public extern static int Z3_is_app(Z3_context a0, Z3_ast a1);
671 
672  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
673  public extern static int Z3_is_numeral_ast(Z3_context a0, Z3_ast a1);
674 
675  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
676  public extern static int Z3_is_algebraic_number(Z3_context a0, Z3_ast a1);
677 
678  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
679  public extern static Z3_app Z3_to_app(Z3_context a0, Z3_ast a1);
680 
681  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
682  public extern static Z3_func_decl Z3_to_func_decl(Z3_context a0, Z3_ast a1);
683 
684  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
685  public extern static IntPtr Z3_get_numeral_string(Z3_context a0, Z3_ast a1);
686 
687  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
688  public extern static IntPtr Z3_get_numeral_decimal_string(Z3_context a0, Z3_ast a1, uint a2);
689 
690  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
691  public extern static Z3_ast Z3_get_numerator(Z3_context a0, Z3_ast a1);
692 
693  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
694  public extern static Z3_ast Z3_get_denominator(Z3_context a0, Z3_ast a1);
695 
696  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
697  public extern static int Z3_get_numeral_small(Z3_context a0, Z3_ast a1, [In, Out] ref Int64 a2, [In, Out] ref Int64 a3);
698 
699  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
700  public extern static int Z3_get_numeral_int(Z3_context a0, Z3_ast a1, [In, Out] ref int a2);
701 
702  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
703  public extern static int Z3_get_numeral_uint(Z3_context a0, Z3_ast a1, [In, Out] ref uint a2);
704 
705  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
706  public extern static int Z3_get_numeral_uint64(Z3_context a0, Z3_ast a1, [In, Out] ref UInt64 a2);
707 
708  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
709  public extern static int Z3_get_numeral_int64(Z3_context a0, Z3_ast a1, [In, Out] ref Int64 a2);
710 
711  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
712  public extern static int Z3_get_numeral_rational_int64(Z3_context a0, Z3_ast a1, [In, Out] ref Int64 a2, [In, Out] ref Int64 a3);
713 
714  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
715  public extern static Z3_ast Z3_get_algebraic_number_lower(Z3_context a0, Z3_ast a1, uint a2);
716 
717  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
718  public extern static Z3_ast Z3_get_algebraic_number_upper(Z3_context a0, Z3_ast a1, uint a2);
719 
720  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
721  public extern static Z3_ast Z3_pattern_to_ast(Z3_context a0, Z3_pattern a1);
722 
723  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
724  public extern static uint Z3_get_pattern_num_terms(Z3_context a0, Z3_pattern a1);
725 
726  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
727  public extern static Z3_ast Z3_get_pattern(Z3_context a0, Z3_pattern a1, uint a2);
728 
729  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
730  public extern static uint Z3_get_index_value(Z3_context a0, Z3_ast a1);
731 
732  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
733  public extern static int Z3_is_quantifier_forall(Z3_context a0, Z3_ast a1);
734 
735  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
736  public extern static uint Z3_get_quantifier_weight(Z3_context a0, Z3_ast a1);
737 
738  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
739  public extern static uint Z3_get_quantifier_num_patterns(Z3_context a0, Z3_ast a1);
740 
741  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
742  public extern static Z3_pattern Z3_get_quantifier_pattern_ast(Z3_context a0, Z3_ast a1, uint a2);
743 
744  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
745  public extern static uint Z3_get_quantifier_num_no_patterns(Z3_context a0, Z3_ast a1);
746 
747  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
748  public extern static Z3_ast Z3_get_quantifier_no_pattern_ast(Z3_context a0, Z3_ast a1, uint a2);
749 
750  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
751  public extern static uint Z3_get_quantifier_num_bound(Z3_context a0, Z3_ast a1);
752 
753  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
754  public extern static IntPtr Z3_get_quantifier_bound_name(Z3_context a0, Z3_ast a1, uint a2);
755 
756  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
757  public extern static Z3_sort Z3_get_quantifier_bound_sort(Z3_context a0, Z3_ast a1, uint a2);
758 
759  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
760  public extern static Z3_ast Z3_get_quantifier_body(Z3_context a0, Z3_ast a1);
761 
762  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
763  public extern static Z3_ast Z3_simplify(Z3_context a0, Z3_ast a1);
764 
765  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
766  public extern static Z3_ast Z3_simplify_ex(Z3_context a0, Z3_ast a1, Z3_params a2);
767 
768  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
769  public extern static IntPtr Z3_simplify_get_help(Z3_context a0);
770 
771  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
772  public extern static Z3_param_descrs Z3_simplify_get_param_descrs(Z3_context a0);
773 
774  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
775  public extern static Z3_ast Z3_update_term(Z3_context a0, Z3_ast a1, uint a2, [In] Z3_ast[] a3);
776 
777  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
778  public extern static Z3_ast Z3_substitute(Z3_context a0, Z3_ast a1, uint a2, [In] Z3_ast[] a3, [In] Z3_ast[] a4);
779 
780  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
781  public extern static Z3_ast Z3_substitute_vars(Z3_context a0, Z3_ast a1, uint a2, [In] Z3_ast[] a3);
782 
783  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
784  public extern static Z3_ast Z3_translate(Z3_context a0, Z3_ast a1, Z3_context a2);
785 
786  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
787  public extern static void Z3_model_inc_ref(Z3_context a0, Z3_model a1);
788 
789  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
790  public extern static void Z3_model_dec_ref(Z3_context a0, Z3_model a1);
791 
792  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
793  public extern static int Z3_model_eval(Z3_context a0, Z3_model a1, Z3_ast a2, int a3, [In, Out] ref Z3_ast a4);
794 
795  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
796  public extern static Z3_ast Z3_model_get_const_interp(Z3_context a0, Z3_model a1, Z3_func_decl a2);
797 
798  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
799  public extern static Z3_func_interp Z3_model_get_func_interp(Z3_context a0, Z3_model a1, Z3_func_decl a2);
800 
801  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
802  public extern static uint Z3_model_get_num_consts(Z3_context a0, Z3_model a1);
803 
804  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
805  public extern static Z3_func_decl Z3_model_get_const_decl(Z3_context a0, Z3_model a1, uint a2);
806 
807  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
808  public extern static uint Z3_model_get_num_funcs(Z3_context a0, Z3_model a1);
809 
810  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
811  public extern static Z3_func_decl Z3_model_get_func_decl(Z3_context a0, Z3_model a1, uint a2);
812 
813  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
814  public extern static uint Z3_model_get_num_sorts(Z3_context a0, Z3_model a1);
815 
816  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
817  public extern static Z3_sort Z3_model_get_sort(Z3_context a0, Z3_model a1, uint a2);
818 
819  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
820  public extern static Z3_ast_vector Z3_model_get_sort_universe(Z3_context a0, Z3_model a1, Z3_sort a2);
821 
822  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
823  public extern static int Z3_is_as_array(Z3_context a0, Z3_ast a1);
824 
825  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
826  public extern static Z3_func_decl Z3_get_as_array_func_decl(Z3_context a0, Z3_ast a1);
827 
828  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
829  public extern static void Z3_func_interp_inc_ref(Z3_context a0, Z3_func_interp a1);
830 
831  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
832  public extern static void Z3_func_interp_dec_ref(Z3_context a0, Z3_func_interp a1);
833 
834  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
835  public extern static uint Z3_func_interp_get_num_entries(Z3_context a0, Z3_func_interp a1);
836 
837  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
838  public extern static Z3_func_entry Z3_func_interp_get_entry(Z3_context a0, Z3_func_interp a1, uint a2);
839 
840  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
841  public extern static Z3_ast Z3_func_interp_get_else(Z3_context a0, Z3_func_interp a1);
842 
843  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
844  public extern static uint Z3_func_interp_get_arity(Z3_context a0, Z3_func_interp a1);
845 
846  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
847  public extern static void Z3_func_entry_inc_ref(Z3_context a0, Z3_func_entry a1);
848 
849  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
850  public extern static void Z3_func_entry_dec_ref(Z3_context a0, Z3_func_entry a1);
851 
852  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
853  public extern static Z3_ast Z3_func_entry_get_value(Z3_context a0, Z3_func_entry a1);
854 
855  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
856  public extern static uint Z3_func_entry_get_num_args(Z3_context a0, Z3_func_entry a1);
857 
858  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
859  public extern static Z3_ast Z3_func_entry_get_arg(Z3_context a0, Z3_func_entry a1, uint a2);
860 
861  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
862  public extern static int Z3_open_log(string a0);
863 
864  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
865  public extern static void Z3_append_log(string a0);
866 
867  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
868  public extern static void Z3_close_log();
869 
870  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
871  public extern static void Z3_toggle_warning_messages(int a0);
872 
873  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
874  public extern static void Z3_set_ast_print_mode(Z3_context a0, uint a1);
875 
876  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
877  public extern static IntPtr Z3_ast_to_string(Z3_context a0, Z3_ast a1);
878 
879  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
880  public extern static IntPtr Z3_pattern_to_string(Z3_context a0, Z3_pattern a1);
881 
882  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
883  public extern static IntPtr Z3_sort_to_string(Z3_context a0, Z3_sort a1);
884 
885  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
886  public extern static IntPtr Z3_func_decl_to_string(Z3_context a0, Z3_func_decl a1);
887 
888  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
889  public extern static IntPtr Z3_model_to_string(Z3_context a0, Z3_model a1);
890 
891  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
892  public extern static IntPtr Z3_benchmark_to_smtlib_string(Z3_context a0, string a1, string a2, string a3, string a4, uint a5, [In] Z3_ast[] a6, Z3_ast a7);
893 
894  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
895  public extern 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);
896 
897  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
898  public extern 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);
899 
900  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
901  public extern 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);
902 
903  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
904  public extern 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);
905 
906  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
907  public extern static uint Z3_get_smtlib_num_formulas(Z3_context a0);
908 
909  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
910  public extern static Z3_ast Z3_get_smtlib_formula(Z3_context a0, uint a1);
911 
912  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
913  public extern static uint Z3_get_smtlib_num_assumptions(Z3_context a0);
914 
915  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
916  public extern static Z3_ast Z3_get_smtlib_assumption(Z3_context a0, uint a1);
917 
918  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
919  public extern static uint Z3_get_smtlib_num_decls(Z3_context a0);
920 
921  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
922  public extern static Z3_func_decl Z3_get_smtlib_decl(Z3_context a0, uint a1);
923 
924  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
925  public extern static uint Z3_get_smtlib_num_sorts(Z3_context a0);
926 
927  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
928  public extern static Z3_sort Z3_get_smtlib_sort(Z3_context a0, uint a1);
929 
930  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
931  public extern static IntPtr Z3_get_smtlib_error(Z3_context a0);
932 
933  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
934  public extern static uint Z3_get_error_code(Z3_context a0);
935 
936  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
937  public extern static void Z3_set_error(Z3_context a0, uint a1);
938 
939  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
940  public extern static IntPtr Z3_get_error_msg(uint a0);
941 
942  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
943  public extern static IntPtr Z3_get_error_msg_ex(Z3_context a0, uint a1);
944 
945  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
946  public extern 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);
947 
948  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
949  public extern static void Z3_enable_trace(string a0);
950 
951  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
952  public extern static void Z3_disable_trace(string a0);
953 
954  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
955  public extern static void Z3_reset_memory();
956 
957  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
958  public extern static Z3_fixedpoint Z3_mk_fixedpoint(Z3_context a0);
959 
960  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
961  public extern static void Z3_fixedpoint_inc_ref(Z3_context a0, Z3_fixedpoint a1);
962 
963  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
964  public extern static void Z3_fixedpoint_dec_ref(Z3_context a0, Z3_fixedpoint a1);
965 
966  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
967  public extern static void Z3_fixedpoint_add_rule(Z3_context a0, Z3_fixedpoint a1, Z3_ast a2, IntPtr a3);
968 
969  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
970  public extern static void Z3_fixedpoint_add_fact(Z3_context a0, Z3_fixedpoint a1, Z3_func_decl a2, uint a3, [In] uint[] a4);
971 
972  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
973  public extern static void Z3_fixedpoint_assert(Z3_context a0, Z3_fixedpoint a1, Z3_ast a2);
974 
975  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
976  public extern static int Z3_fixedpoint_query(Z3_context a0, Z3_fixedpoint a1, Z3_ast a2);
977 
978  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
979  public extern static int Z3_fixedpoint_query_relations(Z3_context a0, Z3_fixedpoint a1, uint a2, [In] Z3_func_decl[] a3);
980 
981  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
982  public extern static Z3_ast Z3_fixedpoint_get_answer(Z3_context a0, Z3_fixedpoint a1);
983 
984  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
985  public extern static IntPtr Z3_fixedpoint_get_reason_unknown(Z3_context a0, Z3_fixedpoint a1);
986 
987  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
988  public extern static void Z3_fixedpoint_update_rule(Z3_context a0, Z3_fixedpoint a1, Z3_ast a2, IntPtr a3);
989 
990  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
991  public extern static uint Z3_fixedpoint_get_num_levels(Z3_context a0, Z3_fixedpoint a1, Z3_func_decl a2);
992 
993  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
994  public extern static Z3_ast Z3_fixedpoint_get_cover_delta(Z3_context a0, Z3_fixedpoint a1, int a2, Z3_func_decl a3);
995 
996  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
997  public extern static void Z3_fixedpoint_add_cover(Z3_context a0, Z3_fixedpoint a1, int a2, Z3_func_decl a3, Z3_ast a4);
998 
999  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1000  public extern static Z3_stats Z3_fixedpoint_get_statistics(Z3_context a0, Z3_fixedpoint a1);
1001 
1002  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1003  public extern static void Z3_fixedpoint_register_relation(Z3_context a0, Z3_fixedpoint a1, Z3_func_decl a2);
1004 
1005  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1006  public extern static void Z3_fixedpoint_set_predicate_representation(Z3_context a0, Z3_fixedpoint a1, Z3_func_decl a2, uint a3, [In] IntPtr[] a4);
1007 
1008  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1009  public extern static Z3_ast_vector Z3_fixedpoint_get_rules(Z3_context a0, Z3_fixedpoint a1);
1010 
1011  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1012  public extern static Z3_ast_vector Z3_fixedpoint_get_assertions(Z3_context a0, Z3_fixedpoint a1);
1013 
1014  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1015  public extern static void Z3_fixedpoint_set_params(Z3_context a0, Z3_fixedpoint a1, Z3_params a2);
1016 
1017  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1018  public extern static IntPtr Z3_fixedpoint_get_help(Z3_context a0, Z3_fixedpoint a1);
1019 
1020  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1021  public extern static Z3_param_descrs Z3_fixedpoint_get_param_descrs(Z3_context a0, Z3_fixedpoint a1);
1022 
1023  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1024  public extern static IntPtr Z3_fixedpoint_to_string(Z3_context a0, Z3_fixedpoint a1, uint a2, [In] Z3_ast[] a3);
1025 
1026  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1027  public extern static Z3_ast_vector Z3_fixedpoint_from_string(Z3_context a0, Z3_fixedpoint a1, string a2);
1028 
1029  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1030  public extern static Z3_ast_vector Z3_fixedpoint_from_file(Z3_context a0, Z3_fixedpoint a1, string a2);
1031 
1032  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1033  public extern static void Z3_fixedpoint_push(Z3_context a0, Z3_fixedpoint a1);
1034 
1035  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1036  public extern static void Z3_fixedpoint_pop(Z3_context a0, Z3_fixedpoint a1);
1037 
1038  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1039  public extern static Z3_ast_vector Z3_mk_ast_vector(Z3_context a0);
1040 
1041  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1042  public extern static void Z3_ast_vector_inc_ref(Z3_context a0, Z3_ast_vector a1);
1043 
1044  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1045  public extern static void Z3_ast_vector_dec_ref(Z3_context a0, Z3_ast_vector a1);
1046 
1047  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1048  public extern static uint Z3_ast_vector_size(Z3_context a0, Z3_ast_vector a1);
1049 
1050  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1051  public extern static Z3_ast Z3_ast_vector_get(Z3_context a0, Z3_ast_vector a1, uint a2);
1052 
1053  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1054  public extern static void Z3_ast_vector_set(Z3_context a0, Z3_ast_vector a1, uint a2, Z3_ast a3);
1055 
1056  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1057  public extern static void Z3_ast_vector_resize(Z3_context a0, Z3_ast_vector a1, uint a2);
1058 
1059  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1060  public extern static void Z3_ast_vector_push(Z3_context a0, Z3_ast_vector a1, Z3_ast a2);
1061 
1062  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1063  public extern static Z3_ast_vector Z3_ast_vector_translate(Z3_context a0, Z3_ast_vector a1, Z3_context a2);
1064 
1065  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1066  public extern static IntPtr Z3_ast_vector_to_string(Z3_context a0, Z3_ast_vector a1);
1067 
1068  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1069  public extern static Z3_ast_map Z3_mk_ast_map(Z3_context a0);
1070 
1071  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1072  public extern static void Z3_ast_map_inc_ref(Z3_context a0, Z3_ast_map a1);
1073 
1074  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1075  public extern static void Z3_ast_map_dec_ref(Z3_context a0, Z3_ast_map a1);
1076 
1077  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1078  public extern static int Z3_ast_map_contains(Z3_context a0, Z3_ast_map a1, Z3_ast a2);
1079 
1080  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1081  public extern static Z3_ast Z3_ast_map_find(Z3_context a0, Z3_ast_map a1, Z3_ast a2);
1082 
1083  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1084  public extern static void Z3_ast_map_insert(Z3_context a0, Z3_ast_map a1, Z3_ast a2, Z3_ast a3);
1085 
1086  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1087  public extern static void Z3_ast_map_erase(Z3_context a0, Z3_ast_map a1, Z3_ast a2);
1088 
1089  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1090  public extern static void Z3_ast_map_reset(Z3_context a0, Z3_ast_map a1);
1091 
1092  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1093  public extern static uint Z3_ast_map_size(Z3_context a0, Z3_ast_map a1);
1094 
1095  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1096  public extern static Z3_ast_vector Z3_ast_map_keys(Z3_context a0, Z3_ast_map a1);
1097 
1098  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1099  public extern static IntPtr Z3_ast_map_to_string(Z3_context a0, Z3_ast_map a1);
1100 
1101  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1102  public extern static Z3_goal Z3_mk_goal(Z3_context a0, int a1, int a2, int a3);
1103 
1104  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1105  public extern static void Z3_goal_inc_ref(Z3_context a0, Z3_goal a1);
1106 
1107  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1108  public extern static void Z3_goal_dec_ref(Z3_context a0, Z3_goal a1);
1109 
1110  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1111  public extern static uint Z3_goal_precision(Z3_context a0, Z3_goal a1);
1112 
1113  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1114  public extern static void Z3_goal_assert(Z3_context a0, Z3_goal a1, Z3_ast a2);
1115 
1116  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1117  public extern static int Z3_goal_inconsistent(Z3_context a0, Z3_goal a1);
1118 
1119  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1120  public extern static uint Z3_goal_depth(Z3_context a0, Z3_goal a1);
1121 
1122  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1123  public extern static void Z3_goal_reset(Z3_context a0, Z3_goal a1);
1124 
1125  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1126  public extern static uint Z3_goal_size(Z3_context a0, Z3_goal a1);
1127 
1128  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1129  public extern static Z3_ast Z3_goal_formula(Z3_context a0, Z3_goal a1, uint a2);
1130 
1131  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1132  public extern static uint Z3_goal_num_exprs(Z3_context a0, Z3_goal a1);
1133 
1134  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1135  public extern static int Z3_goal_is_decided_sat(Z3_context a0, Z3_goal a1);
1136 
1137  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1138  public extern static int Z3_goal_is_decided_unsat(Z3_context a0, Z3_goal a1);
1139 
1140  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1141  public extern static Z3_goal Z3_goal_translate(Z3_context a0, Z3_goal a1, Z3_context a2);
1142 
1143  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1144  public extern static IntPtr Z3_goal_to_string(Z3_context a0, Z3_goal a1);
1145 
1146  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1147  public extern static Z3_tactic Z3_mk_tactic(Z3_context a0, string a1);
1148 
1149  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1150  public extern static void Z3_tactic_inc_ref(Z3_context a0, Z3_tactic a1);
1151 
1152  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1153  public extern static void Z3_tactic_dec_ref(Z3_context a0, Z3_tactic a1);
1154 
1155  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1156  public extern static Z3_probe Z3_mk_probe(Z3_context a0, string a1);
1157 
1158  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1159  public extern static void Z3_probe_inc_ref(Z3_context a0, Z3_probe a1);
1160 
1161  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1162  public extern static void Z3_probe_dec_ref(Z3_context a0, Z3_probe a1);
1163 
1164  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1165  public extern static Z3_tactic Z3_tactic_and_then(Z3_context a0, Z3_tactic a1, Z3_tactic a2);
1166 
1167  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1168  public extern static Z3_tactic Z3_tactic_or_else(Z3_context a0, Z3_tactic a1, Z3_tactic a2);
1169 
1170  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1171  public extern static Z3_tactic Z3_tactic_par_or(Z3_context a0, uint a1, [In] Z3_tactic[] a2);
1172 
1173  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1174  public extern static Z3_tactic Z3_tactic_par_and_then(Z3_context a0, Z3_tactic a1, Z3_tactic a2);
1175 
1176  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1177  public extern static Z3_tactic Z3_tactic_try_for(Z3_context a0, Z3_tactic a1, uint a2);
1178 
1179  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1180  public extern static Z3_tactic Z3_tactic_when(Z3_context a0, Z3_probe a1, Z3_tactic a2);
1181 
1182  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1183  public extern static Z3_tactic Z3_tactic_cond(Z3_context a0, Z3_probe a1, Z3_tactic a2, Z3_tactic a3);
1184 
1185  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1186  public extern static Z3_tactic Z3_tactic_repeat(Z3_context a0, Z3_tactic a1, uint a2);
1187 
1188  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1189  public extern static Z3_tactic Z3_tactic_skip(Z3_context a0);
1190 
1191  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1192  public extern static Z3_tactic Z3_tactic_fail(Z3_context a0);
1193 
1194  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1195  public extern static Z3_tactic Z3_tactic_fail_if(Z3_context a0, Z3_probe a1);
1196 
1197  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1198  public extern static Z3_tactic Z3_tactic_fail_if_not_decided(Z3_context a0);
1199 
1200  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1201  public extern static Z3_tactic Z3_tactic_using_params(Z3_context a0, Z3_tactic a1, Z3_params a2);
1202 
1203  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1204  public extern static Z3_probe Z3_probe_const(Z3_context a0, double a1);
1205 
1206  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1207  public extern static Z3_probe Z3_probe_lt(Z3_context a0, Z3_probe a1, Z3_probe a2);
1208 
1209  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1210  public extern static Z3_probe Z3_probe_gt(Z3_context a0, Z3_probe a1, Z3_probe a2);
1211 
1212  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1213  public extern static Z3_probe Z3_probe_le(Z3_context a0, Z3_probe a1, Z3_probe a2);
1214 
1215  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1216  public extern static Z3_probe Z3_probe_ge(Z3_context a0, Z3_probe a1, Z3_probe a2);
1217 
1218  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1219  public extern static Z3_probe Z3_probe_eq(Z3_context a0, Z3_probe a1, Z3_probe a2);
1220 
1221  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1222  public extern static Z3_probe Z3_probe_and(Z3_context a0, Z3_probe a1, Z3_probe a2);
1223 
1224  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1225  public extern static Z3_probe Z3_probe_or(Z3_context a0, Z3_probe a1, Z3_probe a2);
1226 
1227  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1228  public extern static Z3_probe Z3_probe_not(Z3_context a0, Z3_probe a1);
1229 
1230  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1231  public extern static uint Z3_get_num_tactics(Z3_context a0);
1232 
1233  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1234  public extern static IntPtr Z3_get_tactic_name(Z3_context a0, uint a1);
1235 
1236  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1237  public extern static uint Z3_get_num_probes(Z3_context a0);
1238 
1239  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1240  public extern static IntPtr Z3_get_probe_name(Z3_context a0, uint a1);
1241 
1242  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1243  public extern static IntPtr Z3_tactic_get_help(Z3_context a0, Z3_tactic a1);
1244 
1245  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1246  public extern static Z3_param_descrs Z3_tactic_get_param_descrs(Z3_context a0, Z3_tactic a1);
1247 
1248  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1249  public extern static IntPtr Z3_tactic_get_descr(Z3_context a0, string a1);
1250 
1251  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1252  public extern static IntPtr Z3_probe_get_descr(Z3_context a0, string a1);
1253 
1254  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1255  public extern static double Z3_probe_apply(Z3_context a0, Z3_probe a1, Z3_goal a2);
1256 
1257  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1258  public extern static Z3_apply_result Z3_tactic_apply(Z3_context a0, Z3_tactic a1, Z3_goal a2);
1259 
1260  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1261  public extern static Z3_apply_result Z3_tactic_apply_ex(Z3_context a0, Z3_tactic a1, Z3_goal a2, Z3_params a3);
1262 
1263  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1264  public extern static void Z3_apply_result_inc_ref(Z3_context a0, Z3_apply_result a1);
1265 
1266  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1267  public extern static void Z3_apply_result_dec_ref(Z3_context a0, Z3_apply_result a1);
1268 
1269  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1270  public extern static IntPtr Z3_apply_result_to_string(Z3_context a0, Z3_apply_result a1);
1271 
1272  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1273  public extern static uint Z3_apply_result_get_num_subgoals(Z3_context a0, Z3_apply_result a1);
1274 
1275  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1276  public extern static Z3_goal Z3_apply_result_get_subgoal(Z3_context a0, Z3_apply_result a1, uint a2);
1277 
1278  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1279  public extern static Z3_model Z3_apply_result_convert_model(Z3_context a0, Z3_apply_result a1, uint a2, Z3_model a3);
1280 
1281  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1282  public extern static Z3_solver Z3_mk_solver(Z3_context a0);
1283 
1284  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1285  public extern static Z3_solver Z3_mk_simple_solver(Z3_context a0);
1286 
1287  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1288  public extern static Z3_solver Z3_mk_solver_for_logic(Z3_context a0, IntPtr a1);
1289 
1290  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1291  public extern static Z3_solver Z3_mk_solver_from_tactic(Z3_context a0, Z3_tactic a1);
1292 
1293  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1294  public extern static IntPtr Z3_solver_get_help(Z3_context a0, Z3_solver a1);
1295 
1296  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1297  public extern static Z3_param_descrs Z3_solver_get_param_descrs(Z3_context a0, Z3_solver a1);
1298 
1299  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1300  public extern static void Z3_solver_set_params(Z3_context a0, Z3_solver a1, Z3_params a2);
1301 
1302  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1303  public extern static void Z3_solver_inc_ref(Z3_context a0, Z3_solver a1);
1304 
1305  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1306  public extern static void Z3_solver_dec_ref(Z3_context a0, Z3_solver a1);
1307 
1308  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1309  public extern static void Z3_solver_push(Z3_context a0, Z3_solver a1);
1310 
1311  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1312  public extern static void Z3_solver_pop(Z3_context a0, Z3_solver a1, uint a2);
1313 
1314  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1315  public extern static void Z3_solver_reset(Z3_context a0, Z3_solver a1);
1316 
1317  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1318  public extern static uint Z3_solver_get_num_scopes(Z3_context a0, Z3_solver a1);
1319 
1320  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1321  public extern static void Z3_solver_assert(Z3_context a0, Z3_solver a1, Z3_ast a2);
1322 
1323  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1324  public extern static void Z3_solver_assert_and_track(Z3_context a0, Z3_solver a1, Z3_ast a2, Z3_ast a3);
1325 
1326  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1327  public extern static Z3_ast_vector Z3_solver_get_assertions(Z3_context a0, Z3_solver a1);
1328 
1329  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1330  public extern static int Z3_solver_check(Z3_context a0, Z3_solver a1);
1331 
1332  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1333  public extern static int Z3_solver_check_assumptions(Z3_context a0, Z3_solver a1, uint a2, [In] Z3_ast[] a3);
1334 
1335  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1336  public extern static Z3_model Z3_solver_get_model(Z3_context a0, Z3_solver a1);
1337 
1338  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1339  public extern static Z3_ast Z3_solver_get_proof(Z3_context a0, Z3_solver a1);
1340 
1341  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1342  public extern static Z3_ast_vector Z3_solver_get_unsat_core(Z3_context a0, Z3_solver a1);
1343 
1344  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1345  public extern static IntPtr Z3_solver_get_reason_unknown(Z3_context a0, Z3_solver a1);
1346 
1347  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1348  public extern static Z3_stats Z3_solver_get_statistics(Z3_context a0, Z3_solver a1);
1349 
1350  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1351  public extern static IntPtr Z3_solver_to_string(Z3_context a0, Z3_solver a1);
1352 
1353  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1354  public extern static IntPtr Z3_stats_to_string(Z3_context a0, Z3_stats a1);
1355 
1356  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1357  public extern static void Z3_stats_inc_ref(Z3_context a0, Z3_stats a1);
1358 
1359  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1360  public extern static void Z3_stats_dec_ref(Z3_context a0, Z3_stats a1);
1361 
1362  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1363  public extern static uint Z3_stats_size(Z3_context a0, Z3_stats a1);
1364 
1365  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1366  public extern static IntPtr Z3_stats_get_key(Z3_context a0, Z3_stats a1, uint a2);
1367 
1368  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1369  public extern static int Z3_stats_is_uint(Z3_context a0, Z3_stats a1, uint a2);
1370 
1371  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1372  public extern static int Z3_stats_is_double(Z3_context a0, Z3_stats a1, uint a2);
1373 
1374  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1375  public extern static uint Z3_stats_get_uint_value(Z3_context a0, Z3_stats a1, uint a2);
1376 
1377  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1378  public extern static double Z3_stats_get_double_value(Z3_context a0, Z3_stats a1, uint a2);
1379 
1380  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1381  public extern static Z3_func_decl Z3_mk_injective_function(Z3_context a0, IntPtr a1, uint a2, [In] Z3_sort[] a3, Z3_sort a4);
1382 
1383  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1384  public extern static void Z3_set_logic(Z3_context a0, string a1);
1385 
1386  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1387  public extern static void Z3_push(Z3_context a0);
1388 
1389  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1390  public extern static void Z3_pop(Z3_context a0, uint a1);
1391 
1392  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1393  public extern static uint Z3_get_num_scopes(Z3_context a0);
1394 
1395  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1396  public extern static void Z3_persist_ast(Z3_context a0, Z3_ast a1, uint a2);
1397 
1398  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1399  public extern static void Z3_assert_cnstr(Z3_context a0, Z3_ast a1);
1400 
1401  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1402  public extern static int Z3_check_and_get_model(Z3_context a0, [In, Out] ref Z3_model a1);
1403 
1404  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1405  public extern static int Z3_check(Z3_context a0);
1406 
1407  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1408  public extern 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);
1409 
1410  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1411  public extern static uint Z3_get_implied_equalities(Z3_context a0, uint a1, [In] Z3_ast[] a2, [Out] uint[] a3);
1412 
1413  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1414  public extern static void Z3_del_model(Z3_context a0, Z3_model a1);
1415 
1416  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1417  public extern static void Z3_soft_check_cancel(Z3_context a0);
1418 
1419  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1420  public extern static uint Z3_get_search_failure(Z3_context a0);
1421 
1422  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1423  public extern static Z3_ast Z3_mk_label(Z3_context a0, IntPtr a1, int a2, Z3_ast a3);
1424 
1425  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1426  public extern static Z3_literals Z3_get_relevant_labels(Z3_context a0);
1427 
1428  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1429  public extern static Z3_literals Z3_get_relevant_literals(Z3_context a0);
1430 
1431  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1432  public extern static Z3_literals Z3_get_guessed_literals(Z3_context a0);
1433 
1434  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1435  public extern static void Z3_del_literals(Z3_context a0, Z3_literals a1);
1436 
1437  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1438  public extern static uint Z3_get_num_literals(Z3_context a0, Z3_literals a1);
1439 
1440  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1441  public extern static IntPtr Z3_get_label_symbol(Z3_context a0, Z3_literals a1, uint a2);
1442 
1443  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1444  public extern static Z3_ast Z3_get_literal(Z3_context a0, Z3_literals a1, uint a2);
1445 
1446  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1447  public extern static void Z3_disable_literal(Z3_context a0, Z3_literals a1, uint a2);
1448 
1449  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1450  public extern static void Z3_block_literals(Z3_context a0, Z3_literals a1);
1451 
1452  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1453  public extern static uint Z3_get_model_num_constants(Z3_context a0, Z3_model a1);
1454 
1455  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1456  public extern static Z3_func_decl Z3_get_model_constant(Z3_context a0, Z3_model a1, uint a2);
1457 
1458  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1459  public extern static uint Z3_get_model_num_funcs(Z3_context a0, Z3_model a1);
1460 
1461  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1462  public extern static Z3_func_decl Z3_get_model_func_decl(Z3_context a0, Z3_model a1, uint a2);
1463 
1464  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1465  public extern static int Z3_eval_func_decl(Z3_context a0, Z3_model a1, Z3_func_decl a2, [In, Out] ref Z3_ast a3);
1466 
1467  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1468  public extern static int Z3_is_array_value(Z3_context a0, Z3_model a1, Z3_ast a2, [In, Out] ref uint a3);
1469 
1470  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1471  public extern 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);
1472 
1473  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1474  public extern static Z3_ast Z3_get_model_func_else(Z3_context a0, Z3_model a1, uint a2);
1475 
1476  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1477  public extern static uint Z3_get_model_func_num_entries(Z3_context a0, Z3_model a1, uint a2);
1478 
1479  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1480  public extern static uint Z3_get_model_func_entry_num_args(Z3_context a0, Z3_model a1, uint a2, uint a3);
1481 
1482  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1483  public extern static Z3_ast Z3_get_model_func_entry_arg(Z3_context a0, Z3_model a1, uint a2, uint a3, uint a4);
1484 
1485  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1486  public extern static Z3_ast Z3_get_model_func_entry_value(Z3_context a0, Z3_model a1, uint a2, uint a3);
1487 
1488  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1489  public extern static int Z3_eval(Z3_context a0, Z3_model a1, Z3_ast a2, [In, Out] ref Z3_ast a3);
1490 
1491  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1492  public extern 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);
1493 
1494  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1495  public extern static IntPtr Z3_context_to_string(Z3_context a0);
1496 
1497  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1498  public extern static IntPtr Z3_statistics_to_string(Z3_context a0);
1499 
1500  [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1501  public extern static Z3_ast Z3_get_context_assignment(Z3_context a0);
1502 
1503  }
1504 
1505  public static void Z3_set_error_handler(Z3_context a0, Z3_error_handler a1) {
1506  LIB.Z3_set_error_handler(a0, a1);
1507  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1508  if (err != Z3_error_code.Z3_OK)
1509  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1510  }
1511 
1512  public static Z3_config Z3_mk_config() {
1513  Z3_config r = LIB.Z3_mk_config();
1514  return r;
1515  }
1516 
1517  public static void Z3_del_config(Z3_config a0) {
1518  LIB.Z3_del_config(a0);
1519  }
1520 
1521  public static void Z3_set_param_value(Z3_config a0, string a1, string a2) {
1522  LIB.Z3_set_param_value(a0, a1, a2);
1523  }
1524 
1525  public static Z3_context Z3_mk_context(Z3_config a0) {
1526  Z3_context r = LIB.Z3_mk_context(a0);
1527  return r;
1528  }
1529 
1530  public static Z3_context Z3_mk_context_rc(Z3_config a0) {
1531  Z3_context r = LIB.Z3_mk_context_rc(a0);
1532  return r;
1533  }
1534 
1535  public static void Z3_del_context(Z3_context a0) {
1536  LIB.Z3_del_context(a0);
1537  }
1538 
1539  public static void Z3_inc_ref(Z3_context a0, Z3_ast a1) {
1540  LIB.Z3_inc_ref(a0, a1);
1541  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1542  if (err != Z3_error_code.Z3_OK)
1543  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1544  }
1545 
1546  public static void Z3_dec_ref(Z3_context a0, Z3_ast a1) {
1547  LIB.Z3_dec_ref(a0, a1);
1548  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1549  if (err != Z3_error_code.Z3_OK)
1550  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1551  }
1552 
1553  public static void Z3_update_param_value(Z3_context a0, string a1, string a2) {
1554  LIB.Z3_update_param_value(a0, a1, a2);
1555  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1556  if (err != Z3_error_code.Z3_OK)
1557  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1558  }
1559 
1560  public static int Z3_get_param_value(Z3_context a0, string a1, out IntPtr a2) {
1561  int r = LIB.Z3_get_param_value(a0, a1, out a2);
1562  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1563  if (err != Z3_error_code.Z3_OK)
1564  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1565  return r;
1566  }
1567 
1568  public static void Z3_interrupt(Z3_context a0) {
1569  LIB.Z3_interrupt(a0);
1570  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1571  if (err != Z3_error_code.Z3_OK)
1572  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1573  }
1574 
1575  public static Z3_params Z3_mk_params(Z3_context a0) {
1576  Z3_params r = LIB.Z3_mk_params(a0);
1577  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1578  if (err != Z3_error_code.Z3_OK)
1579  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1580  return r;
1581  }
1582 
1583  public static void Z3_params_inc_ref(Z3_context a0, Z3_params a1) {
1584  LIB.Z3_params_inc_ref(a0, a1);
1585  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1586  if (err != Z3_error_code.Z3_OK)
1587  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1588  }
1589 
1590  public static void Z3_params_dec_ref(Z3_context a0, Z3_params a1) {
1591  LIB.Z3_params_dec_ref(a0, a1);
1592  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1593  if (err != Z3_error_code.Z3_OK)
1594  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1595  }
1596 
1597  public static void Z3_params_set_bool(Z3_context a0, Z3_params a1, IntPtr a2, int a3) {
1598  LIB.Z3_params_set_bool(a0, a1, a2, a3);
1599  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1600  if (err != Z3_error_code.Z3_OK)
1601  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1602  }
1603 
1604  public static void Z3_params_set_uint(Z3_context a0, Z3_params a1, IntPtr a2, uint a3) {
1605  LIB.Z3_params_set_uint(a0, a1, a2, a3);
1606  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1607  if (err != Z3_error_code.Z3_OK)
1608  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1609  }
1610 
1611  public static void Z3_params_set_double(Z3_context a0, Z3_params a1, IntPtr a2, double a3) {
1612  LIB.Z3_params_set_double(a0, a1, a2, a3);
1613  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1614  if (err != Z3_error_code.Z3_OK)
1615  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1616  }
1617 
1618  public static void Z3_params_set_symbol(Z3_context a0, Z3_params a1, IntPtr a2, IntPtr a3) {
1619  LIB.Z3_params_set_symbol(a0, a1, a2, a3);
1620  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1621  if (err != Z3_error_code.Z3_OK)
1622  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1623  }
1624 
1625  public static string Z3_params_to_string(Z3_context a0, Z3_params a1) {
1626  IntPtr r = LIB.Z3_params_to_string(a0, a1);
1627  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1628  if (err != Z3_error_code.Z3_OK)
1629  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1630  return Marshal.PtrToStringAnsi(r);
1631  }
1632 
1633  public static void Z3_params_validate(Z3_context a0, Z3_params a1, Z3_param_descrs a2) {
1634  LIB.Z3_params_validate(a0, a1, a2);
1635  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1636  if (err != Z3_error_code.Z3_OK)
1637  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1638  }
1639 
1640  public static void Z3_param_descrs_inc_ref(Z3_context a0, Z3_param_descrs a1) {
1641  LIB.Z3_param_descrs_inc_ref(a0, a1);
1642  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1643  if (err != Z3_error_code.Z3_OK)
1644  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1645  }
1646 
1647  public static void Z3_param_descrs_dec_ref(Z3_context a0, Z3_param_descrs a1) {
1648  LIB.Z3_param_descrs_dec_ref(a0, a1);
1649  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1650  if (err != Z3_error_code.Z3_OK)
1651  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1652  }
1653 
1654  public static uint Z3_param_descrs_get_kind(Z3_context a0, Z3_param_descrs a1, IntPtr a2) {
1655  uint r = LIB.Z3_param_descrs_get_kind(a0, a1, a2);
1656  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1657  if (err != Z3_error_code.Z3_OK)
1658  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1659  return r;
1660  }
1661 
1662  public static uint Z3_param_descrs_size(Z3_context a0, Z3_param_descrs a1) {
1663  uint r = LIB.Z3_param_descrs_size(a0, a1);
1664  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1665  if (err != Z3_error_code.Z3_OK)
1666  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1667  return r;
1668  }
1669 
1670  public static IntPtr Z3_param_descrs_get_name(Z3_context a0, Z3_param_descrs a1, uint a2) {
1671  IntPtr r = LIB.Z3_param_descrs_get_name(a0, a1, a2);
1672  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1673  if (err != Z3_error_code.Z3_OK)
1674  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1675  return r;
1676  }
1677 
1678  public static string Z3_param_descrs_to_string(Z3_context a0, Z3_param_descrs a1) {
1679  IntPtr r = LIB.Z3_param_descrs_to_string(a0, a1);
1680  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1681  if (err != Z3_error_code.Z3_OK)
1682  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1683  return Marshal.PtrToStringAnsi(r);
1684  }
1685 
1686  public static IntPtr Z3_mk_int_symbol(Z3_context a0, int a1) {
1687  IntPtr r = LIB.Z3_mk_int_symbol(a0, a1);
1688  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1689  if (err != Z3_error_code.Z3_OK)
1690  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1691  return r;
1692  }
1693 
1694  public static IntPtr Z3_mk_string_symbol(Z3_context a0, string a1) {
1695  IntPtr r = LIB.Z3_mk_string_symbol(a0, a1);
1696  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1697  if (err != Z3_error_code.Z3_OK)
1698  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1699  return r;
1700  }
1701 
1702  public static Z3_sort Z3_mk_uninterpreted_sort(Z3_context a0, IntPtr a1) {
1703  Z3_sort r = LIB.Z3_mk_uninterpreted_sort(a0, a1);
1704  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1705  if (err != Z3_error_code.Z3_OK)
1706  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1707  return r;
1708  }
1709 
1710  public static Z3_sort Z3_mk_bool_sort(Z3_context a0) {
1711  Z3_sort r = LIB.Z3_mk_bool_sort(a0);
1712  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1713  if (err != Z3_error_code.Z3_OK)
1714  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1715  return r;
1716  }
1717 
1718  public static Z3_sort Z3_mk_int_sort(Z3_context a0) {
1719  Z3_sort r = LIB.Z3_mk_int_sort(a0);
1720  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1721  if (err != Z3_error_code.Z3_OK)
1722  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1723  return r;
1724  }
1725 
1726  public static Z3_sort Z3_mk_real_sort(Z3_context a0) {
1727  Z3_sort r = LIB.Z3_mk_real_sort(a0);
1728  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1729  if (err != Z3_error_code.Z3_OK)
1730  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1731  return r;
1732  }
1733 
1734  public static Z3_sort Z3_mk_bv_sort(Z3_context a0, uint a1) {
1735  Z3_sort r = LIB.Z3_mk_bv_sort(a0, a1);
1736  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1737  if (err != Z3_error_code.Z3_OK)
1738  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1739  return r;
1740  }
1741 
1742  public static Z3_sort Z3_mk_finite_domain_sort(Z3_context a0, IntPtr a1, UInt64 a2) {
1743  Z3_sort r = LIB.Z3_mk_finite_domain_sort(a0, a1, a2);
1744  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1745  if (err != Z3_error_code.Z3_OK)
1746  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1747  return r;
1748  }
1749 
1750  public static Z3_sort Z3_mk_array_sort(Z3_context a0, Z3_sort a1, Z3_sort a2) {
1751  Z3_sort r = LIB.Z3_mk_array_sort(a0, a1, a2);
1752  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1753  if (err != Z3_error_code.Z3_OK)
1754  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1755  return r;
1756  }
1757 
1758  public 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) {
1759  Z3_sort r = LIB.Z3_mk_tuple_sort(a0, a1, a2, a3, a4, ref a5, a6);
1760  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1761  if (err != Z3_error_code.Z3_OK)
1762  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1763  return r;
1764  }
1765 
1766  public 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) {
1767  Z3_sort r = LIB.Z3_mk_enumeration_sort(a0, a1, a2, a3, a4, a5);
1768  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1769  if (err != Z3_error_code.Z3_OK)
1770  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1771  return r;
1772  }
1773 
1774  public 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) {
1775  Z3_sort r = LIB.Z3_mk_list_sort(a0, a1, a2, ref a3, ref a4, ref a5, ref a6, ref a7, ref a8);
1776  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1777  if (err != Z3_error_code.Z3_OK)
1778  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1779  return r;
1780  }
1781 
1782  public 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) {
1783  Z3_constructor r = LIB.Z3_mk_constructor(a0, a1, a2, a3, a4, a5, a6);
1784  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1785  if (err != Z3_error_code.Z3_OK)
1786  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1787  return r;
1788  }
1789 
1790  public static void Z3_del_constructor(Z3_context a0, Z3_constructor a1) {
1791  LIB.Z3_del_constructor(a0, a1);
1792  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1793  if (err != Z3_error_code.Z3_OK)
1794  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1795  }
1796 
1797  public static Z3_sort Z3_mk_datatype(Z3_context a0, IntPtr a1, uint a2, [In, Out] Z3_constructor[] a3) {
1798  Z3_sort r = LIB.Z3_mk_datatype(a0, a1, a2, a3);
1799  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1800  if (err != Z3_error_code.Z3_OK)
1801  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1802  return r;
1803  }
1804 
1805  public static Z3_constructor_list Z3_mk_constructor_list(Z3_context a0, uint a1, [In] Z3_constructor[] a2) {
1806  Z3_constructor_list r = LIB.Z3_mk_constructor_list(a0, a1, a2);
1807  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1808  if (err != Z3_error_code.Z3_OK)
1809  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1810  return r;
1811  }
1812 
1813  public static void Z3_del_constructor_list(Z3_context a0, Z3_constructor_list a1) {
1814  LIB.Z3_del_constructor_list(a0, a1);
1815  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1816  if (err != Z3_error_code.Z3_OK)
1817  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1818  }
1819 
1820  public static void Z3_mk_datatypes(Z3_context a0, uint a1, [In] IntPtr[] a2, [Out] Z3_sort[] a3, [In, Out] Z3_constructor_list[] a4) {
1821  LIB.Z3_mk_datatypes(a0, a1, a2, a3, a4);
1822  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1823  if (err != Z3_error_code.Z3_OK)
1824  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1825  }
1826 
1827  public 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) {
1828  LIB.Z3_query_constructor(a0, a1, a2, ref a3, ref a4, a5);
1829  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1830  if (err != Z3_error_code.Z3_OK)
1831  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1832  }
1833 
1834  public static Z3_func_decl Z3_mk_func_decl(Z3_context a0, IntPtr a1, uint a2, [In] Z3_sort[] a3, Z3_sort a4) {
1835  Z3_func_decl r = LIB.Z3_mk_func_decl(a0, a1, a2, a3, a4);
1836  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1837  if (err != Z3_error_code.Z3_OK)
1838  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1839  return r;
1840  }
1841 
1842  public static Z3_ast Z3_mk_app(Z3_context a0, Z3_func_decl a1, uint a2, [In] Z3_ast[] a3) {
1843  Z3_ast r = LIB.Z3_mk_app(a0, a1, a2, a3);
1844  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1845  if (err != Z3_error_code.Z3_OK)
1846  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1847  return r;
1848  }
1849 
1850  public static Z3_ast Z3_mk_const(Z3_context a0, IntPtr a1, Z3_sort a2) {
1851  Z3_ast r = LIB.Z3_mk_const(a0, a1, a2);
1852  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1853  if (err != Z3_error_code.Z3_OK)
1854  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1855  return r;
1856  }
1857 
1858  public static Z3_func_decl Z3_mk_fresh_func_decl(Z3_context a0, string a1, uint a2, [In] Z3_sort[] a3, Z3_sort a4) {
1859  Z3_func_decl r = LIB.Z3_mk_fresh_func_decl(a0, a1, a2, a3, a4);
1860  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1861  if (err != Z3_error_code.Z3_OK)
1862  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1863  return r;
1864  }
1865 
1866  public static Z3_ast Z3_mk_fresh_const(Z3_context a0, string a1, Z3_sort a2) {
1867  Z3_ast r = LIB.Z3_mk_fresh_const(a0, a1, a2);
1868  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1869  if (err != Z3_error_code.Z3_OK)
1870  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1871  return r;
1872  }
1873 
1874  public static Z3_ast Z3_mk_true(Z3_context a0) {
1875  Z3_ast r = LIB.Z3_mk_true(a0);
1876  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1877  if (err != Z3_error_code.Z3_OK)
1878  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1879  return r;
1880  }
1881 
1882  public static Z3_ast Z3_mk_false(Z3_context a0) {
1883  Z3_ast r = LIB.Z3_mk_false(a0);
1884  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1885  if (err != Z3_error_code.Z3_OK)
1886  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1887  return r;
1888  }
1889 
1890  public static Z3_ast Z3_mk_eq(Z3_context a0, Z3_ast a1, Z3_ast a2) {
1891  Z3_ast r = LIB.Z3_mk_eq(a0, a1, a2);
1892  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1893  if (err != Z3_error_code.Z3_OK)
1894  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1895  return r;
1896  }
1897 
1898  public static Z3_ast Z3_mk_distinct(Z3_context a0, uint a1, [In] Z3_ast[] a2) {
1899  Z3_ast r = LIB.Z3_mk_distinct(a0, a1, a2);
1900  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1901  if (err != Z3_error_code.Z3_OK)
1902  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1903  return r;
1904  }
1905 
1906  public static Z3_ast Z3_mk_not(Z3_context a0, Z3_ast a1) {
1907  Z3_ast r = LIB.Z3_mk_not(a0, a1);
1908  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1909  if (err != Z3_error_code.Z3_OK)
1910  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1911  return r;
1912  }
1913 
1914  public static Z3_ast Z3_mk_ite(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3) {
1915  Z3_ast r = LIB.Z3_mk_ite(a0, a1, a2, a3);
1916  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1917  if (err != Z3_error_code.Z3_OK)
1918  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1919  return r;
1920  }
1921 
1922  public static Z3_ast Z3_mk_iff(Z3_context a0, Z3_ast a1, Z3_ast a2) {
1923  Z3_ast r = LIB.Z3_mk_iff(a0, a1, a2);
1924  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1925  if (err != Z3_error_code.Z3_OK)
1926  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1927  return r;
1928  }
1929 
1930  public static Z3_ast Z3_mk_implies(Z3_context a0, Z3_ast a1, Z3_ast a2) {
1931  Z3_ast r = LIB.Z3_mk_implies(a0, a1, a2);
1932  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1933  if (err != Z3_error_code.Z3_OK)
1934  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1935  return r;
1936  }
1937 
1938  public static Z3_ast Z3_mk_xor(Z3_context a0, Z3_ast a1, Z3_ast a2) {
1939  Z3_ast r = LIB.Z3_mk_xor(a0, a1, a2);
1940  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1941  if (err != Z3_error_code.Z3_OK)
1942  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1943  return r;
1944  }
1945 
1946  public static Z3_ast Z3_mk_and(Z3_context a0, uint a1, [In] Z3_ast[] a2) {
1947  Z3_ast r = LIB.Z3_mk_and(a0, a1, a2);
1948  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1949  if (err != Z3_error_code.Z3_OK)
1950  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1951  return r;
1952  }
1953 
1954  public static Z3_ast Z3_mk_or(Z3_context a0, uint a1, [In] Z3_ast[] a2) {
1955  Z3_ast r = LIB.Z3_mk_or(a0, a1, a2);
1956  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1957  if (err != Z3_error_code.Z3_OK)
1958  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1959  return r;
1960  }
1961 
1962  public static Z3_ast Z3_mk_add(Z3_context a0, uint a1, [In] Z3_ast[] a2) {
1963  Z3_ast r = LIB.Z3_mk_add(a0, a1, a2);
1964  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1965  if (err != Z3_error_code.Z3_OK)
1966  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1967  return r;
1968  }
1969 
1970  public static Z3_ast Z3_mk_mul(Z3_context a0, uint a1, [In] Z3_ast[] a2) {
1971  Z3_ast r = LIB.Z3_mk_mul(a0, a1, a2);
1972  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1973  if (err != Z3_error_code.Z3_OK)
1974  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1975  return r;
1976  }
1977 
1978  public static Z3_ast Z3_mk_sub(Z3_context a0, uint a1, [In] Z3_ast[] a2) {
1979  Z3_ast r = LIB.Z3_mk_sub(a0, a1, a2);
1980  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1981  if (err != Z3_error_code.Z3_OK)
1982  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1983  return r;
1984  }
1985 
1986  public static Z3_ast Z3_mk_unary_minus(Z3_context a0, Z3_ast a1) {
1987  Z3_ast r = LIB.Z3_mk_unary_minus(a0, a1);
1988  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1989  if (err != Z3_error_code.Z3_OK)
1990  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1991  return r;
1992  }
1993 
1994  public static Z3_ast Z3_mk_div(Z3_context a0, Z3_ast a1, Z3_ast a2) {
1995  Z3_ast r = LIB.Z3_mk_div(a0, a1, a2);
1996  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
1997  if (err != Z3_error_code.Z3_OK)
1998  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
1999  return r;
2000  }
2001 
2002  public static Z3_ast Z3_mk_mod(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2003  Z3_ast r = LIB.Z3_mk_mod(a0, a1, a2);
2004  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2005  if (err != Z3_error_code.Z3_OK)
2006  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2007  return r;
2008  }
2009 
2010  public static Z3_ast Z3_mk_rem(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2011  Z3_ast r = LIB.Z3_mk_rem(a0, a1, a2);
2012  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2013  if (err != Z3_error_code.Z3_OK)
2014  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2015  return r;
2016  }
2017 
2018  public static Z3_ast Z3_mk_power(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2019  Z3_ast r = LIB.Z3_mk_power(a0, a1, a2);
2020  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2021  if (err != Z3_error_code.Z3_OK)
2022  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2023  return r;
2024  }
2025 
2026  public static Z3_ast Z3_mk_lt(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2027  Z3_ast r = LIB.Z3_mk_lt(a0, a1, a2);
2028  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2029  if (err != Z3_error_code.Z3_OK)
2030  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2031  return r;
2032  }
2033 
2034  public static Z3_ast Z3_mk_le(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2035  Z3_ast r = LIB.Z3_mk_le(a0, a1, a2);
2036  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2037  if (err != Z3_error_code.Z3_OK)
2038  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2039  return r;
2040  }
2041 
2042  public static Z3_ast Z3_mk_gt(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2043  Z3_ast r = LIB.Z3_mk_gt(a0, a1, a2);
2044  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2045  if (err != Z3_error_code.Z3_OK)
2046  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2047  return r;
2048  }
2049 
2050  public static Z3_ast Z3_mk_ge(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2051  Z3_ast r = LIB.Z3_mk_ge(a0, a1, a2);
2052  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2053  if (err != Z3_error_code.Z3_OK)
2054  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2055  return r;
2056  }
2057 
2058  public static Z3_ast Z3_mk_int2real(Z3_context a0, Z3_ast a1) {
2059  Z3_ast r = LIB.Z3_mk_int2real(a0, a1);
2060  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2061  if (err != Z3_error_code.Z3_OK)
2062  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2063  return r;
2064  }
2065 
2066  public static Z3_ast Z3_mk_real2int(Z3_context a0, Z3_ast a1) {
2067  Z3_ast r = LIB.Z3_mk_real2int(a0, a1);
2068  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2069  if (err != Z3_error_code.Z3_OK)
2070  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2071  return r;
2072  }
2073 
2074  public static Z3_ast Z3_mk_is_int(Z3_context a0, Z3_ast a1) {
2075  Z3_ast r = LIB.Z3_mk_is_int(a0, a1);
2076  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2077  if (err != Z3_error_code.Z3_OK)
2078  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2079  return r;
2080  }
2081 
2082  public static Z3_ast Z3_mk_bvnot(Z3_context a0, Z3_ast a1) {
2083  Z3_ast r = LIB.Z3_mk_bvnot(a0, a1);
2084  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2085  if (err != Z3_error_code.Z3_OK)
2086  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2087  return r;
2088  }
2089 
2090  public static Z3_ast Z3_mk_bvredand(Z3_context a0, Z3_ast a1) {
2091  Z3_ast r = LIB.Z3_mk_bvredand(a0, a1);
2092  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2093  if (err != Z3_error_code.Z3_OK)
2094  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2095  return r;
2096  }
2097 
2098  public static Z3_ast Z3_mk_bvredor(Z3_context a0, Z3_ast a1) {
2099  Z3_ast r = LIB.Z3_mk_bvredor(a0, a1);
2100  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2101  if (err != Z3_error_code.Z3_OK)
2102  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2103  return r;
2104  }
2105 
2106  public static Z3_ast Z3_mk_bvand(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2107  Z3_ast r = LIB.Z3_mk_bvand(a0, a1, a2);
2108  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2109  if (err != Z3_error_code.Z3_OK)
2110  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2111  return r;
2112  }
2113 
2114  public static Z3_ast Z3_mk_bvor(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2115  Z3_ast r = LIB.Z3_mk_bvor(a0, a1, a2);
2116  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2117  if (err != Z3_error_code.Z3_OK)
2118  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2119  return r;
2120  }
2121 
2122  public static Z3_ast Z3_mk_bvxor(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2123  Z3_ast r = LIB.Z3_mk_bvxor(a0, a1, a2);
2124  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2125  if (err != Z3_error_code.Z3_OK)
2126  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2127  return r;
2128  }
2129 
2130  public static Z3_ast Z3_mk_bvnand(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2131  Z3_ast r = LIB.Z3_mk_bvnand(a0, a1, a2);
2132  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2133  if (err != Z3_error_code.Z3_OK)
2134  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2135  return r;
2136  }
2137 
2138  public static Z3_ast Z3_mk_bvnor(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2139  Z3_ast r = LIB.Z3_mk_bvnor(a0, a1, a2);
2140  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2141  if (err != Z3_error_code.Z3_OK)
2142  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2143  return r;
2144  }
2145 
2146  public static Z3_ast Z3_mk_bvxnor(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2147  Z3_ast r = LIB.Z3_mk_bvxnor(a0, a1, a2);
2148  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2149  if (err != Z3_error_code.Z3_OK)
2150  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2151  return r;
2152  }
2153 
2154  public static Z3_ast Z3_mk_bvneg(Z3_context a0, Z3_ast a1) {
2155  Z3_ast r = LIB.Z3_mk_bvneg(a0, a1);
2156  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2157  if (err != Z3_error_code.Z3_OK)
2158  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2159  return r;
2160  }
2161 
2162  public static Z3_ast Z3_mk_bvadd(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2163  Z3_ast r = LIB.Z3_mk_bvadd(a0, a1, a2);
2164  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2165  if (err != Z3_error_code.Z3_OK)
2166  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2167  return r;
2168  }
2169 
2170  public static Z3_ast Z3_mk_bvsub(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2171  Z3_ast r = LIB.Z3_mk_bvsub(a0, a1, a2);
2172  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2173  if (err != Z3_error_code.Z3_OK)
2174  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2175  return r;
2176  }
2177 
2178  public static Z3_ast Z3_mk_bvmul(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2179  Z3_ast r = LIB.Z3_mk_bvmul(a0, a1, a2);
2180  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2181  if (err != Z3_error_code.Z3_OK)
2182  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2183  return r;
2184  }
2185 
2186  public static Z3_ast Z3_mk_bvudiv(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2187  Z3_ast r = LIB.Z3_mk_bvudiv(a0, a1, a2);
2188  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2189  if (err != Z3_error_code.Z3_OK)
2190  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2191  return r;
2192  }
2193 
2194  public static Z3_ast Z3_mk_bvsdiv(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2195  Z3_ast r = LIB.Z3_mk_bvsdiv(a0, a1, a2);
2196  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2197  if (err != Z3_error_code.Z3_OK)
2198  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2199  return r;
2200  }
2201 
2202  public static Z3_ast Z3_mk_bvurem(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2203  Z3_ast r = LIB.Z3_mk_bvurem(a0, a1, a2);
2204  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2205  if (err != Z3_error_code.Z3_OK)
2206  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2207  return r;
2208  }
2209 
2210  public static Z3_ast Z3_mk_bvsrem(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2211  Z3_ast r = LIB.Z3_mk_bvsrem(a0, a1, a2);
2212  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2213  if (err != Z3_error_code.Z3_OK)
2214  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2215  return r;
2216  }
2217 
2218  public static Z3_ast Z3_mk_bvsmod(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2219  Z3_ast r = LIB.Z3_mk_bvsmod(a0, a1, a2);
2220  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2221  if (err != Z3_error_code.Z3_OK)
2222  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2223  return r;
2224  }
2225 
2226  public static Z3_ast Z3_mk_bvult(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2227  Z3_ast r = LIB.Z3_mk_bvult(a0, a1, a2);
2228  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2229  if (err != Z3_error_code.Z3_OK)
2230  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2231  return r;
2232  }
2233 
2234  public static Z3_ast Z3_mk_bvslt(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2235  Z3_ast r = LIB.Z3_mk_bvslt(a0, a1, a2);
2236  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2237  if (err != Z3_error_code.Z3_OK)
2238  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2239  return r;
2240  }
2241 
2242  public static Z3_ast Z3_mk_bvule(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2243  Z3_ast r = LIB.Z3_mk_bvule(a0, a1, a2);
2244  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2245  if (err != Z3_error_code.Z3_OK)
2246  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2247  return r;
2248  }
2249 
2250  public static Z3_ast Z3_mk_bvsle(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2251  Z3_ast r = LIB.Z3_mk_bvsle(a0, a1, a2);
2252  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2253  if (err != Z3_error_code.Z3_OK)
2254  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2255  return r;
2256  }
2257 
2258  public static Z3_ast Z3_mk_bvuge(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2259  Z3_ast r = LIB.Z3_mk_bvuge(a0, a1, a2);
2260  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2261  if (err != Z3_error_code.Z3_OK)
2262  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2263  return r;
2264  }
2265 
2266  public static Z3_ast Z3_mk_bvsge(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2267  Z3_ast r = LIB.Z3_mk_bvsge(a0, a1, a2);
2268  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2269  if (err != Z3_error_code.Z3_OK)
2270  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2271  return r;
2272  }
2273 
2274  public static Z3_ast Z3_mk_bvugt(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2275  Z3_ast r = LIB.Z3_mk_bvugt(a0, a1, a2);
2276  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2277  if (err != Z3_error_code.Z3_OK)
2278  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2279  return r;
2280  }
2281 
2282  public static Z3_ast Z3_mk_bvsgt(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2283  Z3_ast r = LIB.Z3_mk_bvsgt(a0, a1, a2);
2284  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2285  if (err != Z3_error_code.Z3_OK)
2286  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2287  return r;
2288  }
2289 
2290  public static Z3_ast Z3_mk_concat(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2291  Z3_ast r = LIB.Z3_mk_concat(a0, a1, a2);
2292  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2293  if (err != Z3_error_code.Z3_OK)
2294  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2295  return r;
2296  }
2297 
2298  public static Z3_ast Z3_mk_extract(Z3_context a0, uint a1, uint a2, Z3_ast a3) {
2299  Z3_ast r = LIB.Z3_mk_extract(a0, a1, a2, a3);
2300  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2301  if (err != Z3_error_code.Z3_OK)
2302  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2303  return r;
2304  }
2305 
2306  public static Z3_ast Z3_mk_sign_ext(Z3_context a0, uint a1, Z3_ast a2) {
2307  Z3_ast r = LIB.Z3_mk_sign_ext(a0, a1, a2);
2308  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2309  if (err != Z3_error_code.Z3_OK)
2310  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2311  return r;
2312  }
2313 
2314  public static Z3_ast Z3_mk_zero_ext(Z3_context a0, uint a1, Z3_ast a2) {
2315  Z3_ast r = LIB.Z3_mk_zero_ext(a0, a1, a2);
2316  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2317  if (err != Z3_error_code.Z3_OK)
2318  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2319  return r;
2320  }
2321 
2322  public static Z3_ast Z3_mk_repeat(Z3_context a0, uint a1, Z3_ast a2) {
2323  Z3_ast r = LIB.Z3_mk_repeat(a0, a1, a2);
2324  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2325  if (err != Z3_error_code.Z3_OK)
2326  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2327  return r;
2328  }
2329 
2330  public static Z3_ast Z3_mk_bvshl(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2331  Z3_ast r = LIB.Z3_mk_bvshl(a0, a1, a2);
2332  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2333  if (err != Z3_error_code.Z3_OK)
2334  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2335  return r;
2336  }
2337 
2338  public static Z3_ast Z3_mk_bvlshr(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2339  Z3_ast r = LIB.Z3_mk_bvlshr(a0, a1, a2);
2340  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2341  if (err != Z3_error_code.Z3_OK)
2342  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2343  return r;
2344  }
2345 
2346  public static Z3_ast Z3_mk_bvashr(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2347  Z3_ast r = LIB.Z3_mk_bvashr(a0, a1, a2);
2348  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2349  if (err != Z3_error_code.Z3_OK)
2350  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2351  return r;
2352  }
2353 
2354  public static Z3_ast Z3_mk_rotate_left(Z3_context a0, uint a1, Z3_ast a2) {
2355  Z3_ast r = LIB.Z3_mk_rotate_left(a0, a1, a2);
2356  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2357  if (err != Z3_error_code.Z3_OK)
2358  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2359  return r;
2360  }
2361 
2362  public static Z3_ast Z3_mk_rotate_right(Z3_context a0, uint a1, Z3_ast a2) {
2363  Z3_ast r = LIB.Z3_mk_rotate_right(a0, a1, a2);
2364  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2365  if (err != Z3_error_code.Z3_OK)
2366  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2367  return r;
2368  }
2369 
2370  public static Z3_ast Z3_mk_ext_rotate_left(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2371  Z3_ast r = LIB.Z3_mk_ext_rotate_left(a0, a1, a2);
2372  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2373  if (err != Z3_error_code.Z3_OK)
2374  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2375  return r;
2376  }
2377 
2378  public static Z3_ast Z3_mk_ext_rotate_right(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2379  Z3_ast r = LIB.Z3_mk_ext_rotate_right(a0, a1, a2);
2380  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2381  if (err != Z3_error_code.Z3_OK)
2382  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2383  return r;
2384  }
2385 
2386  public static Z3_ast Z3_mk_int2bv(Z3_context a0, uint a1, Z3_ast a2) {
2387  Z3_ast r = LIB.Z3_mk_int2bv(a0, a1, a2);
2388  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2389  if (err != Z3_error_code.Z3_OK)
2390  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2391  return r;
2392  }
2393 
2394  public static Z3_ast Z3_mk_bv2int(Z3_context a0, Z3_ast a1, int a2) {
2395  Z3_ast r = LIB.Z3_mk_bv2int(a0, a1, a2);
2396  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2397  if (err != Z3_error_code.Z3_OK)
2398  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2399  return r;
2400  }
2401 
2402  public static Z3_ast Z3_mk_bvadd_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2, int a3) {
2403  Z3_ast r = LIB.Z3_mk_bvadd_no_overflow(a0, a1, a2, a3);
2404  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2405  if (err != Z3_error_code.Z3_OK)
2406  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2407  return r;
2408  }
2409 
2410  public static Z3_ast Z3_mk_bvadd_no_underflow(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2411  Z3_ast r = LIB.Z3_mk_bvadd_no_underflow(a0, a1, a2);
2412  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2413  if (err != Z3_error_code.Z3_OK)
2414  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2415  return r;
2416  }
2417 
2418  public static Z3_ast Z3_mk_bvsub_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2419  Z3_ast r = LIB.Z3_mk_bvsub_no_overflow(a0, a1, a2);
2420  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2421  if (err != Z3_error_code.Z3_OK)
2422  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2423  return r;
2424  }
2425 
2426  public static Z3_ast Z3_mk_bvsub_no_underflow(Z3_context a0, Z3_ast a1, Z3_ast a2, int a3) {
2427  Z3_ast r = LIB.Z3_mk_bvsub_no_underflow(a0, a1, a2, a3);
2428  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2429  if (err != Z3_error_code.Z3_OK)
2430  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2431  return r;
2432  }
2433 
2434  public static Z3_ast Z3_mk_bvsdiv_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2435  Z3_ast r = LIB.Z3_mk_bvsdiv_no_overflow(a0, a1, a2);
2436  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2437  if (err != Z3_error_code.Z3_OK)
2438  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2439  return r;
2440  }
2441 
2442  public static Z3_ast Z3_mk_bvneg_no_overflow(Z3_context a0, Z3_ast a1) {
2443  Z3_ast r = LIB.Z3_mk_bvneg_no_overflow(a0, a1);
2444  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2445  if (err != Z3_error_code.Z3_OK)
2446  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2447  return r;
2448  }
2449 
2450  public static Z3_ast Z3_mk_bvmul_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2, int a3) {
2451  Z3_ast r = LIB.Z3_mk_bvmul_no_overflow(a0, a1, a2, a3);
2452  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2453  if (err != Z3_error_code.Z3_OK)
2454  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2455  return r;
2456  }
2457 
2458  public static Z3_ast Z3_mk_bvmul_no_underflow(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2459  Z3_ast r = LIB.Z3_mk_bvmul_no_underflow(a0, a1, a2);
2460  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2461  if (err != Z3_error_code.Z3_OK)
2462  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2463  return r;
2464  }
2465 
2466  public static Z3_ast Z3_mk_select(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2467  Z3_ast r = LIB.Z3_mk_select(a0, a1, a2);
2468  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2469  if (err != Z3_error_code.Z3_OK)
2470  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2471  return r;
2472  }
2473 
2474  public static Z3_ast Z3_mk_store(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3) {
2475  Z3_ast r = LIB.Z3_mk_store(a0, a1, a2, a3);
2476  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2477  if (err != Z3_error_code.Z3_OK)
2478  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2479  return r;
2480  }
2481 
2482  public static Z3_ast Z3_mk_const_array(Z3_context a0, Z3_sort a1, Z3_ast a2) {
2483  Z3_ast r = LIB.Z3_mk_const_array(a0, a1, a2);
2484  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2485  if (err != Z3_error_code.Z3_OK)
2486  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2487  return r;
2488  }
2489 
2490  public static Z3_ast Z3_mk_map(Z3_context a0, Z3_func_decl a1, uint a2, [In] Z3_ast[] a3) {
2491  Z3_ast r = LIB.Z3_mk_map(a0, a1, a2, a3);
2492  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2493  if (err != Z3_error_code.Z3_OK)
2494  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2495  return r;
2496  }
2497 
2498  public static Z3_ast Z3_mk_array_default(Z3_context a0, Z3_ast a1) {
2499  Z3_ast r = LIB.Z3_mk_array_default(a0, a1);
2500  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2501  if (err != Z3_error_code.Z3_OK)
2502  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2503  return r;
2504  }
2505 
2506  public static Z3_sort Z3_mk_set_sort(Z3_context a0, Z3_sort a1) {
2507  Z3_sort r = LIB.Z3_mk_set_sort(a0, a1);
2508  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2509  if (err != Z3_error_code.Z3_OK)
2510  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2511  return r;
2512  }
2513 
2514  public static Z3_ast Z3_mk_empty_set(Z3_context a0, Z3_sort a1) {
2515  Z3_ast r = LIB.Z3_mk_empty_set(a0, a1);
2516  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2517  if (err != Z3_error_code.Z3_OK)
2518  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2519  return r;
2520  }
2521 
2522  public static Z3_ast Z3_mk_full_set(Z3_context a0, Z3_sort a1) {
2523  Z3_ast r = LIB.Z3_mk_full_set(a0, a1);
2524  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2525  if (err != Z3_error_code.Z3_OK)
2526  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2527  return r;
2528  }
2529 
2530  public static Z3_ast Z3_mk_set_add(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2531  Z3_ast r = LIB.Z3_mk_set_add(a0, a1, a2);
2532  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2533  if (err != Z3_error_code.Z3_OK)
2534  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2535  return r;
2536  }
2537 
2538  public static Z3_ast Z3_mk_set_del(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2539  Z3_ast r = LIB.Z3_mk_set_del(a0, a1, a2);
2540  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2541  if (err != Z3_error_code.Z3_OK)
2542  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2543  return r;
2544  }
2545 
2546  public static Z3_ast Z3_mk_set_union(Z3_context a0, uint a1, [In] Z3_ast[] a2) {
2547  Z3_ast r = LIB.Z3_mk_set_union(a0, a1, a2);
2548  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2549  if (err != Z3_error_code.Z3_OK)
2550  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2551  return r;
2552  }
2553 
2554  public static Z3_ast Z3_mk_set_intersect(Z3_context a0, uint a1, [In] Z3_ast[] a2) {
2555  Z3_ast r = LIB.Z3_mk_set_intersect(a0, a1, a2);
2556  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2557  if (err != Z3_error_code.Z3_OK)
2558  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2559  return r;
2560  }
2561 
2562  public static Z3_ast Z3_mk_set_difference(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2563  Z3_ast r = LIB.Z3_mk_set_difference(a0, a1, a2);
2564  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2565  if (err != Z3_error_code.Z3_OK)
2566  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2567  return r;
2568  }
2569 
2570  public static Z3_ast Z3_mk_set_complement(Z3_context a0, Z3_ast a1) {
2571  Z3_ast r = LIB.Z3_mk_set_complement(a0, a1);
2572  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2573  if (err != Z3_error_code.Z3_OK)
2574  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2575  return r;
2576  }
2577 
2578  public static Z3_ast Z3_mk_set_member(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2579  Z3_ast r = LIB.Z3_mk_set_member(a0, a1, a2);
2580  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2581  if (err != Z3_error_code.Z3_OK)
2582  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2583  return r;
2584  }
2585 
2586  public static Z3_ast Z3_mk_set_subset(Z3_context a0, Z3_ast a1, Z3_ast a2) {
2587  Z3_ast r = LIB.Z3_mk_set_subset(a0, a1, a2);
2588  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2589  if (err != Z3_error_code.Z3_OK)
2590  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2591  return r;
2592  }
2593 
2594  public static Z3_ast Z3_mk_numeral(Z3_context a0, string a1, Z3_sort a2) {
2595  Z3_ast r = LIB.Z3_mk_numeral(a0, a1, a2);
2596  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2597  if (err != Z3_error_code.Z3_OK)
2598  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2599  return r;
2600  }
2601 
2602  public static Z3_ast Z3_mk_real(Z3_context a0, int a1, int a2) {
2603  Z3_ast r = LIB.Z3_mk_real(a0, a1, a2);
2604  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2605  if (err != Z3_error_code.Z3_OK)
2606  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2607  return r;
2608  }
2609 
2610  public static Z3_ast Z3_mk_int(Z3_context a0, int a1, Z3_sort a2) {
2611  Z3_ast r = LIB.Z3_mk_int(a0, a1, a2);
2612  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2613  if (err != Z3_error_code.Z3_OK)
2614  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2615  return r;
2616  }
2617 
2618  public static Z3_ast Z3_mk_unsigned_int(Z3_context a0, uint a1, Z3_sort a2) {
2619  Z3_ast r = LIB.Z3_mk_unsigned_int(a0, a1, a2);
2620  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2621  if (err != Z3_error_code.Z3_OK)
2622  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2623  return r;
2624  }
2625 
2626  public static Z3_ast Z3_mk_int64(Z3_context a0, Int64 a1, Z3_sort a2) {
2627  Z3_ast r = LIB.Z3_mk_int64(a0, a1, a2);
2628  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2629  if (err != Z3_error_code.Z3_OK)
2630  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2631  return r;
2632  }
2633 
2634  public static Z3_ast Z3_mk_unsigned_int64(Z3_context a0, UInt64 a1, Z3_sort a2) {
2635  Z3_ast r = LIB.Z3_mk_unsigned_int64(a0, a1, a2);
2636  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2637  if (err != Z3_error_code.Z3_OK)
2638  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2639  return r;
2640  }
2641 
2642  public static Z3_pattern Z3_mk_pattern(Z3_context a0, uint a1, [In] Z3_ast[] a2) {
2643  Z3_pattern r = LIB.Z3_mk_pattern(a0, a1, a2);
2644  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2645  if (err != Z3_error_code.Z3_OK)
2646  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2647  return r;
2648  }
2649 
2650  public static Z3_ast Z3_mk_bound(Z3_context a0, uint a1, Z3_sort a2) {
2651  Z3_ast r = LIB.Z3_mk_bound(a0, a1, a2);
2652  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2653  if (err != Z3_error_code.Z3_OK)
2654  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2655  return r;
2656  }
2657 
2658  public 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) {
2659  Z3_ast r = LIB.Z3_mk_forall(a0, a1, a2, a3, a4, a5, a6, a7);
2660  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2661  if (err != Z3_error_code.Z3_OK)
2662  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2663  return r;
2664  }
2665 
2666  public 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) {
2667  Z3_ast r = LIB.Z3_mk_exists(a0, a1, a2, a3, a4, a5, a6, a7);
2668  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2669  if (err != Z3_error_code.Z3_OK)
2670  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2671  return r;
2672  }
2673 
2674  public 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) {
2675  Z3_ast r = LIB.Z3_mk_quantifier(a0, a1, a2, a3, a4, a5, a6, a7, a8);
2676  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2677  if (err != Z3_error_code.Z3_OK)
2678  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2679  return r;
2680  }
2681 
2682  public 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) {
2683  Z3_ast r = LIB.Z3_mk_quantifier_ex(a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12);
2684  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2685  if (err != Z3_error_code.Z3_OK)
2686  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2687  return r;
2688  }
2689 
2690  public 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) {
2691  Z3_ast r = LIB.Z3_mk_forall_const(a0, a1, a2, a3, a4, a5, a6);
2692  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2693  if (err != Z3_error_code.Z3_OK)
2694  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2695  return r;
2696  }
2697 
2698  public 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) {
2699  Z3_ast r = LIB.Z3_mk_exists_const(a0, a1, a2, a3, a4, a5, a6);
2700  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2701  if (err != Z3_error_code.Z3_OK)
2702  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2703  return r;
2704  }
2705 
2706  public 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) {
2707  Z3_ast r = LIB.Z3_mk_quantifier_const(a0, a1, a2, a3, a4, a5, a6, a7);
2708  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2709  if (err != Z3_error_code.Z3_OK)
2710  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2711  return r;
2712  }
2713 
2714  public 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) {
2715  Z3_ast r = LIB.Z3_mk_quantifier_const_ex(a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11);
2716  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2717  if (err != Z3_error_code.Z3_OK)
2718  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2719  return r;
2720  }
2721 
2722  public static uint Z3_get_symbol_kind(Z3_context a0, IntPtr a1) {
2723  uint r = LIB.Z3_get_symbol_kind(a0, a1);
2724  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2725  if (err != Z3_error_code.Z3_OK)
2726  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2727  return r;
2728  }
2729 
2730  public static int Z3_get_symbol_int(Z3_context a0, IntPtr a1) {
2731  int r = LIB.Z3_get_symbol_int(a0, a1);
2732  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2733  if (err != Z3_error_code.Z3_OK)
2734  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2735  return r;
2736  }
2737 
2738  public static string Z3_get_symbol_string(Z3_context a0, IntPtr a1) {
2739  IntPtr r = LIB.Z3_get_symbol_string(a0, a1);
2740  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2741  if (err != Z3_error_code.Z3_OK)
2742  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
2743  return Marshal.PtrToStringAnsi(r);
2744  }
2745 
2746  public static IntPtr Z3_get_sort_name(Z3_context a0, Z3_sort a1) {
2747  IntPtr r = LIB.Z3_get_sort_name(a0, a1);
2748  Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
2749  if (err != Z3_error_code.Z3_OK)
2750  throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));