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