mod common;

use common::{attack_exists, find_arg_by_conclusion_and_rule, find_premise_arg};
use pickaxe_rs::formula;
use pickaxe_rs::prelude::*;
use pickaxe_rs::system::rules::RuleId;

// ---
// Helper functions
// ---

/// Build the running example from Modgil & Prakken 2014, Example 3.7,
/// ground it, construct arguments, and return the store + contrariness.
fn build_example_3_7() -> (ArgumentStore, ContrarinessFunction) {
    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))
        .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 grounded = NaiveGrounder.ground(&system).unwrap();
    let contrariness = grounded.contrariness.clone();
    let store = ForwardChainingConstructor.construct(&grounded);
    (store, contrariness)
}

/// Build Example 4.1 (bachelor-married), ground, construct, return store + contrariness.
fn build_example_4_1() -> (ArgumentStore, ContrarinessFunction) {
    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();
    let grounded = NaiveGrounder.ground(&system).unwrap();
    let contrariness = grounded.contrariness.clone();
    let store = ForwardChainingConstructor.construct(&grounded);
    (store, contrariness)
}

/// Normalize an attack into a comparable tuple for sorting.
fn attack_key(a: &Attack) -> (usize, usize, u8, usize, String) {
    let kind_tag = match &a.kind {
        AttackKind::Rebut { .. } => 0u8,
        AttackKind::Undermine { .. } => 1,
        AttackKind::Undercut { .. } => 2,
    };
    let (sub_id, rule_str) = match &a.kind {
        AttackKind::Rebut { target_sub, .. } => (target_sub.0, String::new()),
        AttackKind::Undermine { target_premise, .. } => (target_premise.0, String::new()),
        AttackKind::Undercut {
            target_sub,
            rule_id,
        } => (target_sub.0, rule_id.0.clone()),
    };
    (a.attacker.0, a.target.0, kind_tag, sub_id, rule_str)
}

// ---
// relation_between() tests
// ---

#[test]
fn test_relation_between_contrary() {
    let mut cf = ContrarinessFunction::new();
    let a = formula!(a);
    let b = formula!(b);
    cf.add_contrary(a.clone(), b.clone());

    assert_eq!(
        cf.relation_between(&a, &b),
        Some(ContrarinessRelation::Contrary),
        "b is a contrary of a"
    );
    assert_eq!(
        cf.relation_between(&b, &a),
        None,
        "a is NOT a contrary of b (asymmetric)"
    );
}

#[test]
fn test_relation_between_contradictory() {
    let mut cf = ContrarinessFunction::new();
    let a = formula!(a);
    let b = formula!(b);
    cf.add_contradictory(a.clone(), b.clone());

    assert_eq!(
        cf.relation_between(&a, &b),
        Some(ContrarinessRelation::Contradictory),
    );
    assert_eq!(
        cf.relation_between(&b, &a),
        Some(ContrarinessRelation::Contradictory),
        "contradictory is symmetric"
    );
}

#[test]
fn test_relation_between_classical_negation() {
    let cf = ContrarinessFunction::new().with_classical_negation();

    assert_eq!(
        cf.relation_between(&formula!(p), &formula!(!p)),
        Some(ContrarinessRelation::Contradictory),
    );
    assert_eq!(
        cf.relation_between(&formula!(p), &formula!(q)),
        None,
        "unrelated formulae have no relation"
    );
}

// ---
// Example 3.7/3.11 attack completeness and kinds
// ---

#[test]
fn test_example_3_7_undercut_attacks() {
    let (store, contrariness) = build_example_3_7();
    let attacks = PairwiseAttackComputer.compute(&store, &contrariness);

    let a2 = find_arg_by_conclusion_and_rule(&store, &formula!(q), "d1").expect("A2: q via d1");
    let a3 = find_arg_by_conclusion_and_rule(&store, &formula!(r), "s1").expect("A3: r via s1");
    let b3 = find_arg_by_conclusion_and_rule(&store, &formula!(!d1), "d3").expect("B3: !d1 via d3");

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

    assert!(
        attack_exists(&attacks, b3, a3, |k| matches!(
            k,
            AttackKind::Undercut { target_sub, rule_id }
                if *target_sub == a2 && rule_id.0 == "d1"
        )),
        "B3 should undercut A3 (indirect, via A2) on rule d1"
    );
}

#[test]
fn test_example_3_7_undermine_attacks() {
    let (store, contrariness) = build_example_3_7();
    let attacks = PairwiseAttackComputer.compute(&store, &contrariness);

    let b1 = find_premise_arg(&store, &formula!(s)).expect("B1: premise s");
    let b2 = find_arg_by_conclusion_and_rule(&store, &formula!(t), "d2").expect("B2: t via d2");
    let b3 = find_arg_by_conclusion_and_rule(&store, &formula!(!d1), "d3").expect("B3: !d1 via d3");
    let c3 = find_arg_by_conclusion_and_rule(&store, &formula!(!s), "s2").expect("C3: !s via s2");
    let e = find_arg_by_conclusion_and_rule(&store, &formula!(!p), "d6").expect("E: !p via d6");
    let a1 = find_premise_arg(&store, &formula!(p)).expect("A1: premise p");

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

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

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

    // C3 undermines E (¬p via d6) indirectly via B1
    assert!(
        attack_exists(&attacks, c3, e, |k| matches!(
            k,
            AttackKind::Undermine { target_premise, .. } if *target_premise == b1
        )),
        "C3 should undermine E via B1"
    );

    // A1 (axiom) is NOT undermined by anything
    let any_undermine_a1 = attacks
        .iter()
        .any(|a| a.target == a1 && matches!(a.kind, AttackKind::Undermine { .. }));
    assert!(!any_undermine_a1, "A1 (axiom) should not be undermined");
}

#[test]
fn test_example_3_7_rebut_attacks() {
    let (store, contrariness) = build_example_3_7();
    let attacks = PairwiseAttackComputer.compute(&store, &contrariness);

    let b2 = find_arg_by_conclusion_and_rule(&store, &formula!(t), "d2").expect("B2: t via d2");
    let b3 = find_arg_by_conclusion_and_rule(&store, &formula!(!d1), "d3").expect("B3: !d1 via d3");
    let d4 = find_arg_by_conclusion_and_rule(&store, &formula!(!t), "d5").expect("D4: !t via d5");
    let a3 = find_arg_by_conclusion_and_rule(&store, &formula!(r), "s1").expect("A3: r via s1");
    let c3 = find_arg_by_conclusion_and_rule(&store, &formula!(!s), "s2").expect("C3: !s via s2");

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

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

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

    // No rebut on A3 (strict top rule s1)
    let any_rebut_on_a3 = attacks
        .iter()
        .any(|a| matches!(&a.kind, AttackKind::Rebut { target_sub, .. } if *target_sub == a3));
    assert!(
        !any_rebut_on_a3,
        "no rebut should target A3 (strict top s1)"
    );

    // No rebut on C3 (strict top rule s2)
    let any_rebut_on_c3 = attacks
        .iter()
        .any(|a| matches!(&a.kind, AttackKind::Rebut { target_sub, .. } if *target_sub == c3));
    assert!(
        !any_rebut_on_c3,
        "no rebut should target C3 (strict top s2)"
    );
}

#[test]
fn test_example_3_7_no_attack_on_axiom_premise() {
    let (store, contrariness) = build_example_3_7();
    let attacks = PairwiseAttackComputer.compute(&store, &contrariness);
    let a1 = find_premise_arg(&store, &formula!(p)).expect("A1: premise p");

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

#[test]
fn test_example_3_7_no_rebut_on_strict_top() {
    let (store, contrariness) = build_example_3_7();
    let attacks = PairwiseAttackComputer.compute(&store, &contrariness);

    let a3 = find_arg_by_conclusion_and_rule(&store, &formula!(r), "s1").expect("A3: r via s1");
    let c3 = find_arg_by_conclusion_and_rule(&store, &formula!(!s), "s2").expect("C3: !s via s2");

    let rebut_targeting_a3 = attacks
        .iter()
        .any(|a| matches!(&a.kind, AttackKind::Rebut { target_sub, .. } if *target_sub == a3));
    assert!(!rebut_targeting_a3, "A3 (strict top s1) cannot be rebutted");

    let rebut_targeting_c3 = attacks
        .iter()
        .any(|a| matches!(&a.kind, AttackKind::Rebut { target_sub, .. } if *target_sub == c3));
    assert!(!rebut_targeting_c3, "C3 (strict top s2) cannot be rebutted");
}

#[test]
fn test_example_3_7_attack_count() {
    let (store, contrariness) = build_example_3_7();
    let attacks = PairwiseAttackComputer.compute(&store, &contrariness);

    // The attack list should be non-empty and every attack should be sound:
    // each attack's kind conditions must actually hold.
    assert!(!attacks.is_empty(), "should have attacks");
    for attack in &attacks {
        let attacker = store.get(attack.attacker).expect("valid attacker");
        let _target = store.get(attack.target).expect("valid target");
        match &attack.kind {
            AttackKind::Rebut { target_sub, .. } => {
                let sub = store.get(*target_sub).expect("valid sub");
                assert!(
                    sub.top_rule().map(|r| r.is_defeasible()).unwrap_or(false),
                    "rebut target_sub must have defeasible top rule"
                );
                assert!(
                    contrariness.is_contrary(sub.conclusion(), attacker.conclusion()),
                    "rebut: attacker conclusion must be contrary to sub conclusion"
                );
            }
            AttackKind::Undermine { target_premise, .. } => {
                let prem_arg = store.get(*target_premise).expect("valid premise arg");
                if let Argument::Premise { premise, .. } = prem_arg {
                    assert!(
                        matches!(premise.kind, PremiseKind::Ordinary),
                        "undermine target must be ordinary or assumption"
                    );
                    assert!(
                        contrariness.is_contrary(&premise.formula, attacker.conclusion()),
                        "undermine: attacker conclusion must be contrary to premise"
                    );
                } else {
                    panic!("undermine target_premise must be a Premise argument");
                }
            }
            AttackKind::Undercut {
                target_sub,
                rule_id: _,
            } => {
                let sub = store.get(*target_sub).expect("valid sub");
                if let Some(Rule::Defeasible(dr)) = sub.top_rule() {
                    let name = dr.name.as_ref().expect("undercut rule must have name");
                    assert!(
                        contrariness.is_contrary(name, attacker.conclusion()),
                        "undercut: attacker conclusion must be contrary to rule name"
                    );
                } else {
                    panic!("undercut target_sub must have defeasible top rule");
                }
            }
        }
    }
}

#[test]
fn test_attack_kind_fields_correct() {
    let (store, contrariness) = build_example_3_7();
    let attacks = PairwiseAttackComputer.compute(&store, &contrariness);

    let a2 = find_arg_by_conclusion_and_rule(&store, &formula!(q), "d1").expect("A2: q via d1");
    let a3 = find_arg_by_conclusion_and_rule(&store, &formula!(r), "s1").expect("A3: r via s1");
    let b1 = find_premise_arg(&store, &formula!(s)).expect("B1: premise s");
    let b2 = find_arg_by_conclusion_and_rule(&store, &formula!(t), "d2").expect("B2: t via d2");
    let b3 = find_arg_by_conclusion_and_rule(&store, &formula!(!d1), "d3").expect("B3: !d1 via d3");
    let c3 = find_arg_by_conclusion_and_rule(&store, &formula!(!s), "s2").expect("C3: !s via s2");
    let d4 = find_arg_by_conclusion_and_rule(&store, &formula!(!t), "d5").expect("D4: !t via d5");

    // B3→A3 undercut: target_sub = A2, rule_id = d1
    let uc = attacks
        .iter()
        .find(|a| {
            a.attacker == b3 && a.target == a3 && matches!(a.kind, AttackKind::Undercut { .. })
        })
        .expect("B3→A3 undercut should exist");
    assert_eq!(
        uc.kind,
        AttackKind::Undercut {
            target_sub: a2,
            rule_id: RuleId("d1".into())
        }
    );

    // C3→B1 undermine: target_premise = B1
    let um = attacks
        .iter()
        .find(|a| {
            a.attacker == c3 && a.target == b1 && matches!(a.kind, AttackKind::Undermine { .. })
        })
        .expect("C3→B1 undermine should exist");
    assert_eq!(
        um.kind,
        AttackKind::Undermine {
            target_premise: b1,
            contrary: false,
        }
    );

    // D4→B3 rebut: target_sub = B2
    let rb = attacks
        .iter()
        .find(|a| a.attacker == d4 && a.target == b3 && matches!(a.kind, AttackKind::Rebut { .. }))
        .expect("D4→B3 rebut should exist");
    assert_eq!(
        rb.kind,
        AttackKind::Rebut {
            target_sub: b2,
            contrary: false
        }
    );
}

// ---
// Example 4.1: strict top rule blocks rebut
// ---

#[test]
fn test_example_4_1_rebut_on_defeasible_sub() {
    let (store, contrariness) = build_example_4_1();
    let attacks = PairwiseAttackComputer.compute(&store, &contrariness);

    let a2 = find_arg_by_conclusion_and_rule(&store, &formula!(married), "d1")
        .expect("A2: married via d1");
    let a3 = find_arg_by_conclusion_and_rule(&store, &formula!(!bachelor), "s1")
        .expect("A3: !bachelor via s1");
    let b2 = find_arg_by_conclusion_and_rule(&store, &formula!(bachelor), "d2")
        .expect("B2: bachelor via d2");
    let b3 = find_arg_by_conclusion_and_rule(&store, &formula!(!married), "s2")
        .expect("B3: !married via s2");

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

    // A3 rebuts B2 directly
    assert!(
        attack_exists(&attacks, a3, b2, |k| matches!(
            k, AttackKind::Rebut { target_sub, .. } if *target_sub == b2
        )),
        "A3 should rebut B2 directly"
    );

    // B3 rebuts A3 on A2 (defeasible sub)
    assert!(
        attack_exists(&attacks, b3, a3, |k| matches!(
            k, AttackKind::Rebut { target_sub, .. } if *target_sub == a2
        )),
        "B3 should rebut A3 on sub-arg A2"
    );

    // B3 rebuts A2 directly
    assert!(
        attack_exists(&attacks, b3, a2, |k| matches!(
            k, AttackKind::Rebut { target_sub, .. } if *target_sub == a2
        )),
        "B3 should rebut A2 directly"
    );
}

#[test]
fn test_example_4_1_no_rebut_on_strict_top() {
    let (store, contrariness) = build_example_4_1();
    let attacks = PairwiseAttackComputer.compute(&store, &contrariness);

    let a3 = find_arg_by_conclusion_and_rule(&store, &formula!(!bachelor), "s1")
        .expect("A3: !bachelor via s1");
    let b2 = find_arg_by_conclusion_and_rule(&store, &formula!(bachelor), "d2")
        .expect("B2: bachelor via d2");
    let a2 = find_arg_by_conclusion_and_rule(&store, &formula!(married), "d1")
        .expect("A2: married via d1");
    let b3 = find_arg_by_conclusion_and_rule(&store, &formula!(!married), "s2")
        .expect("B3: !married via s2");

    // A2 does NOT rebut B3 (B3's top rule s2 is strict)
    assert!(
        !attack_exists(&attacks, a2, b3, |k| matches!(k, AttackKind::Rebut { .. })),
        "A2 should NOT rebut B3 (strict top s2)"
    );

    // B2 does NOT rebut A3 (A3's top rule s1 is strict)
    assert!(
        !attack_exists(&attacks, b2, a3, |k| matches!(k, AttackKind::Rebut { .. })),
        "B2 should NOT rebut A3 (strict top s1)"
    );
}

#[test]
fn test_example_4_1_no_undermine_across_domains() {
    let (store, contrariness) = build_example_4_1();
    let attacks = PairwiseAttackComputer.compute(&store, &contrariness);

    let a1 = find_premise_arg(&store, &formula!(wearsring)).expect("A1: premise wearsring");
    let a3 = find_arg_by_conclusion_and_rule(&store, &formula!(!bachelor), "s1")
        .expect("A3: !bachelor via s1");
    let b1 = find_premise_arg(&store, &formula!(partyanimal)).expect("B1: premise partyanimal");
    let b3 = find_arg_by_conclusion_and_rule(&store, &formula!(!married), "s2")
        .expect("B3: !married via s2");

    // A3 (¬Bachelor) does NOT undermine B1 (PartyAnimal)
    assert!(
        !attack_exists(&attacks, a3, b1, |k| matches!(
            k,
            AttackKind::Undermine { .. }
        )),
        "A3 should NOT undermine B1 (unrelated formula)"
    );

    // B3 (¬Married) does NOT undermine A1 (WearsRing)
    assert!(
        !attack_exists(&attacks, b3, a1, |k| matches!(
            k,
            AttackKind::Undermine { .. }
        )),
        "B3 should NOT undermine A1 (unrelated formula)"
    );
}

// ---
// Assumption premises are attackable via undermine
// ---

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

    let grounded = NaiveGrounder.ground(&system).unwrap();
    let store = ForwardChainingConstructor.construct(&grounded);
    let attacks = PairwiseAttackComputer.compute(&store, &grounded.contrariness);

    let prem_a = find_premise_arg(&store, &formula!(a)).expect("premise a");

    let has_undermine = attacks.iter().any(|atk| {
        matches!(&atk.kind, AttackKind::Undermine { target_premise, .. } if *target_premise == prem_a)
    });
    assert!(
        has_undermine,
        "ordinary premise should be undermined by argument concluding ¬a"
    );
}

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

    let grounded = NaiveGrounder.ground(&system).unwrap();
    let store = ForwardChainingConstructor.construct(&grounded);
    let attacks = PairwiseAttackComputer.compute(&store, &grounded.contrariness);

    let prem_a = find_premise_arg(&store, &formula!(a)).expect("premise a");

    let has_undermine = attacks.iter().any(|atk| {
        matches!(&atk.kind, AttackKind::Undermine { target_premise, .. } if *target_premise == prem_a)
    });
    assert!(!has_undermine, "axiom premise should NOT be undermined");
}

// ---
// Unnamed defeasible rules cannot be undercut
// ---

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

    let grounded = NaiveGrounder.ground(&system).unwrap();
    let store = ForwardChainingConstructor.construct(&grounded);
    let attacks = PairwiseAttackComputer.compute(&store, &grounded.contrariness);

    let undercuts: Vec<_> = attacks
        .iter()
        .filter(|a| matches!(a.kind, AttackKind::Undercut { .. }))
        .collect();
    assert!(
        undercuts.is_empty(),
        "unnamed defeasible rule should not be undercut, found {undercuts:?}"
    );
}

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

    let grounded = NaiveGrounder.ground(&system).unwrap();
    let store = ForwardChainingConstructor.construct(&grounded);
    let attacks = PairwiseAttackComputer.compute(&store, &grounded.contrariness);

    let undercuts: Vec<_> = attacks
        .iter()
        .filter(|a| matches!(a.kind, AttackKind::Undercut { .. }))
        .collect();
    assert!(
        !undercuts.is_empty(),
        "named defeasible rule should be undercut"
    );
}

// ---
// Pairwise / indexed equivalence
// ---

#[test]
fn test_pairwise_indexed_equivalence_example_3_7() {
    let (store, contrariness) = build_example_3_7();

    let mut pairwise = PairwiseAttackComputer.compute(&store, &contrariness);
    let mut indexed = IndexedAttackComputer.compute(&store, &contrariness);

    pairwise.sort_by_key(attack_key);
    indexed.sort_by_key(attack_key);

    assert_eq!(
        pairwise.len(),
        indexed.len(),
        "pairwise and indexed should produce same number of attacks"
    );

    for (p, i) in pairwise.iter().zip(indexed.iter()) {
        assert_eq!(attack_key(p), attack_key(i), "attack mismatch");
    }
}

#[test]
fn test_pairwise_indexed_equivalence_example_4_1() {
    let (store, contrariness) = build_example_4_1();

    let mut pairwise = PairwiseAttackComputer.compute(&store, &contrariness);
    let mut indexed = IndexedAttackComputer.compute(&store, &contrariness);

    pairwise.sort_by_key(attack_key);
    indexed.sort_by_key(attack_key);

    assert_eq!(pairwise.len(), indexed.len());
    for (p, i) in pairwise.iter().zip(indexed.iter()) {
        assert_eq!(attack_key(p), attack_key(i), "attack mismatch");
    }
}

// ---
// Edge cases
// ---

#[test]
fn test_empty_store_no_attacks() {
    let store = ArgumentStore::new();
    let contrariness = ContrarinessFunction::new().with_classical_negation();
    let attacks = PairwiseAttackComputer.compute(&store, &contrariness);
    assert!(attacks.is_empty(), "empty store should produce no attacks");
}

#[test]
fn test_axiom_only_no_attacks() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .axiom(formula!(a))
        .axiom(formula!(b))
        .axiom(formula!(c))
        .build();
    let grounded = NaiveGrounder.ground(&system).unwrap();
    let store = ForwardChainingConstructor.construct(&grounded);
    let attacks = PairwiseAttackComputer.compute(&store, &grounded.contrariness);
    assert!(
        attacks.is_empty(),
        "axiom-only system should produce no attacks"
    );
}

#[test]
fn test_self_attack() {
    // ordinary premise `a` + defeasible rule a ⇒ ¬a
    // The argument for ¬a undermines the premise argument for a,
    // and a is a sub-argument of the ¬a argument, so it's a self-undermining.
    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .ordinary_premise(formula!(a))
        .named_defeasible_rule("d1", formula!(d1), vec![formula!(a)], formula!(!a))
        .build();

    let grounded = NaiveGrounder.ground(&system).unwrap();
    let store = ForwardChainingConstructor.construct(&grounded);
    let attacks = PairwiseAttackComputer.compute(&store, &grounded.contrariness);

    let neg_a_arg =
        find_arg_by_conclusion_and_rule(&store, &formula!(!a), "d1").expect("!a via d1");
    let prem_a = find_premise_arg(&store, &formula!(a)).expect("premise a");

    // The argument for ¬a should undermine prem(a), and since prem(a) is a
    // sub-argument of the ¬a argument, this creates a self-attack.
    let self_undermine = attacks.iter().any(|atk| {
        atk.attacker == neg_a_arg
            && atk.target == neg_a_arg
            && matches!(&atk.kind, AttackKind::Undermine { target_premise, .. } if *target_premise == prem_a)
    });
    assert!(self_undermine, "self-undermining attack should be reported");
}

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

    let grounded = NaiveGrounder.ground(&system).unwrap();
    let store = ForwardChainingConstructor.construct(&grounded);

    // Use a bare contrariness function with nothing declared, no classical negation
    let empty_cf = ContrarinessFunction::new();
    let attacks = PairwiseAttackComputer.compute(&store, &empty_cf);

    assert!(
        attacks.is_empty(),
        "no contrariness entries + no classical negation = no attacks"
    );
}

// ---
// Contrary vs contradictory defeat semantics
// ---

/// Contrary defeat bypasses preference.
///
/// Setup: a ⇒_d1 φ and b ⇒_d2 ψ. φ is a contrary of ψ (asymmetric).
/// Ordering: d2 > d1 (B2 is strictly preferred).
/// Despite A1 being weaker, its attack on B2 succeeds as defeat because
/// contrary attacks bypass the preference check.
#[test]
fn contrary_defeat_bypasses_preference() {
    let phi = formula!(phi);
    let psi = formula!(psi);
    let f_a = formula!(a);
    let f_b = formula!(b);

    let (system, _) = AspicSystemBuilder::new()
        .ordinary_premise(f_a.clone())
        .ordinary_premise(f_b.clone())
        .defeasible_rule("d1", vec![f_a], phi.clone())
        .defeasible_rule("d2", vec![f_b], psi.clone())
        .contrary(psi.clone(), phi.clone())
        .build();

    let grounder = NaiveGrounder;
    let grounded = grounder.ground(&system).expect("grounding");
    let constructor = ForwardChainingConstructor;
    let store = constructor.construct(&grounded);
    let attacks = PairwiseAttackComputer.compute(&store, &grounded.contrariness);

    let a1 = store
        .all_arguments()
        .find(|(_, a)| *a.conclusion() == phi)
        .map(|(id, _)| id)
        .expect("A1 concluding phi");
    let b2 = store
        .all_arguments()
        .find(|(_, a)| *a.conclusion() == psi)
        .map(|(id, _)| id)
        .expect("B2 concluding psi");

    let attack_on_b2 = attacks
        .iter()
        .find(|atk| atk.attacker == a1 && atk.target == b2);
    assert!(
        attack_on_b2.is_some(),
        "A1 should attack B2 (contrary of psi)"
    );

    let kind = &attack_on_b2.unwrap().kind;
    match kind {
        AttackKind::Rebut { contrary, .. } => {
            assert!(contrary, "rebut via contrary should have contrary=true");
        }
        other => panic!("Expected Rebut, got {other:?}"),
    }

    let rule_ord = pickaxe_rs::system::ordering::TieredOrdering::new(vec![
        vec![RuleId("d2".into())],
        vec![RuleId("d1".into())],
    ]);
    let ordering = LastLinkOrdering {
        rule_ordering: Box::new(rule_ord),
        premise_ordering: Box::new(NoPreference),
        lifting: LiftingStrategy::Elitist,
    };

    assert_eq!(
        ordering.compare(a1, b2, &store),
        Preference::StrictlyDispreferred,
        "A1 should be strictly dispreferred to B2 (d1 < d2)"
    );

    let evaluator = ClassicalEvaluator {
        semantics_solver: Box::new(NaiveEnumerationSolver),
    };
    let pref = PreferenceConfig::ArgumentOrdering(Box::new(ordering));
    let result = evaluator
        .evaluate(&store, &attacks, Semantics::Grounded, &pref)
        .unwrap();
    let lab = &result.labellings[0];

    assert_eq!(
        lab.label_of(a1),
        Label::In,
        "A1 should be In: no attack on A1 from B2 (contrary is asymmetric)"
    );
    assert_eq!(
        lab.label_of(b2),
        Label::Out,
        "B2 should be Out: contrary defeat bypasses preference"
    );
}

/// Contradictory defeat is subject to preference.
///
/// Same setup as `contrary_defeat_bypasses_preference` but φ and ψ are
/// contradictories (symmetric). A1 is strictly dispreferred to B2, so
/// A1's attack on B2 does NOT succeed as defeat. But B2's attack on A1 does.
#[test]
fn contradictory_defeat_subject_to_preference() {
    let phi = formula!(phi);
    let psi = formula!(psi);
    let f_a = formula!(a);
    let f_b = formula!(b);

    let (system, _) = AspicSystemBuilder::new()
        .ordinary_premise(f_a.clone())
        .ordinary_premise(f_b.clone())
        .defeasible_rule("d1", vec![f_a], phi.clone())
        .defeasible_rule("d2", vec![f_b], psi.clone())
        .contradictory(psi.clone(), phi.clone())
        .build();

    let grounder = NaiveGrounder;
    let grounded = grounder.ground(&system).expect("grounding");
    let constructor = ForwardChainingConstructor;
    let store = constructor.construct(&grounded);
    let attacks = PairwiseAttackComputer.compute(&store, &grounded.contrariness);

    let a1 = store
        .all_arguments()
        .find(|(_, a)| *a.conclusion() == phi)
        .map(|(id, _)| id)
        .expect("A1 concluding phi");
    let b2 = store
        .all_arguments()
        .find(|(_, a)| *a.conclusion() == psi)
        .map(|(id, _)| id)
        .expect("B2 concluding psi");

    let attack_a1_on_b2 = attacks
        .iter()
        .find(|atk| atk.attacker == a1 && atk.target == b2);
    assert!(attack_a1_on_b2.is_some(), "A1 should attack B2");
    match &attack_a1_on_b2.unwrap().kind {
        AttackKind::Rebut { contrary, .. } => {
            assert!(!contrary, "contradictory rebut should have contrary=false");
        }
        other => panic!("Expected Rebut, got {other:?}"),
    }

    let rule_ord = pickaxe_rs::system::ordering::TieredOrdering::new(vec![
        vec![RuleId("d2".into())],
        vec![RuleId("d1".into())],
    ]);
    let ordering = LastLinkOrdering {
        rule_ordering: Box::new(rule_ord),
        premise_ordering: Box::new(NoPreference),
        lifting: LiftingStrategy::Elitist,
    };

    let evaluator = ClassicalEvaluator {
        semantics_solver: Box::new(NaiveEnumerationSolver),
    };
    let pref = PreferenceConfig::ArgumentOrdering(Box::new(ordering));
    let result = evaluator
        .evaluate(&store, &attacks, Semantics::Grounded, &pref)
        .unwrap();
    let lab = &result.labellings[0];

    assert_eq!(
        lab.label_of(b2),
        Label::In,
        "B2 should be In: A1 is dispreferred, so A1's attack on B2 does NOT succeed as defeat"
    );
    assert_eq!(
        lab.label_of(a1),
        Label::Out,
        "A1 should be Out: B2's attack on A1 succeeds (B2 is not dispreferred)"
    );
}
