//! SCC-decomposing semantics solver.
//!
//! [`SccDecomposingSolver`] partitions the abstract argumentation framework
//! into its strongly connected components (via Tarjan's algorithm) and solves
//! each component independently, composing partial extensions bottom-up in
//! topological order. This avoids exponential blowup on frameworks where
//! most arguments are in separate, acyclic regions — a common pattern in
//! ASPIC+ systems with many independent inference chains.
//!
//! The decomposition is exact for grounded, complete, preferred, stable, and
//! admissible semantics (Baroni, Giacomin & Guida, 2005). For ideal
//! semantics, preferred extensions are computed via SCC recursion and the
//! ideal extension is derived as the maximal admissible subset of their
//! intersection. Semantics that are not SCC-recursive (semi-stable, eager)
//! fall back to the inner solver on the full framework.

use std::collections::BTreeSet;

use crate::framework::abstract_af::AbstractFramework;
use crate::framework::argument::ArgumentId;
use crate::framework::semantics::{Extension, Semantics};
use crate::pipeline::traits::SemanticsSolver;

/// Semantics solver that decomposes the framework by strongly connected
/// components and solves each independently, composing results bottom-up.
///
/// Wraps any `SemanticsSolver` as the inner delegate. For grounded,
/// complete, preferred, stable, and admissible semantics the decomposition
/// is exact (Baroni, Giacomin & Guida 2005; Baumann et al.; Liao et al.).
///
/// For ideal semantics, the solver computes preferred extensions via SCC
/// decomposition and then derives the ideal extension as the maximal
/// admissible subset of their intersection.
///
/// For semantics that are not SCC-recursive (`SemiStable`, Eager), falls
/// back to calling the inner solver on the full framework.
pub struct SccDecomposingSolver {
    pub inner: Box<dyn SemanticsSolver>,
}

impl SemanticsSolver for SccDecomposingSolver {
    fn extensions(&self, af: &AbstractFramework, sem: Semantics) -> Vec<Extension> {
        match sem {
            Semantics::Preferred
            | Semantics::Stable
            | Semantics::Complete
            | Semantics::Grounded
            | Semantics::Admissible => self.scc_recursive(af, sem),
            Semantics::Ideal => self.compute_ideal(af),
            _ => self.inner.extensions(af, sem),
        }
    }

    fn find_one(&self, af: &AbstractFramework, sem: Semantics) -> Option<Extension> {
        match sem {
            Semantics::Preferred
            | Semantics::Stable
            | Semantics::Complete
            | Semantics::Grounded
            | Semantics::Admissible => self.scc_find_one(af, sem),
            Semantics::Ideal | Semantics::Eager => self.extensions(af, sem).into_iter().next(),
            Semantics::SemiStable => self.inner.find_one(af, sem),
        }
    }
}

impl SccDecomposingSolver {
    /// SCC-recursive `find_one`: process SCCs in topological order, call
    /// `inner.find_one` at each SCC, take the first compatible partial
    /// extension and proceed. Early-terminates once a single consistent
    /// partial extension is found through all SCCs.
    fn scc_find_one(&self, af: &AbstractFramework, sem: Semantics) -> Option<Extension> {
        let sccs = af.sccs();

        if sccs.len() <= 1 {
            return self.inner.find_one(af, sem);
        }

        let sccs: Vec<BTreeSet<ArgumentId>> = sccs.into_iter().rev().collect();

        let mut resolved: BTreeSet<ArgumentId> = BTreeSet::new();
        let mut partial_extensions: Vec<Extension> = vec![BTreeSet::new()];

        for scc in &sccs {
            let mut found_one: Option<Extension> = None;

            for partial in &partial_extensions {
                if found_one.is_some() {
                    break;
                }

                let mut sub_args = scc.clone();
                let mut frozen_in: BTreeSet<ArgumentId> = BTreeSet::new();
                let mut self_attack_args: Vec<ArgumentId> = Vec::new();

                for &arg in scc {
                    for &attacker in af.attackers_of(arg) {
                        if !resolved.contains(&attacker) || sub_args.contains(&attacker) {
                            continue;
                        }
                        if partial.contains(&attacker) {
                            sub_args.insert(attacker);
                            frozen_in.insert(attacker);
                        } else {
                            let is_defended = af
                                .attackers_of(attacker)
                                .iter()
                                .any(|&z| partial.contains(&z));
                            if !is_defended {
                                sub_args.insert(attacker);
                                self_attack_args.push(attacker);
                            }
                        }
                    }
                }

                let mut sub_af = af.sub_framework(&sub_args);
                for &a in &self_attack_args {
                    sub_af.add_defeat(a, a);
                }

                if let Some(ext) = self.inner.find_one(&sub_af, sem) {
                    let frozen_consistent = frozen_in.iter().all(|a| ext.contains(a));

                    if frozen_consistent {
                        let mut combined = partial.clone();
                        for &a in &ext {
                            if scc.contains(&a) {
                                combined.insert(a);
                            }
                        }
                        found_one = Some(combined);
                    }
                }
            }

            match found_one {
                Some(ext) => partial_extensions = vec![ext],
                None => return None,
            }
            resolved.extend(scc.iter());
        }

        partial_extensions.into_iter().next()
    }

    /// Compute the ideal extension by leveraging SCC-recursive preferred.
    ///
    /// Ideal = maximal admissible subset of the intersection of all preferred
    /// extensions. By computing preferred via `scc_recursive`, this benefits
    /// from SCC decomposition rather than falling through to the inner solver
    /// which would compute preferred on the full (undivided) framework.
    fn compute_ideal(&self, af: &AbstractFramework) -> Vec<Extension> {
        let preferred = self.scc_recursive(af, Semantics::Preferred);
        if preferred.is_empty() {
            return vec![BTreeSet::new()];
        }

        let mut intersection = preferred[0].clone();
        for ext in &preferred[1..] {
            intersection = intersection.intersection(ext).copied().collect();
        }

        let admissible = super::naive_solver::admissible_extensions(af);
        let maximal = admissible
            .into_iter()
            .filter(|s| s.is_subset(&intersection))
            .max_by_key(std::collections::BTreeSet::len)
            .unwrap_or_default();

        vec![maximal]
    }

    /// SCC-recursive extension computation.
    ///
    /// Process SCCs in topological order (attackers before attacked).
    /// For each SCC, build a sub-framework containing:
    /// - The SCC's own arguments.
    /// - "In" external attackers (frozen as accepted; must remain "in").
    /// - "Out" external attackers that are **not counter-attacked** by any
    ///   "in" argument. These represent undefendable attacks: no argument
    ///   in the current or future SCCs can counter-attack a previous-SCC
    ///   argument (that would create a cycle, merging the SCCs). A self-
    ///   attack is added to each so the inner solver keeps them "out"
    ///   while still seeing their outgoing attacks.
    ///
    /// Solve the sub-problem, filter for consistency with frozen "in"
    /// assignments, and compose partial extensions.
    fn scc_recursive(&self, af: &AbstractFramework, sem: Semantics) -> Vec<Extension> {
        let sccs = af.sccs();

        if sccs.len() <= 1 {
            return self.inner.extensions(af, sem);
        }

        let sccs: Vec<BTreeSet<ArgumentId>> = sccs.into_iter().rev().collect();

        let mut resolved: BTreeSet<ArgumentId> = BTreeSet::new();
        let mut partial_extensions: Vec<Extension> = vec![BTreeSet::new()];

        for scc in &sccs {
            let mut new_partial_extensions = Vec::new();

            for partial in &partial_extensions {
                let mut sub_args = scc.clone();
                let mut frozen_in: BTreeSet<ArgumentId> = BTreeSet::new();
                let mut self_attack_args: Vec<ArgumentId> = Vec::new();

                for &arg in scc {
                    for &attacker in af.attackers_of(arg) {
                        if !resolved.contains(&attacker) || sub_args.contains(&attacker) {
                            continue;
                        }
                        if partial.contains(&attacker) {
                            sub_args.insert(attacker);
                            frozen_in.insert(attacker);
                        } else {
                            let is_defended = af
                                .attackers_of(attacker)
                                .iter()
                                .any(|&z| partial.contains(&z));
                            if !is_defended {
                                sub_args.insert(attacker);
                                self_attack_args.push(attacker);
                            }
                        }
                    }
                }

                let mut sub_af = af.sub_framework(&sub_args);
                for &a in &self_attack_args {
                    sub_af.add_defeat(a, a);
                }

                let sub_extensions = self.inner.extensions(&sub_af, sem);

                for ext in sub_extensions {
                    let frozen_consistent = frozen_in.iter().all(|a| ext.contains(a));

                    if frozen_consistent {
                        let mut combined = partial.clone();
                        for &a in &ext {
                            if scc.contains(&a) {
                                combined.insert(a);
                            }
                        }
                        new_partial_extensions.push(combined);
                    }
                }
            }

            if new_partial_extensions.is_empty() {
                return vec![];
            }

            partial_extensions = new_partial_extensions;
            resolved.extend(scc.iter());
        }

        partial_extensions.sort();
        partial_extensions.dedup();
        partial_extensions
    }
}
