1 /*++ 2 Copyright (c) 2012 Microsoft Corporation 3 4 Module Name: 5 6 api_quant.cpp 7 8 Abstract: 9 API for models 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_model.h" 22 #include "api/api_ast_vector.h" 23 #include "ast/array_decl_plugin.h" 24 #include "model/model.h" 25 #include "model/model_v2_pp.h" 26 #include "model/model_smt2_pp.h" 27 #include "model/model_params.hpp" 28 #include "model/model_evaluator_params.hpp" 29 30 extern "C" { 31 Z3_mk_model(Z3_context c)32 Z3_model Z3_API Z3_mk_model(Z3_context c) { 33 Z3_TRY; 34 LOG_Z3_mk_model(c); 35 RESET_ERROR_CODE(); 36 Z3_model_ref * m_ref = alloc(Z3_model_ref, *mk_c(c)); 37 m_ref->m_model = alloc(model, mk_c(c)->m()); 38 mk_c(c)->save_object(m_ref); 39 RETURN_Z3(of_model(m_ref)); 40 Z3_CATCH_RETURN(nullptr); 41 } 42 Z3_model_inc_ref(Z3_context c,Z3_model m)43 void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m) { 44 Z3_TRY; 45 LOG_Z3_model_inc_ref(c, m); 46 RESET_ERROR_CODE(); 47 if (m) { 48 to_model(m)->inc_ref(); 49 } 50 Z3_CATCH; 51 } 52 Z3_model_dec_ref(Z3_context c,Z3_model m)53 void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m) { 54 Z3_TRY; 55 LOG_Z3_model_dec_ref(c, m); 56 RESET_ERROR_CODE(); 57 if (m) { 58 to_model(m)->dec_ref(); 59 } 60 Z3_CATCH; 61 } 62 Z3_model_get_const_interp(Z3_context c,Z3_model m,Z3_func_decl a)63 Z3_ast_opt Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a) { 64 Z3_TRY; 65 LOG_Z3_model_get_const_interp(c, m, a); 66 RESET_ERROR_CODE(); 67 CHECK_NON_NULL(m, nullptr); 68 expr * r = to_model_ref(m)->get_const_interp(to_func_decl(a)); 69 if (!r) { 70 RETURN_Z3(nullptr); 71 } 72 mk_c(c)->save_ast_trail(r); 73 RETURN_Z3(of_expr(r)); 74 Z3_CATCH_RETURN(nullptr); 75 } 76 Z3_model_has_interp(Z3_context c,Z3_model m,Z3_func_decl a)77 bool Z3_API Z3_model_has_interp(Z3_context c, Z3_model m, Z3_func_decl a) { 78 Z3_TRY; 79 LOG_Z3_model_has_interp(c, m, a); 80 CHECK_NON_NULL(m, 0); 81 return to_model_ref(m)->has_interpretation(to_func_decl(a)); 82 Z3_CATCH_RETURN(false); 83 } 84 Z3_model_get_func_interp(Z3_context c,Z3_model m,Z3_func_decl f)85 Z3_func_interp Z3_API Z3_model_get_func_interp(Z3_context c, Z3_model m, Z3_func_decl f) { 86 Z3_TRY; 87 LOG_Z3_model_get_func_interp(c, m, f); 88 RESET_ERROR_CODE(); 89 CHECK_NON_NULL(m, nullptr); 90 func_interp * _fi = to_model_ref(m)->get_func_interp(to_func_decl(f)); 91 if (!_fi) { 92 RETURN_Z3(nullptr); 93 } 94 Z3_func_interp_ref * fi = alloc(Z3_func_interp_ref, *mk_c(c), to_model_ref(m)); 95 fi->m_func_interp = _fi; 96 mk_c(c)->save_object(fi); 97 RETURN_Z3(of_func_interp(fi)); 98 Z3_CATCH_RETURN(nullptr); 99 } 100 Z3_model_get_num_consts(Z3_context c,Z3_model m)101 unsigned Z3_API Z3_model_get_num_consts(Z3_context c, Z3_model m) { 102 Z3_TRY; 103 LOG_Z3_model_get_num_consts(c, m); 104 RESET_ERROR_CODE(); 105 CHECK_NON_NULL(m, 0); 106 return to_model_ref(m)->get_num_constants(); 107 Z3_CATCH_RETURN(0); 108 } 109 Z3_model_get_const_decl(Z3_context c,Z3_model m,unsigned i)110 Z3_func_decl Z3_API Z3_model_get_const_decl(Z3_context c, Z3_model m, unsigned i) { 111 Z3_TRY; 112 LOG_Z3_model_get_const_decl(c, m, i); 113 RESET_ERROR_CODE(); 114 CHECK_NON_NULL(m, nullptr); 115 model * _m = to_model_ref(m); 116 if (i < _m->get_num_constants()) { 117 RETURN_Z3(of_func_decl(_m->get_constant(i))); 118 } 119 else { 120 SET_ERROR_CODE(Z3_IOB, nullptr); 121 RETURN_Z3(nullptr); 122 } 123 Z3_CATCH_RETURN(nullptr); 124 } 125 Z3_model_get_num_funcs(Z3_context c,Z3_model m)126 unsigned Z3_API Z3_model_get_num_funcs(Z3_context c, Z3_model m) { 127 Z3_TRY; 128 LOG_Z3_model_get_num_funcs(c, m); 129 RESET_ERROR_CODE(); 130 CHECK_NON_NULL(m, 0); 131 return to_model_ref(m)->get_num_functions(); 132 Z3_CATCH_RETURN(0); 133 } 134 get_model_func_decl_core(Z3_context c,Z3_model m,unsigned i)135 Z3_func_decl get_model_func_decl_core(Z3_context c, Z3_model m, unsigned i) { 136 CHECK_NON_NULL(m, nullptr); 137 model * _m = to_model_ref(m); 138 if (i >= _m->get_num_functions()) { 139 SET_ERROR_CODE(Z3_IOB, nullptr); 140 return nullptr; 141 } 142 return of_func_decl(_m->get_function(i)); 143 } 144 Z3_model_get_func_decl(Z3_context c,Z3_model m,unsigned i)145 Z3_func_decl Z3_API Z3_model_get_func_decl(Z3_context c, Z3_model m, unsigned i) { 146 Z3_TRY; 147 LOG_Z3_model_get_func_decl(c, m, i); 148 RESET_ERROR_CODE(); 149 Z3_func_decl r = get_model_func_decl_core(c, m, i); 150 RETURN_Z3(r); 151 Z3_CATCH_RETURN(nullptr); 152 } 153 Z3_model_eval(Z3_context c,Z3_model m,Z3_ast t,bool model_completion,Z3_ast * v)154 bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast * v) { 155 Z3_TRY; 156 LOG_Z3_model_eval(c, m, t, model_completion, v); 157 if (v) *v = nullptr; 158 RESET_ERROR_CODE(); 159 CHECK_NON_NULL(m, false); 160 CHECK_IS_EXPR(t, false); 161 model * _m = to_model_ref(m); 162 params_ref p; 163 ast_manager& mgr = mk_c(c)->m(); 164 if (!_m->has_solver()) { 165 _m->set_solver(alloc(api::seq_expr_solver, mgr, p)); 166 } 167 expr_ref result(mgr); 168 model::scoped_model_completion _scm(*_m, model_completion); 169 result = (*_m)(to_expr(t)); 170 mk_c(c)->save_ast_trail(result.get()); 171 *v = of_ast(result.get()); 172 RETURN_Z3_model_eval true; 173 Z3_CATCH_RETURN(false); 174 } 175 Z3_model_get_num_sorts(Z3_context c,Z3_model m)176 unsigned Z3_API Z3_model_get_num_sorts(Z3_context c, Z3_model m) { 177 Z3_TRY; 178 LOG_Z3_model_get_num_sorts(c, m); 179 RESET_ERROR_CODE(); 180 return to_model_ref(m)->get_num_uninterpreted_sorts(); 181 Z3_CATCH_RETURN(0); 182 } 183 Z3_model_get_sort(Z3_context c,Z3_model m,unsigned i)184 Z3_sort Z3_API Z3_model_get_sort(Z3_context c, Z3_model m, unsigned i) { 185 Z3_TRY; 186 LOG_Z3_model_get_sort(c, m, i); 187 RESET_ERROR_CODE(); 188 if (i >= to_model_ref(m)->get_num_uninterpreted_sorts()) { 189 SET_ERROR_CODE(Z3_IOB, nullptr); 190 RETURN_Z3(nullptr); 191 } 192 sort * s = to_model_ref(m)->get_uninterpreted_sort(i); 193 RETURN_Z3(of_sort(s)); 194 Z3_CATCH_RETURN(nullptr); 195 } 196 Z3_model_get_sort_universe(Z3_context c,Z3_model m,Z3_sort s)197 Z3_ast_vector Z3_API Z3_model_get_sort_universe(Z3_context c, Z3_model m, Z3_sort s) { 198 Z3_TRY; 199 LOG_Z3_model_get_sort_universe(c, m, s); 200 RESET_ERROR_CODE(); 201 if (!to_model_ref(m)->has_uninterpreted_sort(to_sort(s))) { 202 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 203 RETURN_Z3(nullptr); 204 } 205 ptr_vector<expr> const & universe = to_model_ref(m)->get_universe(to_sort(s)); 206 Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); 207 mk_c(c)->save_object(v); 208 for (expr * e : universe) { 209 v->m_ast_vector.push_back(e); 210 } 211 RETURN_Z3(of_ast_vector(v)); 212 Z3_CATCH_RETURN(nullptr); 213 } 214 Z3_model_translate(Z3_context c,Z3_model m,Z3_context target)215 Z3_model Z3_API Z3_model_translate(Z3_context c, Z3_model m, Z3_context target) { 216 Z3_TRY; 217 LOG_Z3_model_translate(c, m, target); 218 RESET_ERROR_CODE(); 219 Z3_model_ref* dst = alloc(Z3_model_ref, *mk_c(target)); 220 ast_translation tr(mk_c(c)->m(), mk_c(target)->m()); 221 dst->m_model = to_model_ref(m)->translate(tr); 222 mk_c(target)->save_object(dst); 223 RETURN_Z3(of_model(dst)); 224 Z3_CATCH_RETURN(nullptr); 225 } 226 Z3_is_as_array(Z3_context c,Z3_ast a)227 bool Z3_API Z3_is_as_array(Z3_context c, Z3_ast a) { 228 Z3_TRY; 229 LOG_Z3_is_as_array(c, a); 230 RESET_ERROR_CODE(); 231 return a && is_expr(to_ast(a)) && is_app_of(to_expr(a), mk_c(c)->get_array_fid(), OP_AS_ARRAY); 232 Z3_CATCH_RETURN(false); 233 } 234 Z3_get_as_array_func_decl(Z3_context c,Z3_ast a)235 Z3_func_decl Z3_API Z3_get_as_array_func_decl(Z3_context c, Z3_ast a) { 236 Z3_TRY; 237 LOG_Z3_get_as_array_func_decl(c, a); 238 RESET_ERROR_CODE(); 239 if (a && is_expr(to_ast(a)) && is_app_of(to_expr(a), mk_c(c)->get_array_fid(), OP_AS_ARRAY)) { 240 RETURN_Z3(of_func_decl(to_func_decl(to_app(a)->get_decl()->get_parameter(0).get_ast()))); 241 } 242 else { 243 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 244 RETURN_Z3(nullptr); 245 } 246 Z3_CATCH_RETURN(nullptr); 247 } 248 Z3_add_func_interp(Z3_context c,Z3_model m,Z3_func_decl f,Z3_ast else_val)249 Z3_func_interp Z3_API Z3_add_func_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast else_val) { 250 Z3_TRY; 251 LOG_Z3_add_func_interp(c, m, f, else_val); 252 RESET_ERROR_CODE(); 253 CHECK_NON_NULL(f, nullptr); 254 func_decl* d = to_func_decl(f); 255 model* mdl = to_model_ref(m); 256 Z3_func_interp_ref * f_ref = alloc(Z3_func_interp_ref, *mk_c(c), mdl); 257 f_ref->m_func_interp = alloc(func_interp, mk_c(c)->m(), d->get_arity()); 258 mk_c(c)->save_object(f_ref); 259 mdl->register_decl(d, f_ref->m_func_interp); 260 f_ref->m_func_interp->set_else(to_expr(else_val)); 261 RETURN_Z3(of_func_interp(f_ref)); 262 Z3_CATCH_RETURN(nullptr); 263 } 264 Z3_add_const_interp(Z3_context c,Z3_model m,Z3_func_decl f,Z3_ast a)265 void Z3_API Z3_add_const_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast a) { 266 Z3_TRY; 267 LOG_Z3_add_const_interp(c, m, f, a); 268 RESET_ERROR_CODE(); 269 func_decl* d = to_func_decl(f); 270 if (!d || d->get_arity() != 0) { 271 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 272 } 273 else { 274 model* mdl = to_model_ref(m); 275 mdl->register_decl(d, to_expr(a)); 276 } 277 Z3_CATCH; 278 } 279 Z3_func_interp_inc_ref(Z3_context c,Z3_func_interp f)280 void Z3_API Z3_func_interp_inc_ref(Z3_context c, Z3_func_interp f) { 281 Z3_TRY; 282 LOG_Z3_func_interp_inc_ref(c, f); 283 RESET_ERROR_CODE(); 284 if (f) { 285 to_func_interp(f)->inc_ref(); 286 } 287 Z3_CATCH; 288 } 289 Z3_func_interp_dec_ref(Z3_context c,Z3_func_interp f)290 void Z3_API Z3_func_interp_dec_ref(Z3_context c, Z3_func_interp f) { 291 Z3_TRY; 292 LOG_Z3_func_interp_dec_ref(c, f); 293 RESET_ERROR_CODE(); 294 if (f) { 295 to_func_interp(f)->dec_ref(); 296 } 297 Z3_CATCH; 298 } 299 Z3_func_interp_get_num_entries(Z3_context c,Z3_func_interp f)300 unsigned Z3_API Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f) { 301 Z3_TRY; 302 LOG_Z3_func_interp_get_num_entries(c, f); 303 RESET_ERROR_CODE(); 304 CHECK_NON_NULL(f, 0); 305 return to_func_interp_ref(f)->num_entries(); 306 Z3_CATCH_RETURN(0); 307 } 308 Z3_func_interp_get_entry(Z3_context c,Z3_func_interp f,unsigned i)309 Z3_func_entry Z3_API Z3_func_interp_get_entry(Z3_context c, Z3_func_interp f, unsigned i) { 310 Z3_TRY; 311 LOG_Z3_func_interp_get_entry(c, f, i); 312 RESET_ERROR_CODE(); 313 CHECK_NON_NULL(f, nullptr); 314 if (i >= to_func_interp_ref(f)->num_entries()) { 315 SET_ERROR_CODE(Z3_IOB, nullptr); 316 RETURN_Z3(nullptr); 317 } 318 Z3_func_entry_ref * e = alloc(Z3_func_entry_ref, *mk_c(c), to_func_interp(f)->m_model.get()); 319 e->m_func_interp = to_func_interp_ref(f); 320 e->m_func_entry = to_func_interp_ref(f)->get_entry(i); 321 mk_c(c)->save_object(e); 322 RETURN_Z3(of_func_entry(e)); 323 Z3_CATCH_RETURN(nullptr); 324 } 325 Z3_func_interp_get_else(Z3_context c,Z3_func_interp f)326 Z3_ast Z3_API Z3_func_interp_get_else(Z3_context c, Z3_func_interp f) { 327 Z3_TRY; 328 LOG_Z3_func_interp_get_else(c, f); 329 RESET_ERROR_CODE(); 330 CHECK_NON_NULL(f, nullptr); 331 expr * e = to_func_interp_ref(f)->get_else(); 332 if (e) { 333 mk_c(c)->save_ast_trail(e); 334 } 335 RETURN_Z3(of_expr(e)); 336 Z3_CATCH_RETURN(nullptr); 337 } 338 Z3_func_interp_set_else(Z3_context c,Z3_func_interp f,Z3_ast else_value)339 void Z3_API Z3_func_interp_set_else(Z3_context c, Z3_func_interp f, Z3_ast else_value) { 340 Z3_TRY; 341 LOG_Z3_func_interp_set_else(c, f, else_value); 342 RESET_ERROR_CODE(); 343 // CHECK_NON_NULL(f, 0); 344 to_func_interp_ref(f)->set_else(to_expr(else_value)); 345 Z3_CATCH; 346 } 347 Z3_func_interp_get_arity(Z3_context c,Z3_func_interp f)348 unsigned Z3_API Z3_func_interp_get_arity(Z3_context c, Z3_func_interp f) { 349 Z3_TRY; 350 LOG_Z3_func_interp_get_arity(c, f); 351 RESET_ERROR_CODE(); 352 CHECK_NON_NULL(f, 0); 353 return to_func_interp_ref(f)->get_arity(); 354 Z3_CATCH_RETURN(0); 355 } 356 Z3_func_interp_add_entry(Z3_context c,Z3_func_interp fi,Z3_ast_vector args,Z3_ast value)357 void Z3_API Z3_func_interp_add_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value) { 358 Z3_TRY; 359 LOG_Z3_func_interp_add_entry(c, fi, args, value); 360 //CHECK_NON_NULL(fi, void); 361 //CHECK_NON_NULL(args, void); 362 //CHECK_NON_NULL(value, void); 363 func_interp* _fi = to_func_interp_ref(fi); 364 expr* _value = to_expr(value); 365 if (to_ast_vector_ref(args).size() != _fi->get_arity()) { 366 SET_ERROR_CODE(Z3_IOB, nullptr); 367 return; 368 } 369 // check sorts of value 370 expr* const* _args = (expr* const*) to_ast_vector_ref(args).data(); 371 _fi->insert_entry(_args, _value); 372 Z3_CATCH; 373 } 374 Z3_func_entry_inc_ref(Z3_context c,Z3_func_entry e)375 void Z3_API Z3_func_entry_inc_ref(Z3_context c, Z3_func_entry e) { 376 Z3_TRY; 377 LOG_Z3_func_entry_inc_ref(c, e); 378 RESET_ERROR_CODE(); 379 if (e) { 380 to_func_entry(e)->inc_ref(); 381 } 382 Z3_CATCH; 383 } 384 Z3_func_entry_dec_ref(Z3_context c,Z3_func_entry e)385 void Z3_API Z3_func_entry_dec_ref(Z3_context c, Z3_func_entry e) { 386 Z3_TRY; 387 LOG_Z3_func_entry_dec_ref(c, e); 388 RESET_ERROR_CODE(); 389 if (e) { 390 to_func_entry(e)->dec_ref(); 391 } 392 Z3_CATCH; 393 } 394 Z3_func_entry_get_value(Z3_context c,Z3_func_entry e)395 Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e) { 396 Z3_TRY; 397 LOG_Z3_func_entry_get_value(c, e); 398 RESET_ERROR_CODE(); 399 expr * v = to_func_entry_ref(e)->get_result(); 400 mk_c(c)->save_ast_trail(v); 401 RETURN_Z3(of_expr(v)); 402 Z3_CATCH_RETURN(nullptr); 403 } 404 Z3_func_entry_get_num_args(Z3_context c,Z3_func_entry e)405 unsigned Z3_API Z3_func_entry_get_num_args(Z3_context c, Z3_func_entry e) { 406 Z3_TRY; 407 LOG_Z3_func_entry_get_num_args(c, e); 408 RESET_ERROR_CODE(); 409 return to_func_entry(e)->m_func_interp->get_arity(); 410 Z3_CATCH_RETURN(0); 411 } 412 Z3_func_entry_get_arg(Z3_context c,Z3_func_entry e,unsigned i)413 Z3_ast Z3_API Z3_func_entry_get_arg(Z3_context c, Z3_func_entry e, unsigned i) { 414 Z3_TRY; 415 LOG_Z3_func_entry_get_arg(c, e, i); 416 RESET_ERROR_CODE(); 417 if (i >= to_func_entry(e)->m_func_interp->get_arity()) { 418 SET_ERROR_CODE(Z3_IOB, nullptr); 419 RETURN_Z3(nullptr); 420 } 421 expr * r = to_func_entry(e)->m_func_entry->get_arg(i); 422 RETURN_Z3(of_expr(r)); 423 Z3_CATCH_RETURN(nullptr); 424 } 425 Z3_model_to_string(Z3_context c,Z3_model m)426 Z3_API char const * Z3_model_to_string(Z3_context c, Z3_model m) { 427 Z3_TRY; 428 LOG_Z3_model_to_string(c, m); 429 RESET_ERROR_CODE(); 430 CHECK_NON_NULL(m, nullptr); 431 std::ostringstream buffer; 432 std::string result; 433 if (mk_c(c)->get_print_mode() == Z3_PRINT_SMTLIB2_COMPLIANT) { 434 model_smt2_pp(buffer, mk_c(c)->m(), *(to_model_ref(m)), 0); 435 // Hack for removing the trailing '\n' 436 result = buffer.str(); 437 if (!result.empty()) 438 result.resize(result.size()-1); 439 } 440 else { 441 model_params p; 442 model_v2_pp(buffer, *(to_model_ref(m)), p.partial()); 443 result = buffer.str(); 444 } 445 return mk_c(c)->mk_external_string(std::move(result)); 446 Z3_CATCH_RETURN(nullptr); 447 } 448 449 }; 450