3 using System.Collections.Generic;
5 using System.Runtime.InteropServices;
7 #pragma warning disable 1591
42 [UnmanagedFunctionPointer(CallingConvention.Cdecl)]
45 public unsafe
class LIB
47 const string Z3_DLL_NAME =
"libz3.dll";
49 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
52 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
55 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
58 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
61 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
64 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
67 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
70 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
73 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
76 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
79 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
82 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
85 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
88 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
91 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
94 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
97 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
100 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
103 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
106 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
109 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
112 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
115 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
118 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
121 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
124 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
127 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
130 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
133 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
136 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
139 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
142 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
145 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
148 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
151 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
154 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
157 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
160 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
163 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
166 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
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);
172 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
175 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
178 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
181 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
184 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
187 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
190 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
193 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
196 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
199 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
202 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
205 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
208 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
211 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
214 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
217 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
220 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
223 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
226 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
229 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
232 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
235 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
238 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
241 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
244 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
247 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
250 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
253 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
256 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
259 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
262 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
265 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
268 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
271 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
274 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
277 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
280 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
283 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
286 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
289 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
292 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
295 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
298 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
301 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
304 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
307 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
310 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
313 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
316 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
319 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
322 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
325 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
328 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
331 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
334 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
337 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
340 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
343 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
346 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
349 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
352 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
355 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
358 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
361 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
364 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
367 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
370 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
373 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
376 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
379 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
382 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
385 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
388 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
391 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
394 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
397 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
400 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
403 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
406 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
409 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
412 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
415 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
418 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
421 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
424 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
427 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
430 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
433 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
436 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
439 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
442 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
445 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
448 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
451 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
454 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
457 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
460 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
463 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
466 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
469 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
472 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
475 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
478 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
481 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
484 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
487 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
490 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
493 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
496 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
499 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
502 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
505 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
508 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
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);
514 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
517 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
520 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
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);
526 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
529 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
532 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
535 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
538 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
541 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
544 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
547 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
550 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
553 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
556 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
559 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
562 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
565 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
568 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
571 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
574 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
577 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
580 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
583 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
586 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
589 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
592 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
595 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
598 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
601 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
604 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
607 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
610 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
613 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
616 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
619 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
622 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
625 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
628 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
631 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
634 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
637 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
640 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
643 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
646 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
649 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
652 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
655 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
658 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
661 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
664 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
667 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
670 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
673 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
676 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
679 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
682 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
685 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
688 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
691 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
694 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
697 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
700 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
703 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
706 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
709 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
712 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
715 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
718 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
721 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
724 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
727 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
730 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
733 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
736 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
739 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
742 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
745 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
748 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
751 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
754 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
757 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
760 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
763 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
766 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
769 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
772 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
775 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
778 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
781 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
784 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
787 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
790 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
793 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
796 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
799 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
802 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
805 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
808 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
811 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
814 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
817 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
820 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
823 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
826 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
829 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
832 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
835 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
838 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
841 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
844 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
847 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
850 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
853 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
856 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
859 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
862 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
865 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
868 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
871 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
874 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
877 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
880 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
883 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
886 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
889 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
892 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
895 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
898 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
901 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
904 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
907 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
910 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
913 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
916 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
919 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
922 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
925 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
928 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
931 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
934 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
937 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
940 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
943 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
946 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
949 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
952 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
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);
958 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
961 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
964 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
967 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
970 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
973 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
976 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
979 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
982 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
985 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
988 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
991 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
994 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
997 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1000 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1003 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1006 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1009 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1012 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1015 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1018 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1021 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1024 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1027 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1030 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1033 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1036 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1039 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1042 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1045 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1048 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1051 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1054 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1057 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1060 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1063 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1066 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1069 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1072 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1075 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1078 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1081 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1084 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1087 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1090 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1093 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1096 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1099 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1102 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1105 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1108 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1111 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1114 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1117 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1120 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1123 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1126 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1129 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1132 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1135 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1138 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1141 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1144 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1147 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1150 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1153 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1156 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1159 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1162 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1165 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1168 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1171 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1174 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1177 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1180 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1183 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1186 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1189 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1192 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1195 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1198 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1201 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1204 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1207 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1210 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1213 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1216 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1219 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1222 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1225 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1228 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1231 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1234 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1237 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1240 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1243 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1246 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1249 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1252 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1255 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1258 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1261 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1264 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1267 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1270 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1273 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1276 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1279 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1282 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1285 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1288 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1291 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1294 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1297 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1300 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1303 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1306 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1309 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1312 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1315 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1318 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1321 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1324 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1327 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1330 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1333 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1336 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1339 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1342 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1345 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1348 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1351 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1354 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1357 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1360 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1363 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1366 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1369 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1372 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1375 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1378 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1381 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1384 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1387 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1390 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1393 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1396 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1399 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1402 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1405 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1408 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1411 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1414 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1417 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1420 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1423 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1426 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1429 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1432 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1435 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1438 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1441 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1444 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1447 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1450 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1453 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1456 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1459 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1462 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1465 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1468 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1471 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1474 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1477 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1480 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1483 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1486 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1489 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1492 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1495 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1498 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1501 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1504 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1507 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1510 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1513 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1516 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1519 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1522 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1525 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1528 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1531 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1534 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1537 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1540 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1543 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1546 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1549 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1552 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1555 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1558 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1561 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1564 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1567 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1570 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1573 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1576 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1579 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1582 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1585 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1588 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1591 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1594 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1597 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1600 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1603 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1606 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1609 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1612 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1615 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1618 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1621 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1624 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1627 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1630 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1633 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1636 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1639 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1642 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1645 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1648 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1651 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1654 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1657 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1660 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1663 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
1703 if (r == IntPtr.Zero)
1704 throw new Z3Exception(
"Object allocation failed.");
1710 if (r == IntPtr.Zero)
1711 throw new Z3Exception(
"Object allocation failed.");
1802 return Marshal.PtrToStringAnsi(r);
1855 return Marshal.PtrToStringAnsi(r);
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) {
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);
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);
2915 return Marshal.PtrToStringAnsi(r);
3203 return Marshal.PtrToStringAnsi(r);
3339 return Marshal.PtrToStringAnsi(r);
3347 return Marshal.PtrToStringAnsi(r);
3563 return Marshal.PtrToStringAnsi(r);
3837 return Marshal.PtrToStringAnsi(r);
3845 return Marshal.PtrToStringAnsi(r);
3853 return Marshal.PtrToStringAnsi(r);
3861 return Marshal.PtrToStringAnsi(r);
3869 return Marshal.PtrToStringAnsi(r);
3877 return Marshal.PtrToStringAnsi(r);
3979 return Marshal.PtrToStringAnsi(r);
3996 return Marshal.PtrToStringAnsi(r);
4004 return Marshal.PtrToStringAnsi(r);
4007 public 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) {
4095 return Marshal.PtrToStringAnsi(r);
4178 return Marshal.PtrToStringAnsi(r);
4194 return Marshal.PtrToStringAnsi(r);
4299 return Marshal.PtrToStringAnsi(r);
4382 return Marshal.PtrToStringAnsi(r);
4498 return Marshal.PtrToStringAnsi(r);
4734 return Marshal.PtrToStringAnsi(r);
4750 return Marshal.PtrToStringAnsi(r);
4758 return Marshal.PtrToStringAnsi(r);
4774 return Marshal.PtrToStringAnsi(r);
4782 return Marshal.PtrToStringAnsi(r);
4828 return Marshal.PtrToStringAnsi(r);
4892 return Marshal.PtrToStringAnsi(r);
5020 return Marshal.PtrToStringAnsi(r);
5036 return Marshal.PtrToStringAnsi(r);
5044 return Marshal.PtrToStringAnsi(r);
5074 return Marshal.PtrToStringAnsi(r);
5407 return Marshal.PtrToStringAnsi(r);
5415 return Marshal.PtrToStringAnsi(r);
5750 return Marshal.PtrToStringAnsi(r);
5758 return Marshal.PtrToStringAnsi(r);
5802 return Marshal.PtrToStringAnsi(r);
static uint Z3_param_descrs_size(Z3_context a0, Z3_param_descrs a1)
static string Z3_rcf_num_to_decimal_string(Z3_context a0, Z3_rcf_num a1, uint a2)
Z3_bool Z3_API Z3_eval(__in Z3_context c, __in Z3_model m, __in Z3_ast t, __out Z3_ast *v)
Evaluate the AST node t in the given model. Return Z3_TRUE if succeeded, and store the result in v...
Z3_bool Z3_API Z3_algebraic_is_value(__in Z3_context c, __in Z3_ast a)
Return Z3_TRUE if can be used as value in the Z3 real algebraic number package.
static Z3_ast Z3_mk_bvmul(Z3_context a0, Z3_ast a1, Z3_ast a2)
static void Z3_params_set_uint(Z3_context a0, Z3_params a1, IntPtr a2, uint a3)
static void Z3_fixedpoint_dec_ref(Z3_context a0, Z3_fixedpoint a1)
static IntPtr Z3_get_decl_symbol_parameter(Z3_context a0, Z3_func_decl a1, uint a2)
static Z3_ast Z3_mk_select(Z3_context a0, Z3_ast a1, Z3_ast a2)
static int Z3_solver_check_assumptions(Z3_context a0, Z3_solver a1, uint a2, [In] Z3_ast[] a3)
Z3_ast Z3_API Z3_mk_bvadd_no_overflow(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2, Z3_bool is_signed)
Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.
static Z3_func_decl Z3_mk_fresh_func_decl(Z3_context a0, string a1, uint a2, [In] Z3_sort[] a3, Z3_sort a4)
static Z3_solver Z3_mk_solver_from_tactic(Z3_context a0, Z3_tactic a1)
static void Z3_goal_dec_ref(Z3_context a0, Z3_goal a1)
static int Z3_open_log(string a0)
static Z3_ast Z3_mk_bv2int(Z3_context a0, Z3_ast a1, int a2)
static void Z3_query_constructor(Z3_context a0, Z3_constructor a1, uint a2, [In, Out] ref Z3_func_decl a3, [In, Out] ref Z3_func_decl a4, [Out] Z3_func_decl[] a5)
static void Z3_reset_memory()
Z3_ast Z3_API Z3_mk_const(__in Z3_context c, __in Z3_symbol s, __in Z3_sort ty)
Declare and create a constant.
static Z3_param_descrs Z3_fixedpoint_get_param_descrs(Z3_context a0, Z3_fixedpoint a1)
Z3_lbool Z3_API Z3_check_and_get_model(__in Z3_context c, __out Z3_model *m)
Check whether the given logical context is consistent or not.
Z3_bool Z3_API Z3_algebraic_eq(__in Z3_context c, __in Z3_ast a, __in Z3_ast b)
Return Z3_TRUE if a == b, and Z3_FALSE otherwise.
Z3_string Z3_API Z3_ast_map_to_string(__in Z3_context c, __in Z3_ast_map m)
Convert the given map into a string.
static uint Z3_goal_precision(Z3_context a0, Z3_goal a1)
static Z3_sort Z3_mk_tuple_sort(Z3_context a0, IntPtr a1, uint a2, [In] IntPtr[] a3, [In] Z3_sort[] a4, [In, Out] ref Z3_func_decl a5, [Out] Z3_func_decl[] a6)
static Z3_ast Z3_mk_bvadd_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2, int a3)
Z3_ast Z3_API Z3_mk_power(__in Z3_context c, __in Z3_ast arg1, __in Z3_ast arg2)
Create an AST node representing arg1^arg2.
static Z3_sort Z3_mk_uninterpreted_sort(Z3_context a0, IntPtr a1)
static string Z3_get_tactic_name(Z3_context a0, uint a1)
static void Z3_solver_pop(Z3_context a0, Z3_solver a1, uint a2)
static void Z3_tactic_inc_ref(Z3_context a0, Z3_tactic a1)
static void Z3_fixedpoint_push(Z3_context a0, Z3_fixedpoint a1)
static Z3_ast Z3_mk_bvuge(Z3_context a0, Z3_ast a1, Z3_ast a2)
static uint Z3_goal_num_exprs(Z3_context a0, Z3_goal a1)
static void Z3_model_inc_ref(Z3_context a0, Z3_model a1)
Z3_tactic Z3_API Z3_tactic_par_and_then(__in Z3_context c, __in Z3_tactic t1, __in Z3_tactic t2)
Return a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1...
static Z3_tactic Z3_tactic_or_else(Z3_context a0, Z3_tactic a1, Z3_tactic a2)
static void Z3_solver_assert_and_track(Z3_context a0, Z3_solver a1, Z3_ast a2, Z3_ast a3)
static IntPtr Z3_get_sort_name(Z3_context a0, Z3_sort a1)
Z3_ast Z3_API Z3_mk_iff(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Create an AST node representing t1 iff t2.
Z3_ast Z3_API Z3_mk_ext_rotate_right(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Rotate bits of t1 to the right t2 times.
static Z3_ast Z3_ast_vector_get(Z3_context a0, Z3_ast_vector a1, uint a2)
Z3_ast Z3_API Z3_mk_forall_const(__in Z3_context c, unsigned weight, unsigned num_bound, __in_ecount(num_bound) Z3_app const bound[], unsigned num_patterns, __in_ecount(num_patterns) Z3_pattern const patterns[], __in Z3_ast body)
Create a universal quantifier using a list of constants that will form the set of bound variables...
static Z3_sort Z3_mk_list_sort(Z3_context a0, IntPtr a1, Z3_sort a2, [In, Out] ref Z3_func_decl a3, [In, Out] ref Z3_func_decl a4, [In, Out] ref Z3_func_decl a5, [In, Out] ref Z3_func_decl a6, [In, Out] ref Z3_func_decl a7, [In, Out] ref Z3_func_decl a8)
static double Z3_get_decl_double_parameter(Z3_context a0, Z3_func_decl a1, uint a2)
static string Z3_stats_to_string(Z3_context a0, Z3_stats a1)
Z3_bool Z3_API Z3_is_well_sorted(__in Z3_context c, __in Z3_ast t)
Return true if the given expression t is well sorted.
static Z3_func_decl Z3_mk_injective_function(Z3_context a0, IntPtr a1, uint a2, [In] Z3_sort[] a3, Z3_sort a4)
static double Z3_stats_get_double_value(Z3_context a0, Z3_stats a1, uint a2)
static Z3_func_decl Z3_get_model_constant(Z3_context a0, Z3_model a1, uint a2)
static Z3_ast Z3_get_smtlib_formula(Z3_context a0, uint a1)
static Z3_ast Z3_mk_bvneg_no_overflow(Z3_context a0, Z3_ast a1)
void Z3_API Z3_fixedpoint_assert(__in Z3_context c, __in Z3_fixedpoint d, __in Z3_ast axiom)
Assert a constraint to the fixedpoint context.
static Z3_sort Z3_get_array_sort_range(Z3_context a0, Z3_sort a1)
static Z3_ast Z3_translate(Z3_context a0, Z3_ast a1, Z3_context a2)
void Z3_API Z3_solver_assert_and_track(__in Z3_context c, __in Z3_solver s, __in Z3_ast a, __in Z3_ast p)
Assert a constraint a into the solver, and track it (in the unsat) core using the Boolean constant p...
static Z3_sort Z3_get_quantifier_bound_sort(Z3_context a0, Z3_ast a1, uint a2)
Z3_ast Z3_API Z3_mk_bvule(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Unsigned less than or equal to.
Z3_context Z3_API Z3_mk_context_rc(__in Z3_config c)
Create a context using the given configuration. This function is similar to Z3_mk_context. However, in the context returned by this function, the user is responsible for managing Z3_ast reference counters. Managing reference counters is a burden and error-prone, but allows the user to use the memory more efficiently. The user must invoke Z3_inc_ref for any Z3_ast returned by Z3, and Z3_dec_ref whenever the Z3_ast is not needed anymore. This idiom is similar to the one used in BDD (binary decision diagrams) packages such as CUDD.
static Z3_tactic Z3_tactic_par_and_then(Z3_context a0, Z3_tactic a1, Z3_tactic a2)
static void Z3_push(Z3_context a0)
Z3_ast Z3_API Z3_translate(__in Z3_context source, __in Z3_ast a, __in Z3_context target)
Translate/Copy the AST a from context source to context target. AST a must have been created using co...
Z3_ast Z3_API Z3_mk_mul(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create an AST node representing args[0] * ... * args[num_args-1].The array args must have num_args el...
Z3_bool Z3_API Z3_algebraic_neq(__in Z3_context c, __in Z3_ast a, __in Z3_ast b)
Return Z3_TRUE if a != b, and Z3_FALSE otherwise.
Z3_sort Z3_API Z3_mk_bool_sort(__in Z3_context c)
Create the Boolean type.
static Z3_rcf_num Z3_rcf_div(Z3_context a0, Z3_rcf_num a1, Z3_rcf_num a2)
static int Z3_algebraic_is_zero(Z3_context a0, Z3_ast a1)
Z3_string Z3_API Z3_solver_to_string(__in Z3_context c, __in Z3_solver s)
Convert a solver into a string.
static void Z3_block_literals(Z3_context a0, Z3_literals a1)
Z3_string Z3_API Z3_fixedpoint_get_help(__in Z3_context c, __in Z3_fixedpoint f)
Return a string describing all fixedpoint available parameters.
static void Z3_inc_ref(Z3_context a0, Z3_ast a1)
static uint Z3_get_model_num_funcs(Z3_context a0, Z3_model a1)
Z3_ast_vector Z3_API Z3_model_get_sort_universe(__in Z3_context c, __in Z3_model m, __in Z3_sort s)
Return the finite set of distinct values that represent the interpretation for sort s...
static Z3_ast Z3_update_term(Z3_context a0, Z3_ast a1, uint a2, [In] Z3_ast[] a3)
Z3_string Z3_API Z3_func_decl_to_string(__in Z3_context c, __in Z3_func_decl d)
Z3_lbool Z3_API Z3_solver_check(__in Z3_context c, __in Z3_solver s)
Check whether the assertions in a given solver are consistent or not.
Z3_ast Z3_API Z3_algebraic_power(__in Z3_context c, __in Z3_ast a, __in unsigned k)
Return the a^k.
static Z3_ast Z3_mk_zero_ext(Z3_context a0, uint a1, Z3_ast a2)
static Z3_rcf_num Z3_rcf_add(Z3_context a0, Z3_rcf_num a1, Z3_rcf_num a2)
void Z3_API Z3_inc_ref(__in Z3_context c, __in Z3_ast a)
Increment the reference counter of the given AST. The context c should have been created using Z3_mk_...
Z3_ast Z3_API Z3_mk_bvsmod(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed remainder (sign follows divisor).
Z3_bool Z3_API Z3_get_numeral_int(__in Z3_context c, __in Z3_ast v, __out int *i)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine int...
static IntPtr Z3_fixedpoint_to_string(Z3_context a0, Z3_fixedpoint a1, uint a2, [In] Z3_ast[] a3)
static Z3_ast Z3_mk_real2int(Z3_context a0, Z3_ast a1)
static Z3_ast_vector Z3_model_get_sort_universe(Z3_context a0, Z3_model a1, Z3_sort a2)
static Z3_ast Z3_get_literal(Z3_context a0, Z3_literals a1, uint a2)
static Z3_sort Z3_mk_datatype(Z3_context a0, IntPtr a1, uint a2, [In, Out] Z3_constructor[] a3)
static Z3_ast_vector Z3_polynomial_subresultants(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3)
static Z3_sort Z3_mk_array_sort(Z3_context a0, Z3_sort a1, Z3_sort a2)
static Z3_ast Z3_mk_true(Z3_context a0)
static int Z3_is_eq_sort(Z3_context a0, Z3_sort a1, Z3_sort a2)
static uint Z3_get_implied_equalities(Z3_context a0, Z3_solver a1, uint a2, [In] Z3_ast[] a3, [Out] uint[] a4)
static Z3_ast Z3_mk_set_intersect(Z3_context a0, uint a1, [In] Z3_ast[] a2)
static int Z3_get_numeral_int(Z3_context a0, Z3_ast a1, [In, Out] ref int a2)
static Z3_ast Z3_mk_bvuge(Z3_context a0, Z3_ast a1, Z3_ast a2)
Z3_ast Z3_API Z3_mk_bvadd(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Standard two's complement addition.
static uint Z3_get_relation_arity(Z3_context a0, Z3_sort a1)
static IntPtr Z3_get_decl_name(Z3_context a0, Z3_func_decl a1)
static void Z3_rcf_del(Z3_context a0, Z3_rcf_num a1)
static int Z3_algebraic_eq(Z3_context a0, Z3_ast a1, Z3_ast a2)
void Z3_API Z3_params_dec_ref(__in Z3_context c, __in Z3_params p)
Decrement the reference counter of the given parameter set.
void Z3_API Z3_apply_result_inc_ref(__in Z3_context c, __in Z3_apply_result r)
Increment the reference counter of the given Z3_apply_result object.
static Z3_ast Z3_fixedpoint_get_answer(Z3_context a0, Z3_fixedpoint a1)
static Z3_ast Z3_mk_mul(Z3_context a0, uint a1, [In] Z3_ast[] a2)
static void Z3_ast_map_reset(Z3_context a0, Z3_ast_map a1)
static Z3_ast Z3_mk_mod(Z3_context a0, Z3_ast a1, Z3_ast a2)
static void Z3_update_param_value(Z3_context a0, string a1, string a2)
static Z3_tactic Z3_tactic_or_else(Z3_context a0, Z3_tactic a1, Z3_tactic a2)
static Z3_ast Z3_mk_implies(Z3_context a0, Z3_ast a1, Z3_ast a2)
static uint Z3_goal_depth(Z3_context a0, Z3_goal a1)
static Z3_func_decl Z3_get_model_constant(Z3_context a0, Z3_model a1, uint a2)
Z3_ast Z3_API Z3_mk_zero_ext(__in Z3_context c, __in unsigned i, __in Z3_ast t1)
Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i...
static void Z3_interrupt(Z3_context a0)
Z3_ast Z3_API Z3_mk_bvsub_no_underflow(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2, Z3_bool is_signed)
Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow...
Z3_ast_vector Z3_API Z3_algebraic_roots(__in Z3_context c, __in Z3_ast p, __in unsigned n, __in Z3_ast a[])
Given a multivariate polynomial p(x_0, ..., x_{n-1}, x_n), returns the roots of the univariate polyno...
static IntPtr Z3_rcf_num_to_decimal_string(Z3_context a0, Z3_rcf_num a1, uint a2)
static Z3_ast Z3_mk_mod(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_func_interp Z3_model_get_func_interp(Z3_context a0, Z3_model a1, Z3_func_decl a2)
Z3_bool Z3_API Z3_algebraic_le(__in Z3_context c, __in Z3_ast a, __in Z3_ast b)
Return Z3_TRUE if a <= b, and Z3_FALSE otherwise.
static Z3_apply_result Z3_tactic_apply_ex(Z3_context a0, Z3_tactic a1, Z3_goal a2, Z3_params a3)
static void Z3_goal_reset(Z3_context a0, Z3_goal a1)
Z3_func_decl Z3_API Z3_mk_injective_function(__in Z3_context c, __in Z3_symbol s, unsigned domain_size, __in_ecount(domain_size) Z3_sort const domain[], __in Z3_sort range)
Create injective function declaration.
void Z3_API Z3_param_descrs_inc_ref(__in Z3_context c, __in Z3_param_descrs p)
Increment the reference counter of the given parameter description set.
static Z3_sort Z3_mk_bv_sort(Z3_context a0, uint a1)
Z3_tactic Z3_API Z3_mk_tactic(__in Z3_context c, __in Z3_string name)
Return a tactic associated with the given name. The complete list of tactics may be obtained using th...
static int Z3_goal_inconsistent(Z3_context a0, Z3_goal a1)
static Z3_ast Z3_mk_bvneg_no_overflow(Z3_context a0, Z3_ast a1)
Z3_string Z3_API Z3_tactic_get_help(__in Z3_context c, __in Z3_tactic t)
Return a string containing a description of parameters accepted by the given tactic.
static Z3_ast Z3_mk_bvsmod(Z3_context a0, Z3_ast a1, Z3_ast a2)
void Z3_API Z3_del_constructor(__in Z3_context c, __in Z3_constructor constr)
Reclaim memory allocated to constructor.
static uint Z3_get_model_num_constants(Z3_context a0, Z3_model a1)
static Z3_ast Z3_mk_empty_set(Z3_context a0, Z3_sort a1)
static uint Z3_model_get_num_sorts(Z3_context a0, Z3_model a1)
Z3_sort Z3_API Z3_get_array_sort_range(__in Z3_context c, __in Z3_sort t)
Return the range of the given array sort.
static IntPtr Z3_mk_int_symbol(Z3_context a0, int a1)
static void Z3_model_dec_ref(Z3_context a0, Z3_model a1)
static int Z3_stats_is_double(Z3_context a0, Z3_stats a1, uint a2)
unsigned Z3_API Z3_get_num_literals(__in Z3_context c, __in Z3_literals lbls)
Retrieve the number of label symbols that were returned.
static uint Z3_get_num_probes(Z3_context a0)
static void Z3_disable_literal(Z3_context a0, Z3_literals a1, uint a2)
static Z3_ast Z3_mk_bvashr(Z3_context a0, Z3_ast a1, Z3_ast a2)
Z3_search_failure Z3_API Z3_get_search_failure(__in Z3_context c)
Retrieve reason for search failure.
Z3_string Z3_API Z3_get_tactic_name(__in Z3_context c, unsigned i)
Return the name of the idx tactic.
static Z3_sort Z3_get_sort(Z3_context a0, Z3_ast a1)
Z3_bool Z3_API Z3_algebraic_gt(__in Z3_context c, __in Z3_ast a, __in Z3_ast b)
Return Z3_TRUE if a > b, and Z3_FALSE otherwise.
Z3_string Z3_API Z3_param_descrs_to_string(__in Z3_context c, __in Z3_param_descrs p)
Convert a parameter description set into a string. This function is mainly used for printing the cont...
static Z3_apply_result Z3_tactic_apply(Z3_context a0, Z3_tactic a1, Z3_goal a2)
static Z3_ast Z3_get_decl_ast_parameter(Z3_context a0, Z3_func_decl a1, uint a2)
static Z3_ast Z3_mk_quantifier_const(Z3_context a0, int a1, uint a2, uint a3, [In] Z3_app[] a4, uint a5, [In] Z3_pattern[] a6, Z3_ast a7)
static Z3_model Z3_apply_result_convert_model(Z3_context a0, Z3_apply_result a1, uint a2, Z3_model a3)
static Z3_sort Z3_mk_real_sort(Z3_context a0)
static Z3_literals Z3_get_relevant_labels(Z3_context a0)
Z3_sort Z3_API Z3_mk_bv_sort(__in Z3_context c, __in unsigned sz)
Create a bit-vector type of the given size.
Z3_ast Z3_API Z3_mk_bound(__in Z3_context c, __in unsigned index, __in Z3_sort ty)
Create a bound variable.
static void Z3_rcf_get_numerator_denominator(Z3_context a0, Z3_rcf_num a1, [In, Out] ref Z3_rcf_num a2, [In, Out] ref Z3_rcf_num a3)
static uint Z3_ast_map_size(Z3_context a0, Z3_ast_map a1)
static void Z3_ast_vector_resize(Z3_context a0, Z3_ast_vector a1, uint a2)
Z3_symbol Z3_API Z3_get_decl_name(__in Z3_context c, __in Z3_func_decl d)
Return the constant declaration name as a symbol.
static int Z3_check_assumptions(Z3_context a0, uint a1, [In] Z3_ast[] a2, [In, Out] ref Z3_model a3, [In, Out] ref Z3_ast a4, [In, Out] ref uint a5, [Out] Z3_ast[] a6)
static string Z3_stats_get_key(Z3_context a0, Z3_stats a1, uint a2)
static Z3_sort Z3_get_array_sort_range(Z3_context a0, Z3_sort a1)
static void Z3_global_param_reset_all()
static uint Z3_rcf_mk_roots(Z3_context a0, uint a1, [In] Z3_rcf_num[] a2, [Out] Z3_rcf_num[] a3)
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)
Z3_param_kind Z3_API Z3_param_descrs_get_kind(__in Z3_context c, __in Z3_param_descrs p, __in Z3_symbol n)
Return the kind associated with the given parameter name n.
static Z3_ast Z3_mk_bvsgt(Z3_context a0, Z3_ast a1, Z3_ast a2)
Z3_probe Z3_API Z3_probe_eq(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is equal to the value returned ...
void Z3_API Z3_model_inc_ref(__in Z3_context c, __in Z3_model m)
Increment the reference counter of the given model.
static Z3_ast Z3_get_model_func_else(Z3_context a0, Z3_model a1, uint a2)
static Z3_ast_vector Z3_ast_map_keys(Z3_context a0, Z3_ast_map a1)
static Z3_ast Z3_mk_unsigned_int(Z3_context a0, uint a1, Z3_sort a2)
static Z3_tactic Z3_tactic_par_or(Z3_context a0, uint a1, [In] Z3_tactic[] a2)
static uint Z3_get_app_num_args(Z3_context a0, Z3_app a1)
static Z3_ast Z3_mk_app(Z3_context a0, Z3_func_decl a1, uint a2, [In] Z3_ast[] a3)
static Z3_ast Z3_mk_bvashr(Z3_context a0, Z3_ast a1, Z3_ast a2)
void Z3_API Z3_fixedpoint_update_rule(__in Z3_context c, __in Z3_fixedpoint d, __in Z3_ast a, __in Z3_symbol name)
Update a named rule. A rule with the same name must have been previously created. ...
Z3_ast Z3_API Z3_mk_numeral(__in Z3_context c, __in Z3_string numeral, __in Z3_sort ty)
Create a numeral of a given sort.
static int Z3_get_numeral_int64(Z3_context a0, Z3_ast a1, [In, Out] ref Int64 a2)
Z3_func_decl Z3_API Z3_get_datatype_sort_recognizer(__in Z3_context c, __in Z3_sort t, unsigned idx)
Return idx'th recognizer.
Z3_ast Z3_API Z3_substitute_vars(__in Z3_context c, __in Z3_ast a, __in unsigned num_exprs, __in_ecount(num_exprs) Z3_ast const to[])
Substitute the free variables in a with the expressions in to. For every i smaller than num_exprs...
static Z3_rcf_num Z3_rcf_neg(Z3_context a0, Z3_rcf_num a1)
Z3_tactic Z3_API Z3_tactic_fail_if(__in Z3_context c, __in Z3_probe p)
Return a tactic that fails if the probe p evaluates to false.
static Z3_func_decl Z3_get_model_func_decl(Z3_context a0, Z3_model a1, uint a2)
unsigned Z3_API Z3_get_app_num_args(__in Z3_context c, __in Z3_app a)
Return the number of argument of an application. If t is an constant, then the number of arguments is...
static void Z3_apply_result_dec_ref(Z3_context a0, Z3_apply_result a1)
static Z3_ast Z3_mk_bvsge(Z3_context a0, Z3_ast a1, Z3_ast a2)
Z3_ast Z3_API Z3_mk_int2bv(__in Z3_context c, __in unsigned n, __in Z3_ast t1)
Create an n bit bit-vector from the integer argument t1.
Z3_ast Z3_API Z3_mk_bvurem(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Unsigned remainder.
Z3_func_decl Z3_API Z3_get_model_func_decl(__in Z3_context c, __in Z3_model m, __in unsigned i)
Return the declaration of the i-th function in the given model.
void Z3_API Z3_func_entry_dec_ref(__in Z3_context c, __in Z3_func_entry e)
Decrement the reference counter of the given Z3_func_entry object.
static IntPtr Z3_ast_to_string(Z3_context a0, Z3_ast a1)
static void Z3_parse_smtlib_string(Z3_context a0, string a1, uint a2, [In] IntPtr[] a3, [In] Z3_sort[] a4, uint a5, [In] IntPtr[] a6, [In] Z3_func_decl[] a7)
static uint Z3_get_num_scopes(Z3_context a0)
static int Z3_get_numeral_small(Z3_context a0, Z3_ast a1, [In, Out] ref Int64 a2, [In, Out] ref Int64 a3)
Z3_ast Z3_API Z3_mk_bvor(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Bitwise or.
static uint Z3_get_bv_sort_size(Z3_context a0, Z3_sort a1)
static Z3_ast Z3_mk_bv2int(Z3_context a0, Z3_ast a1, int a2)
static int Z3_algebraic_is_neg(Z3_context a0, Z3_ast a1)
Z3_ast Z3_API Z3_get_model_func_else(__in Z3_context c, __in Z3_model m, __in unsigned i)
Return the 'else' value of the i-th function interpretation in the given model.
unsigned Z3_API Z3_get_model_num_constants(__in Z3_context c, __in Z3_model m)
Return the number of constants assigned by the given model.
Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions(__in Z3_context c, __in Z3_fixedpoint f)
Retrieve set of background assertions from fixedpoint context.
int Z3_API Z3_check_interpolant(__in Z3_context ctx, __in unsigned num, __in_ecount(num) Z3_ast cnsts[], __in_ecount(num) unsigned parents[], __in_ecount(num-1) Z3_ast *interps, __out Z3_string_ptr error, __in unsigned num_theory, __in_ecount(num_theory) Z3_ast theory[])
static string Z3_tactic_get_descr(Z3_context a0, string a1)
static Z3_ast Z3_get_smtlib_formula(Z3_context a0, uint a1)
static Z3_sort Z3_mk_enumeration_sort(Z3_context a0, IntPtr a1, uint a2, [In] IntPtr[] a3, [Out] Z3_func_decl[] a4, [Out] Z3_func_decl[] a5)
static Z3_probe Z3_probe_and(Z3_context a0, Z3_probe a1, Z3_probe a2)
Z3_sort Z3_API Z3_mk_enumeration_sort(__in Z3_context c, __in Z3_symbol name, __in unsigned n, __in_ecount(n) Z3_symbol const enum_names[], __out_ecount(n) Z3_func_decl enum_consts[], __out_ecount(n) Z3_func_decl enum_testers[])
Create a enumeration sort.
Z3_ast Z3_API Z3_model_get_const_interp(__in Z3_context c, __in Z3_model m, __in Z3_func_decl a)
Return the interpretation (i.e., assignment) of constant a in the model m. Return NULL...
static int Z3_algebraic_is_value(Z3_context a0, Z3_ast a1)
Z3_func_decl Z3_API Z3_get_tuple_sort_field_decl(__in Z3_context c, __in Z3_sort t, __in unsigned i)
Return the i-th field declaration (i.e., projection function declaration) of the given tuple sort...
static void Z3_ast_vector_inc_ref(Z3_context a0, Z3_ast_vector a1)
static void Z3_ast_map_dec_ref(Z3_context a0, Z3_ast_map a1)
static IntPtr Z3_ast_map_to_string(Z3_context a0, Z3_ast_map a1)
static IntPtr Z3_get_smtlib_error(Z3_context a0)
Z3_bool Z3_API Z3_global_param_get(__in Z3_string param_id, __out Z3_string_ptr param_value)
Get a global (or module) parameter.
Z3_func_decl Z3_API Z3_model_get_func_decl(__in Z3_context c, __in Z3_model m, __in unsigned i)
Return the declaration of the i-th function in the given model.
Z3_bool Z3_API Z3_is_algebraic_number(__in Z3_context c, __in Z3_ast a)
Return true if the give AST is a real algebraic number.
Z3_func_decl Z3_API Z3_get_as_array_func_decl(__in Z3_context c, __in Z3_ast a)
Return the function declaration f associated with a (_ as_array f) node.
static Z3_ast Z3_get_numerator(Z3_context a0, Z3_ast a1)
void Z3_API Z3_solver_dec_ref(__in Z3_context c, __in Z3_solver s)
Decrement the reference counter of the given solver.
void Z3_API Z3_goal_inc_ref(__in Z3_context c, __in Z3_goal g)
Increment the reference counter of the given goal.
Z3_ast Z3_API Z3_mk_bvsub_no_overflow(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow...
Z3_ast Z3_API Z3_mk_set_complement(__in Z3_context c, __in Z3_ast arg)
Take the complement of a set.
unsigned Z3_API Z3_ast_map_size(__in Z3_context c, __in Z3_ast_map m)
Return the size of the given map.
static Z3_func_decl Z3_get_tuple_sort_mk_decl(Z3_context a0, Z3_sort a1)
Z3_ast_map Z3_API Z3_mk_ast_map(__in Z3_context c)
Return an empty mapping from AST to AST.
static void Z3_model_dec_ref(Z3_context a0, Z3_model a1)
void Z3_API Z3_enable_trace(__in Z3_string tag)
Enable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise...
static void Z3_ast_map_insert(Z3_context a0, Z3_ast_map a1, Z3_ast a2, Z3_ast a3)
int Z3_API Z3_get_decl_int_parameter(__in Z3_context c, __in Z3_func_decl d, unsigned idx)
Return the integer value associated with an integer parameter.
static int Z3_ast_map_contains(Z3_context a0, Z3_ast_map a1, Z3_ast a2)
static Z3_ast Z3_ast_map_find(Z3_context a0, Z3_ast_map a1, Z3_ast a2)
unsigned Z3_API Z3_get_model_func_entry_num_args(__in Z3_context c, __in Z3_model m, __in unsigned i, __in unsigned j)
Return the number of arguments of the j-th entry of the i-th function interpretation in the given mod...
Z3_apply_result Z3_API Z3_tactic_apply(__in Z3_context c, __in Z3_tactic t, __in Z3_goal g)
Apply tactic t to the goal g.
static Z3_config Z3_mk_config()
static string Z3_tactic_get_help(Z3_context a0, Z3_tactic a1)
Z3_ast Z3_API Z3_func_entry_get_value(__in Z3_context c, __in Z3_func_entry e)
Return the value of this point.
Z3_func_decl Z3_API Z3_get_datatype_sort_constructor_accessor(__in Z3_context c, __in Z3_sort t, unsigned idx_c, unsigned idx_a)
Return idx_a'th accessor for the idx_c'th constructor.
Z3_error_code
Z3_error_code
static Z3_sort Z3_get_decl_sort_parameter(Z3_context a0, Z3_func_decl a1, uint a2)
static uint Z3_get_sort_kind(Z3_context a0, Z3_sort a1)
static uint Z3_model_get_num_consts(Z3_context a0, Z3_model a1)
unsigned Z3_API Z3_rcf_mk_roots(__in Z3_context c, __in unsigned n, __in_ecount(n) Z3_rcf_num const a[], __out_ecount(n) Z3_rcf_num roots[])
Store in roots the roots of the polynomial a[n-1]*x^{n-1} + ... + a[0]. The output vector roots must ...
static uint Z3_get_bool_value(Z3_context a0, Z3_ast a1)
Z3_goal_prec Z3_API Z3_goal_precision(__in Z3_context c, __in Z3_goal g)
Return the "precision" of the given goal. Goals can be transformed using over and under approximation...
static Z3_probe Z3_probe_or(Z3_context a0, Z3_probe a1, Z3_probe a2)
static Z3_ast Z3_mk_bvand(Z3_context a0, Z3_ast a1, Z3_ast a2)
Z3_model Z3_API Z3_apply_result_convert_model(__in Z3_context c, __in Z3_apply_result r, __in unsigned i, __in Z3_model m)
Convert a model for the subgoal Z3_apply_result_get_subgoal(c, r, i) into a model for the original go...
static uint Z3_get_sort_id(Z3_context a0, Z3_sort a1)
static Z3_ast Z3_mk_exists_const(Z3_context a0, uint a1, uint a2, [In] Z3_app[] a3, uint a4, [In] Z3_pattern[] a5, Z3_ast a6)
static Z3_ast Z3_mk_fresh_const(Z3_context a0, string a1, Z3_sort a2)
Z3_bool Z3_API Z3_rcf_le(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b)
Return Z3_TRUE if a <= b.
Z3_ast Z3_API Z3_parse_smtlib2_file(__in Z3_context c, __in Z3_string file_name, __in unsigned num_sorts, __in_ecount(num_sorts) Z3_symbol const sort_names[], __in_ecount(num_sorts) Z3_sort const sorts[], __in unsigned num_decls, __in_ecount(num_decls) Z3_symbol const decl_names[], __in_ecount(num_decls) Z3_func_decl const decls[])
Similar to Z3_parse_smtlib2_string, but reads the benchmark from a file.
static uint Z3_get_model_num_funcs(Z3_context a0, Z3_model a1)
static Z3_ast Z3_mk_empty_set(Z3_context a0, Z3_sort a1)
static void Z3_del_constructor_list(Z3_context a0, Z3_constructor_list a1)
Z3_bool Z3_API Z3_open_log(__in Z3_string filename)
Log interaction to a file.
static Z3_ast Z3_get_context_assignment(Z3_context a0)
static int Z3_goal_is_decided_sat(Z3_context a0, Z3_goal a1)
static string Z3_get_numeral_string(Z3_context a0, Z3_ast a1)
static Z3_ast Z3_mk_ext_rotate_left(Z3_context a0, Z3_ast a1, Z3_ast a2)
static uint Z3_get_num_probes(Z3_context a0)
static void Z3_dec_ref(Z3_context a0, Z3_ast a1)
static void Z3_fixedpoint_register_relation(Z3_context a0, Z3_fixedpoint a1, Z3_func_decl a2)
static Z3_ast Z3_mk_bvmul_no_underflow(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_mk_bvshl(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_mk_sign_ext(Z3_context a0, uint a1, Z3_ast a2)
static Z3_ast Z3_mk_exists(Z3_context a0, uint a1, uint a2, [In] Z3_pattern[] a3, uint a4, [In] Z3_sort[] a5, [In] IntPtr[] a6, Z3_ast a7)
static int Z3_get_numeral_rational_int64(Z3_context a0, Z3_ast a1, [In, Out] ref Int64 a2, [In, Out] ref Int64 a3)
void Z3_API Z3_toggle_warning_messages(__in Z3_bool enabled)
Enable/disable printing warning messages to the console.
static void Z3_ast_vector_dec_ref(Z3_context a0, Z3_ast_vector a1)
static uint Z3_get_smtlib_num_assumptions(Z3_context a0)
unsigned Z3_API Z3_solver_get_num_scopes(__in Z3_context c, __in Z3_solver s)
Return the number of backtracking points.
void Z3_API Z3_params_inc_ref(__in Z3_context c, __in Z3_params p)
Increment the reference counter of the given parameter set.
Z3_ast Z3_API Z3_mk_fresh_const(__in Z3_context c, __in Z3_string prefix, __in Z3_sort ty)
Declare and create a fresh constant.
void Z3_API Z3_parse_smtlib_file(__in Z3_context c, __in Z3_string file_name, __in unsigned num_sorts, __in_ecount(num_sorts) Z3_symbol const sort_names[], __in_ecount(num_sorts) Z3_sort const sorts[], __in unsigned num_decls, __in_ecount(num_decls) Z3_symbol const decl_names[], __in_ecount(num_decls) Z3_func_decl const decls[])
Similar to Z3_parse_smtlib_string, but reads the benchmark from a file.
static uint Z3_rcf_mk_roots(Z3_context a0, uint a1, [In] Z3_rcf_num[] a2, [Out] Z3_rcf_num[] a3)
static void Z3_func_entry_dec_ref(Z3_context a0, Z3_func_entry a1)
static Z3_ast Z3_mk_bvneg(Z3_context a0, Z3_ast a1)
static uint Z3_get_model_func_entry_num_args(Z3_context a0, Z3_model a1, uint a2, uint a3)
static Z3_probe Z3_probe_le(Z3_context a0, Z3_probe a1, Z3_probe a2)
static Z3_ast Z3_get_algebraic_number_upper(Z3_context a0, Z3_ast a1, uint a2)
Z3_symbol Z3_API Z3_mk_string_symbol(__in Z3_context c, __in Z3_string s)
Create a Z3 symbol using a C string.
static Z3_ast Z3_mk_exists_const(Z3_context a0, uint a1, uint a2, [In] Z3_app[] a3, uint a4, [In] Z3_pattern[] a5, Z3_ast a6)
static Z3_ast Z3_mk_bvsub_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2)
unsigned Z3_API Z3_get_num_tactics(__in Z3_context c)
Return the number of builtin tactics available in Z3.
Z3_error_code
Z3 error codes (See Z3_get_error_code).
static Z3_ast_vector Z3_solver_get_assertions(Z3_context a0, Z3_solver a1)
Z3_sort Z3_API Z3_mk_real_sort(__in Z3_context c)
Create the real type.
static int Z3_algebraic_is_pos(Z3_context a0, Z3_ast a1)
static int Z3_is_eq_func_decl(Z3_context a0, Z3_func_decl a1, Z3_func_decl a2)
static Z3_ast Z3_mk_real(Z3_context a0, int a1, int a2)
static uint Z3_stats_size(Z3_context a0, Z3_stats a1)
static uint Z3_get_func_decl_id(Z3_context a0, Z3_func_decl a1)
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)
unsigned Z3_API Z3_get_quantifier_num_patterns(__in Z3_context c, __in Z3_ast a)
Return number of patterns used in quantifier.
Z3_ast_vector Z3_API Z3_polynomial_subresultants(__in Z3_context c, __in Z3_ast p, __in Z3_ast q, __in Z3_ast x)
Return the nonzero subresultants of p and q with respect to the "variable" x.
static uint Z3_get_quantifier_num_no_patterns(Z3_context a0, Z3_ast a1)
Z3_lbool Z3_API Z3_get_implied_equalities(__in Z3_context c, __in Z3_solver s, __in unsigned num_terms, __in_ecount(num_terms) Z3_ast const terms[], __out_ecount(num_terms) unsigned class_ids[])
Retrieve congruence class representatives for terms.
Z3_ast Z3_API Z3_mk_exists(__in Z3_context c, __in unsigned weight, __in unsigned num_patterns, __in_ecount(num_patterns) Z3_pattern const patterns[], __in unsigned num_decls, __in_ecount(num_decls) Z3_sort const sorts[], __in_ecount(num_decls) Z3_symbol const decl_names[], __in Z3_ast body)
Create an exists formula. Similar to Z3_mk_forall.
static Z3_sort Z3_get_smtlib_sort(Z3_context a0, uint a1)
static void Z3_param_descrs_dec_ref(Z3_context a0, Z3_param_descrs a1)
static Z3_ast Z3_mk_add(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Z3_bool Z3_API Z3_goal_inconsistent(__in Z3_context c, __in Z3_goal g)
Return true if the given goal contains the formula false.
unsigned Z3_API Z3_get_sort_id(__in Z3_context c, Z3_sort s)
Return a unique identifier for s.
Z3_rcf_num Z3_API Z3_rcf_mk_pi(__in Z3_context c)
Return Pi.
Z3_ast_vector Z3_API Z3_fixedpoint_from_string(__in Z3_context c, __in Z3_fixedpoint f, __in Z3_string s)
Parse an SMT-LIB2 string with fixedpoint rules. Add the rules to the current fixedpoint context...
static Z3_ast Z3_substitute(Z3_context a0, Z3_ast a1, uint a2, [In] Z3_ast[] a3, [In] Z3_ast[] a4)
static Z3_rcf_num Z3_rcf_inv(Z3_context a0, Z3_rcf_num a1)
static Z3_sort Z3_mk_int_sort(Z3_context a0)
static Z3_func_decl Z3_get_datatype_sort_constructor(Z3_context a0, Z3_sort a1, uint a2)
static Z3_ast Z3_mk_true(Z3_context a0)
Z3_sort Z3_API Z3_get_range(__in Z3_context c, __in Z3_func_decl d)
Return the range of the given declaration.
static Z3_sort Z3_mk_real_sort(Z3_context a0)
Z3_ast Z3_API Z3_update_term(__in Z3_context c, __in Z3_ast a, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Update the arguments of term a using the arguments args. The number of arguments num_args should coin...
static Z3_tactic Z3_tactic_cond(Z3_context a0, Z3_probe a1, Z3_tactic a2, Z3_tactic a3)
Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow...
static Z3_model Z3_solver_get_model(Z3_context a0, Z3_solver a1)
static void Z3_inc_ref(Z3_context a0, Z3_ast a1)
unsigned Z3_API Z3_get_pattern_num_terms(__in Z3_context c, __in Z3_pattern p)
Return number of terms in pattern.
static Z3_app Z3_to_app(Z3_context a0, Z3_ast a1)
static void Z3_ast_vector_inc_ref(Z3_context a0, Z3_ast_vector a1)
static Z3_ast Z3_mk_false(Z3_context a0)
unsigned Z3_API Z3_get_smtlib_num_decls(__in Z3_context c)
Return the number of declarations parsed by Z3_parse_smtlib_string or Z3_parse_smtlib_file.
static uint Z3_get_decl_num_parameters(Z3_context a0, Z3_func_decl a1)
static string Z3_ast_to_string(Z3_context a0, Z3_ast a1)
static Z3_func_decl Z3_to_func_decl(Z3_context a0, Z3_ast a1)
Z3_sort Z3_API Z3_mk_datatype(__in Z3_context c, __in Z3_symbol name, __in unsigned num_constructors, __inout_ecount(num_constructors) Z3_constructor constructors[])
Create datatype, such as lists, trees, records, enumerations or unions of records. The datatype may be recursive. Return the datatype sort.
static uint Z3_stats_get_uint_value(Z3_context a0, Z3_stats a1, uint a2)
static Z3_ast Z3_get_app_arg(Z3_context a0, Z3_app a1, uint a2)
static int Z3_model_eval(Z3_context a0, Z3_model a1, Z3_ast a2, int a3, [In, Out] ref Z3_ast a4)
Z3_ast Z3_API Z3_mk_unsigned_int(__in Z3_context c, __in unsigned v, __in Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
static Z3_ast Z3_mk_or(Z3_context a0, uint a1, [In] Z3_ast[] a2)
static void Z3_toggle_warning_messages(int a0)
static Z3_func_decl Z3_model_get_func_decl(Z3_context a0, Z3_model a1, uint a2)
static uint Z3_goal_size(Z3_context a0, Z3_goal a1)
static void Z3_del_constructor(Z3_context a0, Z3_constructor a1)
Z3_probe Z3_API Z3_probe_gt(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than the value retur...
static Z3_sort Z3_get_array_sort_domain(Z3_context a0, Z3_sort a1)
static Z3_rcf_num Z3_rcf_mk_pi(Z3_context a0)
static void Z3_del_literals(Z3_context a0, Z3_literals a1)
static Z3_func_decl Z3_get_smtlib_decl(Z3_context a0, uint a1)
static uint Z3_get_quantifier_num_no_patterns(Z3_context a0, Z3_ast a1)
static Z3_ast Z3_mk_interpolant(Z3_context a0, Z3_ast a1)
Z3_ast Z3_API Z3_goal_formula(__in Z3_context c, __in Z3_goal g, __in unsigned idx)
Return a formula from the given goal.
static Z3_stats Z3_solver_get_statistics(Z3_context a0, Z3_solver a1)
static Z3_ast Z3_get_numerator(Z3_context a0, Z3_ast a1)
Z3_bool Z3_API Z3_is_as_array(__in Z3_context c, __in Z3_ast a)
The (_ as-array f) AST node is a construct for assigning interpretations for arrays in Z3...
void Z3_API Z3_stats_inc_ref(__in Z3_context c, __in Z3_stats s)
Increment the reference counter of the given statistics object.
static Z3_ast Z3_mk_bvugt(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_probe Z3_probe_eq(Z3_context a0, Z3_probe a1, Z3_probe a2)
Z3_ast Z3_API Z3_mk_sub(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create an AST node representing args[0] - ... - args[num_args - 1].The array args must have num_args ...
unsigned Z3_API Z3_param_descrs_size(__in Z3_context c, __in Z3_param_descrs p)
Return the number of parameters in the given parameter description set.
static void Z3_soft_check_cancel(Z3_context a0)
static void Z3_apply_result_inc_ref(Z3_context a0, Z3_apply_result a1)
static uint Z3_solver_get_num_scopes(Z3_context a0, Z3_solver a1)
static Z3_ast Z3_mk_forall_const(Z3_context a0, uint a1, uint a2, [In] Z3_app[] a3, uint a4, [In] Z3_pattern[] a5, Z3_ast a6)
static Z3_ast Z3_mk_bvredand(Z3_context a0, Z3_ast a1)
double Z3_API Z3_get_decl_double_parameter(__in Z3_context c, __in Z3_func_decl d, unsigned idx)
Return the double value associated with an double parameter.
static Z3_ast Z3_substitute_vars(Z3_context a0, Z3_ast a1, uint a2, [In] Z3_ast[] a3)
static int Z3_rcf_eq(Z3_context a0, Z3_rcf_num a1, Z3_rcf_num a2)
Z3_ast Z3_API Z3_mk_bvneg_no_overflow(__in Z3_context c, __in Z3_ast t1)
Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector...
void Z3_API Z3_close_log(void)
Close interaction log.
static Z3_ast Z3_algebraic_sub(Z3_context a0, Z3_ast a1, Z3_ast a2)
Z3_ast Z3_API Z3_substitute(__in Z3_context c, __in Z3_ast a, __in unsigned num_exprs, __in_ecount(num_exprs) Z3_ast const from[], __in_ecount(num_exprs) Z3_ast const to[])
Substitute every occurrence of from[i] in a with to[i], for i smaller than num_exprs. The result is the new AST. The arrays from and to must have size num_exprs. For every i smaller than num_exprs, we must have that sort of from[i] must be equal to sort of to[i].
Z3_sort Z3_API Z3_mk_array_sort(__in Z3_context c, __in Z3_sort domain, __in Z3_sort range)
Create an array type.
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)
Z3_ast Z3_API Z3_mk_quantifier_ex(__in Z3_context c, __in Z3_bool is_forall, __in unsigned weight, __in Z3_symbol quantifier_id, __in Z3_symbol skolem_id, __in unsigned num_patterns, __in_ecount(num_patterns) Z3_pattern const patterns[], __in unsigned num_no_patterns, __in_ecount(num_no_patterns) Z3_ast const no_patterns[], __in unsigned num_decls, __in_ecount(num_decls) Z3_sort const sorts[], __in_ecount(num_decls) Z3_symbol const decl_names[], __in Z3_ast body)
Create a quantifier - universal or existential, with pattern hints, no patterns, and attributes...
static void Z3_global_param_set(string a0, string a1)
void Z3_API Z3_ast_map_erase(__in Z3_context c, __in Z3_ast_map m, __in Z3_ast k)
Erase a key from the map.
static uint Z3_get_num_literals(Z3_context a0, Z3_literals a1)
static void Z3_tactic_dec_ref(Z3_context a0, Z3_tactic a1)
Z3_bool Z3_API Z3_is_eq_ast(__in Z3_context c, __in Z3_ast t1, Z3_ast t2)
compare terms.
static int Z3_fixedpoint_query_relations(Z3_context a0, Z3_fixedpoint a1, uint a2, [In] Z3_func_decl[] a3)
static uint Z3_goal_precision(Z3_context a0, Z3_goal a1)
static Z3_ast Z3_goal_formula(Z3_context a0, Z3_goal a1, uint a2)
void Z3_API Z3_params_set_symbol(__in Z3_context c, __in Z3_params p, __in Z3_symbol k, __in Z3_symbol v)
Add a symbol parameter k with value v to the parameter set p.
static Z3_sort Z3_get_domain(Z3_context a0, Z3_func_decl a1, uint a2)
static Z3_ast Z3_mk_forall(Z3_context a0, uint a1, uint a2, [In] Z3_pattern[] a3, uint a4, [In] Z3_sort[] a5, [In] IntPtr[] a6, Z3_ast a7)
static uint Z3_get_ast_hash(Z3_context a0, Z3_ast a1)
static Z3_ast Z3_mk_gt(Z3_context a0, Z3_ast a1, Z3_ast a2)
Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal(__in Z3_context c)
Return a new infinitesimal that is smaller than all elements in the Z3 field.
static Z3_ast Z3_mk_store(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3)
Z3_sort Z3_API Z3_get_decl_sort_parameter(__in Z3_context c, __in Z3_func_decl d, unsigned idx)
Return the sort value associated with a sort parameter.
static Z3_ast Z3_translate(Z3_context a0, Z3_ast a1, Z3_context a2)
static Z3_tactic Z3_tactic_try_for(Z3_context a0, Z3_tactic a1, uint a2)
Z3_ast Z3_API Z3_get_quantifier_no_pattern_ast(__in Z3_context c, __in Z3_ast a, unsigned i)
Return i'th no_pattern.
static void Z3_persist_ast(Z3_context a0, Z3_ast a1, uint a2)
void Z3_API Z3_model_dec_ref(__in Z3_context c, __in Z3_model m)
Decrement the reference counter of the given model.
Z3_ast Z3_API Z3_parse_smtlib2_string(__in Z3_context c, __in Z3_string str, __in unsigned num_sorts, __in_ecount(num_sorts) Z3_symbol const sort_names[], __in_ecount(num_sorts) Z3_sort const sorts[], __in unsigned num_decls, __in_ecount(num_decls) Z3_symbol const decl_names[], __in_ecount(num_decls) Z3_func_decl const decls[])
Parse the given string using the SMT-LIB2 parser.
Z3_ast Z3_API Z3_mk_gt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Create greater than.
static void Z3_disable_literal(Z3_context a0, Z3_literals a1, uint a2)
Z3_ast Z3_API Z3_mk_bvshl(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Shift left.
static Z3_tactic Z3_tactic_fail(Z3_context a0)
static Z3_stats Z3_fixedpoint_get_statistics(Z3_context a0, Z3_fixedpoint a1)
static Z3_ast Z3_simplify_ex(Z3_context a0, Z3_ast a1, Z3_params a2)
static Z3_ast Z3_mk_app(Z3_context a0, Z3_func_decl a1, uint a2, [In] Z3_ast[] a3)
Z3_ast Z3_API Z3_mk_bvsdiv(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed division.
static uint Z3_func_interp_get_num_entries(Z3_context a0, Z3_func_interp a1)
static Z3_tactic Z3_tactic_par_and_then(Z3_context a0, Z3_tactic a1, Z3_tactic a2)
void Z3_API Z3_global_param_set(__in Z3_string param_id, __in Z3_string param_value)
Set a global (or module) parameter. This setting is shared by all Z3 contexts.
Z3_func_interp Z3_API Z3_model_get_func_interp(__in Z3_context c, __in Z3_model m, __in Z3_func_decl f)
Return the interpretation of the function f in the model m. Return NULL, if the model does not assign...
static void Z3_func_entry_inc_ref(Z3_context a0, Z3_func_entry a1)
static string Z3_solver_to_string(Z3_context a0, Z3_solver a1)
Z3_ast Z3_API Z3_mk_bvslt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed less than.
static Z3_ast Z3_mk_implies(Z3_context a0, Z3_ast a1, Z3_ast a2)
static int Z3_rcf_lt(Z3_context a0, Z3_rcf_num a1, Z3_rcf_num a2)
Z3_ast Z3_API Z3_pattern_to_ast(__in Z3_context c, __in Z3_pattern p)
Convert a Z3_pattern into Z3_ast. This is just type casting.
static void Z3_param_descrs_inc_ref(Z3_context a0, Z3_param_descrs a1)
Z3_model Z3_API Z3_solver_get_model(__in Z3_context c, __in Z3_solver s)
Retrieve the model for the last Z3_solver_check or Z3_solver_check_assumptions.
void Z3_API Z3_set_ast_print_mode(__in Z3_context c, __in Z3_ast_print_mode mode)
Select mode for the format used for pretty-printing AST nodes.
unsigned Z3_API Z3_get_decl_num_parameters(__in Z3_context c, __in Z3_func_decl d)
Return the number of parameters associated with a declaration.
static uint Z3_model_get_num_sorts(Z3_context a0, Z3_model a1)
static void Z3_mk_datatypes(Z3_context a0, uint a1, [In] IntPtr[] a2, [Out] Z3_sort[] a3, [In, Out] Z3_constructor_list[] a4)
Z3_string Z3_API Z3_stats_to_string(__in Z3_context c, __in Z3_stats s)
Convert a statistics into a string.
Z3_bool Z3_API Z3_ast_map_contains(__in Z3_context c, __in Z3_ast_map m, __in Z3_ast k)
Return true if the map m contains the AST key k.
static void Z3_solver_reset(Z3_context a0, Z3_solver a1)
static int Z3_get_decl_int_parameter(Z3_context a0, Z3_func_decl a1, uint a2)
Z3_rcf_num Z3_API Z3_rcf_add(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b)
Return the value a + b.
static IntPtr Z3_probe_get_descr(Z3_context a0, string a1)
Z3_string Z3_API Z3_apply_result_to_string(__in Z3_context c, __in Z3_apply_result r)
Convert the Z3_apply_result object returned by Z3_tactic_apply into a string.
void Z3_API Z3_goal_reset(__in Z3_context c, __in Z3_goal g)
Erase all formulas from the given goal.
static uint Z3_get_decl_parameter_kind(Z3_context a0, Z3_func_decl a1, uint a2)
Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(__in Z3_context c, __in Z3_fixedpoint f)
Retrieve set of rules from fixedpoint context.
static Z3_ast Z3_mk_iff(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_param_descrs Z3_solver_get_param_descrs(Z3_context a0, Z3_solver a1)
static int Z3_solver_check(Z3_context a0, Z3_solver a1)
Z3_ast Z3_API Z3_mk_true(__in Z3_context c)
Create an AST node representing true.
static void Z3_rcf_del(Z3_context a0, Z3_rcf_num a1)
static Z3_solver Z3_mk_solver(Z3_context a0)
static Z3_goal Z3_goal_translate(Z3_context a0, Z3_goal a1, Z3_context a2)
void Z3_API Z3_apply_result_dec_ref(__in Z3_context c, __in Z3_apply_result r)
Decrement the reference counter of the given Z3_apply_result object.
Z3_sort Z3_API Z3_mk_uninterpreted_sort(__in Z3_context c, __in Z3_symbol s)
Create a free (uninterpreted) type using the given name (symbol).
static Z3_rcf_num Z3_rcf_mk_pi(Z3_context a0)
static Z3_probe Z3_probe_eq(Z3_context a0, Z3_probe a1, Z3_probe a2)
static string Z3_simplify_get_help(Z3_context a0)
static Z3_ast Z3_mk_set_add(Z3_context a0, Z3_ast a1, Z3_ast a2)
Z3_ast Z3_API Z3_mk_set_intersect(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Take the intersection of a list of sets.
static IntPtr Z3_interpolation_profile(Z3_context a0)
static uint Z3_get_search_failure(Z3_context a0)
Z3_bool Z3_API Z3_get_numeral_uint64(__in Z3_context c, __in Z3_ast v, __out unsigned __int64 *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine unsigned __int6...
static int Z3_algebraic_le(Z3_context a0, Z3_ast a1, Z3_ast a2)
Z3_tactic Z3_API Z3_tactic_fail(__in Z3_context c)
Return a tactic that always fails.
static void Z3_set_error(Z3_context a0, uint a1)
static Z3_ast Z3_mk_sub(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Z3_pattern Z3_API Z3_mk_pattern(__in Z3_context c, __in unsigned num_patterns, __in_ecount(num_patterns) Z3_ast const terms[])
Create a pattern for quantifier instantiation.
Z3_tactic Z3_API Z3_tactic_repeat(__in Z3_context c, __in Z3_tactic t, unsigned max)
Return a tactic that keeps applying t until the goal is not modified anymore or the maximum number of...
static Z3_ast Z3_mk_zero_ext(Z3_context a0, uint a1, Z3_ast a2)
static Z3_ast Z3_get_quantifier_no_pattern_ast(Z3_context a0, Z3_ast a1, uint a2)
static Z3_func_interp Z3_model_get_func_interp(Z3_context a0, Z3_model a1, Z3_func_decl a2)
static void Z3_solver_inc_ref(Z3_context a0, Z3_solver a1)
static void Z3_dec_ref(Z3_context a0, Z3_ast a1)
static uint Z3_get_symbol_kind(Z3_context a0, IntPtr a1)
static uint Z3_get_num_tactics(Z3_context a0)
static Z3_ast Z3_mk_bvsub(Z3_context a0, Z3_ast a1, Z3_ast a2)
static uint Z3_get_ast_kind(Z3_context a0, Z3_ast a1)
static Z3_ast Z3_mk_le(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast_vector Z3_fixedpoint_from_file(Z3_context a0, Z3_fixedpoint a1, string a2)
static void Z3_probe_dec_ref(Z3_context a0, Z3_probe a1)
static void Z3_fixedpoint_set_params(Z3_context a0, Z3_fixedpoint a1, Z3_params a2)
static void Z3_set_logic(Z3_context a0, string a1)
static Z3_probe Z3_probe_const(Z3_context a0, double a1)
Z3_ast_kind Z3_API Z3_get_ast_kind(__in Z3_context c, __in Z3_ast a)
Return the kind of the given AST.
void Z3_API Z3_goal_assert(__in Z3_context c, __in Z3_goal g, __in Z3_ast a)
Add a new formula a to the given goal.
static Z3_ast Z3_mk_set_subset(Z3_context a0, Z3_ast a1, Z3_ast a2)
Z3_ast_vector Z3_API Z3_ast_map_keys(__in Z3_context c, __in Z3_ast_map m)
Return the keys stored in the given map.
static void Z3_del_config(Z3_config a0)
static void Z3_fixedpoint_set_predicate_representation(Z3_context a0, Z3_fixedpoint a1, Z3_func_decl a2, uint a3, [In] IntPtr[] a4)
static uint Z3_get_bool_value(Z3_context a0, Z3_ast a1)
Z3_ast Z3_API Z3_mk_mod(__in Z3_context c, __in Z3_ast arg1, __in Z3_ast arg2)
Create an AST node representing arg1 mod arg2.The arguments must have int type.
Z3_context Z3_API Z3_mk_interpolation_context(__in Z3_config cfg)
This function generates a Z3 context suitable for generation of interpolants. Formulas can be generat...
static Z3_ast Z3_mk_bvsrem(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_stats Z3_fixedpoint_get_statistics(Z3_context a0, Z3_fixedpoint a1)
Z3_context Z3_API Z3_mk_context(__in Z3_config c)
Create a context using the given configuration.
static void Z3_ast_map_erase(Z3_context a0, Z3_ast_map a1, Z3_ast a2)
static uint Z3_get_quantifier_weight(Z3_context a0, Z3_ast a1)
static Z3_ast Z3_mk_bvsdiv_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_substitute_vars(Z3_context a0, Z3_ast a1, uint a2, [In] Z3_ast[] a3)
static Z3_ast Z3_mk_bvadd_no_underflow(Z3_context a0, Z3_ast a1, Z3_ast a2)
static int Z3_is_well_sorted(Z3_context a0, Z3_ast a1)
Z3_ast Z3_API Z3_get_context_assignment(__in Z3_context c)
Extract satisfying assignment from context as a conjunction.
static int Z3_fixedpoint_query(Z3_context a0, Z3_fixedpoint a1, Z3_ast a2)
static Z3_ast Z3_get_literal(Z3_context a0, Z3_literals a1, uint a2)
static void Z3_params_inc_ref(Z3_context a0, Z3_params a1)
static Z3_ast Z3_mk_quantifier_const_ex(Z3_context a0, int a1, uint a2, IntPtr a3, IntPtr a4, uint a5, [In] Z3_app[] a6, uint a7, [In] Z3_pattern[] a8, uint a9, [In] Z3_ast[] a10, Z3_ast a11)
static IntPtr Z3_rcf_num_to_string(Z3_context a0, Z3_rcf_num a1, int a2, int a3)
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)
void Z3_API Z3_fixedpoint_pop(Z3_context c, Z3_fixedpoint d)
Backtrack one backtracking point.
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)
Z3_bool Z3_API Z3_get_finite_domain_sort_size(__in Z3_context c, __in Z3_sort s, __out unsigned __int64 *r)
Store the size of the sort in r. Return Z3_FALSE if the call failed. That is, Z3_get_sort_kind(s) == ...
Z3_apply_result Z3_API Z3_tactic_apply_ex(Z3_context c, Z3_tactic t, Z3_goal g, Z3_params p)
Apply tactic t to the goal g using the parameter set p.
void Z3_API Z3_append_log(__in Z3_string string)
Append user-defined string to interaction log.
static int Z3_is_as_array(Z3_context a0, Z3_ast a1)
static string Z3_get_smtlib_error(Z3_context a0)
static Z3_probe Z3_probe_le(Z3_context a0, Z3_probe a1, Z3_probe a2)
static uint Z3_get_index_value(Z3_context a0, Z3_ast a1)
static IntPtr Z3_get_decl_symbol_parameter(Z3_context a0, Z3_func_decl a1, uint a2)
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)
void Z3_API Z3_get_version(__out unsigned *major, __out unsigned *minor, __out unsigned *build_number, __out unsigned *revision_number)
Return Z3 version number information.
Z3_bool Z3_API Z3_stats_is_double(__in Z3_context c, __in Z3_stats s, __in unsigned idx)
Return Z3_TRUE if the given statistical data is a double.
static int Z3_eval_func_decl(Z3_context a0, Z3_model a1, Z3_func_decl a2, [In, Out] ref Z3_ast a3)
static int Z3_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)
Z3_goal Z3_API Z3_apply_result_get_subgoal(__in Z3_context c, __in Z3_apply_result r, __in unsigned i)
Return one of the subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
static Z3_ast Z3_mk_bvudiv(Z3_context a0, Z3_ast a1, Z3_ast a2)
static IntPtr Z3_get_error_msg_ex(Z3_context a0, uint a1)
static string Z3_rcf_num_to_string(Z3_context a0, Z3_rcf_num a1, int a2, int a3)
static Z3_params Z3_mk_params(Z3_context a0)
static IntPtr Z3_get_numeral_string(Z3_context a0, Z3_ast a1)
static Z3_ast Z3_mk_numeral(Z3_context a0, string a1, Z3_sort a2)
static Z3_ast Z3_mk_and(Z3_context a0, uint a1, [In] Z3_ast[] a2)
static Z3_probe Z3_probe_lt(Z3_context a0, Z3_probe a1, Z3_probe a2)
static uint Z3_get_domain_size(Z3_context a0, Z3_func_decl a1)
static void Z3_set_error_handler(Z3_context a0, Z3_error_handler a1)
static void Z3_fixedpoint_pop(Z3_context a0, Z3_fixedpoint a1)
static Z3_ast Z3_get_quantifier_body(Z3_context a0, Z3_ast a1)
Z3_decl_kind Z3_API Z3_get_decl_kind(__in Z3_context c, __in Z3_func_decl d)
Return declaration kind corresponding to declaration.
Z3_sort Z3_API Z3_mk_tuple_sort(__in Z3_context c, __in Z3_symbol mk_tuple_name, __in unsigned num_fields, __in_ecount(num_fields) Z3_symbol const field_names[], __in_ecount(num_fields) Z3_sort const field_sorts[], __out Z3_func_decl *mk_tuple_decl, __out_ecount(num_fields) Z3_func_decl proj_decl[])
Create a tuple type.
static Z3_ast Z3_mk_bvor(Z3_context a0, Z3_ast a1, Z3_ast a2)
void Z3_API Z3_write_interpolation_problem(__in Z3_context ctx, __in unsigned num, __in_ecount(num) Z3_ast cnsts[], __in_ecount(num) unsigned parents[], __in Z3_string filename, __in unsigned num_theory, __in_ecount(num_theory) Z3_ast theory[])
static uint Z3_apply_result_get_num_subgoals(Z3_context a0, Z3_apply_result a1)
static Z3_probe Z3_probe_ge(Z3_context a0, Z3_probe a1, Z3_probe a2)
Z3_tactic Z3_API Z3_tactic_try_for(__in Z3_context c, __in Z3_tactic t, __in unsigned ms)
Return a tactic that applies t to a given goal for ms milliseconds. If t does not terminate in ms mil...
static Z3_func_entry Z3_func_interp_get_entry(Z3_context a0, Z3_func_interp a1, uint a2)
static IntPtr Z3_mk_string_symbol(Z3_context a0, string a1)
static string Z3_get_error_msg_ex(Z3_context a0, uint a1)
static Z3_func_decl Z3_model_get_const_decl(Z3_context a0, Z3_model a1, uint a2)
static IntPtr Z3_stats_to_string(Z3_context a0, Z3_stats a1)
static int Z3_model_has_interp(Z3_context a0, Z3_model a1, Z3_func_decl a2)
static IntPtr Z3_stats_get_key(Z3_context a0, Z3_stats a1, uint a2)
static Z3_ast Z3_mk_int64(Z3_context a0, Int64 a1, Z3_sort a2)
static Z3_ast Z3_mk_label(Z3_context a0, IntPtr a1, int a2, Z3_ast a3)
static uint Z3_get_decl_kind(Z3_context a0, Z3_func_decl a1)
static Z3_ast Z3_mk_forall_const(Z3_context a0, uint a1, uint a2, [In] Z3_app[] a3, uint a4, [In] Z3_pattern[] a5, Z3_ast a6)
static Z3_sort Z3_mk_set_sort(Z3_context a0, Z3_sort a1)
Z3_ast Z3_API Z3_get_quantifier_body(__in Z3_context c, __in Z3_ast a)
Return body of quantifier.
static Z3_pattern Z3_get_quantifier_pattern_ast(Z3_context a0, Z3_ast a1, uint a2)
Z3_ast Z3_API Z3_mk_ext_rotate_left(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Rotate bits of t1 to the left t2 times.
void Z3_API Z3_solver_inc_ref(__in Z3_context c, __in Z3_solver s)
Increment the reference counter of the given solver.
static void Z3_goal_inc_ref(Z3_context a0, Z3_goal a1)
static void Z3_ast_map_inc_ref(Z3_context a0, Z3_ast_map a1)
static Z3_ast Z3_app_to_ast(Z3_context a0, Z3_app a1)
static uint Z3_func_entry_get_num_args(Z3_context a0, Z3_func_entry a1)
Z3_tactic Z3_API Z3_tactic_using_params(__in Z3_context c, __in Z3_tactic t, __in Z3_params p)
Return a tactic that applies t using the given set of parameters.
static int Z3_fixedpoint_query(Z3_context a0, Z3_fixedpoint a1, Z3_ast a2)
Z3_bool Z3_API Z3_eval_decl(__in Z3_context c, __in Z3_model m, __in Z3_func_decl d, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[], __out Z3_ast *v)
Evaluate declaration given values.
static void Z3_ast_map_erase(Z3_context a0, Z3_ast_map a1, Z3_ast a2)
static void Z3_stats_dec_ref(Z3_context a0, Z3_stats a1)
static Z3_ast Z3_mk_is_int(Z3_context a0, Z3_ast a1)
static Z3_ast Z3_parse_smtlib2_string(Z3_context a0, string a1, uint a2, [In] IntPtr[] a3, [In] Z3_sort[] a4, uint a5, [In] IntPtr[] a6, [In] Z3_func_decl[] a7)
static int Z3_get_numeral_uint64(Z3_context a0, Z3_ast a1, [In, Out] ref UInt64 a2)
Z3_func_decl Z3_API Z3_get_tuple_sort_mk_decl(__in Z3_context c, __in Z3_sort t)
Return the constructor declaration of the given tuple sort.
static uint Z3_get_ast_id(Z3_context a0, Z3_ast a1)
static Z3_ast Z3_algebraic_root(Z3_context a0, Z3_ast a1, uint a2)
static Z3_ast Z3_fixedpoint_get_cover_delta(Z3_context a0, Z3_fixedpoint a1, int a2, Z3_func_decl a3)
static int Z3_get_numeral_rational_int64(Z3_context a0, Z3_ast a1, [In, Out] ref Int64 a2, [In, Out] ref Int64 a3)
Z3_ast Z3_API Z3_mk_ge(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Create greater than or equal to.
static void Z3_fixedpoint_assert(Z3_context a0, Z3_fixedpoint a1, Z3_ast a2)
static Z3_ast Z3_mk_not(Z3_context a0, Z3_ast a1)
unsigned Z3_API Z3_get_model_func_num_entries(__in Z3_context c, __in Z3_model m, __in unsigned i)
Return the number of entries of the i-th function interpretation in the given model.
static string Z3_goal_to_string(Z3_context a0, Z3_goal a1)
void Z3_API Z3_dec_ref(__in Z3_context c, __in Z3_ast a)
Decrement the reference counter of the given AST. The context c should have been created using Z3_mk_...
Z3_ast Z3_API Z3_mk_int(__in Z3_context c, __in int v, __in Z3_sort ty)
Create a numeral of an int, bit-vector, or finite-domain sort.
static Z3_ast Z3_mk_extract(Z3_context a0, uint a1, uint a2, Z3_ast a3)
static Z3_solver Z3_mk_solver_from_tactic(Z3_context a0, Z3_tactic a1)
static void Z3_disable_trace(string a0)
static int Z3_algebraic_neq(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_mk_bvredor(Z3_context a0, Z3_ast a1)
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)
Z3_tactic Z3_API Z3_tactic_and_then(__in Z3_context c, __in Z3_tactic t1, __in Z3_tactic t2)
Return a tactic that applies t1 to a given goal and t2 to every subgoal produced by t1...
static int Z3_algebraic_ge(Z3_context a0, Z3_ast a1, Z3_ast a2)
void Z3_API Z3_fixedpoint_push(Z3_context c, Z3_fixedpoint d)
Create a backtracking point.
Z3_ast Z3_API Z3_mk_bvult(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Unsigned less than.
void Z3_API Z3_del_constructor_list(__in Z3_context c, __in Z3_constructor_list clist)
Reclaim memory allocated for constructor list.
static void Z3_interrupt(Z3_context a0)
static Z3_func_decl Z3_mk_fresh_func_decl(Z3_context a0, string a1, uint a2, [In] Z3_sort[] a3, Z3_sort a4)
static Z3_sort Z3_mk_finite_domain_sort(Z3_context a0, IntPtr a1, UInt64 a2)
Z3_rcf_num Z3_API Z3_rcf_mk_rational(__in Z3_context c, __in Z3_string val)
Return a RCF rational using the given string.
static string Z3_func_decl_to_string(Z3_context a0, Z3_func_decl a1)
static Z3_ast Z3_mk_bvand(Z3_context a0, Z3_ast a1, Z3_ast a2)
Z3_ast Z3_API Z3_simplify(__in Z3_context c, __in Z3_ast a)
Interface to simplifier.
static Z3_ast Z3_mk_is_int(Z3_context a0, Z3_ast a1)
static void Z3_stats_inc_ref(Z3_context a0, Z3_stats a1)
static void Z3_stats_dec_ref(Z3_context a0, Z3_stats a1)
static Z3_ast Z3_model_get_const_interp(Z3_context a0, Z3_model a1, Z3_func_decl a2)
static Z3_ast Z3_algebraic_mul(Z3_context a0, Z3_ast a1, Z3_ast a2)
Z3_string Z3_API Z3_solver_get_help(__in Z3_context c, __in Z3_solver s)
Return a string describing all solver available parameters.
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)
void Z3_API Z3_params_set_uint(__in Z3_context c, __in Z3_params p, __in Z3_symbol k, __in unsigned v)
Add a unsigned parameter k with value v to the parameter set p.
static Z3_solver Z3_mk_simple_solver(Z3_context a0)
static Z3_probe Z3_probe_not(Z3_context a0, Z3_probe a1)
Z3_ast_vector Z3_API Z3_solver_get_unsat_core(__in Z3_context c, __in Z3_solver s)
Retrieve the unsat core for the last Z3_solver_check_assumptions The unsat core is a subset of the as...
void Z3_API Z3_del_literals(__in Z3_context c, __in Z3_literals lbls)
Delete a labels context.
void Z3_API Z3_soft_check_cancel(__in Z3_context c)
Cancel an ongoing check.
Z3_func_entry Z3_API Z3_func_interp_get_entry(__in Z3_context c, __in Z3_func_interp f, unsigned i)
Return a "point" of the given function intepretation. It represents the value of f in a particular po...
static string Z3_statistics_to_string(Z3_context a0)
Z3_tactic Z3_API Z3_tactic_skip(__in Z3_context c)
Return a tactic that just return the given goal.
static void Z3_fixedpoint_set_predicate_representation(Z3_context a0, Z3_fixedpoint a1, Z3_func_decl a2, uint a3, [In] IntPtr[] a4)
static Z3_ast Z3_mk_mul(Z3_context a0, uint a1, [In] Z3_ast[] a2)
static int Z3_get_decl_int_parameter(Z3_context a0, Z3_func_decl a1, uint a2)
static Z3_ast Z3_mk_sub(Z3_context a0, uint a1, [In] Z3_ast[] a2)
unsigned Z3_API Z3_get_smtlib_num_sorts(__in Z3_context c)
Return the number of sorts parsed by Z3_parse_smtlib_string or Z3_parse_smtlib_file.
void Z3_API Z3_set_error(__in Z3_context c, __in Z3_error_code e)
Set an error.
static void Z3_stats_inc_ref(Z3_context a0, Z3_stats a1)
static Z3_tactic Z3_tactic_cond(Z3_context a0, Z3_probe a1, Z3_tactic a2, Z3_tactic a3)
static Z3_func_decl Z3_get_smtlib_decl(Z3_context a0, uint a1)
static Z3_sort Z3_mk_datatype(Z3_context a0, IntPtr a1, uint a2, [In, Out] Z3_constructor[] a3)
Z3_solver Z3_API Z3_mk_solver_for_logic(__in Z3_context c, __in Z3_symbol logic)
Create a new solver customized for the given logic. It behaves like Z3_mk_solver if the logic is unkn...
static Z3_sort Z3_mk_bv_sort(Z3_context a0, uint a1)
Z3_bool Z3_API Z3_model_eval(__in Z3_context c, __in Z3_model m, __in Z3_ast t, __in Z3_bool model_completion, __out Z3_ast *v)
Evaluate the AST node t in the given model. Return Z3_TRUE if succeeded, and store the result in v...
void Z3_API Z3_probe_inc_ref(__in Z3_context c, __in Z3_probe p)
Increment the reference counter of the given probe.
Z3_ast Z3_API Z3_mk_bvmul(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Standard two's complement multiplication.
static int Z3_algebraic_is_zero(Z3_context a0, Z3_ast a1)
static void Z3_solver_assert(Z3_context a0, Z3_solver a1, Z3_ast a2)
Z3_goal Z3_API Z3_goal_translate(__in Z3_context source, __in Z3_goal g, __in Z3_context target)
Copy a goal g from the context source to a the context target.
static Z3_constructor_list Z3_mk_constructor_list(Z3_context a0, uint a1, [In] Z3_constructor[] a2)
static IntPtr Z3_get_symbol_string(Z3_context a0, IntPtr a1)
static void Z3_solver_pop(Z3_context a0, Z3_solver a1, uint a2)
Z3_bool Z3_API Z3_rcf_eq(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b)
Return Z3_TRUE if a == b.
static void Z3_probe_inc_ref(Z3_context a0, Z3_probe a1)
Z3_lbool Z3_API Z3_check(__in Z3_context c)
Check whether the given logical context is consistent or not.
static Z3_ast Z3_mk_le(Z3_context a0, Z3_ast a1, Z3_ast a2)
Z3_string Z3_API Z3_fixedpoint_to_string(__in Z3_context c, __in Z3_fixedpoint f, __in unsigned num_queries, __in_ecount(num_queries) Z3_ast queries[])
Print the current rules and background axioms as a string.
static void Z3_append_log(string a0)
Z3_func_decl Z3_API Z3_get_model_constant(__in Z3_context c, __in Z3_model m, __in unsigned i)
Return the i-th constant in the given model.
static string Z3_probe_get_descr(Z3_context a0, string a1)
Z3_ast Z3_API Z3_mk_set_del(__in Z3_context c, __in Z3_ast set, __in Z3_ast elem)
Remove an element to a set.
static Z3_context Z3_mk_context_rc(Z3_config a0)
Z3_probe Z3_API Z3_probe_not(__in Z3_context x, __in Z3_probe p)
Return a probe that evaluates to "true" when p does not evaluate to true.
static IntPtr Z3_get_numeral_decimal_string(Z3_context a0, Z3_ast a1, uint a2)
static int Z3_algebraic_gt(Z3_context a0, Z3_ast a1, Z3_ast a2)
static int Z3_rcf_gt(Z3_context a0, Z3_rcf_num a1, Z3_rcf_num a2)
unsigned Z3_API Z3_stats_size(__in Z3_context c, __in Z3_stats s)
Return the number of statistical data in s.
Z3_pattern Z3_API Z3_get_quantifier_pattern_ast(__in Z3_context c, __in Z3_ast a, unsigned i)
Return i'th pattern.
void Z3_API Z3_solver_assert(__in Z3_context c, __in Z3_solver s, __in Z3_ast a)
Assert a constraint into the solver.
static void Z3_set_ast_print_mode(Z3_context a0, uint a1)
static Z3_ast Z3_mk_real(Z3_context a0, int a1, int a2)
static Z3_literals Z3_get_relevant_labels(Z3_context a0)
static Z3_ast Z3_mk_concat(Z3_context a0, Z3_ast a1, Z3_ast a2)
Z3_symbol_kind Z3_API Z3_get_symbol_kind(__in Z3_context c, __in Z3_symbol s)
Return Z3_INT_SYMBOL if the symbol was constructed using Z3_mk_int_symbol, and Z3_STRING_SYMBOL if th...
static Z3_tactic Z3_tactic_try_for(Z3_context a0, Z3_tactic a1, uint a2)
static uint Z3_get_decl_kind(Z3_context a0, Z3_func_decl a1)
unsigned Z3_API Z3_func_interp_get_num_entries(__in Z3_context c, __in Z3_func_interp f)
Return the number of entries in the given function interpretation.
static int Z3_is_well_sorted(Z3_context a0, Z3_ast a1)
void Z3_API Z3_persist_ast(__in Z3_context c, __in Z3_ast a, __in unsigned num_scopes)
Persist AST through num_scopes pops. This function is only relevant if c was created using Z3_mk_cont...
static uint Z3_apply_result_get_num_subgoals(Z3_context a0, Z3_apply_result a1)
static string Z3_get_probe_name(Z3_context a0, uint a1)
static Z3_tactic Z3_tactic_and_then(Z3_context a0, Z3_tactic a1, Z3_tactic a2)
Z3_ast Z3_API Z3_mk_map(__in Z3_context c, __in Z3_func_decl f, unsigned n, __in Z3_ast const *args)
map f on the the argument arrays.
static void Z3_fixedpoint_add_rule(Z3_context a0, Z3_fixedpoint a1, Z3_ast a2, IntPtr a3)
BEGIN_MLAPI_EXCLUDE Z3_string Z3_API Z3_get_error_msg_ex(__in Z3_context c, __in Z3_error_code err)
Return a string describing the given error code.
static int Z3_stats_is_double(Z3_context a0, Z3_stats a1, uint a2)
static Z3_ast Z3_mk_sign_ext(Z3_context a0, uint a1, Z3_ast a2)
static Z3_tactic Z3_tactic_fail_if(Z3_context a0, Z3_probe a1)
Z3_ast_vector Z3_API Z3_get_interpolant(__in Z3_context c, __in Z3_ast pf, __in Z3_ast pat, __in Z3_params p)
Z3_lbool Z3_API Z3_fixedpoint_query(__in Z3_context c, __in Z3_fixedpoint d, __in Z3_ast query)
Pose a query against the asserted rules.
static Z3_ast Z3_goal_formula(Z3_context a0, Z3_goal a1, uint a2)
Z3_string Z3_API Z3_goal_to_string(__in Z3_context c, __in Z3_goal g)
Convert a goal into a string.
Z3_lbool Z3_API Z3_fixedpoint_query_relations(__in Z3_context c, __in Z3_fixedpoint d, __in unsigned num_relations, __in_ecount(num_relations) Z3_func_decl const relations[])
Pose multiple queries against the asserted rules.
static IntPtr Z3_get_label_symbol(Z3_context a0, Z3_literals a1, uint a2)
void Z3_API Z3_parse_smtlib_string(__in Z3_context c, __in Z3_string str, __in unsigned num_sorts, __in_ecount(num_sorts) Z3_symbol const sort_names[], __in_ecount(num_sorts) Z3_sort const sorts[], __in unsigned num_decls, __in_ecount(num_decls) Z3_symbol const decl_names[], __in_ecount(num_decls) Z3_func_decl const decls[])
Parse the given string using the SMT-LIB parser.
static Z3_rcf_num Z3_rcf_div(Z3_context a0, Z3_rcf_num a1, Z3_rcf_num a2)
static Z3_rcf_num Z3_rcf_mk_e(Z3_context a0)
static string Z3_get_error_msg(uint a0)
Z3_ast Z3_API Z3_mk_bvnot(__in Z3_context c, __in Z3_ast t1)
Bitwise negation.
static void Z3_params_set_double(Z3_context a0, Z3_params a1, IntPtr a2, double a3)
static Z3_func_decl Z3_mk_func_decl(Z3_context a0, IntPtr a1, uint a2, [In] Z3_sort[] a3, Z3_sort a4)
static Z3_ast Z3_mk_div(Z3_context a0, Z3_ast a1, Z3_ast a2)
static uint Z3_get_implied_equalities(Z3_context a0, Z3_solver a1, uint a2, [In] Z3_ast[] a3, [Out] uint[] a4)
Z3_ast Z3_API Z3_mk_bvmul_no_underflow(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflo...
Z3_func_decl Z3_API Z3_get_smtlib_decl(__in Z3_context c, __in unsigned i)
Return the i-th declaration parsed by the last call to Z3_parse_smtlib_string or Z3_parse_smtlib_file...
static void Z3_fixedpoint_inc_ref(Z3_context a0, Z3_fixedpoint a1)
double Z3_API Z3_stats_get_double_value(__in Z3_context c, __in Z3_stats s, __in unsigned idx)
Return the double value of the given statistical data.
Z3_ast Z3_API Z3_mk_false(__in Z3_context c)
Create an AST node representing false.
static Z3_ast Z3_mk_bvnand(Z3_context a0, Z3_ast a1, Z3_ast a2)
static void Z3_fixedpoint_update_rule(Z3_context a0, Z3_fixedpoint a1, Z3_ast a2, IntPtr a3)
static Z3_tactic Z3_tactic_par_or(Z3_context a0, uint a1, [In] Z3_tactic[] a2)
static int Z3_is_as_array(Z3_context a0, Z3_ast a1)
Z3_string Z3_API Z3_params_to_string(__in Z3_context c, __in Z3_params p)
Convert a parameter set into a string. This function is mainly used for printing the contents of a pa...
static Z3_rcf_num Z3_rcf_mk_small_int(Z3_context a0, int a1)
Z3_ast Z3_API Z3_mk_set_union(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Take the union of a list of sets.
static uint Z3_func_entry_get_num_args(Z3_context a0, Z3_func_entry a1)
static uint Z3_get_relation_arity(Z3_context a0, Z3_sort a1)
void Z3_API Z3_ast_vector_push(__in Z3_context c, __in Z3_ast_vector v, __in Z3_ast a)
Add the AST a in the end of the AST vector v. The size of v is increased by one.
void Z3_API Z3_solver_push(__in Z3_context c, __in Z3_solver s)
Create a backtracking point.
unsigned Z3_API Z3_goal_num_exprs(__in Z3_context c, __in Z3_goal g)
Return the number of formulas, subformulas and terms in the given goal.
static Z3_ast Z3_mk_bvsrem(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_literals Z3_get_guessed_literals(Z3_context a0)
unsigned Z3_API Z3_get_model_num_funcs(__in Z3_context c, __in Z3_model m)
Return the number of function interpretations in the given model.
static void Z3_disable_trace(string a0)
static Z3_func_decl Z3_get_decl_func_decl_parameter(Z3_context a0, Z3_func_decl a1, uint a2)
static uint Z3_get_num_literals(Z3_context a0, Z3_literals a1)
static Z3_ast Z3_parse_smtlib2_string(Z3_context a0, string a1, uint a2, [In] IntPtr[] a3, [In] Z3_sort[] a4, uint a5, [In] IntPtr[] a6, [In] Z3_func_decl[] a7)
static void Z3_solver_dec_ref(Z3_context a0, Z3_solver a1)
static uint Z3_func_interp_get_arity(Z3_context a0, Z3_func_interp a1)
static uint Z3_get_index_value(Z3_context a0, Z3_ast a1)
static Z3_ast_vector Z3_solver_get_assertions(Z3_context a0, Z3_solver a1)
Z3_sort Z3_API Z3_get_array_sort_domain(__in Z3_context c, __in Z3_sort t)
Return the domain of the given array sort.
Z3_ast Z3_API Z3_mk_ite(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2, __in Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
static uint Z3_get_quantifier_num_bound(Z3_context a0, Z3_ast a1)
static Z3_ast Z3_mk_repeat(Z3_context a0, uint a1, Z3_ast a2)
static void Z3_ast_vector_push(Z3_context a0, Z3_ast_vector a1, Z3_ast a2)
static Z3_pattern Z3_get_quantifier_pattern_ast(Z3_context a0, Z3_ast a1, uint a2)
Z3_string Z3_API Z3_get_decl_rational_parameter(__in Z3_context c, __in Z3_func_decl d, unsigned idx)
Return the rational value, as a string, associated with a rational parameter.
static void Z3_param_descrs_dec_ref(Z3_context a0, Z3_param_descrs a1)
void Z3_API Z3_goal_dec_ref(__in Z3_context c, __in Z3_goal g)
Decrement the reference counter of the given goal.
static int Z3_fixedpoint_query_relations(Z3_context a0, Z3_fixedpoint a1, uint a2, [In] Z3_func_decl[] a3)
Z3_rcf_num Z3_API Z3_rcf_mk_small_int(__in Z3_context c, __in int val)
Return a RCF small integer.
void Z3_API Z3_block_literals(__in Z3_context c, __in Z3_literals lbls)
Block subsequent checks using the remaining enabled labels.
void Z3_API Z3_pop(__in Z3_context c, __in unsigned num_scopes)
Backtrack.
static int Z3_get_numeral_small(Z3_context a0, Z3_ast a1, [In, Out] ref Int64 a2, [In, Out] ref Int64 a3)
static Z3_ast Z3_mk_or(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Z3_literals Z3_API Z3_get_guessed_literals(__in Z3_context c)
Retrieve the set of literals that whose assignment were guess, but not propagated during the search...
void Z3_API Z3_fixedpoint_add_fact(__in Z3_context c, __in Z3_fixedpoint d, __in Z3_func_decl r, __in unsigned num_args, __in_ecount(num_args) unsigned args[])
Add a Database fact.
static Z3_tactic Z3_mk_tactic(Z3_context a0, string a1)
Z3_tactic Z3_API Z3_tactic_cond(__in Z3_context c, __in Z3_probe p, __in Z3_tactic t1, __in Z3_tactic t2)
Return a tactic that applies t1 to a given goal if the probe p evaluates to true, and t2 if p evaluat...
static string Z3_fixedpoint_get_help(Z3_context a0, Z3_fixedpoint a1)
static int Z3_get_finite_domain_sort_size(Z3_context a0, Z3_sort a1, [In, Out] ref UInt64 a2)
static int Z3_algebraic_lt(Z3_context a0, Z3_ast a1, Z3_ast a2)
static int Z3_check_and_get_model(Z3_context a0, [In, Out] ref Z3_model a1)
static IntPtr Z3_mk_int_symbol(Z3_context a0, int a1)
static IntPtr Z3_sort_to_string(Z3_context a0, Z3_sort a1)
static Z3_ast Z3_mk_unsigned_int(Z3_context a0, uint a1, Z3_sort a2)
static Z3_ast Z3_mk_eq(Z3_context a0, Z3_ast a1, Z3_ast a2)
Z3_string Z3_API Z3_probe_get_descr(__in Z3_context c, __in Z3_string name)
Return a string containing a description of the probe with the given name.
static Z3_func_decl Z3_get_as_array_func_decl(Z3_context a0, Z3_ast a1)
static void Z3_func_interp_dec_ref(Z3_context a0, Z3_func_interp a1)
static int Z3_global_param_get(string a0, out IntPtr a1)
unsigned Z3_API Z3_model_get_num_funcs(__in Z3_context c, __in Z3_model m)
Return the number of function interpretations in the given model.
static Z3_ast Z3_mk_bvxnor(Z3_context a0, Z3_ast a1, Z3_ast a2)
static void Z3_fixedpoint_add_fact(Z3_context a0, Z3_fixedpoint a1, Z3_func_decl a2, uint a3, [In] uint[] a4)
static Z3_context Z3_mk_context_rc(Z3_config a0)
static int Z3_rcf_lt(Z3_context a0, Z3_rcf_num a1, Z3_rcf_num a2)
Z3_ast Z3_API Z3_mk_bvredor(__in Z3_context c, __in Z3_ast t1)
Take disjunction of bits in vector, return vector of length 1.
Z3_ast Z3_API Z3_mk_bvmul_no_overflow(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2, Z3_bool is_signed)
Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow...
Z3_ast Z3_API Z3_mk_bvsrem(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed remainder (sign follows dividend).
static void Z3_fixedpoint_add_cover(Z3_context a0, Z3_fixedpoint a1, int a2, Z3_func_decl a3, Z3_ast a4)
static Z3_sort Z3_model_get_sort(Z3_context a0, Z3_model a1, uint a2)
static int Z3_goal_is_decided_unsat(Z3_context a0, Z3_goal a1)
static Z3_ast Z3_mk_bvadd_no_underflow(Z3_context a0, Z3_ast a1, Z3_ast a2)
void Z3_API Z3_fixedpoint_inc_ref(__in Z3_context c, __in Z3_fixedpoint d)
Increment the reference counter of the given fixedpoint context.
Z3_ast Z3_API Z3_mk_implies(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Create an AST node representing t1 implies t2.
static void Z3_tactic_inc_ref(Z3_context a0, Z3_tactic a1)
void Z3_API Z3_fixedpoint_add_rule(__in Z3_context c, __in Z3_fixedpoint d, __in Z3_ast rule, __in Z3_symbol name)
Add a universal Horn clause as a named rule. The horn_rule should be of the form: ...
static Z3_ast Z3_mk_set_del(Z3_context a0, Z3_ast a1, Z3_ast a2)
static void Z3_func_entry_dec_ref(Z3_context a0, Z3_func_entry a1)
static uint Z3_get_model_num_constants(Z3_context a0, Z3_model a1)
static int Z3_is_quantifier_forall(Z3_context a0, Z3_ast a1)
static IntPtr Z3_tactic_get_descr(Z3_context a0, string a1)
static Z3_ast Z3_mk_ext_rotate_left(Z3_context a0, Z3_ast a1, Z3_ast a2)
static int Z3_check_and_get_model(Z3_context a0, [In, Out] ref Z3_model a1)
static string Z3_benchmark_to_smtlib_string(Z3_context a0, string a1, string a2, string a3, string a4, uint a5, [In] Z3_ast[] a6, Z3_ast a7)
static uint Z3_model_get_num_funcs(Z3_context a0, Z3_model a1)
static Z3_func_decl Z3_get_tuple_sort_field_decl(Z3_context a0, Z3_sort a1, uint a2)
Z3_ast Z3_API Z3_mk_bvugt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Unsigned greater than.
static Z3_ast Z3_mk_bvsdiv_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2)
Z3_string Z3_API Z3_stats_get_key(__in Z3_context c, __in Z3_stats s, __in unsigned idx)
Return the key (a string) for a particular statistical data.
Z3_func_decl Z3_API Z3_get_datatype_sort_constructor(__in Z3_context c, __in Z3_sort t, unsigned idx)
Return idx'th constructor.
static Z3_ast Z3_sort_to_ast(Z3_context a0, Z3_sort a1)
void Z3_API Z3_func_interp_inc_ref(__in Z3_context c, __in Z3_func_interp f)
Increment the reference counter of the given Z3_func_interp object.
static Z3_constructor Z3_mk_constructor(Z3_context a0, IntPtr a1, IntPtr a2, uint a3, [In] IntPtr[] a4, [In] Z3_sort[] a5, [In] uint[] a6)
static int Z3_goal_is_decided_unsat(Z3_context a0, Z3_goal a1)
static int Z3_eval(Z3_context a0, Z3_model a1, Z3_ast a2, [In, Out] ref Z3_ast a3)
static Z3_ast Z3_mk_bvule(Z3_context a0, Z3_ast a1, Z3_ast a2)
Z3_ast Z3_API Z3_mk_and(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].The array args must have num_arg...
unsigned Z3_API Z3_get_arity(__in Z3_context c, __in Z3_func_decl d)
Alias for Z3_get_domain_size.
static Z3_ast Z3_mk_bvslt(Z3_context a0, Z3_ast a1, Z3_ast a2)
static IntPtr Z3_simplify_get_help(Z3_context a0)
int Z3_API Z3_get_symbol_int(__in Z3_context c, __in Z3_symbol s)
Return the symbol int value.
static Z3_ast Z3_mk_power(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_sort Z3_get_sort(Z3_context a0, Z3_ast a1)
static Z3_ast Z3_mk_bvmul_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2, int a3)
static Z3_ast Z3_mk_bvmul_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2, int a3)
Z3_ast Z3_API Z3_mk_select(__in Z3_context c, __in Z3_ast a, __in Z3_ast i)
Array read. The argument a is the array and i is the index of the array that gets read...
Z3_bool Z3_API Z3_get_numeral_small(__in Z3_context c, __in Z3_ast a, __out __int64 *num, __out __int64 *den)
Return numeral value, as a pair of 64 bit numbers if the representation fits.
unsigned Z3_API Z3_get_ast_id(__in Z3_context c, Z3_ast t)
Return a unique identifier for t.
static Z3_tactic Z3_tactic_fail_if_not_decided(Z3_context a0)
Z3_ast Z3_API Z3_mk_bvsle(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed less than or equal to.
static Z3_sort Z3_model_get_sort(Z3_context a0, Z3_model a1, uint a2)
Z3_string Z3_API Z3_pattern_to_string(__in Z3_context c, __in Z3_pattern p)
static Z3_ast Z3_get_algebraic_number_upper(Z3_context a0, Z3_ast a1, uint a2)
Z3_rcf_num Z3_API Z3_rcf_sub(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b)
Return the value a - b.
static Z3_ast Z3_mk_const_array(Z3_context a0, Z3_sort a1, Z3_ast a2)
Z3_ast Z3_API Z3_mk_quantifier_const_ex(__in Z3_context c, Z3_bool is_forall, unsigned weight, __in Z3_symbol quantifier_id, __in Z3_symbol skolem_id, unsigned num_bound, __in_ecount(num_bound) Z3_app const bound[], unsigned num_patterns, __in_ecount(num_patterns) Z3_pattern const patterns[], unsigned num_no_patterns, __in_ecount(num_no_patterns) Z3_ast const no_patterns[], __in Z3_ast body)
Create a universal or existential quantifier using a list of constants that will form the set of boun...
Z3_ast Z3_API Z3_get_model_func_entry_value(__in Z3_context c, __in Z3_model m, __in unsigned i, __in unsigned j)
Return the return value of the j-th entry of the i-th function interpretation in the given model...
static Z3_ast Z3_mk_gt(Z3_context a0, Z3_ast a1, Z3_ast a2)
Z3_symbol Z3_API Z3_param_descrs_get_name(__in Z3_context c, __in Z3_param_descrs p, __in unsigned i)
Return the number of parameters in the given parameter description set.
static uint Z3_get_sort_id(Z3_context a0, Z3_sort a1)
static void Z3_fixedpoint_add_rule(Z3_context a0, Z3_fixedpoint a1, Z3_ast a2, IntPtr a3)
Z3_bool Z3_API Z3_rcf_neq(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b)
Return Z3_TRUE if a != b.
Z3_bool Z3_API Z3_eval_func_decl(__in Z3_context c, __in Z3_model m, __in Z3_func_decl decl, __out Z3_ast *v)
Return the value of the given constant or function in the given model.
Z3_string Z3_API Z3_get_numeral_decimal_string(__in Z3_context c, __in Z3_ast a, __in unsigned precision)
Return numeral as a string in decimal notation. The result has at most precision decimal places...
static Z3_ast Z3_mk_xor(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_goal Z3_goal_translate(Z3_context a0, Z3_goal a1, Z3_context a2)
static Z3_probe Z3_probe_const(Z3_context a0, double a1)
Z3_bool Z3_API Z3_set_logic(__in Z3_context c, __in Z3_string logic)
Set the SMTLIB logic to be used in the given logical context. It is incorrect to invoke this function...
Z3_ast Z3_API Z3_mk_lt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Create less than.
Z3_func_decl Z3_API Z3_model_get_const_decl(__in Z3_context c, __in Z3_model m, __in unsigned i)
Return the i-th constant in the given model.
unsigned Z3_API Z3_get_ast_hash(__in Z3_context c, __in Z3_ast a)
Return a hash code for the given AST.
static int Z3_model_has_interp(Z3_context a0, Z3_model a1, Z3_func_decl a2)
void Z3_API Z3_query_constructor(__in Z3_context c, __in Z3_constructor constr, __in unsigned num_fields, __out Z3_func_decl *constructor, __out Z3_func_decl *tester, __out_ecount(num_fields) Z3_func_decl accessors[])
Query constructor for declared functions.
static void Z3_set_ast_print_mode(Z3_context a0, uint a1)
static Z3_sort Z3_get_array_sort_domain(Z3_context a0, Z3_sort a1)
static Z3_ast Z3_mk_bvredand(Z3_context a0, Z3_ast a1)
Z3_ast_vector Z3_API Z3_fixedpoint_from_file(__in Z3_context c, __in Z3_fixedpoint f, __in Z3_string s)
Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context...
static uint Z3_get_app_num_args(Z3_context a0, Z3_app a1)
static uint Z3_get_tuple_sort_num_fields(Z3_context a0, Z3_sort a1)
static void Z3_rcf_get_numerator_denominator(Z3_context a0, Z3_rcf_num a1, [In, Out] ref Z3_rcf_num a2, [In, Out] ref Z3_rcf_num a3)
static int Z3_is_quantifier_forall(Z3_context a0, Z3_ast a1)
static Z3_ast Z3_mk_ite(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3)
static Z3_ast Z3_mk_bvadd(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_mk_bvsdiv(Z3_context a0, Z3_ast a1, Z3_ast a2)
static uint Z3_get_quantifier_num_bound(Z3_context a0, Z3_ast a1)
Z3_string Z3_API Z3_interpolation_profile(__in Z3_context ctx)
static Z3_func_decl Z3_get_tuple_sort_field_decl(Z3_context a0, Z3_sort a1, uint a2)
static Z3_ast Z3_mk_ge(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_mk_int(Z3_context a0, int a1, Z3_sort a2)
static void Z3_parse_smtlib_file(Z3_context a0, string a1, uint a2, [In] IntPtr[] a3, [In] Z3_sort[] a4, uint a5, [In] IntPtr[] a6, [In] Z3_func_decl[] a7)
static void Z3_ast_vector_dec_ref(Z3_context a0, Z3_ast_vector a1)
static Z3_ast Z3_mk_xor(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast_vector Z3_get_interpolant(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_params a3)
static Z3_rcf_num Z3_rcf_neg(Z3_context a0, Z3_rcf_num a1)
static Z3_ast Z3_get_model_func_entry_value(Z3_context a0, Z3_model a1, uint a2, uint a3)
static Z3_ast Z3_mk_bvslt(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_mk_repeat(Z3_context a0, uint a1, Z3_ast a2)
Z3_ast Z3_API Z3_mk_bvsub(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Standard two's complement subtraction.
static Z3_ast Z3_get_model_func_entry_arg(Z3_context a0, Z3_model a1, uint a2, uint a3, uint a4)
static Z3_ast Z3_mk_iff(Z3_context a0, Z3_ast a1, Z3_ast a2)
static int Z3_algebraic_lt(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_sort Z3_get_relation_column(Z3_context a0, Z3_sort a1, uint a2)
static Z3_ast Z3_get_app_arg(Z3_context a0, Z3_app a1, uint a2)
static Z3_ast Z3_mk_and(Z3_context a0, uint a1, [In] Z3_ast[] a2)
static int Z3_model_eval(Z3_context a0, Z3_model a1, Z3_ast a2, int a3, [In, Out] ref Z3_ast a4)
static void Z3_del_literals(Z3_context a0, Z3_literals a1)
void Z3_API Z3_params_set_double(__in Z3_context c, __in Z3_params p, __in Z3_symbol k, __in double v)
Add a double parameter k with value v to the parameter set p.
static Z3_ast Z3_mk_unsigned_int64(Z3_context a0, UInt64 a1, Z3_sort a2)
static Z3_ast Z3_mk_distinct(Z3_context a0, uint a1, [In] Z3_ast[] a2)
Z3_ast Z3_API Z3_mk_real2int(__in Z3_context c, __in Z3_ast t1)
Coerce a real to an integer.
Z3_ast Z3_API Z3_mk_int2real(__in Z3_context c, __in Z3_ast t1)
Coerce an integer to a real.
static Z3_rcf_num Z3_rcf_power(Z3_context a0, Z3_rcf_num a1, uint a2)
Z3_bool Z3_API Z3_algebraic_is_pos(__in Z3_context c, __in Z3_ast a)
Return the Z3_TRUE if a is positive, and Z3_FALSE otherwise.
Z3_string Z3_API Z3_sort_to_string(__in Z3_context c, __in Z3_sort s)
Z3_bool Z3_API Z3_rcf_ge(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b)
Return Z3_TRUE if a >= b.
static void Z3_param_descrs_inc_ref(Z3_context a0, Z3_param_descrs a1)
Z3_string Z3_API Z3_ast_to_string(__in Z3_context c, __in Z3_ast a)
Convert the given AST node into a string.
static string Z3_ast_map_to_string(Z3_context a0, Z3_ast_map a1)
Z3_ast Z3_API Z3_get_pattern(__in Z3_context c, __in Z3_pattern p, __in unsigned idx)
Return i'th ast in pattern.
static Z3_ast Z3_mk_select(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast_vector Z3_fixedpoint_get_rules(Z3_context a0, Z3_fixedpoint a1)
static Z3_ast Z3_mk_int2bv(Z3_context a0, uint a1, Z3_ast a2)
static Z3_ast Z3_func_entry_get_arg(Z3_context a0, Z3_func_entry a1, uint a2)
static Z3_ast Z3_get_denominator(Z3_context a0, Z3_ast a1)
static string Z3_apply_result_to_string(Z3_context a0, Z3_apply_result a1)
static int Z3_open_log(string a0)
Z3_ast Z3_API Z3_solver_get_proof(__in Z3_context c, __in Z3_solver s)
Retrieve the proof for the last Z3_solver_check or Z3_solver_check_assumptions.
static Z3_ast Z3_mk_bvnor(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_algebraic_root(Z3_context a0, Z3_ast a1, uint a2)
static IntPtr Z3_mk_string_symbol(Z3_context a0, string a1)
Z3_solver Z3_API Z3_mk_simple_solver(__in Z3_context c)
Create a new (incremental) solver.
Z3_probe Z3_API Z3_probe_const(__in Z3_context x, __in double val)
Return a probe that always evaluates to val.
static Z3_param_descrs Z3_simplify_get_param_descrs(Z3_context a0)
static uint Z3_goal_size(Z3_context a0, Z3_goal a1)
static void Z3_set_error(Z3_context a0, uint a1)
static Z3_tactic Z3_tactic_and_then(Z3_context a0, Z3_tactic a1, Z3_tactic a2)
Z3_string Z3_API Z3_statistics_to_string(__in Z3_context c)
Return runtime statistics as a string.
static Z3_sort Z3_mk_array_sort(Z3_context a0, Z3_sort a1, Z3_sort a2)
static int Z3_rcf_le(Z3_context a0, Z3_rcf_num a1, Z3_rcf_num a2)
Z3_sort Z3_API Z3_mk_int_sort(__in Z3_context c)
Create the integer type.
static uint Z3_get_error_code(Z3_context a0)
static void Z3_ast_vector_resize(Z3_context a0, Z3_ast_vector a1, uint a2)
Z3_ast Z3_API Z3_get_smtlib_assumption(__in Z3_context c, __in unsigned i)
Return the i-th assumption parsed by the last call to Z3_parse_smtlib_string or Z3_parse_smtlib_file...
static uint Z3_get_arity(Z3_context a0, Z3_func_decl a1)
Z3_string Z3_API Z3_tactic_get_descr(__in Z3_context c, __in Z3_string name)
Return a string containing a description of the tactic with the given name.
static Z3_ast Z3_mk_quantifier_ex(Z3_context a0, int a1, uint a2, IntPtr a3, IntPtr a4, uint a5, [In] Z3_pattern[] a6, uint a7, [In] Z3_ast[] a8, uint a9, [In] Z3_sort[] a10, [In] IntPtr[] a11, Z3_ast a12)
static uint Z3_get_model_func_entry_num_args(Z3_context a0, Z3_model a1, uint a2, uint a3)
static Z3_ast Z3_mk_bvadd(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast_vector Z3_model_get_sort_universe(Z3_context a0, Z3_model a1, Z3_sort a2)
static Z3_ast Z3_pattern_to_ast(Z3_context a0, Z3_pattern a1)
Z3_ast Z3_API Z3_get_denominator(__in Z3_context c, __in Z3_ast a)
Return the denominator (as a numeral AST) of a numeral AST of sort Real.
static Z3_context Z3_mk_interpolation_context(Z3_config a0)
Z3_ast Z3_API Z3_mk_bvand(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Bitwise and.
static Z3_sort Z3_mk_int_sort(Z3_context a0)
static void Z3_fixedpoint_pop(Z3_context a0, Z3_fixedpoint a1)
unsigned Z3_API Z3_get_smtlib_num_assumptions(__in Z3_context c)
Return the number of SMTLIB assumptions parsed by Z3_parse_smtlib_string or Z3_parse_smtlib_file.
static uint Z3_param_descrs_get_kind(Z3_context a0, Z3_param_descrs a1, IntPtr a2)
static Z3_ast Z3_mk_interpolant(Z3_context a0, Z3_ast a1)
static void Z3_solver_assert_and_track(Z3_context a0, Z3_solver a1, Z3_ast a2, Z3_ast a3)
static Z3_ast_vector Z3_fixedpoint_get_assertions(Z3_context a0, Z3_fixedpoint a1)
Z3_ast Z3_API Z3_app_to_ast(__in Z3_context c, __in Z3_app a)
Convert a Z3_app into Z3_ast. This is just type casting.
static uint Z3_get_smtlib_num_sorts(Z3_context a0)
static Z3_func_decl Z3_get_datatype_sort_constructor_accessor(Z3_context a0, Z3_sort a1, uint a2, uint a3)
static Z3_solver Z3_mk_solver(Z3_context a0)
static uint Z3_get_datatype_sort_num_constructors(Z3_context a0, Z3_sort a1)
static void Z3_ast_vector_set(Z3_context a0, Z3_ast_vector a1, uint a2, Z3_ast a3)
void Z3_API Z3_del_context(__in Z3_context c)
Delete the given logical context.
void Z3_API Z3_set_error_handler(__in Z3_context c, __in Z3_error_handler h)
Register a Z3 error handler.
static Z3_ast Z3_mk_array_default(Z3_context a0, Z3_ast a1)
static uint Z3_get_ast_hash(Z3_context a0, Z3_ast a1)
Z3_ast Z3_API Z3_algebraic_sub(__in Z3_context c, __in Z3_ast a, __in Z3_ast b)
Return the value a - b.
static void Z3_assert_cnstr(Z3_context a0, Z3_ast a1)
Z3_bool Z3_API Z3_goal_is_decided_sat(__in Z3_context c, __in Z3_goal g)
Return true if the goal is empty, and it is precise or the product of a under approximation.
static Z3_ast Z3_mk_bvmul_no_underflow(Z3_context a0, Z3_ast a1, Z3_ast a2)
static IntPtr Z3_fixedpoint_get_help(Z3_context a0, Z3_fixedpoint a1)
void Z3_API Z3_param_descrs_dec_ref(__in Z3_context c, __in Z3_param_descrs p)
Decrement the reference counter of the given parameter description set.
Z3_stats Z3_API Z3_fixedpoint_get_statistics(__in Z3_context c, __in Z3_fixedpoint d)
Retrieve statistics information from the last call to Z3_fixedpoint_query.
Z3_ast Z3_API Z3_mk_bvuge(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Unsigned greater than or equal to.
static Z3_ast Z3_simplify(Z3_context a0, Z3_ast a1)
Z3_string Z3_API Z3_simplify_get_help(__in Z3_context c)
Return a string describing all available parameters.
Z3_sort Z3_API Z3_mk_set_sort(__in Z3_context c, __in Z3_sort ty)
Create Set type.
static void Z3_del_model(Z3_context a0, Z3_model a1)
static Z3_ast Z3_mk_false(Z3_context a0)
static uint Z3_get_domain_size(Z3_context a0, Z3_func_decl a1)
static Z3_sort Z3_mk_bool_sort(Z3_context a0)
void Z3_API Z3_solver_set_params(__in Z3_context c, __in Z3_solver s, __in Z3_params p)
Set the given solver using the given parameters.
static void Z3_ast_map_dec_ref(Z3_context a0, Z3_ast_map a1)
static Z3_rcf_num Z3_rcf_mk_rational(Z3_context a0, string a1)
static Z3_ast Z3_get_smtlib_assumption(Z3_context a0, uint a1)
Z3_string Z3_API Z3_get_probe_name(__in Z3_context c, unsigned i)
Return the name of the i probe.
Z3_stats Z3_API Z3_solver_get_statistics(__in Z3_context c, __in Z3_solver s)
Return statistics for the given solver.
void Z3_API Z3_disable_trace(__in Z3_string tag)
Disable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise...
static uint Z3_get_func_decl_id(Z3_context a0, Z3_func_decl a1)
static Z3_ast Z3_mk_bound(Z3_context a0, uint a1, Z3_sort a2)
static int Z3_is_eq_sort(Z3_context a0, Z3_sort a1, Z3_sort a2)
static double Z3_probe_apply(Z3_context a0, Z3_probe a1, Z3_goal a2)
static int Z3_check_interpolant(Z3_context a0, uint a1, [In] Z3_ast[] a2, [In] uint[] a3, [In] Z3_ast[] a4, out IntPtr a5, uint a6, [In] Z3_ast[] a7)
static int Z3_is_eq_ast(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_func_interp_get_else(Z3_context a0, Z3_func_interp a1)
static void Z3_func_interp_inc_ref(Z3_context a0, Z3_func_interp a1)
static Z3_tactic Z3_tactic_when(Z3_context a0, Z3_probe a1, Z3_tactic a2)
static Z3_ast Z3_mk_bvnor(Z3_context a0, Z3_ast a1, Z3_ast a2)
Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c, __in Z3_ast pat, __in Z3_params p, __out Z3_ast_vector *interp, __out Z3_model *model)
Z3_string Z3_API Z3_benchmark_to_smtlib_string(__in Z3_context c, __in Z3_string name, __in Z3_string logic, __in Z3_string status, __in Z3_string attributes, __in unsigned num_assumptions, __in_ecount(num_assumptions) Z3_ast const assumptions[], __in Z3_ast formula)
Convert the given benchmark into SMT-LIB formatted string.
static Z3_ast Z3_mk_unsigned_int64(Z3_context a0, UInt64 a1, Z3_sort a2)
Z3_probe Z3_API Z3_probe_ge(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than or equal to the...
static int Z3_ast_map_contains(Z3_context a0, Z3_ast_map a1, Z3_ast a2)
static int Z3_get_numeral_uint(Z3_context a0, Z3_ast a1, [In, Out] ref uint a2)
static Z3_constructor_list Z3_mk_constructor_list(Z3_context a0, uint a1, [In] Z3_constructor[] a2)
unsigned Z3_API Z3_model_get_num_consts(__in Z3_context c, __in Z3_model m)
Return the number of constants assigned by the given model.
Z3_ast Z3_API Z3_mk_not(__in Z3_context c, __in Z3_ast a)
Create an AST node representing not(a).
static void Z3_query_constructor(Z3_context a0, Z3_constructor a1, uint a2, [In, Out] ref Z3_func_decl a3, [In, Out] ref Z3_func_decl a4, [Out] Z3_func_decl[] a5)
static Z3_probe Z3_probe_not(Z3_context a0, Z3_probe a1)
void Z3_API Z3_get_array_value(__in Z3_context c, __in Z3_model m, __in Z3_ast v, __in unsigned num_entries, __inout_ecount(num_entries) Z3_ast indices[], __inout_ecount(num_entries) Z3_ast values[], __out Z3_ast *else_value)
An array values is represented as a dictionary plus a default (else) value. This function returns the...
Z3_ast Z3_API Z3_mk_bvsge(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed greater than or equal to.
static IntPtr Z3_get_decl_rational_parameter(Z3_context a0, Z3_func_decl a1, uint a2)
static Z3_func_decl Z3_get_model_func_decl(Z3_context a0, Z3_model a1, uint a2)
static IntPtr Z3_get_quantifier_bound_name(Z3_context a0, Z3_ast a1, uint a2)
void Z3_API Z3_del_config(__in Z3_config c)
Delete the given configuration object.
static int Z3_rcf_eq(Z3_context a0, Z3_rcf_num a1, Z3_rcf_num a2)
static int Z3_algebraic_le(Z3_context a0, Z3_ast a1, Z3_ast a2)
static string Z3_params_to_string(Z3_context a0, Z3_params a1)
static Z3_tactic Z3_tactic_fail_if(Z3_context a0, Z3_probe a1)
static Z3_context Z3_mk_context(Z3_config a0)
unsigned Z3_API Z3_get_num_scopes(__in Z3_context c)
Retrieve the current scope level.
static Z3_ast Z3_ast_map_find(Z3_context a0, Z3_ast_map a1, Z3_ast a2)
static void Z3_fixedpoint_inc_ref(Z3_context a0, Z3_fixedpoint a1)
static int Z3_get_symbol_int(Z3_context a0, IntPtr a1)
static void Z3_parse_smtlib_file(Z3_context a0, string a1, uint a2, [In] IntPtr[] a3, [In] Z3_sort[] a4, uint a5, [In] IntPtr[] a6, [In] Z3_func_decl[] a7)
static Z3_ast Z3_mk_bvsgt(Z3_context a0, Z3_ast a1, Z3_ast a2)
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)
Z3_ast Z3_API Z3_mk_repeat(__in Z3_context c, __in unsigned i, __in Z3_ast t1)
Repeat the given bit-vector up length i.
static Z3_probe Z3_probe_ge(Z3_context a0, Z3_probe a1, Z3_probe a2)
static Z3_ast Z3_mk_rotate_right(Z3_context a0, uint a1, Z3_ast a2)
static int Z3_rcf_gt(Z3_context a0, Z3_rcf_num a1, Z3_rcf_num a2)
static Z3_ast Z3_algebraic_div(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_func_decl Z3_model_get_const_decl(Z3_context a0, Z3_model a1, uint a2)
Z3_ast Z3_API Z3_mk_bvadd_no_underflow(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow...
Z3_ast Z3_API Z3_mk_bvnand(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Bitwise nand.
static uint Z3_get_ast_id(Z3_context a0, Z3_ast a1)
static int Z3_solver_check(Z3_context a0, Z3_solver a1)
BEGIN_MLAPI_EXCLUDE Z3_constructor Z3_API Z3_mk_constructor(__in Z3_context c, __in Z3_symbol name, __in Z3_symbol recognizer, __in unsigned num_fields, __in_ecount(num_fields) Z3_symbol const field_names[], __in_ecount(num_fields) Z3_sort_opt const sorts[], __in_ecount(num_fields) unsigned sort_refs[])
Create a constructor.
static Z3_sort Z3_mk_uninterpreted_sort(Z3_context a0, IntPtr a1)
Z3_string Z3_API Z3_get_error_msg(__in Z3_error_code err)
Return a string describing the given error code.
void Z3_API Z3_fixedpoint_dec_ref(__in Z3_context c, __in Z3_fixedpoint d)
Decrement the reference counter of the given fixedpoint context.
static Z3_ast Z3_mk_set_subset(Z3_context a0, Z3_ast a1, Z3_ast a2)
static void Z3_ast_vector_set(Z3_context a0, Z3_ast_vector a1, uint a2, Z3_ast a3)
Z3_bool Z3_API Z3_stats_is_uint(__in Z3_context c, __in Z3_stats s, __in unsigned idx)
Return Z3_TRUE if the given statistical data is a unsigned integer.
Z3_bool Z3_API Z3_algebraic_lt(__in Z3_context c, __in Z3_ast a, __in Z3_ast b)
Return Z3_TRUE if a < b, and Z3_FALSE otherwise.
static Z3_ast Z3_mk_bvxor(Z3_context a0, Z3_ast a1, Z3_ast a2)
Z3_ast Z3_API Z3_mk_div(__in Z3_context c, __in Z3_ast arg1, __in Z3_ast arg2)
Create an AST node representing arg1 div arg2.The arguments must either both have int type or both ha...
Z3_ast Z3_API Z3_mk_bvneg(__in Z3_context c, __in Z3_ast t1)
Standard two's complement unary minus.
Z3_ast Z3_API Z3_sort_to_ast(__in Z3_context c, __in Z3_sort s)
Convert a Z3_sort into Z3_ast. This is just type casting.
static void Z3_ast_map_reset(Z3_context a0, Z3_ast_map a1)
static uint Z3_func_interp_get_num_entries(Z3_context a0, Z3_func_interp a1)
void Z3_API Z3_disable_literal(__in Z3_context c, __in Z3_literals lbls, __in unsigned idx)
Disable label.
static Z3_probe Z3_mk_probe(Z3_context a0, string a1)
Z3_symbol Z3_API Z3_get_label_symbol(__in Z3_context c, __in Z3_literals lbls, __in unsigned idx)
Retrieve label symbol at idx.
Z3_ast Z3_API Z3_mk_unary_minus(__in Z3_context c, __in Z3_ast arg)
Create an AST node representing -arg.The arguments must have int or real type.
static void Z3_pop(Z3_context a0, uint a1)
static Z3_apply_result Z3_tactic_apply_ex(Z3_context a0, Z3_tactic a1, Z3_goal a2, Z3_params a3)
unsigned Z3_API Z3_get_quantifier_weight(__in Z3_context c, __in Z3_ast a)
Obtain weight of quantifier.
Z3_ast Z3_API Z3_algebraic_div(__in Z3_context c, __in Z3_ast a, __in Z3_ast b)
Return the value a / b.
Z3_sort Z3_API Z3_get_sort(__in Z3_context c, __in Z3_ast a)
Return the sort of an AST node.
static uint Z3_get_smtlib_num_decls(Z3_context a0)
static Z3_context Z3_mk_context(Z3_config a0)
static void Z3_push(Z3_context a0)
Z3_ast Z3_API Z3_func_entry_get_arg(__in Z3_context c, __in Z3_func_entry e, __in unsigned i)
Return an argument of a Z3_func_entry object.
static Z3_ast Z3_mk_unary_minus(Z3_context a0, Z3_ast a1)
Z3_bool Z3_API Z3_algebraic_ge(__in Z3_context c, __in Z3_ast a, __in Z3_ast b)
Return Z3_TRUE if a >= b, and Z3_FALSE otherwise.
static Z3_ast Z3_mk_unary_minus(Z3_context a0, Z3_ast a1)
Z3_string Z3_API Z3_model_to_string(__in Z3_context c, __in Z3_model m)
Convert the given model into a string.
void Z3_API Z3_ast_map_inc_ref(__in Z3_context c, __in Z3_ast_map m)
Increment the reference counter of the given AST map.
static Z3_ast Z3_algebraic_mul(Z3_context a0, Z3_ast a1, Z3_ast a2)
static int Z3_is_algebraic_number(Z3_context a0, Z3_ast a1)
Z3_ast Z3_API Z3_mk_rotate_left(__in Z3_context c, __in unsigned i, __in Z3_ast t1)
Rotate bits of t1 to the left i times.
static int Z3_algebraic_eq(Z3_context a0, Z3_ast a1, Z3_ast a2)
static int Z3_check_interpolant(Z3_context a0, uint a1, [In] Z3_ast[] a2, [In] uint[] a3, [In] Z3_ast[] a4, out IntPtr a5, uint a6, [In] Z3_ast[] a7)
static Z3_sort Z3_mk_set_sort(Z3_context a0, Z3_sort a1)
Z3_param_descrs Z3_API Z3_tactic_get_param_descrs(__in Z3_context c, __in Z3_tactic t)
Return the parameter description set for the given tactic object.
static Z3_sort Z3_get_range(Z3_context a0, Z3_func_decl a1)
static Z3_ast Z3_mk_set_member(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_stats Z3_solver_get_statistics(Z3_context a0, Z3_solver a1)
static Z3_ast Z3_mk_const_array(Z3_context a0, Z3_sort a1, Z3_ast a2)
unsigned Z3_API Z3_get_relation_arity(__in Z3_context c, __in Z3_sort s)
Return arity of relation.
static Z3_ast Z3_simplify_ex(Z3_context a0, Z3_ast a1, Z3_params a2)
static Z3_ast Z3_mk_set_del(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_mk_bvmul(Z3_context a0, Z3_ast a1, Z3_ast a2)
static uint Z3_get_search_failure(Z3_context a0)
static Z3_ast Z3_mk_full_set(Z3_context a0, Z3_sort a1)
void Z3_API Z3_func_entry_inc_ref(__in Z3_context c, __in Z3_func_entry e)
Increment the reference counter of the given Z3_func_entry object.
Z3_func_decl Z3_API Z3_get_app_decl(__in Z3_context c, __in Z3_app a)
Return the declaration of a constant or function application.
static string Z3_fixedpoint_get_reason_unknown(Z3_context a0, Z3_fixedpoint a1)
unsigned Z3_API Z3_fixedpoint_get_num_levels(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred)
Query the PDR engine for the maximal levels properties are known about predicate. ...
void Z3_API Z3_solver_reset(__in Z3_context c, __in Z3_solver s)
Remove all assertions from the solver.
static Z3_ast Z3_mk_bvlshr(Z3_context a0, Z3_ast a1, Z3_ast a2)
static IntPtr Z3_ast_vector_to_string(Z3_context a0, Z3_ast_vector a1)
void Z3_API Z3_push(__in Z3_context c)
Create a backtracking point.
Z3_solver Z3_API Z3_mk_solver(__in Z3_context c)
Create a new (incremental) solver. This solver also uses a set of builtin tactics for handling the fi...
static Z3_pattern Z3_mk_pattern(Z3_context a0, uint a1, [In] Z3_ast[] a2)
static Z3_ast Z3_mk_add(Z3_context a0, uint a1, [In] Z3_ast[] a2)
static Z3_ast Z3_fixedpoint_get_answer(Z3_context a0, Z3_fixedpoint a1)
static Z3_ast Z3_mk_bvudiv(Z3_context a0, Z3_ast a1, Z3_ast a2)
static void Z3_fixedpoint_add_fact(Z3_context a0, Z3_fixedpoint a1, Z3_func_decl a2, uint a3, [In] uint[] a4)
static Z3_constructor Z3_mk_constructor(Z3_context a0, IntPtr a1, IntPtr a2, uint a3, [In] IntPtr[] a4, [In] Z3_sort[] a5, [In] uint[] a6)
static void Z3_mk_datatypes(Z3_context a0, uint a1, [In] IntPtr[] a2, [Out] Z3_sort[] a3, [In, Out] Z3_constructor_list[] a4)
static IntPtr Z3_get_error_msg(uint a0)
static int Z3_algebraic_is_pos(Z3_context a0, Z3_ast a1)
static void Z3_pop(Z3_context a0, uint a1)
unsigned Z3_API Z3_goal_size(__in Z3_context c, __in Z3_goal g)
Return the number of formulas in the given goal.
static uint Z3_stats_size(Z3_context a0, Z3_stats a1)
Z3_ast Z3_API Z3_func_interp_get_else(__in Z3_context c, __in Z3_func_interp f)
Return the 'else' value of the given function interpretation.
Z3_probe Z3_API Z3_probe_or(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when p1 or p2 evaluates to true.
void Z3_API Z3_fixedpoint_add_cover(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred, Z3_ast property)
Add property about the predicate pred. Add a property of predicate pred at level. It gets pushed forw...
static uint Z3_get_tuple_sort_num_fields(Z3_context a0, Z3_sort a1)
static uint Z3_get_quantifier_num_patterns(Z3_context a0, Z3_ast a1)
static uint Z3_get_model_func_num_entries(Z3_context a0, Z3_model a1, uint a2)
Z3_ast Z3_API Z3_mk_bvsgt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed greater than.
Z3_parameter_kind Z3_API Z3_get_decl_parameter_kind(__in Z3_context c, __in Z3_func_decl d, unsigned idx)
Return the parameter type associated with a declaration.
static string Z3_get_decl_rational_parameter(Z3_context a0, Z3_func_decl a1, uint a2)
Z3_ast Z3_API Z3_mk_bvnor(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Bitwise nor.
static Z3_model Z3_solver_get_model(Z3_context a0, Z3_solver a1)
static Z3_tactic Z3_tactic_repeat(Z3_context a0, Z3_tactic a1, uint a2)
static void Z3_del_constructor_list(Z3_context a0, Z3_constructor_list a1)
static void Z3_del_context(Z3_context a0)
static Z3_ast Z3_func_entry_get_value(Z3_context a0, Z3_func_entry a1)
static void Z3_params_validate(Z3_context a0, Z3_params a1, Z3_param_descrs a2)
static int Z3_rcf_ge(Z3_context a0, Z3_rcf_num a1, Z3_rcf_num a2)
static IntPtr Z3_context_to_string(Z3_context a0)
static int Z3_check(Z3_context a0)
static void Z3_block_literals(Z3_context a0, Z3_literals a1)
static Z3_ast Z3_func_interp_get_else(Z3_context a0, Z3_func_interp a1)
Z3_ast Z3_API Z3_mk_bv2int(__in Z3_context c, __in Z3_ast t1, Z3_bool is_signed)
Create an integer from the bit-vector argument t1. If is_signed is false, then the bit-vector t1 is t...
static void Z3_goal_assert(Z3_context a0, Z3_goal a1, Z3_ast a2)
unsigned Z3_API Z3_get_num_probes(__in Z3_context c)
Return the number of builtin probes available in Z3.
static Z3_ast Z3_get_algebraic_number_lower(Z3_context a0, Z3_ast a1, uint a2)
static uint Z3_get_symbol_kind(Z3_context a0, IntPtr a1)
Z3_ast Z3_API Z3_mk_set_add(__in Z3_context c, __in Z3_ast set, __in Z3_ast elem)
Add an element to a set.
Z3_ast Z3_API Z3_mk_quantifier_const(__in Z3_context c, Z3_bool is_forall, unsigned weight, unsigned num_bound, __in_ecount(num_bound) Z3_app const bound[], unsigned num_patterns, __in_ecount(num_patterns) Z3_pattern const patterns[], __in Z3_ast body)
Create a universal or existential quantifier using a list of constants that will form the set of boun...
void Z3_API Z3_params_validate(__in Z3_context c, __in Z3_params p, __in Z3_param_descrs d)
Validate the parameter set p against the parameter description set d.
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)
void Z3_API Z3_mk_datatypes(__in Z3_context c, __in unsigned num_sorts, __in_ecount(num_sorts) Z3_symbol const sort_names[], __out_ecount(num_sorts) Z3_sort sorts[], __inout_ecount(num_sorts) Z3_constructor_list constructor_lists[])
Create mutually recursive datatypes.
Z3_symbol Z3_API Z3_get_quantifier_bound_name(__in Z3_context c, __in Z3_ast a, unsigned i)
Return symbol of the i'th bound variable.
static uint Z3_model_get_num_funcs(Z3_context a0, Z3_model a1)
BEGIN_MLAPI_EXCLUDE Z3_string Z3_API Z3_get_smtlib_error(__in Z3_context c)
Retrieve that last error message information generated from parsing.
static string Z3_get_numeral_decimal_string(Z3_context a0, Z3_ast a1, uint a2)
static Z3_ast Z3_mk_full_set(Z3_context a0, Z3_sort a1)
static Z3_ast Z3_mk_int2real(Z3_context a0, Z3_ast a1)
unsigned Z3_API Z3_ast_vector_size(__in Z3_context c, __in Z3_ast_vector v)
Return the size of the given AST vector.
Z3_sort Z3_API Z3_get_domain(__in Z3_context c, __in Z3_func_decl d, __in unsigned i)
Return the sort of the i-th parameter of the given function declaration.
Z3_config Z3_API Z3_mk_config(void)
Create a configuration object for the Z3 context object.
void Z3_API Z3_tactic_dec_ref(__in Z3_context c, __in Z3_tactic g)
Decrement the reference counter of the given tactic.
static IntPtr Z3_get_probe_name(Z3_context a0, uint a1)
Z3_bool Z3_API Z3_goal_is_decided_unsat(__in Z3_context c, __in Z3_goal g)
Return true if the goal contains false, and it is precise or the product of an over approximation...
static IntPtr Z3_tactic_get_help(Z3_context a0, Z3_tactic a1)
static void Z3_assert_cnstr(Z3_context a0, Z3_ast a1)
Z3_bool Z3_API Z3_rcf_lt(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b)
Return Z3_TRUE if a < b.
unsigned Z3_API Z3_get_smtlib_num_formulas(__in Z3_context c)
Return the number of SMTLIB formulas parsed by the last call to Z3_parse_smtlib_string or Z3_parse_sm...
unsigned Z3_API Z3_model_get_num_sorts(__in Z3_context c, __in Z3_model m)
Return the number of uninterpreted sorts that m assigs an interpretation to.
int Z3_API Z3_algebraic_sign(__in Z3_context c, __in Z3_ast a)
Return 1 if a is positive, 0 if a is zero, and -1 if a is negative.
static void Z3_solver_dec_ref(Z3_context a0, Z3_solver a1)
static int Z3_is_algebraic_number(Z3_context a0, Z3_ast a1)
static void Z3_get_array_value(Z3_context a0, Z3_model a1, Z3_ast a2, uint a3, [Out] Z3_ast[] a4, [Out] Z3_ast[] a5, [In, Out] ref Z3_ast a6)
static void Z3_params_dec_ref(Z3_context a0, Z3_params a1)
static int Z3_rcf_neq(Z3_context a0, Z3_rcf_num a1, Z3_rcf_num a2)
static Z3_tactic Z3_tactic_when(Z3_context a0, Z3_probe a1, Z3_tactic a2)
static Z3_ast Z3_mk_not(Z3_context a0, Z3_ast a1)
static Z3_ast Z3_mk_set_difference(Z3_context a0, Z3_ast a1, Z3_ast a2)
static IntPtr Z3_get_label_symbol(Z3_context a0, Z3_literals a1, uint a2)
Z3_ast Z3_API Z3_mk_extract(__in Z3_context c, __in unsigned high, __in unsigned low, __in Z3_ast t1)
Extract the bits high down to low from a bitvector of size m to yield a new bitvector of size n...
static void Z3_func_entry_inc_ref(Z3_context a0, Z3_func_entry a1)
Z3_app Z3_API Z3_to_app(__in Z3_context c, __in Z3_ast a)
Convert an ast into an APP_AST. This is just type casting.
static Z3_ast Z3_algebraic_sub(Z3_context a0, Z3_ast a1, Z3_ast a2)
static void Z3_apply_result_inc_ref(Z3_context a0, Z3_apply_result a1)
static uint Z3_get_decl_parameter_kind(Z3_context a0, Z3_func_decl a1, uint a2)
static Z3_ast Z3_mk_ite(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3)
static Z3_ast Z3_mk_bvnot(Z3_context a0, Z3_ast a1)
Z3_ast Z3_API Z3_mk_distinct(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).The distinct construct is us...
static int Z3_get_finite_domain_sort_size(Z3_context a0, Z3_sort a1, [In, Out] ref UInt64 a2)
static Z3_ast Z3_mk_set_difference(Z3_context a0, Z3_ast a1, Z3_ast a2)
Z3_ast Z3_API Z3_mk_bvxnor(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Bitwise xnor.
Z3_ast Z3_API Z3_mk_bvudiv(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Unsigned division.
Z3_ast Z3_API Z3_mk_or(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create an AST node representing args[0] or ... or args[num_args-1].The array args must have num_args ...
static uint Z3_goal_depth(Z3_context a0, Z3_goal a1)
static void Z3_ast_vector_push(Z3_context a0, Z3_ast_vector a1, Z3_ast a2)
static void Z3_del_config(Z3_config a0)
static void Z3_del_context(Z3_context a0)
static void Z3_probe_dec_ref(Z3_context a0, Z3_probe a1)
static string Z3_solver_get_reason_unknown(Z3_context a0, Z3_solver a1)
Z3_ast Z3_API Z3_mk_exists_const(__in Z3_context c, unsigned weight, unsigned num_bound, __in_ecount(num_bound) Z3_app const bound[], unsigned num_patterns, __in_ecount(num_patterns) Z3_pattern const patterns[], __in Z3_ast body)
Similar to Z3_mk_forall_const.
static IntPtr Z3_solver_to_string(Z3_context a0, Z3_solver a1)
static Z3_config Z3_mk_config()
static void Z3_params_set_symbol(Z3_context a0, Z3_params a1, IntPtr a2, IntPtr a3)
static Z3_ast_vector Z3_fixedpoint_from_file(Z3_context a0, Z3_fixedpoint a1, string a2)
static Z3_ast_map Z3_mk_ast_map(Z3_context a0)
void Z3_API Z3_ast_vector_inc_ref(__in Z3_context c, __in Z3_ast_vector v)
Increment the reference counter of the given AST vector.
static Z3_ast Z3_mk_bvsub(Z3_context a0, Z3_ast a1, Z3_ast a2)
static IntPtr Z3_goal_to_string(Z3_context a0, Z3_goal a1)
Z3_rcf_num Z3_API Z3_rcf_power(__in Z3_context c, __in Z3_rcf_num a, __in unsigned k)
Return the value a^k.
static Z3_ast Z3_mk_quantifier(Z3_context a0, int a1, uint a2, uint a3, [In] Z3_pattern[] a4, uint a5, [In] Z3_sort[] a6, [In] IntPtr[] a7, Z3_ast a8)
static Z3_ast Z3_mk_bvsge(Z3_context a0, Z3_ast a1, Z3_ast a2)
static uint Z3_get_smtlib_num_formulas(Z3_context a0)
void Z3_API Z3_rcf_get_numerator_denominator(__in Z3_context c, __in Z3_rcf_num a, __out Z3_rcf_num *n, __out Z3_rcf_num *d)
Extract the "numerator" and "denominator" of the given RCF numeral. We have that a = n/d...
static Z3_rcf_num Z3_rcf_sub(Z3_context a0, Z3_rcf_num a1, Z3_rcf_num a2)
void Z3_API Z3_interrupt(__in Z3_context c)
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers...
Z3_ast Z3_API Z3_get_numerator(__in Z3_context c, __in Z3_ast a)
Return the numerator (as a numeral AST) of a numeral AST of sort Real.
static Z3_ast Z3_mk_lt(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_func_decl Z3_get_app_decl(Z3_context a0, Z3_app a1)
unsigned Z3_API Z3_func_entry_get_num_args(__in Z3_context c, __in Z3_func_entry e)
Return the number of arguments in a Z3_func_entry object.
Z3_ast Z3_API Z3_mk_set_subset(__in Z3_context c, __in Z3_ast arg1, __in Z3_ast arg2)
Check for subsetness of sets.
Z3_symbol Z3_API Z3_get_sort_name(__in Z3_context c, __in Z3_sort d)
Return the sort name as a symbol.
static Z3_ast Z3_mk_bvsle(Z3_context a0, Z3_ast a1, Z3_ast a2)
static IntPtr Z3_param_descrs_get_name(Z3_context a0, Z3_param_descrs a1, uint a2)
static Z3_ast Z3_mk_set_complement(Z3_context a0, Z3_ast a1)
Z3_param_descrs Z3_API Z3_solver_get_param_descrs(__in Z3_context c, __in Z3_solver s)
Return the parameter description set for the given solver object.
static Z3_ast Z3_mk_store(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3)
Z3_ast Z3_API Z3_get_smtlib_formula(__in Z3_context c, __in unsigned i)
Return the i-th formula parsed by the last call to Z3_parse_smtlib_string or Z3_parse_smtlib_file.
static IntPtr Z3_solver_get_help(Z3_context a0, Z3_solver a1)
static uint Z3_func_interp_get_arity(Z3_context a0, Z3_func_interp a1)
static double Z3_get_decl_double_parameter(Z3_context a0, Z3_func_decl a1, uint a2)
static Z3_ast_map Z3_mk_ast_map(Z3_context a0)
Z3_ast Z3_API Z3_mk_xor(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Create an AST node representing t1 xor t2.
static uint Z3_get_ast_kind(Z3_context a0, Z3_ast a1)
static Z3_ast Z3_mk_ext_rotate_right(Z3_context a0, Z3_ast a1, Z3_ast a2)
Z3_string Z3_API Z3_context_to_string(__in Z3_context c)
Convert the given logical context into a string.
static void Z3_tactic_dec_ref(Z3_context a0, Z3_tactic a1)
static string Z3_interpolation_profile(Z3_context a0)
static int Z3_algebraic_eval(Z3_context a0, Z3_ast a1, uint a2, [In] Z3_ast[] a3)
void Z3_API Z3_reset_memory(void)
Reset all allocated resources.
Z3_tactic Z3_API Z3_tactic_when(__in Z3_context c, __in Z3_probe p, __in Z3_tactic t)
Return a tactic that applies t to a given goal is the probe p evaluates to true. If p evaluates to fa...
static Z3_ast Z3_mk_set_member(Z3_context a0, Z3_ast a1, Z3_ast a2)
Z3_rcf_num Z3_API Z3_rcf_neg(__in Z3_context c, __in Z3_rcf_num a)
Return the value -a.
static Z3_ast Z3_substitute(Z3_context a0, Z3_ast a1, uint a2, [In] Z3_ast[] a3, [In] Z3_ast[] a4)
static Z3_ast Z3_pattern_to_ast(Z3_context a0, Z3_pattern a1)
static void Z3_close_log()
Z3_ast Z3_API Z3_ast_vector_get(__in Z3_context c, __in Z3_ast_vector v, __in unsigned i)
Return the AST at position i in the AST vector v.
static Z3_func_decl Z3_mk_func_decl(Z3_context a0, IntPtr a1, uint a2, [In] Z3_sort[] a3, Z3_sort a4)
static Z3_ast Z3_mk_rem(Z3_context a0, Z3_ast a1, Z3_ast a2)
static int Z3_get_numeral_int(Z3_context a0, Z3_ast a1, [In, Out] ref int a2)
static int Z3_algebraic_ge(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_func_decl Z3_get_datatype_sort_recognizer(Z3_context a0, Z3_sort a1, uint a2)
static Z3_ast_vector Z3_fixedpoint_get_assertions(Z3_context a0, Z3_fixedpoint a1)
static Z3_ast Z3_mk_ge(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast_vector Z3_mk_ast_vector(Z3_context a0)
static Z3_tactic Z3_tactic_fail_if_not_decided(Z3_context a0)
Z3_probe Z3_API Z3_probe_le(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than or equal to the va...
static Z3_rcf_num Z3_rcf_power(Z3_context a0, Z3_rcf_num a1, uint a2)
static Z3_solver Z3_mk_simple_solver(Z3_context a0)
static Z3_fixedpoint Z3_mk_fixedpoint(Z3_context a0)
static Z3_ast Z3_mk_label(Z3_context a0, IntPtr a1, int a2, Z3_ast a3)
static Z3_ast Z3_get_pattern(Z3_context a0, Z3_pattern a1, uint a2)
static int Z3_eval_func_decl(Z3_context a0, Z3_model a1, Z3_func_decl a2, [In, Out] ref Z3_ast a3)
static uint Z3_get_error_code(Z3_context a0)
static Z3_param_descrs Z3_tactic_get_param_descrs(Z3_context a0, Z3_tactic a1)
Z3_sort Z3_API Z3_mk_list_sort(__in Z3_context c, __in Z3_symbol name, __in Z3_sort elem_sort, __out Z3_func_decl *nil_decl, __out Z3_func_decl *is_nil_decl, __out Z3_func_decl *cons_decl, __out Z3_func_decl *is_cons_decl, __out Z3_func_decl *head_decl, __out Z3_func_decl *tail_decl)
Create a list sort.
static Z3_ast Z3_solver_get_proof(Z3_context a0, Z3_solver a1)
static Z3_ast Z3_mk_bvlshr(Z3_context a0, Z3_ast a1, Z3_ast a2)
void Z3_API Z3_func_interp_dec_ref(__in Z3_context c, __in Z3_func_interp f)
Decrement the reference counter of the given Z3_func_interp object.
unsigned Z3_API Z3_get_index_value(__in Z3_context c, __in Z3_ast a)
Return index of de-Brujin bound variable.
static Z3_sort Z3_get_quantifier_bound_sort(Z3_context a0, Z3_ast a1, uint a2)
Z3_ast Z3_API Z3_get_algebraic_number_upper(Z3_context c, Z3_ast a, unsigned precision)
Return a upper bound for the given real algebraic number. The interval isolating the number is smalle...
static Z3_sort Z3_get_relation_column(Z3_context a0, Z3_sort a1, uint a2)
static Z3_ast_vector Z3_ast_vector_translate(Z3_context a0, Z3_ast_vector a1, Z3_context a2)
Z3_ast Z3_API Z3_mk_forall(__in Z3_context c, __in unsigned weight, __in unsigned num_patterns, __in_ecount(num_patterns) Z3_pattern const patterns[], __in unsigned num_decls, __in_ecount(num_decls) Z3_sort const sorts[], __in_ecount(num_decls) Z3_symbol const decl_names[], __in Z3_ast body)
Create a forall formula. It takes an expression body that contains bound variables of the same sorts ...
static int Z3_algebraic_gt(Z3_context a0, Z3_ast a1, Z3_ast a2)
Z3_solver Z3_API Z3_mk_solver_from_tactic(__in Z3_context c, __in Z3_tactic t)
Create a new solver that is implemented using the given tactic. The solver supports the commands Z3_s...
static Z3_rcf_num Z3_rcf_mk_e(Z3_context a0)
static uint Z3_param_descrs_get_kind(Z3_context a0, Z3_param_descrs a1, IntPtr a2)
static void Z3_solver_set_params(Z3_context a0, Z3_solver a1, Z3_params a2)
static void Z3_fixedpoint_set_params(Z3_context a0, Z3_fixedpoint a1, Z3_params a2)
static void Z3_solver_set_params(Z3_context a0, Z3_solver a1, Z3_params a2)
Z3_func_decl Z3_API Z3_get_decl_func_decl_parameter(__in Z3_context c, __in Z3_func_decl d, unsigned idx)
Return the expresson value associated with an expression parameter.
static Z3_sort Z3_get_smtlib_sort(Z3_context a0, uint a1)
static Z3_pattern Z3_mk_pattern(Z3_context a0, uint a1, [In] Z3_ast[] a2)
static uint Z3_get_decl_num_parameters(Z3_context a0, Z3_func_decl a1)
Z3_ast Z3_API Z3_mk_bvxor(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Bitwise exclusive-or.
Z3_string Z3_API Z3_ast_vector_to_string(__in Z3_context c, __in Z3_ast_vector v)
Convert AST vector into a string.
Z3_ast_vector Z3_API Z3_solver_get_assertions(__in Z3_context c, __in Z3_solver s)
Return the set of asserted formulas as a goal object.
static void Z3_params_set_uint(Z3_context a0, Z3_params a1, IntPtr a2, uint a3)
static void Z3_params_set_symbol(Z3_context a0, Z3_params a1, IntPtr a2, IntPtr a3)
static int Z3_is_eq_ast(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_mk_bvult(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_tactic Z3_tactic_skip(Z3_context a0)
Z3_string Z3_API Z3_get_numeral_string(__in Z3_context c, __in Z3_ast a)
Return numeral value, as a string of a numeric constant term.
Z3_func_decl Z3_API Z3_mk_fresh_func_decl(__in Z3_context c, __in Z3_string prefix, __in unsigned domain_size, __in_ecount(domain_size) Z3_sort const domain[], __in Z3_sort range)
Declare a fresh constant or function.
static Z3_rcf_num Z3_rcf_mk_small_int(Z3_context a0, int a1)
static Z3_ast Z3_mk_fresh_const(Z3_context a0, string a1, Z3_sort a2)
static Z3_ast Z3_mk_bvnot(Z3_context a0, Z3_ast a1)
static IntPtr Z3_model_to_string(Z3_context a0, Z3_model a1)
static Z3_sort Z3_get_decl_sort_parameter(Z3_context a0, Z3_func_decl a1, uint a2)
static Z3_ast Z3_algebraic_power(Z3_context a0, Z3_ast a1, uint a2)
static uint Z3_get_num_tactics(Z3_context a0)
static void Z3_func_interp_dec_ref(Z3_context a0, Z3_func_interp a1)
static void Z3_close_log()
static void Z3_set_error_handler(Z3_context a0, Z3_error_handler a1)
static uint Z3_get_num_scopes(Z3_context a0)
static Z3_ast Z3_mk_bvsub_no_underflow(Z3_context a0, Z3_ast a1, Z3_ast a2, int a3)
static void Z3_get_array_value(Z3_context a0, Z3_model a1, Z3_ast a2, uint a3, [Out] Z3_ast[] a4, [Out] Z3_ast[] a5, [In, Out] ref Z3_ast a6)
static void Z3_func_interp_inc_ref(Z3_context a0, Z3_func_interp a1)
static Z3_ast Z3_func_decl_to_ast(Z3_context a0, Z3_func_decl a1)
static int Z3_rcf_le(Z3_context a0, Z3_rcf_num a1, Z3_rcf_num a2)
static Z3_ast Z3_mk_bvurem(Z3_context a0, Z3_ast a1, Z3_ast a2)
static uint Z3_get_bv_sort_size(Z3_context a0, Z3_sort a1)
static void Z3_goal_inc_ref(Z3_context a0, Z3_goal a1)
static Z3_ast Z3_mk_bvsdiv(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast_vector Z3_solver_get_unsat_core(Z3_context a0, Z3_solver a1)
static Z3_ast Z3_mk_ext_rotate_right(Z3_context a0, Z3_ast a1, Z3_ast a2)
unsigned Z3_API Z3_get_func_decl_id(__in Z3_context c, Z3_func_decl f)
Return a unique identifier for f.
void Z3_API Z3_fixedpoint_register_relation(__in Z3_context c, __in Z3_fixedpoint d, __in Z3_func_decl f)
Register relation as Fixedpoint defined. Fixedpoint defined relations have least-fixedpoint semantics...
static string Z3_context_to_string(Z3_context a0)
Z3_ast Z3_API Z3_func_decl_to_ast(__in Z3_context c, __in Z3_func_decl f)
Convert a Z3_func_decl into Z3_ast. This is just type casting.
static Z3_literals Z3_get_relevant_literals(Z3_context a0)
static Z3_rcf_num Z3_rcf_mul(Z3_context a0, Z3_rcf_num a1, Z3_rcf_num a2)
static Z3_probe Z3_probe_and(Z3_context a0, Z3_probe a1, Z3_probe a2)
Z3_bool Z3_API Z3_get_numeral_uint(__in Z3_context c, __in Z3_ast v, __out unsigned *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine unsigned int...
static int Z3_algebraic_neq(Z3_context a0, Z3_ast a1, Z3_ast a2)
Z3_probe Z3_API Z3_probe_lt(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than the value returned...
static Z3_ast Z3_algebraic_div(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_mk_distinct(Z3_context a0, uint a1, [In] Z3_ast[] a2)
static Z3_probe Z3_probe_gt(Z3_context a0, Z3_probe a1, Z3_probe a2)
static void Z3_append_log(string a0)
static void Z3_ast_map_inc_ref(Z3_context a0, Z3_ast_map a1)
static int Z3_eval_decl(Z3_context a0, Z3_model a1, Z3_func_decl a2, uint a3, [In] Z3_ast[] a4, [In, Out] ref Z3_ast a5)
static void Z3_del_model(Z3_context a0, Z3_model a1)
static void Z3_goal_assert(Z3_context a0, Z3_goal a1, Z3_ast a2)
static uint Z3_get_smtlib_num_formulas(Z3_context a0)
static IntPtr Z3_get_quantifier_bound_name(Z3_context a0, Z3_ast a1, uint a2)
static Z3_probe Z3_probe_or(Z3_context a0, Z3_probe a1, Z3_probe a2)
static void Z3_enable_trace(string a0)
Z3_lbool Z3_API Z3_check_assumptions(__in Z3_context c, __in unsigned num_assumptions, __in_ecount(num_assumptions) Z3_ast const assumptions[], __out Z3_model *m, __out Z3_ast *proof, __inout unsigned *core_size, __inout_ecount(num_assumptions) Z3_ast core[])
Check whether the given logical context and optional assumptions is consistent or not...
static Z3_fixedpoint Z3_mk_fixedpoint(Z3_context a0)
static Z3_ast Z3_mk_bvsmod(Z3_context a0, Z3_ast a1, Z3_ast a2)
static void Z3_solver_push(Z3_context a0, Z3_solver a1)
static Z3_ast Z3_mk_bvadd_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2, int a3)
Z3_fixedpoint Z3_API Z3_mk_fixedpoint(__in Z3_context c)
Create a new fixedpoint context.
Z3_ast Z3_API Z3_fixedpoint_get_cover_delta(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred)
unsigned Z3_API Z3_goal_depth(__in Z3_context c, __in Z3_goal g)
Return the depth of the given goal. It tracks how many transformations were applied to it...
Z3_ast Z3_API Z3_mk_int64(__in Z3_context c, __in __int64 v, __in Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
static Z3_ast Z3_mk_rotate_right(Z3_context a0, uint a1, Z3_ast a2)
static int Z3_goal_is_decided_sat(Z3_context a0, Z3_goal a1)
static Z3_ast Z3_get_model_func_entry_value(Z3_context a0, Z3_model a1, uint a2, uint a3)
Z3_ast Z3_API Z3_mk_sign_ext(__in Z3_context c, __in unsigned i, __in Z3_ast t1)
Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i, where m is the size of the given bit-vector.
static void Z3_write_interpolation_problem(Z3_context a0, uint a1, [In] Z3_ast[] a2, [In] uint[] a3, string a4, uint a5, [In] Z3_ast[] a6)
static Z3_params Z3_mk_params(Z3_context a0)
static void Z3_reset_memory()
static Z3_ast Z3_mk_bvsle(Z3_context a0, Z3_ast a1, Z3_ast a2)
void Z3_API Z3_params_set_bool(__in Z3_context c, __in Z3_params p, __in Z3_symbol k, __in Z3_bool v)
Add a Boolean parameter k with value v to the parameter set p.
static Z3_ast Z3_algebraic_add(Z3_context a0, Z3_ast a1, Z3_ast a2)
static uint Z3_get_model_func_num_entries(Z3_context a0, Z3_model a1, uint a2)
static Z3_ast Z3_mk_int2real(Z3_context a0, Z3_ast a1)
static Z3_ast Z3_get_denominator(Z3_context a0, Z3_ast a1)
Z3_bool Z3_API Z3_algebraic_is_zero(__in Z3_context c, __in Z3_ast a)
Return the Z3_TRUE if a is zero, and Z3_FALSE otherwise.
Z3_string Z3_API Z3_fixedpoint_get_reason_unknown(__in Z3_context c, __in Z3_fixedpoint d)
Retrieve a string that describes the last status returned by Z3_fixedpoint_query. ...
The exception base class for error reporting from Z3
static void Z3_set_logic(Z3_context a0, string a1)
static Z3_ast Z3_simplify(Z3_context a0, Z3_ast a1)
static Z3_ast Z3_mk_rotate_left(Z3_context a0, uint a1, Z3_ast a2)
static int Z3_algebraic_sign(Z3_context a0, Z3_ast a1)
static Z3_probe Z3_probe_gt(Z3_context a0, Z3_probe a1, Z3_probe a2)
static Z3_ast_vector Z3_fixedpoint_from_string(Z3_context a0, Z3_fixedpoint a1, string a2)
static Z3_tactic Z3_tactic_fail(Z3_context a0)
static Z3_ast Z3_get_model_func_entry_arg(Z3_context a0, Z3_model a1, uint a2, uint a3, uint a4)
static Z3_func_decl Z3_get_decl_func_decl_parameter(Z3_context a0, Z3_func_decl a1, uint a2)
Z3_string Z3_API Z3_get_symbol_string(__in Z3_context c, __in Z3_symbol s)
Return the symbol name.
static Z3_ast Z3_mk_bvult(Z3_context a0, Z3_ast a1, Z3_ast a2)
void Z3_API Z3_probe_dec_ref(__in Z3_context c, __in Z3_probe p)
Decrement the reference counter of the given probe.
Z3_ast Z3_API Z3_mk_eq(__in Z3_context c, __in Z3_ast l, __in Z3_ast r)
Create an AST node representing l = r.
Z3_bool Z3_API Z3_rcf_gt(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b)
Return Z3_TRUE if a > b.
Z3_ast Z3_API Z3_mk_unsigned_int64(__in Z3_context c, __in unsigned __int64 v, __in Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
Z3_ast Z3_API Z3_algebraic_add(__in Z3_context c, __in Z3_ast a, __in Z3_ast b)
Return the value a + b.
static Z3_ast Z3_mk_quantifier(Z3_context a0, int a1, uint a2, uint a3, [In] Z3_pattern[] a4, uint a5, [In] Z3_sort[] a6, [In] IntPtr[] a7, Z3_ast a8)
static Z3_ast Z3_func_decl_to_ast(Z3_context a0, Z3_func_decl a1)
Z3_bool Z3_API Z3_is_app(__in Z3_context c, __in Z3_ast a)
static uint Z3_ast_vector_size(Z3_context a0, Z3_ast_vector a1)
static uint Z3_fixedpoint_get_num_levels(Z3_context a0, Z3_fixedpoint a1, Z3_func_decl a2)
static Z3_literals Z3_get_relevant_literals(Z3_context a0)
static uint Z3_get_smtlib_num_sorts(Z3_context a0)
static Z3_ast Z3_mk_bvugt(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_get_context_assignment(Z3_context a0)
Z3_ast Z3_API Z3_mk_store(__in Z3_context c, __in Z3_ast a, __in Z3_ast i, __in Z3_ast v)
Array update.
static Z3_ast Z3_ast_vector_get(Z3_context a0, Z3_ast_vector a1, uint a2)
static void Z3_fixedpoint_dec_ref(Z3_context a0, Z3_fixedpoint a1)
unsigned Z3_API Z3_get_bv_sort_size(__in Z3_context c, __in Z3_sort t)
Return the size of the given bit-vector sort.
static uint Z3_get_datatype_sort_num_constructors(Z3_context a0, Z3_sort a1)
Z3_tactic Z3_API Z3_tactic_par_or(__in Z3_context c, __in unsigned num, __in_ecount(num) Z3_tactic const ts[])
Return a tactic that applies the given tactics in parallel.
Z3_string Z3_API Z3_rcf_num_to_decimal_string(__in Z3_context c, __in Z3_rcf_num a, __in unsigned prec)
Convert the RCF numeral into a string in decimal notation.
static Z3_ast Z3_mk_lt(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_mk_bvxnor(Z3_context a0, Z3_ast a1, Z3_ast a2)
void Z3_API Z3_ast_map_reset(__in Z3_context c, __in Z3_ast_map m)
Remove all keys from the given map.
static void Z3_apply_result_dec_ref(Z3_context a0, Z3_apply_result a1)
static Z3_rcf_num Z3_rcf_inv(Z3_context a0, Z3_rcf_num a1)
void Z3_API Z3_del_model(__in Z3_context c, __in Z3_model m)
Delete a model object.
static void Z3_enable_trace(string a0)
Z3_sort Z3_API Z3_get_quantifier_bound_sort(__in Z3_context c, __in Z3_ast a, unsigned i)
Return sort of the i'th bound variable.
static Z3_ast_vector Z3_mk_ast_vector(Z3_context a0)
Z3_ast Z3_API Z3_get_model_func_entry_arg(__in Z3_context c, __in Z3_model m, __in unsigned i, __in unsigned j, __in unsigned k)
Return the k-th argument of the j-th entry of the i-th function interpretation in the given model...
static int Z3_rcf_ge(Z3_context a0, Z3_rcf_num a1, Z3_rcf_num a2)
void Z3_API Z3_global_param_reset_all(void)
Restore the value of all global (and module) parameters. This command will not affect already created...
Z3_bool Z3_API Z3_model_has_interp(__in Z3_context c, __in Z3_model m, __in Z3_func_decl a)
Test if there exists an interpretation (i.e., assignment) for a in the model m.
static IntPtr Z3_solver_get_reason_unknown(Z3_context a0, Z3_solver a1)
Z3_ast Z3_API Z3_mk_bvashr(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Arithmetic shift right.
static int Z3_get_numeral_uint64(Z3_context a0, Z3_ast a1, [In, Out] ref UInt64 a2)
static Z3_rcf_num Z3_rcf_mk_infinitesimal(Z3_context a0)
static Z3_func_decl Z3_model_get_func_decl(Z3_context a0, Z3_model a1, uint a2)
static void Z3_model_inc_ref(Z3_context a0, Z3_model a1)
void Z3_API Z3_fixedpoint_set_predicate_representation(__in Z3_context c, __in Z3_fixedpoint d, __in Z3_func_decl f, __in unsigned num_relations, __in_ecount(num_relations) Z3_symbol const relation_kinds[])
Configure the predicate representation.
static string Z3_pattern_to_string(Z3_context a0, Z3_pattern a1)
Z3_sort_kind Z3_API Z3_get_sort_kind(__in Z3_context c, __in Z3_sort t)
Return the sort kind (e.g., array, tuple, int, bool, etc).
static Z3_sort Z3_get_range(Z3_context a0, Z3_func_decl a1)
static IntPtr Z3_pattern_to_string(Z3_context a0, Z3_pattern a1)
static IntPtr Z3_get_decl_name(Z3_context a0, Z3_func_decl a1)
static void Z3_params_validate(Z3_context a0, Z3_params a1, Z3_param_descrs a2)
static Z3_solver Z3_mk_solver_for_logic(Z3_context a0, IntPtr a1)
static Z3_ast Z3_mk_int(Z3_context a0, int a1, Z3_sort a2)
static uint Z3_get_quantifier_weight(Z3_context a0, Z3_ast a1)
void Z3_API Z3_ast_map_dec_ref(__in Z3_context c, __in Z3_ast_map m)
Decrement the reference counter of the given AST map.
static int Z3_goal_inconsistent(Z3_context a0, Z3_goal a1)
static Z3_ast Z3_mk_set_union(Z3_context a0, uint a1, [In] Z3_ast[] a2)
void Z3_error_handler(Z3_context c, Z3_error_code e)
Z3 custom error handler (See Z3_set_error_handler).
static Z3_sort Z3_mk_finite_domain_sort(Z3_context a0, IntPtr a1, UInt64 a2)
static void Z3_update_param_value(Z3_context a0, string a1, string a2)
static Z3_ast Z3_update_term(Z3_context a0, Z3_ast a1, uint a2, [In] Z3_ast[] a3)
static Z3_ast Z3_mk_quantifier_const(Z3_context a0, int a1, uint a2, uint a3, [In] Z3_app[] a4, uint a5, [In] Z3_pattern[] a6, Z3_ast a7)
static Z3_ast Z3_mk_bvurem(Z3_context a0, Z3_ast a1, Z3_ast a2)
static void Z3_goal_reset(Z3_context a0, Z3_goal a1)
static int Z3_solver_check_assumptions(Z3_context a0, Z3_solver a1, uint a2, [In] Z3_ast[] a3)
static void Z3_fixedpoint_register_relation(Z3_context a0, Z3_fixedpoint a1, Z3_func_decl a2)
static Z3_ast Z3_get_pattern(Z3_context a0, Z3_pattern a1, uint a2)
static void Z3_params_set_double(Z3_context a0, Z3_params a1, IntPtr a2, double a3)
static void Z3_fixedpoint_add_cover(Z3_context a0, Z3_fixedpoint a1, int a2, Z3_func_decl a3, Z3_ast a4)
Z3_rcf_num Z3_API Z3_rcf_mul(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b)
Return the value a * b.
static uint Z3_get_pattern_num_terms(Z3_context a0, Z3_pattern a1)
void Z3_API Z3_ast_vector_dec_ref(__in Z3_context c, __in Z3_ast_vector v)
Decrement the reference counter of the given AST vector.
static Z3_ast Z3_mk_set_add(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_goal Z3_apply_result_get_subgoal(Z3_context a0, Z3_apply_result a1, uint a2)
Z3_ast Z3_API Z3_mk_app(__in Z3_context c, __in Z3_func_decl d, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create a constant or function application.
static void Z3_fixedpoint_update_rule(Z3_context a0, Z3_fixedpoint a1, Z3_ast a2, IntPtr a3)
static Z3_goal Z3_mk_goal(Z3_context a0, int a1, int a2, int a3)
Z3_func_decl Z3_API Z3_mk_func_decl(__in Z3_context c, __in Z3_symbol s, __in unsigned domain_size, __in_ecount(domain_size) Z3_sort const domain[], __in Z3_sort range)
Declare a constant or function.
static IntPtr Z3_get_tactic_name(Z3_context a0, uint a1)
static string Z3_param_descrs_to_string(Z3_context a0, Z3_param_descrs a1)
static Z3_ast Z3_mk_bound(Z3_context a0, uint a1, Z3_sort a2)
static int Z3_is_array_value(Z3_context a0, Z3_model a1, Z3_ast a2, [In, Out] ref uint a3)
static void Z3_solver_inc_ref(Z3_context a0, Z3_solver a1)
static string Z3_solver_get_help(Z3_context a0, Z3_solver a1)
static void Z3_del_constructor(Z3_context a0, Z3_constructor a1)
static int Z3_stats_is_uint(Z3_context a0, Z3_stats a1, uint a2)
static Z3_ast_vector Z3_algebraic_roots(Z3_context a0, Z3_ast a1, uint a2, [In] Z3_ast[] a3)
static Z3_rcf_num Z3_rcf_mk_infinitesimal(Z3_context a0)
Z3_sort Z3_API Z3_get_relation_column(__in Z3_context c, __in Z3_sort s, unsigned col)
Return sort at i'th column of relation sort.
static Z3_tactic Z3_tactic_repeat(Z3_context a0, Z3_tactic a1, uint a2)
Z3_ast Z3_API Z3_get_algebraic_number_lower(__in Z3_context c, __in Z3_ast a, __in unsigned precision)
Return a lower bound for the given real algebraic number. The interval isolating the number is smalle...
Z3_ast Z3_API Z3_mk_is_int(__in Z3_context c, __in Z3_ast t1)
Check if a real number is an integer.
static string Z3_get_symbol_string(Z3_context a0, IntPtr a1)
static void Z3_solver_push(Z3_context a0, Z3_solver a1)
static Z3_ast Z3_mk_int2bv(Z3_context a0, uint a1, Z3_ast a2)
void Z3_API Z3_stats_dec_ref(__in Z3_context c, __in Z3_stats s)
Decrement the reference counter of the given statistics object.
Z3_rcf_num Z3_API Z3_rcf_mk_e(__in Z3_context c)
Return e (Euler's constant)
Z3_ast Z3_API Z3_ast_map_find(__in Z3_context c, __in Z3_ast_map m, __in Z3_ast k)
Return the value associated with the key k.
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)
void Z3_API Z3_update_param_value(__in Z3_context c, __in Z3_string param_id, __in Z3_string param_value)
Set a value of a context parameter.
static Z3_ast Z3_mk_bvsub_no_underflow(Z3_context a0, Z3_ast a1, Z3_ast a2, int a3)
static Z3_ast Z3_mk_set_union(Z3_context a0, uint a1, [In] Z3_ast[] a2)
static Z3_ast Z3_mk_rotate_left(Z3_context a0, uint a1, Z3_ast a2)
static Z3_goal Z3_apply_result_get_subgoal(Z3_context a0, Z3_apply_result a1, uint a2)
static uint Z3_ast_map_size(Z3_context a0, Z3_ast_map a1)
static int Z3_is_array_value(Z3_context a0, Z3_model a1, Z3_ast a2, [In, Out] ref uint a3)
static int Z3_stats_is_uint(Z3_context a0, Z3_stats a1, uint a2)
static Z3_ast Z3_mk_rem(Z3_context a0, Z3_ast a1, Z3_ast a2)
Z3_ast Z3_API Z3_mk_quantifier(__in Z3_context c, __in Z3_bool is_forall, __in unsigned weight, __in unsigned num_patterns, __in_ecount(num_patterns) Z3_pattern const patterns[], __in unsigned num_decls, __in_ecount(num_decls) Z3_sort const sorts[], __in_ecount(num_decls) Z3_symbol const decl_names[], __in Z3_ast body)
Create a quantifier - universal or existential, with pattern hints. See the documentation for Z3_mk_f...
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)
Z3_ast Z3_API Z3_mk_concat(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Concatenate the given bit-vectors.
static int Z3_global_param_get(string a0, out IntPtr a1)
static Z3_rcf_num Z3_rcf_add(Z3_context a0, Z3_rcf_num a1, Z3_rcf_num a2)
static void Z3_solver_reset(Z3_context a0, Z3_solver a1)
static Z3_ast Z3_mk_array_default(Z3_context a0, Z3_ast a1)
int Z3_API Z3_read_interpolation_problem(__in Z3_context ctx, __out unsigned *num, __out Z3_ast *cnsts[], __out unsigned *parents[], __in Z3_string filename, __out Z3_string_ptr error, __out unsigned *num_theory, __out Z3_ast *theory[])
Read an interpolation problem from file.
static Z3_ast Z3_mk_bvnand(Z3_context a0, Z3_ast a1, Z3_ast a2)
static uint Z3_get_pattern_num_terms(Z3_context a0, Z3_pattern a1)
static Z3_context Z3_mk_interpolation_context(Z3_config a0)
static IntPtr Z3_fixedpoint_get_reason_unknown(Z3_context a0, Z3_fixedpoint a1)
static Z3_ast Z3_func_entry_get_value(Z3_context a0, Z3_func_entry a1)
static int Z3_is_app(Z3_context a0, Z3_ast a1)
static Z3_ast Z3_mk_real2int(Z3_context a0, Z3_ast a1)
void Z3_API Z3_solver_pop(__in Z3_context c, __in Z3_solver s, unsigned n)
Backtrack n backtracking points.
Z3_tactic Z3_API Z3_tactic_fail_if_not_decided(__in Z3_context c)
Return a tactic that fails if the goal is not trivially satisfiable (i.e., empty) or trivially unsati...
static Z3_goal Z3_mk_goal(Z3_context a0, int a1, int a2, int a3)
static Z3_ast_vector Z3_algebraic_roots(Z3_context a0, Z3_ast a1, uint a2, [In] Z3_ast[] a3)
static int Z3_rcf_neq(Z3_context a0, Z3_rcf_num a1, Z3_rcf_num a2)
unsigned Z3_API Z3_func_interp_get_arity(__in Z3_context c, __in Z3_func_interp f)
Return the arity (number of arguments) of the given function interpretation.
static int Z3_algebraic_is_value(Z3_context a0, Z3_ast a1)
static Z3_param_descrs Z3_solver_get_param_descrs(Z3_context a0, Z3_solver a1)
Z3_params Z3_API Z3_mk_params(__in Z3_context c)
Create a Z3 (empty) parameter set. Starting at Z3 4.0, parameter sets are used to configure many comp...
static IntPtr Z3_apply_result_to_string(Z3_context a0, Z3_apply_result a1)
static IntPtr Z3_param_descrs_to_string(Z3_context a0, Z3_param_descrs a1)
Z3_ast Z3_API Z3_algebraic_mul(__in Z3_context c, __in Z3_ast a, __in Z3_ast b)
Return the value a * b.
static double Z3_probe_apply(Z3_context a0, Z3_probe a1, Z3_goal a2)
static Z3_ast Z3_mk_exists(Z3_context a0, uint a1, uint a2, [In] Z3_pattern[] a3, uint a4, [In] Z3_sort[] a5, [In] IntPtr[] a6, Z3_ast a7)
static Z3_ast Z3_mk_map(Z3_context a0, Z3_func_decl a1, uint a2, [In] Z3_ast[] a3)
static int Z3_is_app(Z3_context a0, Z3_ast a1)
static Z3_ast Z3_mk_const(Z3_context a0, IntPtr a1, Z3_sort a2)
void Z3_API Z3_ast_map_insert(__in Z3_context c, __in Z3_ast_map m, __in Z3_ast k, __in Z3_ast v)
Store/Replace a new key, value pair in the given map.
Z3_ast_vector Z3_API Z3_ast_vector_translate(__in Z3_context s, __in Z3_ast_vector v, __in Z3_context t)
Translate the AST vector v from context s into an AST vector in context t.
Z3_ast Z3_API Z3_get_literal(__in Z3_context c, __in Z3_literals lbls, __in unsigned idx)
Retrieve literal expression at idx.
static void Z3_fixedpoint_assert(Z3_context a0, Z3_fixedpoint a1, Z3_ast a2)
static uint Z3_fixedpoint_get_num_levels(Z3_context a0, Z3_fixedpoint a1, Z3_func_decl a2)
Z3_tactic Z3_API Z3_tactic_or_else(__in Z3_context c, __in Z3_tactic t1, __in Z3_tactic t2)
Return a tactic that first applies t1 to a given goal, if it fails then returns the result of t2 appl...
static Z3_sort Z3_get_domain(Z3_context a0, Z3_func_decl a1, uint a2)
static Z3_func_decl Z3_get_datatype_sort_constructor(Z3_context a0, Z3_sort a1, uint a2)
static Z3_ast Z3_mk_int64(Z3_context a0, Int64 a1, Z3_sort a2)
void Z3_API Z3_ast_vector_set(__in Z3_context c, __in Z3_ast_vector v, __in unsigned i, __in Z3_ast a)
Update position i of the AST vector v with the AST a.
Z3_error_code Z3_API Z3_get_error_code(__in Z3_context c)
Return the error code for the last API call.
Z3_ast Z3_API Z3_get_decl_ast_parameter(__in Z3_context c, __in Z3_func_decl d, unsigned idx)
Return the expresson value associated with an expression parameter.
static uint Z3_goal_num_exprs(Z3_context a0, Z3_goal a1)
static Z3_ast Z3_mk_numeral(Z3_context a0, string a1, Z3_sort a2)
static void Z3_global_param_reset_all()
static string Z3_sort_to_string(Z3_context a0, Z3_sort a1)
static uint Z3_get_sort_kind(Z3_context a0, Z3_sort a1)
unsigned Z3_API Z3_get_tuple_sort_num_fields(__in Z3_context c, __in Z3_sort t)
Return the number of fields of the given tuple sort.
Z3_ast Z3_API Z3_mk_array_default(__in Z3_context c, __in Z3_ast array)
Access the array default value. Produces the default range value, for arrays that can be represented ...
Z3_symbol Z3_API Z3_get_decl_symbol_parameter(__in Z3_context c, __in Z3_func_decl d, unsigned idx)
Return the double value associated with an double parameter.
static int Z3_check(Z3_context a0)
static uint Z3_get_quantifier_num_patterns(Z3_context a0, Z3_ast a1)
static void Z3_ast_map_insert(Z3_context a0, Z3_ast_map a1, Z3_ast a2, Z3_ast a3)
unsigned Z3_API Z3_get_datatype_sort_num_constructors(__in Z3_context c, __in Z3_sort t)
Return number of constructors for datatype.
void Z3_API Z3_fixedpoint_set_params(__in Z3_context c, __in Z3_fixedpoint f, __in Z3_params p)
Set parameters on fixedpoint context.
static void Z3_toggle_warning_messages(int a0)
static void Z3_solver_assert(Z3_context a0, Z3_solver a1, Z3_ast a2)
static int Z3_get_symbol_int(Z3_context a0, IntPtr a1)
static int Z3_get_numeral_int64(Z3_context a0, Z3_ast a1, [In, Out] ref Int64 a2)
Z3_symbol Z3_API Z3_mk_int_symbol(__in Z3_context c, __in int i)
Create a Z3 symbol using an integer.
static IntPtr Z3_func_decl_to_string(Z3_context a0, Z3_func_decl a1)
static Z3_ast Z3_mk_set_intersect(Z3_context a0, uint a1, [In] Z3_ast[] a2)
static Z3_ast Z3_mk_const(Z3_context a0, IntPtr a1, Z3_sort a2)
Z3_bool Z3_API Z3_is_quantifier_forall(__in Z3_context c, __in Z3_ast a)
Determine if quantifier is universal.
Z3_literals Z3_API Z3_get_relevant_labels(__in Z3_context c)
Retrieve the set of labels that were relevant in the context of the current satisfied context...
unsigned Z3_API Z3_get_quantifier_num_no_patterns(__in Z3_context c, __in Z3_ast a)
Return number of no_patterns used in quantifier.
static int Z3_eval_decl(Z3_context a0, Z3_model a1, Z3_func_decl a2, uint a3, [In] Z3_ast[] a4, [In, Out] ref Z3_ast a5)
static string Z3_fixedpoint_to_string(Z3_context a0, Z3_fixedpoint a1, uint a2, [In] Z3_ast[] a3)
Z3_lbool Z3_API Z3_solver_check_assumptions(__in Z3_context c, __in Z3_solver s, __in unsigned num_assumptions, __in_ecount(num_assumptions) Z3_ast const assumptions[])
Check whether the assertions in the given solver and optional assumptions are consistent or not...
static uint Z3_model_get_num_consts(Z3_context a0, Z3_model a1)
static Z3_tactic Z3_mk_tactic(Z3_context a0, string a1)
Z3_sort Z3_API Z3_mk_finite_domain_sort(__in Z3_context c, __in Z3_symbol name, __in unsigned __int64 size)
Create a named finite domain sort.
static Z3_ast Z3_get_quantifier_no_pattern_ast(Z3_context a0, Z3_ast a1, uint a2)
Z3_bool Z3_API Z3_is_numeral_ast(__in Z3_context c, __in Z3_ast a)
static Z3_ast Z3_mk_bvneg(Z3_context a0, Z3_ast a1)
Z3_constructor_list Z3_API Z3_mk_constructor_list(__in Z3_context c, __in unsigned num_constructors, __in_ecount(num_constructors) Z3_constructor const constructors[])
Create list of constructors.
static Z3_ast Z3_mk_set_complement(Z3_context a0, Z3_ast a1)
static Z3_rcf_num Z3_rcf_mk_rational(Z3_context a0, string a1)
Z3_ast Z3_API Z3_mk_add(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create an AST node representing args[0] + ... + args[num_args-1].The array args must have num_args el...
static Z3_tactic Z3_tactic_using_params(Z3_context a0, Z3_tactic a1, Z3_params a2)
static Z3_ast Z3_mk_eq(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_func_decl Z3_get_tuple_sort_mk_decl(Z3_context a0, Z3_sort a1)
Z3_ast Z3_API Z3_get_app_arg(__in Z3_context c, __in Z3_app a, __in unsigned i)
Return the i-th argument of the given application.
static IntPtr Z3_param_descrs_get_name(Z3_context a0, Z3_param_descrs a1, uint a2)
static Z3_ast Z3_mk_bvredor(Z3_context a0, Z3_ast a1)
static Z3_ast Z3_func_entry_get_arg(Z3_context a0, Z3_func_entry a1, uint a2)
void Z3_API Z3_set_param_value(__in Z3_config c, __in Z3_string param_id, __in Z3_string param_value)
Set a configuration parameter.
static Z3_ast Z3_sort_to_ast(Z3_context a0, Z3_sort a1)
static int Z3_algebraic_eval(Z3_context a0, Z3_ast a1, uint a2, [In] Z3_ast[] a3)
static Z3_app Z3_to_app(Z3_context a0, Z3_ast a1)
static Z3_ast Z3_get_algebraic_number_lower(Z3_context a0, Z3_ast a1, uint a2)
static uint Z3_get_smtlib_num_assumptions(Z3_context a0)
static Z3_ast Z3_algebraic_power(Z3_context a0, Z3_ast a1, uint a2)
Z3_probe Z3_API Z3_mk_probe(__in Z3_context c, __in Z3_string name)
Return a probe associated with the given name. The complete list of probes may be obtained using the ...
static Z3_ast_vector Z3_get_interpolant(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_params a3)
static Z3_param_descrs Z3_tactic_get_param_descrs(Z3_context a0, Z3_tactic a1)
static int Z3_is_eq_func_decl(Z3_context a0, Z3_func_decl a1, Z3_func_decl a2)
Z3_sort Z3_API Z3_model_get_sort(__in Z3_context c, __in Z3_model m, __in unsigned i)
Return a uninterpreted sort that m assigns an interpretation.
static Z3_ast Z3_mk_bvshl(Z3_context a0, Z3_ast a1, Z3_ast a2)
Z3_ast Z3_API Z3_mk_rem(__in Z3_context c, __in Z3_ast arg1, __in Z3_ast arg2)
Create an AST node representing arg1 rem arg2.The arguments must have int type.
int Z3_API Z3_algebraic_eval(__in Z3_context c, __in Z3_ast p, __in unsigned n, __in Z3_ast a[])
Given a multivariate polynomial p(x_0, ..., x_{n-1}), return the sign of p(a[0], ..., a[n-1]).
Z3_bool Z3_API Z3_is_array_value(__in Z3_context c, __in Z3_model m, __in Z3_ast v, __out unsigned *num_entries)
Determine whether the term encodes an array value. A term encodes an array value if it is a nested se...
Z3_bool Z3_API Z3_get_numeral_rational_int64(__in Z3_context c, __in Z3_ast v, __out __int64 *num, __out __int64 *den)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit as a rational number as mach...
void Z3_API Z3_rcf_del(__in Z3_context c, __in Z3_rcf_num a)
Delete a RCF numeral created using the RCF API.
Z3_probe Z3_API Z3_probe_and(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when p1 and p2 evaluates to true.
static void Z3_persist_ast(Z3_context a0, Z3_ast a1, uint a2)
static void Z3_params_set_bool(Z3_context a0, Z3_params a1, IntPtr a2, int a3)
static Z3_ast_vector Z3_ast_vector_translate(Z3_context a0, Z3_ast_vector a1, Z3_context a2)
static Z3_func_decl Z3_get_datatype_sort_recognizer(Z3_context a0, Z3_sort a1, uint a2)
static Z3_ast Z3_mk_concat(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_probe Z3_mk_probe(Z3_context a0, string a1)
Z3_bool Z3_API Z3_get_numeral_int64(__in Z3_context c, __in Z3_ast v, __out __int64 *i)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine __int64 int...
Z3_ast Z3_API Z3_mk_bvlshr(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Logical shift right.
static void Z3_goal_dec_ref(Z3_context a0, Z3_goal a1)
static uint Z3_get_smtlib_num_decls(Z3_context a0)
void Z3_API Z3_tactic_inc_ref(__in Z3_context c, __in Z3_tactic t)
Increment the reference counter of the given tactic.
static Z3_tactic Z3_tactic_using_params(Z3_context a0, Z3_tactic a1, Z3_params a2)
static Z3_ast_vector Z3_fixedpoint_get_rules(Z3_context a0, Z3_fixedpoint a1)
static Z3_ast Z3_mk_forall(Z3_context a0, uint a1, uint a2, [In] Z3_pattern[] a3, uint a4, [In] Z3_sort[] a5, [In] IntPtr[] a6, Z3_ast a7)
static Z3_func_decl Z3_get_app_decl(Z3_context a0, Z3_app a1)
static int Z3_eval(Z3_context a0, Z3_model a1, Z3_ast a2, [In, Out] ref Z3_ast a3)
Z3_bool Z3_API Z3_algebraic_is_neg(__in Z3_context c, __in Z3_ast a)
Return the Z3_TRUE if a is negative, and Z3_FALSE otherwise.
static Z3_solver Z3_mk_solver_for_logic(Z3_context a0, IntPtr a1)
Z3_ast Z3_API Z3_mk_const_array(__in Z3_context c, __in Z3_sort domain, __in Z3_ast v)
Create the constant array.
Z3_ast Z3_API Z3_mk_interpolant(__in Z3_context c, __in Z3_ast a)
Create an AST node marking a formula position for interpolation.
Z3_bool Z3_API Z3_is_eq_func_decl(__in Z3_context c, __in Z3_func_decl f1, Z3_func_decl f2)
compare terms.
Z3_ast Z3_API Z3_mk_le(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Create less than or equal to.
static void Z3_params_set_bool(Z3_context a0, Z3_params a1, IntPtr a2, int a3)
static Z3_ast Z3_app_to_ast(Z3_context a0, Z3_app a1)
static Z3_ast Z3_mk_quantifier_ex(Z3_context a0, int a1, uint a2, IntPtr a3, IntPtr a4, uint a5, [In] Z3_pattern[] a6, uint a7, [In] Z3_ast[] a8, uint a9, [In] Z3_sort[] a10, [In] IntPtr[] a11, Z3_ast a12)
static Z3_ast Z3_fixedpoint_get_cover_delta(Z3_context a0, Z3_fixedpoint a1, int a2, Z3_func_decl a3)
Z3_param_descrs Z3_API Z3_fixedpoint_get_param_descrs(__in Z3_context c, __in Z3_fixedpoint f)
Return the parameter description set for the given fixedpoint object.
static Z3_ast Z3_algebraic_add(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast_vector Z3_fixedpoint_from_string(Z3_context a0, Z3_fixedpoint a1, string a2)
static Z3_func_decl Z3_to_func_decl(Z3_context a0, Z3_ast a1)
static int Z3_is_numeral_ast(Z3_context a0, Z3_ast a1)
Z3_ast Z3_API Z3_mk_label(__in Z3_context c, __in Z3_symbol s, Z3_bool is_pos, Z3_ast f)
Create a labeled formula.
static uint Z3_ast_vector_size(Z3_context a0, Z3_ast_vector a1)
static Z3_param_descrs Z3_fixedpoint_get_param_descrs(Z3_context a0, Z3_fixedpoint a1)
double Z3_API Z3_probe_apply(__in Z3_context c, __in Z3_probe p, __in Z3_goal g)
Execute the probe over the goal. The probe always produce a double value. "Boolean" probes return 0...
Z3_ast Z3_API Z3_mk_set_difference(__in Z3_context c, __in Z3_ast arg1, __in Z3_ast arg2)
Take the set difference between two sets.
static void Z3_soft_check_cancel(Z3_context a0)
Z3_lbool Z3_API Z3_get_bool_value(__in Z3_context c, __in Z3_ast a)
Return Z3_L_TRUE if a is true, Z3_L_FALSE if it is false, and Z3_L_UNDEF otherwise.
Z3_ast Z3_API Z3_simplify_ex(__in Z3_context c, __in Z3_ast a, __in Z3_params p)
Interface to simplifier.
static Z3_ast Z3_mk_div(Z3_context a0, Z3_ast a1, Z3_ast a2)
unsigned Z3_API Z3_get_domain_size(__in Z3_context c, __in Z3_func_decl d)
Return the number of parameters of the given declaration.
static Z3_ast_vector Z3_ast_map_keys(Z3_context a0, Z3_ast_map a1)
static int Z3_get_numeral_uint(Z3_context a0, Z3_ast a1, [In, Out] ref uint a2)
static Z3_ast Z3_solver_get_proof(Z3_context a0, Z3_solver a1)
Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(__in Z3_context c)
Return the parameter description set for the simplify procedure.
Z3_ast Z3_API Z3_algebraic_root(__in Z3_context c, __in Z3_ast a, __in unsigned k)
Return the a^(1/k)
Z3_sort Z3_API Z3_get_smtlib_sort(__in Z3_context c, __in unsigned i)
Return the i-th sort parsed by the last call to Z3_parse_smtlib_string or Z3_parse_smtlib_file.
static int Z3_algebraic_sign(Z3_context a0, Z3_ast a1)
static void Z3_set_param_value(Z3_config a0, string a1, string a2)
unsigned Z3_API Z3_apply_result_get_num_subgoals(__in Z3_context c, __in Z3_apply_result r)
Return the number of subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
Z3_literals Z3_API Z3_get_relevant_literals(__in Z3_context c)
Retrieve the set of literals that satisfy the current context.
static Z3_sort Z3_mk_bool_sort(Z3_context a0)
static void Z3_probe_inc_ref(Z3_context a0, Z3_probe a1)
static Z3_ast Z3_mk_bvule(Z3_context a0, Z3_ast a1, Z3_ast a2)
static IntPtr Z3_statistics_to_string(Z3_context a0)
static double Z3_stats_get_double_value(Z3_context a0, Z3_stats a1, uint a2)
static IntPtr Z3_params_to_string(Z3_context a0, Z3_params a1)
static uint Z3_get_arity(Z3_context a0, Z3_func_decl a1)
static uint Z3_param_descrs_size(Z3_context a0, Z3_param_descrs a1)
static Z3_ast Z3_get_smtlib_assumption(Z3_context a0, uint a1)
static Z3_ast Z3_parse_smtlib2_file(Z3_context a0, string a1, uint a2, [In] IntPtr[] a3, [In] Z3_sort[] a4, uint a5, [In] IntPtr[] a6, [In] Z3_func_decl[] a7)
static IntPtr Z3_benchmark_to_smtlib_string(Z3_context a0, string a1, string a2, string a3, string a4, uint a5, [In] Z3_ast[] a6, Z3_ast a7)
static string Z3_ast_vector_to_string(Z3_context a0, Z3_ast_vector a1)
static Z3_rcf_num Z3_rcf_mul(Z3_context a0, Z3_rcf_num a1, Z3_rcf_num a2)
static void Z3_global_param_set(string a0, string a1)
static Z3_ast_vector Z3_polynomial_subresultants(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_ast a3)
Z3_ast Z3_API Z3_mk_set_member(__in Z3_context c, __in Z3_ast elem, __in Z3_ast set)
Check for set membership.
Z3_ast Z3_API Z3_mk_bvredand(__in Z3_context c, __in Z3_ast t1)
Take conjunction of bits in vector, return vector of length 1.
Z3_string Z3_API Z3_rcf_num_to_string(__in Z3_context c, __in Z3_rcf_num a, __in Z3_bool compact, __in Z3_bool html)
Convert the RCF numeral into a string.
static Z3_ast Z3_get_quantifier_body(Z3_context a0, Z3_ast a1)
static string Z3_model_to_string(Z3_context a0, Z3_model a1)
static Z3_ast Z3_get_model_func_else(Z3_context a0, Z3_model a1, uint a2)
Z3_ast Z3_API Z3_mk_rotate_right(__in Z3_context c, __in unsigned i, __in Z3_ast t1)
Rotate bits of t1 to the right i times.
static Z3_ast Z3_mk_extract(Z3_context a0, uint a1, uint a2, Z3_ast a3)
void Z3_API Z3_assert_cnstr(__in Z3_context c, __in Z3_ast a)
Assert a constraint into the logical context.
static Z3_tactic Z3_tactic_skip(Z3_context a0)
static Z3_ast_vector Z3_solver_get_unsat_core(Z3_context a0, Z3_solver a1)
static void Z3_params_inc_ref(Z3_context a0, Z3_params a1)
static Z3_param_descrs Z3_simplify_get_param_descrs(Z3_context a0)
unsigned Z3_API Z3_stats_get_uint_value(__in Z3_context c, __in Z3_stats s, __in unsigned idx)
Return the unsigned value of the given statistical data.
static Z3_rcf_num Z3_rcf_sub(Z3_context a0, Z3_rcf_num a1, Z3_rcf_num a2)
void Z3_API Z3_ast_vector_resize(__in Z3_context c, __in Z3_ast_vector v, __in unsigned n)
Resize the AST vector v.
Z3_ast_vector Z3_API Z3_mk_ast_vector(__in Z3_context c)
Return an empty AST vector.
Z3_bool Z3_API Z3_is_eq_sort(__in Z3_context c, __in Z3_sort s1, __in Z3_sort s2)
compare sorts.
static uint Z3_stats_get_uint_value(Z3_context a0, Z3_stats a1, uint a2)
static Z3_func_decl Z3_mk_injective_function(Z3_context a0, IntPtr a1, uint a2, [In] Z3_sort[] a3, Z3_sort a4)
Z3_ast Z3_API Z3_mk_full_set(__in Z3_context c, __in Z3_sort domain)
Create the full set.
static Z3_ast Z3_mk_bvsub_no_overflow(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_ast Z3_mk_power(Z3_context a0, Z3_ast a1, Z3_ast a2)
Z3_goal Z3_API Z3_mk_goal(__in Z3_context c, __in Z3_bool models, __in Z3_bool unsat_cores, __in Z3_bool proofs)
Create a goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or trans...
static Z3_ast Z3_get_decl_ast_parameter(Z3_context a0, Z3_func_decl a1, uint a2)
static Z3_literals Z3_get_guessed_literals(Z3_context a0)
static Z3_func_entry Z3_func_interp_get_entry(Z3_context a0, Z3_func_interp a1, uint a2)
static Z3_func_decl Z3_get_as_array_func_decl(Z3_context a0, Z3_ast a1)
Z3_ast Z3_API Z3_fixedpoint_get_answer(__in Z3_context c, __in Z3_fixedpoint d)
Retrieve a formula that encodes satisfying answers to the query.
static void Z3_params_dec_ref(Z3_context a0, Z3_params a1)
static uint Z3_solver_get_num_scopes(Z3_context a0, Z3_solver a1)
static Z3_ast Z3_mk_bvor(Z3_context a0, Z3_ast a1, Z3_ast a2)
static Z3_func_decl Z3_get_datatype_sort_constructor_accessor(Z3_context a0, Z3_sort a1, uint a2, uint a3)
static Z3_ast Z3_mk_bvxor(Z3_context a0, Z3_ast a1, Z3_ast a2)
Z3_func_decl Z3_API Z3_to_func_decl(__in Z3_context c, __in Z3_ast a)
Convert an AST into a FUNC_DECL_AST. This is just type casting.
static void Z3_fixedpoint_push(Z3_context a0, Z3_fixedpoint a1)
static Z3_model Z3_apply_result_convert_model(Z3_context a0, Z3_apply_result a1, uint a2, Z3_model a3)
static Z3_ast Z3_model_get_const_interp(Z3_context a0, Z3_model a1, Z3_func_decl a2)
static void Z3_set_param_value(Z3_config a0, string a1, string a2)
Z3_ast Z3_API Z3_mk_real(__in Z3_context c, __in int num, __in int den)
Create a real from a fraction.
static Z3_apply_result Z3_tactic_apply(Z3_context a0, Z3_tactic a1, Z3_goal a2)
Z3_rcf_num Z3_API Z3_rcf_inv(__in Z3_context c, __in Z3_rcf_num a)
Return the value 1/a.
Z3_string Z3_API Z3_solver_get_reason_unknown(__in Z3_context c, __in Z3_solver s)
Return a brief justification for an "unknown" result (i.e., Z3_L_UNDEF) for the commands Z3_solver_ch...
static IntPtr Z3_get_sort_name(Z3_context a0, Z3_sort a1)
unsigned Z3_API Z3_get_quantifier_num_bound(__in Z3_context c, __in Z3_ast a)
Return number of bound variables of quantifier.
static int Z3_algebraic_is_neg(Z3_context a0, Z3_ast a1)
static int Z3_is_numeral_ast(Z3_context a0, Z3_ast a1)
static Z3_probe Z3_probe_lt(Z3_context a0, Z3_probe a1, Z3_probe a2)
static Z3_ast Z3_mk_map(Z3_context a0, Z3_func_decl a1, uint a2, [In] Z3_ast[] a3)
Z3_rcf_num Z3_API Z3_rcf_div(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b)
Return the value a / b.
Z3_ast Z3_API Z3_mk_empty_set(__in Z3_context c, __in Z3_sort domain)
Create the empty set.
static Z3_sort Z3_mk_enumeration_sort(Z3_context a0, IntPtr a1, uint a2, [In] IntPtr[] a3, [Out] Z3_func_decl[] a4, [Out] Z3_func_decl[] a5)