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