Share the quantified expression via a let-binding in the Z3 workaround

The Z3 quantifier workaround emits the equivalence between the declared
Boolean and its quantified definition as two implications. Writing the
quantified expression out in both implications doubles its size in the
SMT2 output, which can be significant for large quantified terms. Bind
it once with an SMT-LIB `let` and reference the binding from both
implications instead.

This was verified to still work around Z3's solve_eqs elimination
(Z3Prover/z3#7743) on the affected Z3 versions: get-value returns a
plain Boolean rather than the quantified expression.

The smt2_convt unit test is adjusted to expect the let-bound form.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Author: tautschnig

src/solvers/smt2/smt2_conv.cpp

@@ -990,19 +990,18 @@ literalt smt2_convt::convert(const exprt &expr)
       // preprocessor eliminates B by substituting the quantified <expr>, and
       // then hands the eliminated form back through get-value (see
       // Z3Prover/z3#7743). Asserting the equivalence as two implications
-      // instead prevents this. The underlying issue is fixed in Z3 >= 4.17
-      // (which also exposes (set-option :smt.solve_eqs.non_ground false)), but
-      // neither is widely available yet, so we keep the workaround for Z3.
-      out << "(assert (=> ";
-      convert_literal(l);
-      out << ' ';
-      convert_expr(prepared_expr);
-      out << "))\n";
-      out << "(assert (=> ";
+      // instead prevents this; a let-binding shares the (possibly large)
+      // quantified expression so that it is emitted only once. The underlying
+      // issue is fixed in Z3 >= 4.17 (which also exposes
+      // (set-option :smt.solve_eqs.non_ground false)), but neither is widely
+      // available yet, so we keep the workaround for Z3.
+      out << "(assert (let ((?def ";
       convert_expr(prepared_expr);
-      out << ' ';
+      out << ")) (and (=> ";
       convert_literal(l);
-      out << "))\n";
+      out << " ?def) (=> ?def ";
+      convert_literal(l);
+      out << "))))\n";
     }
     else
     {

unit/solvers/smt2/smt2_conv.cpp

@@ -227,24 +227,20 @@ TEST_CASE("smt2_convt quantifier definition encoding", "[core][solvers][smt2]")
     const std::string out = convert_handle(quantified, smt2_convt::solvert::Z3);
     INFO("SMT2 output:\n" << out);
 
-    THEN("it is declared and constrained by two implications, in order")
+    THEN("it is declared and constrained by a let-bound equivalence")
     {
       // A single `(assert (= B0 <quantifier>))` would be undone by Z3's
       // solve_eqs preprocessor (Z3Prover/z3#7743), so the equivalence is
-      // emitted as two implications, B0 => <q> followed by <q> => B0.
+      // emitted as two implications. A let-binding shares the quantified
+      // expression so that it is written only once.
       const std::string declare = "(declare-fun B0 () Bool)";
-      const std::string impl1 = "(assert (=> B0 " + quant + "))";
-      const std::string impl2 = "(assert (=> " + quant + " B0))";
-
-      const auto p_declare = out.find(declare);
-      const auto p_impl1 = out.find(impl1);
-      const auto p_impl2 = out.find(impl2);
-
-      REQUIRE(p_declare != std::string::npos);
-      REQUIRE(p_impl1 != std::string::npos);
-      REQUIRE(p_impl2 != std::string::npos);
-      REQUIRE(p_declare < p_impl1);
-      REQUIRE(p_impl1 < p_impl2);
+      const std::string assertion =
+        "(assert (let ((?def " + quant + ")) (and (=> B0 ?def) (=> ?def B0))))";
+
+      REQUIRE(out.find(declare) != std::string::npos);
+      REQUIRE(out.find(assertion) != std::string::npos);
+      // the quantified expression is emitted exactly once
+      REQUIRE(out.find(quant) == out.rfind(quant));
       // no plain equality definition
       REQUIRE(out.find("(assert (= B0 ") == std::string::npos);
     }