#include <catch2/catch_test_macros.hpp>

#include "fold/detect/model_validation.hpp"
#include "fold/symbolic/tactics.hpp"

TEST_CASE("symbolic models validate argument indexes against available arity",
          "[symbolic][model-validation]") {
    using fold::detect::validModeledArgument;
    CHECK(validModeledArgument(0, 1));
    CHECK(validModeledArgument(1, 2, 2));
    CHECK_FALSE(validModeledArgument(-1, 2));
    CHECK_FALSE(validModeledArgument(2, 2));
    CHECK_FALSE(validModeledArgument(1, 2, 1));
}

TEST_CASE("assumption checks fail closed on unsupported distinct translation",
          "[symbolic][model-validation][translator]") {
    z3::context solver_ctx;
    z3::context expression_ctx;
    z3::solver solver(solver_ctx, "QF_BV");
    const z3::expr unknown = expression_ctx.bv_const("unknown", 64);
    const z3::expr narrow = z3::zext(unknown.extract(7, 0), 56).simplify();
    z3::expr_vector assumptions(expression_ctx);
    assumptions.push_back(narrow != expression_ctx.bv_val(0, 64));

    z3::check_result result = z3::sat;
    CHECK_NOTHROW(result = fold::symbolic::checkWithAssumptionsFailClosed(solver, assumptions));
    CHECK(result == z3::unknown);
}

TEST_CASE("portfolio profiling records bounded expression-free query telemetry",
          "[symbolic][profile][portfolio]") {
    z3::context ctx;
    z3::solver solver(ctx, "QF_BV");
    const z3::expr value = ctx.bv_const("value", 64);
    solver.add(value == ctx.bv_val(7, 64));
    z3::expr_vector assumptions(ctx);

    fold::SolverStats stats;
    stats.profiling_enabled = true;
    const z3::check_result result =
        fold::symbolic::checkWithPortfolio(solver, assumptions, 100, stats);
    REQUIRE(result == z3::sat);
    REQUIRE(stats.query_samples.size() == 1);
    const auto& sample = stats.query_samples.front();
    CHECK(sample.canonical_hash != 0);
    CHECK(sample.ast_nodes >= 3);
    CHECK(sample.max_depth >= 2);
    CHECK(sample.symbols == 1);
    CHECK(sample.assertions == 1);
    CHECK(sample.max_bv_width == 64);
    CHECK(sample.bv_ops >= 1);
    CHECK(sample.equality_ops == 1);
    CHECK((sample.winner == "smt" || sample.winner == "bitblast"));
    CHECK(sample.result == "sat");

    fold::SolverStats incremental_stats;
    incremental_stats.profiling_enabled = true;
    REQUIRE(fold::symbolic::checkWithAssumptionsProfiled(solver, assumptions, incremental_stats) ==
            z3::sat);
    REQUIRE(incremental_stats.query_samples.size() == 1);
    CHECK(incremental_stats.query_samples[0].canonical_hash == sample.canonical_hash);
    CHECK(incremental_stats.query_samples[0].winner == "incremental");

    z3::solver renamed_solver(ctx, "QF_BV");
    const z3::expr renamed_value = ctx.bv_const("different_generated_name_917", 64);
    renamed_solver.add(renamed_value == ctx.bv_val(7, 64));
    fold::SolverStats renamed_stats;
    renamed_stats.profiling_enabled = true;
    REQUIRE(fold::symbolic::checkWithAssumptionsProfiled(renamed_solver, assumptions,
                                                         renamed_stats) == z3::sat);
    REQUIRE(renamed_stats.query_samples.size() == 1);
    CHECK(renamed_stats.query_samples[0].canonical_hash == sample.canonical_hash);

    for (std::size_t i = 0; i < fold::SolverStats::kMaxQuerySamples + 2; ++i)
        stats.recordQuerySample({.canonical_hash = i + 1});
    CHECK(stats.query_samples.size() == fold::SolverStats::kMaxQuerySamples);
    CHECK(stats.query_samples_dropped == 3);
}

TEST_CASE("nonlinear bit-vector routing is shape-specific", "[symbolic][validation]") {
    z3::context ctx;
    const z3::expr x = ctx.bv_const("x", 64);
    const z3::expr y = ctx.bv_const("y", 64);
    z3::expr_vector assumptions(ctx);

    z3::solver linear(ctx, "QF_BV");
    linear.add(x == ctx.bv_val(4, 64));
    CHECK_FALSE(fold::symbolic::isNonlinearBitVectorQuery(linear, assumptions));

    z3::solver nonlinear(ctx, "QF_BV");
    nonlinear.add(x * y == ctx.bv_val(4, 64));
    CHECK(fold::symbolic::isNonlinearBitVectorQuery(nonlinear, assumptions));

    const z3::expr memory = ctx.constant("memory", ctx.array_sort(ctx.bv_sort(64), ctx.bv_sort(8)));
    z3::solver with_array(ctx);
    with_array.add(x * y == ctx.bv_val(4, 64));
    with_array.add(z3::select(memory, x) == ctx.bv_val(0, 8));
    CHECK_FALSE(fold::symbolic::isNonlinearBitVectorQuery(with_array, assumptions));
}

TEST_CASE("portfolio translation accepts Fold theory and rejects unsupported expressions",
          "[symbolic][model-validation][portfolio]") {
    z3::context ctx;
    const z3::expr bv = ctx.bv_const("bv", 64);
    const z3::expr predicate = bv == ctx.bv_val(7, 64);
    CHECK(fold::symbolic::isPortfolioExpressionSupported(predicate));

    const z3::sort bytes = ctx.array_sort(ctx.bv_sort(64), ctx.bv_sort(8));
    const z3::expr memory = ctx.constant("memory", bytes);
    CHECK(
        fold::symbolic::isPortfolioExpressionSupported(z3::select(memory, bv) == ctx.bv_val(0, 8)));

    const z3::expr integer = ctx.int_const("integer");
    CHECK_FALSE(fold::symbolic::isPortfolioExpressionSupported(integer > 0));
    CHECK_FALSE(fold::symbolic::isPortfolioExpressionSupported(z3::forall(bv, predicate)));

    z3::solver unsupported_solver(ctx);
    unsupported_solver.add(integer > 0);
    z3::expr_vector assumptions(ctx);
    fold::SolverStats stats;
    CHECK(fold::symbolic::checkWithPortfolio(unsupported_solver, assumptions, 100, stats) ==
          z3::unknown);
}

TEST_CASE("portfolio verdicts stand only when the re-check agrees", "[portfolio][soundness]") {
    // The re-check used to be consulted only for its model/core; a SAT
    // portfolio verdict whose re-check timed out was still reported as SAT.
    using fold::symbolic::reconcilePortfolioRecheck;
    CHECK(reconcilePortfolioRecheck(z3::sat, z3::sat) == z3::sat);
    CHECK(reconcilePortfolioRecheck(z3::unsat, z3::unsat) == z3::unsat);
    CHECK(reconcilePortfolioRecheck(z3::sat, z3::unknown) == z3::unknown);
    CHECK(reconcilePortfolioRecheck(z3::unsat, z3::unknown) == z3::unknown);
    CHECK(reconcilePortfolioRecheck(z3::sat, z3::unsat) == z3::unknown);
    CHECK(reconcilePortfolioRecheck(z3::unsat, z3::sat) == z3::unknown);
}

TEST_CASE("portfolio re-check on the reporting solver records disagreements",
          "[portfolio][soundness]") {
    // A disagreement used to be silent, and the detectors memoized the
    // re-check's unsat core even when the verdict became unknown.
    z3::context ctx;
    z3::solver solver(ctx, "QF_BV");
    const z3::expr value = ctx.bv_const("value", 64);
    solver.add(value == ctx.bv_val(7, 64));
    z3::expr_vector assumptions(ctx);
    using fold::symbolic::recheckPortfolioVerdict;

    fold::SolverStats stats;
    CHECK(recheckPortfolioVerdict(solver, assumptions, z3::sat, stats) == z3::sat);
    CHECK(stats.portfolio_disagreements == 0);
    CHECK(recheckPortfolioVerdict(solver, assumptions, z3::unknown, stats) == z3::unknown);
    CHECK(stats.portfolio_disagreements == 0);
    CHECK(recheckPortfolioVerdict(solver, assumptions, z3::unsat, stats) == z3::unknown);
    CHECK(stats.portfolio_disagreements == 1);

    fold::SolverStats merged;
    merged.merge(stats);
    CHECK(merged.portfolio_disagreements == 1);
}