//! Behavioural tests for the solver, driven entirely through the public API
//! (parse → compile → solve), so they live as integration tests.
use elenchus_compiler::{KIND_UNSAT, Value, kw};
use elenchus_solver::*;
use std::collections::BTreeSet;

/// Verify a single inline source under a default `DOMAIN t` (so test programs
/// need not repeat it); atoms land in domain `t`, labelled `t.subject …`.
fn vs(src: &str) -> Result<Report, CompileError> {
    verify_source("t.vrf", &format!("DOMAIN t\n{src}"))
}

#[test]
fn clean_consistent() {
    let r = vs("FACT x a\nCHECK x\n").unwrap();
    assert_eq!(r.status, Status::Consistent);
    assert!(r.conflicts.is_empty() && r.warnings.is_empty());
}

#[test]
fn fact_contradiction_is_conflict() {
    let r = vs("FACT x a\nNOT x a\n").unwrap();
    assert_eq!(r.status, Status::Conflict);
    assert_eq!(r.conflicts.len(), 1);
}

#[test]
fn exclusive_violation_is_conflict() {
    let src = include_str!("../../../docs/examples/conflict.vrf");
    let r = verify_source("conflict.vrf", src).unwrap();
    assert_eq!(r.status, Status::Conflict);
    assert_eq!(
        r.conflicts[0].origin.premise.as_deref(),
        Some("fly_xor_swim")
    );
    assert_eq!(r.conflicts[0].atoms.len(), 2);
}

#[test]
fn exclusive_with_unknown_is_consistent_not_warning() {
    // flying TRUE, swimming UNKNOWN — at most one can hold, no conflict, no warning.
    let r = vs(r"
        FACT A has flying
        PREMISE e:
            EXCLUSIVE
                A has flying
                A has swimming
        ")
    .unwrap();
    assert_eq!(r.status, Status::Consistent);
    assert!(r.warnings.is_empty());
}

#[test]
fn exists_witness_that_holds_is_consistent() {
    // The author names the witness; the engine checks it holds. `auth is ready` is
    // asserted, so the existential is satisfied — no SET needed.
    let r = vs("FACT auth is ready\nPREMISE p:\n    EXISTS h WITNESS auth\n        h is ready\nCHECK auth\n")
        .unwrap();
    assert_eq!(r.status, Status::Consistent);
    assert!(r.conflicts.is_empty());
}

#[test]
fn exists_witness_that_fails_is_conflict() {
    // The named witness is forced FALSE elsewhere → the existential cannot be met by
    // it: CONFLICT, blamed on the EXISTS premise.
    let r = vs("NOT auth is ready\nPREMISE p:\n    EXISTS h WITNESS auth\n        h is ready\n")
        .unwrap();
    assert_eq!(r.status, Status::Conflict);
    assert_eq!(r.conflicts.len(), 1);
    assert_eq!(r.conflicts[0].origin.premise.as_deref(), Some("p"));
    assert_eq!(r.conflicts[0].origin.kind, kw::EXISTS);
}

#[test]
fn exists_unwitnessed_is_warning() {
    // ∃ that names neither a SET nor a WITNESS cannot be checked — the forge voice:
    // WARNING with a hint to name a witness, not a clause and not a blow-up.
    let r = vs("PREMISE someone_ready:\n    EXISTS h\n        h is ready\n").unwrap();
    assert_eq!(r.status, Status::Warning);
    assert_eq!(r.warnings.len(), 1);
    assert_eq!(
        r.warnings[0].origin.premise.as_deref(),
        Some("someone_ready")
    );
    assert_eq!(r.warnings[0].blocked_by, vec![String::from("t.h is ready")]);
    assert!(r.warnings[0].hint.as_deref().unwrap().contains("WITNESS"));
}

#[test]
fn exists_unwitnessed_warning_does_not_hide_a_conflict() {
    // A real CONFLICT still wins over the unwitnessed-∃ WARNING (verdict precedence).
    let r = vs("FACT x a\nNOT x a\nPREMISE p:\n    EXISTS h\n        h is ready\n").unwrap();
    assert_eq!(r.status, Status::Conflict);
}

// --- FACT … BECAUSE (justification / L2) -----------------------------------

#[test]
fn fact_because_ground_holds_is_consistent() {
    // The author cites a ground; the engine checks it holds. `db reachable` is
    // asserted TRUE, so the justification stands — no clause, no noise.
    let r = vs("FACT db reachable\nFACT api healthy BECAUSE db reachable\nCHECK api\n").unwrap();
    assert_eq!(r.status, Status::Consistent);
    assert!(r.conflicts.is_empty() && r.warnings.is_empty());
    // Neither the belief nor the ground is an inert leftover: the justification uses
    // both, so the orphan lint must stay silent.
    assert!(r.orphans.is_empty());
}

#[test]
fn fact_because_ground_derived_by_rule_holds_is_consistent() {
    // The ground need not be asserted directly — a RULE that derives it also
    // satisfies the justification (the check reads the settled model value).
    let r = vs(
        "FACT db up\nRULE r:\n    WHEN db up\n    THEN db reachable\nFACT api healthy BECAUSE db reachable\nCHECK api\n",
    )
    .unwrap();
    assert_eq!(r.status, Status::Consistent);
}

#[test]
fn fact_because_ground_false_is_conflict() {
    // The cited ground is forced FALSE → the stated reason does not hold: CONFLICT,
    // blamed on the BECAUSE, and its trace explains why the ground is false.
    let r = vs("NOT db reachable\nFACT api healthy BECAUSE db reachable\nCHECK api\n").unwrap();
    assert_eq!(r.status, Status::Conflict);
    assert_eq!(r.conflicts.len(), 1);
    assert_eq!(r.conflicts[0].origin.kind, kw::BECAUSE);
    assert!(r.conflicts[0].atoms[0].contains("t.db reachable is FALSE"));
    // The trace names the NOT that forced the ground false.
    assert!(!r.conflicts[0].trace.is_empty());
}

#[test]
fn fact_because_ground_unknown_is_warning() {
    // The cited ground is never established (stays UNKNOWN) → the reason is
    // unestablished: WARNING with a hint to establish it, not a clause.
    let r = vs("FACT api healthy BECAUSE db reachable\nCHECK api\n").unwrap();
    assert_eq!(r.status, Status::Warning);
    assert_eq!(r.warnings.len(), 1);
    assert_eq!(r.warnings[0].origin.kind, kw::BECAUSE);
    assert_eq!(
        r.warnings[0].blocked_by,
        vec![String::from("t.db reachable")]
    );
    assert!(r.warnings[0].hint.as_deref().unwrap().contains("FACT"));
}

#[test]
fn fact_because_unknown_ground_does_not_hide_a_conflict() {
    // A real CONFLICT wins over the unestablished-ground WARNING (verdict precedence).
    let r = vs("FACT x a\nNOT x a\nFACT api healthy BECAUSE db reachable\n").unwrap();
    assert_eq!(r.status, Status::Conflict);
}

#[test]
fn plain_fact_is_unaffected_by_the_justification_layer() {
    // A FACT with no BECAUSE never produces a justification conflict/warning.
    let r = vs("FACT api healthy\nCHECK api\n").unwrap();
    assert_eq!(r.status, Status::Consistent);
    assert!(r.conflicts.is_empty() && r.warnings.is_empty());
}

#[test]
fn because_chain_all_grounds_hold_is_consistent() {
    // A ground may itself be a justified FACT, so BECAUSE composes: each link is
    // checked independently and, when every link holds, the whole chain stands. No
    // extra machinery — the chain is emergent from the one-hop check.
    let r = vs(
        "FACT net up\nFACT db reachable BECAUSE net up\nFACT api healthy BECAUSE db reachable\nCHECK api\n",
    )
    .unwrap();
    assert_eq!(r.status, Status::Consistent);
    assert!(r.conflicts.is_empty() && r.warnings.is_empty());
}

#[test]
fn because_chain_surfaces_the_weakest_link() {
    // The deepest ground (`net up`) is never established; the chain's WARNING points
    // straight at that weakest link, not at the top-level claim.
    let r =
        vs("FACT db reachable BECAUSE net up\nFACT api healthy BECAUSE db reachable\nCHECK api\n")
            .unwrap();
    assert_eq!(r.status, Status::Warning);
    assert_eq!(r.warnings.len(), 1);
    assert_eq!(r.warnings[0].blocked_by, vec![String::from("t.net up")]);
}

#[test]
fn because_chain_deep_false_ground_is_conflict() {
    // A false ground anywhere in the chain surfaces as a CONFLICT at that link.
    let r = vs(
        "NOT net up\nFACT db reachable BECAUSE net up\nFACT api healthy BECAUSE db reachable\nCHECK api\n",
    )
    .unwrap();
    assert_eq!(r.status, Status::Conflict);
    assert!(r.conflicts[0].atoms[0].contains("t.net up is FALSE"));
}

#[test]
fn fact_because_unknown_ground_under_bidirectional_stays_warning() {
    // The interned-but-free ground does not manufacture a spurious UNDERDETERMINED
    // under BIDIRECTIONAL (the backward pass does not project an unconstrained
    // ground); the justification WARNING is the verdict.
    let r = vs("FACT api healthy BECAUSE db reachable\nCHECK BIDIRECTIONAL\n").unwrap();
    assert_eq!(r.status, Status::Warning);
    assert_eq!(r.warnings.len(), 1);
    assert_eq!(r.warnings[0].origin.kind, kw::BECAUSE);
}

#[test]
fn implication_missing_consequent_is_warning() {
    // WHEN flying THEN wing: flying TRUE, wing UNKNOWN → blocked → WARNING.
    let r = vs(r#"
        FACT A has flying
        PREMISE w:
            WHEN A has flying
            THEN A has wing
        "#)
    .unwrap();
    assert_eq!(r.status, Status::Warning);
    assert_eq!(r.warnings.len(), 1);
    assert_eq!(r.warnings[0].blocked_by, vec![String::from("t.A has wing")]);
}

#[test]
fn warning_hint_points_at_rule_when_atom_is_a_free_input() {
    // `A has wing` is nothing's consequent: it can only be set by a FACT, or by
    // turning a PREMISE meant to establish it into a RULE. The hint says so.
    let r = vs(r"
        FACT A has flying
        PREMISE w:
            WHEN A has flying
            THEN A has wing
        ")
    .unwrap();
    let hint = r.warnings[0].hint.as_deref().unwrap();
    assert!(hint.contains("make that PREMISE a RULE"), "{hint}");
    assert!(hint.contains("t.A has wing"), "{hint}");
}

#[test]
fn warning_hint_points_at_antecedent_when_a_rule_could_derive_it() {
    // `c ready` IS a RULE consequent, but the rule has not fired (its `x trigger`
    // is UNKNOWN). The blocking premise's hint sends you to the rule's input.
    let r = vs(r"
        RULE d:
            WHEN x trigger
            THEN c ready
        FACT go now
        PREMISE p:
            WHEN go now
            THEN c ready
        ")
    .unwrap();
    assert_eq!(r.status, Status::Warning);
    let hint = r.warnings[0].hint.as_deref().unwrap();
    assert!(
        hint.contains("derived by a RULE that has not fired"),
        "{hint}"
    );
}

#[test]
fn human_report_dedupes_repeated_fix_lines() {
    // Three *distinct* premises all blocked: p1 and p2 by the SAME atom
    // (`gate one_ok`, via different antecedents so the clauses don't dedupe)
    // → one identical fix, deduped; p3 by a different atom → its own fix. So:
    // 3 warnings, but only 2 distinct `fix:` lines in the human report (while
    // every warning still carries its hint in the structured data / JSON).
    let r = vs(r"
        FACT a on
        FACT b on
        PREMISE p1:
            WHEN a on
            THEN gate one_ok
        PREMISE p2:
            WHEN b on
            THEN gate one_ok
        PREMISE p3:
            WHEN a on
            THEN gate two_ok
        ")
    .unwrap();
    assert_eq!(r.warnings.len(), 3);
    // Every warning keeps its hint in the structured form.
    assert!(r.warnings.iter().all(|w| w.hint.is_some()));
    let distinct_hints: BTreeSet<&str> = r
        .warnings
        .iter()
        .filter_map(|w| w.hint.as_deref())
        .collect();
    assert_eq!(distinct_hints.len(), 2);
    // The human report prints exactly one `fix:` per distinct hint.
    let text = format!("{r}");
    let shown = text
        .lines()
        .filter(|l| l.trim_start().starts_with("fix:"))
        .count();
    assert_eq!(shown, distinct_hints.len());
}

#[test]
fn implication_satisfied_is_consistent() {
    let r = vs(r"
        FACT A has flying
        FACT A has wing
        PREMISE w:
            WHEN A has flying
            THEN A has wing
        ")
    .unwrap();
    assert_eq!(r.status, Status::Consistent);
}

#[test]
fn implication_violated_is_conflict() {
    // antecedent TRUE, consequent FALSE → CONFLICT.
    let r = vs(r"
        FACT A has flying
        NOT A has wing
        PREMISE w:
            WHEN A has flying
            THEN A has wing
        ")
    .unwrap();
    assert_eq!(r.status, Status::Conflict);
}

#[test]
fn rule_derives_fact() {
    let r = vs(r#"
        FACT A has flying
        RULE o:
            WHEN A has flying
            THEN A needs oxygen
        "#)
    .unwrap();
    assert_eq!(r.status, Status::Consistent);
    assert_eq!(r.derived.len(), 1);
    assert_eq!(r.derived[0].atom, "t.A needs oxygen");
}

#[test]
fn rule_derivation_contradiction_is_conflict() {
    // rule derives `A needs oxygen` TRUE, but it's asserted FALSE.
    let r = vs(r"
        FACT A has flying
        NOT A needs oxygen
        RULE o:
            WHEN A has flying
            THEN A needs oxygen
        ")
    .unwrap();
    assert_eq!(r.status, Status::Conflict);
}

#[test]
fn bidirectional_finds_alternative_model_underdetermined() {
    // EXCLUSIVE(a,b) with no facts: {FF, TF, FT} all satisfy → not unique.
    let r = vs(r#"
        PREMISE e:
            EXCLUSIVE
                x a
                x b
        CHECK x BIDIRECTIONAL
        "#)
    .unwrap();
    assert_eq!(r.status, Status::Underdetermined);
}

#[test]
fn fact_pins_unique_model_consistent() {
    // Same premise, but FACT x a forces b false → the only model → CONSISTENT.
    let r = vs(r#"
        FACT x a
        PREMISE e:
            EXCLUSIVE
                x a
                x b
        CHECK x BIDIRECTIONAL
        "#)
    .unwrap();
    assert_eq!(r.status, Status::Consistent);
}

#[test]
fn no_bidirectional_skips_backward_pass() {
    // Plain CHECK: alternatives are not searched → stays CONSISTENT, not UNDERDETERMINED.
    let r = vs(r#"
        PREMISE e:
            EXCLUSIVE
                x a
                x b
        CHECK x
        "#)
    .unwrap();
    assert_eq!(r.status, Status::Consistent);
}

#[test]
fn creature_example_forward_pass() {
    let src = include_str!("../../../docs/examples/creature.vrf");
    let r = verify_source("creature.vrf", src).unwrap();
    // fly_xor_swim & no_dual_temp consistent; wings_need_bone → 2 warnings
    // (wing, bone); needs_oxygen derived; no conflicts.
    assert_eq!(r.status, Status::Warning);
    assert!(r.conflicts.is_empty());
    assert_eq!(r.warnings.len(), 2);
    assert_eq!(r.derived.len(), 1);
    assert_eq!(r.derived[0].atom, "creatures.Creature_A needs oxygen");
}

#[test]
fn roles_puzzle_is_uniquely_solved() {
    // 3 people × 3 roles, ONEOF per person and per role, two clues. The
    // backward (SAT) pass must find the assignment satisfiable AND unique —
    // i.e. CONSISTENT, not UNDERDETERMINED.
    let src = include_str!("../../../docs/examples/roles-puzzle.vrf");
    let r = verify_source("roles-puzzle.vrf", src).unwrap();
    assert_eq!(r.status, Status::Consistent);
    assert!(r.conflicts.is_empty());
    assert!(r.underdetermined.is_none());
}

#[test]
fn roles_puzzle_underdetermined_without_a_clue() {
    // Drop the `NOT bob is qa` clue and the solution is no longer unique
    // (bob/carol can swap dev/qa) — the SAT pass reports UNDERDETERMINED.
    // Normalize CRLF first: on a Windows checkout include_str! embeds the file
    // with \r\n, so a literal "...\n" match would otherwise miss the line.
    let src = include_str!("../../../docs/examples/roles-puzzle.vrf")
        .replace("\r\n", "\n")
        .replace("NOT  bob is qa\n", "");
    let r = verify_source("roles-puzzle.vrf", &src).unwrap();
    assert_eq!(r.status, Status::Underdetermined);
}

#[test]
fn socrates_chain_is_a_conflict() {
    // human → animal → living → mortal (3 derivations), then mortal EXCLUSIVE
    // immortal with `immortal` asserted → CONFLICT on the exclusivity premise.
    let src = include_str!("../../../docs/examples/socrates.vrf");
    let r = verify_source("socrates.vrf", src).unwrap();
    assert_eq!(r.status, Status::Conflict);
    assert_eq!(r.conflicts.len(), 1);
    assert_eq!(
        r.conflicts[0].origin.premise.as_deref(),
        Some("mortal_xor_immortal")
    );
    assert_eq!(r.derived.len(), 3); // animal, living, mortal
}

// --- conflict explainability: derivation trace + minimal unsat core ------

#[test]
fn forward_conflict_carries_a_trace_of_its_facts() {
    let r = vs(r#"
        FACT x a
        FACT x b
        PREMISE e:
            EXCLUSIVE
                x a
                x b
        CHECK x
        "#)
    .unwrap();
    assert_eq!(r.status, Status::Conflict);
    let t = &r.conflicts[0].trace;
    assert_eq!(t.len(), 2);
    assert_eq!(t[0].atom, "t.x a");
    assert_eq!(t[0].value, Value::True);
    assert!(matches!(t[0].reason, TraceReason::Asserted(_)));
    assert!(r.unsat_core.is_empty());
}

#[test]
fn derivation_chain_is_traced_back_to_the_root_fact() {
    // human → animal → living → mortal, then mortal XOR immortal (immortal asserted).
    let src = include_str!("../../../docs/examples/socrates.vrf");
    let r = verify_source("socrates.vrf", src).unwrap();
    let t = &r.conflicts[0].trace;
    // human (fact) + animal, living, mortal (derived) + immortal (fact) = 5 steps,
    // supports before dependents.
    assert_eq!(t.len(), 5);
    assert_eq!(t[0].atom, "philosophy.socrates is human");
    assert!(matches!(t[0].reason, TraceReason::Asserted(_)));
    let mortal = t
        .iter()
        .find(|s| s.atom == "philosophy.socrates is mortal")
        .unwrap();
    match &mortal.reason {
        TraceReason::Derived { from, .. } => {
            assert_eq!(from, &vec![String::from("philosophy.socrates is living")]);
        }
        _ => panic!("mortal should be derived, not asserted"),
    }
}

#[test]
fn direct_fact_contradiction_has_no_trace() {
    let r = vs("FACT x a\nNOT x a\nCHECK x\n").unwrap();
    assert_eq!(r.status, Status::Conflict);
    assert!(r.conflicts[0].trace.is_empty());
}

#[test]
fn jointly_unsatisfiable_reports_a_minimal_core() {
    // ONEOF(a,b); a→c; b→c; NOT c. Unsat only via case-split, so the forward
    // pass misses it and the backward pass produces the core.
    let src = r#"
        PREMISE one:
            ONEOF
                x a
                x b
        PREMISE ac:
            WHEN x a
            THEN x c
        PREMISE bc:
            WHEN x b
            THEN x c
        NOT x c
        CHECK x BIDIRECTIONAL
        "#;
    let r = vs(src).unwrap();
    assert_eq!(r.status, Status::Conflict);
    assert_eq!(r.conflicts[0].origin.kind, KIND_UNSAT);
    assert_eq!(r.unsat_core.len(), 4);
    let labels: Vec<&str> = r.unsat_core.iter().map(|c| c.label.as_str()).collect();
    assert!(labels.contains(&"one"));
    assert!(labels.contains(&"t.x c")); // the bare NOT fact is labelled by its atom
}

#[test]
fn unsat_core_excludes_irrelevant_constructs() {
    // The same unsat cluster, plus an unrelated fact + premise that must not
    // appear in the (irreducible) core.
    let src = r#"
        PREMISE one:
            ONEOF
                x a
                x b
        PREMISE ac:
            WHEN x a
            THEN x c
        PREMISE bc:
            WHEN x b
            THEN x c
        NOT x c
        FACT z here
        PREMISE noise:
            EXCLUSIVE
                z here
                z gone
        CHECK x BIDIRECTIONAL
        "#;
    let r = vs(src).unwrap();
    assert_eq!(r.status, Status::Conflict);
    assert_eq!(r.unsat_core.len(), 4);
    let labels: Vec<&str> = r.unsat_core.iter().map(|c| c.label.as_str()).collect();
    assert!(!labels.contains(&"noise"));
    assert!(!labels.iter().any(|l| l.contains("here")));
}

#[test]
fn unsat_core_blames_the_rules_that_form_it() {
    // Same case-split unsat as `jointly_unsatisfiable_reports_a_minimal_core`,
    // but the implications are RULEs (→ `c.rules`), not PREMISEs (→ `c.clauses`).
    // This is the only path that drives the RULE branch of `constructs`, so the
    // minimal core must name the two rules (plus `one` and the `NOT x c` fact).
    let src = r#"
        PREMISE one:
            ONEOF
                x a
                x b
        RULE ac:
            WHEN x a
            THEN x c
        RULE bc:
            WHEN x b
            THEN x c
        NOT x c
        CHECK x BIDIRECTIONAL
        "#;
    let r = vs(src).unwrap();
    assert_eq!(r.status, Status::Conflict);
    assert_eq!(r.conflicts[0].origin.kind, KIND_UNSAT);
    assert_eq!(r.unsat_core.len(), 4);
    let labels: Vec<&str> = r.unsat_core.iter().map(|c| c.label.as_str()).collect();
    assert!(labels.contains(&"one"));
    assert!(labels.contains(&"ac"));
    assert!(labels.contains(&"bc"));
    assert!(labels.contains(&"t.x c")); // the bare NOT fact, labelled by its atom
}

#[test]
fn consistent_report_has_empty_core_and_no_trace() {
    let r = vs("FACT x a\nCHECK x BIDIRECTIONAL\n").unwrap();
    assert_eq!(r.status, Status::Consistent);
    assert!(r.unsat_core.is_empty());
    assert!(r.conflicts.is_empty());
}

// --- ASSUME: soft (retractable) hypotheses -----------------------------

#[test]
fn compatible_assumptions_behave_like_facts() {
    // ASSUME that does not clash with anything → ordinary CONSISTENT, and the
    // assumption participates like a fact (no retract, no conflict).
    let r = vs("ASSUME rel in_prod\nFACT rel reviewed\nCHECK rel\n").unwrap();
    assert_eq!(r.status, Status::Consistent);
    assert!(r.retract.is_empty());
    assert!(r.conflicts.is_empty());
}

#[test]
fn assume_drives_a_rule_like_a_fact() {
    // A soft assumption fires forward chaining just like a hard fact.
    let r = vs(r"
        ASSUME A has flying
        RULE o:
            WHEN A has flying
            THEN A needs oxygen
        CHECK A
        ")
    .unwrap();
    assert_eq!(r.status, Status::Consistent);
    assert_eq!(r.derived.len(), 1);
    assert_eq!(r.derived[0].atom, "t.A needs oxygen");
}

#[test]
fn clashing_assumptions_yield_conflict_with_a_retract_set() {
    // in_prod needs a rollback OR a feature flag; assuming in_prod plus
    // neither makes the premise unsatisfiable — but only via the guesses.
    let src = r#"
        FACT rel reviewed
        PREMISE prod_needs_safety:
            WHEN rel in_prod
            THEN rel has_rollback
            OR   rel has_feature_flag
        ASSUME rel in_prod
        ASSUME NOT rel has_rollback
        ASSUME NOT rel has_feature_flag
        CHECK rel
        "#;
    let r = vs(src).unwrap();
    assert_eq!(r.status, Status::Conflict);
    assert_eq!(r.exit_code(), 2);
    // All three guesses are jointly to blame: dropping any one fixes it.
    assert_eq!(r.retract.len(), 3, "{:?}", r.retract);
    let labels: Vec<&str> = r.retract.iter().map(|it| it.label.as_str()).collect();
    assert!(labels.contains(&"t.rel in_prod"));
    assert!(labels.contains(&"NOT t.rel has_rollback"));
    assert!(labels.contains(&"NOT t.rel has_feature_flag"));
    // Every retract item is an ASSUME — a FACT/PREMISE is never blamed.
    assert!(r.retract.iter().all(|it| it.origin.kind == kw::ASSUME));
    // The human report leads with RETRACT and hides the raw conflict pool.
    let shown = format!("{r}");
    assert!(shown.contains("RETRACT"), "{shown}");
    assert!(!shown.contains("CONFLICT  "), "{shown}");
}

#[test]
fn assume_vs_fact_retracts_only_the_assumption() {
    // FACT x a is ground truth; ASSUME NOT x a is the only removable thing.
    let r = vs("FACT x a\nASSUME NOT x a\nCHECK x\n").unwrap();
    assert_eq!(r.status, Status::Conflict);
    assert_eq!(r.retract.len(), 1);
    assert_eq!(r.retract[0].label, "NOT t.x a");
    assert_eq!(r.retract[0].origin.kind, kw::ASSUME);
}

#[test]
fn hard_conflict_is_not_blamed_on_assumptions() {
    // The FACTs themselves contradict; an unrelated ASSUME must NOT appear in
    // a retract set (the hard program is already broken).
    let r = vs("FACT x a\nNOT x a\nASSUME y b\nCHECK x\n").unwrap();
    assert_eq!(r.status, Status::Conflict);
    assert!(r.retract.is_empty(), "{:?}", r.retract);
}

#[test]
fn two_assumptions_directly_contradict() {
    let r = vs("ASSUME x a\nASSUME NOT x a\nCHECK x\n").unwrap();
    assert_eq!(r.status, Status::Conflict);
    assert_eq!(r.retract.len(), 2, "{:?}", r.retract);
}

#[test]
fn assume_retract_is_in_json() {
    let r = vs("FACT x a\nASSUME NOT x a\nCHECK x\n").unwrap();
    let j = r.to_json();
    assert!(j.contains("\"retract\":["), "{j}");
    assert!(j.contains("\"kind\":\"ASSUME\""), "{j}");
    assert!(j.contains("NOT t.x a"), "{j}");
}

// --- near-duplicate atom hints (advisory typo detector) ----------------

#[test]
fn hint_flags_underscore_vs_space_and_is_advisory_only() {
    // The real trap: `is rolled_back` (obj) vs `is_rolled_back` (pred) are
    // DIFFERENT atoms — no contradiction, so the verdict stays CONSISTENT —
    // but the hint warns they were probably meant to be one atom.
    let r = vs(r#"
        FACT auth is rolled_back
        NOT auth is_rolled_back
        CHECK
        "#)
    .unwrap();
    assert_eq!(
        r.status,
        Status::Consistent,
        "hint must not change the verdict"
    );
    assert_eq!(r.exit_code(), 0, "hint must not change the exit code");
    assert_eq!(r.hints.len(), 1, "{:?}", r.hints);
    assert!(r.hints[0].reason.contains('_') || r.hints[0].reason.contains("case"));
}

#[test]
fn hint_flags_case_only_difference() {
    let r = vs("FACT Engine has_fuel\nNOT Engine Has_fuel\nCHECK\n").unwrap();
    assert_eq!(r.hints.len(), 1, "{:?}", r.hints);
}

#[test]
fn hint_flags_single_char_typo_same_subject() {
    // alphabetic, same subject, edit distance 1, len >= 5 → signal B.
    let r = vs("FACT svc deployed\nNOT svc deployd\nCHECK\n").unwrap();
    assert_eq!(r.hints.len(), 1, "{:?}", r.hints);
}

#[test]
fn no_hint_for_short_distinct_atoms() {
    // `x a` vs `x b`: distance 1 but intentionally different — must NOT flag.
    let r = vs("FACT x a\nNOT x b\nCHECK\n").unwrap();
    assert!(r.hints.is_empty(), "{:?}", r.hints);
}

#[test]
fn no_hint_for_distinct_words() {
    let r = vs("FACT p is lead\nNOT p is dev\nNOT p is qa\nCHECK\n").unwrap();
    assert!(r.hints.is_empty(), "{:?}", r.hints);
}

#[test]
fn russian_case_typo_is_flagged() {
    // Signal A is script-agnostic: lowercasing works for Cyrillic too.
    let r = vs("FACT кот спит\nNOT Кот спит\nCHECK\n").unwrap();
    assert_eq!(r.hints.len(), 1, "{:?}", r.hints);
}

#[test]
fn russian_single_char_typo_is_flagged() {
    let r = vs("FACT кот пушистый\nNOT кот пушстый\nCHECK\n").unwrap();
    assert_eq!(r.hints.len(), 1, "{:?}", r.hints);
}

#[test]
fn cjk_one_char_difference_is_not_flagged() {
    // Caseless script: a one-character change is a different word, not a typo,
    // so the edit-distance signal is skipped (only exact fold-equality fires).
    let r = vs("FACT a 是黑\nNOT a 是白\nCHECK\n").unwrap();
    assert!(r.hints.is_empty(), "{:?}", r.hints);
}

#[test]
fn cjk_underscore_vs_space_is_flagged() {
    // Signal A still applies to any script: `a 猫_黑` (pred) vs `a 猫 黑`
    // (pred+obj) fold to the same name.
    let r = vs("FACT a 猫_黑\nNOT a 猫 黑\nCHECK\n").unwrap();
    assert_eq!(r.hints.len(), 1, "{:?}", r.hints);
}

// --- orphan facts (advisory: assertions no premise/rule references) -----

#[test]
fn orphan_fact_is_flagged_but_advisory_only() {
    // `x a` is asserted but never referenced by a premise or rule: inert.
    // The verdict stays CONSISTENT and the exit code stays 0.
    let r = vs("FACT x a\nCHECK\n").unwrap();
    assert_eq!(
        r.status,
        Status::Consistent,
        "orphan must not change verdict"
    );
    assert_eq!(r.exit_code(), 0, "orphan must not change exit code");
    assert_eq!(r.orphans.len(), 1, "{:?}", r.orphans);
    assert_eq!(r.orphans[0].atom, "t.x a");
    assert_eq!(r.orphans[0].origin.kind, kw::FACT);
}

#[test]
fn fact_used_by_a_premise_is_not_orphan() {
    // `x a` feeds an EXCLUSIVE constraint → referenced → not an orphan.
    let r = vs(r"
        FACT x a
        PREMISE p:
            EXCLUSIVE
                x a
                x b
        CHECK
        ")
    .unwrap();
    assert!(r.orphans.is_empty(), "{:?}", r.orphans);
}

#[test]
fn fact_used_by_a_rule_antecedent_is_not_orphan() {
    let r = vs(r"
        FACT x a
        RULE r:
            WHEN x a
            THEN x c
        CHECK
        ")
    .unwrap();
    assert!(r.orphans.is_empty(), "{:?}", r.orphans);
}

#[test]
fn negation_and_assumption_orphans_keep_their_surface_polarity() {
    // A `NOT` orphan and an `ASSUME NOT` orphan render with the polarity the
    // model wrote, so the report points at the exact line it typed.
    let r = vs("NOT x a\nASSUME NOT y b\nCHECK\n").unwrap();
    assert_eq!(r.orphans.len(), 2, "{:?}", r.orphans);
    let text = format!("{r}");
    assert!(text.contains("ORPHAN    NOT t.x a"), "{text}");
    assert!(text.contains("ORPHAN    ASSUME NOT t.y b"), "{text}");
}

#[test]
fn orphan_is_in_json() {
    let r = vs("FACT x a\nCHECK\n").unwrap();
    let j = r.to_json();
    assert!(j.contains("\"orphans\":["), "{j}");
    assert!(j.contains("\"atom\":\"t.x a\""), "{j}");
    assert!(j.contains("\"kind\":\"FACT\""), "{j}");
}

#[test]
fn unused_import_is_advisory_only_in_the_report() {
    // main imports physics but never references it. The advisory shows up but
    // the verdict stays CONSISTENT (exit 0) — it is purely informational.
    let mut r = MemoryResolver::new();
    r.add("physics.vrf", "DOMAIN physics\nFACT Motor over_100\n");
    r.add(
        "main.vrf",
        "DOMAIN main\nIMPORT \"physics.vrf\"\nFACT x a\nCHECK\n",
    );
    let rep = verify("main.vrf", &r).unwrap();
    assert_eq!(rep.status, Status::Consistent);
    assert_eq!(rep.exit_code(), 0);
    assert_eq!(rep.unused_imports.len(), 1);
    assert_eq!(rep.unused_imports[0].domain, "physics");
    let text = format!("{rep}");
    assert!(text.contains("UNUSED IMPORT  physics"), "{text}");
    assert!(
        rep.to_json().contains("\"unused_imports\":[{"),
        "{}",
        rep.to_json()
    );
}

#[test]
fn a_derived_atom_does_not_make_its_consumer_orphan() {
    // `x c` is derived by the rule and then referenced by the premise; the
    // seeding fact `x a` is referenced by the rule. Nothing is orphan.
    let r = vs(r"
        FACT x a
        RULE r:
            WHEN x a
            THEN x c
        PREMISE p:
            WHEN x c
            THEN x d
        CHECK
        ")
    .unwrap();
    assert!(r.orphans.is_empty(), "{:?}", r.orphans);
}

// --- Defeasible rules: RULE … UNLESS (L3) --------------------------------------

#[test]
fn defeasible_established_exception_suppresses_the_default() {
    // The antecedent holds, but the exception is *established* TRUE → the default is
    // retracted, so the rule derives nothing and `NOT … can_fly` is consistent.
    let r = vs(r"
        RULE fly:
            WHEN pengu is bird
            THEN pengu can_fly
            UNLESS pengu is penguin
        FACT pengu is bird
        FACT pengu is penguin
        NOT pengu can_fly
        CHECK
        ")
    .unwrap();
    assert_eq!(r.status, Status::Consistent);
    assert!(r.conflicts.is_empty());
    // The default was defeated: nothing derived can_fly.
    assert!(!r.derived.iter().any(|d| d.atom.contains("can_fly")));
    // The defeat is surfaced as an informational note naming the exception.
    assert_eq!(r.defeated.len(), 1);
    assert!(r.defeated[0].consequent.contains("can_fly"));
    assert_eq!(
        r.defeated[0].blocked_by,
        vec![String::from("t.pengu is penguin")]
    );
}

#[test]
fn defeasible_backward_pass_agrees_when_fully_pinned() {
    // Under BIDIRECTIONAL the exception enters the rule's clause (¬bird ∨ penguin ∨
    // can_fly). With every atom pinned by a fact the clause is satisfied and there is
    // exactly one model → CONSISTENT, matching the forward pass (no false conflict).
    let r = vs(r"
        RULE fly:
            WHEN pengu is bird
            THEN pengu can_fly
            UNLESS pengu is penguin
        FACT pengu is bird
        FACT pengu is penguin
        NOT pengu can_fly
        CHECK BIDIRECTIONAL
        ")
    .unwrap();
    assert_eq!(r.status, Status::Consistent);
    assert!(r.conflicts.is_empty());
}

#[test]
fn a_default_that_fires_normally_records_no_defeat() {
    // When no exception is established, the rule fires and there is no DEFEATED note.
    let r = vs(r"
        RULE fly:
            WHEN pengu is bird
            THEN pengu can_fly
            UNLESS pengu is penguin
        FACT pengu is bird
        CHECK
        ")
    .unwrap();
    assert!(r.defeated.is_empty());
}

#[test]
fn defeasible_unknown_exception_lets_the_default_fire() {
    // The exception is never established (stays UNKNOWN) → assume-normal: the default
    // still fires and derives the consequent.
    let r = vs(r"
        RULE fly:
            WHEN pengu is bird
            THEN pengu can_fly
            UNLESS pengu is penguin
        FACT pengu is bird
        CHECK
        ")
    .unwrap();
    assert_eq!(r.status, Status::Consistent);
    assert!(
        r.derived
            .iter()
            .any(|d| d.atom.contains("can_fly") && d.value == Value::True)
    );
}

#[test]
fn defeasible_false_exception_lets_the_default_fire() {
    // An exception forced FALSE does not defeat the rule (only an established TRUE
    // does) → the default fires, contradicting `NOT … can_fly`: CONFLICT.
    let r = vs(r"
        RULE fly:
            WHEN pengu is bird
            THEN pengu can_fly
            UNLESS pengu is penguin
        FACT pengu is bird
        NOT pengu is penguin
        NOT pengu can_fly
        CHECK
        ")
    .unwrap();
    assert_eq!(r.status, Status::Conflict);
}

#[test]
fn defeasible_default_without_exception_fires_and_can_conflict() {
    // No exception is established, so the default fires and derives can_fly; a
    // `NOT … can_fly` then contradicts the derived value → CONFLICT (non-monotonic:
    // adding `FACT pengu is penguin` would make this consistent).
    let r = vs(r"
        RULE fly:
            WHEN pengu is bird
            THEN pengu can_fly
            UNLESS pengu is penguin
        FACT pengu is bird
        NOT pengu can_fly
        CHECK
        ")
    .unwrap();
    assert_eq!(r.status, Status::Conflict);
}

#[test]
fn defeasible_multiple_unless_blocks_if_any_fires() {
    // Two exceptions; the rule is suppressed when *any* is established TRUE.
    let r = vs(r"
        RULE fly:
            WHEN robin is bird
            THEN robin can_fly
            UNLESS robin is penguin
            UNLESS robin is injured
        FACT robin is bird
        FACT robin is injured
        NOT robin can_fly
        CHECK
        ")
    .unwrap();
    assert_eq!(r.status, Status::Consistent);
    assert!(!r.derived.iter().any(|d| d.atom.contains("can_fly")));
}

#[test]
fn defeasible_per_element_over_a_set_defeats_only_the_exceptional_one() {
    // `FOR EACH` instantiates the defeasible rule per element: tweety (no exception)
    // flies, pengu (a penguin) is defeated — one rule, two outcomes.
    let r = vs(r"
        SET creatures
            tweety
            pengu
        RULE fly FOR EACH x IN creatures:
            WHEN x is bird
            THEN x can_fly
            UNLESS x is penguin
        FACT tweety is bird
        FACT pengu is bird
        FACT pengu is penguin
        NOT pengu can_fly
        CHECK
        ")
    .unwrap();
    assert_eq!(r.status, Status::Consistent);
    assert!(
        r.derived
            .iter()
            .any(|d| d.atom.contains("tweety") && d.atom.contains("can_fly"))
    );
    assert!(!r.derived.iter().any(|d| d.atom.contains("pengu")));
}

#[test]
fn defeasible_exception_atom_is_not_flagged_as_orphan() {
    // An atom mentioned only in an UNLESS is referenced by the rule, so the orphan
    // lint stays silent.
    let r = vs(r"
        RULE fly:
            WHEN pengu is bird
            THEN pengu can_fly
            UNLESS pengu is penguin
        FACT pengu is bird
        FACT pengu is penguin
        CHECK
        ")
    .unwrap();
    assert!(r.orphans.is_empty(), "{:?}", r.orphans);
}

#[test]
fn premise_with_unless_is_a_compile_error() {
    // UNLESS is RULE-only; a PREMISE carrying one is rejected at compile time.
    let err = vs(r"
        PREMISE p:
            WHEN a is x
            THEN b is y
            UNLESS c is z
        CHECK
        ")
    .unwrap_err();
    let msg = format!("{err}");
    assert!(msg.contains("UNLESS"), "{msg}");
    assert!(msg.contains("RULE"), "{msg}");
}

// --- Cross-file relation feeding (template + facts-only entry file) ------------

/// The two-file template pattern: the imported template owns the `dep`
/// relation (closed transitively) and a FORBIDS premise over it; the entry
/// file supplies the edges by qualifying facts into the template's domain.
fn verify_fed(entry: &str) -> Report {
    let mut r = MemoryResolver::new();
    r.add(
        "tmpl.vrf",
        r"DOMAIN tmpl
FACT a dep b
CLOSE dep TRANSITIVE
PREMISE no_hot_chain FOR EACH x dep y:
    FORBIDS
        x hot on
        y hot on
",
    );
    r.add("entry.vrf", entry);
    verify("entry.vrf", &r).unwrap()
}

#[test]
fn a_cross_file_fed_edge_is_consumed_not_orphan() {
    // The qualified edge is read as data by the template's FOR EACH — the
    // orphan lint must stay silent about it.
    let rep = verify_fed(
        "DOMAIN e\nIMPORT \"tmpl.vrf\"\nFACT tmpl.b dep c\nNOT tmpl.a hot on\nNOT tmpl.b hot on\nNOT tmpl.c hot on\nCHECK\n",
    );
    assert_eq!(rep.status, Status::Consistent);
    assert!(rep.orphans.is_empty(), "{:?}", rep.orphans);
}

#[test]
fn a_bare_entry_edge_stays_orphan() {
    // Without the domain prefix the edge lands in the ENTRY domain, feeds
    // nothing, and is correctly flagged as an idle fact.
    let rep = verify_fed(
        "DOMAIN e\nIMPORT \"tmpl.vrf\"\nFACT b dep c\nNOT tmpl.a hot on\nNOT tmpl.b hot on\nCHECK\n",
    );
    assert_eq!(rep.orphans.len(), 1, "{:?}", rep.orphans);
    assert_eq!(rep.orphans[0].atom, "e.b dep c");
}

#[test]
fn fed_transitive_closure_reaches_the_verdict() {
    // a->b (template) + b->c (entry) close to a->c, so `a hot` and `c hot`
    // together violate the grounded FORBIDS — a conflict only reachable
    // through the fed, closed pair.
    let rep = verify_fed(
        "DOMAIN e\nIMPORT \"tmpl.vrf\"\nFACT tmpl.b dep c\nFACT tmpl.a hot on\nFACT tmpl.c hot on\nNOT tmpl.b hot on\nCHECK\n",
    );
    assert_eq!(rep.status, Status::Conflict);
    assert!(
        rep.conflicts
            .iter()
            .any(|c| c.origin.premise.as_deref() == Some("no_hot_chain")),
        "{:?}",
        rep.conflicts
    );
}

// --- PROVE (entailment / the ⊨ goal, F1) -------------------------------------

#[test]
fn prove_entailed_goal_is_proved() {
    // A fact plus a rule force the goal: theory ∧ ¬goal is unsatisfiable.
    let r = vs(
        "FACT s is human\nRULE mortal:\n    WHEN s is human\n    THEN s is mortal\nPROVE s is mortal\nCHECK s\n",
    )
    .unwrap();
    assert_eq!(r.status, Status::Consistent); // advisory: the goal never raises it
    assert_eq!(r.goals.len(), 1);
    assert_eq!(r.goals[0].label, "t.s is mortal");
    assert_eq!(r.goals[0].outcome, ProveOutcome::Proved);
    assert_eq!(r.goals[0].origin.kind, kw::PROVE);
}

#[test]
fn prove_contradicted_goal_is_refuted() {
    // The theory establishes the goal's negation: theory ∧ goal is unsatisfiable.
    let r = vs("NOT s is immortal\nPROVE s is immortal\nCHECK s\n").unwrap();
    assert_eq!(r.goals[0].outcome, ProveOutcome::Refuted);
}

#[test]
fn prove_unpinned_goal_is_open() {
    // Nothing determines the goal either way — the honest three-valued answer.
    let r = vs("FACT x a\nPROVE x b\nCHECK x\n").unwrap();
    assert_eq!(r.status, Status::Consistent);
    assert_eq!(r.goals[0].outcome, ProveOutcome::Open);
}

#[test]
fn prove_on_inconsistent_theory_is_vacuous() {
    // Both refutation calls come back unsatisfiable: the theory itself is broken,
    // so the goal line says VACUOUS instead of a misleading PROVED.
    let r = vs("FACT x a\nNOT x a\nPROVE x b\n").unwrap();
    assert_eq!(r.status, Status::Conflict); // the conflict is the theory's, not the goal's
    assert_eq!(r.goals[0].outcome, ProveOutcome::Vacuous);
}

#[test]
fn prove_not_carries_polarity_in_label_and_check() {
    // `PROVE NOT g` asks whether ¬g follows; here it does (g is asserted FALSE).
    let r = vs("NOT door open\nPROVE NOT door open\nCHECK door\n").unwrap();
    assert_eq!(r.goals[0].label, "NOT t.door open");
    assert_eq!(r.goals[0].outcome, ProveOutcome::Proved);
}

#[test]
fn prove_never_commits_the_goal() {
    // The goal atom stays UNKNOWN in the model: no DERIVED, no WARNING from it, and
    // a premise blocked by that atom still warns exactly as without the PROVE.
    let with =
        vs("FACT x a\nPREMISE p:\n    WHEN x a\n    THEN x b\nPROVE x b\nCHECK x\n").unwrap();
    let without = vs("FACT x a\nPREMISE p:\n    WHEN x a\n    THEN x b\nCHECK x\n").unwrap();
    assert_eq!(with.status, without.status);
    assert_eq!(with.warnings.len(), without.warnings.len());
    assert_eq!(with.goals.len(), 1);
    // Refutational reading: theory ∧ ¬(x b) violates the premise ⇒ PROVED — the
    // constraint *forces* x b even though the forward pass could not confirm it.
    assert_eq!(with.goals[0].outcome, ProveOutcome::Proved);
}

// --- HENCE … FROM (checked derivation / the proof kernel, F2) -----------------

#[test]
fn hence_valid_step_holds() {
    // Modus ponens as a witness: the cited premise + cited fact entail the
    // conclusion, so the step holds. Advisory: the verdict is what it would be
    // without the HENCE line.
    let r = vs(
        "FACT socrates is human\nRULE all_mortal:\n    WHEN socrates is human\n    THEN socrates is mortal\nHENCE socrates is mortal FROM all_mortal, socrates is human\nCHECK socrates\n",
    )
    .unwrap();
    assert_eq!(r.derivation.len(), 1);
    assert!(r.derivation[0].holds);
    assert_eq!(r.derivation[0].conclusion, "t.socrates is mortal");
    assert_eq!(
        r.derivation[0].from,
        vec!["all_mortal".to_string(), "t.socrates is human".to_string()]
    );
    assert_eq!(r.derivation[0].origin.kind, kw::HENCE);
}

#[test]
fn hence_gap_is_named_per_step() {
    // The cited premise talks about `x b`, not `x a` — the conclusion does not
    // follow from what the step cites, even though the program is consistent.
    let r =
        vs("FACT x a\nPREMISE p:\n    WHEN x b\n    THEN x c\nHENCE x c FROM p, x a\nCHECK x\n")
            .unwrap();
    assert!(!r.derivation[0].holds);
    assert_eq!(r.status, Status::Warning); // p is blocked by UNKNOWN x b — unrelated to HENCE
}

#[test]
fn hence_may_cite_an_earlier_hence_conclusion() {
    // A linear chain: step 2 rests on step 1's conclusion (never on the whole
    // program). Both steps hold; each was checked separately.
    let r = vs(
        "FACT socrates is human\nRULE all_mortal:\n    WHEN socrates is human\n    THEN socrates is mortal\nRULE mortal_dies:\n    WHEN socrates is mortal\n    THEN socrates will_die\nHENCE socrates is mortal FROM all_mortal, socrates is human\nHENCE socrates will_die FROM mortal_dies, socrates is mortal\nCHECK socrates\n",
    )
    .unwrap();
    assert_eq!(r.derivation.len(), 2);
    assert!(r.derivation[0].holds && r.derivation[1].holds);
    assert_eq!(r.derivation[1].from[1], "t.socrates is mortal");
}

#[test]
fn hence_may_cite_a_construct_written_later() {
    // Resolution is deferred until the whole program is read, so citing a premise
    // defined further down the file works.
    let r = vs("FACT x a\nHENCE x b FROM ab, x a\nRULE ab:\n    WHEN x a\n    THEN x b\nCHECK x\n")
        .unwrap();
    assert!(r.derivation[0].holds);
}

#[test]
fn hence_not_conclusion_and_negated_ref() {
    // Polarity flows through both slots: a NOT conclusion checked against a
    // written NOT fact.
    let r = vs("NOT door open\nHENCE NOT door open FROM NOT door open\nCHECK door\n").unwrap();
    assert!(r.derivation[0].holds);
    assert_eq!(r.derivation[0].conclusion, "NOT t.door open");
    assert_eq!(r.derivation[0].from, vec!["NOT t.door open".to_string()]);
}

#[test]
fn hence_unknown_reference_is_a_compile_error_with_suggestion() {
    // Citing a name that is neither a construct, a written fact, nor an earlier
    // conclusion fails compilation — the engine refuses to guess (Law 5).
    let err = vs(
        "FACT x a\nRULE all_mortal:\n    WHEN x a\n    THEN x b\nHENCE x b FROM all_mortel\nCHECK x\n",
    )
    .unwrap_err();
    match err {
        CompileError::UnknownHenceRef {
            line,
            reference,
            suggestion,
            ..
        } => {
            assert_eq!(line, 6);
            assert_eq!(reference, "all_mortel");
            assert!(suggestion.contains("all_mortal"), "{suggestion}");
        }
        other => panic!("expected UnknownHenceRef, got {other}"),
    }
}

#[test]
fn hence_cited_fact_is_not_an_orphan() {
    // A fact used only as proof data would otherwise be flagged ORPHAN; citing it
    // in a HENCE counts as consumption.
    let r = vs("FACT x a\nHENCE x a FROM x a\nCHECK x\n").unwrap();
    assert!(r.orphans.is_empty(), "{:?}", r.orphans);
    assert!(r.derivation[0].holds);
}

#[test]
fn hence_broken_earlier_step_stays_local() {
    // Step 1 is a gap; step 2 cites its conclusion and is checked *locally* (the
    // chain is a witness, not a proof search): step 2 holds on its own line while
    // step 1's line names the gap — the reader repairs the first broken step.
    let r = vs(
        "FACT x a\nHENCE x b FROM x a\nRULE bc:\n    WHEN x b\n    THEN x c\nHENCE x c FROM bc, x b\nCHECK x\n",
    )
    .unwrap();
    assert!(!r.derivation[0].holds);
    assert!(r.derivation[1].holds);
}

// --- FOR EACH <x> MENTIONED (the universal schema, F3) -------------------------

#[test]
fn mentioned_schema_reaches_an_unenlisted_individual() {
    // "All men are mortal" reaches Socrates although no SET lists him — writing a
    // fact about him is what makes him an individual of the domain.
    let r = vs(
        "FACT socrates is human\nRULE mortal FOR EACH x MENTIONED:\n    WHEN x is human\n    THEN x is mortal\nCHECK socrates\n",
    )
    .unwrap();
    assert_eq!(r.status, Status::Consistent);
    assert!(
        r.derived
            .iter()
            .any(|d| d.atom == "t.socrates is mortal" && d.value == Value::True),
        "{:?}",
        r.derived
    );
}

#[test]
fn mentioned_includes_not_and_assume_subjects() {
    // NOT and ASSUME introduce individuals too. Each blocked instance surfaces as
    // its own WARNING: `known` warns for a (FACT) and c (ASSUME) — TRUE antecedent,
    // UNKNOWN consequent — while `voided` warns for b (NOT). Three warnings ⇒ all
    // three subjects were instantiated.
    let r = vs(
        "FACT a is thing\nNOT b is thing\nASSUME c is thing\nPREMISE known FOR EACH x MENTIONED:\n    WHEN x is thing\n    THEN x is known\nPREMISE voided FOR EACH y MENTIONED:\n    WHEN NOT y is thing\n    THEN y is voided\nCHECK\n",
    )
    .unwrap();
    assert_eq!(r.status, Status::Warning);
    assert_eq!(r.warnings.len(), 3, "{:?}", r.warnings);
}

#[test]
fn mentioned_schema_grounds_once_per_subject() {
    // Two individuals, both human: the schema derives mortality for each.
    let r = vs(
        "FACT socrates is human\nFACT plato is human\nRULE mortal FOR EACH x MENTIONED:\n    WHEN x is human\n    THEN x is mortal\nCHECK\n",
    )
    .unwrap();
    assert_eq!(r.derived.len(), 2, "{:?}", r.derived);
}

#[test]
fn mentioned_excludes_var_ports() {
    // A bare proposition (a VAR port) is not an individual: only `x` is mentioned,
    // so exactly one instance grounds and exactly one derivation happens.
    let r = vs(
        "VAR db_ready DEFAULT true\nFACT x is human\nRULE mortal FOR EACH s MENTIONED:\n    WHEN s is human\n    THEN s is mortal\nCHECK\n",
    )
    .unwrap();
    assert_eq!(r.derived.len(), 1, "{:?}", r.derived);
}

#[test]
fn mentioned_empty_domain_grounds_to_nothing() {
    // No ground assertion mentions anyone — the schema grounds to zero instances,
    // like a FOR EACH over an empty relation. VARs alone name no individual.
    let r = vs(
        "VAR flag DEFAULT true\nRULE mortal FOR EACH x MENTIONED:\n    WHEN x is human\n    THEN x is mortal\nCHECK\n",
    )
    .unwrap();
    assert_eq!(r.status, Status::Consistent);
    assert!(r.derived.is_empty() && r.warnings.is_empty());
}

#[test]
fn mentioned_is_same_domain_only() {
    // The schema lives in the template's domain. The entry file's *bare* fact
    // belongs to the entry domain and must NOT grow the template's schema; the
    // *qualified* fact deliberately feeds it. Exactly one derivation: tmpl.sock.
    let mut res = MemoryResolver::new();
    res.add(
        "tmpl.vrf",
        "DOMAIN tmpl\nRULE mortal FOR EACH x MENTIONED:\n    WHEN x is human\n    THEN x is mortal\n",
    )
    .add(
        "entry.vrf",
        "DOMAIN entry\nIMPORT \"tmpl.vrf\"\nFACT tmpl.sock is human\nFACT local is human\nCHECK\n",
    );
    let r = verify("entry.vrf", &res).unwrap();
    assert_eq!(
        r.derived
            .iter()
            .map(|d| d.atom.as_str())
            .collect::<Vec<_>>(),
        vec!["tmpl.sock is mortal"],
        "{:?}",
        r.derived
    );
}

#[test]
fn mentioned_schema_redefinition_with_different_quant_is_an_error() {
    // The quantifier participates in the redefinition hash: the same name with a
    // MENTIONED quantifier vs a plain body is a real redefinition.
    let err = vs(
        "FACT a is thing\nRULE r FOR EACH x MENTIONED:\n    WHEN x is thing\n    THEN x is fine\nRULE r:\n    WHEN a is thing\n    THEN a is fine\n",
    )
    .unwrap_err();
    assert!(matches!(err, CompileError::PremiseRedefinition { .. }));
}

// --- TOTAL <relation> ON <set> (Skolem witness tables, F4) ---------------------

#[test]
fn total_fully_served_is_silent_and_consumes_pairs() {
    // Every task has an assignee pair — the ∀∃ claim is discharged by data. No
    // warning, and the witness pairs are not ORPHANs (they are read by the check).
    let r = vs(
        "SET tasks\n    deploy\n    backup\nFACT deploy assigned ana\nFACT backup assigned bob\nTOTAL assigned ON tasks\nCHECK\n",
    )
    .unwrap();
    assert_eq!(r.status, Status::Consistent);
    assert!(r.warnings.is_empty());
    assert!(r.orphans.is_empty(), "{:?}", r.orphans);
}

#[test]
fn total_missing_witness_is_a_warning_naming_the_element() {
    // `backup` has no assignee: WARNING, the unserved element named, with a
    // data-shaped fix (the LLM supplies the witness, the engine re-checks).
    let r = vs(
        "SET tasks\n    deploy\n    backup\nFACT deploy assigned ana\nTOTAL assigned ON tasks\nCHECK\n",
    )
    .unwrap();
    assert_eq!(r.status, Status::Warning);
    assert_eq!(r.warnings.len(), 1);
    assert_eq!(r.warnings[0].origin.kind, kw::TOTAL);
    assert_eq!(
        r.warnings[0].blocked_by,
        vec!["backup (no assigned witness)"]
    );
    assert!(
        r.warnings[0]
            .hint
            .as_deref()
            .unwrap()
            .contains("FACT backup assigned"),
        "{:?}",
        r.warnings[0].hint
    );
}

#[test]
fn total_over_an_empty_relation_names_every_element() {
    // No pair declared at all (or a typo'd relation): everything is unserved.
    let r = vs("SET tasks\n    deploy\n    backup\nTOTAL assigned ON tasks\nCHECK\n").unwrap();
    assert_eq!(r.status, Status::Warning);
    assert_eq!(r.warnings[0].blocked_by.len(), 2);
}

#[test]
fn total_counts_closed_pairs() {
    // CLOSE runs before the totality scan, so closure-produced pairs serve too:
    // `a dep b` + `b dep c` close to `a dep c` — every element of `starts` then
    // has a `dep` pair as subject except `c` (a leaf), which is named.
    let r = vs(
        "SET starts\n    a\n    b\n    c\nFACT a dep b\nFACT b dep c\nCLOSE dep TRANSITIVE\nTOTAL dep ON starts\nCHECK\n",
    )
    .unwrap();
    assert_eq!(r.status, Status::Warning);
    assert_eq!(r.warnings[0].blocked_by, vec!["c (no dep witness)"]);
}

#[test]
fn total_unknown_set_is_a_compile_error_with_suggestion() {
    let err = vs("SET tasks\n    deploy\nFACT deploy assigned ana\nTOTAL assigned ON taks\n")
        .unwrap_err();
    match err {
        CompileError::UnknownTotalSet {
            line,
            set,
            suggestion,
            ..
        } => {
            assert_eq!(line, 5);
            assert_eq!(set, "taks");
            assert!(suggestion.contains("tasks"), "{suggestion}");
        }
        other => panic!("expected UnknownTotalSet, got {other}"),
    }
}

#[test]
fn total_is_fed_by_a_qualified_cross_file_pair() {
    // The witness table may live in the importing file: a qualified pair feeds
    // the template's relation before the template's TOTAL is evaluated.
    let mut res = MemoryResolver::new();
    res.add(
        "tmpl.vrf",
        "DOMAIN tmpl\nSET tasks\n    deploy\n    backup\nFACT deploy assigned ana\nTOTAL assigned ON tasks\n",
    )
    .add(
        "entry.vrf",
        "DOMAIN entry\nIMPORT \"tmpl.vrf\"\nFACT tmpl.backup assigned bob\nCHECK\n",
    );
    let r = verify("entry.vrf", &res).unwrap();
    assert_eq!(r.status, Status::Consistent, "{:?}", r.warnings);
    assert!(r.warnings.is_empty());
}

// --- TRY <H> FOR <G> (targeted abduction, F6) ----------------------------------

#[test]
fn try_for_a_hypothesis_that_explains_the_goal() {
    // The textbook abduction question, completed: H is consistent with the theory
    // AND theory + H entails G — the missing premise genuinely explains the goal.
    let r = vs(
        "RULE gate:\n    WHEN deploys is_ready\n    THEN deploys unblocked\nTRY deploys is_ready FOR deploys unblocked\nCHECK\n",
    )
    .unwrap();
    assert_eq!(r.tried.len(), 1);
    assert_eq!(r.tried[0].outcome, TryOutcome::Explains);
    assert_eq!(r.tried[0].goal.as_deref(), Some("t.deploys unblocked"));
}

#[test]
fn try_for_a_hypothesis_that_does_not_explain() {
    // H is compatible, but the goal still does not follow — no explanation.
    let r = vs(
        "RULE gate:\n    WHEN deploys is_ready\n    THEN deploys unblocked\nTRY backup done FOR deploys unblocked\nCHECK\n",
    )
    .unwrap();
    assert_eq!(r.tried[0].outcome, TryOutcome::NotExplaining);
}

#[test]
fn try_for_a_contradicting_hypothesis_conflicts() {
    // Check (a) comes first: an H that clashes with the theory can explain
    // nothing, whatever the goal.
    let r = vs("FACT deploys is_ready\nTRY NOT deploys is_ready FOR deploys unblocked\nCHECK\n")
        .unwrap();
    assert_eq!(r.tried[0].outcome, TryOutcome::Conflicts);
}

#[test]
fn plain_try_and_targeted_try_coexist() {
    // The goal-less line keeps the exact L5 outcomes; the targeted one answers the
    // FOR question. One program, both voices.
    let r = vs(
        "RULE gate:\n    WHEN deploys is_ready\n    THEN deploys unblocked\nCHECK BIDIRECTIONAL\nTRY deploys is_ready\nTRY deploys is_ready FOR deploys unblocked\n",
    )
    .unwrap();
    assert_eq!(r.tried.len(), 2);
    assert_eq!(r.tried[0].outcome, TryOutcome::Closes);
    assert_eq!(r.tried[0].goal, None);
    assert_eq!(r.tried[1].outcome, TryOutcome::Explains);
}

#[test]
fn try_for_with_negated_goal() {
    // Polarity flows through the goal slot: H entails NOT G here.
    let r = vs(
        "RULE off:\n    WHEN power cut\n    THEN NOT lamp on\nTRY power cut FOR NOT lamp on\nCHECK\n",
    )
    .unwrap();
    assert_eq!(r.tried[0].outcome, TryOutcome::Explains);
    assert_eq!(r.tried[0].goal.as_deref(), Some("NOT t.lamp on"));
}

// --- PREFERS <winner> OVER <loser> (default priorities, F7) --------------------

#[test]
fn prefers_penguin_beats_bird() {
    // Specificity: both defaults are applicable, the declared winner stands, the
    // loser is suppressed and visible as DEFEATED — no conflict.
    let r = vs(
        "RULE bird_flies:\n    WHEN pengu is bird\n    THEN pengu can_fly\nRULE penguin_grounded:\n    WHEN pengu is penguin\n    THEN NOT pengu can_fly\nPREFERS penguin_grounded OVER bird_flies\nFACT pengu is bird\nFACT pengu is penguin\nCHECK\n",
    )
    .unwrap();
    assert_eq!(r.status, Status::Consistent, "{:?}", r.conflicts);
    assert!(
        r.derived
            .iter()
            .any(|d| d.atom == "t.pengu can_fly" && d.value == Value::False),
        "{:?}",
        r.derived
    );
    assert_eq!(r.defeated.len(), 1);
    assert_eq!(r.defeated[0].origin.premise.as_deref(), Some("bird_flies"));
}

#[test]
fn prefers_works_whatever_the_source_order() {
    // The loser is written FIRST: without the winners-first re-ordering it would
    // fire in the same sweep before the winner. The verdict must be identical to
    // the winner-first spelling.
    let r = vs(
        "PREFERS penguin_grounded OVER bird_flies\nRULE penguin_grounded:\n    WHEN pengu is penguin\n    THEN NOT pengu can_fly\nRULE bird_flies:\n    WHEN pengu is bird\n    THEN pengu can_fly\nFACT pengu is bird\nFACT pengu is penguin\nCHECK\n",
    )
    .unwrap();
    assert_eq!(r.status, Status::Consistent, "{:?}", r.conflicts);
    assert_eq!(r.defeated.len(), 1);
}

#[test]
fn prefers_loser_still_fires_when_winner_is_inapplicable() {
    // Not a penguin: the winner never fires, so the default stands untouched.
    let r = vs(
        "RULE bird_flies:\n    WHEN tweety is bird\n    THEN tweety can_fly\nRULE penguin_grounded:\n    WHEN tweety is penguin\n    THEN NOT tweety can_fly\nPREFERS penguin_grounded OVER bird_flies\nFACT tweety is bird\nCHECK\n",
    )
    .unwrap();
    assert_eq!(r.status, Status::Consistent);
    assert!(
        r.derived
            .iter()
            .any(|d| d.atom == "t.tweety can_fly" && d.value == Value::True)
    );
    assert!(r.defeated.is_empty());
}

#[test]
fn prefers_chain_ranks_transitively() {
    // a beats b, b beats c: with all three applicable only `a`'s consequent
    // lands; b is defeated by a, and c by b's... b never fired, so c's exception
    // (b's consequent) is not established — c fires too. Declared, not derived:
    // to silence c under a, the author writes PREFERS a OVER c as well (attack
    // edges are written, never computed — the Dung seed).
    let r = vs(
        "RULE a:\n    WHEN x is thing\n    THEN x mode alpha\nRULE b:\n    WHEN x is thing\n    THEN x mode beta\nRULE c:\n    WHEN x is thing\n    THEN x mode gamma\nPREFERS a OVER b\nPREFERS b OVER c\nFACT x is thing\nCHECK\n",
    )
    .unwrap();
    assert_eq!(r.status, Status::Consistent, "{:?}", r.conflicts);
    let modes: Vec<&str> = r.derived.iter().map(|d| d.atom.as_str()).collect();
    assert!(modes.contains(&"t.x mode alpha"), "{modes:?}");
    assert!(!modes.contains(&"t.x mode beta"), "{modes:?}");
    assert!(modes.contains(&"t.x mode gamma"), "{modes:?}");
    assert_eq!(r.defeated.len(), 1);
}

#[test]
fn prefers_cycle_is_a_compile_error() {
    let err = vs(
        "RULE a:\n    WHEN x p\n    THEN x q\nRULE b:\n    WHEN x p\n    THEN NOT x q\nPREFERS a OVER b\nPREFERS b OVER a\nFACT x p\n",
    )
    .unwrap_err();
    assert!(matches!(err, CompileError::PreferenceCycle { .. }), "{err}");
}

#[test]
fn prefers_unknown_or_premise_name_is_an_error() {
    // A PREMISE is not a RULE (it checks, it does not derive) — priorities only
    // rank defeasible defaults.
    let err = vs(
        "RULE a:\n    WHEN x p\n    THEN x q\nPREMISE guard:\n    WHEN x p\n    THEN x q\nPREFERS a OVER guard\nFACT x p\n",
    )
    .unwrap_err();
    match err {
        CompileError::UnknownRuleName { name, .. } => assert_eq!(name, "guard"),
        other => panic!("expected UnknownRuleName, got {other}"),
    }
    // And a typo'd rule name gets a suggestion.
    let err = vs("RULE alpha:\n    WHEN x p\n    THEN x q\nRULE beta:\n    WHEN x p\n    THEN NOT x q\nPREFERS alpa OVER beta\n")
        .unwrap_err();
    match err {
        CompileError::UnknownRuleName {
            name, suggestion, ..
        } => {
            assert_eq!(name, "alpa");
            assert!(suggestion.contains("alpha"), "{suggestion}");
        }
        other => panic!("expected UnknownRuleName, got {other}"),
    }
}

#[test]
fn prefers_with_quantified_winner_covers_every_instance() {
    // The winner is a FOR EACH rule: every instance's consequent joins the
    // loser's exceptions, so whichever instance fires suppresses the default.
    let r = vs(
        "SET birds\n    pengu\nRULE grounded FOR EACH b IN birds:\n    WHEN b is penguin\n    THEN NOT b can_fly\nRULE bird_flies:\n    WHEN pengu is bird\n    THEN pengu can_fly\nPREFERS grounded OVER bird_flies\nFACT pengu is bird\nFACT pengu is penguin\nCHECK\n",
    )
    .unwrap();
    assert_eq!(r.status, Status::Consistent, "{:?}", r.conflicts);
    assert_eq!(r.defeated.len(), 1);
}

#[test]
fn prefers_backward_pass_stays_consistent() {
    // BIDIRECTIONAL exercises the CNF path: the loser's clause carries the
    // winner's consequent as an escape literal, so the SAT view agrees with the
    // forward pass — no phantom joint unsatisfiability.
    let r = vs(
        "RULE bird_flies:\n    WHEN pengu is bird\n    THEN pengu can_fly\nRULE penguin_grounded:\n    WHEN pengu is penguin\n    THEN NOT pengu can_fly\nPREFERS penguin_grounded OVER bird_flies\nFACT pengu is bird\nFACT pengu is penguin\nCHECK BIDIRECTIONAL\n",
    )
    .unwrap();
    assert_ne!(r.status, Status::Conflict, "{:?}", r.conflicts);
}

// --- the proof kernel × IMPORT: qualified references work across files ---------

#[test]
fn hence_and_prove_reach_imported_atoms_by_qualified_name() {
    // The entry file proves against, and derives from, the template's atoms via
    // the ordinary `domain.` qualification — the proof-kernel layer needs no new
    // import machinery. The HENCE cites a qualified fact of ANOTHER domain (facts
    // match by atom identity, not by source), and PROVE asks about a derived
    // template atom.
    let mut res = MemoryResolver::new();
    res.add(
        "tmpl.vrf",
        "DOMAIN tmpl\nRULE mortal FOR EACH x MENTIONED:\n    WHEN x is human\n    THEN x is mortal\n",
    )
    .add(
        "entry.vrf",
        "DOMAIN entry\nIMPORT \"tmpl.vrf\"\nFACT tmpl.sock is human\nPROVE tmpl.sock is mortal\nHENCE tmpl.sock is human FROM tmpl.sock is human\nCHECK\n",
    );
    let r = verify("entry.vrf", &res).unwrap();
    assert_eq!(r.goals[0].outcome, ProveOutcome::Proved, "{:?}", r.goals);
    assert!(r.derivation[0].holds, "{:?}", r.derivation);
    assert_eq!(r.derivation[0].conclusion, "tmpl.sock is human");
}
