From 9c37b16d2f055f0ff326ca2215516ca141c2b66d Mon Sep 17 00:00:00 2001 From: Chai Zhenhua Date: Thu, 10 Sep 2026 08:46:09 +0800 Subject: [PATCH] Batch Z3 model value requests and validate responses The SMT2 backend currently writes one get-value command per identifier. Request the same sorted identifier set in one Z3 command, and consume every identifier/value pair through the existing typed model decoder. Reject malformed pairs, parser errors and omitted requested typed values instead of accepting a partial SAT model. Keep singleton responses, Boolean set_to fallback, UNSAT model errors and other solvers' behavior. Leave the current Z3 use_as_const setting and type encodings unchanged. Add decision-table unit coverage for empty/singleton/multiple requests, escaped identifiers, typed batched responses, invalid/missing responses, and compatibility cases, plus a real Z3 model round trip. Relinking these tests against the parent solver library reproduces the request assertion failure and six malformed-response failures. Validation: clang-format 15 changed-line check and cpplint pass; [smt2] 308 assertions/46 cases; [z3] 27/7; [core] 18,839 assertions/595 cases, including two expected failures. CBMC CORE passes 1,128 tests (67 skipped), and SMT2 solver CORE passes 42 (2 skipped). The wider Z3 CORE run passes 1,102 (92 skipped); complex2 times out at 20 seconds on both parent and candidate and at 60 seconds on candidate. Its generated formula is identical except for get-value grouping. On one generated 1,000-scalar SAT fixture with Z3 4.15.4, requests fall from 10,006 to 1, SMT input from 1,733,249 to 1,593,179 bytes and model output from 324,598 to 314,593 bytes. Seven alternating Z3 runs have median wall times 49.44/41.78 ms; five CBMC runs have medians 308.03/294.30 ms. Model assignments and decoded traces match exactly. These local sample measurements do not establish a general speedup. --- src/solvers/smt2/smt2_conv.cpp | 20 ++- src/solvers/smt2/smt2_conv.h | 4 +- src/solvers/smt2/smt2_dec.cpp | 68 ++++++-- unit/solvers/smt2/smt2_conv.cpp | 297 ++++++++++++++++++++++++++++++++ 4 files changed, 368 insertions(+), 21 deletions(-) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 4a232f41eee..30f4d65affe 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 ca94493a6be..c9bed868e06 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 cbe6ecb8ebc..2e0b3d0c3c1 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 caa69059f9d..ec968e39583 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]")