#include <array>
#include <catch2/catch_test_macros.hpp>
#include <cstddef>

#include "fold/ir/access_path.hpp"
#include "fold/symbolic/encoder.hpp"
#include "fold/symbolic/guarded_facts.hpp"

namespace {

fold::ir::Symbol synthSymbol(std::size_t id) {
    static const std::array<int, 16> slots{};
    return fold::ir::Symbol{static_cast<const void*>(&slots.at(id))};
}

fold::ir::AccessPath synthPath(std::size_t id) {
    return fold::ir::AccessPath::local(synthSymbol(id), "value", "test").field("count");
}

} // namespace

TEST_CASE("GuardedFactStore returns unguarded range facts as fallback",
          "[symbolic][guarded-facts]") {
    z3::context ctx;
    fold::symbolic::GuardedFactStore store;
    const auto subject = synthPath(1);

    store.setRange(subject, fold::IntInterval{2, 8, false});

    auto range = store.range(subject, ctx.bool_val(true));
    REQUIRE(range.has_value());
    CHECK(range->lo == 2);
    CHECK(range->hi == 8);
}

TEST_CASE("GuardedFactStore returns facts when current path implies guard",
          "[symbolic][guarded-facts]") {
    z3::context ctx;
    fold::symbolic::GuardedFactStore store;
    const auto subject = synthPath(2);
    z3::expr x = ctx.bv_const("x", fold::kBitvecWidth);
    z3::expr zero = ctx.bv_val(0, fold::kBitvecWidth);
    z3::expr five = ctx.bv_val(5, fold::kBitvecWidth);

    store.markNonNull(subject, fold::symbolic::FactGuard::when(x != zero));
    store.setRange(subject, fold::IntInterval{1, 10, false},
                   fold::symbolic::FactGuard::when(x != zero));

    z3::expr current_path = x == five;
    CHECK(store.isNonNull(subject, current_path, 100));
    auto range = store.range(subject, current_path, 100);
    REQUIRE(range.has_value());
    CHECK(range->lo == 1);
}

TEST_CASE("GuardedFactStore ignores guarded facts not implied by current path",
          "[symbolic][guarded-facts]") {
    z3::context ctx;
    fold::symbolic::GuardedFactStore store;
    const auto subject = synthPath(3);
    z3::expr flag = ctx.bool_const("flag");

    store.markNonZero(subject, fold::symbolic::FactGuard::when(flag));
    store.setRange(subject, fold::IntInterval{4, 4, false}, fold::symbolic::FactGuard::when(flag));

    CHECK_FALSE(store.isNonZero(subject, !flag, 100));
    CHECK_FALSE(store.range(subject, !flag, 100).has_value());
}

TEST_CASE("GuardedFactStore resolves latest matching fact and preserves subjects",
          "[symbolic][guarded-facts]") {
    z3::context ctx;
    fold::symbolic::GuardedFactStore store;
    const auto subject = synthPath(4);
    const auto other = synthPath(5);

    store.setRange(subject, fold::IntInterval{1, 2, false});
    store.setRange(subject, fold::IntInterval{7, 9, false});
    store.setRange(other, fold::IntInterval{20, 30, false});

    auto range = store.range(subject, ctx.bool_val(true));
    REQUIRE(range.has_value());
    CHECK(range->lo == 7);
    CHECK(range->hi == 9);

    auto other_range = store.range(other, ctx.bool_val(true));
    REQUIRE(other_range.has_value());
    CHECK(other_range->lo == 20);
}

TEST_CASE("GuardedFactStore stores equality and member value facts", "[symbolic][guarded-facts]") {
    z3::context ctx;
    fold::symbolic::GuardedFactStore store;
    const auto eq_subject = synthPath(6);
    const auto member_subject = synthPath(7);
    z3::expr eq_value = ctx.bv_val(42, fold::kBitvecWidth);
    z3::expr member_value = ctx.bv_val(99, fold::kBitvecWidth);

    store.setEquality(eq_subject, eq_value);
    store.setMemberValue(member_subject, member_value);

    auto equality = store.equality(eq_subject, ctx.bool_val(true));
    auto member = store.memberValue(member_subject, ctx.bool_val(true));
    REQUIRE(equality.has_value());
    REQUIRE(member.has_value());
    CHECK(z3::eq(*equality, eq_value));
    CHECK(z3::eq(*member, member_value));
}

TEST_CASE("GuardedFactStore join collapses facts proved by both branches",
          "[symbolic][guarded-facts][join]") {
    z3::context ctx;
    fold::symbolic::GuardedFactStore then_store;
    fold::symbolic::GuardedFactStore else_store;
    const auto subject = synthPath(8);
    z3::expr cond = ctx.bool_const("cond");

    then_store.markNonNull(subject);
    else_store.markNonNull(subject);
    then_store.setRange(subject, fold::IntInterval{1, 3, false});
    else_store.setRange(subject, fold::IntInterval{1, 3, false});

    auto joined = fold::symbolic::GuardedFactStore::joinBranches(
        then_store, fold::symbolic::FactGuard::when(cond), else_store,
        fold::symbolic::FactGuard::when(!cond));

    CHECK(joined.isNonNull(subject, ctx.bool_val(true), 100));
    auto range = joined.range(subject, ctx.bool_val(true), 100);
    REQUIRE(range.has_value());
    CHECK(range->lo == 1);
    CHECK(range->hi == 3);
}

TEST_CASE("GuardedFactStore join retains branch-specific alternatives under guards",
          "[symbolic][guarded-facts][join]") {
    z3::context ctx;
    fold::symbolic::GuardedFactStore then_store;
    fold::symbolic::GuardedFactStore else_store;
    const auto subject = synthPath(9);
    z3::expr cond = ctx.bool_const("cond");

    then_store.setRange(subject, fold::IntInterval{1, 2, false});
    else_store.setRange(subject, fold::IntInterval{7, 8, false});

    auto joined = fold::symbolic::GuardedFactStore::joinBranches(
        then_store, fold::symbolic::FactGuard::when(cond), else_store,
        fold::symbolic::FactGuard::when(!cond));

    CHECK_FALSE(joined.range(subject, ctx.bool_val(true), 100).has_value());

    auto then_range = joined.range(subject, cond, 100);
    REQUIRE(then_range.has_value());
    CHECK(then_range->lo == 1);
    CHECK(then_range->hi == 2);

    auto else_range = joined.range(subject, !cond, 100);
    REQUIRE(else_range.has_value());
    CHECK(else_range->lo == 7);
    CHECK(else_range->hi == 8);
}

TEST_CASE("GuardedFactStore join conjoins original fact guards with branch guards",
          "[symbolic][guarded-facts][join]") {
    z3::context ctx;
    fold::symbolic::GuardedFactStore then_store;
    fold::symbolic::GuardedFactStore else_store;
    const auto subject = synthPath(10);
    z3::expr cond = ctx.bool_const("cond");
    z3::expr local_guard = ctx.bool_const("local_guard");

    then_store.markNonZero(subject, fold::symbolic::FactGuard::when(local_guard));

    auto joined = fold::symbolic::GuardedFactStore::joinBranches(
        then_store, fold::symbolic::FactGuard::when(cond), else_store,
        fold::symbolic::FactGuard::when(!cond));

    CHECK(joined.isNonZero(subject, cond && local_guard, 100));
    CHECK_FALSE(joined.isNonZero(subject, cond && !local_guard, 100));
    CHECK_FALSE(joined.isNonZero(subject, !cond && local_guard, 100));
}

TEST_CASE("GuardedFactStore degrades precision when guard feasibility is unknown",
          "[symbolic][guarded-facts]") {
    z3::context guard_ctx;
    z3::context path_ctx;
    fold::symbolic::GuardedFactStore store;
    fold::EncodingPrecisionContext precision;
    const auto subject = synthPath(11);
    store.markNonNull(subject,
                      fold::symbolic::FactGuard::when(guard_ctx.bool_const("foreign_guard")));

    CHECK_FALSE(store.isNonNull(subject, path_ctx.bool_val(true), 100, &precision));
    CHECK(precision.isImprecise());
}

TEST_CASE("SymbolicEnv exposes guarded fact reads against current path",
          "[symbolic][guarded-facts][env]") {
    auto env = fold::SymbolicEnv::create();
    const auto subject = synthPath(12);
    z3::expr x = env.ctx().bv_const("env_guard_x", fold::kBitvecWidth);
    z3::expr zero = env.ctx().bv_val(0, fold::kBitvecWidth);

    env.markFactNonZero(subject, fold::symbolic::FactGuard::when(x != zero));
    env.setFactRange(subject, fold::IntInterval{1, 32, false},
                     fold::symbolic::FactGuard::when(x != zero));

    env.setPath(x == env.ctx().bv_val(7, fold::kBitvecWidth));
    CHECK(env.isFactNonZero(subject, 100));
    auto range = env.factRange(subject, 100);
    REQUIRE(range.has_value());
    CHECK(range->lo == 1);
    CHECK(range->hi == 32);

    env.setPath(x == zero);
    CHECK_FALSE(env.isFactNonZero(subject, 100));
    CHECK_FALSE(env.factRange(subject, 100).has_value());
}

TEST_CASE("SymbolicEnv clears only AccessPath facts below a mutated root",
          "[symbolic][guarded-facts][env][havoc]") {
    auto env = fold::SymbolicEnv::create();
    auto root = fold::ir::AccessPath::synthetic("doc");
    auto size = root.field("sections").stableQuery(fold::ir::AccessKind::Size);
    auto title = root.field("title");
    auto other = fold::ir::AccessPath::synthetic("other").field("sections");

    env.setRange(size, fold::IntInterval{1, 8, false});
    env.setFactRange(size, fold::IntInterval{1, 8, false});
    env.markDefinitelyNonNull(title);
    env.setRange(other, fold::IntInterval{2, 9, false});
    env.setFactRange(other, fold::IntInterval{2, 9, false});

    env.clearAccessPathFacts(root);

    CHECK_FALSE(env.tryGetRange(size).has_value());
    CHECK_FALSE(env.factRange(size, 100).has_value());
    CHECK_FALSE(env.isDefinitelyNonNull(title));
    REQUIRE(env.tryGetRange(other).has_value());
    REQUIRE(env.factRange(other, 100).has_value());
}