//! Accrual evaluator implementing Prakken (2019) accrual semantics.
//!
//! This evaluator computes labelling-relative defeat and extensions via
//! fixpoint iteration of the characteristic function F (Definition 4.6).
//! Unlike [`ClassicalEvaluator`](super::classical::ClassicalEvaluator),
//! it does not delegate to an `AbstractFramework` or `SemanticsSolver` —
//! the fixpoint computation replaces them entirely.
//!
//! # Formal Reference
//!
//! Prakken, H. (2019). *Modelling Accrual of Arguments in ASPIC+*.
//! In Proc. ICAIL '19, pp. 103–112. ACM.
//!
//! Key definitions implemented:
//! - Accrual sets: Definition 4.1
//! - l-defeat: Definition 4.4 (generalised for undermining)
//! - Characteristic function F: Definition 4.6
//! - Monotonicity: Proposition 5.2
//! - Reduction to ASPIC+: Proposition 5.5

use std::collections::{BTreeSet, HashMap};

use crate::framework::argument::{Argument, ArgumentId};
use crate::framework::argument_store::ArgumentStore;
use crate::framework::attack::{Attack, AttackKind};
use crate::framework::semantics::{Extension, Label, Labelling, Semantics};
use crate::pipeline::traits::{EvaluationResult, Evaluator, PreferenceConfig};
use crate::system::ordering::{Preference, SetPreference};

use crate::error::{AspicError, SolverError};

const POWERSET_LIMIT: usize = 64;

// ───────────────────────────────────────────────────────────────────────
// Public API
// ───────────────────────────────────────────────────────────────────────

/// Evaluator implementing Prakken (2019) accrual semantics.
///
/// The `SetPreference` used for l-defeat computation is supplied via
/// [`PreferenceConfig::SetPreference`] at evaluation time.
pub struct AccrualEvaluator;

impl Evaluator for AccrualEvaluator {
    fn find_one(
        &self,
        store: &ArgumentStore,
        attacks: &[Attack],
        semantics: Semantics,
        preference: &PreferenceConfig,
    ) -> Result<EvaluationResult, AspicError> {
        let set_preference = preference.as_set_preference().ok_or_else(|| {
            AspicError::from(SolverError::UnsupportedSemantics(
                "AccrualEvaluator requires a SetPreference, not an ArgumentOrdering".into(),
            ))
        })?;
        let p_attacks = PAttackIndex::build(attacks);
        let all_args: Vec<ArgumentId> = store.all_arguments().map(|(id, _)| id).collect();

        let grounded = compute_grounded(&all_args, store, &p_attacks, set_preference)?;

        match semantics {
            Semantics::Grounded => Ok(labelling_to_result(vec![grounded], &all_args)),
            Semantics::Complete => {
                let one = find_one_complete_labelling(
                    &grounded,
                    &all_args,
                    store,
                    &p_attacks,
                    set_preference,
                )?;
                Ok(labelling_to_result(
                    one.map(|l| vec![l]).unwrap_or_default(),
                    &all_args,
                ))
            }
            Semantics::Preferred => {
                let complete =
                    compute_complete(&grounded, &all_args, store, &p_attacks, set_preference)?;
                let preferred = filter_maximal(complete);
                let first = preferred.into_iter().next();
                Ok(labelling_to_result(
                    first.map(|l| vec![l]).unwrap_or_default(),
                    &all_args,
                ))
            }
            Semantics::Stable => {
                let complete =
                    compute_complete(&grounded, &all_args, store, &p_attacks, set_preference)?;
                let stable = complete.into_iter().find(|l| l.undec_set().is_empty());
                Ok(labelling_to_result(
                    stable.map(|l| vec![l]).unwrap_or_default(),
                    &all_args,
                ))
            }
            Semantics::SemiStable => {
                let complete =
                    compute_complete(&grounded, &all_args, store, &p_attacks, set_preference)?;
                let semi_stable = filter_semi_stable(complete);
                let first = semi_stable.into_iter().next();
                Ok(labelling_to_result(
                    first.map(|l| vec![l]).unwrap_or_default(),
                    &all_args,
                ))
            }
            Semantics::Ideal => {
                let complete =
                    compute_complete(&grounded, &all_args, store, &p_attacks, set_preference)?;
                let preferred = filter_maximal(complete);
                let ideal =
                    compute_ideal(&preferred, &all_args, store, &p_attacks, set_preference)?;
                Ok(labelling_to_result(vec![ideal], &all_args))
            }
            Semantics::Eager => {
                let complete =
                    compute_complete(&grounded, &all_args, store, &p_attacks, set_preference)?;
                let semi_stable = filter_semi_stable(complete);
                let eager =
                    compute_eager(&semi_stable, &all_args, store, &p_attacks, set_preference)?;
                Ok(labelling_to_result(vec![eager], &all_args))
            }
            Semantics::Admissible => Err(SolverError::UnsupportedSemantics(
                "Admissible semantics is not supported by the accrual evaluator; \
                 use ClassicalEvaluator instead"
                    .into(),
            )
            .into()),
        }
    }

    fn evaluate(
        &self,
        store: &ArgumentStore,
        attacks: &[Attack],
        semantics: Semantics,
        preference: &PreferenceConfig,
    ) -> Result<EvaluationResult, AspicError> {
        let set_preference = preference.as_set_preference().ok_or_else(|| {
            AspicError::from(SolverError::UnsupportedSemantics(
                "AccrualEvaluator requires a SetPreference, not an ArgumentOrdering".into(),
            ))
        })?;
        let p_attacks = PAttackIndex::build(attacks);
        let all_args: Vec<ArgumentId> = store.all_arguments().map(|(id, _)| id).collect();

        let grounded = compute_grounded(&all_args, store, &p_attacks, set_preference)?;

        match semantics {
            Semantics::Grounded => Ok(labelling_to_result(vec![grounded], &all_args)),
            Semantics::Complete => {
                let complete =
                    compute_complete(&grounded, &all_args, store, &p_attacks, set_preference)?;
                Ok(labelling_to_result(complete, &all_args))
            }
            Semantics::Preferred => {
                let complete =
                    compute_complete(&grounded, &all_args, store, &p_attacks, set_preference)?;
                let preferred = filter_maximal(complete);
                Ok(labelling_to_result(preferred, &all_args))
            }
            Semantics::Stable => {
                let complete =
                    compute_complete(&grounded, &all_args, store, &p_attacks, set_preference)?;
                let stable = complete
                    .into_iter()
                    .filter(|l| l.undec_set().is_empty())
                    .collect();
                Ok(labelling_to_result(stable, &all_args))
            }
            Semantics::SemiStable => {
                let complete =
                    compute_complete(&grounded, &all_args, store, &p_attacks, set_preference)?;
                let semi_stable = filter_semi_stable(complete);
                Ok(labelling_to_result(semi_stable, &all_args))
            }
            Semantics::Ideal => {
                let complete =
                    compute_complete(&grounded, &all_args, store, &p_attacks, set_preference)?;
                let preferred = filter_maximal(complete);
                let ideal =
                    compute_ideal(&preferred, &all_args, store, &p_attacks, set_preference)?;
                Ok(labelling_to_result(vec![ideal], &all_args))
            }
            Semantics::Eager => {
                let complete =
                    compute_complete(&grounded, &all_args, store, &p_attacks, set_preference)?;
                let semi_stable = filter_semi_stable(complete.clone());
                let eager =
                    compute_eager(&semi_stable, &all_args, store, &p_attacks, set_preference)?;
                Ok(labelling_to_result(vec![eager], &all_args))
            }
            Semantics::Admissible => Err(SolverError::UnsupportedSemantics(
                "Admissible semantics is not supported by the accrual evaluator; \
                 use ClassicalEvaluator instead"
                    .into(),
            )
            .into()),
        }
    }

    fn count(
        &self,
        store: &ArgumentStore,
        attacks: &[Attack],
        semantics: Semantics,
        preference: &PreferenceConfig,
    ) -> Result<usize, AspicError> {
        let set_preference = preference.as_set_preference().ok_or_else(|| {
            AspicError::from(SolverError::UnsupportedSemantics(
                "AccrualEvaluator requires a SetPreference, not an ArgumentOrdering".into(),
            ))
        })?;
        let p_attacks = PAttackIndex::build(attacks);
        let all_args: Vec<ArgumentId> = store.all_arguments().map(|(id, _)| id).collect();
        let grounded = compute_grounded(&all_args, store, &p_attacks, set_preference)?;

        match semantics {
            Semantics::Grounded | Semantics::Ideal | Semantics::Eager => Ok(1),
            Semantics::Complete => {
                let complete =
                    compute_complete(&grounded, &all_args, store, &p_attacks, set_preference)?;
                Ok(complete.len())
            }
            Semantics::Preferred => {
                let complete =
                    compute_complete(&grounded, &all_args, store, &p_attacks, set_preference)?;
                Ok(filter_maximal(complete).len())
            }
            Semantics::Stable => {
                let complete =
                    compute_complete(&grounded, &all_args, store, &p_attacks, set_preference)?;
                Ok(complete.iter().filter(|l| l.undec_set().is_empty()).count())
            }
            Semantics::SemiStable => {
                let complete =
                    compute_complete(&grounded, &all_args, store, &p_attacks, set_preference)?;
                Ok(filter_semi_stable(complete).len())
            }
            Semantics::Admissible => Err(SolverError::UnsupportedSemantics(
                "Admissible semantics is not supported by the accrual evaluator; \
                 use ClassicalEvaluator instead"
                    .into(),
            )
            .into()),
        }
    }
}

// ───────────────────────────────────────────────────────────────────────
// p-Attack types (Definition 2.6, generalised for undermining)
// ───────────────────────────────────────────────────────────────────────

#[derive(Clone, Debug)]
enum PAttackKind {
    Undercut,
    Rebut { contrary: bool },
    Undermine { contrary: bool },
}

#[derive(Clone, Debug)]
struct PAttack {
    attacker: ArgumentId,
    kind: PAttackKind,
}

/// Index of p-attacks by target argument.
///
/// Built from standard ASPIC+ attacks by extracting the sub-argument
/// or premise target (not the top-level target) as the p-attack target.
struct PAttackIndex {
    by_target: HashMap<ArgumentId, Vec<PAttack>>,
}

impl PAttackIndex {
    /// Build a p-attack index from standard ASPIC+ attacks (Research R1).
    fn build(attacks: &[Attack]) -> Self {
        let mut by_target: HashMap<ArgumentId, Vec<PAttack>> = HashMap::new();
        for attack in attacks {
            let (target, kind) = match &attack.kind {
                AttackKind::Undercut { target_sub, .. } => (*target_sub, PAttackKind::Undercut),
                AttackKind::Rebut {
                    target_sub,
                    contrary,
                } => (
                    *target_sub,
                    PAttackKind::Rebut {
                        contrary: *contrary,
                    },
                ),
                AttackKind::Undermine {
                    target_premise,
                    contrary,
                } => (
                    *target_premise,
                    PAttackKind::Undermine {
                        contrary: *contrary,
                    },
                ),
            };
            by_target.entry(target).or_default().push(PAttack {
                attacker: attack.attacker,
                kind,
            });
        }
        PAttackIndex { by_target }
    }

    fn attackers_of(&self, target: ArgumentId) -> &[PAttack] {
        self.by_target
            .get(&target)
            .map_or(&[], std::vec::Vec::as_slice)
    }

    fn undercutters_of(&self, target: ArgumentId) -> impl Iterator<Item = ArgumentId> + '_ {
        self.attackers_of(target)
            .iter()
            .filter(|p| matches!(p.kind, PAttackKind::Undercut))
            .map(|p| p.attacker)
    }
}

// ───────────────────────────────────────────────────────────────────────
// AccrualLabelling (Definition 2.10)
// ───────────────────────────────────────────────────────────────────────

#[derive(Clone, Debug)]
struct AccrualLabelling {
    labels: HashMap<ArgumentId, Label>,
}

impl AccrualLabelling {
    fn empty(all_args: &[ArgumentId]) -> Self {
        let labels = all_args.iter().map(|&id| (id, Label::Undec)).collect();
        AccrualLabelling { labels }
    }

    fn is_in(&self, id: ArgumentId) -> bool {
        self.labels.get(&id) == Some(&Label::In)
    }

    fn is_out(&self, id: ArgumentId) -> bool {
        self.labels.get(&id) == Some(&Label::Out)
    }

    fn in_set(&self) -> BTreeSet<ArgumentId> {
        self.labels
            .iter()
            .filter(|(_, l)| **l == Label::In)
            .map(|(id, _)| *id)
            .collect()
    }

    fn undec_set(&self) -> BTreeSet<ArgumentId> {
        self.labels
            .iter()
            .filter(|(_, l)| **l == Label::Undec)
            .map(|(id, _)| *id)
            .collect()
    }

    fn to_labelling(&self) -> Labelling {
        Labelling::new(self.labels.clone())
    }

    fn to_extension(&self) -> Extension {
        self.in_set()
    }
}

impl PartialEq for AccrualLabelling {
    fn eq(&self, other: &Self) -> bool {
        self.labels == other.labels
    }
}

// ───────────────────────────────────────────────────────────────────────
// Applicability (Definition 4.1 conditions)
// ───────────────────────────────────────────────────────────────────────

/// Strongly applicable: all undercutters are Out AND all `ImmSub` are In.
fn is_strongly_applicable(
    arg: &Argument,
    labelling: &AccrualLabelling,
    p_attacks: &PAttackIndex,
) -> bool {
    let id = arg.id();
    let all_undercutters_out = p_attacks.undercutters_of(id).all(|u| labelling.is_out(u));
    if !all_undercutters_out {
        return false;
    }
    arg.direct_sub_ids().iter().all(|&sub| labelling.is_in(sub))
}

/// Weakly applicable: no undercutter is In AND no `ImmSub` is Out.
/// (Does NOT include strongly applicable — caller must subtract.)
fn is_weakly_applicable(
    arg: &Argument,
    labelling: &AccrualLabelling,
    p_attacks: &PAttackIndex,
) -> bool {
    let id = arg.id();
    let no_undercutter_in = p_attacks.undercutters_of(id).all(|u| !labelling.is_in(u));
    if !no_undercutter_in {
        return false;
    }
    arg.direct_sub_ids()
        .iter()
        .all(|&sub| !labelling.is_out(sub))
}

// ───────────────────────────────────────────────────────────────────────
// Accrual set computation (Definition 4.1)
// ───────────────────────────────────────────────────────────────────────

/// Compute all accrual sets for a conclusion under the given labelling.
///
/// Returns a vec of accrual sets. In the common case (no weakly applicable
/// arguments), returns a single set containing all strongly applicable args.
fn accrual_sets_for(
    conclusion: &crate::language::formula::Formula,
    labelling: &AccrualLabelling,
    store: &ArgumentStore,
    p_attacks: &PAttackIndex,
) -> Result<Vec<BTreeSet<ArgumentId>>, AspicError> {
    let arg_ids = store.arguments_for(conclusion);

    let mut strong = BTreeSet::new();
    let mut weak = Vec::new();

    for &aid in arg_ids {
        if let Some(arg) = store.get(aid) {
            if is_strongly_applicable(arg, labelling, p_attacks) {
                strong.insert(aid);
            } else if is_weakly_applicable(arg, labelling, p_attacks) {
                weak.push(aid);
            }
        }
    }

    if strong.is_empty() && weak.is_empty() {
        return Ok(vec![]);
    }

    if weak.is_empty() {
        return Ok(vec![strong]);
    }

    let n = weak.len();
    if n >= POWERSET_LIMIT {
        return Err(SolverError::PowersetLimitExceeded {
            count: n,
            limit: POWERSET_LIMIT,
        }
        .into());
    }

    let mut result = Vec::new();
    for mask in 0..(1u64 << n) {
        let mut set = strong.clone();
        for (i, &w) in weak.iter().enumerate() {
            if mask & (1u64 << i) != 0 {
                set.insert(w);
            }
        }
        if !set.is_empty() {
            result.push(set);
        }
    }
    Ok(result)
}

// ───────────────────────────────────────────────────────────────────────
// l-defeat (Definition 4.4, generalised for undermining)
// ───────────────────────────────────────────────────────────────────────

/// Check if attacker l-defeats target under the given labelling.
///
/// Cases:
/// 1. Undercut: always succeeds.
/// 2. Rebut (contrary): always succeeds.
/// 3. Rebut (non-contrary): succeeds iff some pair of accrual sets
///    for Conc(A) and Conc(B) has A's set not strictly dispreferred.
/// 4. Undermine (contrary): always succeeds.
/// 5. Undermine (non-contrary): same logic as rebut.
fn l_defeats(
    p_attack: &PAttack,
    target: ArgumentId,
    labelling: &AccrualLabelling,
    store: &ArgumentStore,
    p_attacks: &PAttackIndex,
    set_preference: &dyn SetPreference,
) -> Result<bool, AspicError> {
    match &p_attack.kind {
        PAttackKind::Undercut => Ok(true),
        PAttackKind::Rebut { contrary } | PAttackKind::Undermine { contrary } => {
            if *contrary {
                return Ok(true);
            }
            let attacker_conc = store.get(p_attack.attacker).map(|a| a.conclusion().clone());
            let target_conc = store.get(target).map(|a| a.conclusion().clone());

            if let (Some(a_conc), Some(t_conc)) = (attacker_conc, target_conc) {
                let a_sets = accrual_sets_for(&a_conc, labelling, store, p_attacks)?;
                let t_sets = accrual_sets_for(&t_conc, labelling, store, p_attacks)?;

                for a_set in &a_sets {
                    for t_set in &t_sets {
                        let pref = set_preference.compare(a_set, t_set, store);
                        if pref != Preference::StrictlyDispreferred {
                            return Ok(true);
                        }
                    }
                }
                Ok(false)
            } else {
                Ok(false)
            }
        }
    }
}

// ───────────────────────────────────────────────────────────────────────
// Characteristic function F (Definition 4.6)
// ───────────────────────────────────────────────────────────────────────

/// Compute F(l) — one iteration of the characteristic function.
///
/// For each argument A:
/// - A ∈ In' iff all l-defeaters of A are in Out AND all ImmSub(A) are in In.
/// - A ∈ Out' iff some l-defeater of A is in In OR some ImmSub(A) is in Out.
/// - Otherwise A is Undec.
fn apply_f(
    labelling: &AccrualLabelling,
    all_args: &[ArgumentId],
    store: &ArgumentStore,
    p_attacks: &PAttackIndex,
    set_preference: &dyn SetPreference,
) -> Result<AccrualLabelling, AspicError> {
    let mut new_labels = HashMap::new();

    for &arg_id in all_args {
        let Some(arg) = store.get(arg_id) else {
            continue;
        };

        let imm_subs = arg.direct_sub_ids();
        let all_imm_sub_in = imm_subs.iter().all(|&s| labelling.is_in(s));
        let some_imm_sub_out = imm_subs.iter().any(|&s| labelling.is_out(s));

        let p_attackers = p_attacks.attackers_of(arg_id);

        let mut all_defeaters_out = true;
        for pa in p_attackers {
            if l_defeats(pa, arg_id, labelling, store, p_attacks, set_preference)?
                && !labelling.is_out(pa.attacker)
            {
                all_defeaters_out = false;
            }
        }

        let mut some_defeater_in = false;
        for pa in p_attackers {
            if l_defeats(pa, arg_id, labelling, store, p_attacks, set_preference)?
                && labelling.is_in(pa.attacker)
            {
                some_defeater_in = true;
                break;
            }
        }

        let label = if all_defeaters_out && all_imm_sub_in {
            Label::In
        } else if some_defeater_in || some_imm_sub_out {
            Label::Out
        } else {
            Label::Undec
        };

        new_labels.insert(arg_id, label);
    }

    Ok(AccrualLabelling { labels: new_labels })
}

// ───────────────────────────────────────────────────────────────────────
// Grounded l-labelling (least fixpoint of F)
// ───────────────────────────────────────────────────────────────────────

/// Compute the grounded l-labelling as the least fixpoint of the
/// characteristic function F (Definition 4.6, Prakken 2019).
///
/// Starting from the all-Undec labelling, F is applied iteratively until
/// the labelling stabilises. Monotonicity of F (Proposition 5.2) guarantees
/// convergence in at most |Args| steps; the bounded loop is a defensive
/// guard against unexpected non-convergence.
fn compute_grounded(
    all_args: &[ArgumentId],
    store: &ArgumentStore,
    p_attacks: &PAttackIndex,
    set_preference: &dyn SetPreference,
) -> Result<AccrualLabelling, AspicError> {
    let mut current = AccrualLabelling::empty(all_args);

    for _ in 0..=all_args.len() {
        let next = apply_f(&current, all_args, store, p_attacks, set_preference)?;
        if next == current {
            return Ok(current);
        }
        current = next;
    }

    Ok(current)
}

// ───────────────────────────────────────────────────────────────────────
// Complete l-labellings (all fixpoints of F)
// ───────────────────────────────────────────────────────────────────────

#[allow(clippy::cast_possible_truncation)]
fn compute_complete(
    grounded: &AccrualLabelling,
    all_args: &[ArgumentId],
    store: &ArgumentStore,
    p_attacks: &PAttackIndex,
    set_preference: &dyn SetPreference,
) -> Result<Vec<AccrualLabelling>, AspicError> {
    let undec: Vec<ArgumentId> = grounded.undec_set().into_iter().collect();

    if undec.is_empty() {
        return Ok(vec![grounded.clone()]);
    }

    let n = undec.len();
    let mut results = Vec::new();

    let total = 3u128.checked_pow(n as u32).unwrap_or(u128::MAX);

    for candidate_idx in 0..total {
        let mut labels = grounded.labels.clone();
        let mut idx = candidate_idx;

        for &arg in &undec {
            let choice = idx % 3;
            idx /= 3;
            match choice {
                1 => {
                    labels.insert(arg, Label::In);
                }
                2 => {
                    labels.insert(arg, Label::Out);
                }
                _ => {}
            }
        }

        let candidate = AccrualLabelling { labels };
        let applied = apply_f(&candidate, all_args, store, p_attacks, set_preference)?;

        if applied == candidate {
            results.push(candidate);
        }
    }

    if results.is_empty() {
        results.push(grounded.clone());
    }

    Ok(results)
}

/// Find the first complete l-labelling (fixpoint of F), if any.
///
/// Same search as `compute_complete` but returns as soon as the first
/// fixpoint is found, avoiding full enumeration when only one is needed.
#[allow(clippy::cast_possible_truncation)]
fn find_one_complete_labelling(
    grounded: &AccrualLabelling,
    all_args: &[ArgumentId],
    store: &ArgumentStore,
    p_attacks: &PAttackIndex,
    set_preference: &dyn SetPreference,
) -> Result<Option<AccrualLabelling>, AspicError> {
    let undec: Vec<ArgumentId> = grounded.undec_set().into_iter().collect();
    if undec.is_empty() {
        return Ok(Some(grounded.clone()));
    }
    let n = undec.len();
    let total = 3u128.checked_pow(n as u32).unwrap_or(u128::MAX);

    for candidate_idx in 0..total {
        let mut labels = grounded.labels.clone();
        let mut idx = candidate_idx;

        for &arg in &undec {
            let choice = idx % 3;
            idx /= 3;
            match choice {
                1 => {
                    labels.insert(arg, Label::In);
                }
                2 => {
                    labels.insert(arg, Label::Out);
                }
                _ => {}
            }
        }

        let candidate = AccrualLabelling { labels };
        let applied = apply_f(&candidate, all_args, store, p_attacks, set_preference)?;

        if applied == candidate {
            return Ok(Some(candidate));
        }
    }

    Ok(None)
}

// ───────────────────────────────────────────────────────────────────────
// Preferred l-labellings (⊆-maximal In-sets)
// ───────────────────────────────────────────────────────────────────────

fn filter_maximal(labellings: Vec<AccrualLabelling>) -> Vec<AccrualLabelling> {
    crate::algorithms::maximal::retain_maximal_by(labellings, AccrualLabelling::in_set)
}

// ───────────────────────────────────────────────────────────────────────
// Semi-stable l-labellings (minimise Undec)
// ───────────────────────────────────────────────────────────────────────

fn filter_semi_stable(complete: Vec<AccrualLabelling>) -> Vec<AccrualLabelling> {
    if complete.is_empty() {
        return vec![];
    }

    let undec_sizes: Vec<usize> = complete.iter().map(|l| l.undec_set().len()).collect();
    let min_undec = *undec_sizes.iter().min().unwrap();

    complete
        .into_iter()
        .zip(undec_sizes)
        .filter(|(_, size)| *size == min_undec)
        .map(|(l, _)| l)
        .collect()
}

// ───────────────────────────────────────────────────────────────────────
// Ideal l-labelling
// ───────────────────────────────────────────────────────────────────────

fn compute_ideal(
    preferred: &[AccrualLabelling],
    all_args: &[ArgumentId],
    store: &ArgumentStore,
    p_attacks: &PAttackIndex,
    set_preference: &dyn SetPreference,
) -> Result<AccrualLabelling, AspicError> {
    if preferred.is_empty() {
        return Ok(AccrualLabelling::empty(all_args));
    }

    let mut intersection: BTreeSet<ArgumentId> = preferred[0].in_set();
    for pref in &preferred[1..] {
        intersection = intersection.intersection(&pref.in_set()).copied().collect();
    }

    find_largest_admissible_within(&intersection, all_args, store, p_attacks, set_preference)
}

// ───────────────────────────────────────────────────────────────────────
// Eager l-labelling
// ───────────────────────────────────────────────────────────────────────

fn compute_eager(
    semi_stable: &[AccrualLabelling],
    all_args: &[ArgumentId],
    store: &ArgumentStore,
    p_attacks: &PAttackIndex,
    set_preference: &dyn SetPreference,
) -> Result<AccrualLabelling, AspicError> {
    if semi_stable.is_empty() {
        return Ok(AccrualLabelling::empty(all_args));
    }

    let mut intersection: BTreeSet<ArgumentId> = semi_stable[0].in_set();
    for ss in &semi_stable[1..] {
        intersection = intersection.intersection(&ss.in_set()).copied().collect();
    }

    find_largest_admissible_within(&intersection, all_args, store, p_attacks, set_preference)
}

/// Find the largest admissible l-labelling whose In-set is a subset of `candidates`.
fn find_largest_admissible_within(
    candidates: &BTreeSet<ArgumentId>,
    all_args: &[ArgumentId],
    store: &ArgumentStore,
    p_attacks: &PAttackIndex,
    set_preference: &dyn SetPreference,
) -> Result<AccrualLabelling, AspicError> {
    let candidate_vec: Vec<ArgumentId> = candidates.iter().copied().collect();
    let n = candidate_vec.len().min(20);

    let mut best: Option<AccrualLabelling> = None;
    let mut best_size = 0;

    for mask in 0..(1u64 << n) {
        let mut in_set = BTreeSet::new();
        for (i, &arg) in candidate_vec.iter().take(n).enumerate() {
            if mask & (1u64 << i) != 0 {
                in_set.insert(arg);
            }
        }

        let mut labels = HashMap::new();
        for &arg in all_args {
            if in_set.contains(&arg) {
                labels.insert(arg, Label::In);
            } else {
                labels.insert(arg, Label::Undec);
            }
        }

        let labelling = AccrualLabelling {
            labels: labels.clone(),
        };
        for &arg in all_args {
            if in_set.contains(&arg) {
                continue;
            }
            let p_attackers = p_attacks.attackers_of(arg);
            let mut defeated_by_in = false;
            for pa in p_attackers {
                if in_set.contains(&pa.attacker)
                    && l_defeats(pa, arg, &labelling, store, p_attacks, set_preference)?
                {
                    defeated_by_in = true;
                    break;
                }
            }
            if defeated_by_in {
                labels.insert(arg, Label::Out);
            }
        }
        let labelling = AccrualLabelling { labels };

        let applied = apply_f(&labelling, all_args, store, p_attacks, set_preference)?;
        if applied == labelling && in_set.len() > best_size {
            best_size = in_set.len();
            best = Some(labelling);
        }
    }

    Ok(best.unwrap_or_else(|| AccrualLabelling::empty(all_args)))
}

// ───────────────────────────────────────────────────────────────────────
// Conversion helpers
// ───────────────────────────────────────────────────────────────────────

fn labelling_to_result(
    accrual_labellings: Vec<AccrualLabelling>,
    all_args: &[ArgumentId],
) -> EvaluationResult {
    if accrual_labellings.is_empty() {
        return EvaluationResult {
            labellings: vec![],
            extensions: vec![],
        };
    }

    let mut labellings = Vec::new();
    let mut extensions = Vec::new();

    for al in accrual_labellings {
        let mut final_labels = HashMap::new();
        for &arg in all_args {
            final_labels.insert(arg, al.labels.get(&arg).cloned().unwrap_or(Label::Undec));
        }
        let full_labelling = AccrualLabelling {
            labels: final_labels,
        };
        extensions.push(full_labelling.to_extension());
        labellings.push(full_labelling.to_labelling());
    }

    EvaluationResult {
        labellings,
        extensions,
    }
}
