diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 4a232f41eeee..30f4d65affe5 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -231,7 +231,25 @@ void smt2_convt::write_footer() out << "\n"; - if(solver!=solvert::BOOLECTOR) + if(solver == solvert::Z3) + { + // Request the same identifiers in their existing deterministic order, + // using one command instead of a separate command for each identifier. + if(!smt2_identifiers.empty()) + { + out << "(get-value ("; + bool first = true; + for(const auto &id : smt2_identifiers) + { + if(!first) + out << ' '; + first = false; + out << id; + } + out << "))\n"; + } + } + else if(solver != solvert::BOOLECTOR) { // Output get-value commands for all identifiers // Note: smt2_identifiers is std::set, so iteration is deterministic diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index ca94493a6be4..c9bed868e066 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -118,8 +118,8 @@ class smt2_convt : public stack_decision_proceduret /// * The object size definitions. /// * The assertions based on the `assumptions` member variable. /// * The `(check-sat)` or `check-sat-assuming` command. - /// * A `(get-value |identifier|)` command for each of the identifiers in - /// `smt2_convt::smt2_identifiers`. + /// * A get-value request for every identifier in `smt2_identifiers`, + /// grouped into one command for Z3 and omitted for Boolector. /// * An `(exit)` command. void write_footer(); diff --git a/src/solvers/smt2/smt2_dec.cpp b/src/solvers/smt2/smt2_dec.cpp index cbe6ecb8ebc3..2e0b3d0c3c13 100644 --- a/src/solvers/smt2/smt2_dec.cpp +++ b/src/solvers/smt2/smt2_dec.cpp @@ -167,10 +167,19 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in) while(in) { + const auto errors_before = + message_handler.get_message_count(messaget::M_ERROR); auto parsed_opt = smt2irep(in, message_handler); if(!parsed_opt.has_value()) + { + // The parser returns no value for both clean EOF and a syntax error. + if( + solver == solvert::Z3 && + message_handler.get_message_count(messaget::M_ERROR) != errors_before) + return resultt::D_ERROR; break; + } const auto &parsed = parsed_opt.value(); @@ -184,21 +193,6 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in) log.error() << "SMT2 solver returned \"unknown\"" << messaget::eom; return decision_proceduret::resultt::D_ERROR; } - else if( - parsed.id().empty() && parsed.get_sub().size() == 1 && - parsed.get_sub().front().get_sub().size() == 2) - { - const irept &s0=parsed.get_sub().front().get_sub()[0]; - const irept &s1=parsed.get_sub().front().get_sub()[1]; - - // Examples: - // ( (B0 true) ) - // ( (|__CPROVER_pipe_count#1| (_ bv0 32)) ) - // ( (|some_integer| 0) ) - // ( (|some_integer| (- 10)) ) - - parsed_values[s0.id()] = s1; - } else if( parsed.id().empty() && parsed.get_sub().size() == 2 && parsed.get_sub().front().id() == "error") @@ -215,6 +209,31 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in) return decision_proceduret::resultt::D_ERROR; } } + else if( + parsed.id().empty() && (solver == solvert::Z3 || + (parsed.get_sub().size() == 1 && + parsed.get_sub().front().get_sub().size() == 2))) + { + // A get-value response contains one or more (identifier value) pairs. + // Validate every Z3 pair so a malformed tail cannot become a partial + // model. Other solvers retain their existing singleton response handling. + if(parsed.get_sub().empty()) + return resultt::D_ERROR; + for(const auto &pair : parsed.get_sub()) + { + if( + solver == solvert::Z3 && + (!pair.id().empty() || pair.get_sub().size() != 2 || + !pair.get_sub()[0].get_sub().empty())) + { + messaget log{message_handler}; + log.error() << "SMT2 solver returned malformed get-value response" + << messaget::eom; + return resultt::D_ERROR; + } + parsed_values[pair.get_sub()[0].id()] = pair.get_sub()[1]; + } + } } // If the result is not satisfiable don't bother updating the assignments and @@ -224,9 +243,22 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in) for(auto &assignment : identifier_map) { - std::string conv_id = drop_quotes(convert_identifier(assignment.first)); - const irept &value = parsed_values[conv_id]; - assignment.second.value = parse_rec(value, assignment.second.type); + const auto identifier = convert_identifier(assignment.first); + const auto conv_id = drop_quotes(identifier); + const auto value = parsed_values.find(conv_id); + if( + solver == solvert::Z3 && value == parsed_values.end() && + smt2_identifiers.count(identifier) != 0) + { + messaget log{message_handler}; + log.error() << "SMT2 solver omitted value for variable " << conv_id + << messaget::eom; + return resultt::D_ERROR; + } + // Preserve existing handling for identifiers excluded from model queries. + assignment.second.value = parse_rec( + value == parsed_values.end() ? irept{} : value->second, + assignment.second.type); } // Booleans diff --git a/unit/solvers/smt2/smt2_conv.cpp b/unit/solvers/smt2/smt2_conv.cpp index caa69059f9dd..ec968e395832 100644 --- a/unit/solvers/smt2/smt2_conv.cpp +++ b/unit/solvers/smt2/smt2_conv.cpp @@ -20,6 +20,303 @@ #include #include +namespace +{ +/// Expose the existing response reader to supply solver protocol fixtures. +class smt2_result_testt : public smt2_dect +{ +public: + using smt2_dect::read_result; + using smt2_dect::smt2_dect; +}; +} // namespace + +TEST_CASE( + "SMT model queries preserve the identifier set", + "[core][solvers][smt2]") +{ + symbol_tablet symbol_table; + namespacet ns{symbol_table}; + const auto solver = GENERATE( + smt2_convt::solvert::Z3, + smt2_convt::solvert::GENERIC, + smt2_convt::solvert::BITWUZLA, + smt2_convt::solvert::BOOLECTOR, + smt2_convt::solvert::CPROVER_SMT2, + smt2_convt::solvert::CVC5, + smt2_convt::solvert::MATHSAT, + smt2_convt::solvert::YICES); + std::ostringstream output; + smt2_convt converter{ns, "queries", "", "ALL", solver, output}; + std::string expected; + SECTION("Empty") + { + // Q1: no identifiers means no model request, including no empty Z3 query. + } + SECTION("Singleton") + { + // Q2: one identifier keeps exactly the previous singleton request. + const symbol_exprt x{"x", unsignedbv_typet{8}}; + converter.set_to(equal_exprt{x, from_integer(1, x.type())}, true); + expected = "(get-value (x))\n"; + } + SECTION("Multiple, including escaped identifier") + { + // Q3: Z3 batches every identifier in the existing sorted set once; + // Q4: other solvers retain singleton commands, and Boolector retains none. + // Deliberately discover the symbols out of order and include an escaped id. + for(const auto &name : {"x|y", "z", "a"}) + { + const symbol_exprt x{name, unsignedbv_typet{8}}; + converter.set_to(equal_exprt{x, from_integer(1, x.type())}, true); + } + expected = solver == smt2_convt::solvert::Z3 + ? "(get-value (a z |x&124;y|))\n" + : "(get-value (a))\n(get-value (z))\n" + "(get-value (|x&124;y|))\n"; + } + if(solver == smt2_convt::solvert::BOOLECTOR) + expected.clear(); + CHECK(converter() == decision_proceduret::resultt::D_ERROR); + const auto text = output.str(); + const auto check = text.find("(check-sat)\n"); + REQUIRE(check != std::string::npos); + CHECK( + text.substr(check) == + "(check-sat)\n\n" + expected + "\n(exit)\n; end of SMT2 file\n"); +} + +TEST_CASE( + "SMT model responses decode every typed value", + "[core][solvers][smt2]") +{ + symbol_tablet symbol_table; + namespacet ns{symbol_table}; + null_message_handlert messages; + smt2_result_testt solver{ + ns, "results", "", "ALL", smt2_convt::solvert::Z3, "", messages}; + const unsignedbv_typet byte{8}; + const symbol_exprt x{"x|y", byte}; + const symbol_exprt empty_name{"", byte}; + const symbol_exprt number{"number", integer_typet{}}; + const struct_typet record_type{{{"field", byte}}}; + const symbol_exprt record{"record", record_type}; + const array_typet array_type{byte, from_integer(2, unsignedbv_typet{64})}; + const symbol_exprt array{"array", array_type}; + solver.set_to(equal_exprt{x, from_integer(42, byte)}, true); + solver.set_to(equal_exprt{empty_name, from_integer(9, byte)}, true); + solver.set_to(equal_exprt{number, from_integer(-10, number.type())}, true); + solver.set_to( + equal_exprt{record, struct_exprt{{from_integer(3, byte)}, record_type}}, + true); + solver.set_to( + equal_exprt{array, array_of_exprt{from_integer(7, byte), array_type}}, + true); + const auto yes = solver.handle(equal_exprt{x, from_integer(42, byte)}); + const auto no = + solver.handle(equal_exprt{number, from_integer(0, number.type())}); + + // Q5/Q6: singleton and multiline batched responses must produce the same + // actual values. Reordered pairs, quoted/escaped ids, both Boolean values, + // the legal empty quoted identifier, indexed bitvectors, negative integers, + // arrays and structs all use the + // original parsed_values map and typed parse_rec implementation. + const std::vector pairs{ + "(B1 false)", + "(|| #x09)", + "(array ((as const (Array (_ BitVec 64) (_ BitVec 8))) #x07))", + "(|x&124;y| (_ bv42 8))", + "(record (mk-struct.0 #x03))", + "(B0 true)", + "(number (- 10))"}; + std::string response = "sat\n"; + SECTION("Singleton responses") + { + for(const auto &pair : pairs) + response += "(" + pair + ")\n"; + } + SECTION("Batched response") + { + response += "(\n"; + for(const auto &pair : pairs) + response += pair + "\n"; + response += ")\n"; + } + std::istringstream input{response}; + REQUIRE( + solver.read_result(input) == decision_proceduret::resultt::D_SATISFIABLE); + CHECK(solver.get(x) == from_integer(42, byte)); + CHECK(solver.get(empty_name) == from_integer(9, byte)); + CHECK(solver.get(number) == from_integer(-10, number.type())); + CHECK( + solver.get(record) == struct_exprt{{from_integer(3, byte)}, record_type}); + CHECK( + solver.get(array) == + array_exprt{{from_integer(7, byte), from_integer(7, byte)}, array_type}); + CHECK(solver.get(yes) == true_exprt{}); + CHECK(solver.get(no) == false_exprt{}); +} + +TEST_CASE( + "SMT model response failures do not become SAT", + "[core][solvers][smt2]") +{ + symbol_tablet symbol_table; + namespacet ns{symbol_table}; + null_message_handlert messages; + smt2_result_testt solver{ + ns, "results", "", "ALL", smt2_convt::solvert::Z3, "", messages}; + const auto response = GENERATE( + "sat\n(error \"model unavailable\")\n", + "unknown\n", + "sat\n()\n", + "sat\n((x #x01) (broken) (y #x02))\n", + "sat\n((x #x01) (y #x02 extra))\n", + "sat\n((x #x01) ((bad name) #x02))\n", + "sat\n((x #x01) (y #x02)\n", + "sat\n((x #x01))\n)\n"); + // Q7: SAT errors and UNKNOWN are failures as before. Q8: malformed middle + // or last pairs, empty lists and syntax errors also fail, even after valid + // values or SAT were parsed. Never return a partially accepted model. + std::istringstream input{response}; + CHECK(solver.read_result(input) == decision_proceduret::resultt::D_ERROR); +} + +TEST_CASE( + "SMT model status and Boolean fallback remain compatible", + "[core][solvers][smt2]") +{ + symbol_tablet symbol_table; + namespacet ns{symbol_table}; + null_message_handlert messages; + smt2_result_testt solver{ + ns, "results", "", "ALL", smt2_convt::solvert::Z3, "", messages}; + SECTION("UNSAT ignores later model errors") + { + // Q9: no model exists after UNSAT; retain the existing error exemption. + std::istringstream input{"unsat\n(error \"model unavailable\")\n"}; + CHECK( + solver.read_result(input) == + decision_proceduret::resultt::D_UNSATISFIABLE); + } + SECTION("Historical diagnostics do not invalidate a clean response") + { + // Q10: syntax-error detection compares the current parser call's error + // count, not unrelated diagnostics previously sent to the shared handler. + messaget log{messages}; + log.error() << "earlier diagnostic" << messaget::eom; + std::istringstream input{"sat\n"}; + CHECK( + solver.read_result(input) == decision_proceduret::resultt::D_SATISFIABLE); + } + SECTION("Missing typed value") + { + // Q11: a required typed identifier cannot silently parse an absent value. + const symbol_exprt x{"x", unsignedbv_typet{8}}; + solver.set_to(equal_exprt{x, from_integer(1, x.type())}, true); + std::istringstream input{"sat\n"}; + CHECK(solver.read_result(input) == decision_proceduret::resultt::D_ERROR); + } + SECTION("Missing Boolean without fallback") + { + // Q12: a missing solver Boolean must not default to false. + const symbol_exprt x{"x", unsignedbv_typet{8}}; + solver.handle(equal_exprt{x, from_integer(1, x.type())}); + std::istringstream input{"sat\n((x #x01))\n"}; + CHECK(solver.read_result(input) == decision_proceduret::resultt::D_ERROR); + } + SECTION("Missing Boolean with set_to fallback") + { + // Q13: the established set_to fallback remains valid for a literal whose + // value is already fixed by an assertion; no model value is invented. + const symbol_exprt x{"x", unsignedbv_typet{8}}; + const equal_exprt expression{x, from_integer(1, x.type())}; + const auto literal = solver.handle(expression); + solver.set_to(expression, true); + std::istringstream input{"sat\n((x #x01))\n"}; + REQUIRE( + solver.read_result(input) == decision_proceduret::resultt::D_SATISFIABLE); + CHECK(solver.get(literal) == true_exprt{}); + } +} + +TEST_CASE( + "SMT missing-value handling for other solvers is unchanged", + "[core][solvers][smt2]") +{ + symbol_tablet symbol_table; + namespacet ns{symbol_table}; + null_message_handlert messages; + const auto backend = + GENERATE(smt2_convt::solvert::BOOLECTOR, smt2_convt::solvert::GENERIC); + smt2_result_testt solver{ns, "results", "", "ALL", backend, "", messages}; + const symbol_exprt x{"x", unsignedbv_typet{8}}; + solver.set_to(equal_exprt{x, from_integer(1, x.type())}, true); + + // Q15: smt2_identifiers is not a request receipt for every backend: + // Boolector never emits get-value. The new missing-requested-value failure + // is limited to Z3; preserve other backends' existing result handling. + std::istringstream input{"sat\n"}; + CHECK( + solver.read_result(input) == decision_proceduret::resultt::D_SATISFIABLE); +} + +TEST_CASE( + "SMT other solver responses retain singleton and extra-model handling", + "[core][solvers][smt2]") +{ + symbol_tablet symbol_table; + namespacet ns{symbol_table}; + null_message_handlert messages; + const auto backend = + GENERATE(smt2_convt::solvert::BOOLECTOR, smt2_convt::solvert::GENERIC); + smt2_result_testt solver{ns, "results", "", "ALL", backend, "", messages}; + const symbol_exprt x{"x", unsignedbv_typet{8}}; + solver.set_to(equal_exprt{x, from_integer(42, x.type())}, true); + std::string response = "sat\n((x #x2a))\n"; + SECTION("Additional model list") + { + // Q16: a non-Z3 solver can emit an extra model list. Preserve the old + // unknown-list handling and the actual value read from its singleton. + response += "(model (define-fun x () (_ BitVec 8) #x2a))\n"; + } + SECTION("Historical syntax-error behavior") + { + // Q17: this patch's new syntax-error rejection is scoped to Z3 batching; + // do not change other solvers' existing EOF/error interpretation here. + response += "("; + } + std::istringstream input{response}; + REQUIRE( + solver.read_result(input) == decision_proceduret::resultt::D_SATISFIABLE); + CHECK(solver.get(x) == from_integer(42, x.type())); +} + +TEST_CASE("Z3 batched model values retain their assignments", "[smt2][z3]") +{ + // Q18: multiple differently typed, constrained symbols trigger one model + // request. A real Z3 response must recover each value, including both + // Boolean outcomes. This exercises generation, transport and decoding. + symbol_tablet symbol_table; + namespacet ns{symbol_table}; + null_message_handlert messages; + smt2_dect solver{ + ns, "batch", "", "ALL", smt2_convt::solvert::Z3, "", messages}; + const symbol_exprt x{"x|y", unsignedbv_typet{8}}; + const symbol_exprt number{"number", integer_typet{}}; + const equal_exprt condition{x, from_integer(42, x.type())}; + const auto yes = solver.handle(condition); + const auto no = + solver.handle(equal_exprt{number, from_integer(0, number.type())}); + solver.set_to(condition, true); + solver.set_to(equal_exprt{number, from_integer(-10, number.type())}, true); + REQUIRE(solver() == decision_proceduret::resultt::D_SATISFIABLE); + CHECK(solver.get(x) == from_integer(42, x.type())); + CHECK(solver.get(number) == from_integer(-10, number.type())); + CHECK(solver.get(yes) == true_exprt{}); + CHECK(solver.get(no) == false_exprt{}); +} + TEST_CASE( "smt2_convt::convert_identifier character escaping.", "[core][solvers][smt2]")