//! Integration tests for ASPIC+ instantiation patterns from Modgil &
//! Prakken (2014) §4–5: witness testimony, negation as failure, material
//! implications, classical-logic strict rules, and systems without
//! defeasible rules.

use std::collections::BTreeSet;

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

mod common;

use common::*;

// --- Witness testimony — argument schemes with undercutters (§4.3) ---

/// Build the §4.3 witness testimony system.
///
/// Bob claims John was in Holland Park. Jan claims John was in Amsterdam.
/// Bob's memory is questioned (distorted). Jan's credibility is questioned.
/// Argument schemes: position-to-know (dw), memory (dm), perception (dp).
/// Undercutters: memory undercutter (um), credibility undercutter (uw).
fn build_witness_testimony_system() -> AspicSystem {
    let (system, _) = AspicSystemBuilder::new()
        .with_classical_negation()
        // Axioms
        .axiom(formula!(ptk_bob))
        .axiom(formula!(says_bob))
        .axiom(formula!(sees_pictures_bob))
        .axiom(formula!(ptk_jan))
        .axiom(formula!(says_jan))
        .axiom(formula!(friends_jan_john))
        .axiom(formula!(suspected_robber_john))
        .axiom(formula!(involved_john_jan))
        // Defeasible rules — argument scheme instances
        .named_defeasible_rule(
            "dw_bob",
            formula!(dw_bob),
            vec![formula!(ptk_bob), formula!(says_bob)],
            formula!(recalls_bob),
        )
        .named_defeasible_rule(
            "dm_bob",
            formula!(dm_bob),
            vec![formula!(recalls_bob)],
            formula!(sees_bob_hp),
        )
        .named_defeasible_rule(
            "dp_bob",
            formula!(dp_bob),
            vec![formula!(sees_bob_hp)],
            formula!(in_hp),
        )
        .named_defeasible_rule(
            "dw_jan",
            formula!(dw_jan),
            vec![formula!(ptk_jan), formula!(says_jan)],
            formula!(recalls_jan),
        )
        .named_defeasible_rule(
            "dm_jan",
            formula!(dm_jan),
            vec![formula!(recalls_jan)],
            formula!(sees_jan_ams),
        )
        .named_defeasible_rule(
            "dp_jan",
            formula!(dp_jan),
            vec![formula!(sees_jan_ams)],
            formula!(in_ams),
        )
        // Undercutters
        .named_defeasible_rule(
            "um_bob",
            formula!(um_bob),
            vec![formula!(distorted_bob)],
            formula!(!dm_bob),
        )
        .named_defeasible_rule(
            "uw_jan",
            formula!(uw_jan),
            vec![formula!(!credible_jan)],
            formula!(!dw_jan),
        )
        // Strict rules — modus ponens instances for material implications
        .strict_rule(
            "s_f4",
            vec![formula!(sees_pictures_bob)],
            formula!(distorted_bob),
        )
        .strict_rule("s_f5", vec![formula!(in_hp)], formula!(in_london))
        .strict_rule("s_f12a", vec![formula!(in_london)], formula!(!in_ams))
        .strict_rule("s_f12b", vec![formula!(in_ams)], formula!(!in_hp))
        .strict_rule(
            "s_f10",
            vec![
                formula!(friends_jan_john),
                formula!(suspected_robber_john),
                formula!(involved_john_jan),
            ],
            formula!(!credible_jan),
        )
        .build();
    system
}

/// §4.3: All expected inference arguments exist with correct conclusions.
#[test]
fn test_witness_testimony_argument_construction() {
    let pipeline =
        AspicPipeline::classical(build_witness_testimony_system(), Box::new(EqualOrdering));
    let result = pipeline.evaluate(Semantics::Grounded).unwrap();
    let store = &result.store;

    // Bob's testimony chain: A3 → A4 → A5 → A7 → A8
    let a3 = find_arg_by_conclusion_and_rule(store, &formula!(recalls_bob), "dw_bob")
        .expect("A3: recalls_bob via dw_bob");
    find_arg_by_conclusion_and_rule(store, &formula!(sees_bob_hp), "dm_bob")
        .expect("A4: sees_bob_hp via dm_bob");
    let a5 = find_arg_by_conclusion_and_rule(store, &formula!(in_hp), "dp_bob")
        .expect("A5: in_hp via dp_bob");
    find_arg_by_conclusion_and_rule(store, &formula!(in_london), "s_f5")
        .expect("A7: in_london via s_f5");
    find_arg_by_conclusion_and_rule(store, &formula!(!in_ams), "s_f12a")
        .expect("A8: ¬in_ams via s_f12a");

    // Bob's undercutter: B3 → B4
    find_arg_by_conclusion_and_rule(store, &formula!(distorted_bob), "s_f4")
        .expect("B3: distorted_bob via s_f4");
    find_arg_by_conclusion_and_rule(store, &formula!(!dm_bob), "um_bob")
        .expect("B4: ¬dm_bob via um_bob");

    // Jan's testimony chain: C3 → C4 → C5 → C8
    let c3 = find_arg_by_conclusion_and_rule(store, &formula!(recalls_jan), "dw_jan")
        .expect("C3: recalls_jan via dw_jan");
    find_arg_by_conclusion_and_rule(store, &formula!(sees_jan_ams), "dm_jan")
        .expect("C4: sees_jan_ams via dm_jan");
    find_arg_by_conclusion_and_rule(store, &formula!(in_ams), "dp_jan")
        .expect("C5: in_ams via dp_jan");
    find_arg_by_conclusion_and_rule(store, &formula!(!in_hp), "s_f12b")
        .expect("C8: ¬in_hp via s_f12b");

    // Jan's undercutter: D4 → D5
    find_arg_by_conclusion_and_rule(store, &formula!(!credible_jan), "s_f10")
        .expect("D4: ¬credible_jan via s_f10");
    find_arg_by_conclusion_and_rule(store, &formula!(!dw_jan), "uw_jan")
        .expect("D5: ¬dw_jan via uw_jan");

    // Structural checks
    assert!(
        !store.get(a3).unwrap().is_strict(store),
        "A3 uses defeasible dw_bob"
    );
    assert!(
        !store.get(a5).unwrap().is_strict(store),
        "A5 chain includes defeasible rules"
    );
    assert!(
        a3.0 != c3.0,
        "Bob's and Jan's chains are distinct arguments"
    );
}

/// §4.3: All expected attack relations hold.
#[test]
fn test_witness_testimony_attack_relations() {
    let pipeline =
        AspicPipeline::classical(build_witness_testimony_system(), Box::new(EqualOrdering));
    let result = pipeline.evaluate(Semantics::Grounded).unwrap();
    let store = &result.store;
    let attacks = &result.attacks;

    let a4 = find_arg_by_conclusion_and_rule(store, &formula!(sees_bob_hp), "dm_bob").unwrap();
    let a5 = find_arg_by_conclusion_and_rule(store, &formula!(in_hp), "dp_bob").unwrap();
    let a7 = find_arg_by_conclusion_and_rule(store, &formula!(in_london), "s_f5").unwrap();
    let a8 = find_arg_by_conclusion_and_rule(store, &formula!(!in_ams), "s_f12a").unwrap();
    let b4 = find_arg_by_conclusion_and_rule(store, &formula!(!dm_bob), "um_bob").unwrap();
    let c3 = find_arg_by_conclusion_and_rule(store, &formula!(recalls_jan), "dw_jan").unwrap();
    let c4 = find_arg_by_conclusion_and_rule(store, &formula!(sees_jan_ams), "dm_jan").unwrap();
    let c5 = find_arg_by_conclusion_and_rule(store, &formula!(in_ams), "dp_jan").unwrap();
    let c8 = find_arg_by_conclusion_and_rule(store, &formula!(!in_hp), "s_f12b").unwrap();
    let d5 = find_arg_by_conclusion_and_rule(store, &formula!(!dw_jan), "uw_jan").unwrap();

    // B4 undercuts A4 on dm_bob — propagates to A5, A7, A8
    for &target in &[a4, a5, a7, a8] {
        assert!(
            attack_exists(attacks, b4, target, |k| matches!(
                k,
                AttackKind::Undercut { target_sub, .. } if *target_sub == a4
            )),
            "B4 should undercut {target:?} on sub-arg A4 (dm_bob)"
        );
    }

    // C8 rebuts A5 on in_hp — propagates to A7, A8
    for &target in &[a5, a7, a8] {
        assert!(
            attack_exists(attacks, c8, target, |k| matches!(
                k,
                AttackKind::Rebut { target_sub, .. } if *target_sub == a5
            )),
            "C8 should rebut {target:?} on sub-arg A5 (in_hp)"
        );
    }

    // D5 undercuts C3 on dw_jan — propagates to C4, C5, C8
    for &target in &[c3, c4, c5, c8] {
        assert!(
            attack_exists(attacks, d5, target, |k| matches!(
                k,
                AttackKind::Undercut { target_sub, .. } if *target_sub == c3
            )),
            "D5 should undercut {target:?} on sub-arg C3 (dw_jan)"
        );
    }

    // A8 rebuts C5 on in_ams — propagates to C8
    for &target in &[c5, c8] {
        assert!(
            attack_exists(attacks, a8, target, |k| matches!(
                k,
                AttackKind::Rebut { target_sub, .. } if *target_sub == c5
            )),
            "A8 should rebut {target:?} on sub-arg C5 (in_ams)"
        );
    }
}

/// §4.3: With both undercutters present, neither testimony is justified.
#[test]
fn test_witness_testimony_extensions() {
    let system = build_witness_testimony_system();

    let grounded = AspicPipeline::classical(system.clone(), Box::new(EqualOrdering))
        .evaluate(Semantics::Grounded)
        .unwrap();
    let g_conc = conclusions_in(&grounded.extensions[0], &grounded.store);

    assert!(
        !g_conc.contains(&formula!(in_hp)),
        "in_hp NOT justified (Bob's chain undercut by B4)"
    );
    assert!(
        !g_conc.contains(&formula!(in_ams)),
        "in_ams NOT justified (Jan's chain undercut by D5)"
    );
    assert!(
        !g_conc.contains(&formula!(in_london)),
        "in_london NOT justified (depends on in_hp)"
    );
    assert!(
        g_conc.contains(&formula!(!dm_bob)),
        "¬dm_bob justified (B4 is unattacked)"
    );
    assert!(
        g_conc.contains(&formula!(!dw_jan)),
        "¬dw_jan justified (D5 is unattacked)"
    );

    let preferred = AspicPipeline::classical(system, Box::new(EqualOrdering))
        .evaluate(Semantics::Preferred)
        .unwrap();

    for ext in &preferred.extensions {
        let c = conclusions_in(ext, &preferred.store);
        assert!(
            !c.contains(&formula!(in_hp)),
            "in_hp not in any preferred extension"
        );
        assert!(
            !c.contains(&formula!(in_ams)),
            "in_ams not in any preferred extension"
        );
    }
}

// --- Negation as failure (§5) ---

/// Build the modified Example 3.7 from §5.
///
/// d4 (u ⇒ v) is replaced by d4' (naf_u ⇒ v). The premise ∼u (encoded as
/// `naf_u`) is an ordinary premise whose contrary is u — meaning u attacks
/// naf_u but not vice versa.
fn build_negation_as_failure_system() -> AspicSystem {
    let (system, _) = AspicSystemBuilder::new()
        .with_classical_negation()
        .contrary(formula!(naf_u), formula!(u))
        .axiom(formula!(p))
        .ordinary_premise(formula!(s))
        .ordinary_premise(formula!(naf_u))
        .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!(naf_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();
    system
}

/// §5: u contrary-undermines arguments built on the ∼u (naf_u) premise.
#[test]
fn test_negation_as_failure_contrary_attack() {
    let pipeline =
        AspicPipeline::classical(build_negation_as_failure_system(), Box::new(EqualOrdering));
    let result = pipeline.evaluate(Semantics::Grounded).unwrap();
    let store = &result.store;
    let attacks = &result.attacks;

    let c1 = find_premise_arg(store, &formula!(u)).expect("C1: premise u");
    let e = find_premise_arg(store, &formula!(naf_u)).expect("E: premise naf_u");
    let c2_prime =
        find_arg_by_conclusion_and_rule(store, &formula!(v), "d4").expect("C2': v via d4");

    // C1 (u) contrary-undermines E (naf_u) with contrary=true
    assert!(
        attack_exists(attacks, c1, e, |k| matches!(
            k,
            AttackKind::Undermine { target_premise, contrary }
                if *target_premise == e && *contrary
        )),
        "C1 should contrary-undermine E (naf_u premise)"
    );

    // The attack propagates to C2' (which has E as sub-argument)
    assert!(
        attack_exists(attacks, c1, c2_prime, |k| matches!(
            k,
            AttackKind::Undermine { target_premise, contrary }
                if *target_premise == e && *contrary
        )),
        "C1 should contrary-undermine C2' on E"
    );
}

/// §5: Contrary-undermine defeats bypass preferences.
#[test]
fn test_negation_as_failure_defeats_bypass_preferences() {
    /// Ordering that makes the u-premise argument strictly dispreferred.
    #[derive(Debug)]
    struct UWeakerOrdering;
    impl ArgumentOrdering for UWeakerOrdering {
        fn compare(&self, a: ArgumentId, _b: ArgumentId, store: &ArgumentStore) -> Preference {
            let a_is_u = store
                .get(a)
                .map(|arg| *arg.conclusion() == formula!(u))
                .unwrap_or(false);
            if a_is_u {
                Preference::StrictlyDispreferred
            } else {
                Preference::Equal
            }
        }
    }

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

    let c1 = find_premise_arg(store, &formula!(u)).unwrap();
    let e = find_premise_arg(store, &formula!(naf_u)).unwrap();
    let c2_prime = find_arg_by_conclusion_and_rule(store, &formula!(v), "d4").unwrap();

    let defeats = compute_defeats(&result.attacks, store, &UWeakerOrdering);

    assert!(
        defeat_exists(&defeats, c1, e),
        "C1→E contrary-undermine succeeds as defeat even when C1 is strictly dispreferred"
    );
    assert!(
        defeat_exists(&defeats, c1, c2_prime),
        "C1→C2' contrary-undermine succeeds as defeat even when C1 is strictly dispreferred"
    );
}

/// §5: The contrary relation is asymmetric — naf_u does NOT attack u.
#[test]
fn test_negation_as_failure_asymmetric_direction() {
    let pipeline =
        AspicPipeline::classical(build_negation_as_failure_system(), Box::new(EqualOrdering));
    let result = pipeline.evaluate(Semantics::Grounded).unwrap();
    let attacks = &result.attacks;
    let store = &result.store;

    let c1 = find_premise_arg(store, &formula!(u)).unwrap();
    let e = find_premise_arg(store, &formula!(naf_u)).unwrap();

    let e_attacks_c1 = attacks.iter().any(|a| a.attacker == e && a.target == c1);
    assert!(
        !e_attacks_c1,
        "naf_u should NOT attack u (contrary is asymmetric: u attacks naf_u only)"
    );

    let any_attack_on_c1_from_naf = attacks.iter().any(|a| a.target == c1 && a.attacker == e);
    assert!(
        !any_attack_on_c1_from_naf,
        "no attack from naf_u premise on u premise"
    );
}

// --- The Tweety Triangle — material implications (§4.5) ---

/// §4.5: Classical-logic variant with material implications and normality
/// assumptions. penguin ⊃ ab1 produces ab1 which undermines ¬ab1,
/// killing the canfly argument. ¬canfly is justified.
#[test]
fn test_tweety_material_implications() {
    let bird_and_nab1_implies_canfly = Formula::Implies(
        Box::new(Formula::And(vec![formula!(bird), formula!(!ab1)])),
        Box::new(formula!(canfly)),
    );
    let penguin_and_nab2_implies_not_canfly = Formula::Implies(
        Box::new(Formula::And(vec![formula!(penguin), formula!(!ab2)])),
        Box::new(formula!(!canfly)),
    );
    let penguin_implies_bird =
        Formula::Implies(Box::new(formula!(penguin)), Box::new(formula!(bird)));
    let penguin_implies_ab1 =
        Formula::Implies(Box::new(formula!(penguin)), Box::new(formula!(ab1)));

    let (system, _) = AspicSystemBuilder::new()
        .with_classical_negation()
        // Axioms (Kn)
        .axiom(bird_and_nab1_implies_canfly.clone())
        .axiom(penguin_and_nab2_implies_not_canfly.clone())
        .axiom(penguin_implies_bird.clone())
        .axiom(penguin_implies_ab1.clone())
        .axiom(formula!(penguin))
        // Ordinary premises (Kp) — normality assumptions
        .ordinary_premise(formula!(!ab1))
        .ordinary_premise(formula!(!ab2))
        // Strict rules — modus ponens for each implication
        .strict_rule(
            "mp1",
            vec![formula!(bird), formula!(!ab1), bird_and_nab1_implies_canfly],
            formula!(canfly),
        )
        .strict_rule(
            "mp2",
            vec![
                formula!(penguin),
                formula!(!ab2),
                penguin_and_nab2_implies_not_canfly,
            ],
            formula!(!canfly),
        )
        .strict_rule(
            "mp3",
            vec![formula!(penguin), penguin_implies_bird],
            formula!(bird),
        )
        .strict_rule(
            "mp4",
            vec![formula!(penguin), penguin_implies_ab1],
            formula!(ab1),
        )
        .build();

    // Use NoPreference for premises because TieredOrdering penalises
    // formulas absent from tiers (axiom premises like penguin ⊃ ab1),
    // which would incorrectly block the ab1 undermine on ¬ab1.
    // The paper's ¬ab1 <' ¬ab2 ordering matters only when there is
    // a competing attack on ¬ab2 (via modus tollens, not encoded here).
    let ordering = LastLinkOrdering {
        rule_ordering: Box::new(NoPreference),
        premise_ordering: Box::new(NoPreference),
        lifting: LiftingStrategy::Elitist,
    };
    let result = AspicPipeline::classical(system, Box::new(ordering))
        .evaluate(Semantics::Grounded)
        .unwrap();
    let conc = conclusions_in(&result.extensions[0], &result.store);

    assert!(
        conc.contains(&formula!(!canfly)),
        "¬canfly should be justified"
    );
    assert!(
        !conc.contains(&formula!(canfly)),
        "canfly should NOT be justified (¬ab1 undermined by ab1)"
    );
    assert!(
        conc.contains(&formula!(penguin)),
        "penguin should be justified (axiom)"
    );
    assert!(
        conc.contains(&formula!(bird)),
        "bird should be justified (from penguin ⊃ bird)"
    );
    assert!(
        conc.contains(&formula!(ab1)),
        "ab1 should be justified (from penguin ⊃ ab1)"
    );
}

// --- Classical-logic strict rules — material implication (§4.1.2) ---

/// §4.1.2: Material-implication variant of Example 4.1 (Bachelor/Married).
/// Domain-specific strict rules are replaced by a material implication axiom
/// plus modus ponens and modus tollens.
#[test]
fn test_bachelor_married_material_implication() {
    let married_implies_not_bachelor =
        Formula::Implies(Box::new(formula!(Married)), Box::new(formula!(!Bachelor)));

    let (system, _) = AspicSystemBuilder::new()
        .with_classical_negation()
        .ordinary_premise(formula!(WearsRing))
        .ordinary_premise(formula!(PartyAnimal))
        .axiom(married_implies_not_bachelor.clone())
        // Modus ponens: Married, (Married ⊃ ¬Bachelor) → ¬Bachelor
        .strict_rule(
            "mp",
            vec![formula!(Married), married_implies_not_bachelor.clone()],
            formula!(!Bachelor),
        )
        // Modus tollens: Bachelor, (Married ⊃ ¬Bachelor) → ¬Married
        .strict_rule(
            "mt",
            vec![formula!(Bachelor), married_implies_not_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 store_for_ids = {
        let r = AspicPipeline::classical(system.clone(), Box::new(EqualOrdering))
            .evaluate(Semantics::Grounded)
            .unwrap();
        let s = &r.store;

        let a2 = find_arg_by_conclusion_and_rule(s, &formula!(Married), "d1")
            .expect("A2: Married via d1");
        let b2 = find_arg_by_conclusion_and_rule(s, &formula!(Bachelor), "d2")
            .expect("B2: Bachelor via d2");
        let a4 = find_arg_by_conclusion_and_rule(s, &formula!(!Bachelor), "mp")
            .expect("A4: ¬Bachelor via mp");
        let b4 = find_arg_by_conclusion_and_rule(s, &formula!(!Married), "mt")
            .expect("B4: ¬Married via mt");

        let attacks = &r.attacks;

        // A4 (¬Bachelor) rebuts B2 (Bachelor via defeasible d2)
        assert!(
            attack_exists(attacks, a4, b2, |k| matches!(
                k,
                AttackKind::Rebut { target_sub, .. } if *target_sub == b2
            )),
            "A4 should rebut B2 on B2"
        );
        // A4 rebuts B4 on B2 (B4 has B2 as sub-argument)
        assert!(
            attack_exists(attacks, a4, b4, |k| matches!(
                k,
                AttackKind::Rebut { target_sub, .. } if *target_sub == b2
            )),
            "A4 should rebut B4 on sub-arg B2"
        );
        // B4 (¬Married) rebuts A2 (Married via defeasible d1)
        assert!(
            attack_exists(attacks, b4, a2, |k| matches!(
                k,
                AttackKind::Rebut { target_sub, .. } if *target_sub == a2
            )),
            "B4 should rebut A2 on A2"
        );
        // B4 rebuts A4 on A2 (A4 has A2 as sub-argument)
        assert!(
            attack_exists(attacks, b4, a4, |k| matches!(
                k,
                AttackKind::Rebut { target_sub, .. } if *target_sub == a2
            )),
            "B4 should rebut A4 on sub-arg A2"
        );

        (a2, b2, a4, b4)
    };
    let _ = store_for_ids;

    // Under equal preferences: mutual defeat → two preferred extensions
    let grounded = AspicPipeline::classical(system.clone(), Box::new(EqualOrdering))
        .evaluate(Semantics::Grounded)
        .unwrap();
    let g_conc = conclusions_in(&grounded.extensions[0], &grounded.store);
    assert!(
        !g_conc.contains(&formula!(Married)),
        "Grounded: Married NOT justified (mutual defeat)"
    );
    assert!(
        !g_conc.contains(&formula!(Bachelor)),
        "Grounded: Bachelor NOT justified (mutual defeat)"
    );

    let preferred = AspicPipeline::classical(system, Box::new(EqualOrdering))
        .evaluate(Semantics::Preferred)
        .unwrap();
    assert_eq!(
        preferred.extensions.len(),
        2,
        "Two preferred extensions under equal preferences"
    );

    let pref_concs: Vec<BTreeSet<Formula>> = preferred
        .extensions
        .iter()
        .map(|ext| conclusions_in(ext, &preferred.store))
        .collect();
    let has_married = pref_concs.iter().any(|c| c.contains(&formula!(Married)));
    let has_bachelor = pref_concs.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");
}

// --- No defeasible rules (§4.4) ---

fn build_no_defeasible_rules_system() -> AspicSystem {
    let (system, _) = AspicSystemBuilder::new()
        .with_classical_negation()
        .ordinary_premise(formula!(p))
        .ordinary_premise(formula!(q))
        .ordinary_premise(formula!(!p))
        .strict_rule("s1", vec![formula!(p), formula!(q)], formula!(r))
        .build();
    system
}

/// §4.4: All arguments are strict, all attacks are undermining.
#[test]
fn test_no_defeasible_rules_undermining_only() {
    let pipeline =
        AspicPipeline::classical(build_no_defeasible_rules_system(), Box::new(EqualOrdering));
    let result = pipeline.evaluate(Semantics::Grounded).unwrap();
    let attacks = &result.attacks;

    assert!(!attacks.is_empty(), "should have at least one attack");

    for attack in attacks {
        assert!(
            matches!(attack.kind, AttackKind::Undermine { .. }),
            "all attacks should be Undermine, got {:?}",
            attack.kind
        );
    }

    let has_rebut = attacks
        .iter()
        .any(|a| matches!(a.kind, AttackKind::Rebut { .. }));
    let has_undercut = attacks
        .iter()
        .any(|a| matches!(a.kind, AttackKind::Undercut { .. }));
    assert!(!has_rebut, "no Rebut attacks in a purely strict system");
    assert!(
        !has_undercut,
        "no Undercut attacks (no named defeasible rules)"
    );

    // All arguments should have empty DefRules
    for (_id, arg) in result.store.all_arguments() {
        assert!(
            arg.defeasible_rules(&result.store).is_empty(),
            "all arguments should have 0 defeasible rules"
        );
    }
}

/// §4.4: Preferred extensions correspond to maximal consistent subsets.
#[test]
fn test_no_defeasible_rules_max_consistent_subsets() {
    let result =
        AspicPipeline::classical(build_no_defeasible_rules_system(), Box::new(EqualOrdering))
            .evaluate(Semantics::Preferred)
            .unwrap();

    assert_eq!(
        result.extensions.len(),
        2,
        "two preferred extensions from {{p, q, ¬p}}"
    );

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

    // Extension 1: {p, q, r} — from maximal consistent subset {p, q}
    let has_pqr = ext_concs.iter().any(|c| {
        c.contains(&formula!(p))
            && c.contains(&formula!(q))
            && c.contains(&formula!(r))
            && !c.contains(&formula!(!p))
    });
    // Extension 2: {¬p, q} — from maximal consistent subset {¬p, q}
    let has_npq = ext_concs.iter().any(|c| {
        c.contains(&formula!(!p))
            && c.contains(&formula!(q))
            && !c.contains(&formula!(p))
            && !c.contains(&formula!(r))
    });

    assert!(
        has_pqr,
        "one extension should contain {{p, q, r}} (maximal consistent subset {{p, q}})"
    );
    assert!(
        has_npq,
        "one extension should contain {{¬p, q}} (maximal consistent subset {{¬p, q}})"
    );
}

/// §4.4: A total ordering on premises yields a unique preferred extension,
/// corresponding to Brewka's (1989) Preferred Subtheories.
#[test]
fn test_no_defeasible_rules_total_ordering() {
    let system = build_no_defeasible_rules_system();

    // Premise ordering: ¬p most preferred, q middle, p least preferred
    // This means ¬p strictly defeats p, but p cannot defeat ¬p.
    let ordering = last_link(
        vec![],
        vec![vec![formula!(!p)], vec![formula!(q)], vec![formula!(p)]],
    );

    let result = AspicPipeline::classical(system, Box::new(ordering))
        .evaluate(Semantics::Preferred)
        .unwrap();

    assert_eq!(
        result.extensions.len(),
        1,
        "total ordering should yield a unique preferred extension"
    );

    let conc = conclusions_in(&result.extensions[0], &result.store);
    assert!(
        conc.contains(&formula!(!p)),
        "¬p should be justified (most preferred)"
    );
    assert!(
        conc.contains(&formula!(q)),
        "q should be justified (uncontested)"
    );
    assert!(
        !conc.contains(&formula!(p)),
        "p should NOT be justified (defeated by ¬p)"
    );
    assert!(
        !conc.contains(&formula!(r)),
        "r should NOT be justified (p is out)"
    );
}
