1 /*++ 2 Copyright (c) 2012 Microsoft Corporation 3 4 Module Name: 5 6 api_context.cpp 7 8 Abstract: 9 Interface of Z3 with "external world". 10 11 It was called _Z3_context 12 13 Author: 14 15 Leonardo de Moura (leonardo) 2012-02-29. 16 17 Revision History: 18 19 --*/ 20 #include<typeinfo> 21 #include "util/z3_version.h" 22 #include "api/api_context.h" 23 #include "ast/ast_pp.h" 24 #include "ast/ast_ll_pp.h" 25 #include "api/api_log_macros.h" 26 #include "api/api_util.h" 27 #include "ast/reg_decl_plugins.h" 28 #include "math/realclosure/realclosure.h" 29 30 31 // The install_tactics procedure is automatically generated 32 void install_tactics(tactic_manager & ctx); 33 34 namespace api { 35 object(context & c)36 object::object(context& c): m_ref_count(0), m_context(c) { this->m_id = m_context.add_object(this); } 37 inc_ref()38 void object::inc_ref() { m_ref_count++; } 39 dec_ref()40 void object::dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (m_ref_count == 0) m_context.del_object(this); } 41 add_object(api::object * o)42 unsigned context::add_object(api::object* o) { 43 unsigned id = m_allocated_objects.size(); 44 if (!m_free_object_ids.empty()) { 45 id = m_free_object_ids.back(); 46 m_free_object_ids.pop_back(); 47 } 48 m_allocated_objects.insert(id, o); 49 return id; 50 } 51 del_object(api::object * o)52 void context::del_object(api::object* o) { 53 m_free_object_ids.push_back(o->id()); 54 m_allocated_objects.remove(o->id()); 55 dealloc(o); 56 } 57 default_error_handler(Z3_context ctx,Z3_error_code c)58 static void default_error_handler(Z3_context ctx, Z3_error_code c) { 59 printf("Error: %s\n", Z3_get_error_msg(ctx, c)); 60 exit(1); 61 } 62 add_plugins(ast_manager & m)63 context::add_plugins::add_plugins(ast_manager & m) { 64 reg_decl_plugins(m); 65 } 66 67 // ------------------------ 68 // 69 // Core 70 // 71 // ------------------------ 72 context(context_params * p,bool user_ref_count)73 context::context(context_params * p, bool user_ref_count): 74 m_params(p != nullptr ? *p : context_params()), 75 m_user_ref_count(user_ref_count), 76 m_manager(m_params.mk_ast_manager()), 77 m_plugins(m()), 78 m_arith_util(m()), 79 m_bv_util(m()), 80 m_datalog_util(m()), 81 m_fpa_util(m()), 82 m_sutil(m()), 83 m_recfun(m()), 84 m_last_result(m()), 85 m_ast_trail(m()), 86 m_pmanager(m_limit) { 87 88 m_error_code = Z3_OK; 89 m_print_mode = Z3_PRINT_SMTLIB_FULL; 90 m_searching = false; 91 92 93 m_interruptable = nullptr; 94 m_error_handler = &default_error_handler; 95 96 m_basic_fid = m().get_basic_family_id(); 97 m_arith_fid = m().mk_family_id("arith"); 98 m_bv_fid = m().mk_family_id("bv"); 99 m_pb_fid = m().mk_family_id("pb"); 100 m_array_fid = m().mk_family_id("array"); 101 m_dt_fid = m().mk_family_id("datatype"); 102 m_datalog_fid = m().mk_family_id("datalog_relation"); 103 m_fpa_fid = m().mk_family_id("fpa"); 104 m_seq_fid = m().mk_family_id("seq"); 105 m_special_relations_fid = m().mk_family_id("specrels"); 106 m_dt_plugin = static_cast<datatype_decl_plugin*>(m().get_plugin(m_dt_fid)); 107 108 install_tactics(*this); 109 } 110 111 ~context()112 context::~context() { 113 m_last_obj = nullptr; 114 for (auto& kv : m_allocated_objects) { 115 api::object* val = kv.m_value; 116 DEBUG_CODE(warning_msg("Uncollected memory: %d: %s", kv.m_key, typeid(*val).name());); 117 dealloc(val); 118 } 119 if (m_params.owns_manager()) 120 m_manager.detach(); 121 } 122 set_interruptable(context & ctx,event_handler & i)123 context::set_interruptable::set_interruptable(context & ctx, event_handler & i): 124 m_ctx(ctx) { 125 lock_guard lock(ctx.m_mux); 126 SASSERT(m_ctx.m_interruptable == 0); 127 m_ctx.m_interruptable = &i; 128 } 129 ~set_interruptable()130 context::set_interruptable::~set_interruptable() { 131 lock_guard lock(m_ctx.m_mux); 132 m_ctx.m_interruptable = nullptr; 133 } 134 interrupt()135 void context::interrupt() { 136 lock_guard lock(m_mux); 137 if (m_interruptable) 138 (*m_interruptable)(API_INTERRUPT_EH_CALLER); 139 m_limit.cancel(); 140 m().limit().cancel(); 141 } 142 set_error_code(Z3_error_code err,char const * opt_msg)143 void context::set_error_code(Z3_error_code err, char const* opt_msg) { 144 m_error_code = err; 145 if (err != Z3_OK) { 146 m_exception_msg.clear(); 147 if (opt_msg) m_exception_msg = opt_msg; 148 invoke_error_handler(err); 149 } 150 } 151 set_error_code(Z3_error_code err,std::string && opt_msg)152 void context::set_error_code(Z3_error_code err, std::string &&opt_msg) { 153 m_error_code = err; 154 if (err != Z3_OK) { 155 m_exception_msg = std::move(opt_msg); 156 invoke_error_handler(err); 157 } 158 } 159 check_searching()160 void context::check_searching() { 161 if (m_searching) { 162 set_error_code(Z3_INVALID_USAGE, "cannot use function while searching"); // TBD: error code could be fixed. 163 } 164 } 165 mk_external_string(char const * str)166 char * context::mk_external_string(char const * str) { 167 m_string_buffer = str?str:""; 168 return const_cast<char *>(m_string_buffer.c_str()); 169 } 170 mk_external_string(char const * str,unsigned n)171 char * context::mk_external_string(char const * str, unsigned n) { 172 m_string_buffer.clear(); 173 m_string_buffer.append(str, n); 174 return const_cast<char *>(m_string_buffer.c_str()); 175 } 176 mk_external_string(std::string && str)177 char * context::mk_external_string(std::string && str) { 178 m_string_buffer = std::move(str); 179 return const_cast<char *>(m_string_buffer.c_str()); 180 } 181 mk_numeral_core(rational const & n,sort * s)182 expr * context::mk_numeral_core(rational const & n, sort * s) { 183 expr* e = nullptr; 184 family_id fid = s->get_family_id(); 185 if (fid == m_arith_fid) { 186 e = m_arith_util.mk_numeral(n, s); 187 } 188 else if (fid == m_bv_fid) { 189 e = m_bv_util.mk_numeral(n, s); 190 } 191 else if (fid == get_datalog_fid() && n.is_uint64()) { 192 uint64_t sz; 193 if (m_datalog_util.try_get_size(s, sz) && 194 sz <= n.get_uint64()) { 195 invoke_error_handler(Z3_INVALID_ARG); 196 } 197 e = m_datalog_util.mk_numeral(n.get_uint64(), s); 198 } 199 else if (fid == m_fpa_fid) { 200 scoped_mpf tmp(fpautil().fm()); 201 fpautil().fm().set(tmp, fpautil().get_ebits(s), fpautil().get_sbits(s), n.get_double()); 202 e = fpautil().mk_value(tmp); 203 } 204 else { 205 invoke_error_handler(Z3_INVALID_ARG); 206 } 207 save_ast_trail(e); 208 return e; 209 } 210 mk_and(unsigned num_exprs,expr * const * exprs)211 expr * context::mk_and(unsigned num_exprs, expr * const * exprs) { 212 switch(num_exprs) { 213 case 0: 214 return m().mk_true(); 215 case 1: 216 save_ast_trail(exprs[0]); 217 return exprs[0]; 218 default: { 219 expr * a = m().mk_and(num_exprs, exprs); 220 save_ast_trail(a); 221 return a; 222 } } 223 } 224 225 save_ast_trail(ast * n)226 void context::save_ast_trail(ast * n) { 227 SASSERT(m().contains(n)); 228 if (m_user_ref_count) { 229 // Corner case bug: n may be in m_last_result, and this is the only reference to n. 230 // When, we execute reset() it is deleted 231 // To avoid this bug, I bump the reference counter before resetting m_last_result 232 ast_ref node(n, m()); 233 m_last_result.reset(); 234 m_last_result.push_back(std::move(node)); 235 } 236 else { 237 m_ast_trail.push_back(n); 238 } 239 } 240 save_multiple_ast_trail(ast * n)241 void context::save_multiple_ast_trail(ast * n) { 242 if (m_user_ref_count) 243 m_last_result.push_back(n); 244 else 245 m_ast_trail.push_back(n); 246 } 247 reset_last_result()248 void context::reset_last_result() { 249 if (m_user_ref_count) 250 m_last_result.reset(); 251 m_last_obj = nullptr; 252 } 253 save_object(object * r)254 void context::save_object(object * r) { 255 m_last_obj = r; 256 } 257 handle_exception(z3_exception & ex)258 void context::handle_exception(z3_exception & ex) { 259 if (ex.has_error_code()) { 260 switch(ex.error_code()) { 261 case ERR_MEMOUT: 262 set_error_code(Z3_MEMOUT_FAIL, nullptr); 263 break; 264 case ERR_PARSER: 265 set_error_code(Z3_PARSER_ERROR, ex.msg()); 266 break; 267 case ERR_INI_FILE: 268 set_error_code(Z3_INVALID_ARG, nullptr); 269 break; 270 case ERR_OPEN_FILE: 271 set_error_code(Z3_FILE_ACCESS_ERROR, nullptr); 272 break; 273 default: 274 set_error_code(Z3_INTERNAL_FATAL, nullptr); 275 break; 276 } 277 } 278 else { 279 set_error_code(Z3_EXCEPTION, ex.msg()); 280 } 281 } 282 invoke_error_handler(Z3_error_code c)283 void context::invoke_error_handler(Z3_error_code c) { 284 if (m_error_handler) { 285 if (g_z3_log) { 286 // error handler can do crazy stuff such as longjmp 287 g_z3_log_enabled = true; 288 } 289 m_error_handler(reinterpret_cast<Z3_context>(this), c); 290 } 291 } 292 check_sorts(ast * n)293 void context::check_sorts(ast * n) { 294 if (!m().check_sorts(n)) { 295 switch(n->get_kind()) { 296 case AST_APP: { 297 std::ostringstream buffer; 298 app * a = to_app(n); 299 buffer << mk_pp(a->get_decl(), m()) << " applied to: "; 300 if (a->get_num_args() > 1) buffer << "\n"; 301 for (unsigned i = 0; i < a->get_num_args(); ++i) { 302 buffer << mk_bounded_pp(a->get_arg(i), m(), 3) << " of sort "; 303 buffer << mk_pp(m().get_sort(a->get_arg(i)), m()) << "\n"; 304 } 305 auto str = buffer.str(); 306 warning_msg("%s", str.c_str()); 307 break; 308 } 309 case AST_VAR: 310 case AST_QUANTIFIER: 311 case AST_SORT: 312 case AST_FUNC_DECL: 313 break; 314 } 315 set_error_code(Z3_SORT_ERROR, nullptr); 316 } 317 } 318 319 // ------------------------ 320 // 321 // RCF manager 322 // 323 // ----------------------- rcfm()324 realclosure::manager & context::rcfm() { 325 if (m_rcf_manager.get() == nullptr) { 326 m_rcf_manager = alloc(realclosure::manager, m_limit, m_rcf_qm); 327 } 328 return *(m_rcf_manager.get()); 329 } 330 331 }; 332 333 334 // ------------------------ 335 // 336 // Context creation API 337 // 338 // ------------------------ 339 340 extern "C" { 341 Z3_mk_context(Z3_config c)342 Z3_context Z3_API Z3_mk_context(Z3_config c) { 343 Z3_TRY; 344 LOG_Z3_mk_context(c); 345 memory::initialize(UINT_MAX); 346 Z3_context r = reinterpret_cast<Z3_context>(alloc(api::context, reinterpret_cast<context_params*>(c), false)); 347 RETURN_Z3(r); 348 Z3_CATCH_RETURN_NO_HANDLE(nullptr); 349 } 350 Z3_mk_context_rc(Z3_config c)351 Z3_context Z3_API Z3_mk_context_rc(Z3_config c) { 352 Z3_TRY; 353 LOG_Z3_mk_context_rc(c); 354 memory::initialize(UINT_MAX); 355 Z3_context r = reinterpret_cast<Z3_context>(alloc(api::context, reinterpret_cast<context_params*>(c), true)); 356 RETURN_Z3(r); 357 Z3_CATCH_RETURN_NO_HANDLE(nullptr); 358 } 359 Z3_del_context(Z3_context c)360 void Z3_API Z3_del_context(Z3_context c) { 361 Z3_TRY; 362 LOG_Z3_del_context(c); 363 RESET_ERROR_CODE(); 364 dealloc(mk_c(c)); 365 Z3_CATCH; 366 } 367 Z3_interrupt(Z3_context c)368 void Z3_API Z3_interrupt(Z3_context c) { 369 Z3_TRY; 370 LOG_Z3_interrupt(c); 371 mk_c(c)->interrupt(); 372 Z3_CATCH; 373 } 374 Z3_toggle_warning_messages(bool enabled)375 void Z3_API Z3_toggle_warning_messages(bool enabled) { 376 LOG_Z3_toggle_warning_messages(enabled); 377 enable_warning_messages(enabled != 0); 378 } 379 Z3_inc_ref(Z3_context c,Z3_ast a)380 void Z3_API Z3_inc_ref(Z3_context c, Z3_ast a) { 381 Z3_TRY; 382 LOG_Z3_inc_ref(c, a); 383 RESET_ERROR_CODE(); 384 mk_c(c)->m().inc_ref(to_ast(a)); 385 Z3_CATCH; 386 } 387 Z3_dec_ref(Z3_context c,Z3_ast a)388 void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a) { 389 Z3_TRY; 390 LOG_Z3_dec_ref(c, a); 391 RESET_ERROR_CODE(); 392 if (a && to_ast(a)->get_ref_count() == 0) { 393 SET_ERROR_CODE(Z3_DEC_REF_ERROR, nullptr); 394 return; 395 } 396 if (a) { 397 mk_c(c)->m().dec_ref(to_ast(a)); 398 } 399 Z3_CATCH; 400 } 401 402 Z3_get_version(unsigned * major,unsigned * minor,unsigned * build_number,unsigned * revision_number)403 void Z3_API Z3_get_version(unsigned * major, 404 unsigned * minor, 405 unsigned * build_number, 406 unsigned * revision_number) { 407 LOG_Z3_get_version(major, minor, build_number, revision_number); 408 *major = Z3_MAJOR_VERSION; 409 *minor = Z3_MINOR_VERSION; 410 *build_number = Z3_BUILD_NUMBER; 411 *revision_number = Z3_REVISION_NUMBER; 412 } 413 Z3_get_full_version(void)414 Z3_string Z3_API Z3_get_full_version(void) { 415 LOG_Z3_get_full_version(); 416 return Z3_FULL_VERSION; 417 } 418 Z3_enable_trace(Z3_string tag)419 void Z3_API Z3_enable_trace(Z3_string tag) { 420 memory::initialize(UINT_MAX); 421 LOG_Z3_enable_trace(tag); 422 // Tag is a string that was probably not allocated by Z3. Create a copy using symbol. 423 symbol tag_sym(tag); 424 enable_trace(tag_sym.bare_str()); 425 } 426 Z3_disable_trace(Z3_string tag)427 void Z3_API Z3_disable_trace(Z3_string tag) { 428 LOG_Z3_disable_trace(tag); 429 disable_trace(tag); 430 } 431 Z3_reset_memory(void)432 void Z3_API Z3_reset_memory(void) { 433 LOG_Z3_reset_memory(); 434 memory::finalize(false); 435 memory::initialize(0); 436 } 437 Z3_finalize_memory(void)438 void Z3_API Z3_finalize_memory(void) { 439 LOG_Z3_finalize_memory(); 440 memory::finalize(true); 441 } 442 Z3_get_error_code(Z3_context c)443 Z3_error_code Z3_API Z3_get_error_code(Z3_context c) { 444 LOG_Z3_get_error_code(c); 445 return mk_c(c)->get_error_code(); 446 } 447 Z3_set_error_handler(Z3_context c,Z3_error_handler h)448 void Z3_API Z3_set_error_handler(Z3_context c, Z3_error_handler h) { 449 RESET_ERROR_CODE(); 450 mk_c(c)->set_error_handler(h); 451 } 452 Z3_set_error(Z3_context c,Z3_error_code e)453 void Z3_API Z3_set_error(Z3_context c, Z3_error_code e) { 454 SET_ERROR_CODE(e, nullptr); 455 } 456 _get_error_msg(Z3_context c,Z3_error_code err)457 static char const * _get_error_msg(Z3_context c, Z3_error_code err) { 458 if (c) { 459 char const* msg = mk_c(c)->get_exception_msg(); 460 if (msg && *msg) return msg; 461 } 462 switch(err) { 463 case Z3_OK: return "ok"; 464 case Z3_SORT_ERROR: return "type error"; 465 case Z3_IOB: return "index out of bounds"; 466 case Z3_INVALID_ARG: return "invalid argument"; 467 case Z3_PARSER_ERROR: return "parser error"; 468 case Z3_NO_PARSER: return "parser (data) is not available"; 469 case Z3_INVALID_PATTERN: return "invalid pattern"; 470 case Z3_MEMOUT_FAIL: return "out of memory"; 471 case Z3_FILE_ACCESS_ERROR: return "file access error"; 472 case Z3_INTERNAL_FATAL: return "internal error"; 473 case Z3_INVALID_USAGE: return "invalid usage"; 474 case Z3_DEC_REF_ERROR: return "invalid dec_ref command"; 475 case Z3_EXCEPTION: return "Z3 exception"; 476 default: return "unknown"; 477 } 478 } 479 Z3_get_error_msg(Z3_context c,Z3_error_code err)480 Z3_API char const * Z3_get_error_msg(Z3_context c, Z3_error_code err) { 481 LOG_Z3_get_error_msg(c, err); 482 return _get_error_msg(c, err); 483 } 484 Z3_set_ast_print_mode(Z3_context c,Z3_ast_print_mode mode)485 void Z3_API Z3_set_ast_print_mode(Z3_context c, Z3_ast_print_mode mode) { 486 Z3_TRY; 487 LOG_Z3_set_ast_print_mode(c, mode); 488 RESET_ERROR_CODE(); 489 mk_c(c)->set_print_mode(mode); 490 Z3_CATCH; 491 } 492 493 }; 494