#include <z3++.h>

#include <catch2/catch_test_macros.hpp>

#include "fold/report/finding.hpp"
#include "fold/symbolic/assumption_provenance.hpp"
#include "fold/symbolic/encoder.hpp"
#include "fold/symbolic/modeling_options.hpp"

using fold::Confidence;
using fold::ModelingOptions;
using fold::SymbolicEnv;
namespace sym = fold::symbolic;

namespace {

z3::expr bv(SymbolicEnv& env, const char* name) { return env.ctx().bv_const(name, 64); }
z3::expr bv(SymbolicEnv& env, int v) { return env.ctx().bv_val(v, 64); }

} // namespace

TEST_CASE("proveUnsat: empty ledger proves without provenance", "[provenance]") {
    SymbolicEnv env = SymbolicEnv::create();
    z3::solver solver(env.ctx(), "QF_BV");
    z3::expr x = bv(env, "x");
    // `x == x` is always true, so the negated goal `x != x` is UNSAT.
    auto r = sym::proveUnsat(solver, env, x != x);
    REQUIRE(r.proved);
    REQUIRE(r.leaned_on.empty());
    // No approximation => confidence stays Proved.
    REQUIRE(sym::downgradeForProvenance(Confidence::Proved, r.leaned_on) == Confidence::Proved);
}

TEST_CASE("proveUnsat: proof that leans on a loop-bound pin is attributed", "[provenance]") {
    SymbolicEnv env = SymbolicEnv::create();
    z3::solver solver(env.ctx(), "QF_BV");
    z3::expr iv = bv(env, "iv");
    // Bounded unrolling pins the induction variable to iteration 0.
    env.addTrackedAssumption(iv == bv(env, 0), sym::AssumptionKind::LoopBoundUnroll,
                             "loop iv 'iv' pinned to 0");

    // The in-bound guard `iv < 6` is "always true" ONLY because of the pin, so
    // the negated goal `iv >= 6` is UNSAT only under the tracked assumption.
    auto r = sym::proveUnsat(solver, env, !(z3::slt(iv, bv(env, 6))));
    REQUIRE(r.proved);
    REQUIRE_FALSE(r.leaned_on.empty());
    REQUIRE(r.leaned_on.front().kind == sym::AssumptionKind::LoopBoundUnroll);

    // Provenance downgrades Proved -> Heuristic.
    REQUIRE(sym::downgradeForProvenance(Confidence::Proved, r.leaned_on) == Confidence::Heuristic);
}

TEST_CASE("proveUnsat: a pin present but not needed keeps Proved", "[provenance]") {
    SymbolicEnv env = SymbolicEnv::create();
    z3::solver solver(env.ctx(), "QF_BV");
    z3::expr iv = bv(env, "iv");
    env.addTrackedAssumption(iv == bv(env, 0), sym::AssumptionKind::LoopBoundUnroll,
                             "loop iv 'iv' pinned to 0");

    // A proof about an unrelated variable that holds regardless of the pin: the
    // UNSAT core must NOT include the loop-bound tracker.
    z3::expr y = bv(env, "y");
    auto r = sym::proveUnsat(solver, env, y != y);
    REQUIRE(r.proved);
    REQUIRE(r.leaned_on.empty());
    REQUIRE(sym::downgradeForProvenance(Confidence::Proved, r.leaned_on) == Confidence::Proved);
}

TEST_CASE("proveUnsat: a satisfiable goal is not proved", "[provenance]") {
    SymbolicEnv env = SymbolicEnv::create();
    z3::solver solver(env.ctx(), "QF_BV");
    z3::expr iv = bv(env, "iv");
    env.addTrackedAssumption(iv == bv(env, 0), sym::AssumptionKind::LoopBoundUnroll, "pin");
    // `iv < 6` is satisfiable (iv could be anything if the pin isn't forced as a
    // hard fact — and even with the pin, the goal `iv < 6` is SAT), so the
    // negated-goal-style query on a non-tautology is not proved.
    auto r = sym::proveUnsat(solver, env, z3::slt(iv, bv(env, 6)));
    REQUIRE_FALSE(r.proved);
    REQUIRE(r.leaned_on.empty());
}

TEST_CASE("shouldSuppressProof honours the loop-bound toggle", "[provenance]") {
    std::vector<sym::AssumptionProvenance> leaned{{sym::AssumptionKind::LoopBoundUnroll, "pin"}};

    ModelingOptions off; // all false
    REQUIRE_FALSE(sym::shouldSuppressProof(leaned, off));

    ModelingOptions on;
    on.suppress_loop_bound_always_conditions = true;
    REQUIRE(sym::shouldSuppressProof(leaned, on));

    // A non-loop approximation is not suppressed by the loop-bound toggle.
    std::vector<sym::AssumptionProvenance> ext{
        {sym::AssumptionKind::ExternalSymbolConcretized, "edata"}};
    REQUIRE_FALSE(sym::shouldSuppressProof(ext, on));
}

TEST_CASE("annotateMessageWithProvenance names the approximation", "[provenance]") {
    std::vector<sym::AssumptionProvenance> leaned{{sym::AssumptionKind::LoopBoundUnroll, "pin"}};
    const std::string msg = sym::annotateMessageWithProvenance("Condition is always true", leaned);
    REQUIRE(msg.find("bounded-unroll loop bound") != std::string::npos);

    // Empty leaned_on leaves the message untouched.
    REQUIRE(sym::annotateMessageWithProvenance("unchanged", {}) == "unchanged");
}