#include <catch2/catch_test_macros.hpp>

#include "fold/symbolic/encoder.hpp"
#include "fold/symbolic/encoder_coerce.hpp"
#include "fold/symbolic/theory.hpp"

namespace {

fold::SymbolicEnv make_env() { return fold::SymbolicEnv::create(); }

z3::expr bv(fold::SymbolicEnv& env, std::uint64_t value, unsigned width) {
    return env.ctx().bv_val(value, width);
}

bool bv_eq(const z3::expr& lhs, std::uint64_t expected, unsigned width) {
    z3::expr target = lhs.ctx().bv_val(expected, width);
    z3::expr eq = (lhs == target).simplify();
    return eq.is_true();
}

} // namespace

TEST_CASE("coerceToBv: bv already at kBitvecWidth round-trips unchanged", "[encoder][coerce][bv]") {
    auto env = make_env();
    z3::expr v = bv(env, 0xDEAD'BEEF'CAFE'BABEULL, fold::kBitvecWidth);
    z3::expr out = fold::coerceToBv(env, v);
    REQUIRE(out.is_bv());
    REQUIRE(out.get_sort().bv_size() == fold::kBitvecWidth);
    REQUIRE(bv_eq(out, 0xDEAD'BEEF'CAFE'BABEULL, fold::kBitvecWidth));
}

TEST_CASE("coerceToBv: narrow signed bv sign-extends to kBitvecWidth", "[encoder][coerce][bv]") {
    auto env = make_env();
    // 8-bit two's-complement -1
    z3::expr v = bv(env, 0xFF, 8);
    z3::expr out = fold::coerceToBv(env, v, /*width=*/8, /*is_unsigned=*/false);
    REQUIRE(out.get_sort().bv_size() == fold::kBitvecWidth);
    // Sign-extended -1 in 64-bit = 0xFFFF'FFFF'FFFF'FFFF
    REQUIRE(bv_eq(out, 0xFFFF'FFFF'FFFF'FFFFULL, fold::kBitvecWidth));
}

TEST_CASE("coerceToBv: narrow unsigned bv zero-extends to kBitvecWidth", "[encoder][coerce][bv]") {
    auto env = make_env();
    z3::expr v = bv(env, 0xFF, 8);
    z3::expr out = fold::coerceToBv(env, v, /*width=*/8, /*is_unsigned=*/true);
    REQUIRE(out.get_sort().bv_size() == fold::kBitvecWidth);
    REQUIRE(bv_eq(out, 0xFFULL, fold::kBitvecWidth));
}

TEST_CASE("coerceToBv: wide bv truncates at the requested width then re-widens",
          "[encoder][coerce][bv]") {
    auto env = make_env();
    // 64-bit value with bits set above the source-width-32 truncation point.
    z3::expr v = bv(env, 0xFFFF'FFFF'AAAA'BBBBULL, fold::kBitvecWidth);
    z3::expr out = fold::coerceToBv(env, v, /*width=*/32, /*is_unsigned=*/true);
    REQUIRE(out.get_sort().bv_size() == fold::kBitvecWidth);
    // Truncated to 32 bits → 0xAAAABBBB, then zero-extended → 0xAAAABBBB.
    REQUIRE(bv_eq(out, 0xAAAA'BBBBULL, fold::kBitvecWidth));
}

TEST_CASE("coerceToBv: bool maps to 1/0 at width then widens", "[encoder][coerce][bv]") {
    auto env = make_env();
    z3::expr out_true = fold::coerceToBv(env, env.ctx().bool_val(true));
    z3::expr out_false = fold::coerceToBv(env, env.ctx().bool_val(false));
    REQUIRE(out_true.get_sort().bv_size() == fold::kBitvecWidth);
    REQUIRE(bv_eq(out_true, 1, fold::kBitvecWidth));
    REQUIRE(bv_eq(out_false, 0, fold::kBitvecWidth));
}

TEST_CASE("coerceToExactBv: leaves narrow result at exact width", "[encoder][coerce][exact]") {
    auto env = make_env();
    z3::expr v = bv(env, 0xFFFF'FFFF'AAAA'BBBBULL, fold::kBitvecWidth);
    z3::expr out = fold::coerceToExactBv(env, v, /*width=*/32, /*is_unsigned=*/true);
    REQUIRE(out.is_bv());
    REQUIRE(out.get_sort().bv_size() == 32);
    REQUIRE(bv_eq(out, 0xAAAA'BBBBULL, 32));
}

TEST_CASE("coerceToExactBv: bool widens to requested bv width", "[encoder][coerce][exact]") {
    auto env = make_env();
    z3::expr out = fold::coerceToExactBv(env, env.ctx().bool_val(true),
                                         /*width=*/16, /*is_unsigned=*/true);
    REQUIRE(out.get_sort().bv_size() == 16);
    REQUIRE(bv_eq(out, 1, 16));
}

TEST_CASE("coerceToBool: bv compares against zero at its own width", "[encoder][coerce][bool]") {
    auto env = make_env();
    z3::expr zero8 = bv(env, 0, 8);
    z3::expr one8 = bv(env, 1, 8);
    REQUIRE(fold::coerceToBool(env, zero8).simplify().is_false());
    REQUIRE(fold::coerceToBool(env, one8).simplify().is_true());
}

TEST_CASE("coerceToBool: identity on a bool expression", "[encoder][coerce][bool]") {
    auto env = make_env();
    z3::expr t = env.ctx().bool_val(true);
    REQUIRE(fold::coerceToBool(env, t).is_bool());
    REQUIRE(fold::coerceToBool(env, t).simplify().is_true());
}