1 /*++ 2 Copyright (c) 2012 Microsoft Corporation 3 4 Module Name: 5 6 api_ast.cpp 7 8 Abstract: 9 Basic API for ASTs 10 11 Author: 12 13 Leonardo de Moura (leonardo) 2012-02-29. 14 15 Revision History: 16 17 --*/ 18 #include<iostream> 19 #include "api/api_log_macros.h" 20 #include "api/api_context.h" 21 #include "api/api_util.h" 22 #include "ast/well_sorted.h" 23 #include "ast/arith_decl_plugin.h" 24 #include "ast/bv_decl_plugin.h" 25 #include "ast/datatype_decl_plugin.h" 26 #include "ast/array_decl_plugin.h" 27 #include "ast/pb_decl_plugin.h" 28 #include "ast/ast_translation.h" 29 #include "ast/ast_pp.h" 30 #include "ast/ast_ll_pp.h" 31 #include "ast/ast_smt_pp.h" 32 #include "ast/ast_smt2_pp.h" 33 #include "ast/rewriter/th_rewriter.h" 34 #include "ast/rewriter/var_subst.h" 35 #include "ast/rewriter/expr_safe_replace.h" 36 #include "ast/rewriter/recfun_replace.h" 37 #include "ast/rewriter/seq_rewriter.h" 38 #include "ast/pp.h" 39 #include "util/scoped_ctrl_c.h" 40 #include "util/cancel_eh.h" 41 #include "util/scoped_timer.h" 42 #include "ast/pp_params.hpp" 43 #include "ast/expr_abstract.h" 44 45 46 extern bool is_numeral_sort(Z3_context c, Z3_sort ty); 47 48 extern "C" { 49 Z3_mk_int_symbol(Z3_context c,int i)50 Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i) { 51 Z3_TRY; 52 LOG_Z3_mk_int_symbol(c, i); 53 RESET_ERROR_CODE(); 54 if (i < 0 || (size_t)i >= (SIZE_MAX >> PTR_ALIGNMENT)) { 55 SET_ERROR_CODE(Z3_IOB, nullptr); 56 return of_symbol(symbol::null); 57 } 58 Z3_symbol result = of_symbol(symbol((unsigned)i)); 59 return result; 60 Z3_CATCH_RETURN(of_symbol(symbol::null)); 61 } 62 Z3_mk_string_symbol(Z3_context c,char const * str)63 Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, char const * str) { 64 Z3_TRY; 65 LOG_Z3_mk_string_symbol(c, str); 66 RESET_ERROR_CODE(); 67 symbol s; 68 if (str == nullptr || *str == 0) 69 s = symbol::null; 70 else 71 s = symbol(str); 72 Z3_symbol result = of_symbol(s); 73 return result; 74 Z3_CATCH_RETURN(of_symbol(symbol::null)); 75 } 76 Z3_is_eq_sort(Z3_context c,Z3_sort s1,Z3_sort s2)77 bool Z3_API Z3_is_eq_sort(Z3_context c, Z3_sort s1, Z3_sort s2) { 78 RESET_ERROR_CODE(); 79 return s1 == s2; 80 } 81 Z3_mk_uninterpreted_sort(Z3_context c,Z3_symbol name)82 Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol name) { 83 Z3_TRY; 84 LOG_Z3_mk_uninterpreted_sort(c, name); 85 RESET_ERROR_CODE(); 86 sort* ty = mk_c(c)->m().mk_uninterpreted_sort(to_symbol(name)); 87 mk_c(c)->save_ast_trail(ty); 88 RETURN_Z3(of_sort(ty)); 89 Z3_CATCH_RETURN(nullptr); 90 } 91 Z3_is_eq_ast(Z3_context c,Z3_ast s1,Z3_ast s2)92 bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast s1, Z3_ast s2) { 93 RESET_ERROR_CODE(); 94 return s1 == s2; 95 } 96 Z3_is_eq_func_decl(Z3_context c,Z3_func_decl s1,Z3_func_decl s2)97 bool Z3_API Z3_is_eq_func_decl(Z3_context c, Z3_func_decl s1, Z3_func_decl s2) { 98 RESET_ERROR_CODE(); 99 return s1 == s2; 100 } 101 Z3_mk_func_decl(Z3_context c,Z3_symbol s,unsigned domain_size,Z3_sort const * domain,Z3_sort range)102 Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const* domain, 103 Z3_sort range) { 104 Z3_TRY; 105 LOG_Z3_mk_func_decl(c, s, domain_size, domain, range); 106 RESET_ERROR_CODE(); 107 func_decl* d = mk_c(c)->m().mk_func_decl(to_symbol(s), 108 domain_size, 109 to_sorts(domain), 110 to_sort(range)); 111 112 mk_c(c)->save_ast_trail(d); 113 RETURN_Z3(of_func_decl(d)); 114 Z3_CATCH_RETURN(nullptr); 115 } 116 Z3_mk_rec_func_decl(Z3_context c,Z3_symbol s,unsigned domain_size,Z3_sort const * domain,Z3_sort range)117 Z3_func_decl Z3_API Z3_mk_rec_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const* domain, 118 Z3_sort range) { 119 Z3_TRY; 120 LOG_Z3_mk_rec_func_decl(c, s, domain_size, domain, range); 121 RESET_ERROR_CODE(); 122 // 123 recfun::promise_def def = 124 mk_c(c)->recfun().get_plugin().mk_def(to_symbol(s), 125 domain_size, 126 to_sorts(domain), 127 to_sort(range)); 128 func_decl* d = def.get_def()->get_decl(); 129 mk_c(c)->save_ast_trail(d); 130 RETURN_Z3(of_func_decl(d)); 131 Z3_CATCH_RETURN(nullptr); 132 } 133 Z3_add_rec_def(Z3_context c,Z3_func_decl f,unsigned n,Z3_ast args[],Z3_ast body)134 void Z3_API Z3_add_rec_def(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast args[], Z3_ast body) { 135 Z3_TRY; 136 LOG_Z3_add_rec_def(c, f, n, args, body); 137 func_decl* d = to_func_decl(f); 138 ast_manager& m = mk_c(c)->m(); 139 recfun::decl::plugin& p = mk_c(c)->recfun().get_plugin(); 140 expr_ref abs_body(m); 141 expr_ref_vector _args(m); 142 var_ref_vector _vars(m); 143 for (unsigned i = 0; i < n; ++i) { 144 _args.push_back(to_expr(args[i])); 145 _vars.push_back(m.mk_var(n - i - 1, m.get_sort(_args.back()))); 146 if (m.get_sort(_args.back()) != d->get_domain(i)) { 147 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 148 return; 149 } 150 } 151 expr_abstract(m, 0, n, _args.c_ptr(), to_expr(body), abs_body); 152 recfun::promise_def pd = p.get_promise_def(d); 153 if (!pd.get_def()) { 154 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 155 return; 156 } 157 if (m.get_sort(abs_body) != d->get_range()) { 158 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 159 return; 160 } 161 recfun_replace replace(m); 162 p.set_definition(replace, pd, n, _vars.c_ptr(), abs_body); 163 Z3_CATCH; 164 } 165 Z3_mk_app(Z3_context c,Z3_func_decl d,unsigned num_args,Z3_ast const * args)166 Z3_ast Z3_API Z3_mk_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const * args) { 167 Z3_TRY; 168 LOG_Z3_mk_app(c, d, num_args, args); 169 RESET_ERROR_CODE(); 170 ptr_buffer<expr> arg_list; 171 for (unsigned i = 0; i < num_args; ++i) { 172 arg_list.push_back(to_expr(args[i])); 173 } 174 func_decl* _d = reinterpret_cast<func_decl*>(d); 175 app* a = mk_c(c)->m().mk_app(_d, num_args, arg_list.c_ptr()); 176 mk_c(c)->save_ast_trail(a); 177 check_sorts(c, a); 178 RETURN_Z3(of_ast(a)); 179 Z3_CATCH_RETURN(nullptr); 180 } 181 Z3_mk_const(Z3_context c,Z3_symbol s,Z3_sort ty)182 Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty) { 183 Z3_TRY; 184 LOG_Z3_mk_const(c, s, ty); 185 RESET_ERROR_CODE(); 186 app* a = mk_c(c)->m().mk_const(mk_c(c)->m().mk_const_decl(to_symbol(s), to_sort(ty))); 187 mk_c(c)->save_ast_trail(a); 188 RETURN_Z3(of_ast(a)); 189 Z3_CATCH_RETURN(nullptr); 190 } 191 192 Z3_mk_fresh_func_decl(Z3_context c,const char * prefix,unsigned domain_size,Z3_sort const domain[],Z3_sort range)193 Z3_func_decl Z3_API Z3_mk_fresh_func_decl(Z3_context c, const char * prefix, unsigned domain_size, 194 Z3_sort const domain[], Z3_sort range) { 195 Z3_TRY; 196 LOG_Z3_mk_fresh_func_decl(c, prefix, domain_size, domain, range); 197 RESET_ERROR_CODE(); 198 if (prefix == nullptr) { 199 prefix = ""; 200 } 201 202 func_decl* d = mk_c(c)->m().mk_fresh_func_decl(prefix, 203 domain_size, 204 reinterpret_cast<sort*const*>(domain), 205 to_sort(range), false); 206 207 mk_c(c)->save_ast_trail(d); 208 RETURN_Z3(of_func_decl(d)); 209 Z3_CATCH_RETURN(nullptr); 210 } 211 Z3_mk_fresh_const(Z3_context c,const char * prefix,Z3_sort ty)212 Z3_ast Z3_API Z3_mk_fresh_const(Z3_context c, const char * prefix, Z3_sort ty) { 213 Z3_TRY; 214 LOG_Z3_mk_fresh_const(c, prefix, ty); 215 RESET_ERROR_CODE(); 216 if (prefix == nullptr) { 217 prefix = ""; 218 } 219 app* a = mk_c(c)->m().mk_fresh_const(prefix, to_sort(ty), false); 220 mk_c(c)->save_ast_trail(a); 221 RETURN_Z3(of_ast(a)); 222 Z3_CATCH_RETURN(nullptr); 223 } 224 Z3_mk_true(Z3_context c)225 Z3_ast Z3_API Z3_mk_true(Z3_context c) { 226 Z3_TRY; 227 LOG_Z3_mk_true(c); 228 RESET_ERROR_CODE(); 229 Z3_ast r = of_ast(mk_c(c)->m().mk_true()); 230 RETURN_Z3(r); 231 Z3_CATCH_RETURN(nullptr); 232 } 233 Z3_mk_false(Z3_context c)234 Z3_ast Z3_API Z3_mk_false(Z3_context c) { 235 Z3_TRY; 236 LOG_Z3_mk_false(c); 237 RESET_ERROR_CODE(); 238 Z3_ast r = of_ast(mk_c(c)->m().mk_false()); 239 RETURN_Z3(r); 240 Z3_CATCH_RETURN(nullptr); 241 } 242 243 MK_UNARY(Z3_mk_not, mk_c(c)->get_basic_fid(), OP_NOT, SKIP); 244 MK_BINARY(Z3_mk_eq, mk_c(c)->get_basic_fid(), OP_EQ, SKIP); 245 MK_NARY(Z3_mk_distinct, mk_c(c)->get_basic_fid(), OP_DISTINCT, SKIP); 246 MK_BINARY(Z3_mk_iff, mk_c(c)->get_basic_fid(), OP_EQ, SKIP); 247 MK_BINARY(Z3_mk_implies, mk_c(c)->get_basic_fid(), OP_IMPLIES, SKIP); 248 MK_BINARY(Z3_mk_xor, mk_c(c)->get_basic_fid(), OP_XOR, SKIP); 249 MK_NARY(Z3_mk_and, mk_c(c)->get_basic_fid(), OP_AND, SKIP); 250 MK_NARY(Z3_mk_or, mk_c(c)->get_basic_fid(), OP_OR, SKIP); 251 mk_ite_core(Z3_context c,Z3_ast t1,Z3_ast t2,Z3_ast t3)252 Z3_ast mk_ite_core(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3) { 253 expr * result = mk_c(c)->m().mk_ite(to_expr(t1), to_expr(t2), to_expr(t3)); 254 mk_c(c)->save_ast_trail(result); 255 check_sorts(c, result); 256 return of_ast(result); 257 } 258 Z3_mk_ite(Z3_context c,Z3_ast t1,Z3_ast t2,Z3_ast t3)259 Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3) { 260 Z3_TRY; 261 LOG_Z3_mk_ite(c, t1, t2, t3); 262 RESET_ERROR_CODE(); 263 Z3_ast r = mk_ite_core(c, t1, t2, t3); 264 RETURN_Z3(r); 265 Z3_CATCH_RETURN(nullptr); 266 } 267 Z3_mk_bool_sort(Z3_context c)268 Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c) { 269 Z3_TRY; 270 LOG_Z3_mk_bool_sort(c); 271 RESET_ERROR_CODE(); 272 Z3_sort r = of_sort(mk_c(c)->m().mk_sort(mk_c(c)->m().get_basic_family_id(), BOOL_SORT)); 273 RETURN_Z3(r); 274 Z3_CATCH_RETURN(nullptr); 275 } 276 Z3_app_to_ast(Z3_context c,Z3_app a)277 Z3_ast Z3_API Z3_app_to_ast(Z3_context c, Z3_app a) { 278 RESET_ERROR_CODE(); 279 return (Z3_ast)(a); 280 } 281 Z3_sort_to_ast(Z3_context c,Z3_sort s)282 Z3_ast Z3_API Z3_sort_to_ast(Z3_context c, Z3_sort s) { 283 RESET_ERROR_CODE(); 284 return (Z3_ast)(s); 285 } 286 Z3_func_decl_to_ast(Z3_context c,Z3_func_decl f)287 Z3_ast Z3_API Z3_func_decl_to_ast(Z3_context c, Z3_func_decl f) { 288 RESET_ERROR_CODE(); 289 return (Z3_ast)(f); 290 } 291 292 // ------------------------ 293 Z3_get_ast_id(Z3_context c,Z3_ast t)294 unsigned Z3_API Z3_get_ast_id(Z3_context c, Z3_ast t) { 295 LOG_Z3_get_ast_id(c, t); 296 RESET_ERROR_CODE(); 297 return to_expr(t)->get_id(); 298 } 299 Z3_get_func_decl_id(Z3_context c,Z3_func_decl f)300 unsigned Z3_API Z3_get_func_decl_id(Z3_context c, Z3_func_decl f) { 301 LOG_Z3_get_func_decl_id(c, f); 302 RESET_ERROR_CODE(); 303 return to_func_decl(f)->get_id(); 304 } 305 Z3_get_sort_id(Z3_context c,Z3_sort s)306 unsigned Z3_API Z3_get_sort_id(Z3_context c, Z3_sort s) { 307 LOG_Z3_get_sort_id(c, s); 308 RESET_ERROR_CODE(); 309 return to_sort(s)->get_id(); 310 } 311 Z3_is_well_sorted(Z3_context c,Z3_ast t)312 bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t) { 313 Z3_TRY; 314 LOG_Z3_is_well_sorted(c, t); 315 RESET_ERROR_CODE(); 316 return is_well_sorted(mk_c(c)->m(), to_expr(t)); 317 Z3_CATCH_RETURN(false); 318 } 319 Z3_get_symbol_kind(Z3_context c,Z3_symbol s)320 Z3_symbol_kind Z3_API Z3_get_symbol_kind(Z3_context c, Z3_symbol s) { 321 Z3_TRY; 322 LOG_Z3_get_symbol_kind(c, s); 323 RESET_ERROR_CODE(); 324 symbol _s = to_symbol(s); 325 return _s.is_numerical() ? Z3_INT_SYMBOL : Z3_STRING_SYMBOL; 326 Z3_CATCH_RETURN(Z3_INT_SYMBOL); 327 } 328 Z3_get_symbol_int(Z3_context c,Z3_symbol s)329 int Z3_API Z3_get_symbol_int(Z3_context c, Z3_symbol s) { 330 Z3_TRY; 331 LOG_Z3_get_symbol_int(c, s); 332 RESET_ERROR_CODE(); 333 symbol _s = to_symbol(s); 334 if (_s.is_numerical()) { 335 return _s.get_num(); 336 } 337 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 338 return -1; 339 Z3_CATCH_RETURN(-1); 340 } 341 Z3_get_symbol_string(Z3_context c,Z3_symbol s)342 Z3_API char const * Z3_get_symbol_string(Z3_context c, Z3_symbol s) { 343 Z3_TRY; 344 LOG_Z3_get_symbol_string(c, s); 345 RESET_ERROR_CODE(); 346 symbol _s = to_symbol(s); 347 if (_s.is_numerical()) { 348 std::ostringstream buffer; 349 buffer << _s.get_num(); 350 return mk_c(c)->mk_external_string(buffer.str()); 351 } 352 else { 353 return mk_c(c)->mk_external_string(_s.bare_str()); 354 } 355 Z3_CATCH_RETURN(""); 356 } 357 Z3_get_ast_kind(Z3_context c,Z3_ast a)358 Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a) { 359 Z3_TRY; 360 LOG_Z3_get_ast_kind(c, a); 361 RESET_ERROR_CODE(); 362 CHECK_VALID_AST(a, Z3_UNKNOWN_AST); 363 ast * _a = to_expr(a); 364 switch (_a->get_kind()) { 365 case AST_APP: { 366 expr * e = to_expr(_a); 367 // Real algebraic numbers are not considered Z3_NUMERAL_AST 368 if (is_numeral_sort(c, of_sort(mk_c(c)->m().get_sort(e))) && mk_c(c)->m().is_unique_value(e)) 369 return Z3_NUMERAL_AST; 370 return Z3_APP_AST; 371 } 372 case AST_VAR: return Z3_VAR_AST; 373 case AST_QUANTIFIER: return Z3_QUANTIFIER_AST; 374 case AST_SORT: return Z3_SORT_AST; 375 case AST_FUNC_DECL: return Z3_FUNC_DECL_AST; 376 default: return Z3_UNKNOWN_AST; 377 } 378 Z3_CATCH_RETURN(Z3_UNKNOWN_AST); 379 } 380 Z3_get_ast_hash(Z3_context c,Z3_ast a)381 unsigned Z3_API Z3_get_ast_hash(Z3_context c, Z3_ast a) { 382 LOG_Z3_get_ast_hash(c, a); 383 RESET_ERROR_CODE(); 384 return to_ast(a)->hash(); 385 } 386 Z3_is_app(Z3_context c,Z3_ast a)387 bool Z3_API Z3_is_app(Z3_context c, Z3_ast a) { 388 LOG_Z3_is_app(c, a); 389 RESET_ERROR_CODE(); 390 return a != nullptr && is_app(reinterpret_cast<ast*>(a)); 391 } 392 Z3_to_app(Z3_context c,Z3_ast a)393 Z3_app Z3_API Z3_to_app(Z3_context c, Z3_ast a) { 394 LOG_Z3_to_app(c, a); 395 RESET_ERROR_CODE(); 396 SASSERT(is_app(reinterpret_cast<ast*>(a))); 397 RETURN_Z3(of_app(reinterpret_cast<app*>(a))); 398 } 399 Z3_to_func_decl(Z3_context c,Z3_ast a)400 Z3_func_decl Z3_API Z3_to_func_decl(Z3_context c, Z3_ast a) { 401 LOG_Z3_to_func_decl(c, a); 402 RESET_ERROR_CODE(); 403 SASSERT(is_func_decl(reinterpret_cast<ast*>(a))); 404 RETURN_Z3(of_func_decl(reinterpret_cast<func_decl*>(a))); 405 } 406 Z3_get_app_decl(Z3_context c,Z3_app a)407 Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a) { 408 LOG_Z3_get_app_decl(c, a); 409 RESET_ERROR_CODE(); 410 if (!is_app(reinterpret_cast<ast*>(a))) { 411 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 412 RETURN_Z3(nullptr); 413 } 414 RETURN_Z3(of_func_decl(to_app(a)->get_decl())); 415 } 416 Z3_get_app_num_args(Z3_context c,Z3_app a)417 unsigned Z3_API Z3_get_app_num_args(Z3_context c, Z3_app a) { 418 LOG_Z3_get_app_num_args(c, a); 419 RESET_ERROR_CODE(); 420 return to_app(a)->get_num_args(); 421 } 422 Z3_get_app_arg(Z3_context c,Z3_app a,unsigned i)423 Z3_ast Z3_API Z3_get_app_arg(Z3_context c, Z3_app a, unsigned i) { 424 LOG_Z3_get_app_arg(c, a, i); 425 RESET_ERROR_CODE(); 426 if (!is_app(reinterpret_cast<ast*>(a))) { 427 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 428 RETURN_Z3(nullptr); 429 } 430 if (i >= to_app(a)->get_num_args()) { 431 SET_ERROR_CODE(Z3_IOB, nullptr); 432 RETURN_Z3(nullptr); 433 } 434 RETURN_Z3(of_ast(to_app(a)->get_arg(i))); 435 } 436 Z3_get_decl_name(Z3_context c,Z3_func_decl d)437 Z3_symbol Z3_API Z3_get_decl_name(Z3_context c, Z3_func_decl d) { 438 LOG_Z3_get_decl_name(c, d); 439 RESET_ERROR_CODE(); 440 CHECK_VALID_AST(d, of_symbol(symbol::null)); 441 return of_symbol(to_func_decl(d)->get_name()); 442 } 443 Z3_get_decl_num_parameters(Z3_context c,Z3_func_decl d)444 unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d) { 445 LOG_Z3_get_decl_num_parameters(c, d); 446 RESET_ERROR_CODE(); 447 CHECK_VALID_AST(d, 0); 448 return to_func_decl(d)->get_num_parameters(); 449 } 450 Z3_get_decl_parameter_kind(Z3_context c,Z3_func_decl d,unsigned idx)451 Z3_parameter_kind Z3_API Z3_get_decl_parameter_kind(Z3_context c, Z3_func_decl d, unsigned idx) { 452 Z3_TRY; 453 LOG_Z3_get_decl_parameter_kind(c, d, idx); 454 RESET_ERROR_CODE(); 455 CHECK_VALID_AST(d, Z3_PARAMETER_INT); 456 if (idx >= to_func_decl(d)->get_num_parameters()) { 457 SET_ERROR_CODE(Z3_IOB, nullptr); 458 return Z3_PARAMETER_INT; 459 } 460 parameter const& p = to_func_decl(d)->get_parameters()[idx]; 461 if (p.is_int()) { 462 return Z3_PARAMETER_INT; 463 } 464 if (p.is_double()) { 465 return Z3_PARAMETER_DOUBLE; 466 } 467 if (p.is_symbol()) { 468 return Z3_PARAMETER_SYMBOL; 469 } 470 if (p.is_rational()) { 471 return Z3_PARAMETER_RATIONAL; 472 } 473 if (p.is_ast() && is_sort(p.get_ast())) { 474 return Z3_PARAMETER_SORT; 475 } 476 if (p.is_ast() && is_expr(p.get_ast())) { 477 return Z3_PARAMETER_AST; 478 } 479 SASSERT(p.is_ast() && is_func_decl(p.get_ast())); 480 return Z3_PARAMETER_FUNC_DECL; 481 Z3_CATCH_RETURN(Z3_PARAMETER_INT); 482 } 483 Z3_get_decl_int_parameter(Z3_context c,Z3_func_decl d,unsigned idx)484 int Z3_API Z3_get_decl_int_parameter(Z3_context c, Z3_func_decl d, unsigned idx) { 485 Z3_TRY; 486 LOG_Z3_get_decl_int_parameter(c, d, idx); 487 RESET_ERROR_CODE(); 488 CHECK_VALID_AST(d, 0); 489 if (idx >= to_func_decl(d)->get_num_parameters()) { 490 SET_ERROR_CODE(Z3_IOB, nullptr); 491 return 0; 492 } 493 parameter const& p = to_func_decl(d)->get_parameters()[idx]; 494 if (!p.is_int()) { 495 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 496 return 0; 497 } 498 return p.get_int(); 499 Z3_CATCH_RETURN(0); 500 } 501 Z3_get_decl_double_parameter(Z3_context c,Z3_func_decl d,unsigned idx)502 double Z3_API Z3_get_decl_double_parameter(Z3_context c, Z3_func_decl d, unsigned idx) { 503 Z3_TRY; 504 LOG_Z3_get_decl_double_parameter(c, d, idx); 505 RESET_ERROR_CODE(); 506 CHECK_VALID_AST(d, 0); 507 if (idx >= to_func_decl(d)->get_num_parameters()) { 508 SET_ERROR_CODE(Z3_IOB, nullptr); 509 return 0; 510 } 511 parameter const& p = to_func_decl(d)->get_parameters()[idx]; 512 if (!p.is_double()) { 513 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 514 return 0; 515 } 516 return p.get_double(); 517 Z3_CATCH_RETURN(0.0); 518 } 519 Z3_get_decl_symbol_parameter(Z3_context c,Z3_func_decl d,unsigned idx)520 Z3_symbol Z3_API Z3_get_decl_symbol_parameter(Z3_context c, Z3_func_decl d, unsigned idx) { 521 Z3_TRY; 522 LOG_Z3_get_decl_symbol_parameter(c, d, idx); 523 RESET_ERROR_CODE(); 524 CHECK_VALID_AST(d, of_symbol(symbol::null)); 525 if (idx >= to_func_decl(d)->get_num_parameters()) { 526 SET_ERROR_CODE(Z3_IOB, nullptr); 527 return of_symbol(symbol::null); 528 } 529 parameter const& p = to_func_decl(d)->get_parameters()[idx]; 530 if (!p.is_symbol()) { 531 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 532 return of_symbol(symbol::null); 533 } 534 return of_symbol(p.get_symbol()); 535 Z3_CATCH_RETURN(of_symbol(symbol::null)); 536 } 537 Z3_get_decl_sort_parameter(Z3_context c,Z3_func_decl d,unsigned idx)538 Z3_sort Z3_API Z3_get_decl_sort_parameter(Z3_context c, Z3_func_decl d, unsigned idx) { 539 Z3_TRY; 540 LOG_Z3_get_decl_sort_parameter(c, d, idx); 541 RESET_ERROR_CODE(); 542 CHECK_VALID_AST(d, nullptr); 543 if (idx >= to_func_decl(d)->get_num_parameters()) { 544 SET_ERROR_CODE(Z3_IOB, nullptr); 545 RETURN_Z3(nullptr); 546 } 547 parameter const& p = to_func_decl(d)->get_parameters()[idx]; 548 if (!p.is_ast() || !is_sort(p.get_ast())) { 549 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 550 RETURN_Z3(nullptr); 551 } 552 RETURN_Z3(of_sort(to_sort(p.get_ast()))); 553 Z3_CATCH_RETURN(nullptr); 554 } 555 Z3_get_decl_ast_parameter(Z3_context c,Z3_func_decl d,unsigned idx)556 Z3_ast Z3_API Z3_get_decl_ast_parameter(Z3_context c, Z3_func_decl d, unsigned idx) { 557 Z3_TRY; 558 LOG_Z3_get_decl_ast_parameter(c, d, idx); 559 RESET_ERROR_CODE(); 560 CHECK_VALID_AST(d, nullptr); 561 if (idx >= to_func_decl(d)->get_num_parameters()) { 562 SET_ERROR_CODE(Z3_IOB, nullptr); 563 RETURN_Z3(nullptr); 564 } 565 parameter const& p = to_func_decl(d)->get_parameters()[idx]; 566 if (!p.is_ast()) { 567 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 568 RETURN_Z3(nullptr); 569 } 570 RETURN_Z3(of_ast(p.get_ast())); 571 Z3_CATCH_RETURN(nullptr); 572 } 573 Z3_get_decl_func_decl_parameter(Z3_context c,Z3_func_decl d,unsigned idx)574 Z3_func_decl Z3_API Z3_get_decl_func_decl_parameter(Z3_context c, Z3_func_decl d, unsigned idx) { 575 Z3_TRY; 576 LOG_Z3_get_decl_func_decl_parameter(c, d, idx); 577 RESET_ERROR_CODE(); 578 CHECK_VALID_AST(d, nullptr); 579 if (idx >= to_func_decl(d)->get_num_parameters()) { 580 SET_ERROR_CODE(Z3_IOB, nullptr); 581 RETURN_Z3(nullptr); 582 } 583 parameter const& p = to_func_decl(d)->get_parameters()[idx]; 584 if (!p.is_ast() || !is_func_decl(p.get_ast())) { 585 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 586 RETURN_Z3(nullptr); 587 } 588 RETURN_Z3(of_func_decl(to_func_decl(p.get_ast()))); 589 Z3_CATCH_RETURN(nullptr); 590 } 591 Z3_get_decl_rational_parameter(Z3_context c,Z3_func_decl d,unsigned idx)592 Z3_string Z3_API Z3_get_decl_rational_parameter(Z3_context c, Z3_func_decl d, unsigned idx) { 593 Z3_TRY; 594 LOG_Z3_get_decl_rational_parameter(c, d, idx); 595 RESET_ERROR_CODE(); 596 CHECK_VALID_AST(d, ""); 597 if (idx >= to_func_decl(d)->get_num_parameters()) { 598 SET_ERROR_CODE(Z3_IOB, nullptr); 599 return ""; 600 } 601 parameter const& p = to_func_decl(d)->get_parameters()[idx]; 602 if (!p.is_rational()) { 603 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 604 return ""; 605 } 606 return mk_c(c)->mk_external_string(p.get_rational().to_string()); 607 Z3_CATCH_RETURN(""); 608 } 609 610 Z3_get_sort_name(Z3_context c,Z3_sort t)611 Z3_symbol Z3_API Z3_get_sort_name(Z3_context c, Z3_sort t) { 612 Z3_TRY; 613 LOG_Z3_get_sort_name(c, t); 614 RESET_ERROR_CODE(); 615 CHECK_VALID_AST(t, of_symbol(symbol::null)); 616 return of_symbol(to_sort(t)->get_name()); 617 Z3_CATCH_RETURN(of_symbol(symbol::null)); 618 } 619 Z3_get_sort(Z3_context c,Z3_ast a)620 Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a) { 621 Z3_TRY; 622 LOG_Z3_get_sort(c, a); 623 RESET_ERROR_CODE(); 624 CHECK_IS_EXPR(a, nullptr); 625 Z3_sort r = of_sort(mk_c(c)->m().get_sort(to_expr(a))); 626 RETURN_Z3(r); 627 Z3_CATCH_RETURN(nullptr); 628 } 629 Z3_get_arity(Z3_context c,Z3_func_decl d)630 unsigned Z3_API Z3_get_arity(Z3_context c, Z3_func_decl d) { 631 Z3_TRY; 632 LOG_Z3_get_arity(c, d); 633 RESET_ERROR_CODE(); 634 CHECK_VALID_AST(d, 0); 635 return to_func_decl(d)->get_arity(); 636 Z3_CATCH_RETURN(0); 637 } 638 Z3_get_domain_size(Z3_context c,Z3_func_decl d)639 unsigned Z3_API Z3_get_domain_size(Z3_context c, Z3_func_decl d) { 640 Z3_TRY; 641 LOG_Z3_get_domain_size(c, d); 642 RESET_ERROR_CODE(); 643 CHECK_VALID_AST(d, 0); 644 return to_func_decl(d)->get_arity(); 645 Z3_CATCH_RETURN(0); 646 } 647 Z3_get_domain(Z3_context c,Z3_func_decl d,unsigned i)648 Z3_sort Z3_API Z3_get_domain(Z3_context c, Z3_func_decl d, unsigned i) { 649 Z3_TRY; 650 LOG_Z3_get_domain(c, d, i); 651 RESET_ERROR_CODE(); 652 CHECK_VALID_AST(d, nullptr); 653 if (i >= to_func_decl(d)->get_arity()) { 654 SET_ERROR_CODE(Z3_IOB, nullptr); 655 RETURN_Z3(nullptr); 656 } 657 Z3_sort r = of_sort(to_func_decl(d)->get_domain(i)); 658 RETURN_Z3(r); 659 Z3_CATCH_RETURN(nullptr); 660 } 661 Z3_get_range(Z3_context c,Z3_func_decl d)662 Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d) { 663 Z3_TRY; 664 LOG_Z3_get_range(c, d); 665 RESET_ERROR_CODE(); 666 CHECK_VALID_AST(d, nullptr); 667 Z3_sort r = of_sort(to_func_decl(d)->get_range()); 668 RETURN_Z3(r); 669 Z3_CATCH_RETURN(nullptr); 670 } 671 Z3_get_sort_kind(Z3_context c,Z3_sort t)672 Z3_sort_kind Z3_get_sort_kind(Z3_context c, Z3_sort t) { 673 LOG_Z3_get_sort_kind(c, t); 674 RESET_ERROR_CODE(); 675 CHECK_VALID_AST(t, Z3_UNKNOWN_SORT); 676 family_id fid = to_sort(t)->get_family_id(); 677 decl_kind k = to_sort(t)->get_decl_kind(); 678 if (mk_c(c)->m().is_uninterp(to_sort(t))) { 679 return Z3_UNINTERPRETED_SORT; 680 } 681 else if (fid == mk_c(c)->m().get_basic_family_id() && k == BOOL_SORT) { 682 return Z3_BOOL_SORT; 683 } 684 else if (fid == mk_c(c)->get_arith_fid() && k == INT_SORT) { 685 return Z3_INT_SORT; 686 } 687 else if (fid == mk_c(c)->get_arith_fid() && k == REAL_SORT) { 688 return Z3_REAL_SORT; 689 } 690 else if (fid == mk_c(c)->get_bv_fid() && k == BV_SORT) { 691 return Z3_BV_SORT; 692 } 693 else if (fid == mk_c(c)->get_array_fid() && k == ARRAY_SORT) { 694 return Z3_ARRAY_SORT; 695 } 696 else if (fid == mk_c(c)->get_dt_fid() && k == DATATYPE_SORT) { 697 return Z3_DATATYPE_SORT; 698 } 699 else if (fid == mk_c(c)->get_datalog_fid() && k == datalog::DL_RELATION_SORT) { 700 return Z3_RELATION_SORT; 701 } 702 else if (fid == mk_c(c)->get_datalog_fid() && k == datalog::DL_FINITE_SORT) { 703 return Z3_FINITE_DOMAIN_SORT; 704 } 705 else if (fid == mk_c(c)->get_fpa_fid() && k == FLOATING_POINT_SORT) { 706 return Z3_FLOATING_POINT_SORT; 707 } 708 else if (fid == mk_c(c)->get_fpa_fid() && k == ROUNDING_MODE_SORT) { 709 return Z3_ROUNDING_MODE_SORT; 710 } 711 else if (fid == mk_c(c)->get_seq_fid() && k == SEQ_SORT) { 712 return Z3_SEQ_SORT; 713 } 714 else if (fid == mk_c(c)->get_seq_fid() && k == RE_SORT) { 715 return Z3_RE_SORT; 716 } 717 else { 718 return Z3_UNKNOWN_SORT; 719 } 720 } 721 Z3_get_bool_value(Z3_context c,Z3_ast a)722 Z3_lbool Z3_API Z3_get_bool_value(Z3_context c, Z3_ast a) { 723 Z3_TRY; 724 LOG_Z3_get_bool_value(c, a); 725 RESET_ERROR_CODE(); 726 CHECK_IS_EXPR(a, Z3_L_UNDEF); 727 ast_manager & m = mk_c(c)->m(); 728 ast * n = to_ast(a); 729 if (m.is_true(to_expr(n))) 730 return Z3_L_TRUE; 731 if (m.is_false(to_expr(n))) 732 return Z3_L_FALSE; 733 return Z3_L_UNDEF; 734 Z3_CATCH_RETURN(Z3_L_UNDEF); 735 } 736 737 simplify(Z3_context c,Z3_ast _a,Z3_params _p)738 static Z3_ast simplify(Z3_context c, Z3_ast _a, Z3_params _p) { 739 Z3_TRY; 740 RESET_ERROR_CODE(); 741 ast_manager & m = mk_c(c)->m(); 742 expr * a = to_expr(_a); 743 auto &p = to_param_ref(_p); 744 unsigned timeout = p.get_uint("timeout", mk_c(c)->get_timeout()); 745 bool use_ctrl_c = p.get_bool("ctrl_c", false); 746 th_rewriter m_rw(m, p); 747 m_rw.set_solver(alloc(api::seq_expr_solver, m, p)); 748 expr_ref result(m); 749 cancel_eh<reslimit> eh(m.limit()); 750 api::context::set_interruptable si(*(mk_c(c)), eh); 751 { 752 scoped_ctrl_c ctrlc(eh, false, use_ctrl_c); 753 scoped_timer timer(timeout, &eh); 754 try { 755 m_rw(a, result); 756 } 757 catch (z3_exception & ex) { 758 mk_c(c)->handle_exception(ex); 759 return nullptr; 760 } 761 } 762 mk_c(c)->save_ast_trail(result); 763 return of_ast(result.get()); 764 Z3_CATCH_RETURN(nullptr); 765 } 766 Z3_simplify(Z3_context c,Z3_ast _a)767 Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast _a) { 768 LOG_Z3_simplify(c, _a); 769 RETURN_Z3(simplify(c, _a, nullptr)); 770 } 771 Z3_simplify_ex(Z3_context c,Z3_ast _a,Z3_params p)772 Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast _a, Z3_params p) { 773 LOG_Z3_simplify_ex(c, _a, p); 774 RETURN_Z3(simplify(c, _a, p)); 775 } 776 Z3_simplify_get_help(Z3_context c)777 Z3_string Z3_API Z3_simplify_get_help(Z3_context c) { 778 Z3_TRY; 779 LOG_Z3_simplify_get_help(c); 780 RESET_ERROR_CODE(); 781 std::ostringstream buffer; 782 param_descrs descrs; 783 th_rewriter::get_param_descrs(descrs); 784 descrs.display(buffer); 785 return mk_c(c)->mk_external_string(buffer.str()); 786 Z3_CATCH_RETURN(""); 787 } 788 Z3_simplify_get_param_descrs(Z3_context c)789 Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(Z3_context c) { 790 Z3_TRY; 791 LOG_Z3_simplify_get_param_descrs(c); 792 RESET_ERROR_CODE(); 793 Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref, *mk_c(c)); 794 mk_c(c)->save_object(d); 795 th_rewriter::get_param_descrs(d->m_descrs); 796 Z3_param_descrs r = of_param_descrs(d); 797 RETURN_Z3(r); 798 Z3_CATCH_RETURN(nullptr); 799 } 800 Z3_update_term(Z3_context c,Z3_ast _a,unsigned num_args,Z3_ast const _args[])801 Z3_ast Z3_API Z3_update_term(Z3_context c, Z3_ast _a, unsigned num_args, Z3_ast const _args[]) { 802 Z3_TRY; 803 LOG_Z3_update_term(c, _a, num_args, _args); 804 RESET_ERROR_CODE(); 805 ast_manager& m = mk_c(c)->m(); 806 expr* a = to_expr(_a); 807 expr* const* args = to_exprs(num_args, _args); 808 switch(a->get_kind()) { 809 case AST_APP: { 810 app* e = to_app(a); 811 if (e->get_num_args() != num_args) { 812 SET_ERROR_CODE(Z3_IOB, nullptr); 813 } 814 else { 815 a = m.mk_app(e->get_decl(), num_args, args); 816 } 817 break; 818 } 819 case AST_QUANTIFIER: { 820 if (num_args != 1) { 821 SET_ERROR_CODE(Z3_IOB, nullptr); 822 } 823 else { 824 a = m.update_quantifier(to_quantifier(a), args[0]); 825 } 826 break; 827 } 828 default: 829 break; 830 } 831 mk_c(c)->save_ast_trail(a); 832 RETURN_Z3(of_expr(a)); 833 Z3_CATCH_RETURN(nullptr); 834 } 835 Z3_substitute(Z3_context c,Z3_ast _a,unsigned num_exprs,Z3_ast const _from[],Z3_ast const _to[])836 Z3_ast Z3_API Z3_substitute(Z3_context c, 837 Z3_ast _a, 838 unsigned num_exprs, 839 Z3_ast const _from[], 840 Z3_ast const _to[]) { 841 Z3_TRY; 842 LOG_Z3_substitute(c, _a, num_exprs, _from, _to); 843 RESET_ERROR_CODE(); 844 ast_manager & m = mk_c(c)->m(); 845 expr * a = to_expr(_a); 846 expr * const * from = to_exprs(num_exprs, _from); 847 expr * const * to = to_exprs(num_exprs, _to); 848 expr * r = nullptr; 849 for (unsigned i = 0; i < num_exprs; i++) { 850 if (m.get_sort(from[i]) != m.get_sort(to[i])) { 851 SET_ERROR_CODE(Z3_SORT_ERROR, nullptr); 852 RETURN_Z3(of_expr(nullptr)); 853 } 854 SASSERT(from[i]->get_ref_count() > 0); 855 SASSERT(to[i]->get_ref_count() > 0); 856 } 857 expr_safe_replace subst(m); 858 for (unsigned i = 0; i < num_exprs; i++) { 859 subst.insert(from[i], to[i]); 860 } 861 expr_ref new_a(m); 862 subst(a, new_a); 863 mk_c(c)->save_ast_trail(new_a); 864 r = new_a.get(); 865 RETURN_Z3(of_expr(r)); 866 Z3_CATCH_RETURN(nullptr); 867 } 868 Z3_substitute_vars(Z3_context c,Z3_ast _a,unsigned num_exprs,Z3_ast const _to[])869 Z3_ast Z3_API Z3_substitute_vars(Z3_context c, 870 Z3_ast _a, 871 unsigned num_exprs, 872 Z3_ast const _to[]) { 873 Z3_TRY; 874 LOG_Z3_substitute_vars(c, _a, num_exprs, _to); 875 RESET_ERROR_CODE(); 876 ast_manager & m = mk_c(c)->m(); 877 expr * a = to_expr(_a); 878 expr * const * to = to_exprs(num_exprs, _to); 879 var_subst subst(m, false); 880 expr_ref new_a = subst(a, num_exprs, to); 881 mk_c(c)->save_ast_trail(new_a); 882 RETURN_Z3(of_expr(new_a.get())); 883 Z3_CATCH_RETURN(nullptr); 884 } 885 Z3_ast_to_string(Z3_context c,Z3_ast a)886 Z3_API char const * Z3_ast_to_string(Z3_context c, Z3_ast a) { 887 Z3_TRY; 888 LOG_Z3_ast_to_string(c, a); 889 RESET_ERROR_CODE(); 890 std::ostringstream buffer; 891 switch (mk_c(c)->get_print_mode()) { 892 case Z3_PRINT_SMTLIB_FULL: { 893 params_ref p; 894 p.set_uint("max_depth", 4294967295u); 895 p.set_uint("min_alias_size", 4294967295u); 896 buffer << mk_pp(to_ast(a), mk_c(c)->m(), p); 897 break; 898 } 899 case Z3_PRINT_LOW_LEVEL: 900 buffer << mk_ll_pp(to_ast(a), mk_c(c)->m()); 901 break; 902 case Z3_PRINT_SMTLIB2_COMPLIANT: 903 buffer << mk_ismt2_pp(to_ast(a), mk_c(c)->m()); 904 break; 905 default: 906 UNREACHABLE(); 907 } 908 return mk_c(c)->mk_external_string(buffer.str()); 909 Z3_CATCH_RETURN(nullptr); 910 } 911 Z3_sort_to_string(Z3_context c,Z3_sort s)912 Z3_API char const * Z3_sort_to_string(Z3_context c, Z3_sort s) { 913 return Z3_ast_to_string(c, reinterpret_cast<Z3_ast>(s)); 914 } 915 Z3_func_decl_to_string(Z3_context c,Z3_func_decl f)916 Z3_API char const * Z3_func_decl_to_string(Z3_context c, Z3_func_decl f) { 917 return Z3_ast_to_string(c, reinterpret_cast<Z3_ast>(f)); 918 } 919 Z3_benchmark_to_smtlib_string(Z3_context c,Z3_string name,Z3_string logic,Z3_string status,Z3_string attributes,unsigned num_assumptions,Z3_ast const assumptions[],Z3_ast formula)920 Z3_string Z3_API Z3_benchmark_to_smtlib_string(Z3_context c, 921 Z3_string name, 922 Z3_string logic, 923 Z3_string status, 924 Z3_string attributes, 925 unsigned num_assumptions, 926 Z3_ast const assumptions[], 927 Z3_ast formula) { 928 Z3_TRY; 929 LOG_Z3_benchmark_to_smtlib_string(c, name, logic, status, attributes, num_assumptions, assumptions, formula); 930 RESET_ERROR_CODE(); 931 std::ostringstream buffer; 932 ast_smt_pp pp(mk_c(c)->m()); 933 pp.set_benchmark_name(name); 934 pp.set_logic(logic?symbol(logic):symbol::null); 935 pp.set_status(status); 936 pp.add_attributes(attributes); 937 pp_params params; 938 pp.set_simplify_implies(params.simplify_implies()); 939 for (unsigned i = 0; i < num_assumptions; ++i) { 940 pp.add_assumption(to_expr(assumptions[i])); 941 } 942 pp.display_smt2(buffer, to_expr(formula)); 943 return mk_c(c)->mk_external_string(buffer.str()); 944 Z3_CATCH_RETURN(""); 945 } 946 Z3_get_decl_kind(Z3_context c,Z3_func_decl d)947 Z3_decl_kind Z3_API Z3_get_decl_kind(Z3_context c, Z3_func_decl d) { 948 Z3_TRY; 949 LOG_Z3_get_decl_kind(c, d); 950 RESET_ERROR_CODE(); 951 func_decl* _d = to_func_decl(d); 952 953 if (d == nullptr || null_family_id == _d->get_family_id()) { 954 return Z3_OP_UNINTERPRETED; 955 } 956 if (mk_c(c)->get_basic_fid() == _d->get_family_id()) { 957 switch(_d->get_decl_kind()) { 958 case OP_TRUE: return Z3_OP_TRUE; 959 case OP_FALSE: return Z3_OP_FALSE; 960 case OP_EQ: return Z3_OP_EQ; 961 case OP_DISTINCT: return Z3_OP_DISTINCT; 962 case OP_ITE: return Z3_OP_ITE; 963 case OP_AND: return Z3_OP_AND; 964 case OP_OR: return Z3_OP_OR; 965 case OP_XOR: return Z3_OP_XOR; 966 case OP_NOT: return Z3_OP_NOT; 967 case OP_IMPLIES: return Z3_OP_IMPLIES; 968 case OP_OEQ: return Z3_OP_OEQ; 969 970 case PR_UNDEF: return Z3_OP_PR_UNDEF; 971 case PR_TRUE: return Z3_OP_PR_TRUE; 972 case PR_ASSERTED: return Z3_OP_PR_ASSERTED; 973 case PR_GOAL: return Z3_OP_PR_GOAL; 974 case PR_MODUS_PONENS: return Z3_OP_PR_MODUS_PONENS; 975 case PR_REFLEXIVITY: return Z3_OP_PR_REFLEXIVITY; 976 case PR_SYMMETRY: return Z3_OP_PR_SYMMETRY; 977 case PR_TRANSITIVITY: return Z3_OP_PR_TRANSITIVITY; 978 case PR_TRANSITIVITY_STAR: return Z3_OP_PR_TRANSITIVITY_STAR; 979 case PR_MONOTONICITY: return Z3_OP_PR_MONOTONICITY; 980 case PR_QUANT_INTRO: return Z3_OP_PR_QUANT_INTRO; 981 case PR_BIND: return Z3_OP_PR_BIND; 982 case PR_DISTRIBUTIVITY: return Z3_OP_PR_DISTRIBUTIVITY; 983 case PR_AND_ELIM: return Z3_OP_PR_AND_ELIM; 984 case PR_NOT_OR_ELIM: return Z3_OP_PR_NOT_OR_ELIM; 985 case PR_REWRITE: return Z3_OP_PR_REWRITE; 986 case PR_REWRITE_STAR: return Z3_OP_PR_REWRITE_STAR; 987 case PR_PULL_QUANT: return Z3_OP_PR_PULL_QUANT; 988 case PR_PUSH_QUANT: return Z3_OP_PR_PUSH_QUANT; 989 case PR_ELIM_UNUSED_VARS: return Z3_OP_PR_ELIM_UNUSED_VARS; 990 case PR_DER: return Z3_OP_PR_DER; 991 case PR_QUANT_INST: return Z3_OP_PR_QUANT_INST; 992 case PR_HYPOTHESIS: return Z3_OP_PR_HYPOTHESIS; 993 case PR_LEMMA: return Z3_OP_PR_LEMMA; 994 case PR_UNIT_RESOLUTION: return Z3_OP_PR_UNIT_RESOLUTION; 995 case PR_IFF_TRUE: return Z3_OP_PR_IFF_TRUE; 996 case PR_IFF_FALSE: return Z3_OP_PR_IFF_FALSE; 997 case PR_COMMUTATIVITY: return Z3_OP_PR_COMMUTATIVITY; 998 case PR_DEF_AXIOM: return Z3_OP_PR_DEF_AXIOM; 999 case PR_ASSUMPTION_ADD: return Z3_OP_PR_ASSUMPTION_ADD; 1000 case PR_LEMMA_ADD: return Z3_OP_PR_LEMMA_ADD; 1001 case PR_REDUNDANT_DEL: return Z3_OP_PR_REDUNDANT_DEL; 1002 case PR_CLAUSE_TRAIL: return Z3_OP_PR_CLAUSE_TRAIL; 1003 case PR_DEF_INTRO: return Z3_OP_PR_DEF_INTRO; 1004 case PR_APPLY_DEF: return Z3_OP_PR_APPLY_DEF; 1005 case PR_IFF_OEQ: return Z3_OP_PR_IFF_OEQ; 1006 case PR_NNF_POS: return Z3_OP_PR_NNF_POS; 1007 case PR_NNF_NEG: return Z3_OP_PR_NNF_NEG; 1008 case PR_SKOLEMIZE: return Z3_OP_PR_SKOLEMIZE; 1009 case PR_MODUS_PONENS_OEQ: return Z3_OP_PR_MODUS_PONENS_OEQ; 1010 case PR_TH_LEMMA: return Z3_OP_PR_TH_LEMMA; 1011 case PR_HYPER_RESOLVE: return Z3_OP_PR_HYPER_RESOLVE; 1012 default: 1013 return Z3_OP_INTERNAL; 1014 } 1015 } 1016 if (mk_c(c)->get_arith_fid() == _d->get_family_id()) { 1017 switch(_d->get_decl_kind()) { 1018 case OP_NUM: return Z3_OP_ANUM; 1019 case OP_IRRATIONAL_ALGEBRAIC_NUM: return Z3_OP_AGNUM; 1020 case OP_LE: return Z3_OP_LE; 1021 case OP_GE: return Z3_OP_GE; 1022 case OP_LT: return Z3_OP_LT; 1023 case OP_GT: return Z3_OP_GT; 1024 case OP_ADD: return Z3_OP_ADD; 1025 case OP_SUB: return Z3_OP_SUB; 1026 case OP_UMINUS: return Z3_OP_UMINUS; 1027 case OP_MUL: return Z3_OP_MUL; 1028 case OP_DIV: return Z3_OP_DIV; 1029 case OP_IDIV: return Z3_OP_IDIV; 1030 case OP_REM: return Z3_OP_REM; 1031 case OP_MOD: return Z3_OP_MOD; 1032 case OP_POWER: return Z3_OP_POWER; 1033 case OP_TO_REAL: return Z3_OP_TO_REAL; 1034 case OP_TO_INT: return Z3_OP_TO_INT; 1035 case OP_IS_INT: return Z3_OP_IS_INT; 1036 default: 1037 return Z3_OP_INTERNAL; 1038 } 1039 } 1040 if (mk_c(c)->get_array_fid() == _d->get_family_id()) { 1041 switch(_d->get_decl_kind()) { 1042 case OP_STORE: return Z3_OP_STORE; 1043 case OP_SELECT: return Z3_OP_SELECT; 1044 case OP_CONST_ARRAY: return Z3_OP_CONST_ARRAY; 1045 case OP_ARRAY_DEFAULT: return Z3_OP_ARRAY_DEFAULT; 1046 case OP_ARRAY_MAP: return Z3_OP_ARRAY_MAP; 1047 case OP_SET_UNION: return Z3_OP_SET_UNION; 1048 case OP_SET_INTERSECT: return Z3_OP_SET_INTERSECT; 1049 case OP_SET_DIFFERENCE: return Z3_OP_SET_DIFFERENCE; 1050 case OP_SET_COMPLEMENT: return Z3_OP_SET_COMPLEMENT; 1051 case OP_SET_SUBSET: return Z3_OP_SET_SUBSET; 1052 case OP_AS_ARRAY: return Z3_OP_AS_ARRAY; 1053 case OP_ARRAY_EXT: return Z3_OP_ARRAY_EXT; 1054 case OP_SET_CARD: return Z3_OP_SET_CARD; 1055 case OP_SET_HAS_SIZE: return Z3_OP_SET_HAS_SIZE; 1056 default: 1057 return Z3_OP_INTERNAL; 1058 } 1059 } 1060 1061 if (mk_c(c)->get_special_relations_fid() == _d->get_family_id()) { 1062 switch(_d->get_decl_kind()) { 1063 case OP_SPECIAL_RELATION_LO : return Z3_OP_SPECIAL_RELATION_LO; 1064 case OP_SPECIAL_RELATION_PO : return Z3_OP_SPECIAL_RELATION_PO; 1065 case OP_SPECIAL_RELATION_PLO: return Z3_OP_SPECIAL_RELATION_PLO; 1066 case OP_SPECIAL_RELATION_TO : return Z3_OP_SPECIAL_RELATION_TO; 1067 case OP_SPECIAL_RELATION_TC : return Z3_OP_SPECIAL_RELATION_TC; 1068 default: UNREACHABLE(); 1069 } 1070 } 1071 1072 1073 if (mk_c(c)->get_bv_fid() == _d->get_family_id()) { 1074 switch(_d->get_decl_kind()) { 1075 case OP_BV_NUM: return Z3_OP_BNUM; 1076 case OP_BIT1: return Z3_OP_BIT1; 1077 case OP_BIT0: return Z3_OP_BIT0; 1078 case OP_BNEG: return Z3_OP_BNEG; 1079 case OP_BADD: return Z3_OP_BADD; 1080 case OP_BSUB: return Z3_OP_BSUB; 1081 case OP_BMUL: return Z3_OP_BMUL; 1082 case OP_BSDIV: return Z3_OP_BSDIV; 1083 case OP_BUDIV: return Z3_OP_BUDIV; 1084 case OP_BSREM: return Z3_OP_BSREM; 1085 case OP_BUREM: return Z3_OP_BUREM; 1086 case OP_BSMOD: return Z3_OP_BSMOD; 1087 case OP_BSDIV0: return Z3_OP_BSDIV0; 1088 case OP_BUDIV0: return Z3_OP_BUDIV0; 1089 case OP_BSREM0: return Z3_OP_BUREM0; 1090 case OP_BUREM0: return Z3_OP_BUREM0; 1091 case OP_BSMOD0: return Z3_OP_BSMOD0; 1092 case OP_ULEQ: return Z3_OP_ULEQ; 1093 case OP_SLEQ: return Z3_OP_SLEQ; 1094 case OP_UGEQ: return Z3_OP_UGEQ; 1095 case OP_SGEQ: return Z3_OP_SGEQ; 1096 case OP_ULT: return Z3_OP_ULT; 1097 case OP_SLT: return Z3_OP_SLT; 1098 case OP_UGT: return Z3_OP_UGT; 1099 case OP_SGT: return Z3_OP_SGT; 1100 case OP_BAND: return Z3_OP_BAND; 1101 case OP_BOR: return Z3_OP_BOR; 1102 case OP_BNOT: return Z3_OP_BNOT; 1103 case OP_BXOR: return Z3_OP_BXOR; 1104 case OP_BNAND: return Z3_OP_BNAND; 1105 case OP_BNOR: return Z3_OP_BNOR; 1106 case OP_BXNOR: return Z3_OP_BXNOR; 1107 case OP_CONCAT: return Z3_OP_CONCAT; 1108 case OP_SIGN_EXT: return Z3_OP_SIGN_EXT; 1109 case OP_ZERO_EXT: return Z3_OP_ZERO_EXT; 1110 case OP_EXTRACT: return Z3_OP_EXTRACT; 1111 case OP_REPEAT: return Z3_OP_REPEAT; 1112 case OP_BREDOR: return Z3_OP_BREDOR; 1113 case OP_BREDAND: return Z3_OP_BREDAND; 1114 case OP_BCOMP: return Z3_OP_BCOMP; 1115 case OP_BSHL: return Z3_OP_BSHL; 1116 case OP_BLSHR: return Z3_OP_BLSHR; 1117 case OP_BASHR: return Z3_OP_BASHR; 1118 case OP_ROTATE_LEFT: return Z3_OP_ROTATE_LEFT; 1119 case OP_ROTATE_RIGHT: return Z3_OP_ROTATE_RIGHT; 1120 case OP_EXT_ROTATE_LEFT: return Z3_OP_EXT_ROTATE_LEFT; 1121 case OP_EXT_ROTATE_RIGHT: return Z3_OP_EXT_ROTATE_RIGHT; 1122 case OP_INT2BV: return Z3_OP_INT2BV; 1123 case OP_BV2INT: return Z3_OP_BV2INT; 1124 case OP_CARRY: return Z3_OP_CARRY; 1125 case OP_XOR3: return Z3_OP_XOR3; 1126 case OP_BIT2BOOL: return Z3_OP_BIT2BOOL; 1127 case OP_BSMUL_NO_OVFL: return Z3_OP_BSMUL_NO_OVFL; 1128 case OP_BUMUL_NO_OVFL: return Z3_OP_BUMUL_NO_OVFL; 1129 case OP_BSMUL_NO_UDFL: return Z3_OP_BSMUL_NO_UDFL; 1130 case OP_BSDIV_I: return Z3_OP_BSDIV_I; 1131 case OP_BUDIV_I: return Z3_OP_BUDIV_I; 1132 case OP_BSREM_I: return Z3_OP_BSREM_I; 1133 case OP_BUREM_I: return Z3_OP_BUREM_I; 1134 case OP_BSMOD_I: return Z3_OP_BSMOD_I; 1135 default: 1136 return Z3_OP_INTERNAL; 1137 } 1138 } 1139 if (mk_c(c)->get_dt_fid() == _d->get_family_id()) { 1140 switch(_d->get_decl_kind()) { 1141 case OP_DT_CONSTRUCTOR: return Z3_OP_DT_CONSTRUCTOR; 1142 case OP_DT_RECOGNISER: return Z3_OP_DT_RECOGNISER; 1143 case OP_DT_IS: return Z3_OP_DT_IS; 1144 case OP_DT_ACCESSOR: return Z3_OP_DT_ACCESSOR; 1145 case OP_DT_UPDATE_FIELD: return Z3_OP_DT_UPDATE_FIELD; 1146 default: 1147 return Z3_OP_INTERNAL; 1148 } 1149 } 1150 if (mk_c(c)->get_datalog_fid() == _d->get_family_id()) { 1151 switch(_d->get_decl_kind()) { 1152 case datalog::OP_RA_STORE: return Z3_OP_RA_STORE; 1153 case datalog::OP_RA_EMPTY: return Z3_OP_RA_EMPTY; 1154 case datalog::OP_RA_IS_EMPTY: return Z3_OP_RA_IS_EMPTY; 1155 case datalog::OP_RA_JOIN: return Z3_OP_RA_JOIN; 1156 case datalog::OP_RA_UNION: return Z3_OP_RA_UNION; 1157 case datalog::OP_RA_WIDEN: return Z3_OP_RA_WIDEN; 1158 case datalog::OP_RA_PROJECT: return Z3_OP_RA_PROJECT; 1159 case datalog::OP_RA_FILTER: return Z3_OP_RA_FILTER; 1160 case datalog::OP_RA_NEGATION_FILTER: return Z3_OP_RA_NEGATION_FILTER; 1161 case datalog::OP_RA_RENAME: return Z3_OP_RA_RENAME; 1162 case datalog::OP_RA_COMPLEMENT: return Z3_OP_RA_COMPLEMENT; 1163 case datalog::OP_RA_SELECT: return Z3_OP_RA_SELECT; 1164 case datalog::OP_RA_CLONE: return Z3_OP_RA_CLONE; 1165 case datalog::OP_DL_CONSTANT: return Z3_OP_FD_CONSTANT; 1166 case datalog::OP_DL_LT: return Z3_OP_FD_LT; 1167 default: 1168 return Z3_OP_INTERNAL; 1169 } 1170 } 1171 1172 if (mk_c(c)->get_seq_fid() == _d->get_family_id()) { 1173 switch (_d->get_decl_kind()) { 1174 case OP_SEQ_UNIT: return Z3_OP_SEQ_UNIT; 1175 case OP_SEQ_EMPTY: return Z3_OP_SEQ_EMPTY; 1176 case OP_SEQ_CONCAT: return Z3_OP_SEQ_CONCAT; 1177 case OP_SEQ_PREFIX: return Z3_OP_SEQ_PREFIX; 1178 case OP_SEQ_SUFFIX: return Z3_OP_SEQ_SUFFIX; 1179 case OP_SEQ_CONTAINS: return Z3_OP_SEQ_CONTAINS; 1180 case OP_SEQ_EXTRACT: return Z3_OP_SEQ_EXTRACT; 1181 case OP_SEQ_REPLACE: return Z3_OP_SEQ_REPLACE; 1182 case OP_SEQ_AT: return Z3_OP_SEQ_AT; 1183 case OP_SEQ_NTH: return Z3_OP_SEQ_NTH; 1184 case OP_SEQ_LENGTH: return Z3_OP_SEQ_LENGTH; 1185 case OP_SEQ_INDEX: return Z3_OP_SEQ_INDEX; 1186 case OP_SEQ_TO_RE: return Z3_OP_SEQ_TO_RE; 1187 case OP_SEQ_IN_RE: return Z3_OP_SEQ_IN_RE; 1188 1189 case _OP_STRING_STRREPL: return Z3_OP_SEQ_REPLACE; 1190 case _OP_STRING_CONCAT: return Z3_OP_SEQ_CONCAT; 1191 case _OP_STRING_LENGTH: return Z3_OP_SEQ_LENGTH; 1192 case _OP_STRING_STRCTN: return Z3_OP_SEQ_CONTAINS; 1193 case _OP_STRING_PREFIX: return Z3_OP_SEQ_PREFIX; 1194 case _OP_STRING_SUFFIX: return Z3_OP_SEQ_SUFFIX; 1195 case _OP_STRING_IN_REGEXP: return Z3_OP_SEQ_IN_RE; 1196 case _OP_STRING_TO_REGEXP: return Z3_OP_SEQ_TO_RE; 1197 case _OP_STRING_CHARAT: return Z3_OP_SEQ_AT; 1198 case _OP_STRING_SUBSTR: return Z3_OP_SEQ_EXTRACT; 1199 case _OP_STRING_STRIDOF: return Z3_OP_SEQ_INDEX; 1200 case _OP_REGEXP_EMPTY: return Z3_OP_RE_EMPTY_SET; 1201 case _OP_REGEXP_FULL_CHAR: return Z3_OP_RE_FULL_SET; 1202 1203 case OP_STRING_STOI: return Z3_OP_STR_TO_INT; 1204 case OP_STRING_ITOS: return Z3_OP_INT_TO_STR; 1205 case OP_STRING_LT: return Z3_OP_STRING_LT; 1206 case OP_STRING_LE: return Z3_OP_STRING_LE; 1207 1208 case OP_RE_PLUS: return Z3_OP_RE_PLUS; 1209 case OP_RE_STAR: return Z3_OP_RE_STAR; 1210 case OP_RE_OPTION: return Z3_OP_RE_OPTION; 1211 case OP_RE_CONCAT: return Z3_OP_RE_CONCAT; 1212 case OP_RE_UNION: return Z3_OP_RE_UNION; 1213 case OP_RE_INTERSECT: return Z3_OP_RE_INTERSECT; 1214 case OP_RE_LOOP: return Z3_OP_RE_LOOP; 1215 case OP_RE_FULL_SEQ_SET: return Z3_OP_RE_FULL_SET; 1216 //case OP_RE_FULL_CHAR_SET: return Z3_OP_RE_FULL_SET; 1217 case OP_RE_EMPTY_SET: return Z3_OP_RE_EMPTY_SET; 1218 default: 1219 return Z3_OP_INTERNAL; 1220 } 1221 } 1222 1223 if (mk_c(c)->get_fpa_fid() == _d->get_family_id()) { 1224 switch (_d->get_decl_kind()) { 1225 case OP_FPA_RM_NEAREST_TIES_TO_EVEN: return Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; 1226 case OP_FPA_RM_NEAREST_TIES_TO_AWAY: return Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; 1227 case OP_FPA_RM_TOWARD_POSITIVE: return Z3_OP_FPA_RM_TOWARD_POSITIVE; 1228 case OP_FPA_RM_TOWARD_NEGATIVE: return Z3_OP_FPA_RM_TOWARD_NEGATIVE; 1229 case OP_FPA_RM_TOWARD_ZERO: return Z3_OP_FPA_RM_TOWARD_ZERO; 1230 case OP_FPA_NUM: return Z3_OP_FPA_NUM; 1231 case OP_FPA_PLUS_INF: return Z3_OP_FPA_PLUS_INF; 1232 case OP_FPA_MINUS_INF: return Z3_OP_FPA_MINUS_INF; 1233 case OP_FPA_NAN: return Z3_OP_FPA_NAN; 1234 case OP_FPA_MINUS_ZERO: return Z3_OP_FPA_MINUS_ZERO; 1235 case OP_FPA_PLUS_ZERO: return Z3_OP_FPA_PLUS_ZERO; 1236 case OP_FPA_ADD: return Z3_OP_FPA_ADD; 1237 case OP_FPA_SUB: return Z3_OP_FPA_SUB; 1238 case OP_FPA_NEG: return Z3_OP_FPA_NEG; 1239 case OP_FPA_MUL: return Z3_OP_FPA_MUL; 1240 case OP_FPA_DIV: return Z3_OP_FPA_DIV; 1241 case OP_FPA_REM: return Z3_OP_FPA_REM; 1242 case OP_FPA_ABS: return Z3_OP_FPA_ABS; 1243 case OP_FPA_MIN: return Z3_OP_FPA_MIN; 1244 case OP_FPA_MAX: return Z3_OP_FPA_MAX; 1245 case OP_FPA_FMA: return Z3_OP_FPA_FMA; 1246 case OP_FPA_SQRT: return Z3_OP_FPA_SQRT; 1247 case OP_FPA_EQ: return Z3_OP_FPA_EQ; 1248 case OP_FPA_ROUND_TO_INTEGRAL: return Z3_OP_FPA_ROUND_TO_INTEGRAL; 1249 case OP_FPA_LT: return Z3_OP_FPA_LT; 1250 case OP_FPA_GT: return Z3_OP_FPA_GT; 1251 case OP_FPA_LE: return Z3_OP_FPA_LE; 1252 case OP_FPA_GE: return Z3_OP_FPA_GE; 1253 case OP_FPA_IS_NAN: return Z3_OP_FPA_IS_NAN; 1254 case OP_FPA_IS_INF: return Z3_OP_FPA_IS_INF; 1255 case OP_FPA_IS_ZERO: return Z3_OP_FPA_IS_ZERO; 1256 case OP_FPA_IS_NORMAL: return Z3_OP_FPA_IS_NORMAL; 1257 case OP_FPA_IS_SUBNORMAL: return Z3_OP_FPA_IS_SUBNORMAL; 1258 case OP_FPA_IS_NEGATIVE: return Z3_OP_FPA_IS_NEGATIVE; 1259 case OP_FPA_IS_POSITIVE: return Z3_OP_FPA_IS_POSITIVE; 1260 case OP_FPA_FP: return Z3_OP_FPA_FP; 1261 case OP_FPA_TO_FP: return Z3_OP_FPA_TO_FP; 1262 case OP_FPA_TO_FP_UNSIGNED: return Z3_OP_FPA_TO_FP_UNSIGNED; 1263 case OP_FPA_TO_UBV: return Z3_OP_FPA_TO_UBV; 1264 case OP_FPA_TO_SBV: return Z3_OP_FPA_TO_SBV; 1265 case OP_FPA_TO_REAL: return Z3_OP_FPA_TO_REAL; 1266 case OP_FPA_TO_IEEE_BV: return Z3_OP_FPA_TO_IEEE_BV; 1267 case OP_FPA_BVWRAP: return Z3_OP_FPA_BVWRAP; 1268 case OP_FPA_BV2RM: return Z3_OP_FPA_BV2RM; 1269 return Z3_OP_UNINTERPRETED; 1270 default: 1271 return Z3_OP_INTERNAL; 1272 } 1273 } 1274 1275 if (mk_c(c)->m().get_label_family_id() == _d->get_family_id()) { 1276 switch(_d->get_decl_kind()) { 1277 case OP_LABEL: return Z3_OP_LABEL; 1278 case OP_LABEL_LIT: return Z3_OP_LABEL_LIT; 1279 default: 1280 return Z3_OP_INTERNAL; 1281 } 1282 } 1283 1284 if (mk_c(c)->get_pb_fid() == _d->get_family_id()) { 1285 switch(_d->get_decl_kind()) { 1286 case OP_PB_LE: return Z3_OP_PB_LE; 1287 case OP_PB_GE: return Z3_OP_PB_GE; 1288 case OP_PB_EQ: return Z3_OP_PB_EQ; 1289 case OP_AT_MOST_K: return Z3_OP_PB_AT_MOST; 1290 case OP_AT_LEAST_K: return Z3_OP_PB_AT_LEAST; 1291 default: return Z3_OP_INTERNAL; 1292 } 1293 } 1294 1295 return Z3_OP_UNINTERPRETED; 1296 Z3_CATCH_RETURN(Z3_OP_UNINTERPRETED); 1297 } 1298 Z3_get_index_value(Z3_context c,Z3_ast a)1299 unsigned Z3_API Z3_get_index_value(Z3_context c, Z3_ast a) { 1300 Z3_TRY; 1301 LOG_Z3_get_index_value(c, a); 1302 RESET_ERROR_CODE(); 1303 ast* _a = reinterpret_cast<ast*>(a); 1304 if (!_a || _a->get_kind() != AST_VAR) { 1305 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 1306 return 0; 1307 } 1308 var* va = to_var(_a); 1309 if (va) { 1310 return va->get_idx(); 1311 } 1312 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 1313 return 0; 1314 Z3_CATCH_RETURN(0); 1315 } 1316 Z3_translate(Z3_context c,Z3_ast a,Z3_context target)1317 Z3_ast Z3_API Z3_translate(Z3_context c, Z3_ast a, Z3_context target) { 1318 Z3_TRY; 1319 LOG_Z3_translate(c, a, target); 1320 RESET_ERROR_CODE(); 1321 CHECK_VALID_AST(a, nullptr); 1322 if (c == target) { 1323 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 1324 RETURN_Z3(nullptr); 1325 } 1326 SASSERT(mk_c(c)->m().contains(to_ast(a))); 1327 ast_translation translator(mk_c(c)->m(), mk_c(target)->m()); 1328 ast * _result = translator(to_ast(a)); 1329 mk_c(target)->save_ast_trail(_result); 1330 RETURN_Z3(of_ast(_result)); 1331 Z3_CATCH_RETURN(nullptr); 1332 } 1333 1334 }; 1335