| 468 | } |
| 469 | |
| 470 | Result Solver::check(const char *query_name, bool dont_skip) const { |
| 471 | if (!valid) { |
| 472 | ++num_invalid; |
| 473 | return Result::INVALID; |
| 474 | } |
| 475 | |
| 476 | if (is_unsat) { |
| 477 | ++num_trivial; |
| 478 | return Result::UNSAT; |
| 479 | } |
| 480 | |
| 481 | if (!config::smt_benchmark_dir.empty()) { |
| 482 | const char *banner = |
| 483 | R"(Alive2 compiler optimization refinement query |
| 484 | ; More info in "Alive2: Bounded Translation Validation for LLVM", PLDI'21.)"; |
| 485 | expr fml = assertions(); |
| 486 | if (!fml.isTrue()) { |
| 487 | auto str = Z3_benchmark_to_smtlib_string(ctx(), banner, nullptr, nullptr, |
| 488 | nullptr, 0, nullptr, fml()); |
| 489 | ofstream file( |
| 490 | get_random_filename(config::smt_benchmark_dir, "smt2", query_name)); |
| 491 | if (!file.is_open()) { |
| 492 | dbg() << "Alive2: Couldn't open smtlib benchmark file!" << endl; |
| 493 | exit(1); |
| 494 | } |
| 495 | file << str; |
| 496 | } |
| 497 | } |
| 498 | |
| 499 | if (config::skip_smt && !dont_skip) { |
| 500 | ++num_skips; |
| 501 | return Result::SKIP; |
| 502 | } |
| 503 | |
| 504 | ++num_queries; |
| 505 | if (print_queries) { |
| 506 | dbg() << "\nSMT query (" << query_name << "):\n" |
| 507 | << Z3_solver_to_string(ctx(), s) << endl; |
| 508 | } |
| 509 | |
| 510 | tactic->check(); |
| 511 | |
| 512 | switch (Z3_solver_check(ctx(), s)) { |
| 513 | case Z3_L_FALSE: |
| 514 | ++num_unsats; |
| 515 | return Result::UNSAT; |
| 516 | case Z3_L_TRUE: |
| 517 | ++num_sats; |
| 518 | return Z3_solver_get_model(ctx(), s); |
| 519 | case Z3_L_UNDEF: { |
| 520 | string_view reason = Z3_solver_get_reason_unknown(ctx(), s); |
| 521 | if (reason == "timeout") { |
| 522 | ++num_timeout; |
| 523 | return Result::TIMEOUT; |
| 524 | } |
| 525 | ++num_errors; |
| 526 | return { Result::ERROR, string(reason) }; |
| 527 | } |
no test coverage detected