Detect binder origins in SMT value definitions

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

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:

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());

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);
+  }
+}