mod common;
use common::build_af;
#[cfg(feature = "sat")]
use common::sorted_exts;

use pickaxe_rs::prelude::*;
use proptest::prelude::*;
use std::collections::BTreeSet;

fn solver() -> NaiveEnumerationSolver {
    NaiveEnumerationSolver
}

#[cfg(feature = "sat")]
fn scc_solver() -> SccDecomposingSolver {
    SccDecomposingSolver {
        inner: Box::new(NaiveEnumerationSolver),
    }
}

#[cfg(feature = "sat")]
fn sat_solver() -> SatSolver {
    SatSolver::default()
}

/// Test grounded semantics: single unattacked argument.
#[test]
fn grounded_single_unattacked() {
    let af = build_af(1, &[]);
    let exts = solver().extensions(&af, Semantics::Grounded);
    assert_eq!(exts.len(), 1);
    assert!(exts[0].contains(&ArgumentId(0)));
}

/// Test grounded semantics: simple defeat chain.
/// A0 -> A1 -> A2
/// Grounded: {A0, A2} (A0 unattacked; A0 defeats A1; A1 defeated so A2 defended)
#[test]
fn grounded_chain() {
    let af = build_af(3, &[(0, 1), (1, 2)]);
    let exts = solver().extensions(&af, Semantics::Grounded);
    assert_eq!(exts.len(), 1);
    let grounded = &exts[0];
    assert!(grounded.contains(&ArgumentId(0)));
    assert!(!grounded.contains(&ArgumentId(1)));
    assert!(grounded.contains(&ArgumentId(2)));
}

/// Test grounded semantics: mutual attack (A0 <-> A1).
/// Grounded: {} (neither can be accepted)
#[test]
fn grounded_mutual_attack() {
    let af = build_af(2, &[(0, 1), (1, 0)]);
    let exts = solver().extensions(&af, Semantics::Grounded);
    assert_eq!(exts.len(), 1);
    assert!(exts[0].is_empty());
}

/// Test preferred semantics: mutual attack should yield two preferred extensions.
#[test]
fn preferred_mutual_attack() {
    let af = build_af(2, &[(0, 1), (1, 0)]);
    let exts = solver().extensions(&af, Semantics::Preferred);

    // Two preferred: {A0} and {A1}
    assert_eq!(exts.len(), 2);

    let ext_sets: Vec<BTreeSet<ArgumentId>> = exts.clone();
    let s0: BTreeSet<_> = [ArgumentId(0)].into_iter().collect();
    let s1: BTreeSet<_> = [ArgumentId(1)].into_iter().collect();
    assert!(ext_sets.contains(&s0));
    assert!(ext_sets.contains(&s1));
}

/// Test stable semantics: same as preferred for mutual attack.
#[test]
fn stable_mutual_attack() {
    let af = build_af(2, &[(0, 1), (1, 0)]);
    let exts = solver().extensions(&af, Semantics::Stable);
    assert_eq!(exts.len(), 2);
}

/// Test complete semantics: mutual attack should have three complete extensions.
/// {} (empty is complete), {A0}, {A1}
#[test]
fn complete_mutual_attack() {
    let af = build_af(2, &[(0, 1), (1, 0)]);
    let exts = solver().extensions(&af, Semantics::Complete);

    // Should be at least 3: empty, {A0}, {A1}
    assert!(
        exts.len() >= 3,
        "expected >= 3 complete extensions, got {}",
        exts.len()
    );

    let empty: BTreeSet<ArgumentId> = BTreeSet::new();
    let s0: BTreeSet<_> = [ArgumentId(0)].into_iter().collect();
    let s1: BTreeSet<_> = [ArgumentId(1)].into_iter().collect();
    assert!(exts.contains(&empty));
    assert!(exts.contains(&s0));
    assert!(exts.contains(&s1));
}

/// Test grounded labelling.
#[test]
fn grounded_labelling_test() {
    let af = build_af(3, &[(0, 1), (1, 2)]);
    let labellings = solver().labellings(&af, Semantics::Grounded);
    assert_eq!(labellings.len(), 1);
    let labelling = &labellings[0];

    assert_eq!(labelling.label_of(ArgumentId(0)), Label::In);
    assert_eq!(labelling.label_of(ArgumentId(1)), Label::Out);
    assert_eq!(labelling.label_of(ArgumentId(2)), Label::In);
}

/// Test grounded labelling for mutual attack: all undecided.
#[test]
fn grounded_labelling_mutual() {
    let af = build_af(2, &[(0, 1), (1, 0)]);
    let labellings = solver().labellings(&af, Semantics::Grounded);
    assert_eq!(labellings.len(), 1);
    let labelling = &labellings[0];

    assert_eq!(labelling.label_of(ArgumentId(0)), Label::Undec);
    assert_eq!(labelling.label_of(ArgumentId(1)), Label::Undec);
}

/// Test no arguments, no defeats.
#[test]
fn empty_framework() {
    let af = build_af(0, &[]);
    let exts = solver().extensions(&af, Semantics::Grounded);
    assert_eq!(exts.len(), 1);
    assert!(exts[0].is_empty());
}

/// Self-attacking argument: A0 -> A0.
/// Grounded: {} (A0 is not defended).
#[test]
fn self_attack() {
    let af = build_af(1, &[(0, 0)]);
    let exts = solver().extensions(&af, Semantics::Grounded);
    assert_eq!(exts.len(), 1);
    assert!(exts[0].is_empty());
}

/// Test that stable labellings contain no Undec arguments.
#[test]
fn stable_labellings_no_undec() {
    let af = build_af(2, &[(0, 1), (1, 0)]);
    let labellings = solver().labellings(&af, Semantics::Stable);

    assert_eq!(
        labellings.len(),
        2,
        "mutual attack should have 2 stable labellings"
    );
    for labelling in &labellings {
        assert!(
            labelling.undec_args().is_empty(),
            "stable labelling should have no Undec arguments, got Undec = {:?}",
            labelling.undec_args()
        );
    }
}

/// Test AF export formats.
#[test]
fn export_formats() {
    let af = build_af(3, &[(0, 1), (1, 2)]);

    let store = {
        let mut s = ArgumentStore::new();
        for i in 0..3 {
            use pickaxe_rs::framework::argument::Argument;
            use pickaxe_rs::system::knowledge::{Premise, PremiseKind};
            s.add(Argument::Premise {
                id: ArgumentId(i),
                premise: Premise {
                    formula: Formula::prop(format!("p{}", i)),
                    kind: PremiseKind::Ordinary,
                },
            });
        }
        s
    };

    let tgf = af.to_tgf();
    assert!(tgf.contains("#"));
    assert!(tgf.contains("0"));

    let aspartix = af.to_aspartix();
    assert!(aspartix.contains("arg(a0)."));
    assert!(aspartix.contains("att(a0,a1)."));

    let dot = af.to_dot(&store);
    assert!(dot.contains("digraph AF"));
    assert!(dot.contains("->"));

    let iccma = af.to_iccma();
    assert!(iccma.contains("p af 3"));
}

// --- Proptest AF generation strategy ---

/// Generate a random AbstractFramework with `n` arguments (2..=6) and a random
/// subset of the n² possible defeat pairs.
fn arb_af() -> impl Strategy<Value = AbstractFramework> {
    (2..=6usize).prop_flat_map(|n| {
        proptest::collection::vec(proptest::bool::ANY, n * n).prop_map(move |bits| {
            let mut defeats = Vec::new();
            for i in 0..n {
                for j in 0..n {
                    if bits[i * n + j] {
                        defeats.push((i, j));
                    }
                }
            }
            build_af(n, &defeats)
        })
    })
}

// --- Proptest smoke test ---

proptest! {
    #[test]
    fn smoke_arb_af_has_args(af in arb_af()) {
        prop_assert!(af.arguments.len() >= 2);
    }
}

// --- Targeted semantics tests ---

/// Semi-stable semantics — mutual defeat A0 ↔ A1.
/// Semi-stable extensions coincide with stable when stable exists.
/// Ref: Caminada, Carnielli & Dunne (2012).
#[test]
fn semi_stable_mutual_defeat() {
    let af = build_af(2, &[(0, 1), (1, 0)]);
    let exts = solver().extensions(&af, Semantics::SemiStable);
    assert_eq!(
        exts.len(),
        2,
        "mutual defeat should have 2 semi-stable extensions"
    );
    let s0: BTreeSet<_> = [ArgumentId(0)].into_iter().collect();
    let s1: BTreeSet<_> = [ArgumentId(1)].into_iter().collect();
    assert!(exts.contains(&s0));
    assert!(exts.contains(&s1));
}

/// Semi-stable semantics — 3-cycle A0 → A1 → A2 → A0.
/// No stable extension exists. The unique complete extension is ∅,
/// so the semi-stable extension is ∅.
/// Ref: Caminada, Carnielli & Dunne (2012).
#[test]
fn semi_stable_three_cycle() {
    let af = build_af(3, &[(0, 1), (1, 2), (2, 0)]);
    let exts = solver().extensions(&af, Semantics::SemiStable);
    assert_eq!(exts.len(), 1, "3-cycle should have 1 semi-stable extension");
    assert!(exts[0].is_empty(), "semi-stable of 3-cycle should be empty");
}

/// Ideal semantics — A0 ↔ A1 plus unattacked A2.
/// Preferred: {A0, A2} and {A1, A2}. Intersection: {A2}. {A2} is admissible.
/// So ideal = {A2}.
/// Ref: Dung, Mancarella & Toni (2007).
#[test]
fn ideal_with_unattacked() {
    let af = build_af(3, &[(0, 1), (1, 0)]);
    let exts = solver().extensions(&af, Semantics::Ideal);
    assert_eq!(exts.len(), 1, "ideal extension is unique");
    let expected: BTreeSet<_> = [ArgumentId(2)].into_iter().collect();
    assert_eq!(exts[0], expected, "ideal should be {{A2}}");
}

/// Eager semantics — A0 ↔ A1, A2 unattacked.
/// Semi-stable = stable = {A0, A2} and {A1, A2}. Intersection: {A2}.
/// Maximal admissible subset: {A2}. So eager = {A2}.
/// Ref: Caminada (2007).
#[test]
fn eager_with_unattacked() {
    let af = build_af(3, &[(0, 1), (1, 0)]);
    let exts = solver().extensions(&af, Semantics::Eager);
    assert_eq!(exts.len(), 1, "eager extension is unique");
    let expected: BTreeSet<_> = [ArgumentId(2)].into_iter().collect();
    assert_eq!(exts[0], expected, "eager should be {{A2}}");
}

/// Benchmark AF with exactly two preferred extensions and one grounded extension.
/// AF: A0 ↔ A1, A2 unattacked.
/// Grounded: {A2}. Preferred: {A0, A2} and {A1, A2}.
/// Verify grounded ⊆ both preferred extensions.
#[test]
fn benchmark_grounded_subset_of_preferred() {
    let af = build_af(3, &[(0, 1), (1, 0)]);
    let grounded = solver().extensions(&af, Semantics::Grounded);
    let preferred = solver().extensions(&af, Semantics::Preferred);

    assert_eq!(grounded.len(), 1);
    assert_eq!(
        preferred.len(),
        2,
        "should have exactly 2 preferred extensions"
    );

    let g = &grounded[0];
    for (i, p) in preferred.iter().enumerate() {
        assert!(
            g.is_subset(p),
            "grounded {g:?} should be a subset of preferred[{i}] {p:?}"
        );
    }
}

// --- Inter-semantics property tests ---

proptest! {
    /// For any AF, grounded ⊆ every preferred extension.
    /// Ref: Definition 3.1, Modgil & Prakken (2014).
    #[test]
    fn prop_grounded_subset_of_preferred(af in arb_af()) {
        let grounded = solver().extensions(&af, Semantics::Grounded);
        let preferred = solver().extensions(&af, Semantics::Preferred);
        prop_assert_eq!(grounded.len(), 1);
        let g = &grounded[0];
        for p in &preferred {
            prop_assert!(
                g.is_subset(p),
                "grounded {:?} not subset of preferred {:?}", g, p
            );
        }
    }

    /// For any AF, every stable extension is a preferred extension.
    /// Ref: Definition 3.1, Modgil & Prakken (2014).
    #[test]
    fn prop_stable_subset_of_preferred(af in arb_af()) {
        let stable = solver().extensions(&af, Semantics::Stable);
        let preferred = solver().extensions(&af, Semantics::Preferred);
        for s in &stable {
            prop_assert!(
                preferred.contains(s),
                "stable {:?} not in preferred set", s
            );
        }
    }

    /// For any AF, every preferred extension is a complete extension.
    /// Ref: Definition 3.1, Modgil & Prakken (2014).
    #[test]
    fn prop_preferred_is_complete(af in arb_af()) {
        let preferred = solver().extensions(&af, Semantics::Preferred);
        let complete = solver().extensions(&af, Semantics::Complete);
        for p in &preferred {
            prop_assert!(
                complete.contains(p),
                "preferred {:?} not in complete set", p
            );
        }
    }

    /// For any AF, the ideal extension is a subset of every preferred extension.
    /// Ref: Dung, Mancarella & Toni (2007).
    #[test]
    fn prop_ideal_subset_of_preferred(af in arb_af()) {
        let ideal = solver().extensions(&af, Semantics::Ideal);
        let preferred = solver().extensions(&af, Semantics::Preferred);
        prop_assert_eq!(ideal.len(), 1);
        let i = &ideal[0];
        for p in &preferred {
            prop_assert!(
                i.is_subset(p),
                "ideal {:?} not subset of preferred {:?}", i, p
            );
        }
    }
}

// --- Edge case tests ---

/// AF with a 3-cycle (odd cycle). Stable returns zero extensions;
/// all other semantics return at least one.
#[test]
fn odd_cycle_no_stable() {
    let af = build_af(3, &[(0, 1), (1, 2), (2, 0)]);

    let stable = solver().extensions(&af, Semantics::Stable);
    assert!(
        stable.is_empty(),
        "3-cycle should have no stable extensions"
    );

    for sem in [
        Semantics::Grounded,
        Semantics::Complete,
        Semantics::Preferred,
        Semantics::SemiStable,
        Semantics::Ideal,
        Semantics::Eager,
        Semantics::Admissible,
    ] {
        let exts = solver().extensions(&af, sem);
        assert!(
            !exts.is_empty(),
            "{sem:?} should return at least one extension for 3-cycle"
        );
    }
}

/// Self-attacking argument A0 → A0.
/// Grounded: ∅. Stable: zero extensions. Preferred: {∅}.
#[test]
fn self_attack_all_semantics() {
    let af = build_af(1, &[(0, 0)]);

    let grounded = solver().extensions(&af, Semantics::Grounded);
    assert_eq!(grounded.len(), 1);
    assert!(
        grounded[0].is_empty(),
        "grounded of self-attack should be empty"
    );

    let stable = solver().extensions(&af, Semantics::Stable);
    assert!(
        stable.is_empty(),
        "self-attack should have no stable extensions"
    );

    let preferred = solver().extensions(&af, Semantics::Preferred);
    assert_eq!(
        preferred.len(),
        1,
        "self-attack should have one preferred extension"
    );
    assert!(
        preferred[0].is_empty(),
        "preferred of self-attack should be empty"
    );
}

// --- Labelling property tests ---

proptest! {
    /// For any complete extension E, the derived labelling's In-arguments equal E.
    /// Ref: Caminada (2006).
    #[test]
    fn prop_labelling_in_args_eq_extension(af in arb_af()) {
        let exts = solver().extensions(&af, Semantics::Complete);
        for ext in &exts {
            let labelling = Labelling::from_extension(ext, &af);
            prop_assert_eq!(
                &labelling.in_args(), ext,
                "In-args {:?} != extension {:?}", labelling.in_args(), ext
            );
        }
    }

    /// For any stable extension, the derived labelling has no Undec arguments.
    /// Ref: Definition 3.1, Modgil & Prakken (2014).
    #[test]
    fn prop_stable_labelling_no_undec(af in arb_af()) {
        let exts = solver().extensions(&af, Semantics::Stable);
        for ext in &exts {
            let labelling = Labelling::from_extension(ext, &af);
            prop_assert!(
                labelling.undec_args().is_empty(),
                "stable labelling has Undec args: {:?}", labelling.undec_args()
            );
        }
    }

    /// For any complete extension, In ∪ Out ∪ Undec = AF arguments
    /// (labelling is a partition).
    /// Ref: Caminada (2006).
    #[test]
    fn prop_labelling_partitions_af(af in arb_af()) {
        let all_args = af.arguments.clone();
        let exts = solver().extensions(&af, Semantics::Complete);
        for ext in &exts {
            let labelling = Labelling::from_extension(ext, &af);
            let mut union = labelling.in_args();
            union.extend(labelling.out_args());
            union.extend(labelling.undec_args());
            prop_assert_eq!(
                union, all_args.clone(),
                "In ∪ Out ∪ Undec should equal AF arguments"
            );
        }
    }
}

// --- Abstract-level justification test ---

/// AF: A0 ↔ A1, A2 unattacked.
/// Preferred: {A0, A2} and {A1, A2}.
/// A2 is sceptically justified (in all preferred extensions).
/// A0 is credulously justified (in one but not all).
/// Ref: Definition 3.17, Modgil & Prakken (2014).
#[test]
fn justification_sceptical_and_credulous() {
    let af = build_af(3, &[(0, 1), (1, 0)]);
    let preferred = solver().extensions(&af, Semantics::Preferred);
    assert_eq!(preferred.len(), 2);

    let a0 = ArgumentId(0);
    let a2 = ArgumentId(2);

    let a2_in_all = preferred.iter().all(|ext| ext.contains(&a2));
    assert!(
        a2_in_all,
        "A2 should be sceptically justified (in all preferred)"
    );

    let a0_in_some = preferred.iter().any(|ext| ext.contains(&a0));
    let a0_in_all = preferred.iter().all(|ext| ext.contains(&a0));
    assert!(
        a0_in_some,
        "A0 should be in at least one preferred extension"
    );
    assert!(!a0_in_all, "A0 should NOT be in all preferred extensions");
}

// --- Solver completeness property test ---

proptest! {
    /// For any AF, the NaiveEnumerationSolver produces at least one extension
    /// for grounded, complete, preferred, semi-stable, ideal, and eager.
    /// Stable may return zero.
    #[test]
    fn prop_all_semantics_return_extensions(af in arb_af()) {
        for sem in [
            Semantics::Grounded,
            Semantics::Complete,
            Semantics::Preferred,
            Semantics::SemiStable,
            Semantics::Ideal,
            Semantics::Eager,
            Semantics::Admissible,
        ] {
            let exts = solver().extensions(&af, sem);
            prop_assert!(
                !exts.is_empty(),
                "{:?} returned no extensions for AF with {} args",
                sem, af.arguments.len()
            );
        }
    }
}

// --- Admissible semantics: targeted tests ---

/// Empty AF — the only admissible set is ∅.
/// Ref: Dung (1995), Definition 6.
#[test]
fn admissible_empty_af() {
    let af = build_af(0, &[]);
    let exts = solver().extensions(&af, Semantics::Admissible);
    assert_eq!(
        exts.len(),
        1,
        "empty AF should have exactly 1 admissible set"
    );
    assert!(exts[0].is_empty(), "the sole admissible set should be ∅");
}

/// Single unattacked argument A0 — admissible sets are ∅ and {A0}.
/// Ref: Dung (1995), Definition 6.
#[test]
fn admissible_single_unattacked() {
    let af = build_af(1, &[]);
    let exts = solver().extensions(&af, Semantics::Admissible);

    let empty: BTreeSet<ArgumentId> = BTreeSet::new();
    let singleton: BTreeSet<_> = [ArgumentId(0)].into_iter().collect();

    assert_eq!(exts.len(), 2, "should have exactly 2 admissible sets");
    assert!(exts.contains(&empty), "∅ should be admissible");
    assert!(exts.contains(&singleton), "{{A0}} should be admissible");
}

/// Mutual defeat A0 ↔ A1 — admissible sets are ∅, {A0}, {A1}.
/// Ref: Dung (1995), Definition 6.
#[test]
fn admissible_mutual_defeat() {
    let af = build_af(2, &[(0, 1), (1, 0)]);
    let exts = solver().extensions(&af, Semantics::Admissible);

    let empty: BTreeSet<ArgumentId> = BTreeSet::new();
    let s0: BTreeSet<_> = [ArgumentId(0)].into_iter().collect();
    let s1: BTreeSet<_> = [ArgumentId(1)].into_iter().collect();

    assert_eq!(exts.len(), 3, "should have exactly 3 admissible sets");
    assert!(exts.contains(&empty));
    assert!(exts.contains(&s0));
    assert!(exts.contains(&s1));
}

/// Chain A0 → A1 → A2 — admissible sets include ∅, {A0}, {A0, A2}.
/// A1 is attacked by A0 and undefended, so {A1} is not admissible.
/// A2 alone is attacked by A1 with no defender, so {A2} is not admissible.
/// {A0, A2} is admissible: A0 is unattacked, A2 is attacked by A1 which is
/// defeated by A0.
/// Ref: Dung (1995), Definition 6.
#[test]
fn admissible_chain() {
    let af = build_af(3, &[(0, 1), (1, 2)]);
    let exts = solver().extensions(&af, Semantics::Admissible);

    let empty: BTreeSet<ArgumentId> = BTreeSet::new();
    let s0: BTreeSet<_> = [ArgumentId(0)].into_iter().collect();
    let s02: BTreeSet<_> = [ArgumentId(0), ArgumentId(2)].into_iter().collect();

    assert!(exts.contains(&empty), "∅ should be admissible");
    assert!(exts.contains(&s0), "{{A0}} should be admissible");
    assert!(exts.contains(&s02), "{{A0, A2}} should be admissible");
    assert_eq!(
        exts.len(),
        3,
        "chain A0→A1→A2 should have exactly 3 admissible sets"
    );
}

/// Self-attack A0 → A0 — the only admissible set is ∅.
/// Ref: Dung (1995), Definition 6.
#[test]
fn admissible_self_attack() {
    let af = build_af(1, &[(0, 0)]);
    let exts = solver().extensions(&af, Semantics::Admissible);
    assert_eq!(
        exts.len(),
        1,
        "self-attack should have exactly 1 admissible set"
    );
    assert!(exts[0].is_empty(), "the sole admissible set should be ∅");
}

// --- Admissible semantics: property tests ---

proptest! {
    /// Every admissible set is conflict-free.
    /// Ref: Dung (1995), Definition 6.
    #[test]
    fn admissible_sets_are_conflict_free(af in arb_af()) {
        let exts = solver().extensions(&af, Semantics::Admissible);
        for ext in &exts {
            prop_assert!(
                af.is_conflict_free(ext),
                "admissible set {:?} is not conflict-free", ext
            );
        }
    }

    /// Every admissible set is self-defending.
    /// Ref: Dung (1995), Definition 6.
    #[test]
    fn admissible_sets_are_self_defending(af in arb_af()) {
        let exts = solver().extensions(&af, Semantics::Admissible);
        for ext in &exts {
            prop_assert!(
                af.is_admissible(ext),
                "set {:?} returned as admissible but is_admissible() returns false", ext
            );
        }
    }

    /// The empty set is always among the admissible extensions.
    /// Ref: Dung (1995), Definition 6.
    #[test]
    fn admissible_always_includes_empty_set(af in arb_af()) {
        let exts = solver().extensions(&af, Semantics::Admissible);
        let empty: BTreeSet<ArgumentId> = BTreeSet::new();
        prop_assert!(
            exts.contains(&empty),
            "∅ should always be admissible"
        );
    }
}

// --- Admissible semantics: labelling tests ---

/// Labelling for admissible extension {A0, A2} on chain A0 → A1 → A2.
/// A0=In, A1=Out, A2=In.
#[test]
fn admissible_labelling_chain() {
    let af = build_af(3, &[(0, 1), (1, 2)]);
    let ext: BTreeSet<_> = [ArgumentId(0), ArgumentId(2)].into_iter().collect();
    let labelling = Labelling::from_extension(&ext, &af);

    assert_eq!(labelling.label_of(ArgumentId(0)), Label::In);
    assert_eq!(labelling.label_of(ArgumentId(1)), Label::Out);
    assert_eq!(labelling.label_of(ArgumentId(2)), Label::In);
}

/// Labelling for the empty admissible extension — all arguments Undec.
#[test]
fn admissible_labelling_empty_extension() {
    let af = build_af(3, &[(0, 1), (1, 0)]);
    let empty: BTreeSet<ArgumentId> = BTreeSet::new();
    let labelling = Labelling::from_extension(&empty, &af);

    for &arg in &af.arguments {
        assert_eq!(
            labelling.label_of(arg),
            Label::Undec,
            "argument {:?} should be Undec in empty-extension labelling",
            arg
        );
    }
}

proptest! {
    /// For admissible extensions, In-arguments equal the extension
    /// and each Out-argument has at least one In defeater.
    #[test]
    fn admissible_labellings_are_consistent(af in arb_af()) {
        let exts = solver().extensions(&af, Semantics::Admissible);
        for ext in &exts {
            let labelling = Labelling::from_extension(ext, &af);
            prop_assert_eq!(
                &labelling.in_args(), ext,
                "In-args should equal admissible extension"
            );
            for &out_arg in &labelling.out_args() {
                let has_in_defeater = ext.iter().any(|&a| af.defeats(a, out_arg));
                prop_assert!(
                    has_in_defeater,
                    "Out-argument {:?} has no In defeater", out_arg
                );
            }
        }
    }
}

// --- Admissible semantics: inter-semantics property tests ---

proptest! {
    /// Every complete extension is among the admissible sets.
    /// Ref: Dung (1995), Fundamental Lemma.
    #[test]
    fn admissible_complete_extensions_are_admissible(af in arb_af()) {
        let admissible = solver().extensions(&af, Semantics::Admissible);
        let complete = solver().extensions(&af, Semantics::Complete);
        for c in &complete {
            prop_assert!(
                admissible.contains(c),
                "complete extension {:?} not among admissible sets", c
            );
        }
    }

    /// Every preferred extension is among the admissible sets.
    /// Ref: Dung (1995), Fundamental Lemma.
    #[test]
    fn admissible_preferred_extensions_are_admissible(af in arb_af()) {
        let admissible = solver().extensions(&af, Semantics::Admissible);
        let preferred = solver().extensions(&af, Semantics::Preferred);
        for p in &preferred {
            prop_assert!(
                admissible.contains(p),
                "preferred extension {:?} not among admissible sets", p
            );
        }
    }
}

// --- Cross-solver equivalence ---

#[cfg(feature = "sat")]
proptest! {
    /// SCC-decomposed admissible must produce the same extensions as naive.
    #[test]
    fn scc_admissible_matches_naive(af in arb_af()) {
        let naive = sorted_exts(solver().extensions(&af, Semantics::Admissible));
        let scc = sorted_exts(scc_solver().extensions(&af, Semantics::Admissible));
        prop_assert_eq!(naive, scc, "SCC admissible differs from naive");
    }

    /// SAT solver admissible (now classical dispatch) must match naive.
    #[test]
    fn sat_admissible_matches_naive(af in arb_af()) {
        let naive = sorted_exts(solver().extensions(&af, Semantics::Admissible));
        let sat = sorted_exts(sat_solver().extensions(&af, Semantics::Admissible));
        prop_assert_eq!(naive, sat, "SAT admissible differs from naive");
    }

    /// SCC-optimised ideal must produce the same extension as naive.
    #[test]
    fn scc_ideal_matches_naive(af in arb_af()) {
        let naive = sorted_exts(solver().extensions(&af, Semantics::Ideal));
        let scc = sorted_exts(scc_solver().extensions(&af, Semantics::Ideal));
        prop_assert_eq!(naive, scc, "SCC ideal differs from naive");
    }
}
