#include <z3++.h>

#include <catch2/catch_test_macros.hpp>
#include <functional>
#include <optional>
#include <string>
#include <vector>

#include "fold/symbolic/summary.hpp"
#include "fold/symbolic/summary_cache.hpp"

using namespace fold::symbolic;

namespace {

SymbolicSummary makeDummySummary(const std::string& ret) {
    SymbolicSummary s;
    s.return_post = ret;
    s.is_pure = true;
    return s;
}

} // namespace

TEST_CASE("SummaryCache: empty lookup returns nullptr", "[summary_cache]") {
    SummaryCache cache;
    REQUIRE(cache.lookup("foo::bar", 42) == nullptr);
    REQUIRE(cache.size() == 0);
}

TEST_CASE("SummaryCache: store then lookup returns same value", "[summary_cache]") {
    SummaryCache cache;
    SymbolicSummary s = makeDummySummary("arg0");
    cache.store("foo::bar", 42, s);

    const auto* found = cache.lookup("foo::bar", 42);
    REQUIRE(found != nullptr);
    REQUIRE(found->return_post == "arg0");
    REQUIRE(found->is_pure == true);
    REQUIRE(cache.size() == 1);
}

TEST_CASE("SummaryCache: stale hash returns nullptr", "[summary_cache]") {
    SummaryCache cache;
    cache.store("foo::bar", 42, makeDummySummary("arg0"));

    // Different hash = stale
    REQUIRE(cache.lookup("foo::bar", 99) == nullptr);
    REQUIRE(cache.isStale("foo::bar", 99) == true);
    REQUIRE(cache.isStale("foo::bar", 42) == false);
}

TEST_CASE("SummaryCache: invalidate removes entry", "[summary_cache]") {
    SummaryCache cache;
    cache.store("foo::bar", 42, makeDummySummary("arg0"));
    REQUIRE(cache.size() == 1);

    cache.invalidate("foo::bar");
    REQUIRE(cache.size() == 0);
    REQUIRE(cache.lookup("foo::bar", 42) == nullptr);
}

TEST_CASE("SummaryCache: getOrCompute hits cache", "[summary_cache]") {
    SummaryCache cache;
    cache.store("foo::bar", 42, makeDummySummary("cached"));

    int call_count = 0;
    auto compute_fn = [&](const std::string&) -> std::optional<SymbolicSummary> {
        ++call_count;
        return makeDummySummary("computed");
    };

    const auto* result = cache.getOrCompute("foo::bar", 42, compute_fn);
    REQUIRE(result != nullptr);
    REQUIRE(result->return_post == "cached");
    REQUIRE(call_count == 0); // should not have called compute_fn
}

TEST_CASE("SummaryCache: getOrCompute misses calls compute_fn", "[summary_cache]") {
    SummaryCache cache;

    int call_count = 0;
    auto compute_fn = [&](const std::string& name) -> std::optional<SymbolicSummary> {
        ++call_count;
        REQUIRE(name == "foo::bar");
        return makeDummySummary("computed");
    };

    const auto* result = cache.getOrCompute("foo::bar", 42, compute_fn);
    REQUIRE(result != nullptr);
    REQUIRE(result->return_post == "computed");
    REQUIRE(call_count == 1);
    REQUIRE(cache.size() == 1);

    // Second call with same hash: cache hit.
    const auto* result2 = cache.getOrCompute("foo::bar", 42, compute_fn);
    REQUIRE(result2 != nullptr);
    REQUIRE(result2->return_post == "computed");
    REQUIRE(call_count == 1); // not called again
}

TEST_CASE("SummaryCache: getOrCompute returns nullptr on compute failure", "[summary_cache]") {
    SummaryCache cache;

    auto compute_fn = [&](const std::string&) -> std::optional<SymbolicSummary> {
        return std::nullopt;
    };

    const auto* result = cache.getOrCompute("foo::bar", 42, compute_fn);
    REQUIRE(result == nullptr);
    REQUIRE(cache.size() == 0);
}

TEST_CASE("SummaryCache: recursion guard returns nullptr", "[summary_cache]") {
    SummaryCache cache;

    const SymbolicSummary* outer_result = nullptr;
    int inner_calls = 0;

    auto compute_fn = [&](const std::string& name) -> std::optional<SymbolicSummary> {
        // Simulate recursive lookup: while computing "foo::bar", try to
        // look up "foo::bar" again.
        auto result =
            cache.getOrCompute(name, 42, [&](const std::string&) -> std::optional<SymbolicSummary> {
                ++inner_calls;
                return makeDummySummary("inner");
            });
        // Should return nullptr due to recursion guard.
        REQUIRE(result == nullptr);
        return makeDummySummary("outer");
    };

    outer_result = cache.getOrCompute("foo::bar", 42, compute_fn);
    REQUIRE(outer_result != nullptr);
    REQUIRE(outer_result->return_post == "outer");
    REQUIRE(inner_calls == 0); // inner compute_fn never called because guard kicked in
}

TEST_CASE("SummaryCache: markComputed updates hash without summary", "[summary_cache]") {
    SummaryCache cache;
    cache.markComputed("foo::bar", 42);
    REQUIRE(cache.isStale("foo::bar", 99) == true);
    // No summary stored yet, so lookup with correct hash returns nullptr.
    REQUIRE(cache.lookup("foo::bar", 42) == nullptr);
}

TEST_CASE("SummaryCache: clear removes everything", "[summary_cache]") {
    SummaryCache cache;
    cache.store("a", 1, makeDummySummary("a"));
    cache.store("b", 2, makeDummySummary("b"));
    REQUIRE(cache.size() == 2);

    cache.clear();
    REQUIRE(cache.size() == 0);
    REQUIRE(cache.lookup("a", 1) == nullptr);
    REQUIRE(cache.lookup("b", 2) == nullptr);
}

TEST_CASE("SummaryCache: store overwrites same name", "[summary_cache]") {
    SummaryCache cache;
    cache.store("foo::bar", 1, makeDummySummary("v1"));
    cache.store("foo::bar", 2, makeDummySummary("v2"));

    // Old hash is stale.
    REQUIRE(cache.lookup("foo::bar", 1) == nullptr);
    // New hash works.
    const auto* v2 = cache.lookup("foo::bar", 2);
    REQUIRE(v2 != nullptr);
    REQUIRE(v2->return_post == "v2");
    REQUIRE(cache.size() == 1);
}

TEST_CASE("SummaryCache: preconditions survive caching", "[summary_cache]") {
    SummaryCache cache;
    SymbolicSummary s;
    s.param_pre[0] = {{"nonnull", "(not (= arg0 #x0000000000000000))"}};
    s.return_post = "arg0";
    s.is_pure = false;
    s.reads_globals = {"g_x"};
    s.writes_globals = {"g_y"};

    cache.store("with_pre", 10, s);

    const auto* found = cache.lookup("with_pre", 10);
    REQUIRE(found != nullptr);
    REQUIRE(found->param_pre.count(0) == 1);
    REQUIRE(found->param_pre.at(0).size() == 1);
    REQUIRE(found->param_pre.at(0)[0].kind == "nonnull");
    REQUIRE(found->reads_globals.count("g_x") == 1);
    REQUIRE(found->writes_globals.count("g_y") == 1);
}