// Matrix row Z5 — refine a SAT model into a "minimal witness" with
// smaller integer values, so fuzz seeds emit human-readable params
// (e.g., `arg=1` instead of `arg=0xDEADBEEF`).
//
// Contract pins:
//   1. A model refined from `solver.check()` has integer-witness values
//      no larger than the vanilla model's, for each refined param.
//   2. The refined model still satisfies the original path predicate
//      (refinement never invents an infeasible assignment).
//   3. Refining a path that's already minimal is a no-op (or produces
//      equal-magnitude values).
//   4. Multiple-param refinement minimizes each independently subject
//      to the joint constraints.

#include <z3++.h>

#include <catch2/catch_test_macros.hpp>
#include <cstdint>
#include <vector>

#include "fold/fuzz/minimal_witness.hpp"

using fold::fuzz::refineModelForMinimalWitness;

namespace {

std::uint64_t numeralU64(const z3::expr& e) {
    std::uint64_t v = 0;
    REQUIRE(e.is_numeral_u64(v));
    return v;
}

} // namespace

TEST_CASE("minimal-witness: refines a single integer param to its smallest value",
          "[fuzz][z5][refine]") {
    z3::context c;
    z3::expr x = c.bv_const("x", 64);
    z3::expr path = (x > c.bv_val(0, 64)) && (x < c.bv_val(1000000, 64));

    z3::solver s(c);
    s.add(path);
    REQUIRE(s.check() == z3::sat);
    z3::model vanilla = s.get_model();

    auto refined = refineModelForMinimalWitness(c, path, {x});
    REQUIRE(refined.has_value());

    const std::uint64_t vanilla_x = numeralU64(vanilla.eval(x));
    const std::uint64_t refined_x = numeralU64(refined->eval(x));
    REQUIRE(refined_x <= vanilla_x);
    REQUIRE(refined_x == 1); // path requires x > 0, smallest is 1
}

TEST_CASE("minimal-witness: refined model still satisfies the path predicate",
          "[fuzz][z5][soundness]") {
    z3::context c;
    z3::expr x = c.bv_const("x", 64);
    z3::expr y = c.bv_const("y", 64);
    z3::expr path = (x + y == c.bv_val(100, 64)) && (x > c.bv_val(0, 64)) && (y > c.bv_val(0, 64));

    auto refined = refineModelForMinimalWitness(c, path, {x, y});
    REQUIRE(refined.has_value());

    z3::solver s(c);
    s.add(path);
    s.add(x == refined->eval(x));
    s.add(y == refined->eval(y));
    REQUIRE(s.check() == z3::sat);
}

TEST_CASE("minimal-witness: already-minimal path returns same magnitudes", "[fuzz][z5][noop]") {
    z3::context c;
    z3::expr x = c.bv_const("x", 64);
    z3::expr path = (x == c.bv_val(42, 64));

    auto refined = refineModelForMinimalWitness(c, path, {x});
    REQUIRE(refined.has_value());
    REQUIRE(numeralU64(refined->eval(x)) == 42);
}

TEST_CASE("minimal-witness: multi-param refinement reduces each independently",
          "[fuzz][z5][multi]") {
    z3::context c;
    z3::expr a = c.bv_const("a", 64);
    z3::expr b = c.bv_const("b", 64);
    z3::expr path = (a > c.bv_val(5, 64)) && (b > c.bv_val(10, 64));

    auto refined = refineModelForMinimalWitness(c, path, {a, b});
    REQUIRE(refined.has_value());

    REQUIRE(numeralU64(refined->eval(a)) == 6);  // smallest a > 5
    REQUIRE(numeralU64(refined->eval(b)) == 11); // smallest b > 10
}

TEST_CASE("minimal-witness: empty param list returns a model of the path alone",
          "[fuzz][z5][empty]") {
    z3::context c;
    z3::expr x = c.bv_const("x", 64);
    z3::expr path = (x > c.bv_val(0, 64));

    auto refined = refineModelForMinimalWitness(c, path, {});
    REQUIRE(refined.has_value());
    // With no minimization targets, optimize behaves like a normal solver.
    // Just require SAT-feasibility — value is arbitrary.
    z3::solver s(c);
    s.add(path);
    s.add(x == refined->eval(x));
    REQUIRE(s.check() == z3::sat);
}