use std::collections::BTreeSet;

use pickaxe_rs::formula;
use pickaxe_rs::prelude::*;

mod common;

use common::*;

// --- Test 1: Argument Construction ---

#[test]
fn test_01_argument_construction() {
    let pipeline = AspicPipeline::classical(running_example(), Box::new(EqualOrdering));
    let result = pipeline.evaluate(Semantics::Grounded).unwrap();
    let store = &result.store;
    let args = find_running_example_args(store);

    // A1: premise p — strict, firm, 0 defeasible rules
    let a1 = store.get(args.a1).unwrap();
    assert!(a1.top_rule().is_none(), "A1: no top rule (premise)");
    assert!(a1.is_strict(store), "A1: strict");
    assert!(a1.is_firm(store), "A1: firm (axiom)");
    assert_eq!(
        a1.defeasible_rules(store).len(),
        0,
        "A1: 0 defeasible rules"
    );

    // B1: premise s — strict, not firm (ordinary), 0 defeasible rules
    let b1 = store.get(args.b1).unwrap();
    assert!(b1.top_rule().is_none(), "B1: no top rule");
    assert!(b1.is_strict(store), "B1: strict");
    assert!(!b1.is_firm(store), "B1: not firm (ordinary premise)");
    assert_eq!(
        b1.defeasible_rules(store).len(),
        0,
        "B1: 0 defeasible rules"
    );

    // C1: premise u — strict, not firm, 0 defeasible rules
    let c1 = store.get(args.c1).unwrap();
    assert!(c1.is_strict(store), "C1: strict");
    assert!(!c1.is_firm(store), "C1: not firm");
    assert_eq!(
        c1.defeasible_rules(store).len(),
        0,
        "C1: 0 defeasible rules"
    );

    // D3: premise x — strict, not firm, 0 defeasible rules
    let d3 = store.get(args.d3_prem).unwrap();
    assert!(d3.is_strict(store), "D3: strict");
    assert!(!d3.is_firm(store), "D3: not firm");
    assert_eq!(
        d3.defeasible_rules(store).len(),
        0,
        "D3: 0 defeasible rules"
    );

    // A2: d1 ⇒ q — defeasible top rule, not strict, firm, 1 def rule
    let a2 = store.get(args.a2).unwrap();
    assert!(
        a2.top_rule().unwrap().is_defeasible(),
        "A2: top rule d1 is defeasible"
    );
    assert!(!a2.is_strict(store), "A2: not strict");
    assert!(a2.is_firm(store), "A2: firm (only uses axiom p)");
    assert_eq!(a2.defeasible_rules(store).len(), 1, "A2: 1 defeasible rule");

    // B2: d2 ⇒ t — defeasible top rule, not strict, not firm, 1 def rule
    let b2 = store.get(args.b2).unwrap();
    assert!(
        b2.top_rule().unwrap().is_defeasible(),
        "B2: top rule d2 is defeasible"
    );
    assert!(!b2.is_strict(store), "B2: not strict");
    assert!(!b2.is_firm(store), "B2: not firm");
    assert_eq!(b2.defeasible_rules(store).len(), 1, "B2: 1 defeasible rule");

    // A3: s1 → r — strict top rule, but not strict overall (sub-arg uses d1)
    //   Firm (only axiom p used). 1 defeasible rule (d1).
    let a3 = store.get(args.a3).unwrap();
    assert!(
        a3.top_rule().unwrap().is_strict(),
        "A3: top rule s1 is strict"
    );
    assert!(
        !a3.is_strict(store),
        "A3: not strict (d1 used in sub-arg A2)"
    );
    assert!(a3.is_firm(store), "A3: firm");
    assert_eq!(
        a3.defeasible_rules(store).len(),
        1,
        "A3: 1 defeasible rule (d1)"
    );

    // B3: d3 ⇒ ¬d1 — defeasible top rule, not strict, not firm, 2 def rules
    let b3 = store.get(args.b3).unwrap();
    assert!(
        b3.top_rule().unwrap().is_defeasible(),
        "B3: top rule d3 is defeasible"
    );
    assert!(!b3.is_strict(store), "B3: not strict");
    assert!(!b3.is_firm(store), "B3: not firm");
    assert_eq!(
        b3.defeasible_rules(store).len(),
        2,
        "B3: 2 defeasible rules (d2, d3)"
    );

    // C2: d4 ⇒ v — not strict, not firm, 1 defeasible rule
    let c2 = store.get(args.c2).unwrap();
    assert!(!c2.is_strict(store), "C2: not strict");
    assert!(!c2.is_firm(store), "C2: not firm");
    assert_eq!(c2.defeasible_rules(store).len(), 1, "C2: 1 defeasible rule");

    // C3: s2 → ¬s — strict top rule, not strict overall (d4 via sub-arg C2),
    //   not firm, 1 defeasible rule (d4)
    let c3 = store.get(args.c3).unwrap();
    assert!(
        c3.top_rule().unwrap().is_strict(),
        "C3: top rule s2 is strict"
    );
    assert!(!c3.is_strict(store), "C3: not strict (d4 via C2)");
    assert!(!c3.is_firm(store), "C3: not firm");
    assert_eq!(
        c3.defeasible_rules(store).len(),
        1,
        "C3: 1 defeasible rule (d4)"
    );

    // D4: d5 ⇒ ¬t — defeasible top rule, not strict, not firm, 2 def rules
    let d4 = store.get(args.d4).unwrap();
    assert!(
        d4.top_rule().unwrap().is_defeasible(),
        "D4: top rule d5 is defeasible"
    );
    assert!(!d4.is_strict(store), "D4: not strict");
    assert!(!d4.is_firm(store), "D4: not firm");
    assert_eq!(
        d4.defeasible_rules(store).len(),
        2,
        "D4: 2 defeasible rules (d4, d5)"
    );
}

// --- Test 2: Attack Classification ---

#[test]
fn test_02_attack_classification() {
    let pipeline = AspicPipeline::classical(running_example(), Box::new(EqualOrdering));
    let result = pipeline.evaluate(Semantics::Grounded).unwrap();
    let store = &result.store;
    let attacks = &result.attacks;
    let args = find_running_example_args(store);

    // B3 undercuts A2 (on sub-arg A2, targeting rule d1)
    assert!(
        attack_exists(attacks, args.b3, args.a2, |k| matches!(
            k,
            AttackKind::Undercut { target_sub, rule_id }
                if *target_sub == args.a2 && rule_id.0 == "d1"
        )),
        "B3 should undercut A2 on rule d1"
    );

    // B3 undercuts A3 (on sub-arg A2, targeting rule d1)
    assert!(
        attack_exists(attacks, args.b3, args.a3, |k| matches!(
            k,
            AttackKind::Undercut { target_sub, rule_id }
                if *target_sub == args.a2 && rule_id.0 == "d1"
        )),
        "B3 should undercut A3 on sub-arg A2's rule d1"
    );

    // C3 undermines B1 (on premise s / B1)
    assert!(
        attack_exists(attacks, args.c3, args.b1, |k| matches!(
            k,
            AttackKind::Undermine { target_premise, .. } if *target_premise == args.b1
        )),
        "C3 should undermine B1"
    );

    // C3 undermines B2 (via premise B1)
    assert!(
        attack_exists(attacks, args.c3, args.b2, |k| matches!(
            k,
            AttackKind::Undermine { target_premise, .. } if *target_premise == args.b1
        )),
        "C3 should undermine B2 via premise B1"
    );

    // C3 undermines B3 (via premise B1)
    assert!(
        attack_exists(attacks, args.c3, args.b3, |k| matches!(
            k,
            AttackKind::Undermine { target_premise, .. } if *target_premise == args.b1
        )),
        "C3 should undermine B3 via premise B1"
    );

    // D4 rebuts B2 (on sub-arg B2)
    assert!(
        attack_exists(attacks, args.d4, args.b2, |k| matches!(
            k,
            AttackKind::Rebut { target_sub, .. } if *target_sub == args.b2
        )),
        "D4 should rebut B2"
    );

    // D4 rebuts B3 (on sub-arg B2)
    assert!(
        attack_exists(attacks, args.d4, args.b3, |k| matches!(
            k,
            AttackKind::Rebut { target_sub, .. } if *target_sub == args.b2
        )),
        "D4 should rebut B3 on sub-arg B2"
    );

    // B2 rebuts D4 (on D4 itself)
    assert!(
        attack_exists(attacks, args.b2, args.d4, |k| matches!(
            k,
            AttackKind::Rebut { target_sub, .. } if *target_sub == args.d4
        )),
        "B2 should rebut D4"
    );

    // B1 does NOT rebut C3 (C3 has strict top rule s2)
    assert!(
        !attack_exists(attacks, args.b1, args.c3, |k| matches!(
            k,
            AttackKind::Rebut { .. }
        )),
        "B1 should NOT rebut C3 (strict top rule s2)"
    );

    // Nothing attacks A1 (axiom premise)
    let any_attack_on_a1 = attacks.iter().any(|a| a.target == args.a1);
    assert!(!any_attack_on_a1, "nothing should attack A1 (axiom)");
}

// --- Test 3: Defeat with Last-Link ordering ---
//   Priorities: d2 < d5, d4 < d2, u < s, x < s

#[test]
fn test_03_defeat_with_last_link() {
    let ordering = last_link(
        vec![
            vec![RuleId("d5".into())],
            vec![RuleId("d2".into())],
            vec![RuleId("d4".into())],
        ],
        vec![vec![formula!(s)], vec![formula!(u), formula!(x)]],
    );

    let pipeline = AspicPipeline::classical(running_example(), Box::new(ordering));
    let result = pipeline.evaluate(Semantics::Grounded).unwrap();
    let store = &result.store;
    let args = find_running_example_args(store);

    let ordering2 = last_link(
        vec![
            vec![RuleId("d5".into())],
            vec![RuleId("d2".into())],
            vec![RuleId("d4".into())],
        ],
        vec![vec![formula!(s)], vec![formula!(u), formula!(x)]],
    );
    let defeats = compute_defeats(&result.attacks, store, &ordering2);

    // B3 undercuts A2 → defeat succeeds (undercuts always succeed)
    assert!(
        defeat_exists(&defeats, args.b3, args.a2),
        "B3 undercut on A2 should succeed as defeat"
    );

    // C3 undermines B1 → defeat FAILS (C3 has defeasible rules, B1 is premise)
    assert!(
        !defeat_exists(&defeats, args.c3, args.b1),
        "C3 undermine on B1 should fail (premise preferred over defeasible)"
    );

    // D4 rebuts B2 → defeat succeeds (d5 > d2)
    assert!(
        defeat_exists(&defeats, args.d4, args.b2),
        "D4 rebut on B2 should succeed (d5 > d2)"
    );

    // B2 rebuts D4 → defeat FAILS (d2 < d5)
    assert!(
        !defeat_exists(&defeats, args.b2, args.d4),
        "B2 rebut on D4 should fail (d2 < d5)"
    );
}

// --- Test 4: Extensions Scenario A ---
//   D4 strictly defeats B2 (d5 > d2), C3 does NOT defeat B1.
//   Expected: {r, p, q, ¬t, v, ¬s, s} justified; {t, ¬d1} not.

#[test]
fn test_04_extensions_scenario_a() {
    let ordering = last_link(
        vec![
            vec![RuleId("d5".into())],
            vec![RuleId("d2".into())],
            vec![RuleId("d4".into())],
        ],
        vec![vec![formula!(s)], vec![formula!(u), formula!(x)]],
    );

    let pipeline = AspicPipeline::classical(running_example(), Box::new(ordering));
    let result = pipeline.evaluate(Semantics::Grounded).unwrap();
    let store = &result.store;
    assert!(
        !result.extensions.is_empty(),
        "should have at least one extension"
    );

    let conclusions = conclusions_in(&result.extensions[0], store);

    for (f, label) in [
        (formula!(r), "r"),
        (formula!(p), "p"),
        (formula!(q), "q"),
        (formula!(!t), "¬t"),
        (formula!(v), "v"),
        (formula!(!s), "¬s"),
        (formula!(s), "s"),
    ] {
        assert!(
            conclusions.contains(&f),
            "{label} should be justified in scenario A. Got: {conclusions:?}"
        );
    }

    assert!(
        !conclusions.contains(&formula!(t)),
        "t should NOT be justified in scenario A"
    );
    assert!(
        !conclusions.contains(&formula!(!d1)),
        "¬d1 should NOT be justified in scenario A"
    );
}

// --- Test 5: Extensions Scenario B ---
//   C3 defeats B1 (EqualOrdering: undermine succeeds).
//   B1 is out → B2, B3 out → A2, A3 freed → r justified.

#[test]
fn test_05_extensions_scenario_b() {
    let pipeline = AspicPipeline::classical(running_example(), Box::new(EqualOrdering));
    let result = pipeline.evaluate(Semantics::Grounded).unwrap();
    let store = &result.store;

    let conclusions = conclusions_in(&result.extensions[0], store);

    assert!(
        conclusions.contains(&formula!(r)),
        "r should be justified in scenario B"
    );
    assert!(
        conclusions.contains(&formula!(q)),
        "q should be justified in scenario B"
    );
    assert!(
        conclusions.contains(&formula!(!t)),
        "¬t should be justified in scenario B"
    );

    // s should NOT be justified (B1 undermined by C3)
    assert!(
        !conclusions.contains(&formula!(s)),
        "s should NOT be justified (B1 defeated by C3)"
    );
}

// --- Test 6: Extensions Scenario C ---
//   B2 strictly defeats D4 (d2 > d5), C3 does NOT defeat B1.
//   Expected: {t, ¬d1, s, v, ¬s, p} justified; r, q NOT justified.

#[test]
fn test_06_extensions_scenario_c() {
    let ordering = last_link(
        vec![vec![RuleId("d2".into())], vec![RuleId("d5".into())]],
        vec![],
    );

    let pipeline = AspicPipeline::classical(running_example(), Box::new(ordering));
    let result = pipeline.evaluate(Semantics::Grounded).unwrap();
    let store = &result.store;

    let conclusions = conclusions_in(&result.extensions[0], store);

    for (f, label) in [
        (formula!(t), "t"),
        (formula!(!d1), "¬d1"),
        (formula!(s), "s"),
        (formula!(v), "v"),
        (formula!(!s), "¬s"),
        (formula!(p), "p"),
    ] {
        assert!(
            conclusions.contains(&f),
            "{label} should be justified in scenario C. Got: {conclusions:?}"
        );
    }

    assert!(
        !conclusions.contains(&formula!(r)),
        "r should NOT be justified in scenario C"
    );
    assert!(
        !conclusions.contains(&formula!(q)),
        "q should NOT be justified in scenario C"
    );
}

// --- Test 7: Extensions Scenario D ---
//   B2 and D4 defeat each other (mutual), C3 does NOT defeat B1.
//   Grounded: {p, s, u, x, v, ¬s}; r NOT justified.
//   Preferred/Stable: two extensions.

#[test]
fn test_07_extensions_scenario_d() {
    let system = running_example();

    // --- Grounded ---
    let grounded_result = AspicPipeline::classical(
        system.clone(),
        Box::new(LastLinkOrdering {
            rule_ordering: Box::new(NoPreference),
            premise_ordering: Box::new(NoPreference),
            lifting: LiftingStrategy::Elitist,
        }),
    )
    .evaluate(Semantics::Grounded)
    .unwrap();

    let g_conclusions = conclusions_in(&grounded_result.extensions[0], &grounded_result.store);

    for (f, label) in [
        (formula!(p), "p"),
        (formula!(s), "s"),
        (formula!(u), "u"),
        (formula!(v), "v"),
        (formula!(!s), "¬s"),
    ] {
        assert!(
            g_conclusions.contains(&f),
            "Grounded should include {label}. Got: {g_conclusions:?}"
        );
    }
    assert!(
        !g_conclusions.contains(&formula!(r)),
        "Grounded should NOT include r"
    );

    // --- Preferred ---
    let preferred_result = AspicPipeline::classical(
        system.clone(),
        Box::new(LastLinkOrdering {
            rule_ordering: Box::new(NoPreference),
            premise_ordering: Box::new(NoPreference),
            lifting: LiftingStrategy::Elitist,
        }),
    )
    .evaluate(Semantics::Preferred)
    .unwrap();

    assert_eq!(
        preferred_result.extensions.len(),
        2,
        "Preferred semantics should yield 2 extensions"
    );

    let pref_conclusions: Vec<BTreeSet<Formula>> = preferred_result
        .extensions
        .iter()
        .map(|ext| conclusions_in(ext, &preferred_result.store))
        .collect();

    // One extension should contain t (and ¬d1), the other should contain r (and ¬t)
    let has_t_ext = pref_conclusions.iter().any(|c| c.contains(&formula!(t)));
    let has_r_ext = pref_conclusions.iter().any(|c| c.contains(&formula!(r)));
    assert!(has_t_ext, "One preferred extension should contain t");
    assert!(has_r_ext, "One preferred extension should contain r");

    // --- Stable ---
    let stable_result = AspicPipeline::classical(
        system,
        Box::new(LastLinkOrdering {
            rule_ordering: Box::new(NoPreference),
            premise_ordering: Box::new(NoPreference),
            lifting: LiftingStrategy::Elitist,
        }),
    )
    .evaluate(Semantics::Stable)
    .unwrap();

    assert_eq!(
        stable_result.extensions.len(),
        2,
        "Stable semantics should yield 2 extensions"
    );
}

// --- Test 8: Transposition Restores Consistency ---
//   Add s2': s → ¬v (strict). Creates argument B1' → ¬v.
//   B1' rebuts C2 (v via defeasible d4).

#[test]
fn test_08_transposition() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .axiom(formula!(p))
        .ordinary_premise(formula!(s))
        .ordinary_premise(formula!(u))
        .ordinary_premise(formula!(x))
        .strict_rule("s1", vec![formula!(p), formula!(q)], formula!(r))
        .strict_rule("s2", vec![formula!(v)], formula!(!s))
        .strict_rule("s2p", vec![formula!(s)], formula!(!v))
        .named_defeasible_rule("d1", formula!(d1), vec![formula!(p)], formula!(q))
        .named_defeasible_rule("d2", formula!(d2), vec![formula!(s)], formula!(t))
        .named_defeasible_rule("d3", formula!(d3), vec![formula!(t)], formula!(!d1))
        .named_defeasible_rule("d4", formula!(d4), vec![formula!(u)], formula!(v))
        .named_defeasible_rule(
            "d5",
            formula!(d5),
            vec![formula!(v), formula!(x)],
            formula!(!t),
        )
        .named_defeasible_rule("d6", formula!(d6), vec![formula!(s)], formula!(!p))
        .build();

    let pipeline = AspicPipeline::classical(system, Box::new(EqualOrdering));
    let result = pipeline.evaluate(Semantics::Grounded).unwrap();
    let store = &result.store;
    let attacks = &result.attacks;

    // B1': [B1; s2'] → ¬v
    let b1_prime = find_arg_by_conclusion_and_rule(store, &formula!(!v), "s2p")
        .expect("B1' (¬v via s2p) should exist after transposition");

    // C2: [C1; d4] → v
    let c2 = find_arg_by_conclusion_and_rule(store, &formula!(v), "d4")
        .expect("C2 (v via d4) should exist");

    // B1' rebuts C2 (v via defeasible d4)
    assert!(
        attack_exists(attacks, b1_prime, c2, |k| matches!(
            k,
            AttackKind::Rebut { target_sub, .. } if *target_sub == c2
        )),
        "B1' should rebut C2 (transposition creates ¬v which attacks v via defeasible d4)"
    );
}

// --- Test 9: Bachelor / Married ---
//   Kp = {WearsRing, PartyAnimal}
//   Rs = {s1: Married → ¬Bachelor;  s2: Bachelor → ¬Married}
//   Rd = {d1: WearsRing ⇒ Married;  d2: PartyAnimal ⇒ Bachelor}

#[test]
fn test_09_bachelor_married() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .ordinary_premise(formula!(WearsRing))
        .ordinary_premise(formula!(PartyAnimal))
        .strict_rule("s1", vec![formula!(Married)], formula!(!Bachelor))
        .strict_rule("s2", vec![formula!(Bachelor)], formula!(!Married))
        .named_defeasible_rule(
            "d1",
            formula!(d1),
            vec![formula!(WearsRing)],
            formula!(Married),
        )
        .named_defeasible_rule(
            "d2",
            formula!(d2),
            vec![formula!(PartyAnimal)],
            formula!(Bachelor),
        )
        .build();

    // --- No preferences (EqualOrdering) ---
    // Grounded: only premises
    let grounded_result = AspicPipeline::classical(system.clone(), Box::new(EqualOrdering))
        .evaluate(Semantics::Grounded)
        .unwrap();

    let g_conclusions = conclusions_in(&grounded_result.extensions[0], &grounded_result.store);

    assert!(
        g_conclusions.contains(&formula!(WearsRing)),
        "Grounded (no pref) should include WearsRing"
    );
    assert!(
        g_conclusions.contains(&formula!(PartyAnimal)),
        "Grounded (no pref) should include PartyAnimal"
    );
    assert!(
        !g_conclusions.contains(&formula!(Married)),
        "Grounded (no pref) should NOT include Married"
    );
    assert!(
        !g_conclusions.contains(&formula!(Bachelor)),
        "Grounded (no pref) should NOT include Bachelor"
    );

    // Preferred: two extensions
    let preferred_result = AspicPipeline::classical(system.clone(), Box::new(EqualOrdering))
        .evaluate(Semantics::Preferred)
        .unwrap();

    assert_eq!(
        preferred_result.extensions.len(),
        2,
        "Preferred (no pref) should have 2 extensions"
    );

    let pref_conclusions: Vec<BTreeSet<Formula>> = preferred_result
        .extensions
        .iter()
        .map(|ext| conclusions_in(ext, &preferred_result.store))
        .collect();

    let has_married = pref_conclusions
        .iter()
        .any(|c| c.contains(&formula!(Married)));
    let has_bachelor = pref_conclusions
        .iter()
        .any(|c| c.contains(&formula!(Bachelor)));
    assert!(has_married, "One preferred ext should contain Married");
    assert!(has_bachelor, "One preferred ext should contain Bachelor");

    // Stable: two extensions
    let stable_result = AspicPipeline::classical(system.clone(), Box::new(EqualOrdering))
        .evaluate(Semantics::Stable)
        .unwrap();

    assert_eq!(
        stable_result.extensions.len(),
        2,
        "Stable (no pref) should have 2 extensions"
    );

    // --- With d1 < d2 (d2 preferred, last-link) ---
    // Single extension: {A1, B1, B2, B3} → Bachelor, ¬Married
    let ordered_result = AspicPipeline::classical(
        system,
        Box::new(last_link(
            vec![vec![RuleId("d2".into())], vec![RuleId("d1".into())]],
            vec![],
        )),
    )
    .evaluate(Semantics::Grounded)
    .unwrap();

    let ord_conclusions = conclusions_in(&ordered_result.extensions[0], &ordered_result.store);

    assert!(
        ord_conclusions.contains(&formula!(Bachelor)),
        "With d1 < d2: Bachelor should be justified"
    );
    assert!(
        ord_conclusions.contains(&formula!(!Married)),
        "With d1 < d2: ¬Married should be justified"
    );
    assert!(
        !ord_conclusions.contains(&formula!(Married)),
        "With d1 < d2: Married should NOT be justified"
    );
}

// --- Test 10: Bachelor / Married without transposition ---
//   Remove s2. Only s1: Married → ¬Bachelor.
//   With d1 < d2: A3 does NOT defeat B2.
//   Single extension: both Bachelor and ¬Bachelor.

#[test]
fn test_10_bachelor_married_no_transposition() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .ordinary_premise(formula!(WearsRing))
        .ordinary_premise(formula!(PartyAnimal))
        .strict_rule("s1", vec![formula!(Married)], formula!(!Bachelor))
        .named_defeasible_rule(
            "d1",
            formula!(d1),
            vec![formula!(WearsRing)],
            formula!(Married),
        )
        .named_defeasible_rule(
            "d2",
            formula!(d2),
            vec![formula!(PartyAnimal)],
            formula!(Bachelor),
        )
        .build();

    let ordering = last_link(
        vec![vec![RuleId("d2".into())], vec![RuleId("d1".into())]],
        vec![],
    );

    let pipeline = AspicPipeline::classical(system, Box::new(ordering));
    let result = pipeline.evaluate(Semantics::Grounded).unwrap();
    let store = &result.store;

    let a2 = find_arg_by_conclusion_and_rule(store, &formula!(Married), "d1")
        .expect("A2: Married via d1");
    let b2 = find_arg_by_conclusion_and_rule(store, &formula!(Bachelor), "d2")
        .expect("B2: Bachelor via d2");
    let a3 = find_arg_by_conclusion_and_rule(store, &formula!(!Bachelor), "s1")
        .expect("A3: ¬Bachelor via s1");

    let ordering2 = last_link(
        vec![vec![RuleId("d2".into())], vec![RuleId("d1".into())]],
        vec![],
    );
    let defeats = compute_defeats(&result.attacks, store, &ordering2);

    // A3 rebuts B2 but A3 ≺ B2 (d1 < d2), so A3 does NOT defeat B2
    assert!(
        !defeat_exists(&defeats, a3, b2),
        "A3 should NOT defeat B2 (d1 < d2 makes A3 strictly dispreferred)"
    );

    // No argument for ¬Married (s2 removed), so nothing attacks A2
    assert!(
        !defeats.iter().any(|d| d.target == a2),
        "A2 should have no defeaters (no transposed rule)"
    );

    let conclusions = conclusions_in(&result.extensions[0], store);

    // Both Bachelor and ¬Bachelor are justified (inconsistency without transposition)
    assert!(
        conclusions.contains(&formula!(Bachelor)),
        "Bachelor should be justified"
    );
    assert!(
        conclusions.contains(&formula!(!Bachelor)),
        "¬Bachelor should be justified (inconsistency without transposition)"
    );
    assert!(
        conclusions.contains(&formula!(Married)),
        "Married should be justified"
    );
}

// --- Test 11a: Library Access — Last-Link ---

#[test]
fn test_11a_library_access_last_link() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .ordinary_premise(formula!(Snores))
        .ordinary_premise(formula!(Professor))
        .named_defeasible_rule(
            "d1",
            formula!(d1),
            vec![formula!(Snores)],
            formula!(Misbehaves),
        )
        .named_defeasible_rule(
            "d2",
            formula!(d2),
            vec![formula!(Misbehaves)],
            formula!(AccessDenied),
        )
        .named_defeasible_rule(
            "d3",
            formula!(d3),
            vec![formula!(Professor)],
            formula!(!AccessDenied),
        )
        .build();

    let rule_ord = TieredOrdering::new(vec![
        vec![RuleId("d2".into())],
        vec![RuleId("d3".into())],
        vec![RuleId("d1".into())],
    ]);
    let premise_ord = TieredOrdering::new(vec![vec![formula!(Professor)], vec![formula!(Snores)]]);

    let pipeline = AspicPipeline::classical(
        system,
        Box::new(LastLinkOrdering {
            rule_ordering: Box::new(rule_ord),
            premise_ordering: Box::new(premise_ord),
            lifting: LiftingStrategy::Elitist,
        }),
    );

    let result = pipeline.evaluate(Semantics::Preferred).unwrap();
    assert_eq!(
        result.extensions.len(),
        1,
        "should have one preferred extension"
    );

    let conc = conclusions_in(&result.extensions[0], &result.store);
    assert!(
        conc.contains(&formula!(AccessDenied)),
        "AccessDenied justified under last-link"
    );
    assert!(
        !conc.contains(&formula!(!AccessDenied)),
        "¬AccessDenied NOT justified under last-link"
    );
    assert!(conc.contains(&formula!(Misbehaves)), "Misbehaves justified");
}

// --- Test 11b: Library Access — Weakest-Link ---

#[test]
fn test_11b_library_access_weakest_link() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .ordinary_premise(formula!(Snores))
        .ordinary_premise(formula!(Professor))
        .named_defeasible_rule(
            "d1",
            formula!(d1),
            vec![formula!(Snores)],
            formula!(Misbehaves),
        )
        .named_defeasible_rule(
            "d2",
            formula!(d2),
            vec![formula!(Misbehaves)],
            formula!(AccessDenied),
        )
        .named_defeasible_rule(
            "d3",
            formula!(d3),
            vec![formula!(Professor)],
            formula!(!AccessDenied),
        )
        .build();

    let rule_ord = TieredOrdering::new(vec![
        vec![RuleId("d2".into())],
        vec![RuleId("d3".into())],
        vec![RuleId("d1".into())],
    ]);
    let premise_ord = TieredOrdering::new(vec![vec![formula!(Professor)], vec![formula!(Snores)]]);

    let pipeline = AspicPipeline::classical(
        system,
        Box::new(WeakestLinkOrdering {
            rule_ordering: Box::new(rule_ord),
            premise_ordering: Box::new(premise_ord),
            lifting: LiftingStrategy::Elitist,
        }),
    );

    let result = pipeline.evaluate(Semantics::Preferred).unwrap();
    assert_eq!(
        result.extensions.len(),
        1,
        "should have one preferred extension"
    );

    let conc = conclusions_in(&result.extensions[0], &result.store);
    assert!(
        conc.contains(&formula!(!AccessDenied)),
        "¬AccessDenied justified under weakest-link"
    );
    assert!(
        !conc.contains(&formula!(AccessDenied)),
        "AccessDenied NOT justified under weakest-link"
    );
    assert!(
        conc.contains(&formula!(Misbehaves)),
        "Misbehaves still justified"
    );
}

// --- Test 12: Scottish Whisky — Weakest-Link ---

#[test]
fn test_12_scottish_whisky_weakest_link() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .ordinary_premise(formula!(BornInScotland))
        .ordinary_premise(formula!(FitnessLover))
        .named_defeasible_rule(
            "d1",
            formula!(d1),
            vec![formula!(BornInScotland)],
            formula!(Scottish),
        )
        .named_defeasible_rule(
            "d2",
            formula!(d2),
            vec![formula!(Scottish)],
            formula!(LikesWhisky),
        )
        .named_defeasible_rule(
            "d3",
            formula!(d3),
            vec![formula!(FitnessLover)],
            formula!(!LikesWhisky),
        )
        .build();

    let rule_ord = TieredOrdering::new(vec![
        vec![RuleId("d2".into())],
        vec![RuleId("d3".into())],
        vec![RuleId("d1".into())],
    ]);
    let premise_ord = TieredOrdering::new(vec![
        vec![formula!(FitnessLover)],
        vec![formula!(BornInScotland)],
    ]);

    let pipeline = AspicPipeline::classical(
        system,
        Box::new(WeakestLinkOrdering {
            rule_ordering: Box::new(rule_ord),
            premise_ordering: Box::new(premise_ord),
            lifting: LiftingStrategy::Elitist,
        }),
    );

    let result = pipeline.evaluate(Semantics::Preferred).unwrap();
    assert_eq!(result.extensions.len(), 1);

    let conc = conclusions_in(&result.extensions[0], &result.store);
    assert!(
        conc.contains(&formula!(!LikesWhisky)),
        "¬LikesWhisky justified"
    );
    assert!(
        !conc.contains(&formula!(LikesWhisky)),
        "LikesWhisky NOT justified"
    );
    assert!(
        conc.contains(&formula!(Scottish)),
        "Scottish still justified"
    );
}

// --- Test 13: Tweety Triangle via Undercutting ---

#[test]
fn test_13_tweety_undercutting() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .axiom(formula!(observed_as_penguin))
        .strict_rule("s1", vec![formula!(penguin)], formula!(bird))
        .strict_rule("s2", vec![formula!(penguin)], formula!(ab1))
        .strict_rule("s3", vec![formula!(ab1)], formula!(!d1))
        .named_defeasible_rule("d1", formula!(d1), vec![formula!(bird)], formula!(canfly))
        .named_defeasible_rule(
            "d2",
            formula!(d2),
            vec![formula!(penguin)],
            formula!(!canfly),
        )
        .named_defeasible_rule(
            "d3",
            formula!(d3),
            vec![formula!(observed_as_penguin)],
            formula!(penguin),
        )
        .build();

    let pipeline = AspicPipeline::classical(
        system,
        Box::new(LastLinkOrdering {
            rule_ordering: Box::new(NoPreference),
            premise_ordering: Box::new(NoPreference),
            lifting: LiftingStrategy::Elitist,
        }),
    );

    let result = pipeline.evaluate(Semantics::Grounded).unwrap();
    let conc = conclusions_in(&result.extensions[0], &result.store);

    assert!(conc.contains(&formula!(penguin)), "penguin justified");
    assert!(conc.contains(&formula!(bird)), "bird justified");
    assert!(
        conc.contains(&formula!(!d1)),
        "¬d1 justified (undercuts d1)"
    );
    assert!(conc.contains(&formula!(!canfly)), "¬canfly justified");
    assert!(
        !conc.contains(&formula!(canfly)),
        "canfly NOT justified (d1 undercut)"
    );
}

// --- Test 14: Undercutting Immune to Preferences ---

#[test]
fn test_14_undercutting_immune_to_preferences() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .ordinary_premise(formula!(a))
        .ordinary_premise(formula!(b))
        .named_defeasible_rule("d1", formula!(d1), vec![formula!(a)], formula!(c))
        .named_defeasible_rule("d2", formula!(d2), vec![formula!(b)], formula!(!d1))
        .build();

    let rule_ord = TieredOrdering::new(vec![vec![RuleId("d1".into())], vec![RuleId("d2".into())]]);
    let premise_ord = TieredOrdering::new(vec![vec![formula!(a)], vec![formula!(b)]]);

    let pipeline = AspicPipeline::classical(
        system,
        Box::new(LastLinkOrdering {
            rule_ordering: Box::new(rule_ord),
            premise_ordering: Box::new(premise_ord),
            lifting: LiftingStrategy::Elitist,
        }),
    );

    let result = pipeline.evaluate(Semantics::Grounded).unwrap();
    let conc = conclusions_in(&result.extensions[0], &result.store);

    assert!(
        conc.contains(&formula!(!d1)),
        "¬d1 justified (undercut always succeeds)"
    );
    assert!(
        !conc.contains(&formula!(c)),
        "c NOT justified (d1 undercut)"
    );
}

// --- Test 15a: Undermining — No Preferences ---

#[test]
fn test_15a_undermining_no_preferences() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .ordinary_premise(formula!(a))
        .named_defeasible_rule("d1", formula!(d1), vec![], formula!(!a))
        .build();

    // Grounded: empty (mutual defeat)
    let result_g = AspicPipeline::classical(system.clone(), Box::new(EqualOrdering))
        .evaluate(Semantics::Grounded)
        .unwrap();
    assert!(
        result_g.extensions[0].is_empty(),
        "Grounded should be empty"
    );

    // Preferred: two extensions
    let result_p = AspicPipeline::classical(system, Box::new(EqualOrdering))
        .evaluate(Semantics::Preferred)
        .unwrap();
    assert_eq!(
        result_p.extensions.len(),
        2,
        "Should have two preferred extensions"
    );

    let ext_concs: Vec<BTreeSet<Formula>> = result_p
        .extensions
        .iter()
        .map(|ext| conclusions_in(ext, &result_p.store))
        .collect();
    let has_a = ext_concs
        .iter()
        .any(|c| c.contains(&formula!(a)) && !c.contains(&formula!(!a)));
    let has_not_a = ext_concs
        .iter()
        .any(|c| c.contains(&formula!(!a)) && !c.contains(&formula!(a)));
    assert!(has_a, "One extension should contain a");
    assert!(has_not_a, "One extension should contain ¬a");
}

// --- Test 15b: Undermining — Premise Preferred (last-link) ---

#[test]
fn test_15b_undermining_premise_preferred() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .ordinary_premise(formula!(a))
        .named_defeasible_rule("d1", formula!(d1), vec![], formula!(!a))
        .build();

    let pipeline = AspicPipeline::classical(
        system,
        Box::new(LastLinkOrdering {
            rule_ordering: Box::new(NoPreference),
            premise_ordering: Box::new(NoPreference),
            lifting: LiftingStrategy::Elitist,
        }),
    );

    let result = pipeline.evaluate(Semantics::Grounded).unwrap();
    let conc = conclusions_in(&result.extensions[0], &result.store);
    assert!(
        conc.contains(&formula!(a)),
        "a justified (premise > defeasible)"
    );
    assert!(!conc.contains(&formula!(!a)), "¬a NOT justified");
}

// --- Test 15c: Undermining — Defeasible Rule Preferred (custom ordering) ---

#[test]
fn test_15c_undermining_defeasible_preferred() {
    /// Custom ordering where premise arguments are strictly dispreferred.
    #[derive(Debug)]
    struct PremiseWeakerOrdering;
    impl ArgumentOrdering for PremiseWeakerOrdering {
        fn compare(&self, a: ArgumentId, b: ArgumentId, store: &ArgumentStore) -> Preference {
            let a_is_premise = matches!(store.get(a), Some(Argument::Premise { .. }));
            let b_is_premise = matches!(store.get(b), Some(Argument::Premise { .. }));
            match (a_is_premise, b_is_premise) {
                (true, false) => Preference::StrictlyDispreferred,
                (false, true) => Preference::StrictlyPreferred,
                _ => Preference::Equal,
            }
        }
    }

    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .ordinary_premise(formula!(a))
        .named_defeasible_rule("d1", formula!(d1), vec![], formula!(!a))
        .build();

    let pipeline = AspicPipeline::classical(system, Box::new(PremiseWeakerOrdering));

    let result = pipeline.evaluate(Semantics::Grounded).unwrap();
    let conc = conclusions_in(&result.extensions[0], &result.store);
    assert!(
        conc.contains(&formula!(!a)),
        "¬a justified when premise is weaker"
    );
    assert!(
        !conc.contains(&formula!(a)),
        "a NOT justified when premise is weaker"
    );
}

// --- Test 16: Strict Rules Cannot Be Attacked ---

#[test]
fn test_16_strict_rules_cannot_be_attacked() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .axiom(formula!(a))
        .ordinary_premise(formula!(b))
        .strict_rule("s1", vec![formula!(a)], formula!(c))
        .named_defeasible_rule("d1", formula!(d1), vec![formula!(b)], formula!(!c))
        .build();

    let pipeline = AspicPipeline::classical(
        system,
        Box::new(LastLinkOrdering {
            rule_ordering: Box::new(NoPreference),
            premise_ordering: Box::new(NoPreference),
            lifting: LiftingStrategy::Elitist,
        }),
    );

    let result = pipeline.evaluate(Semantics::Grounded).unwrap();
    let conc = conclusions_in(&result.extensions[0], &result.store);

    assert!(
        conc.contains(&formula!(c)),
        "c justified (strict rule cannot be rebutted)"
    );
    assert!(
        conc.contains(&formula!(b)),
        "b (ordinary premise) still in extension"
    );
    assert!(!conc.contains(&formula!(!c)), "¬c NOT justified");
}

// --- Test 17: LastDefRules Through Mixed Chains ---

#[test]
fn test_17_last_def_rules_through_mixed_chains() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .ordinary_premise(formula!(p))
        .ordinary_premise(formula!(q))
        .strict_rule("s1", vec![formula!(r), formula!(s)], formula!(t))
        .named_defeasible_rule("d1", formula!(d1), vec![formula!(p)], formula!(r))
        .named_defeasible_rule("d2", formula!(d2), vec![formula!(q)], formula!(s))
        .build();

    let pipeline = AspicPipeline::classical(
        system,
        Box::new(LastLinkOrdering {
            rule_ordering: Box::new(NoPreference),
            premise_ordering: Box::new(NoPreference),
            lifting: LiftingStrategy::Elitist,
        }),
    );

    let result = pipeline.evaluate(Semantics::Grounded).unwrap();
    let t_id =
        find_arg_by_conclusion(&result.store, &formula!(t)).expect("should have argument for t");
    let t_arg = result.store.get(t_id).unwrap();

    let last_def = t_arg.last_defeasible_rules(&result.store);
    let last_def_ids: BTreeSet<String> = last_def.iter().map(|r| r.id.0.clone()).collect();

    assert!(
        last_def_ids.contains("d1"),
        "LastDefRules should contain d1"
    );
    assert!(
        last_def_ids.contains("d2"),
        "LastDefRules should contain d2"
    );
    assert_eq!(
        last_def_ids.len(),
        2,
        "LastDefRules should have exactly 2 rules"
    );
}

// --- Test 18: Self-Defeating Argument ---

#[test]
fn test_18_self_defeating_argument() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .ordinary_premise(formula!(a))
        .named_defeasible_rule("d1", formula!(d1), vec![formula!(a)], formula!(!d1))
        .build();

    let pipeline = AspicPipeline::classical(system, Box::new(EqualOrdering));

    let result = pipeline.evaluate(Semantics::Grounded).unwrap();
    let conc = conclusions_in(&result.extensions[0], &result.store);

    assert!(
        conc.contains(&formula!(a)),
        "a (premise) should be in extension"
    );
    assert!(
        !conc.contains(&formula!(!d1)),
        "¬d1 NOT justified (self-defeating)"
    );

    // Verify the self-attack exists
    let a2 = find_arg_by_conclusion_and_rule(&result.store, &formula!(!d1), "d1")
        .expect("A2 (¬d1 via d1) should exist");
    let self_attacks: Vec<_> = result
        .attacks
        .iter()
        .filter(|a| a.attacker == a2 && a.target == a2)
        .collect();
    assert!(!self_attacks.is_empty(), "A2 should self-attack");
}

// --- Test 19: Odd Cycle — 3 Arguments ---

#[test]
fn test_19_odd_cycle_three_arguments() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .ordinary_premise(formula!(a))
        .ordinary_premise(formula!(b))
        .ordinary_premise(formula!(c))
        .contrary(formula!(b), formula!(!b))
        .contrary(formula!(c), formula!(!c))
        .contrary(formula!(a), formula!(!a))
        .named_defeasible_rule("d1", formula!(d1), vec![formula!(a)], formula!(!b))
        .named_defeasible_rule("d2", formula!(d2), vec![formula!(b)], formula!(!c))
        .named_defeasible_rule("d3", formula!(d3), vec![formula!(c)], formula!(!a))
        .build();

    // Grounded: empty
    let result_g = AspicPipeline::classical(system.clone(), Box::new(EqualOrdering))
        .evaluate(Semantics::Grounded)
        .unwrap();
    assert!(
        result_g.extensions[0].is_empty(),
        "Grounded should be empty in odd cycle"
    );

    // Preferred: single empty extension
    let result_p = AspicPipeline::classical(system.clone(), Box::new(EqualOrdering))
        .evaluate(Semantics::Preferred)
        .unwrap();
    assert_eq!(
        result_p.extensions.len(),
        1,
        "Should have exactly one preferred extension"
    );
    assert!(
        result_p.extensions[0].is_empty(),
        "Preferred extension should be empty"
    );

    // Stable: none exists
    let result_s = AspicPipeline::classical(system, Box::new(EqualOrdering))
        .evaluate(Semantics::Stable)
        .unwrap();
    assert!(
        result_s.extensions.is_empty(),
        "No stable extension should exist in odd cycle"
    );
}

// --- Test 20: Even Cycle — 2 Arguments ---

#[test]
fn test_20_even_cycle_two_arguments() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .ordinary_premise(formula!(a))
        .ordinary_premise(formula!(b))
        .contrary(formula!(b), formula!(!b))
        .contrary(formula!(a), formula!(!a))
        .named_defeasible_rule("d1", formula!(d1), vec![formula!(a)], formula!(!b))
        .named_defeasible_rule("d2", formula!(d2), vec![formula!(b)], formula!(!a))
        .build();

    // Grounded: empty
    let result_g = AspicPipeline::classical(system.clone(), Box::new(EqualOrdering))
        .evaluate(Semantics::Grounded)
        .unwrap();
    assert!(
        result_g.extensions[0].is_empty(),
        "Grounded should be empty in even cycle"
    );

    // Preferred: two extensions
    let result_p = AspicPipeline::classical(system.clone(), Box::new(EqualOrdering))
        .evaluate(Semantics::Preferred)
        .unwrap();
    assert_eq!(
        result_p.extensions.len(),
        2,
        "Should have two preferred extensions"
    );

    let pref_concs: Vec<BTreeSet<Formula>> = result_p
        .extensions
        .iter()
        .map(|ext| conclusions_in(ext, &result_p.store))
        .collect();
    let has_a_ext = pref_concs.iter().any(|c| {
        c.contains(&formula!(a)) && c.contains(&formula!(!b)) && !c.contains(&formula!(b))
    });
    let has_b_ext = pref_concs.iter().any(|c| {
        c.contains(&formula!(b)) && c.contains(&formula!(!a)) && !c.contains(&formula!(a))
    });
    assert!(has_a_ext, "One preferred extension should justify a and ¬b");
    assert!(has_b_ext, "One preferred extension should justify b and ¬a");

    // Stable: same two extensions
    let result_s = AspicPipeline::classical(system, Box::new(EqualOrdering))
        .evaluate(Semantics::Stable)
        .unwrap();
    assert_eq!(
        result_s.extensions.len(),
        2,
        "Should have two stable extensions"
    );
}
