From a144ad4f74048a1b6dadce60c5a3ff0e9b7c3729 Mon Sep 17 00:00:00 2001 From: Chai Zhenhua Date: Thu, 10 Sep 2026 09:07:00 +0800 Subject: [PATCH] Detect binder origins in SMT value definitions Z3 rejects get-value queries whose expanded definitions contain quantifiers or lambdas. Extend the existing quantifier traversal to recognize array comprehensions when they lower to lambdas, and use it at both Boolean and typed value origins. This preserves define-fun for ordinary Z3 values while keeping binders behind declare-fun plus an equality assertion. Tests cover Boolean binder origins, typed binder origins, the binder-free control, the existing lambda-unflatten regression, real Z3 solving, and the CBMC and SMT2 solver CORE suites. --- regression/cbmc/z3-lambda-unflatten/main.c | 4 +- regression/cbmc/z3-lambda-unflatten/test.desc | 4 +- src/solvers/smt2/smt2_conv.cpp | 32 +++++----- unit/solvers/smt2/smt2_conv.cpp | 63 +++++++++++++++++++ 4 files changed, 82 insertions(+), 21 deletions(-) diff --git a/regression/cbmc/z3-lambda-unflatten/main.c b/regression/cbmc/z3-lambda-unflatten/main.c index 029c084315f..c325a4d5ec4 100644 --- a/regression/cbmc/z3-lambda-unflatten/main.c +++ b/regression/cbmc/z3-lambda-unflatten/main.c @@ -3,8 +3,8 @@ // // Z3 rejects `(get-value ...)` on symbols whose `define-fun` body // contains a lambda, so smt2_convt::set_to switches to -// `(declare-fun X () T) (assert (= X body))` whenever -// use_lambda_for_array is set (currently only Z3). This test +// `(declare-fun X () T) (assert (= X body))` when the prepared body contains +// a binder. This test // exercises the path -- the variable-length unsigned-char array // `src` ends up encoded with an `array_comprehension` that produces a // lambda body, and the new gate keeps the assignment to the diff --git a/regression/cbmc/z3-lambda-unflatten/test.desc b/regression/cbmc/z3-lambda-unflatten/test.desc index 2d83b15768c..a347941754c 100644 --- a/regression/cbmc/z3-lambda-unflatten/test.desc +++ b/regression/cbmc/z3-lambda-unflatten/test.desc @@ -12,8 +12,8 @@ Pins the SMT2 emitted under `--z3` to a `(declare-fun ...) (assert (= ... (lambda ...)))` form rather than `(define-fun ... (lambda ...))` -- which Z3 rejects on `(get-value ...)`. The lambda comes from CBMC's array comprehension lowering for the variable-length `src` array; without the -`set_to` re-routing introduced when `use_lambda_for_array` is true (gated on -`use_lambda_for_array`, currently only Z3) the SMT2 would emit a +`set_to` re-routing for binder-containing prepared expressions, the SMT2 +would emit a `define-fun` body that prevents Z3 from returning a model. The regex tolerates the two ways the memcpy SSA symbol is named: diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 4a232f41eee..ebffd98dec0 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -944,13 +944,17 @@ void smt2_convt::convert_address_of_rec( expr.id_string()); } -static bool has_quantifier(const exprt &expr) +static bool has_smt_binder(const exprt &expr, bool use_lambda_for_array) { bool result = false; - expr.visit_post([&result](const exprt &node) { - if(node.id() == ID_exists || node.id() == ID_forall) - result = true; - }); + expr.visit_post( + [&result, use_lambda_for_array](const exprt &node) + { + if( + node.id() == ID_exists || node.id() == ID_forall || + (use_lambda_for_array && node.id() == ID_array_comprehension)) + result = true; + }); return result; } @@ -984,8 +988,9 @@ literalt smt2_convt::convert(const exprt &expr) // Note that here we are always converting, so we do not need to consider // other literal kinds, only "|B###|" - // Z3 refuses get-value when a defined symbol contains a quantifier. - if(has_quantifier(prepared_expr)) + // Z3 refuses get-value when a defined symbol contains a quantifier or a + // lambda, including array comprehensions introduced during preparation. + if(has_smt_binder(prepared_expr, use_lambda_for_array)) { out << "(declare-fun "; convert_literal(l); @@ -5531,17 +5536,10 @@ void smt2_convt::set_to(const exprt &expr, bool value) convert_expr(prepared_rhs); out << ')' << ')' << '\n'; } - else if(use_lambda_for_array) + else if(has_smt_binder(prepared_rhs, use_lambda_for_array)) { - // The body emitted below may contain a `(lambda ...)` from - // `unflatten` (used as a stand-in for `(as const ...)` for - // back-ends with `use_as_const = false`). Z3 rejects - // `get-value` on symbols whose `define-fun` body contains - // a lambda, so we use `declare-fun` + `assert (= ...)` here. - // Back-ends with `use_lambda_for_array = false` (the - // default, currently every back-end other than Z3) keep - // using the `define-fun` form below, so their SMT2 output - // is unaffected. + // Stop binder-containing definitions at their origin, before an + // alias can expand them into a get-value term rejected by Z3. out << "(declare-fun " << smt2_identifier; out << " () "; convert_type(equal_expr.lhs().type()); diff --git a/unit/solvers/smt2/smt2_conv.cpp b/unit/solvers/smt2/smt2_conv.cpp index caa69059f9d..5de4669496d 100644 --- a/unit/solvers/smt2/smt2_conv.cpp +++ b/unit/solvers/smt2/smt2_conv.cpp @@ -615,3 +615,66 @@ TEST_CASE( REQUIRE(operands_map.size() == 1); REQUIRE(operands_map.count(-1) == 1); } + +TEST_CASE( + "SMT value definitions stop at actual binder origins", + "[core][solvers][smt2]") +{ + // Cause-effect design: B1 selects Z3's lambda array encoding, B2 says the + // prepared value contains an array comprehension, and B3 selects a Boolean + // handle rather than a typed assignment. R1 (B1,B2,B3) declares and asserts + // a Boolean handle; R2 (B1,B2,!B3) declares and asserts the typed origin; + // R3 (B1,!B2,!B3) keeps define-fun. Constraint: an array comprehension is an + // SMT binder only for a back-end that emits it as a lambda. + symbol_tablet symbol_table; + namespacet ns{symbol_table}; + std::ostringstream out; + smt2_convt conv{ns, "binder origin", "", "ALL", smt2_convt::solvert::Z3, out}; + const unsignedbv_typet byte{8}; + const unsignedbv_typet index_type{64}; + const array_typet array_type{byte, from_integer(2, index_type)}; + const symbol_exprt index{"i", index_type}; + const array_comprehension_exprt comprehension{ + index, typecast_exprt{index, byte}, array_type}; + + SECTION("Boolean handle containing an array comprehension") + { + // Causes: B1, B2, and B3. Effect R1: declare and constrain the handle at + // its origin, so later get-value queries never expand the binder. + const equal_exprt predicate{ + index_exprt{comprehension, from_integer(1, index_type)}, + from_integer(1, byte)}; + conv.handle(predicate); + const std::string output = out.str(); + CHECK(output.find("(declare-fun B0 () Bool)") != std::string::npos); + CHECK(output.find("(assert (= B0 ") != std::string::npos); + CHECK(output.find("(lambda ((i ") != std::string::npos); + CHECK(output.find("(define-fun B0 ") == std::string::npos); + } + + SECTION("Typed assignment whose prepared value contains a binder") + { + // Causes: B1, B2, and !B3. Effect R2: use the same declaration-and-equality + // form and preserve the complete lambda body. + const symbol_exprt array{"array", array_type}; + conv.set_to(equal_exprt{array, comprehension}, true); + const std::string output = out.str(); + CHECK(output.find("(declare-fun array () (Array ") != std::string::npos); + CHECK(output.find("(assert (= array ") != std::string::npos); + CHECK(output.find("(lambda ((i ") != std::string::npos); + CHECK(output.find("(define-fun array ") == std::string::npos); + } + + SECTION("Binder-free typed assignment") + { + // Causes: B1, !B2, and !B3. Effect R3: retain the existing define-fun + // form; selecting Z3 alone must not force every value through + // declare/assert. + const symbol_exprt plain{"plain", byte}; + conv.set_to(equal_exprt{plain, from_integer(7, byte)}, true); + const std::string output = out.str(); + CHECK( + output.find("(define-fun plain () (_ BitVec 8) ") != std::string::npos); + CHECK(output.find("(declare-fun plain ") == std::string::npos); + } +}