// Matrix row Z10 — confirm Z3 pretty-printer let-bindings are enabled
// for serialised summaries so shared subterms collapse on the wire.
//
// Test pins:
//   1. A body with shared subterms serialises to a string containing
//      `let ` (let-bindings are active).
//   2. The let-compacted body round-trips through deserialize() back
//      to a structurally-equivalent expression (semantic-preserving).
//   3. A body with no shared structure does NOT bloat — same length
//      class before vs after compaction.

#include <z3++.h>

#include <catch2/catch_test_macros.hpp>
#include <string>

#include "fold/symbolic/encoder.hpp"
#include "fold/symbolic/serialize.hpp"
#include "fold/symbolic/summary_encoder.hpp"

namespace {

// Build a synthetic FunctionSummarized whose return_value contains
// shared subterms ACROSS BRANCHES of an ite. simplify() can't collapse
// these into one occurrence (the branches are semantically distinct
// arithmetic), so the let-binding factor-out remains visible after
// adaptSerializedBody's terminal simplify.
fold::FunctionSummarized makeSharedSubtermSummary() {
    auto env = fold::SymbolicEnv::create();
    z3::context& c = env.ctx();
    z3::expr a = c.bv_const("a", 64);
    z3::expr b = c.bv_const("b", 64);
    z3::expr sum = a + b;
    z3::expr diff = a - b;
    z3::expr cond = a > c.bv_val(0, 64);
    // Two arithmetically-distinct ite arms each reuse sum + diff —
    // simplify can rewrite within each arm but can't merge across.
    z3::expr then_arm = sum * diff;
    z3::expr else_arm = sum + diff;
    z3::expr body = z3::ite(cond, then_arm * then_arm, else_arm + else_arm);
    return fold::FunctionSummarized{
        .env = std::move(env),
        .inputs = {a, b},
        .return_value = body,
        .soundness = fold::SoundnessTag{},
    };
}

} // namespace

TEST_CASE("serialize: shared subterms collapse via z3 `let` bindings", "[serialize][z10][let]") {
    auto fs = makeSharedSubtermSummary();
    auto serialized =
        fold::serialize("test-id", "shared_test", "input.cpp", 1, 1, "signature_key", fs);
    REQUIRE(serialized.body_smt.find("let ") != std::string::npos);
}

TEST_CASE("serialize: let-compacted body round-trips structurally", "[serialize][z10][roundtrip]") {
    auto fs = makeSharedSubtermSummary();
    auto serialized =
        fold::serialize("test-id", "shared_test", "input.cpp", 1, 1, "signature_key", fs);

    z3::context fresh;
    auto restored = fold::deserialize(fresh, serialized);
    REQUIRE(restored.has_value());

    // Structural equality after simplification: both should reduce to
    // the same canonical normal form. `to_string()` round-trips through
    // the same printer config, so equal-after-simplify is the right
    // invariant here.
    z3::expr orig_simpl = const_cast<z3::expr&>(fs.return_value).simplify();
    z3::expr restored_simpl = restored->return_value.simplify();

    // Re-serialise both with let-bindings to compare canonical strings.
    REQUIRE(orig_simpl.to_string() == restored_simpl.to_string());
}

TEST_CASE("serialize: simple non-shared body still serialises", "[serialize][z10][nonshared]") {
    // A body with zero shared structure must remain serialisable. The
    // let-binding param is opportunistic — when there's nothing to
    // factor, output is identical to the un-tuned case (modulo any z3
    // implementation drift). This test confirms the change doesn't
    // break the simple path, not that the output matches a specific
    // string.
    auto makeFs = [] {
        auto env = fold::SymbolicEnv::create();
        z3::context& c = env.ctx();
        z3::expr a = c.bv_const("a", 64);
        z3::expr body = a + c.bv_val(1, 64);
        return fold::FunctionSummarized{
            .env = std::move(env),
            .inputs = {a},
            .return_value = body,
            .soundness = fold::SoundnessTag{},
        };
    };
    auto fs = makeFs();
    auto serialized =
        fold::serialize("simple-id", "simple_test", "input.cpp", 1, 1, "signature_key", fs);
    REQUIRE_FALSE(serialized.body_smt.empty());
    // Roundtrip is covered by the shared-subterm test above; this case
    // only needs to confirm the simple path still serialises (no
    // accidental let-related crash on the trivial input).
}

TEST_CASE("serialize: statement count survives worker NDJSON round-trip",
          "[serialize][equiv][wire]") {
    auto fs = makeSharedSubtermSummary();
    auto serialized =
        fold::serialize("test-id", "shared_test", "input.cpp", 1, 1, "signature_key", fs);
    serialized.body_statement_count = 7;

    const auto restored = fold::fromJson(fold::toJson(serialized));
    CHECK(restored.body_statement_count == 7);
    CHECK(restored.id == serialized.id);
    CHECK(restored.body_smt == serialized.body_smt);
}