1 /*++ 2 Copyright (c) 2012 Microsoft Corporation 3 4 Module Name: 5 6 api_solver.cpp 7 8 Abstract: 9 10 Solver API 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2012-03-07. 15 16 Revision History: 17 18 --*/ 19 #include<iostream> 20 #include "util/scoped_ctrl_c.h" 21 #include "util/cancel_eh.h" 22 #include "util/file_path.h" 23 #include "util/scoped_timer.h" 24 #include "util/file_path.h" 25 #include "ast/ast_pp.h" 26 #include "api/z3.h" 27 #include "api/api_log_macros.h" 28 #include "api/api_context.h" 29 #include "api/api_tactic.h" 30 #include "api/api_solver.h" 31 #include "api/api_model.h" 32 #include "api/api_stats.h" 33 #include "api/api_ast_vector.h" 34 #include "model/model_params.hpp" 35 #include "smt/smt_solver.h" 36 #include "smt/smt_implied_equalities.h" 37 #include "solver/smt_logics.h" 38 #include "solver/tactic2solver.h" 39 #include "solver/solver_params.hpp" 40 #include "cmd_context/cmd_context.h" 41 #include "parsers/smt2/smt2parser.h" 42 #include "sat/dimacs.h" 43 #include "sat/sat_solver.h" 44 #include "sat/tactic/goal2sat.h" 45 46 47 extern "C" { 48 assert_expr(expr * e)49 void solver2smt2_pp::assert_expr(expr* e) { 50 m_pp_util.collect(e); 51 m_pp_util.display_decls(m_out); 52 m_pp_util.display_assert(m_out, e, true); 53 } 54 assert_expr(expr * e,expr * t)55 void solver2smt2_pp::assert_expr(expr* e, expr* t) { 56 m_pp_util.collect(e); 57 m_pp_util.collect(t); 58 m_pp_util.display_decls(m_out); 59 m_pp_util.display_assert_and_track(m_out, e, t, true); 60 m_tracked.push_back(t); 61 } 62 push()63 void solver2smt2_pp::push() { 64 m_out << "(push 1)\n"; 65 m_pp_util.push(); 66 m_tracked_lim.push_back(m_tracked.size()); 67 } 68 pop(unsigned n)69 void solver2smt2_pp::pop(unsigned n) { 70 m_out << "(pop " << n << ")\n"; 71 m_pp_util.pop(n); 72 m_tracked.shrink(m_tracked_lim[m_tracked_lim.size() - n]); 73 m_tracked_lim.shrink(m_tracked_lim.size() - n); 74 } 75 reset()76 void solver2smt2_pp::reset() { 77 m_out << "(reset)\n"; 78 m_pp_util.reset(); 79 } 80 check(unsigned n,expr * const * asms)81 void solver2smt2_pp::check(unsigned n, expr* const* asms) { 82 for (unsigned i = 0; i < n; ++i) 83 m_pp_util.collect(asms[i]); 84 m_pp_util.display_decls(m_out); 85 m_out << "(check-sat"; 86 for (unsigned i = 0; i < n; ++i) 87 m_pp_util.display_expr(m_out << "\n", asms[i]); 88 for (expr* e : m_tracked) 89 m_pp_util.display_expr(m_out << "\n", e); 90 m_out << ")\n"; 91 m_out.flush(); 92 } 93 get_consequences(expr_ref_vector const & assumptions,expr_ref_vector const & variables)94 void solver2smt2_pp::get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& variables) { 95 for (expr* a : assumptions) 96 m_pp_util.collect(a); 97 for (expr* v : variables) 98 m_pp_util.collect(v); 99 m_pp_util.display_decls(m_out); 100 m_out << "(get-consequences ("; 101 for (expr* f : assumptions) { 102 m_out << "\n"; 103 m_pp_util.display_expr(m_out, f); 104 } 105 m_out << ") ("; 106 for (expr* f : variables) { 107 m_out << "\n"; 108 m_pp_util.display_expr(m_out, f); 109 } 110 m_out << "))\n"; 111 m_out.flush(); 112 } 113 solver2smt2_pp(ast_manager & m,const std::string & file)114 solver2smt2_pp::solver2smt2_pp(ast_manager& m, const std::string& file): 115 m_pp_util(m), m_out(file), m_tracked(m) { 116 if (!m_out) { 117 throw default_exception("could not open " + file + " for output"); 118 } 119 } 120 set_eh(event_handler * eh)121 void Z3_solver_ref::set_eh(event_handler* eh) { 122 lock_guard lock(m_mux); 123 m_eh = eh; 124 } 125 set_cancel()126 void Z3_solver_ref::set_cancel() { 127 lock_guard lock(m_mux); 128 if (m_eh) (*m_eh)(API_INTERRUPT_EH_CALLER); 129 } 130 assert_expr(expr * e)131 void Z3_solver_ref::assert_expr(expr * e) { 132 if (m_pp) m_pp->assert_expr(e); 133 m_solver->assert_expr(e); 134 } 135 assert_expr(expr * e,expr * t)136 void Z3_solver_ref::assert_expr(expr * e, expr* t) { 137 if (m_pp) m_pp->assert_expr(e, t); 138 m_solver->assert_expr(e, t); 139 } 140 init_solver_core(Z3_context c,Z3_solver _s)141 static void init_solver_core(Z3_context c, Z3_solver _s) { 142 Z3_solver_ref * s = to_solver(_s); 143 bool proofs_enabled, models_enabled, unsat_core_enabled; 144 params_ref p = s->m_params; 145 mk_c(c)->params().get_solver_params(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled); 146 s->m_solver = (*(s->m_solver_factory))(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled, s->m_logic); 147 148 param_descrs r; 149 s->m_solver->collect_param_descrs(r); 150 context_params::collect_solver_param_descrs(r); 151 p.validate(r); 152 s->m_solver->updt_params(p); 153 } 154 init_solver(Z3_context c,Z3_solver s)155 static void init_solver(Z3_context c, Z3_solver s) { 156 if (to_solver(s)->m_solver.get() == nullptr) 157 init_solver_core(c, s); 158 } 159 init_solver_log(Z3_context c,Z3_solver s)160 static void init_solver_log(Z3_context c, Z3_solver s) { 161 solver_params sp(to_solver(s)->m_params); 162 symbol smt2log = sp.smtlib2_log(); 163 if (smt2log.is_non_empty_string() && !to_solver(s)->m_pp) { 164 to_solver(s)->m_pp = alloc(solver2smt2_pp, mk_c(c)->m(), smt2log.str()); 165 } 166 } 167 Z3_mk_simple_solver(Z3_context c)168 Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c) { 169 Z3_TRY; 170 LOG_Z3_mk_simple_solver(c); 171 RESET_ERROR_CODE(); 172 Z3_solver_ref * s = alloc(Z3_solver_ref, *mk_c(c), mk_smt_solver_factory()); 173 mk_c(c)->save_object(s); 174 Z3_solver r = of_solver(s); 175 init_solver_log(c, r); 176 RETURN_Z3(r); 177 Z3_CATCH_RETURN(nullptr); 178 } 179 Z3_mk_solver(Z3_context c)180 Z3_solver Z3_API Z3_mk_solver(Z3_context c) { 181 Z3_TRY; 182 LOG_Z3_mk_solver(c); 183 RESET_ERROR_CODE(); 184 Z3_solver_ref * s = alloc(Z3_solver_ref, *mk_c(c), mk_smt_strategic_solver_factory()); 185 mk_c(c)->save_object(s); 186 Z3_solver r = of_solver(s); 187 init_solver_log(c, r); 188 RETURN_Z3(r); 189 Z3_CATCH_RETURN(nullptr); 190 } 191 Z3_mk_solver_for_logic(Z3_context c,Z3_symbol logic)192 Z3_solver Z3_API Z3_mk_solver_for_logic(Z3_context c, Z3_symbol logic) { 193 Z3_TRY; 194 LOG_Z3_mk_solver_for_logic(c, logic); 195 RESET_ERROR_CODE(); 196 if (!smt_logics::supported_logic(to_symbol(logic))) { 197 std::ostringstream strm; 198 strm << "logic '" << to_symbol(logic) << "' is not recognized"; 199 throw default_exception(strm.str()); 200 RETURN_Z3(nullptr); 201 } 202 else { 203 Z3_solver_ref * s = alloc(Z3_solver_ref, *mk_c(c), mk_smt_strategic_solver_factory(to_symbol(logic))); 204 mk_c(c)->save_object(s); 205 Z3_solver r = of_solver(s); 206 init_solver_log(c, r); 207 RETURN_Z3(r); 208 } 209 Z3_CATCH_RETURN(nullptr); 210 } 211 Z3_mk_solver_from_tactic(Z3_context c,Z3_tactic t)212 Z3_solver Z3_API Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t) { 213 Z3_TRY; 214 LOG_Z3_mk_solver_from_tactic(c, t); 215 RESET_ERROR_CODE(); 216 Z3_solver_ref * s = alloc(Z3_solver_ref, *mk_c(c), mk_tactic2solver_factory(to_tactic_ref(t))); 217 mk_c(c)->save_object(s); 218 Z3_solver r = of_solver(s); 219 init_solver_log(c, r); 220 RETURN_Z3(r); 221 Z3_CATCH_RETURN(nullptr); 222 } 223 Z3_solver_translate(Z3_context c,Z3_solver s,Z3_context target)224 Z3_solver Z3_API Z3_solver_translate(Z3_context c, Z3_solver s, Z3_context target) { 225 Z3_TRY; 226 LOG_Z3_solver_translate(c, s, target); 227 RESET_ERROR_CODE(); 228 params_ref const& p = to_solver(s)->m_params; 229 Z3_solver_ref * sr = alloc(Z3_solver_ref, *mk_c(target), nullptr); 230 init_solver(c, s); 231 sr->m_solver = to_solver(s)->m_solver->translate(mk_c(target)->m(), p); 232 mk_c(target)->save_object(sr); 233 Z3_solver r = of_solver(sr); 234 init_solver_log(target, r); 235 RETURN_Z3(r); 236 Z3_CATCH_RETURN(nullptr); 237 } 238 239 Z3_solver_import_model_converter(Z3_context c,Z3_solver src,Z3_solver dst)240 void Z3_API Z3_solver_import_model_converter(Z3_context c, Z3_solver src, Z3_solver dst) { 241 Z3_TRY; 242 LOG_Z3_solver_import_model_converter(c, src, dst); 243 model_converter_ref mc = to_solver_ref(src)->get_model_converter(); 244 to_solver_ref(dst)->set_model_converter(mc.get()); 245 Z3_CATCH; 246 } 247 solver_from_stream(Z3_context c,Z3_solver s,std::istream & is)248 void solver_from_stream(Z3_context c, Z3_solver s, std::istream& is) { 249 scoped_ptr<cmd_context> ctx = alloc(cmd_context, false, &(mk_c(c)->m())); 250 ctx->set_ignore_check(true); 251 std::stringstream errstrm; 252 ctx->set_regular_stream(errstrm); 253 254 if (!parse_smt2_commands(*ctx.get(), is)) { 255 ctx = nullptr; 256 SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str()); 257 return; 258 } 259 260 bool initialized = to_solver(s)->m_solver.get() != nullptr; 261 if (!initialized) 262 init_solver(c, s); 263 for (expr* e : ctx->tracked_assertions()) 264 to_solver(s)->assert_expr(e); 265 to_solver_ref(s)->set_model_converter(ctx->get_model_converter()); 266 } 267 solver_from_dimacs_stream(Z3_context c,Z3_solver s,std::istream & is)268 static void solver_from_dimacs_stream(Z3_context c, Z3_solver s, std::istream& is) { 269 init_solver(c, s); 270 ast_manager& m = to_solver_ref(s)->get_manager(); 271 std::stringstream err; 272 sat::solver solver(to_solver_ref(s)->get_params(), m.limit()); 273 if (!parse_dimacs(is, err, solver)) { 274 SET_ERROR_CODE(Z3_PARSER_ERROR, err.str()); 275 return; 276 } 277 sat2goal s2g; 278 ref<sat2goal::mc> mc; 279 atom2bool_var a2b(m); 280 for (unsigned v = 0; v < solver.num_vars(); ++v) { 281 a2b.insert(m.mk_const(symbol(v), m.mk_bool_sort()), v); 282 } 283 goal g(m); 284 s2g(solver, a2b, to_solver_ref(s)->get_params(), g, mc); 285 for (unsigned i = 0; i < g.size(); ++i) { 286 to_solver(s)->assert_expr(g.form(i)); 287 } 288 } 289 290 // DIMACS files start with "p cnf" and number of variables/clauses. 291 // This is not legal SMT syntax, so use the DIMACS parser. is_dimacs_string(Z3_string c_str)292 static bool is_dimacs_string(Z3_string c_str) { 293 return c_str[0] == 'p' && c_str[1] == ' ' && c_str[2] == 'c'; 294 } 295 Z3_solver_from_string(Z3_context c,Z3_solver s,Z3_string c_str)296 void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string c_str) { 297 Z3_TRY; 298 LOG_Z3_solver_from_string(c, s, c_str); 299 std::string str(c_str); 300 std::istringstream is(str); 301 if (is_dimacs_string(c_str)) { 302 solver_from_dimacs_stream(c, s, is); 303 } 304 else { 305 solver_from_stream(c, s, is); 306 } 307 Z3_CATCH; 308 } 309 Z3_solver_from_file(Z3_context c,Z3_solver s,Z3_string file_name)310 void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name) { 311 Z3_TRY; 312 LOG_Z3_solver_from_file(c, s, file_name); 313 char const* ext = get_extension(file_name); 314 std::ifstream is(file_name); 315 init_solver(c, s); 316 if (!is) { 317 SET_ERROR_CODE(Z3_FILE_ACCESS_ERROR, nullptr); 318 } 319 else if (ext && (std::string("dimacs") == ext || std::string("cnf") == ext)) { 320 solver_from_dimacs_stream(c, s, is); 321 } 322 else { 323 solver_from_stream(c, s, is); 324 } 325 Z3_CATCH; 326 } 327 Z3_solver_get_help(Z3_context c,Z3_solver s)328 Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s) { 329 Z3_TRY; 330 LOG_Z3_solver_get_help(c, s); 331 RESET_ERROR_CODE(); 332 std::ostringstream buffer; 333 param_descrs descrs; 334 bool initialized = to_solver(s)->m_solver.get() != nullptr; 335 if (!initialized) 336 init_solver(c, s); 337 to_solver_ref(s)->collect_param_descrs(descrs); 338 context_params::collect_solver_param_descrs(descrs); 339 if (!initialized) 340 to_solver(s)->m_solver = nullptr; 341 descrs.display(buffer); 342 return mk_c(c)->mk_external_string(buffer.str()); 343 Z3_CATCH_RETURN(""); 344 } 345 Z3_solver_get_param_descrs(Z3_context c,Z3_solver s)346 Z3_param_descrs Z3_API Z3_solver_get_param_descrs(Z3_context c, Z3_solver s) { 347 Z3_TRY; 348 LOG_Z3_solver_get_param_descrs(c, s); 349 RESET_ERROR_CODE(); 350 Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref, *mk_c(c)); 351 mk_c(c)->save_object(d); 352 bool initialized = to_solver(s)->m_solver.get() != nullptr; 353 if (!initialized) 354 init_solver(c, s); 355 to_solver_ref(s)->collect_param_descrs(d->m_descrs); 356 context_params::collect_solver_param_descrs(d->m_descrs); 357 if (!initialized) 358 to_solver(s)->m_solver = nullptr; 359 Z3_param_descrs r = of_param_descrs(d); 360 RETURN_Z3(r); 361 Z3_CATCH_RETURN(nullptr); 362 } 363 364 Z3_solver_set_params(Z3_context c,Z3_solver s,Z3_params p)365 void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p) { 366 Z3_TRY; 367 LOG_Z3_solver_set_params(c, s, p); 368 RESET_ERROR_CODE(); 369 370 auto ¶ms = to_param_ref(p); 371 symbol logic = params.get_sym("smt.logic", symbol::null); 372 if (logic != symbol::null) { 373 to_solver(s)->m_logic = logic; 374 } 375 if (to_solver(s)->m_solver) { 376 bool old_model = to_solver(s)->m_params.get_bool("model", true); 377 bool new_model = params.get_bool("model", true); 378 if (old_model != new_model) 379 to_solver_ref(s)->set_produce_models(new_model); 380 param_descrs r; 381 to_solver_ref(s)->collect_param_descrs(r); 382 context_params::collect_solver_param_descrs(r); 383 params.validate(r); 384 to_solver_ref(s)->updt_params(params); 385 } 386 to_solver(s)->m_params.append(params); 387 388 init_solver_log(c, s); 389 390 Z3_CATCH; 391 } 392 Z3_solver_inc_ref(Z3_context c,Z3_solver s)393 void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s) { 394 Z3_TRY; 395 LOG_Z3_solver_inc_ref(c, s); 396 RESET_ERROR_CODE(); 397 to_solver(s)->inc_ref(); 398 Z3_CATCH; 399 } 400 Z3_solver_dec_ref(Z3_context c,Z3_solver s)401 void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s) { 402 Z3_TRY; 403 LOG_Z3_solver_dec_ref(c, s); 404 RESET_ERROR_CODE(); 405 to_solver(s)->dec_ref(); 406 Z3_CATCH; 407 } 408 Z3_solver_push(Z3_context c,Z3_solver s)409 void Z3_API Z3_solver_push(Z3_context c, Z3_solver s) { 410 Z3_TRY; 411 LOG_Z3_solver_push(c, s); 412 RESET_ERROR_CODE(); 413 init_solver(c, s); 414 to_solver_ref(s)->push(); 415 if (to_solver(s)->m_pp) to_solver(s)->m_pp->push(); 416 Z3_CATCH; 417 } 418 Z3_solver_interrupt(Z3_context c,Z3_solver s)419 void Z3_API Z3_solver_interrupt(Z3_context c, Z3_solver s) { 420 to_solver(s)->set_cancel(); 421 } 422 Z3_solver_pop(Z3_context c,Z3_solver s,unsigned n)423 void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n) { 424 Z3_TRY; 425 LOG_Z3_solver_pop(c, s, n); 426 RESET_ERROR_CODE(); 427 init_solver(c, s); 428 if (n > to_solver_ref(s)->get_scope_level()) { 429 SET_ERROR_CODE(Z3_IOB, nullptr); 430 return; 431 } 432 if (n > 0) { 433 to_solver_ref(s)->pop(n); 434 if (to_solver(s)->m_pp) to_solver(s)->m_pp->pop(n); 435 } 436 Z3_CATCH; 437 } 438 Z3_solver_reset(Z3_context c,Z3_solver s)439 void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s) { 440 Z3_TRY; 441 LOG_Z3_solver_reset(c, s); 442 RESET_ERROR_CODE(); 443 to_solver(s)->m_solver = nullptr; 444 if (to_solver(s)->m_pp) to_solver(s)->m_pp->reset(); 445 Z3_CATCH; 446 } 447 Z3_solver_get_num_scopes(Z3_context c,Z3_solver s)448 unsigned Z3_API Z3_solver_get_num_scopes(Z3_context c, Z3_solver s) { 449 Z3_TRY; 450 LOG_Z3_solver_get_num_scopes(c, s); 451 RESET_ERROR_CODE(); 452 init_solver(c, s); 453 return to_solver_ref(s)->get_scope_level(); 454 Z3_CATCH_RETURN(0); 455 } 456 Z3_solver_assert(Z3_context c,Z3_solver s,Z3_ast a)457 void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a) { 458 Z3_TRY; 459 LOG_Z3_solver_assert(c, s, a); 460 RESET_ERROR_CODE(); 461 init_solver(c, s); 462 CHECK_FORMULA(a,); 463 to_solver(s)->assert_expr(to_expr(a)); 464 Z3_CATCH; 465 } 466 Z3_solver_assert_and_track(Z3_context c,Z3_solver s,Z3_ast a,Z3_ast p)467 void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p) { 468 Z3_TRY; 469 LOG_Z3_solver_assert_and_track(c, s, a, p); 470 RESET_ERROR_CODE(); 471 init_solver(c, s); 472 CHECK_FORMULA(a,); 473 CHECK_FORMULA(p,); 474 to_solver(s)->assert_expr(to_expr(a), to_expr(p)); 475 Z3_CATCH; 476 } 477 478 Z3_solver_get_assertions(Z3_context c,Z3_solver s)479 Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s) { 480 Z3_TRY; 481 LOG_Z3_solver_get_assertions(c, s); 482 RESET_ERROR_CODE(); 483 init_solver(c, s); 484 Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); 485 mk_c(c)->save_object(v); 486 unsigned sz = to_solver_ref(s)->get_num_assertions(); 487 for (unsigned i = 0; i < sz; i++) { 488 v->m_ast_vector.push_back(to_solver_ref(s)->get_assertion(i)); 489 } 490 RETURN_Z3(of_ast_vector(v)); 491 Z3_CATCH_RETURN(nullptr); 492 } 493 494 Z3_solver_get_units(Z3_context c,Z3_solver s)495 Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s) { 496 Z3_TRY; 497 LOG_Z3_solver_get_units(c, s); 498 RESET_ERROR_CODE(); 499 init_solver(c, s); 500 Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); 501 mk_c(c)->save_object(v); 502 expr_ref_vector fmls = to_solver_ref(s)->get_units(); 503 for (expr* f : fmls) { 504 v->m_ast_vector.push_back(f); 505 } 506 RETURN_Z3(of_ast_vector(v)); 507 Z3_CATCH_RETURN(nullptr); 508 } 509 Z3_solver_get_non_units(Z3_context c,Z3_solver s)510 Z3_ast_vector Z3_API Z3_solver_get_non_units(Z3_context c, Z3_solver s) { 511 Z3_TRY; 512 LOG_Z3_solver_get_non_units(c, s); 513 RESET_ERROR_CODE(); 514 init_solver(c, s); 515 Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); 516 mk_c(c)->save_object(v); 517 expr_ref_vector fmls = to_solver_ref(s)->get_non_units(); 518 for (expr* f : fmls) { 519 v->m_ast_vector.push_back(f); 520 } 521 RETURN_Z3(of_ast_vector(v)); 522 Z3_CATCH_RETURN(nullptr); 523 } 524 Z3_solver_get_levels(Z3_context c,Z3_solver s,Z3_ast_vector literals,unsigned sz,unsigned levels[])525 void Z3_API Z3_solver_get_levels(Z3_context c, Z3_solver s, Z3_ast_vector literals, unsigned sz, unsigned levels[]) { 526 Z3_TRY; 527 LOG_Z3_solver_get_levels(c, s, literals, sz, levels); 528 RESET_ERROR_CODE(); 529 init_solver(c, s); 530 if (sz != Z3_ast_vector_size(c, literals)) { 531 SET_ERROR_CODE(Z3_IOB, nullptr); 532 return; 533 } 534 ptr_vector<expr> _vars; 535 for (unsigned i = 0; i < sz; ++i) { 536 expr* e = to_expr(Z3_ast_vector_get(c, literals, i)); 537 mk_c(c)->m().is_not(e, e); 538 _vars.push_back(e); 539 } 540 unsigned_vector _levels(sz); 541 to_solver_ref(s)->get_levels(_vars, _levels); 542 for (unsigned i = 0; i < sz; ++i) { 543 levels[i] = _levels[i]; 544 } 545 Z3_CATCH; 546 } 547 Z3_solver_get_trail(Z3_context c,Z3_solver s)548 Z3_ast_vector Z3_API Z3_solver_get_trail(Z3_context c, Z3_solver s) { 549 Z3_TRY; 550 LOG_Z3_solver_get_trail(c, s); 551 RESET_ERROR_CODE(); 552 init_solver(c, s); 553 Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); 554 mk_c(c)->save_object(v); 555 expr_ref_vector trail = to_solver_ref(s)->get_trail(); 556 for (expr* f : trail) { 557 v->m_ast_vector.push_back(f); 558 } 559 RETURN_Z3(of_ast_vector(v)); 560 Z3_CATCH_RETURN(nullptr); 561 } 562 _solver_check(Z3_context c,Z3_solver s,unsigned num_assumptions,Z3_ast const assumptions[])563 static Z3_lbool _solver_check(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[]) { 564 for (unsigned i = 0; i < num_assumptions; i++) { 565 if (!is_expr(to_ast(assumptions[i]))) { 566 SET_ERROR_CODE(Z3_INVALID_ARG, "assumption is not an expression"); 567 return Z3_L_UNDEF; 568 } 569 } 570 expr * const * _assumptions = to_exprs(num_assumptions, assumptions); 571 solver_params sp(to_solver(s)->m_params); 572 unsigned timeout = mk_c(c)->get_timeout(); 573 timeout = to_solver(s)->m_params.get_uint("timeout", timeout); 574 timeout = sp.timeout() != UINT_MAX ? sp.timeout() : timeout; 575 unsigned rlimit = to_solver(s)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit()); 576 bool use_ctrl_c = to_solver(s)->m_params.get_bool("ctrl_c", true); 577 cancel_eh<reslimit> eh(mk_c(c)->m().limit()); 578 to_solver(s)->set_eh(&eh); 579 api::context::set_interruptable si(*(mk_c(c)), eh); 580 lbool result = l_undef; 581 { 582 scoped_ctrl_c ctrlc(eh, false, use_ctrl_c); 583 scoped_timer timer(timeout, &eh); 584 scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit); 585 try { 586 if (to_solver(s)->m_pp) to_solver(s)->m_pp->check(num_assumptions, _assumptions); 587 result = to_solver_ref(s)->check_sat(num_assumptions, _assumptions); 588 } 589 catch (z3_exception & ex) { 590 to_solver_ref(s)->set_reason_unknown(eh); 591 to_solver(s)->set_eh(nullptr); 592 if (mk_c(c)->m().inc()) { 593 mk_c(c)->handle_exception(ex); 594 } 595 return Z3_L_UNDEF; 596 } 597 catch (...) { 598 to_solver_ref(s)->set_reason_unknown(eh); 599 to_solver(s)->set_eh(nullptr); 600 return Z3_L_UNDEF; 601 } 602 } 603 to_solver(s)->set_eh(nullptr); 604 if (result == l_undef) { 605 to_solver_ref(s)->set_reason_unknown(eh); 606 } 607 return static_cast<Z3_lbool>(result); 608 } 609 Z3_solver_check(Z3_context c,Z3_solver s)610 Z3_lbool Z3_API Z3_solver_check(Z3_context c, Z3_solver s) { 611 Z3_TRY; 612 LOG_Z3_solver_check(c, s); 613 RESET_ERROR_CODE(); 614 init_solver(c, s); 615 return _solver_check(c, s, 0, nullptr); 616 Z3_CATCH_RETURN(Z3_L_UNDEF); 617 } 618 Z3_solver_check_assumptions(Z3_context c,Z3_solver s,unsigned num_assumptions,Z3_ast const assumptions[])619 Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[]) { 620 Z3_TRY; 621 LOG_Z3_solver_check_assumptions(c, s, num_assumptions, assumptions); 622 RESET_ERROR_CODE(); 623 init_solver(c, s); 624 return _solver_check(c, s, num_assumptions, assumptions); 625 Z3_CATCH_RETURN(Z3_L_UNDEF); 626 } 627 Z3_solver_get_model(Z3_context c,Z3_solver s)628 Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s) { 629 Z3_TRY; 630 LOG_Z3_solver_get_model(c, s); 631 RESET_ERROR_CODE(); 632 init_solver(c, s); 633 model_ref _m; 634 to_solver_ref(s)->get_model(_m); 635 if (!_m) { 636 SET_ERROR_CODE(Z3_INVALID_USAGE, "there is no current model"); 637 RETURN_Z3(nullptr); 638 } 639 if (_m) { 640 model_params mp(to_solver_ref(s)->get_params()); 641 if (mp.compact()) _m->compress(); 642 } 643 Z3_model_ref * m_ref = alloc(Z3_model_ref, *mk_c(c)); 644 m_ref->m_model = _m; 645 mk_c(c)->save_object(m_ref); 646 RETURN_Z3(of_model(m_ref)); 647 Z3_CATCH_RETURN(nullptr); 648 } 649 Z3_solver_get_proof(Z3_context c,Z3_solver s)650 Z3_ast Z3_API Z3_solver_get_proof(Z3_context c, Z3_solver s) { 651 Z3_TRY; 652 LOG_Z3_solver_get_proof(c, s); 653 RESET_ERROR_CODE(); 654 init_solver(c, s); 655 proof * p = to_solver_ref(s)->get_proof(); 656 if (!p) { 657 SET_ERROR_CODE(Z3_INVALID_USAGE, "there is no current proof"); 658 RETURN_Z3(nullptr); 659 } 660 mk_c(c)->save_ast_trail(p); 661 RETURN_Z3(of_ast(p)); 662 Z3_CATCH_RETURN(nullptr); 663 } 664 Z3_solver_get_unsat_core(Z3_context c,Z3_solver s)665 Z3_ast_vector Z3_API Z3_solver_get_unsat_core(Z3_context c, Z3_solver s) { 666 Z3_TRY; 667 LOG_Z3_solver_get_unsat_core(c, s); 668 RESET_ERROR_CODE(); 669 init_solver(c, s); 670 expr_ref_vector core(mk_c(c)->m()); 671 to_solver_ref(s)->get_unsat_core(core); 672 Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); 673 mk_c(c)->save_object(v); 674 for (expr* e : core) { 675 v->m_ast_vector.push_back(e); 676 } 677 RETURN_Z3(of_ast_vector(v)); 678 Z3_CATCH_RETURN(nullptr); 679 } 680 Z3_solver_get_reason_unknown(Z3_context c,Z3_solver s)681 Z3_string Z3_API Z3_solver_get_reason_unknown(Z3_context c, Z3_solver s) { 682 Z3_TRY; 683 LOG_Z3_solver_get_reason_unknown(c, s); 684 RESET_ERROR_CODE(); 685 init_solver(c, s); 686 return mk_c(c)->mk_external_string(to_solver_ref(s)->reason_unknown()); 687 Z3_CATCH_RETURN(""); 688 } 689 Z3_solver_get_statistics(Z3_context c,Z3_solver s)690 Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s) { 691 Z3_TRY; 692 LOG_Z3_solver_get_statistics(c, s); 693 RESET_ERROR_CODE(); 694 init_solver(c, s); 695 Z3_stats_ref * st = alloc(Z3_stats_ref, *mk_c(c)); 696 to_solver_ref(s)->collect_statistics(st->m_stats); 697 get_memory_statistics(st->m_stats); 698 get_rlimit_statistics(mk_c(c)->m().limit(), st->m_stats); 699 to_solver_ref(s)->collect_timer_stats(st->m_stats); 700 mk_c(c)->save_object(st); 701 Z3_stats r = of_stats(st); 702 RETURN_Z3(r); 703 Z3_CATCH_RETURN(nullptr); 704 } 705 Z3_solver_to_string(Z3_context c,Z3_solver s)706 Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s) { 707 Z3_TRY; 708 LOG_Z3_solver_to_string(c, s); 709 RESET_ERROR_CODE(); 710 init_solver(c, s); 711 std::ostringstream buffer; 712 to_solver_ref(s)->display(buffer); 713 return mk_c(c)->mk_external_string(buffer.str()); 714 Z3_CATCH_RETURN(""); 715 } 716 Z3_solver_to_dimacs_string(Z3_context c,Z3_solver s,bool include_names)717 Z3_string Z3_API Z3_solver_to_dimacs_string(Z3_context c, Z3_solver s, bool include_names) { 718 Z3_TRY; 719 LOG_Z3_solver_to_string(c, s); 720 RESET_ERROR_CODE(); 721 init_solver(c, s); 722 std::ostringstream buffer; 723 to_solver_ref(s)->display_dimacs(buffer, include_names); 724 return mk_c(c)->mk_external_string(buffer.str()); 725 Z3_CATCH_RETURN(""); 726 } 727 728 Z3_get_implied_equalities(Z3_context c,Z3_solver s,unsigned num_terms,Z3_ast const terms[],unsigned class_ids[])729 Z3_lbool Z3_API Z3_get_implied_equalities(Z3_context c, 730 Z3_solver s, 731 unsigned num_terms, 732 Z3_ast const terms[], 733 unsigned class_ids[]) { 734 Z3_TRY; 735 LOG_Z3_get_implied_equalities(c, s, num_terms, terms, class_ids); 736 ast_manager& m = mk_c(c)->m(); 737 RESET_ERROR_CODE(); 738 CHECK_SEARCHING(c); 739 init_solver(c, s); 740 lbool result = smt::implied_equalities(m, *to_solver_ref(s), num_terms, to_exprs(num_terms, terms), class_ids); 741 return static_cast<Z3_lbool>(result); 742 Z3_CATCH_RETURN(Z3_L_UNDEF); 743 } 744 Z3_solver_get_consequences(Z3_context c,Z3_solver s,Z3_ast_vector assumptions,Z3_ast_vector variables,Z3_ast_vector consequences)745 Z3_lbool Z3_API Z3_solver_get_consequences(Z3_context c, 746 Z3_solver s, 747 Z3_ast_vector assumptions, 748 Z3_ast_vector variables, 749 Z3_ast_vector consequences) { 750 Z3_TRY; 751 LOG_Z3_solver_get_consequences(c, s, assumptions, variables, consequences); 752 ast_manager& m = mk_c(c)->m(); 753 RESET_ERROR_CODE(); 754 CHECK_SEARCHING(c); 755 init_solver(c, s); 756 expr_ref_vector _assumptions(m), _consequences(m), _variables(m); 757 ast_ref_vector const& __assumptions = to_ast_vector_ref(assumptions); 758 for (ast* e : __assumptions) { 759 if (!is_expr(e)) { 760 _assumptions.finalize(); _consequences.finalize(); _variables.finalize(); 761 SET_ERROR_CODE(Z3_INVALID_USAGE, "assumption is not an expression"); 762 return Z3_L_UNDEF; 763 } 764 _assumptions.push_back(to_expr(e)); 765 } 766 ast_ref_vector const& __variables = to_ast_vector_ref(variables); 767 for (ast* a : __variables) { 768 if (!is_expr(a)) { 769 _assumptions.finalize(); _consequences.finalize(); _variables.finalize(); 770 SET_ERROR_CODE(Z3_INVALID_USAGE, "variable is not an expression"); 771 return Z3_L_UNDEF; 772 } 773 _variables.push_back(to_expr(a)); 774 } 775 lbool result = l_undef; 776 unsigned timeout = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout()); 777 unsigned rlimit = to_solver(s)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit()); 778 bool use_ctrl_c = to_solver(s)->m_params.get_bool("ctrl_c", true); 779 cancel_eh<reslimit> eh(mk_c(c)->m().limit()); 780 to_solver(s)->set_eh(&eh); 781 api::context::set_interruptable si(*(mk_c(c)), eh); 782 { 783 scoped_ctrl_c ctrlc(eh, false, use_ctrl_c); 784 scoped_timer timer(timeout, &eh); 785 scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit); 786 try { 787 if (to_solver(s)->m_pp) to_solver(s)->m_pp->get_consequences(_assumptions, _variables); 788 result = to_solver_ref(s)->get_consequences(_assumptions, _variables, _consequences); 789 } 790 catch (z3_exception & ex) { 791 to_solver(s)->set_eh(nullptr); 792 to_solver_ref(s)->set_reason_unknown(eh); 793 _assumptions.finalize(); _consequences.finalize(); _variables.finalize(); 794 mk_c(c)->handle_exception(ex); 795 return Z3_L_UNDEF; 796 } 797 catch (...) { 798 } 799 } 800 to_solver(s)->set_eh(nullptr); 801 if (result == l_undef) { 802 to_solver_ref(s)->set_reason_unknown(eh); 803 } 804 for (expr* e : _consequences) { 805 to_ast_vector_ref(consequences).push_back(e); 806 } 807 return static_cast<Z3_lbool>(result); 808 Z3_CATCH_RETURN(Z3_L_UNDEF); 809 } 810 Z3_solver_cube(Z3_context c,Z3_solver s,Z3_ast_vector vs,unsigned cutoff)811 Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, Z3_ast_vector vs, unsigned cutoff) { 812 Z3_TRY; 813 LOG_Z3_solver_cube(c, s, vs, cutoff); 814 ast_manager& m = mk_c(c)->m(); 815 expr_ref_vector result(m), vars(m); 816 for (ast* a : to_ast_vector_ref(vs)) { 817 if (!is_expr(a)) { 818 SET_ERROR_CODE(Z3_INVALID_USAGE, "cube contains a non-expression"); 819 } 820 else { 821 vars.push_back(to_expr(a)); 822 } 823 } 824 unsigned timeout = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout()); 825 unsigned rlimit = to_solver(s)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit()); 826 bool use_ctrl_c = to_solver(s)->m_params.get_bool("ctrl_c", true); 827 cancel_eh<reslimit> eh(mk_c(c)->m().limit()); 828 to_solver(s)->set_eh(&eh); 829 api::context::set_interruptable si(*(mk_c(c)), eh); 830 { 831 scoped_ctrl_c ctrlc(eh, false, use_ctrl_c); 832 scoped_timer timer(timeout, &eh); 833 scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit); 834 try { 835 result.append(to_solver_ref(s)->cube(vars, cutoff)); 836 } 837 catch (z3_exception & ex) { 838 to_solver(s)->set_eh(nullptr); 839 mk_c(c)->handle_exception(ex); 840 return nullptr; 841 } 842 catch (...) { 843 } 844 } 845 to_solver(s)->set_eh(nullptr); 846 Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); 847 mk_c(c)->save_object(v); 848 for (expr* e : result) { 849 v->m_ast_vector.push_back(e); 850 } 851 to_ast_vector_ref(vs).reset(); 852 for (expr* a : vars) { 853 to_ast_vector_ref(vs).push_back(a); 854 } 855 RETURN_Z3(of_ast_vector(v)); 856 Z3_CATCH_RETURN(nullptr); 857 } 858 859 class api_context_obj : public solver::context_obj { 860 api::context* c; 861 public: api_context_obj(api::context * c)862 api_context_obj(api::context* c):c(c) {} ~api_context_obj()863 ~api_context_obj() override { dealloc(c); } 864 }; 865 Z3_solver_propagate_init(Z3_context c,Z3_solver s,void * user_context,Z3_push_eh push_eh,Z3_pop_eh pop_eh,Z3_fresh_eh fresh_eh)866 void Z3_API Z3_solver_propagate_init( 867 Z3_context c, 868 Z3_solver s, 869 void* user_context, 870 Z3_push_eh push_eh, 871 Z3_pop_eh pop_eh, 872 Z3_fresh_eh fresh_eh) { 873 Z3_TRY; 874 RESET_ERROR_CODE(); 875 init_solver(c, s); 876 solver::push_eh_t _push = push_eh; 877 solver::pop_eh_t _pop = pop_eh; 878 solver::fresh_eh_t _fresh = [&](void * user_ctx, ast_manager& m, solver::context_obj*& _ctx) { 879 context_params params; 880 params.set_foreign_manager(&m); 881 auto* ctx = alloc(api::context, ¶ms, false); 882 _ctx = alloc(api_context_obj, ctx); 883 return fresh_eh(user_ctx, reinterpret_cast<Z3_context>(ctx)); 884 }; 885 to_solver_ref(s)->user_propagate_init(user_context, _push, _pop, _fresh); 886 Z3_CATCH; 887 } 888 Z3_solver_propagate_fixed(Z3_context c,Z3_solver s,Z3_fixed_eh fixed_eh)889 void Z3_API Z3_solver_propagate_fixed( 890 Z3_context c, 891 Z3_solver s, 892 Z3_fixed_eh fixed_eh) { 893 Z3_TRY; 894 RESET_ERROR_CODE(); 895 solver::fixed_eh_t _fixed = (void(*)(void*,solver::propagate_callback*,unsigned,expr*))fixed_eh; 896 to_solver_ref(s)->user_propagate_register_fixed(_fixed); 897 Z3_CATCH; 898 } 899 Z3_solver_propagate_final(Z3_context c,Z3_solver s,Z3_final_eh final_eh)900 void Z3_API Z3_solver_propagate_final( 901 Z3_context c, 902 Z3_solver s, 903 Z3_final_eh final_eh) { 904 Z3_TRY; 905 RESET_ERROR_CODE(); 906 solver::final_eh_t _final = (bool(*)(void*,solver::propagate_callback*))final_eh; 907 to_solver_ref(s)->user_propagate_register_final(_final); 908 Z3_CATCH; 909 } 910 Z3_solver_propagate_eq(Z3_context c,Z3_solver s,Z3_eq_eh eq_eh)911 void Z3_API Z3_solver_propagate_eq( 912 Z3_context c, 913 Z3_solver s, 914 Z3_eq_eh eq_eh) { 915 Z3_TRY; 916 RESET_ERROR_CODE(); 917 solver::eq_eh_t _eq = (void(*)(void*,solver::propagate_callback*,unsigned,unsigned))eq_eh; 918 to_solver_ref(s)->user_propagate_register_eq(_eq); 919 Z3_CATCH; 920 } 921 Z3_solver_propagate_diseq(Z3_context c,Z3_solver s,Z3_eq_eh diseq_eh)922 void Z3_API Z3_solver_propagate_diseq( 923 Z3_context c, 924 Z3_solver s, 925 Z3_eq_eh diseq_eh) { 926 Z3_TRY; 927 RESET_ERROR_CODE(); 928 solver::eq_eh_t _diseq = (void(*)(void*,solver::propagate_callback*,unsigned,unsigned))diseq_eh; 929 to_solver_ref(s)->user_propagate_register_diseq(_diseq); 930 Z3_CATCH; 931 } 932 Z3_solver_propagate_register(Z3_context c,Z3_solver s,Z3_ast e)933 unsigned Z3_API Z3_solver_propagate_register(Z3_context c, Z3_solver s, Z3_ast e) { 934 Z3_TRY; 935 LOG_Z3_solver_propagate_register(c, s, e); 936 RESET_ERROR_CODE(); 937 return to_solver_ref(s)->user_propagate_register(to_expr(e)); 938 Z3_CATCH_RETURN(0); 939 } 940 Z3_solver_propagate_consequence(Z3_context c,Z3_solver_callback s,unsigned num_fixed,unsigned const * fixed_ids,unsigned num_eqs,unsigned const * eq_lhs,unsigned const * eq_rhs,Z3_ast conseq)941 void Z3_API Z3_solver_propagate_consequence(Z3_context c, Z3_solver_callback s, unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, Z3_ast conseq) { 942 Z3_TRY; 943 LOG_Z3_solver_propagate_consequence(c, s, num_fixed, fixed_ids, num_eqs, eq_lhs, eq_rhs, conseq); 944 RESET_ERROR_CODE(); 945 reinterpret_cast<solver::propagate_callback*>(s)->propagate_cb(num_fixed, fixed_ids, num_eqs, eq_lhs, eq_rhs, to_expr(conseq)); 946 Z3_CATCH; 947 } 948 949 }; 950