1 /*++ 2 Copyright (c) 2012 Microsoft Corporation 3 4 Module Name: 5 6 api_datatype.cpp 7 8 Abstract: 9 API for datatype theory 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 "ast/datatype_decl_plugin.h" 23 24 extern "C" { 25 Z3_mk_tuple_sort(Z3_context c,Z3_symbol name,unsigned num_fields,Z3_symbol const field_names[],Z3_sort const field_sorts[],Z3_func_decl * mk_tuple_decl,Z3_func_decl proj_decls[])26 Z3_sort Z3_API Z3_mk_tuple_sort(Z3_context c, 27 Z3_symbol name, 28 unsigned num_fields, 29 Z3_symbol const field_names[], 30 Z3_sort const field_sorts[], 31 Z3_func_decl * mk_tuple_decl, 32 Z3_func_decl proj_decls[]) { 33 Z3_TRY; 34 LOG_Z3_mk_tuple_sort(c, name, num_fields, field_names, field_sorts, mk_tuple_decl, proj_decls); 35 RESET_ERROR_CODE(); 36 mk_c(c)->reset_last_result(); 37 ast_manager& m = mk_c(c)->m(); 38 datatype_util& dt_util = mk_c(c)->dtutil(); 39 40 sort_ref_vector tuples(m); 41 sort* tuple; 42 std::string recognizer_s("is_"); 43 recognizer_s += to_symbol(name).str(); 44 symbol recognizer(recognizer_s.c_str()); 45 46 ptr_vector<accessor_decl> acc; 47 for (unsigned i = 0; i < num_fields; ++i) { 48 acc.push_back(mk_accessor_decl(m, to_symbol(field_names[i]), type_ref(to_sort(field_sorts[i])))); 49 } 50 51 constructor_decl* constrs[1] = { mk_constructor_decl(to_symbol(name), recognizer, acc.size(), acc.c_ptr()) }; 52 53 { 54 datatype_decl * dt = mk_datatype_decl(dt_util, to_symbol(name), 0, nullptr, 1, constrs); 55 bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &dt, 0, nullptr, tuples); 56 del_datatype_decl(dt); 57 58 if (!is_ok) { 59 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 60 RETURN_Z3(nullptr); 61 } 62 } 63 64 // create tuple type 65 SASSERT(tuples.size() == 1); 66 tuple = tuples[0].get(); 67 mk_c(c)->save_multiple_ast_trail(tuple); 68 69 // create constructor 70 SASSERT(dt_util.is_datatype(tuple)); 71 SASSERT(!dt_util.is_recursive(tuple)); 72 ptr_vector<func_decl> const & decls = *dt_util.get_datatype_constructors(tuple); 73 func_decl* decl = (decls)[0]; 74 mk_c(c)->save_multiple_ast_trail(decl); 75 *mk_tuple_decl = of_func_decl(decl); 76 77 // Create projections 78 ptr_vector<func_decl> const & _accs = *dt_util.get_constructor_accessors(decl); 79 SASSERT(_accs.size() == num_fields); 80 for (unsigned i = 0; i < _accs.size(); i++) { 81 mk_c(c)->save_multiple_ast_trail(_accs[i]); 82 proj_decls[i] = of_func_decl(_accs[i]); 83 } 84 RETURN_Z3_mk_tuple_sort(of_sort(tuple)); 85 Z3_CATCH_RETURN(nullptr); 86 } 87 Z3_mk_enumeration_sort(Z3_context c,Z3_symbol name,unsigned n,Z3_symbol const enum_names[],Z3_func_decl enum_consts[],Z3_func_decl enum_testers[])88 Z3_sort Z3_API Z3_mk_enumeration_sort(Z3_context c, 89 Z3_symbol name, 90 unsigned n, 91 Z3_symbol const enum_names[], 92 Z3_func_decl enum_consts[], 93 Z3_func_decl enum_testers[]) { 94 Z3_TRY; 95 LOG_Z3_mk_enumeration_sort(c, name, n, enum_names, enum_consts, enum_testers); 96 RESET_ERROR_CODE(); 97 mk_c(c)->reset_last_result(); 98 ast_manager& m = mk_c(c)->m(); 99 datatype_util& dt_util = mk_c(c)->dtutil(); 100 101 sort_ref_vector sorts(m); 102 sort* e; 103 104 ptr_vector<constructor_decl> constrs; 105 for (unsigned i = 0; i < n; ++i) { 106 symbol e_name(to_symbol(enum_names[i])); 107 std::string recognizer_s("is_"); 108 recognizer_s += e_name.str(); 109 symbol recognizer(recognizer_s.c_str()); 110 111 constrs.push_back(mk_constructor_decl(e_name, recognizer, 0, nullptr)); 112 } 113 114 115 { 116 datatype_decl * dt = mk_datatype_decl(dt_util, to_symbol(name), 0, nullptr, n, constrs.c_ptr()); 117 bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &dt, 0, nullptr, sorts); 118 del_datatype_decl(dt); 119 120 if (!is_ok) { 121 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 122 RETURN_Z3(nullptr); 123 } 124 } 125 126 // create enum type. 127 SASSERT(sorts.size() == 1); 128 e = sorts[0].get(); 129 mk_c(c)->save_multiple_ast_trail(e); 130 131 // create constructor 132 SASSERT(dt_util.is_datatype(e)); 133 SASSERT(!dt_util.is_recursive(e)); 134 ptr_vector<func_decl> const & decls = *dt_util.get_datatype_constructors(e); 135 SASSERT(decls.size() == n); 136 for (unsigned i = 0; i < n; ++i) { 137 func_decl* decl = (decls)[i]; 138 mk_c(c)->save_multiple_ast_trail(decl); 139 enum_consts[i] = of_func_decl(decl); 140 decl = dt_util.get_constructor_is(decl); 141 mk_c(c)->save_multiple_ast_trail(decl); 142 enum_testers[i] = of_func_decl(decl); 143 } 144 145 RETURN_Z3_mk_enumeration_sort(of_sort(e)); 146 Z3_CATCH_RETURN(nullptr); 147 } 148 Z3_mk_list_sort(Z3_context c,Z3_symbol name,Z3_sort elem_sort,Z3_func_decl * nil_decl,Z3_func_decl * is_nil_decl,Z3_func_decl * cons_decl,Z3_func_decl * is_cons_decl,Z3_func_decl * head_decl,Z3_func_decl * tail_decl)149 Z3_sort Z3_API Z3_mk_list_sort(Z3_context c, 150 Z3_symbol name, 151 Z3_sort elem_sort, 152 Z3_func_decl* nil_decl, 153 Z3_func_decl* is_nil_decl, 154 Z3_func_decl* cons_decl, 155 Z3_func_decl* is_cons_decl, 156 Z3_func_decl* head_decl, 157 Z3_func_decl* tail_decl 158 ) { 159 Z3_TRY; 160 LOG_Z3_mk_list_sort(c, name, elem_sort, nil_decl, is_nil_decl, cons_decl, is_cons_decl, head_decl, tail_decl); 161 RESET_ERROR_CODE(); 162 ast_manager& m = mk_c(c)->m(); 163 func_decl_ref nil(m), is_nil(m), cons(m), is_cons(m), head(m), tail(m); 164 datatype_util& dt_util = mk_c(c)->dtutil(); 165 mk_c(c)->reset_last_result(); 166 sort_ref s = dt_util.mk_list_datatype(to_sort(elem_sort), to_symbol(name), cons, is_cons, head, tail, nil, is_nil); 167 168 if (!s) { 169 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 170 RETURN_Z3(nullptr); 171 } 172 173 mk_c(c)->save_multiple_ast_trail(s); 174 if (nil_decl) { 175 mk_c(c)->save_multiple_ast_trail(nil); 176 *nil_decl = of_func_decl(nil); 177 } 178 if (is_nil_decl) { 179 mk_c(c)->save_multiple_ast_trail(is_nil); 180 *is_nil_decl = of_func_decl(is_nil); 181 } 182 if (cons_decl) { 183 mk_c(c)->save_multiple_ast_trail(cons); 184 *cons_decl = of_func_decl(cons); 185 } 186 if (is_cons_decl) { 187 mk_c(c)->save_multiple_ast_trail(is_cons); 188 *is_cons_decl = of_func_decl(is_cons); 189 } 190 if (head_decl) { 191 mk_c(c)->save_multiple_ast_trail(head); 192 *head_decl = of_func_decl(head); 193 } 194 if (tail_decl) { 195 mk_c(c)->save_multiple_ast_trail(tail); 196 *tail_decl = of_func_decl(tail); 197 } 198 RETURN_Z3_mk_list_sort(of_sort(s)); 199 Z3_CATCH_RETURN(nullptr); 200 } 201 202 struct constructor { 203 symbol m_name; 204 symbol m_tester; 205 svector<symbol> m_field_names; 206 sort_ref_vector m_sorts; 207 unsigned_vector m_sort_refs; 208 func_decl_ref m_constructor; constructorconstructor209 constructor(ast_manager& m) : m_sorts(m), m_constructor(m) {} 210 }; 211 Z3_mk_constructor(Z3_context c,Z3_symbol name,Z3_symbol tester,unsigned num_fields,Z3_symbol const field_names[],Z3_sort const sorts[],unsigned sort_refs[])212 Z3_constructor Z3_API Z3_mk_constructor(Z3_context c, 213 Z3_symbol name, 214 Z3_symbol tester, 215 unsigned num_fields, 216 Z3_symbol const field_names[], 217 Z3_sort const sorts[], 218 unsigned sort_refs[] 219 ) { 220 Z3_TRY; 221 LOG_Z3_mk_constructor(c, name, tester, num_fields, field_names, sorts, sort_refs); 222 RESET_ERROR_CODE(); 223 ast_manager& m = mk_c(c)->m(); 224 constructor* cnstr = alloc(constructor, m); 225 cnstr->m_name = to_symbol(name); 226 cnstr->m_tester = to_symbol(tester); 227 for (unsigned i = 0; i < num_fields; ++i) { 228 cnstr->m_field_names.push_back(to_symbol(field_names[i])); 229 cnstr->m_sorts.push_back(to_sort(sorts[i])); 230 cnstr->m_sort_refs.push_back(sort_refs[i]); 231 } 232 RETURN_Z3(reinterpret_cast<Z3_constructor>(cnstr)); 233 Z3_CATCH_RETURN(nullptr); 234 } 235 236 Z3_query_constructor(Z3_context c,Z3_constructor constr,unsigned num_fields,Z3_func_decl * constructor_decl,Z3_func_decl * tester,Z3_func_decl accessors[])237 void Z3_API Z3_query_constructor(Z3_context c, 238 Z3_constructor constr, 239 unsigned num_fields, 240 Z3_func_decl* constructor_decl, 241 Z3_func_decl* tester, 242 Z3_func_decl accessors[]) { 243 Z3_TRY; 244 LOG_Z3_query_constructor(c, constr, num_fields, constructor_decl, tester, accessors); 245 RESET_ERROR_CODE(); 246 mk_c(c)->reset_last_result(); 247 if (!constr) { 248 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 249 return; 250 } 251 ast_manager& m = mk_c(c)->m(); 252 datatype_util data_util(m); 253 func_decl* f = reinterpret_cast<constructor*>(constr)->m_constructor.get(); 254 255 if (!f) { 256 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 257 return; 258 } 259 if (constructor_decl) { 260 mk_c(c)->save_multiple_ast_trail(f); 261 *constructor_decl = of_func_decl(f); 262 } 263 if (tester) { 264 func_decl* f2 = data_util.get_constructor_is(f); 265 mk_c(c)->save_multiple_ast_trail(f2); 266 *tester = of_func_decl(f2); 267 } 268 269 ptr_vector<func_decl> const& accs = *data_util.get_constructor_accessors(f); 270 for (unsigned i = 0; i < num_fields; ++i) { 271 func_decl* f2 = (accs)[i]; 272 mk_c(c)->save_multiple_ast_trail(f2); 273 accessors[i] = of_func_decl(f2); 274 } 275 RETURN_Z3_query_constructor; 276 Z3_CATCH; 277 } 278 Z3_del_constructor(Z3_context c,Z3_constructor constr)279 void Z3_API Z3_del_constructor(Z3_context c, Z3_constructor constr) { 280 Z3_TRY; 281 LOG_Z3_del_constructor(c, constr); 282 RESET_ERROR_CODE(); 283 dealloc(reinterpret_cast<constructor*>(constr)); 284 Z3_CATCH; 285 } 286 mk_datatype_decl(Z3_context c,Z3_symbol name,unsigned num_constructors,Z3_constructor constructors[])287 static datatype_decl* mk_datatype_decl(Z3_context c, 288 Z3_symbol name, 289 unsigned num_constructors, 290 Z3_constructor constructors[]) { 291 datatype_util& dt_util = mk_c(c)->dtutil(); 292 ast_manager& m = mk_c(c)->m(); 293 ptr_vector<constructor_decl> constrs; 294 for (unsigned i = 0; i < num_constructors; ++i) { 295 constructor* cn = reinterpret_cast<constructor*>(constructors[i]); 296 ptr_vector<accessor_decl> acc; 297 for (unsigned j = 0; j < cn->m_sorts.size(); ++j) { 298 if (cn->m_sorts[j].get()) { 299 acc.push_back(mk_accessor_decl(m, cn->m_field_names[j], type_ref(cn->m_sorts[j].get()))); 300 } 301 else { 302 acc.push_back(mk_accessor_decl(m, cn->m_field_names[j], type_ref(cn->m_sort_refs[j]))); 303 } 304 } 305 constrs.push_back(mk_constructor_decl(cn->m_name, cn->m_tester, acc.size(), acc.c_ptr())); 306 } 307 return mk_datatype_decl(dt_util, to_symbol(name), 0, nullptr, num_constructors, constrs.c_ptr()); 308 } 309 Z3_mk_datatype(Z3_context c,Z3_symbol name,unsigned num_constructors,Z3_constructor constructors[])310 Z3_sort Z3_API Z3_mk_datatype(Z3_context c, 311 Z3_symbol name, 312 unsigned num_constructors, 313 Z3_constructor constructors[]) { 314 Z3_TRY; 315 LOG_Z3_mk_datatype(c, name, num_constructors, constructors); 316 RESET_ERROR_CODE(); 317 ast_manager& m = mk_c(c)->m(); 318 datatype_util data_util(m); 319 320 sort_ref_vector sorts(m); 321 { 322 datatype_decl * data = mk_datatype_decl(c, name, num_constructors, constructors); 323 bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &data, 0, nullptr, sorts); 324 del_datatype_decl(data); 325 326 if (!is_ok) { 327 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 328 RETURN_Z3(nullptr); 329 } 330 } 331 sort * s = sorts.get(0); 332 333 mk_c(c)->save_ast_trail(s); 334 ptr_vector<func_decl> const& cnstrs = *data_util.get_datatype_constructors(s); 335 336 for (unsigned i = 0; i < num_constructors; ++i) { 337 constructor* cn = reinterpret_cast<constructor*>(constructors[i]); 338 cn->m_constructor = cnstrs[i]; 339 } 340 RETURN_Z3_mk_datatype(of_sort(s)); 341 Z3_CATCH_RETURN(nullptr); 342 } 343 344 typedef ptr_vector<constructor> constructor_list; 345 Z3_mk_constructor_list(Z3_context c,unsigned num_constructors,Z3_constructor const constructors[])346 Z3_constructor_list Z3_API Z3_mk_constructor_list(Z3_context c, 347 unsigned num_constructors, 348 Z3_constructor const constructors[]) { 349 Z3_TRY; 350 LOG_Z3_mk_constructor_list(c, num_constructors, constructors); 351 RESET_ERROR_CODE(); 352 constructor_list* result = alloc(ptr_vector<constructor>); 353 for (unsigned i = 0; i < num_constructors; ++i) { 354 result->push_back(reinterpret_cast<constructor*>(constructors[i])); 355 } 356 RETURN_Z3(reinterpret_cast<Z3_constructor_list>(result)); 357 Z3_CATCH_RETURN(nullptr); 358 } 359 Z3_del_constructor_list(Z3_context c,Z3_constructor_list clist)360 void Z3_API Z3_del_constructor_list(Z3_context c, Z3_constructor_list clist) { 361 Z3_TRY; 362 LOG_Z3_del_constructor_list(c, clist); 363 RESET_ERROR_CODE(); 364 dealloc(reinterpret_cast<constructor_list*>(clist)); 365 Z3_CATCH; 366 } 367 Z3_mk_datatypes(Z3_context c,unsigned num_sorts,Z3_symbol const sort_names[],Z3_sort sorts[],Z3_constructor_list constructor_lists[])368 void Z3_API Z3_mk_datatypes(Z3_context c, 369 unsigned num_sorts, 370 Z3_symbol const sort_names[], 371 Z3_sort sorts[], 372 Z3_constructor_list constructor_lists[]) { 373 Z3_TRY; 374 LOG_Z3_mk_datatypes(c, num_sorts, sort_names, sorts, constructor_lists); 375 RESET_ERROR_CODE(); 376 ast_manager& m = mk_c(c)->m(); 377 mk_c(c)->reset_last_result(); 378 datatype_util data_util(m); 379 380 ptr_vector<datatype_decl> datas; 381 for (unsigned i = 0; i < num_sorts; ++i) { 382 constructor_list* cl = reinterpret_cast<constructor_list*>(constructor_lists[i]); 383 datas.push_back(mk_datatype_decl(c, sort_names[i], cl->size(), reinterpret_cast<Z3_constructor*>(cl->c_ptr()))); 384 } 385 sort_ref_vector _sorts(m); 386 bool ok = mk_c(c)->get_dt_plugin()->mk_datatypes(datas.size(), datas.c_ptr(), 0, nullptr, _sorts); 387 del_datatype_decls(datas.size(), datas.c_ptr()); 388 389 if (!ok) { 390 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 391 return; 392 } 393 394 SASSERT(_sorts.size() == num_sorts); 395 for (unsigned i = 0; i < _sorts.size(); ++i) { 396 sort* s = _sorts[i].get(); 397 mk_c(c)->save_multiple_ast_trail(s); 398 sorts[i] = of_sort(s); 399 constructor_list* cl = reinterpret_cast<constructor_list*>(constructor_lists[i]); 400 ptr_vector<func_decl> const& cnstrs = *data_util.get_datatype_constructors(s); 401 for (unsigned j = 0; j < cl->size(); ++j) { 402 constructor* cn = (*cl)[j]; 403 cn->m_constructor = cnstrs[j]; 404 } 405 } 406 RETURN_Z3_mk_datatypes; 407 Z3_CATCH; 408 } 409 Z3_get_datatype_sort_num_constructors(Z3_context c,Z3_sort t)410 unsigned Z3_API Z3_get_datatype_sort_num_constructors(Z3_context c, Z3_sort t) { 411 Z3_TRY; 412 LOG_Z3_get_datatype_sort_num_constructors(c, t); 413 RESET_ERROR_CODE(); 414 CHECK_VALID_AST(t, 0); 415 sort * _t = to_sort(t); 416 datatype_util& dt_util = mk_c(c)->dtutil(); 417 418 if (!dt_util.is_datatype(_t)) { 419 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 420 return 0; 421 } 422 return dt_util.get_datatype_constructors(_t)->size(); 423 Z3_CATCH_RETURN(0); 424 } 425 get_datatype_sort_constructor_core(Z3_context c,Z3_sort t,unsigned idx)426 Z3_func_decl get_datatype_sort_constructor_core(Z3_context c, Z3_sort t, unsigned idx) { 427 RESET_ERROR_CODE(); 428 CHECK_VALID_AST(t, nullptr); 429 sort * _t = to_sort(t); 430 datatype_util& dt_util = mk_c(c)->dtutil(); 431 if (!dt_util.is_datatype(_t)) { 432 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 433 return nullptr; 434 } 435 ptr_vector<func_decl> const & decls = *dt_util.get_datatype_constructors(_t); 436 if (idx >= decls.size()) { 437 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 438 return nullptr; 439 } 440 func_decl* decl = (decls)[idx]; 441 mk_c(c)->save_ast_trail(decl); 442 return of_func_decl(decl); 443 } 444 Z3_get_datatype_sort_constructor(Z3_context c,Z3_sort t,unsigned idx)445 Z3_func_decl Z3_API Z3_get_datatype_sort_constructor(Z3_context c, Z3_sort t, unsigned idx) { 446 Z3_TRY; 447 LOG_Z3_get_datatype_sort_constructor(c, t, idx); 448 RESET_ERROR_CODE(); 449 Z3_func_decl r = get_datatype_sort_constructor_core(c, t, idx); 450 RETURN_Z3(r); 451 Z3_CATCH_RETURN(nullptr); 452 } 453 Z3_get_datatype_sort_recognizer(Z3_context c,Z3_sort t,unsigned idx)454 Z3_func_decl Z3_API Z3_get_datatype_sort_recognizer(Z3_context c, Z3_sort t, unsigned idx) { 455 Z3_TRY; 456 LOG_Z3_get_datatype_sort_recognizer(c, t, idx); 457 RESET_ERROR_CODE(); 458 sort * _t = to_sort(t); 459 datatype_util& dt_util = mk_c(c)->dtutil(); 460 461 if (!dt_util.is_datatype(_t)) { 462 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 463 RETURN_Z3(nullptr); 464 } 465 ptr_vector<func_decl> const & decls = *dt_util.get_datatype_constructors(_t); 466 if (idx >= decls.size()) { 467 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 468 RETURN_Z3(nullptr); 469 } 470 func_decl* decl = (decls)[idx]; 471 decl = dt_util.get_constructor_is(decl); 472 mk_c(c)->save_ast_trail(decl); 473 RETURN_Z3(of_func_decl(decl)); 474 Z3_CATCH_RETURN(nullptr); 475 } 476 Z3_get_datatype_sort_constructor_accessor(Z3_context c,Z3_sort t,unsigned idx_c,unsigned idx_a)477 Z3_func_decl Z3_API Z3_get_datatype_sort_constructor_accessor(Z3_context c, Z3_sort t, unsigned idx_c, unsigned idx_a) { 478 Z3_TRY; 479 LOG_Z3_get_datatype_sort_constructor_accessor(c, t, idx_c, idx_a); 480 RESET_ERROR_CODE(); 481 sort * _t = to_sort(t); 482 datatype_util& dt_util = mk_c(c)->dtutil(); 483 484 if (!dt_util.is_datatype(_t)) { 485 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 486 RETURN_Z3(nullptr); 487 } 488 ptr_vector<func_decl> const & decls = *dt_util.get_datatype_constructors(_t); 489 if (idx_c >= decls.size()) { 490 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 491 return nullptr; 492 } 493 func_decl* decl = (decls)[idx_c]; 494 if (decl->get_arity() <= idx_a) { 495 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 496 RETURN_Z3(nullptr); 497 } 498 ptr_vector<func_decl> const & accs = *dt_util.get_constructor_accessors(decl); 499 SASSERT(accs.size() == decl->get_arity()); 500 if (accs.size() <= idx_a) { 501 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 502 RETURN_Z3(nullptr); 503 } 504 decl = (accs)[idx_a]; 505 mk_c(c)->save_ast_trail(decl); 506 RETURN_Z3(of_func_decl(decl)); 507 Z3_CATCH_RETURN(nullptr); 508 } 509 Z3_get_tuple_sort_mk_decl(Z3_context c,Z3_sort t)510 Z3_func_decl Z3_API Z3_get_tuple_sort_mk_decl(Z3_context c, Z3_sort t) { 511 Z3_TRY; 512 LOG_Z3_get_tuple_sort_mk_decl(c, t); 513 RESET_ERROR_CODE(); 514 sort * tuple = to_sort(t); 515 datatype_util& dt_util = mk_c(c)->dtutil(); 516 if (!dt_util.is_datatype(tuple) || dt_util.is_recursive(tuple) || dt_util.get_datatype_num_constructors(tuple) != 1) { 517 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 518 RETURN_Z3(nullptr); 519 } 520 Z3_func_decl r = get_datatype_sort_constructor_core(c, t, 0); 521 RETURN_Z3(r); 522 Z3_CATCH_RETURN(nullptr); 523 } 524 Z3_get_tuple_sort_num_fields(Z3_context c,Z3_sort t)525 unsigned Z3_API Z3_get_tuple_sort_num_fields(Z3_context c, Z3_sort t) { 526 Z3_TRY; 527 LOG_Z3_get_tuple_sort_num_fields(c, t); 528 RESET_ERROR_CODE(); 529 sort * tuple = to_sort(t); 530 datatype_util& dt_util = mk_c(c)->dtutil(); 531 if (!dt_util.is_datatype(tuple) || dt_util.is_recursive(tuple) || dt_util.get_datatype_num_constructors(tuple) != 1) { 532 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 533 return 0; 534 } 535 ptr_vector<func_decl> const & decls = *dt_util.get_datatype_constructors(tuple); 536 if (decls.size() != 1) { 537 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 538 return 0; 539 } 540 ptr_vector<func_decl> const & accs = *dt_util.get_constructor_accessors(decls[0]); 541 return accs.size(); 542 Z3_CATCH_RETURN(0); 543 } 544 Z3_get_tuple_sort_field_decl(Z3_context c,Z3_sort t,unsigned i)545 Z3_func_decl Z3_API Z3_get_tuple_sort_field_decl(Z3_context c, Z3_sort t, unsigned i) { 546 Z3_TRY; 547 LOG_Z3_get_tuple_sort_field_decl(c, t, i); 548 RESET_ERROR_CODE(); 549 sort * tuple = to_sort(t); 550 datatype_util& dt_util = mk_c(c)->dtutil(); 551 if (!dt_util.is_datatype(tuple) || dt_util.is_recursive(tuple) || dt_util.get_datatype_num_constructors(tuple) != 1) { 552 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 553 RETURN_Z3(nullptr); 554 } 555 ptr_vector<func_decl> const & decls = *dt_util.get_datatype_constructors(tuple); 556 if (decls.size() != 1) { 557 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 558 RETURN_Z3(nullptr); 559 } 560 ptr_vector<func_decl> const & accs = *dt_util.get_constructor_accessors((decls)[0]); 561 if (accs.size() <= i) { 562 SET_ERROR_CODE(Z3_IOB, nullptr); 563 RETURN_Z3(nullptr); 564 } 565 func_decl* acc = (accs)[i]; 566 mk_c(c)->save_ast_trail(acc); 567 RETURN_Z3(of_func_decl(acc)); 568 Z3_CATCH_RETURN(nullptr); 569 } 570 Z3_datatype_update_field(Z3_context c,Z3_func_decl f,Z3_ast t,Z3_ast v)571 Z3_ast Z3_datatype_update_field( 572 Z3_context c, Z3_func_decl f, Z3_ast t, Z3_ast v) { 573 Z3_TRY; 574 LOG_Z3_datatype_update_field(c, f, t, v); 575 RESET_ERROR_CODE(); 576 ast_manager & m = mk_c(c)->m(); 577 func_decl* _f = to_func_decl(f); 578 expr* _t = to_expr(t); 579 expr* _v = to_expr(v); 580 expr* args[2] = { _t, _v }; 581 sort* domain[2] = { m.get_sort(_t), m.get_sort(_v) }; 582 parameter param(_f); 583 func_decl * d = m.mk_func_decl(mk_c(c)->get_dt_fid(), OP_DT_UPDATE_FIELD, 1, ¶m, 2, domain); 584 app* r = m.mk_app(d, 2, args); 585 mk_c(c)->save_ast_trail(r); 586 check_sorts(c, r); 587 RETURN_Z3(of_ast(r)); 588 Z3_CATCH_RETURN(nullptr); 589 } 590 591 592 }; 593