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

mod common;

use common::{find_arg_by_conclusion_and_rule, find_premise_arg, EqualOrdering};

// ---
// Test infrastructure
// ---

#[derive(Debug, Clone)]
struct TieredArgOrdering {
    tiers: Vec<Vec<ArgumentId>>,
}

impl TieredArgOrdering {
    fn new(tiers: Vec<Vec<ArgumentId>>) -> Self {
        Self { tiers }
    }
}

impl ArgumentOrdering for TieredArgOrdering {
    fn compare(&self, a: ArgumentId, b: ArgumentId, _store: &ArgumentStore) -> Preference {
        let tier_a = self.tiers.iter().position(|t| t.contains(&a));
        let tier_b = self.tiers.iter().position(|t| t.contains(&b));
        match (tier_a, tier_b) {
            (Some(ta), Some(tb)) if ta < tb => Preference::StrictlyPreferred,
            (Some(ta), Some(tb)) if ta > tb => Preference::StrictlyDispreferred,
            (Some(_), Some(_)) => Preference::Equal,
            (Some(_), None) => Preference::StrictlyPreferred,
            (None, Some(_)) => Preference::StrictlyDispreferred,
            (None, None) => Preference::Equal,
        }
    }
}

fn build_and_evaluate(
    system: AspicSystem,
    set_preference: Box<dyn SetPreference>,
    semantics: Semantics,
) -> (ArgumentStore, Vec<Attack>, EvaluationResult) {
    let grounder = NaiveGrounder;
    let grounded = grounder.ground(&system).expect("grounding");
    let constructor = ForwardChainingConstructor;
    let store = constructor.construct(&grounded);
    let attack_computer = PairwiseAttackComputer;
    let attacks = attack_computer.compute(&store, &grounded.contrariness);
    let pref = PreferenceConfig::SetPreference(set_preference);
    let result = AccrualEvaluator
        .evaluate(&store, &attacks, semantics, &pref)
        .unwrap();
    (store, attacks, result)
}

fn build_classical(
    system: AspicSystem,
    ordering: Box<dyn ArgumentOrdering>,
    semantics: Semantics,
) -> (ArgumentStore, Vec<Attack>, EvaluationResult) {
    let grounder = NaiveGrounder;
    let grounded = grounder.ground(&system).expect("grounding");
    let constructor = ForwardChainingConstructor;
    let store = constructor.construct(&grounded);
    let attack_computer = PairwiseAttackComputer;
    let attacks = attack_computer.compute(&store, &grounded.contrariness);
    let evaluator = ClassicalEvaluator {
        semantics_solver: Box::new(NaiveEnumerationSolver),
    };
    let pref = PreferenceConfig::ArgumentOrdering(ordering);
    let result = evaluator
        .evaluate(&store, &attacks, semantics, &pref)
        .unwrap();
    (store, attacks, result)
}

// ---
// Basic accrual evaluation
// ---

mod basic_accrual {
    use super::*;

    /// Accrual with Elitist set comparison and equal ordering.
    ///
    /// AT: f1 ⇒r1 p, f2 ⇒r2 p, f3 ⇒r3 ¬p
    /// With Elitist + EqualOrdering: {A1, A2} and {B} are Equal-strength
    /// accrual sets, so mutual l-defeat occurs and all conflicting
    /// arguments are Undec in grounded semantics.
    #[test]
    fn accrual_equal_strength_mutual_defeat() {
        let (system, _) = AspicSystemBuilder::new()
            .with_classical_negation()
            .ordinary_premise(formula!(f1))
            .ordinary_premise(formula!(f2))
            .ordinary_premise(formula!(f3))
            .defeasible_rule("r1", vec![formula!(f1)], formula!(p))
            .defeasible_rule("r2", vec![formula!(f2)], formula!(p))
            .defeasible_rule("r3", vec![formula!(f3)], formula!(!p))
            .build();

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

        let a1 = find_arg_by_conclusion_and_rule(&store, &formula!(p), "r1").expect("A1");
        let a2 = find_arg_by_conclusion_and_rule(&store, &formula!(p), "r2").expect("A2");
        let b = find_arg_by_conclusion_and_rule(&store, &formula!(!p), "r3").expect("B");

        let set_pref = LiftedSetPreference {
            base: Box::new(EqualOrdering),
            lifting: LiftingStrategy::Elitist,
        };

        let pref = PreferenceConfig::SetPreference(Box::new(set_pref));
        let result = AccrualEvaluator
            .evaluate(&store, &attacks, Semantics::Grounded, &pref)
            .unwrap();

        assert_eq!(result.extensions.len(), 1);
        let ext = &result.extensions[0];
        let lab = &result.labellings[0];

        assert!(!ext.contains(&a1), "A1 should not be In (mutual defeat)");
        assert!(!ext.contains(&a2), "A2 should not be In (mutual defeat)");
        assert!(!ext.contains(&b), "B should not be In (mutual defeat)");
        assert_eq!(lab.label_of(a1), Label::Undec, "A1 Undec");
        assert_eq!(lab.label_of(a2), Label::Undec, "A2 Undec");
        assert_eq!(lab.label_of(b), Label::Undec, "B Undec");
    }

    /// Classical evaluator diverges on the same AT.
    #[test]
    fn classical_divergence_baseline() {
        let (system, _) = AspicSystemBuilder::new()
            .with_classical_negation()
            .ordinary_premise(formula!(f1))
            .ordinary_premise(formula!(f2))
            .ordinary_premise(formula!(f3))
            .defeasible_rule("r1", vec![formula!(f1)], formula!(p))
            .defeasible_rule("r2", vec![formula!(f2)], formula!(p))
            .defeasible_rule("r3", vec![formula!(f3)], formula!(!p))
            .build();

        let (store, _, result) =
            build_classical(system, Box::new(EqualOrdering), Semantics::Grounded);

        let a1 = find_arg_by_conclusion_and_rule(&store, &formula!(p), "r1");
        let a2 = find_arg_by_conclusion_and_rule(&store, &formula!(p), "r2");
        let b = find_arg_by_conclusion_and_rule(&store, &formula!(!p), "r3");

        let ext = &result.extensions[0];

        // Under classical with equal ordering, mutual rebutting defeats
        // mean both sides are undecided in grounded semantics.
        let both_in =
            a1.is_some_and(|id| ext.contains(&id)) && a2.is_some_and(|id| ext.contains(&id));
        let b_out = b.is_some_and(|id| !ext.contains(&id));

        // Classical should NOT have both A1,A2 In with B Out simultaneously
        // (since equal ordering means all defeats succeed in both directions).
        assert!(
            !(both_in && b_out),
            "classical: should not have both pro-p In and con-p Out with equal ordering"
        );
    }

    /// Reduction property — unique conclusions yield identical results (Proposition 5.5).
    #[test]
    fn reduction_property_unique_conclusions() {
        let (system, _) = AspicSystemBuilder::new()
            .with_classical_negation()
            .ordinary_premise(formula!(a))
            .ordinary_premise(formula!(b))
            .defeasible_rule("r1", vec![formula!(a)], formula!(c))
            .defeasible_rule("r2", vec![formula!(b)], formula!(!c))
            .build();

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

        let classical_eval = ClassicalEvaluator {
            semantics_solver: Box::new(NaiveEnumerationSolver),
        };
        let classical_pref = PreferenceConfig::ArgumentOrdering(Box::new(EqualOrdering));
        let classical_result = classical_eval
            .evaluate(&store, &attacks, Semantics::Grounded, &classical_pref)
            .unwrap();

        let accrual_pref = PreferenceConfig::SetPreference(Box::new(LiftedSetPreference {
            base: Box::new(EqualOrdering),
            lifting: LiftingStrategy::Elitist,
        }));
        let accrual_result = AccrualEvaluator
            .evaluate(&store, &attacks, Semantics::Grounded, &accrual_pref)
            .unwrap();

        assert_eq!(
            classical_result.extensions, accrual_result.extensions,
            "Proposition 5.5: unique conclusions should yield identical extensions"
        );
    }
}

// ---
// Fixpoint convergence
// ---

mod fixpoint_convergence {
    use super::*;

    /// Chain of 5 arguments — correct In/Out alternation.
    #[test]
    fn chain_of_five() {
        // a1 ← a2 ← a3 ← a4 ← a5 (each attacks its predecessor)
        // Expected grounded: a5 In, a4 Out, a3 In, a2 Out, a1 In
        let (system, _) = AspicSystemBuilder::new()
            .with_classical_negation()
            .ordinary_premise(formula!(f1))
            .ordinary_premise(formula!(f2))
            .ordinary_premise(formula!(f3))
            .ordinary_premise(formula!(f4))
            .ordinary_premise(formula!(f5))
            .defeasible_rule("r1", vec![formula!(f1)], formula!(p1))
            .defeasible_rule("r2", vec![formula!(f2)], formula!(!p1))
            .defeasible_rule("r3", vec![formula!(f3)], formula!(p2))
            .defeasible_rule("r4", vec![formula!(f4)], formula!(!p2))
            .defeasible_rule("r5", vec![formula!(f5)], formula!(p3))
            .build();

        let set_pref = LiftedSetPreference {
            base: Box::new(EqualOrdering),
            lifting: LiftingStrategy::Elitist,
        };

        let (store, _, result) =
            build_and_evaluate(system, Box::new(set_pref), Semantics::Grounded);

        assert_eq!(result.extensions.len(), 1, "grounded should be unique");

        // Unrelated conclusions — no accrual. This tests fixpoint termination.
        let p3_arg = find_arg_by_conclusion_and_rule(&store, &formula!(p3), "r5");
        assert!(
            p3_arg.is_some_and(|id| result.extensions[0].contains(&id)),
            "unattacked argument for p3 should be In"
        );
    }

    /// Mutual rebuttal cycle — both undecided.
    #[test]
    fn mutual_rebuttal_cycle_undecided() {
        let (system, _) = AspicSystemBuilder::new()
            .with_classical_negation()
            .ordinary_premise(formula!(f1))
            .ordinary_premise(formula!(f2))
            .defeasible_rule("r1", vec![formula!(f1)], formula!(p))
            .defeasible_rule("r2", vec![formula!(f2)], formula!(!p))
            .build();

        let set_pref = LiftedSetPreference {
            base: Box::new(EqualOrdering),
            lifting: LiftingStrategy::Elitist,
        };

        let (store, _, result) =
            build_and_evaluate(system, Box::new(set_pref), Semantics::Grounded);

        assert_eq!(result.extensions.len(), 1);
        let ext = &result.extensions[0];
        let lab = &result.labellings[0];

        let a = find_arg_by_conclusion_and_rule(&store, &formula!(p), "r1").expect("A");
        let b = find_arg_by_conclusion_and_rule(&store, &formula!(!p), "r2").expect("B");

        assert!(!ext.contains(&a), "A should not be In (cycle)");
        assert!(!ext.contains(&b), "B should not be In (cycle)");
        assert_eq!(lab.label_of(a), Label::Undec, "A should be Undec");
        assert_eq!(lab.label_of(b), Label::Undec, "B should be Undec");
    }

    /// Unattacked premise arguments are labelled In immediately.
    #[test]
    fn unattacked_premises_in() {
        let (system, _) = AspicSystemBuilder::new()
            .with_classical_negation()
            .ordinary_premise(formula!(a))
            .defeasible_rule("r1", vec![formula!(a)], formula!(b))
            .build();

        let set_pref = LiftedSetPreference {
            base: Box::new(EqualOrdering),
            lifting: LiftingStrategy::Elitist,
        };

        let (store, _, result) =
            build_and_evaluate(system, Box::new(set_pref), Semantics::Grounded);

        let ext = &result.extensions[0];

        let prem_a = find_premise_arg(&store, &formula!(a)).expect("premise a");
        let arg_b = find_arg_by_conclusion_and_rule(&store, &formula!(b), "r1").expect("arg b");

        assert!(ext.contains(&prem_a), "premise a should be In");
        assert!(ext.contains(&arg_b), "argument b should be In");
    }
}

// ---
// Accrual principles
// ---

mod accrual_principles {
    use super::*;

    /// Accrual subsumption preserves individual justification.
    ///
    /// {A1, A2} for p vs {B} for ¬p. Both A1 and A2 are individually
    /// preferred over B (tier 0 vs tier 1).
    /// Under Elitist: {B} ≤_Eli {A1,A2} iff ∃b∈{B}: ∀a∈{A1,A2}: b≤a.
    /// B ≤ A1 (yes) AND B ≤ A2 (yes) → TRUE.
    /// {A1,A2} ≤_Eli {B}: ∃a∈{A1,A2}: a≤B. A1≤B? No. A2≤B? No → FALSE.
    /// Result: {A1,A2} strictly preferred → p justified under accrual,
    /// matching the classical result (subsumption principle).
    #[test]
    fn subsumption_preserves_justification() {
        let (system, _) = AspicSystemBuilder::new()
            .with_classical_negation()
            .ordinary_premise(formula!(f1))
            .ordinary_premise(formula!(f2))
            .ordinary_premise(formula!(f3))
            .defeasible_rule("r1", vec![formula!(f1)], formula!(p))
            .defeasible_rule("r2", vec![formula!(f2)], formula!(p))
            .defeasible_rule("r3", vec![formula!(f3)], formula!(!p))
            .build();

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

        let a1 = find_arg_by_conclusion_and_rule(&store, &formula!(p), "r1").expect("A1");
        let a2 = find_arg_by_conclusion_and_rule(&store, &formula!(p), "r2").expect("A2");
        let b = find_arg_by_conclusion_and_rule(&store, &formula!(!p), "r3").expect("B");

        let ordering = TieredArgOrdering::new(vec![vec![a1, a2], vec![b]]);

        let set_pref = LiftedSetPreference {
            base: Box::new(ordering),
            lifting: LiftingStrategy::Elitist,
        };

        let pref = PreferenceConfig::SetPreference(Box::new(set_pref));
        let result = AccrualEvaluator
            .evaluate(&store, &attacks, Semantics::Grounded, &pref)
            .unwrap();

        let ext = &result.extensions[0];

        assert!(ext.contains(&a1), "A1 should be In (subsumption)");
        assert!(ext.contains(&a2), "A2 should be In (subsumption)");
        assert!(!ext.contains(&b), "B should be Out (subsumption)");
    }

    /// Flawed arguments are excluded from accrual sets.
    ///
    /// A1 for p has an undercut sub-argument. A2 for p is healthy.
    /// A1 should be excluded from the accrual set, leaving only {A2}.
    #[test]
    fn flawed_arguments_excluded() {
        // f1 ⇒r1 q, q ⇒r2 p — A1 for p uses sub-argument for q
        // f2 ⇒r3 p — A2 for p, independent
        // f3 ⇒r4 ¬r1 — undercuts r1, defeating A1's sub-argument
        // f4 ⇒r5 ¬p — B for ¬p
        let (system, _) = AspicSystemBuilder::new()
            .with_classical_negation()
            .ordinary_premise(formula!(f1))
            .ordinary_premise(formula!(f2))
            .ordinary_premise(formula!(f3))
            .ordinary_premise(formula!(f4))
            .named_defeasible_rule("r1", formula!(r1), vec![formula!(f1)], formula!(q))
            .defeasible_rule("r2", vec![formula!(q)], formula!(p))
            .defeasible_rule("r3", vec![formula!(f2)], formula!(p))
            .defeasible_rule("r4", vec![formula!(f3)], formula!(!r1))
            .defeasible_rule("r5", vec![formula!(f4)], formula!(!p))
            .build();

        let set_pref = LiftedSetPreference {
            base: Box::new(EqualOrdering),
            lifting: LiftingStrategy::Elitist,
        };

        let (store, _, result) =
            build_and_evaluate(system, Box::new(set_pref), Semantics::Grounded);

        let lab = &result.labellings[0];

        // The undercut argument for ¬r1 should be In (unattacked).
        // The sub-argument for q via r1 should be Out (undercut).
        // Therefore A1 (p via r2) should be Out (ImmSub is Out).
        // A2 (p via r3) should still be valid.

        let undercut_arg = find_arg_by_conclusion_and_rule(&store, &formula!(!r1), "r4");
        if let Some(uc) = undercut_arg {
            assert_eq!(
                lab.label_of(uc),
                Label::In,
                "undercut argument should be In"
            );
        }

        // A1's sub-argument for q via r1 should be Out
        let sub_q = find_arg_by_conclusion_and_rule(&store, &formula!(q), "r1");
        if let Some(sq) = sub_q {
            assert_eq!(
                lab.label_of(sq),
                Label::Out,
                "undercut sub-argument should be Out"
            );
        }

        // A1 (p via r2 with q as sub) should be Out (ImmSub q is Out)
        let a1 = find_arg_by_conclusion_and_rule(&store, &formula!(p), "r2");
        if let Some(a1_id) = a1 {
            assert_eq!(
                lab.label_of(a1_id),
                Label::Out,
                "A1 with defeated sub should be Out"
            );
        }
    }
}

// ---
// Semantics coverage (preferred, stable, Dungean properties)
// ---

mod semantics_coverage {
    use super::*;

    /// Preferred semantics produces multiple labellings on a mutual rebuttal cycle.
    #[test]
    fn preferred_produces_multiple_labellings() {
        let (system, _) = AspicSystemBuilder::new()
            .with_classical_negation()
            .ordinary_premise(formula!(f1))
            .ordinary_premise(formula!(f2))
            .defeasible_rule("r1", vec![formula!(f1)], formula!(p))
            .defeasible_rule("r2", vec![formula!(f2)], formula!(!p))
            .build();

        let set_pref = LiftedSetPreference {
            base: Box::new(EqualOrdering),
            lifting: LiftingStrategy::Elitist,
        };

        let (store, _, result) =
            build_and_evaluate(system, Box::new(set_pref), Semantics::Preferred);

        // Two preferred labellings: one where A is In, one where B is In
        assert!(
            result.extensions.len() >= 2,
            "preferred should produce at least 2 labellings for mutual rebuttal, got {}",
            result.extensions.len()
        );

        let a = find_arg_by_conclusion_and_rule(&store, &formula!(p), "r1").expect("A");
        let b = find_arg_by_conclusion_and_rule(&store, &formula!(!p), "r2").expect("B");

        let a_in_some = result.extensions.iter().any(|ext| ext.contains(&a));
        let b_in_some = result.extensions.iter().any(|ext| ext.contains(&b));

        assert!(a_in_some, "A should be In in some preferred labelling");
        assert!(b_in_some, "B should be In in some preferred labelling");
    }

    /// Dungean inclusion relationships: grounded ⊆ complete ⊆ preferred.
    #[test]
    fn dungean_inclusion_relationships() {
        let (system, _) = AspicSystemBuilder::new()
            .with_classical_negation()
            .ordinary_premise(formula!(f1))
            .ordinary_premise(formula!(f2))
            .ordinary_premise(formula!(f3))
            .defeasible_rule("r1", vec![formula!(f1)], formula!(p))
            .defeasible_rule("r2", vec![formula!(f2)], formula!(!p))
            .defeasible_rule("r3", vec![formula!(f3)], formula!(q))
            .build();

        let make_pref = || -> Box<dyn SetPreference> {
            Box::new(LiftedSetPreference {
                base: Box::new(EqualOrdering),
                lifting: LiftingStrategy::Elitist,
            })
        };

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

        let pref = PreferenceConfig::SetPreference(make_pref());
        let grounded = AccrualEvaluator
            .evaluate(&store, &attacks, Semantics::Grounded, &pref)
            .unwrap();
        let pref = PreferenceConfig::SetPreference(make_pref());
        let complete = AccrualEvaluator
            .evaluate(&store, &attacks, Semantics::Complete, &pref)
            .unwrap();
        let pref = PreferenceConfig::SetPreference(make_pref());
        let preferred = AccrualEvaluator
            .evaluate(&store, &attacks, Semantics::Preferred, &pref)
            .unwrap();

        let grounded_in = &grounded.extensions[0];

        // Grounded In ⊆ every complete In
        for comp_ext in &complete.extensions {
            assert!(
                grounded_in.is_subset(comp_ext),
                "grounded In should be subset of complete In"
            );
        }

        // Grounded In ⊆ every preferred In
        for pref_ext in &preferred.extensions {
            assert!(
                grounded_in.is_subset(pref_ext),
                "grounded In should be subset of preferred In"
            );
        }

        // Every preferred is a complete
        for pref_ext in &preferred.extensions {
            assert!(
                complete.extensions.iter().any(|c| c == pref_ext),
                "every preferred extension should also be a complete extension"
            );
        }
    }

    /// Reduction property under Preferred semantics.
    #[test]
    fn reduction_property_preferred() {
        let (system, _) = AspicSystemBuilder::new()
            .with_classical_negation()
            .ordinary_premise(formula!(a))
            .ordinary_premise(formula!(b))
            .defeasible_rule("r1", vec![formula!(a)], formula!(c))
            .defeasible_rule("r2", vec![formula!(b)], formula!(!c))
            .build();

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

        let classical = ClassicalEvaluator {
            semantics_solver: Box::new(NaiveEnumerationSolver),
        };
        let classical_pref = PreferenceConfig::ArgumentOrdering(Box::new(EqualOrdering));
        let classical_result = classical
            .evaluate(&store, &attacks, Semantics::Preferred, &classical_pref)
            .unwrap();

        let accrual_pref = PreferenceConfig::SetPreference(Box::new(LiftedSetPreference {
            base: Box::new(EqualOrdering),
            lifting: LiftingStrategy::Elitist,
        }));
        let accrual_result = AccrualEvaluator
            .evaluate(&store, &attacks, Semantics::Preferred, &accrual_pref)
            .unwrap();

        // Same number of preferred extensions
        assert_eq!(
            classical_result.extensions.len(),
            accrual_result.extensions.len(),
            "same number of preferred extensions"
        );

        // Same In-sets (order may differ)
        let mut classical_sorted: Vec<_> = classical_result.extensions.clone();
        classical_sorted.sort();
        let mut accrual_sorted: Vec<_> = accrual_result.extensions.clone();
        accrual_sorted.sort();
        assert_eq!(
            classical_sorted, accrual_sorted,
            "same preferred extensions"
        );
    }

    /// Stable semantics on a simple conflict.
    #[test]
    fn stable_semantics() {
        let (system, _) = AspicSystemBuilder::new()
            .with_classical_negation()
            .ordinary_premise(formula!(f1))
            .ordinary_premise(formula!(f2))
            .defeasible_rule("r1", vec![formula!(f1)], formula!(p))
            .defeasible_rule("r2", vec![formula!(f2)], formula!(!p))
            .build();

        let set_pref = LiftedSetPreference {
            base: Box::new(EqualOrdering),
            lifting: LiftingStrategy::Elitist,
        };

        let (_, _, result) = build_and_evaluate(system, Box::new(set_pref), Semantics::Stable);

        // Each stable labelling should have no undecided arguments
        for lab in &result.labellings {
            assert!(
                lab.undec_args().is_empty(),
                "stable labelling should have no Undec arguments"
            );
        }
    }
}

// ---
// Pipeline integration
// ---

mod pipeline_integration {
    use super::*;

    /// AspicPipeline::accrual() compiles, evaluates, and returns PipelineResult.
    #[test]
    fn pipeline_accrual_constructor() {
        let (system, _) = AspicSystemBuilder::new()
            .with_classical_negation()
            .ordinary_premise(formula!(a))
            .defeasible_rule("r1", vec![formula!(a)], formula!(b))
            .build();

        let set_pref = LiftedSetPreference {
            base: Box::new(EqualOrdering),
            lifting: LiftingStrategy::Elitist,
        };

        let pipeline = AspicPipeline::accrual(system, Box::new(set_pref));

        let result = pipeline
            .evaluate(Semantics::Grounded)
            .expect("pipeline should succeed");

        assert!(!result.store.is_empty(), "store should have arguments");
        assert!(!result.extensions.is_empty(), "should have extensions");
        assert_eq!(
            result.extensions.len(),
            result.labellings.len(),
            "extensions and labellings count should match"
        );
    }

    /// Classical and accrual pipelines produce identical results on unique conclusions.
    #[test]
    fn pipeline_equivalence_unique_conclusions() {
        let (system, _) = AspicSystemBuilder::new()
            .with_classical_negation()
            .ordinary_premise(formula!(a))
            .ordinary_premise(formula!(b))
            .defeasible_rule("r1", vec![formula!(a)], formula!(c))
            .defeasible_rule("r2", vec![formula!(b)], formula!(d))
            .build();

        let classical_pipeline = AspicPipeline::classical(system.clone(), Box::new(EqualOrdering));
        let classical_result = classical_pipeline.evaluate(Semantics::Grounded).unwrap();

        let set_pref = LiftedSetPreference {
            base: Box::new(EqualOrdering),
            lifting: LiftingStrategy::Elitist,
        };
        let accrual_pipeline = AspicPipeline::accrual(system, Box::new(set_pref));
        let accrual_result = accrual_pipeline.evaluate(Semantics::Grounded).unwrap();

        assert_eq!(
            classical_result.extensions, accrual_result.extensions,
            "unique conclusions → identical extensions"
        );
    }
}

// ---
// Legal reasoning scenarios
// ---

mod legal_reasoning {
    use super::*;

    /// Legislative debate — both pro-premises defeated (§6.2).
    ///
    /// GC1: f1 ⇒r1 BillGood (premise f1 attacked by C)
    /// GC2: f2 ⇒r2 BillGood (premise f2 attacked by E)
    /// GC3: f3 ⇒r3 BillGood (unattacked)
    /// BC1: f4 ⇒r4 ¬BillGood
    /// BC2: f5 ⇒r5 ¬BillGood
    /// C: f6 ⇒r6 ¬f1 (attacks GC1's premise)
    /// E: f7 ⇒r7 ¬f2 (attacks GC2's premise)
    ///
    /// Ordering: C > prem(f1), E > prem(f2) (attackers strictly defeat
    /// premises), and BC1, BC2 > GC3 (con arguments preferred over
    /// the remaining pro argument). With GC1 and GC2 excluded from the
    /// accrual set, {BC1,BC2} strictly defeats {GC3} under Elitist.
    #[test]
    fn legislative_debate_both_premises_defeated() {
        let (system, _) = AspicSystemBuilder::new()
            .with_classical_negation()
            .ordinary_premise(formula!(f1))
            .ordinary_premise(formula!(f2))
            .ordinary_premise(formula!(f3))
            .ordinary_premise(formula!(f4))
            .ordinary_premise(formula!(f5))
            .ordinary_premise(formula!(f6))
            .ordinary_premise(formula!(f7))
            .defeasible_rule("r1", vec![formula!(f1)], formula!(good))
            .defeasible_rule("r2", vec![formula!(f2)], formula!(good))
            .defeasible_rule("r3", vec![formula!(f3)], formula!(good))
            .defeasible_rule("r4", vec![formula!(f4)], formula!(!good))
            .defeasible_rule("r5", vec![formula!(f5)], formula!(!good))
            .defeasible_rule("r6", vec![formula!(f6)], formula!(!f1))
            .defeasible_rule("r7", vec![formula!(f7)], formula!(!f2))
            .build();

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

        let c_arg = find_arg_by_conclusion_and_rule(&store, &formula!(!f1), "r6").expect("C");
        let e_arg = find_arg_by_conclusion_and_rule(&store, &formula!(!f2), "r7").expect("E");
        let prem_f1 = find_premise_arg(&store, &formula!(f1)).expect("prem f1");
        let prem_f2 = find_premise_arg(&store, &formula!(f2)).expect("prem f2");
        let gc3 = find_arg_by_conclusion_and_rule(&store, &formula!(good), "r3").expect("GC3");
        let bc1 = find_arg_by_conclusion_and_rule(&store, &formula!(!good), "r4").expect("BC1");
        let bc2 = find_arg_by_conclusion_and_rule(&store, &formula!(!good), "r5").expect("BC2");

        // Tier 0: C, E (highest); Tier 1: BC1, BC2; Tier 2: prem_f1, prem_f2, GC3
        let ordering = TieredArgOrdering::new(vec![
            vec![c_arg, e_arg],
            vec![bc1, bc2],
            vec![prem_f1, prem_f2, gc3],
        ]);

        let set_pref = LiftedSetPreference {
            base: Box::new(ordering),
            lifting: LiftingStrategy::Elitist,
        };

        let pref = PreferenceConfig::SetPreference(Box::new(set_pref));
        let result = AccrualEvaluator
            .evaluate(&store, &attacks, Semantics::Grounded, &pref)
            .unwrap();
        let lab = &result.labellings[0];

        assert_eq!(
            lab.label_of(c_arg),
            Label::In,
            "C (attack on f1) should be In"
        );
        assert_eq!(
            lab.label_of(e_arg),
            Label::In,
            "E (attack on f2) should be In"
        );

        assert_eq!(lab.label_of(prem_f1), Label::Out, "prem f1 should be Out");
        assert_eq!(lab.label_of(prem_f2), Label::Out, "prem f2 should be Out");

        assert_eq!(lab.label_of(bc1), Label::In, "BC1 should be In");
        assert_eq!(lab.label_of(bc2), Label::In, "BC2 should be In");
    }

    /// Legislative debate — premise attacks create cycles under equal ordering.
    ///
    /// Under equal ordering, the mutual undermining between premise
    /// arguments and their attackers creates cycles, leaving both
    /// sides undecided in the grounded labelling.
    #[test]
    fn legislative_debate_equal_ordering_undecided() {
        let (system, _) = AspicSystemBuilder::new()
            .with_classical_negation()
            .ordinary_premise(formula!(f1))
            .ordinary_premise(formula!(f2))
            .ordinary_premise(formula!(f3))
            .ordinary_premise(formula!(f4))
            .ordinary_premise(formula!(f5))
            .ordinary_premise(formula!(f6))
            .defeasible_rule("r1", vec![formula!(f1)], formula!(good))
            .defeasible_rule("r2", vec![formula!(f2)], formula!(good))
            .defeasible_rule("r3", vec![formula!(f3)], formula!(!good))
            .defeasible_rule("r4", vec![formula!(f4)], formula!(!good))
            .defeasible_rule("r5", vec![formula!(f5)], formula!(!f1))
            .defeasible_rule("r6", vec![formula!(f6)], formula!(!f2))
            .build();

        let set_pref = LiftedSetPreference {
            base: Box::new(EqualOrdering),
            lifting: LiftingStrategy::Elitist,
        };

        let (store, _, result) =
            build_and_evaluate(system, Box::new(set_pref), Semantics::Grounded);

        assert_eq!(result.extensions.len(), 1, "grounded is unique");
        let lab = &result.labellings[0];

        // With equal ordering, mutual undermining creates cycles
        // The good/¬good arguments should be Undec
        let gc1 = find_arg_by_conclusion_and_rule(&store, &formula!(good), "r1");
        let bc1 = find_arg_by_conclusion_and_rule(&store, &formula!(!good), "r3");

        if let Some(gc1_id) = gc1 {
            assert_eq!(
                lab.label_of(gc1_id),
                Label::Undec,
                "GC1 should be Undec (cycle)"
            );
        }
        if let Some(bc1_id) = bc1 {
            assert_eq!(
                lab.label_of(bc1_id),
                Label::Undec,
                "BC1 should be Undec (cycle)"
            );
        }

        // Preferred should yield multiple labellings
        let set_pref2 = LiftedSetPreference {
            base: Box::new(EqualOrdering),
            lifting: LiftingStrategy::Elitist,
        };
        let (_, _, pref_result) = build_and_evaluate(
            AspicSystemBuilder::new()
                .with_classical_negation()
                .ordinary_premise(formula!(f1))
                .ordinary_premise(formula!(f2))
                .ordinary_premise(formula!(f3))
                .ordinary_premise(formula!(f4))
                .ordinary_premise(formula!(f5))
                .ordinary_premise(formula!(f6))
                .defeasible_rule("r1", vec![formula!(f1)], formula!(good))
                .defeasible_rule("r2", vec![formula!(f2)], formula!(good))
                .defeasible_rule("r3", vec![formula!(f3)], formula!(!good))
                .defeasible_rule("r4", vec![formula!(f4)], formula!(!good))
                .defeasible_rule("r5", vec![formula!(f5)], formula!(!f1))
                .defeasible_rule("r6", vec![formula!(f6)], formula!(!f2))
                .build()
                .0,
            Box::new(set_pref2),
            Semantics::Preferred,
        );

        assert!(
            pref_result.extensions.len() >= 2,
            "preferred should yield multiple labellings, got {}",
            pref_result.extensions.len()
        );
    }
}

// ---
// Accrual equivalence on Example 3.7
// ---

/// On Example 3.7 (all conclusions unique), the accrual evaluator produces
/// the same extensions as the classical evaluator.
#[test]
fn accrual_equivalence_example_3_7() {
    let (system, _) = AspicSystemBuilder::new()
        .with_classical_negation()
        .axiom(formula!(s))
        .axiom(formula!(t))
        .ordinary_premise(formula!(p))
        .ordinary_premise(formula!(q))
        .ordinary_premise(formula!(r))
        .strict_rule("s1", vec![formula!(s)], formula!(q1))
        .strict_rule("s2", vec![formula!(t)], formula!(r1))
        .defeasible_rule("d1", vec![formula!(p)], formula!(!q1))
        .defeasible_rule("d2", vec![formula!(q)], formula!(!r1))
        .defeasible_rule("d3", vec![formula!(r)], formula!(!p))
        .build();

    let set_pref = LiftedSetPreference {
        base: Box::new(EqualOrdering),
        lifting: LiftingStrategy::Elitist,
    };

    let classical = AspicPipeline::classical(system.clone(), Box::new(EqualOrdering));
    let accrual = AspicPipeline::accrual(system, Box::new(set_pref));

    let cr = classical
        .evaluate(Semantics::Grounded)
        .expect("classical pipeline");
    let ar = accrual
        .evaluate(Semantics::Grounded)
        .expect("accrual pipeline");

    assert_eq!(
        cr.extensions.len(),
        ar.extensions.len(),
        "same number of extensions"
    );

    for (ce, ae) in cr.extensions.iter().zip(ar.extensions.iter()) {
        assert_eq!(
            ce, ae,
            "extensions should be identical for unique conclusions"
        );
    }
}
