1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6     api_quant.cpp
7 
8 Abstract:
9     API for quantifiers
10 
11 Author:
12 
13     Leonardo de Moura (leonardo) 2012-02-29.
14 
15 Revision History:
16 
17 --*/
18 #include "api/z3.h"
19 #include "api/api_log_macros.h"
20 #include "api/api_context.h"
21 #include "api/api_util.h"
22 #include "parsers/util/pattern_validation.h"
23 #include "ast/expr_abstract.h"
24 
25 extern "C" {
26 
Z3_mk_quantifier(Z3_context c,bool is_forall,unsigned weight,unsigned num_patterns,Z3_pattern const patterns[],unsigned num_decls,Z3_sort const sorts[],Z3_symbol const decl_names[],Z3_ast body)27     Z3_ast Z3_API Z3_mk_quantifier(
28         Z3_context c,
29         bool is_forall,
30         unsigned weight,
31         unsigned num_patterns, Z3_pattern const patterns[],
32         unsigned num_decls, Z3_sort const sorts[],
33         Z3_symbol const decl_names[],
34         Z3_ast body)
35     {
36         return Z3_mk_quantifier_ex(
37             c,
38             is_forall,
39             weight,
40             of_symbol(symbol::null),
41             of_symbol(symbol::null),
42             num_patterns, patterns,
43             0, nullptr,
44             num_decls, sorts,
45             decl_names,
46             body
47             );
48 
49     }
50 
mk_quantifier_ex_core(Z3_context c,bool is_forall,unsigned weight,Z3_symbol quantifier_id,Z3_symbol skolem_id,unsigned num_patterns,Z3_pattern const patterns[],unsigned num_no_patterns,Z3_ast const no_patterns[],unsigned num_decls,Z3_sort const sorts[],Z3_symbol const decl_names[],Z3_ast body)51     Z3_ast mk_quantifier_ex_core(
52         Z3_context c,
53         bool is_forall,
54         unsigned weight,
55         Z3_symbol quantifier_id,
56         Z3_symbol skolem_id,
57         unsigned num_patterns, Z3_pattern const patterns[],
58         unsigned num_no_patterns, Z3_ast const no_patterns[],
59         unsigned num_decls, Z3_sort const sorts[],
60         Z3_symbol const decl_names[],
61         Z3_ast body) {
62         Z3_TRY;
63         RESET_ERROR_CODE();
64         if (!mk_c(c)->m().is_bool(to_expr(body))) {
65             SET_ERROR_CODE(Z3_SORT_ERROR, nullptr);
66             return nullptr;
67         }
68         if (num_patterns > 0 && num_no_patterns > 0) {
69             SET_ERROR_CODE(Z3_INVALID_USAGE, nullptr);
70             return nullptr;
71         }
72         expr * const* ps = reinterpret_cast<expr * const*>(patterns);
73         expr * const* no_ps = reinterpret_cast<expr * const*>(no_patterns);
74         symbol qid = to_symbol(quantifier_id);
75         pattern_validator v(mk_c(c)->m());
76         for (unsigned i = 0; i < num_patterns; i++) {
77             if (!v(num_decls, ps[i], 0, 0)) {
78                 SET_ERROR_CODE(Z3_INVALID_PATTERN, nullptr);
79                 return nullptr;
80             }
81         }
82         sort* const* ts = reinterpret_cast<sort * const*>(sorts);
83         svector<symbol> names;
84         for (unsigned i = 0; i < num_decls; ++i) {
85             names.push_back(to_symbol(decl_names[i]));
86         }
87         expr_ref result(mk_c(c)->m());
88         if (num_decls > 0) {
89             result = mk_c(c)->m().mk_quantifier(
90                 is_forall ? forall_k : exists_k,
91                 names.size(), ts, names.data(), to_expr(body),
92                 weight,
93                 qid,
94                 to_symbol(skolem_id),
95                 num_patterns, ps,
96                 num_no_patterns, no_ps
97                 );
98         }
99         else {
100             result = to_expr(body);
101         }
102         mk_c(c)->save_ast_trail(result.get());
103         return of_ast(result.get());
104         Z3_CATCH_RETURN(nullptr);
105     }
106 
Z3_mk_quantifier_ex(Z3_context c,bool is_forall,unsigned weight,Z3_symbol quantifier_id,Z3_symbol skolem_id,unsigned num_patterns,Z3_pattern const patterns[],unsigned num_no_patterns,Z3_ast const no_patterns[],unsigned num_decls,Z3_sort const sorts[],Z3_symbol const decl_names[],Z3_ast body)107     Z3_ast Z3_API Z3_mk_quantifier_ex(
108         Z3_context c,
109         bool is_forall,
110         unsigned weight,
111         Z3_symbol quantifier_id,
112         Z3_symbol skolem_id,
113         unsigned num_patterns, Z3_pattern const patterns[],
114         unsigned num_no_patterns, Z3_ast const no_patterns[],
115         unsigned num_decls, Z3_sort const sorts[],
116         Z3_symbol const decl_names[],
117         Z3_ast body)
118     {
119         LOG_Z3_mk_quantifier_ex(c, is_forall, weight, quantifier_id, skolem_id, num_patterns, patterns,
120                                 num_no_patterns, no_patterns, num_decls, sorts, decl_names, body);
121         Z3_ast r = mk_quantifier_ex_core(c, is_forall, weight, quantifier_id, skolem_id, num_patterns, patterns,
122                                          num_no_patterns, no_patterns, num_decls, sorts, decl_names, body);
123         RETURN_Z3(r);
124     }
125 
Z3_mk_forall(Z3_context c,unsigned weight,unsigned num_patterns,Z3_pattern const patterns[],unsigned num_decls,Z3_sort const types[],Z3_symbol const decl_names[],Z3_ast body)126     Z3_ast Z3_API Z3_mk_forall(Z3_context c,
127                                unsigned weight,
128                                unsigned num_patterns, Z3_pattern const patterns[],
129                                unsigned num_decls, Z3_sort const types[],
130                                Z3_symbol const decl_names[],
131                                Z3_ast body) {
132         return Z3_mk_quantifier(c, true, weight, num_patterns, patterns, num_decls, types, decl_names, body);
133     }
134 
Z3_mk_exists(Z3_context c,unsigned weight,unsigned num_patterns,Z3_pattern const patterns[],unsigned num_decls,Z3_sort const types[],Z3_symbol const decl_names[],Z3_ast body)135     Z3_ast Z3_API Z3_mk_exists(Z3_context c,
136                                unsigned weight,
137                                unsigned num_patterns, Z3_pattern const patterns[],
138                                unsigned num_decls, Z3_sort const types[],
139                                Z3_symbol const decl_names[],
140                                Z3_ast body) {
141         return Z3_mk_quantifier(c, false, weight, num_patterns, patterns, num_decls, types, decl_names, body);
142     }
143 
Z3_mk_lambda(Z3_context c,unsigned num_decls,Z3_sort const types[],Z3_symbol const decl_names[],Z3_ast body)144     Z3_ast Z3_API Z3_mk_lambda(Z3_context c,
145                                unsigned num_decls, Z3_sort const types[],
146                                Z3_symbol const decl_names[],
147                                Z3_ast body) {
148 
149         Z3_TRY;
150         LOG_Z3_mk_lambda(c, num_decls, types, decl_names, body);
151         RESET_ERROR_CODE();
152         expr_ref result(mk_c(c)->m());
153         if (num_decls == 0) {
154             SET_ERROR_CODE(Z3_INVALID_USAGE, nullptr);
155             RETURN_Z3(nullptr);
156         }
157 
158         sort* const* ts = reinterpret_cast<sort * const*>(types);
159         svector<symbol> names;
160         for (unsigned i = 0; i < num_decls; ++i) {
161             names.push_back(to_symbol(decl_names[i]));
162         }
163         result = mk_c(c)->m().mk_lambda(names.size(), ts, names.data(), to_expr(body));
164         mk_c(c)->save_ast_trail(result.get());
165         RETURN_Z3(of_ast(result.get()));
166         Z3_CATCH_RETURN(nullptr);
167     }
168 
Z3_mk_lambda_const(Z3_context c,unsigned num_decls,Z3_app const vars[],Z3_ast body)169     Z3_ast Z3_API Z3_mk_lambda_const(Z3_context c,
170                                      unsigned num_decls, Z3_app const vars[],
171                                      Z3_ast body) {
172 
173         Z3_TRY;
174         LOG_Z3_mk_lambda_const(c, num_decls, vars, body);
175         RESET_ERROR_CODE();
176         if (num_decls == 0) {
177             SET_ERROR_CODE(Z3_INVALID_USAGE, nullptr);
178             RETURN_Z3(nullptr);
179         }
180 
181         svector<symbol>  _names;
182         ptr_vector<sort> _vars;
183         ptr_vector<expr> _args;
184         for (unsigned i = 0; i < num_decls; ++i) {
185             app* a = to_app(vars[i]);
186             _names.push_back(to_app(a)->get_decl()->get_name());
187             _args.push_back(a);
188             _vars.push_back(a->get_sort());
189         }
190         expr_ref result(mk_c(c)->m());
191         expr_abstract(mk_c(c)->m(), 0, num_decls, _args.data(), to_expr(body), result);
192 
193         result = mk_c(c)->m().mk_lambda(_vars.size(), _vars.data(), _names.data(), result);
194         mk_c(c)->save_ast_trail(result.get());
195         RETURN_Z3(of_ast(result.get()));
196         Z3_CATCH_RETURN(nullptr);
197     }
198 
199 
Z3_mk_quantifier_const_ex(Z3_context c,bool is_forall,unsigned weight,Z3_symbol quantifier_id,Z3_symbol skolem_id,unsigned num_bound,Z3_app const bound[],unsigned num_patterns,Z3_pattern const patterns[],unsigned num_no_patterns,Z3_ast const no_patterns[],Z3_ast body)200     Z3_ast Z3_API Z3_mk_quantifier_const_ex(Z3_context c,
201                                             bool is_forall,
202                                             unsigned weight,
203                                             Z3_symbol quantifier_id,
204                                             Z3_symbol skolem_id,
205                                             unsigned num_bound,
206                                             Z3_app const bound[],
207                                             unsigned num_patterns,
208                                             Z3_pattern const patterns[],
209                                             unsigned num_no_patterns,
210                                             Z3_ast const no_patterns[],
211                                             Z3_ast body) {
212         Z3_TRY;
213         LOG_Z3_mk_quantifier_const_ex(c, is_forall, weight, quantifier_id, skolem_id, num_bound, bound, num_patterns, patterns,
214                                       num_no_patterns, no_patterns, body);
215         RESET_ERROR_CODE();
216         svector<Z3_symbol> names;
217         svector<Z3_sort> types;
218         ptr_vector<expr> bound_asts;
219         if (num_patterns > 0 && num_no_patterns > 0) {
220             SET_ERROR_CODE(Z3_INVALID_USAGE, nullptr);
221             RETURN_Z3(nullptr);
222         }
223         if (num_bound == 0) {
224             SET_ERROR_CODE(Z3_INVALID_USAGE, "number of bound variables is 0");
225             RETURN_Z3(nullptr);
226         }
227         for (unsigned i = 0; i < num_bound; ++i) {
228             app* a = to_app(bound[i]);
229             if (a->get_kind() != AST_APP) {
230                 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
231                 RETURN_Z3(nullptr);
232             }
233             symbol s(to_app(a)->get_decl()->get_name());
234             names.push_back(of_symbol(s));
235             types.push_back(of_sort(a->get_sort()));
236             bound_asts.push_back(a);
237             if (a->get_family_id() != null_family_id || a->get_num_args() != 0) {
238                 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
239                 RETURN_Z3(nullptr);
240             }
241         }
242         // Abstract patterns
243         svector<Z3_pattern> _patterns;
244         expr_ref_vector pinned(mk_c(c)->m());
245         for (unsigned i = 0; i < num_patterns; ++i) {
246             expr_ref result(mk_c(c)->m());
247             app* pat = to_pattern(patterns[i]);
248             SASSERT(mk_c(c)->m().is_pattern(pat));
249             expr_abstract(mk_c(c)->m(), 0, num_bound, bound_asts.data(), pat, result);
250             SASSERT(result.get()->get_kind() == AST_APP);
251             pinned.push_back(result.get());
252             SASSERT(mk_c(c)->m().is_pattern(result.get()));
253             _patterns.push_back(of_pattern(result.get()));
254         }
255         svector<Z3_ast> _no_patterns;
256         for (unsigned i = 0; i < num_no_patterns; ++i) {
257             expr_ref result(mk_c(c)->m());
258             if (!is_app(to_expr(no_patterns[i]))) {
259                 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
260                 RETURN_Z3(nullptr);
261             }
262             app* pat = to_app(to_expr(no_patterns[i]));
263             expr_abstract(mk_c(c)->m(), 0, num_bound, bound_asts.data(), pat, result);
264             SASSERT(result.get()->get_kind() == AST_APP);
265             pinned.push_back(result.get());
266             _no_patterns.push_back(of_ast(result.get()));
267         }
268         expr_ref abs_body(mk_c(c)->m());
269         expr_abstract(mk_c(c)->m(), 0, num_bound, bound_asts.data(), to_expr(body), abs_body);
270 
271         Z3_ast result = mk_quantifier_ex_core(c, is_forall, weight,
272                                               quantifier_id,
273                                               skolem_id,
274                                               num_patterns, _patterns.data(),
275                                               num_no_patterns, _no_patterns.data(),
276                                               names.size(), types.data(), names.data(),
277                                               of_ast(abs_body.get()));
278         RETURN_Z3(result);
279         Z3_CATCH_RETURN(nullptr);
280     }
281 
Z3_mk_quantifier_const(Z3_context c,bool is_forall,unsigned weight,unsigned num_bound,Z3_app const bound[],unsigned num_patterns,Z3_pattern const patterns[],Z3_ast body)282     Z3_ast Z3_API Z3_mk_quantifier_const(Z3_context c,
283                                          bool is_forall,
284                                          unsigned weight,
285                                          unsigned num_bound,
286                                          Z3_app const bound[],
287                                          unsigned num_patterns,
288                                          Z3_pattern const patterns[],
289                                          Z3_ast body) {
290         return Z3_mk_quantifier_const_ex(c, is_forall, weight, of_symbol(symbol::null), of_symbol(symbol::null),
291                                          num_bound, bound,
292                                          num_patterns, patterns,
293                                          0, nullptr,
294                                          body);
295     }
296 
Z3_mk_forall_const(Z3_context c,unsigned weight,unsigned num_bound,Z3_app const bound[],unsigned num_patterns,Z3_pattern const patterns[],Z3_ast body)297     Z3_ast Z3_API Z3_mk_forall_const(Z3_context c,
298                                      unsigned weight,
299                                      unsigned num_bound,
300                                      Z3_app const bound[],
301                                      unsigned num_patterns,
302                                      Z3_pattern const patterns[],
303                                      Z3_ast body) {
304         return Z3_mk_quantifier_const(c, true, weight, num_bound, bound, num_patterns, patterns, body);
305     }
306 
Z3_mk_exists_const(Z3_context c,unsigned weight,unsigned num_bound,Z3_app const bound[],unsigned num_patterns,Z3_pattern const patterns[],Z3_ast body)307     Z3_ast Z3_API Z3_mk_exists_const(Z3_context c,
308                                      unsigned weight,
309                                      unsigned num_bound,
310                                      Z3_app const bound[],
311                                      unsigned num_patterns,
312                                      Z3_pattern const patterns[],
313                                      Z3_ast body) {
314         return Z3_mk_quantifier_const(c, false, weight, num_bound, bound, num_patterns, patterns, body);
315     }
316 
Z3_mk_pattern(Z3_context c,unsigned num_patterns,Z3_ast const terms[])317     Z3_pattern Z3_API Z3_mk_pattern(Z3_context c, unsigned num_patterns, Z3_ast const terms[]) {
318         Z3_TRY;
319         LOG_Z3_mk_pattern(c, num_patterns, terms);
320         RESET_ERROR_CODE();
321         for (unsigned i = 0; i < num_patterns; ++i) {
322             if (!is_app(to_expr(terms[i]))) {
323                 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
324                 RETURN_Z3(nullptr);
325             }
326         }
327         app* a = mk_c(c)->m().mk_pattern(num_patterns, reinterpret_cast<app*const*>(to_exprs(num_patterns, terms)));
328         mk_c(c)->save_ast_trail(a);
329         RETURN_Z3(of_pattern(a));
330         Z3_CATCH_RETURN(nullptr);
331     }
332 
Z3_mk_bound(Z3_context c,unsigned index,Z3_sort ty)333     Z3_ast Z3_API Z3_mk_bound(Z3_context c, unsigned index, Z3_sort ty) {
334         Z3_TRY;
335         LOG_Z3_mk_bound(c, index, ty);
336         RESET_ERROR_CODE();
337         ast* a = mk_c(c)->m().mk_var(index, to_sort(ty));
338         mk_c(c)->save_ast_trail(a);
339         RETURN_Z3(of_ast(a));
340         Z3_CATCH_RETURN(nullptr);
341     }
342 
Z3_is_quantifier_forall(Z3_context c,Z3_ast a)343     bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a) {
344         Z3_TRY;
345         LOG_Z3_is_quantifier_forall(c, a);
346         RESET_ERROR_CODE();
347         return ::is_forall(to_ast(a));
348         Z3_CATCH_RETURN(false);
349     }
350 
Z3_is_quantifier_exists(Z3_context c,Z3_ast a)351     bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a) {
352         Z3_TRY;
353         LOG_Z3_is_quantifier_exists(c, a);
354         RESET_ERROR_CODE();
355         return ::is_exists(to_ast(a));
356         Z3_CATCH_RETURN(false);
357     }
358 
Z3_is_lambda(Z3_context c,Z3_ast a)359     bool Z3_API Z3_is_lambda(Z3_context c, Z3_ast a) {
360         Z3_TRY;
361         LOG_Z3_is_lambda(c, a);
362         RESET_ERROR_CODE();
363         return ::is_lambda(to_ast(a));
364         Z3_CATCH_RETURN(false);
365     }
366 
367 
Z3_get_quantifier_weight(Z3_context c,Z3_ast a)368     unsigned Z3_API Z3_get_quantifier_weight(Z3_context c, Z3_ast a) {
369         Z3_TRY;
370         LOG_Z3_get_quantifier_weight(c, a);
371         RESET_ERROR_CODE();
372         ast * _a = to_ast(a);
373         if (_a->get_kind() == AST_QUANTIFIER) {
374             return to_quantifier(_a)->get_weight();
375         }
376         else {
377             SET_ERROR_CODE(Z3_SORT_ERROR, nullptr);
378             return 0;
379         }
380         Z3_CATCH_RETURN(0);
381     }
382 
Z3_get_quantifier_num_patterns(Z3_context c,Z3_ast a)383     unsigned Z3_API Z3_get_quantifier_num_patterns(Z3_context c, Z3_ast a) {
384         Z3_TRY;
385         LOG_Z3_get_quantifier_num_patterns(c, a);
386         RESET_ERROR_CODE();
387         ast * _a = to_ast(a);
388         if (_a->get_kind() == AST_QUANTIFIER) {
389             return to_quantifier(_a)->get_num_patterns();
390         }
391         else {
392             SET_ERROR_CODE(Z3_SORT_ERROR, nullptr);
393             return 0;
394         }
395         Z3_CATCH_RETURN(0);
396     }
397 
Z3_get_quantifier_pattern_ast(Z3_context c,Z3_ast a,unsigned i)398     Z3_pattern Z3_API Z3_get_quantifier_pattern_ast(Z3_context c, Z3_ast a, unsigned i) {
399         Z3_TRY;
400         LOG_Z3_get_quantifier_pattern_ast(c, a, i);
401         RESET_ERROR_CODE();
402         ast * _a = to_ast(a);
403         if (_a->get_kind() == AST_QUANTIFIER) {
404             Z3_pattern r = of_pattern(to_quantifier(_a)->get_patterns()[i]);
405             RETURN_Z3(r);
406         }
407         else {
408             SET_ERROR_CODE(Z3_SORT_ERROR, nullptr);
409             RETURN_Z3(nullptr);
410         }
411         Z3_CATCH_RETURN(nullptr);
412     }
413 
414 
Z3_get_quantifier_num_no_patterns(Z3_context c,Z3_ast a)415     unsigned Z3_API Z3_get_quantifier_num_no_patterns(Z3_context c, Z3_ast a) {
416         Z3_TRY;
417         LOG_Z3_get_quantifier_num_no_patterns(c, a);
418         RESET_ERROR_CODE();
419         ast * _a = to_ast(a);
420         if (_a->get_kind() == AST_QUANTIFIER) {
421             return to_quantifier(_a)->get_num_no_patterns();
422         }
423         else {
424             SET_ERROR_CODE(Z3_SORT_ERROR, nullptr);
425             return 0;
426         }
427         Z3_CATCH_RETURN(0);
428     }
429 
Z3_get_quantifier_no_pattern_ast(Z3_context c,Z3_ast a,unsigned i)430     Z3_ast Z3_API Z3_get_quantifier_no_pattern_ast(Z3_context c, Z3_ast a, unsigned i) {
431         Z3_TRY;
432         LOG_Z3_get_quantifier_no_pattern_ast(c, a, i);
433         RESET_ERROR_CODE();
434         ast * _a = to_ast(a);
435         if (_a->get_kind() == AST_QUANTIFIER) {
436             Z3_ast r = of_ast(to_quantifier(_a)->get_no_pattern(i));
437             RETURN_Z3(r);
438         }
439         else {
440             SET_ERROR_CODE(Z3_SORT_ERROR, nullptr);
441             RETURN_Z3(nullptr);
442         }
443         Z3_CATCH_RETURN(nullptr);
444     }
445 
Z3_get_quantifier_bound_name(Z3_context c,Z3_ast a,unsigned i)446     Z3_symbol Z3_API Z3_get_quantifier_bound_name(Z3_context c, Z3_ast a, unsigned i) {
447         Z3_TRY;
448         LOG_Z3_get_quantifier_bound_name(c, a, i);
449         RESET_ERROR_CODE();
450         ast * _a = to_ast(a);
451         if (_a->get_kind() == AST_QUANTIFIER) {
452             return of_symbol(to_quantifier(_a)->get_decl_names()[i]);
453         }
454         else {
455             SET_ERROR_CODE(Z3_SORT_ERROR, nullptr);
456             return of_symbol(symbol::null);
457         }
458         Z3_CATCH_RETURN(of_symbol(symbol::null));
459     }
460 
Z3_get_quantifier_bound_sort(Z3_context c,Z3_ast a,unsigned i)461     Z3_sort Z3_API Z3_get_quantifier_bound_sort(Z3_context c, Z3_ast a, unsigned i) {
462         Z3_TRY;
463         LOG_Z3_get_quantifier_bound_sort(c, a, i);
464         RESET_ERROR_CODE();
465         ast * _a = to_ast(a);
466         if (_a->get_kind() == AST_QUANTIFIER) {
467             Z3_sort r = of_sort(to_quantifier(_a)->get_decl_sort(i));
468             RETURN_Z3(r);
469         }
470         else {
471             SET_ERROR_CODE(Z3_SORT_ERROR, nullptr);
472             RETURN_Z3(nullptr);
473         }
474         Z3_CATCH_RETURN(nullptr);
475     }
476 
Z3_get_quantifier_body(Z3_context c,Z3_ast a)477     Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a) {
478         Z3_TRY;
479         LOG_Z3_get_quantifier_body(c, a);
480         RESET_ERROR_CODE();
481         ast * _a = to_ast(a);
482         if (_a->get_kind() == AST_QUANTIFIER) {
483             Z3_ast r = of_ast(to_quantifier(_a)->get_expr());
484             RETURN_Z3(r);
485         }
486         else {
487             SET_ERROR_CODE(Z3_SORT_ERROR, nullptr);
488             RETURN_Z3(nullptr);
489         }
490         Z3_CATCH_RETURN(nullptr);
491     }
492 
Z3_get_quantifier_num_bound(Z3_context c,Z3_ast a)493     unsigned Z3_API Z3_get_quantifier_num_bound(Z3_context c, Z3_ast a) {
494         Z3_TRY;
495         LOG_Z3_get_quantifier_num_bound(c, a);
496         RESET_ERROR_CODE();
497         ast * _a = to_ast(a);
498         if (_a->get_kind() == AST_QUANTIFIER) {
499 
500             return to_quantifier(_a)->get_num_decls();
501         }
502         else {
503             SET_ERROR_CODE(Z3_SORT_ERROR, nullptr);
504             return 0;
505         }
506         Z3_CATCH_RETURN(0);
507     }
508 
Z3_get_pattern_num_terms(Z3_context c,Z3_pattern p)509     unsigned Z3_API Z3_get_pattern_num_terms(Z3_context c, Z3_pattern p) {
510         Z3_TRY;
511         LOG_Z3_get_pattern_num_terms(c, p);
512         RESET_ERROR_CODE();
513         app* _p = to_pattern(p);
514         if (mk_c(c)->m().is_pattern(_p)) {
515             return _p->get_num_args();
516         }
517         else {
518             SET_ERROR_CODE(Z3_SORT_ERROR, nullptr);
519             return 0;
520         }
521         Z3_CATCH_RETURN(0);
522     }
523 
Z3_get_pattern(Z3_context c,Z3_pattern p,unsigned idx)524     Z3_ast Z3_API Z3_get_pattern(Z3_context c, Z3_pattern p, unsigned idx) {
525         Z3_TRY;
526         LOG_Z3_get_pattern(c, p, idx);
527         RESET_ERROR_CODE();
528         app* _p = to_pattern(p);
529         if (mk_c(c)->m().is_pattern(_p)) {
530             Z3_ast r = of_ast(_p->get_arg(idx));
531             RETURN_Z3(r);
532         }
533         else {
534             SET_ERROR_CODE(Z3_SORT_ERROR, nullptr);
535             RETURN_Z3(nullptr);
536         }
537         Z3_CATCH_RETURN(nullptr);
538     }
539 
Z3_pattern_to_ast(Z3_context c,Z3_pattern p)540     Z3_ast Z3_API Z3_pattern_to_ast(Z3_context c, Z3_pattern p) {
541         RESET_ERROR_CODE();
542         return (Z3_ast)(p);
543     }
544 
Z3_pattern_to_string(Z3_context c,Z3_pattern p)545     Z3_API char const * Z3_pattern_to_string(Z3_context c, Z3_pattern p) {
546         return Z3_ast_to_string(c, reinterpret_cast<Z3_ast>(p));
547     }
548 
549 };
550 
551