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

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

fn ext(ids: &[usize]) -> Extension {
    ids.iter().map(|&i| ArgumentId(i)).collect()
}

// ---------------------------------------------------------------------------
// SCC decomposition on AbstractFramework
// ---------------------------------------------------------------------------

#[test]
fn scc_single_argument() {
    let af = build_af(1, &[]);
    let sccs = af.sccs();
    assert_eq!(sccs.len(), 1);
    assert_eq!(sccs[0], ext(&[0]));
}

#[test]
fn scc_linear_chain() {
    // 0 -> 1 -> 2: three singleton SCCs
    let af = build_af(3, &[(0, 1), (1, 2)]);
    let sccs = af.sccs();
    assert_eq!(sccs.len(), 3);
    // Each SCC is a singleton
    for scc in &sccs {
        assert_eq!(scc.len(), 1);
    }
}

#[test]
fn scc_mutual_attack() {
    // 0 <-> 1: one SCC with both arguments
    let af = build_af(2, &[(0, 1), (1, 0)]);
    let sccs = af.sccs();
    assert_eq!(sccs.len(), 1);
    assert_eq!(sccs[0], ext(&[0, 1]));
}

#[test]
fn scc_two_components() {
    // 0 <-> 1, 2 (isolated): two SCCs
    let af = build_af(3, &[(0, 1), (1, 0)]);
    let sccs = af.sccs();
    assert_eq!(sccs.len(), 2);
    let all: BTreeSet<_> = sccs.iter().flat_map(|s| s.iter()).copied().collect();
    assert_eq!(all, ext(&[0, 1, 2]));
}

#[test]
fn scc_diamond() {
    // 0 -> 1, 0 -> 2, 1 -> 3, 2 -> 3: four singleton SCCs
    let af = build_af(4, &[(0, 1), (0, 2), (1, 3), (2, 3)]);
    let sccs = af.sccs();
    assert_eq!(sccs.len(), 4);
}

#[test]
fn scc_cycle_of_three() {
    // 0 -> 1 -> 2 -> 0: one SCC with all three
    let af = build_af(3, &[(0, 1), (1, 2), (2, 0)]);
    let sccs = af.sccs();
    assert_eq!(sccs.len(), 1);
    assert_eq!(sccs[0], ext(&[0, 1, 2]));
}

#[test]
fn sub_framework_extracts_correctly() {
    let af = build_af(4, &[(0, 1), (1, 2), (2, 3), (3, 0)]);
    let subset: BTreeSet<_> = [ArgumentId(0), ArgumentId(1)].into_iter().collect();
    let sub = af.sub_framework(&subset);
    assert_eq!(sub.arguments.len(), 2);
    assert_eq!(sub.defeats.len(), 1); // only (0,1) is within subset
    assert!(sub.defeats.contains(&(ArgumentId(0), ArgumentId(1))));
}

#[cfg(feature = "sat")]
mod sat_backend_tests {
    use super::*;

    fn naive_solver() -> NaiveEnumerationSolver {
        NaiveEnumerationSolver
    }

    fn scc_solver() -> SccDecomposingSolver {
        SccDecomposingSolver {
            inner: Box::new(NaiveEnumerationSolver),
        }
    }

    fn sat_solver() -> SatSolver {
        SatSolver::default()
    }

    fn scc_sat_solver() -> SccDecomposingSolver {
        SccDecomposingSolver {
            inner: Box::new(SatSolver::<rustsat_batsat::BasicSolver>::default()),
        }
    }

    // SCC-decomposing solver vs naive solver

    #[test]
    fn scc_solver_grounded_matches_naive() {
        let af = build_af(3, &[(0, 1), (1, 2)]);
        let naive = naive_solver().extensions(&af, Semantics::Grounded);
        let scc = scc_solver().extensions(&af, Semantics::Grounded);
        assert_eq!(naive, scc);
    }

    #[test]
    fn scc_solver_stable_matches_naive() {
        let af = build_af(3, &[(0, 1), (1, 2)]);
        let naive = sorted_exts(naive_solver().extensions(&af, Semantics::Stable));
        let scc = sorted_exts(scc_solver().extensions(&af, Semantics::Stable));
        assert_eq!(naive, scc);
    }

    #[test]
    fn scc_solver_preferred_mutual_attack() {
        let af = build_af(2, &[(0, 1), (1, 0)]);
        let naive = sorted_exts(naive_solver().extensions(&af, Semantics::Preferred));
        let scc = sorted_exts(scc_solver().extensions(&af, Semantics::Preferred));
        assert_eq!(naive, scc);
    }

    #[test]
    fn scc_solver_complete_chain() {
        let af = build_af(3, &[(0, 1), (1, 2)]);
        let naive = sorted_exts(naive_solver().extensions(&af, Semantics::Complete));
        let scc = sorted_exts(scc_solver().extensions(&af, Semantics::Complete));
        assert_eq!(naive, scc);
    }

    // SAT solver vs naive solver

    #[test]
    fn sat_grounded_matches_naive() {
        let af = build_af(3, &[(0, 1), (1, 2)]);
        let naive = naive_solver().extensions(&af, Semantics::Grounded);
        let sat = sat_solver().extensions(&af, Semantics::Grounded);
        assert_eq!(naive, sat);
    }

    #[test]
    fn sat_stable_chain() {
        let af = build_af(3, &[(0, 1), (1, 2)]);
        let sat = sat_solver().extensions(&af, Semantics::Stable);
        assert_eq!(sat.len(), 1);
        assert_eq!(sat[0], ext(&[0, 2]));
    }

    #[test]
    fn sat_stable_mutual_attack() {
        let af = build_af(2, &[(0, 1), (1, 0)]);
        let naive = sorted_exts(naive_solver().extensions(&af, Semantics::Stable));
        let sat = sorted_exts(sat_solver().extensions(&af, Semantics::Stable));
        assert_eq!(naive, sat);
    }

    #[test]
    fn sat_stable_self_attack() {
        let af = build_af(1, &[(0, 0)]);
        let sat = sat_solver().extensions(&af, Semantics::Stable);
        assert!(sat.is_empty());
    }

    #[test]
    fn sat_complete_mutual_attack() {
        let af = build_af(2, &[(0, 1), (1, 0)]);
        let naive = sorted_exts(naive_solver().extensions(&af, Semantics::Complete));
        let sat = sorted_exts(sat_solver().extensions(&af, Semantics::Complete));
        assert_eq!(naive, sat);
    }

    #[test]
    fn sat_complete_chain() {
        let af = build_af(3, &[(0, 1), (1, 2)]);
        let naive = sorted_exts(naive_solver().extensions(&af, Semantics::Complete));
        let sat = sorted_exts(sat_solver().extensions(&af, Semantics::Complete));
        assert_eq!(naive, sat);
    }

    #[test]
    fn sat_preferred_mutual_attack() {
        let af = build_af(2, &[(0, 1), (1, 0)]);
        let naive = sorted_exts(naive_solver().extensions(&af, Semantics::Preferred));
        let sat = sorted_exts(sat_solver().extensions(&af, Semantics::Preferred));
        assert_eq!(naive, sat);
    }

    #[test]
    fn sat_preferred_chain() {
        let af = build_af(3, &[(0, 1), (1, 2)]);
        let naive = sorted_exts(naive_solver().extensions(&af, Semantics::Preferred));
        let sat = sorted_exts(sat_solver().extensions(&af, Semantics::Preferred));
        assert_eq!(naive, sat);
    }

    #[test]
    fn sat_empty_framework() {
        let af = build_af(0, &[]);
        let sat = sat_solver().extensions(&af, Semantics::Stable);
        assert_eq!(sat.len(), 1);
        assert!(sat[0].is_empty());
    }

    // SCC + SAT composed solver

    #[test]
    fn scc_sat_stable_chain() {
        let af = build_af(3, &[(0, 1), (1, 2)]);
        let naive = sorted_exts(naive_solver().extensions(&af, Semantics::Stable));
        let scc_sat = sorted_exts(scc_sat_solver().extensions(&af, Semantics::Stable));
        assert_eq!(naive, scc_sat);
    }

    #[test]
    fn scc_sat_preferred_mutual_attack() {
        let af = build_af(2, &[(0, 1), (1, 0)]);
        let naive = sorted_exts(naive_solver().extensions(&af, Semantics::Preferred));
        let scc_sat = sorted_exts(scc_sat_solver().extensions(&af, Semantics::Preferred));
        assert_eq!(naive, scc_sat);
    }

    // Regression: out/undecided external attackers (A<->B, C<->D, A->C)

    #[test]
    fn scc_solver_out_attacker_complete() {
        let af = build_af(4, &[(0, 1), (1, 0), (2, 3), (3, 2), (0, 2)]);
        let naive = sorted_exts(naive_solver().extensions(&af, Semantics::Complete));
        let scc = sorted_exts(scc_solver().extensions(&af, Semantics::Complete));
        assert_eq!(naive, scc);
    }

    #[test]
    fn scc_solver_out_attacker_stable() {
        let af = build_af(4, &[(0, 1), (1, 0), (2, 3), (3, 2), (0, 2)]);
        let naive = sorted_exts(naive_solver().extensions(&af, Semantics::Stable));
        let scc = sorted_exts(scc_solver().extensions(&af, Semantics::Stable));
        assert_eq!(naive, scc);
    }

    #[test]
    fn scc_solver_out_attacker_preferred() {
        let af = build_af(4, &[(0, 1), (1, 0), (2, 3), (3, 2), (0, 2)]);
        let naive = sorted_exts(naive_solver().extensions(&af, Semantics::Preferred));
        let scc = sorted_exts(scc_solver().extensions(&af, Semantics::Preferred));
        assert_eq!(naive, scc);
    }

    #[test]
    fn scc_solver_out_attacker_grounded() {
        let af = build_af(4, &[(0, 1), (1, 0), (2, 3), (3, 2), (0, 2)]);
        let naive = sorted_exts(naive_solver().extensions(&af, Semantics::Grounded));
        let scc = sorted_exts(scc_solver().extensions(&af, Semantics::Grounded));
        assert_eq!(naive, scc);
    }

    #[test]
    fn scc_solver_undecided_attacker_grounded() {
        let af = build_af(3, &[(0, 1), (1, 0), (0, 2)]);
        let naive = sorted_exts(naive_solver().extensions(&af, Semantics::Grounded));
        let scc = sorted_exts(scc_solver().extensions(&af, Semantics::Grounded));
        assert_eq!(naive, scc);
    }

    #[test]
    fn scc_sat_out_attacker_complete() {
        let af = build_af(4, &[(0, 1), (1, 0), (2, 3), (3, 2), (0, 2)]);
        let naive = sorted_exts(naive_solver().extensions(&af, Semantics::Complete));
        let scc_sat = sorted_exts(scc_sat_solver().extensions(&af, Semantics::Complete));
        assert_eq!(naive, scc_sat);
    }

    #[test]
    fn scc_sat_out_attacker_stable() {
        let af = build_af(4, &[(0, 1), (1, 0), (2, 3), (3, 2), (0, 2)]);
        let naive = sorted_exts(naive_solver().extensions(&af, Semantics::Stable));
        let scc_sat = sorted_exts(scc_sat_solver().extensions(&af, Semantics::Stable));
        assert_eq!(naive, scc_sat);
    }

    // SCC solver — admissible semantics

    #[test]
    fn scc_solver_admissible_chain() {
        let af = build_af(3, &[(0, 1), (1, 2)]);
        let naive = sorted_exts(naive_solver().extensions(&af, Semantics::Admissible));
        let scc = sorted_exts(scc_solver().extensions(&af, Semantics::Admissible));
        assert_eq!(naive, scc);
    }

    #[test]
    fn scc_solver_admissible_mutual_attack() {
        let af = build_af(2, &[(0, 1), (1, 0)]);
        let naive = sorted_exts(naive_solver().extensions(&af, Semantics::Admissible));
        let scc = sorted_exts(scc_solver().extensions(&af, Semantics::Admissible));
        assert_eq!(naive, scc);
    }

    #[test]
    fn scc_solver_admissible_out_attacker() {
        let af = build_af(4, &[(0, 1), (1, 0), (2, 3), (3, 2), (0, 2)]);
        let naive = sorted_exts(naive_solver().extensions(&af, Semantics::Admissible));
        let scc = sorted_exts(scc_solver().extensions(&af, Semantics::Admissible));
        assert_eq!(naive, scc);
    }

    #[test]
    fn scc_sat_admissible_chain() {
        let af = build_af(3, &[(0, 1), (1, 2)]);
        let naive = sorted_exts(naive_solver().extensions(&af, Semantics::Admissible));
        let scc_sat = sorted_exts(scc_sat_solver().extensions(&af, Semantics::Admissible));
        assert_eq!(naive, scc_sat);
    }

    #[test]
    fn scc_sat_admissible_out_attacker() {
        let af = build_af(4, &[(0, 1), (1, 0), (2, 3), (3, 2), (0, 2)]);
        let naive = sorted_exts(naive_solver().extensions(&af, Semantics::Admissible));
        let scc_sat = sorted_exts(scc_sat_solver().extensions(&af, Semantics::Admissible));
        assert_eq!(naive, scc_sat);
    }

    #[test]
    fn scc_solver_admissible_empty_af() {
        let af = build_af(0, &[]);
        let exts = scc_solver().extensions(&af, Semantics::Admissible);
        assert_eq!(exts.len(), 1);
        assert!(exts[0].is_empty());
    }

    #[test]
    fn scc_solver_admissible_no_attacks() {
        let af = build_af(3, &[]);
        let naive = sorted_exts(naive_solver().extensions(&af, Semantics::Admissible));
        let scc = sorted_exts(scc_solver().extensions(&af, Semantics::Admissible));
        assert_eq!(naive, scc);
    }

    // SAT solver — admissible semantics

    #[test]
    fn sat_admissible_chain() {
        let af = build_af(3, &[(0, 1), (1, 2)]);
        let naive = sorted_exts(naive_solver().extensions(&af, Semantics::Admissible));
        let sat = sorted_exts(sat_solver().extensions(&af, Semantics::Admissible));
        assert_eq!(naive, sat);
    }

    #[test]
    fn sat_admissible_mutual_attack() {
        let af = build_af(2, &[(0, 1), (1, 0)]);
        let naive = sorted_exts(naive_solver().extensions(&af, Semantics::Admissible));
        let sat = sorted_exts(sat_solver().extensions(&af, Semantics::Admissible));
        assert_eq!(naive, sat);
    }

    #[test]
    fn sat_admissible_empty_af() {
        let af = build_af(0, &[]);
        let exts = sat_solver().extensions(&af, Semantics::Admissible);
        assert_eq!(exts.len(), 1);
        assert!(exts[0].is_empty());
    }

    // SCC solver — ideal semantics

    #[test]
    fn scc_solver_ideal_chain() {
        let af = build_af(3, &[(0, 1), (1, 2)]);
        let naive = sorted_exts(naive_solver().extensions(&af, Semantics::Ideal));
        let scc = sorted_exts(scc_solver().extensions(&af, Semantics::Ideal));
        assert_eq!(naive, scc);
    }

    #[test]
    fn scc_solver_ideal_mutual_attack_with_unattacked() {
        let af = build_af(3, &[(0, 1), (1, 0)]);
        let naive = sorted_exts(naive_solver().extensions(&af, Semantics::Ideal));
        let scc = sorted_exts(scc_solver().extensions(&af, Semantics::Ideal));
        assert_eq!(naive, scc);
        assert_eq!(scc[0], ext(&[2]));
    }

    #[test]
    fn scc_sat_ideal_multi_scc() {
        let af = build_af(4, &[(0, 1), (1, 0), (2, 3), (3, 2), (0, 2)]);
        let naive = sorted_exts(naive_solver().extensions(&af, Semantics::Ideal));
        let scc_sat = sorted_exts(scc_sat_solver().extensions(&af, Semantics::Ideal));
        assert_eq!(naive, scc_sat);
    }
}

// ---------------------------------------------------------------------------
// Indexed attack computer vs pairwise
// ---------------------------------------------------------------------------

fn build_system_for_attack_test() -> (ArgumentStore, ContrarinessFunction) {
    use pickaxe_rs::framework::argument::Argument;
    use pickaxe_rs::system::knowledge::{Premise, PremiseKind};

    let mut store = ArgumentStore::new();
    let contrariness = ContrarinessFunction::new().with_classical_negation();

    store.add(Argument::Premise {
        id: ArgumentId(0),
        premise: Premise {
            formula: Formula::prop("a"),
            kind: PremiseKind::Ordinary,
        },
    });
    store.add(Argument::Premise {
        id: ArgumentId(1),
        premise: Premise {
            formula: Formula::neg_prop("a"),
            kind: PremiseKind::Ordinary,
        },
    });
    store.add(Argument::Premise {
        id: ArgumentId(2),
        premise: Premise {
            formula: Formula::prop("b"),
            kind: PremiseKind::Ordinary,
        },
    });

    (store, contrariness)
}

#[test]
fn indexed_attack_matches_pairwise() {
    let (store, contrariness) = build_system_for_attack_test();

    let pairwise = PairwiseAttackComputer;
    let indexed = IndexedAttackComputer;

    let pairwise_attacks = pairwise.compute(&store, &contrariness);
    let indexed_attacks = indexed.compute(&store, &contrariness);

    // Same number of attacks
    assert_eq!(
        pairwise_attacks.len(),
        indexed_attacks.len(),
        "pairwise found {} attacks, indexed found {}",
        pairwise_attacks.len(),
        indexed_attacks.len()
    );

    // Same attack pairs (ignoring order)
    let mut pairwise_pairs: Vec<_> = pairwise_attacks
        .iter()
        .map(|a| (a.attacker, a.target))
        .collect();
    let mut indexed_pairs: Vec<_> = indexed_attacks
        .iter()
        .map(|a| (a.attacker, a.target))
        .collect();
    pairwise_pairs.sort();
    indexed_pairs.sort();
    assert_eq!(pairwise_pairs, indexed_pairs);
}

// ---------------------------------------------------------------------------
// Semi-naive grounder vs naive grounder
// ---------------------------------------------------------------------------

fn build_simple_system() -> AspicSystem {
    let (system, _warnings) = AspicSystemBuilder::new()
        .ordinary_premise(Formula::prop("bird"))
        .ordinary_premise(Formula::prop("penguin"))
        .named_defeasible_rule(
            "r1",
            Formula::prop("r1_name"),
            vec![Formula::prop("bird")],
            Formula::prop("flies"),
        )
        .strict_rule("s1", vec![Formula::prop("penguin")], Formula::prop("bird"))
        .build();
    system
}

#[test]
fn semi_naive_produces_valid_grounded_system() {
    let system = build_simple_system();
    let grounder = SemiNaiveGrounder;
    let result = grounder.ground(&system);
    assert!(result.is_ok());

    let grounded = result.unwrap();
    assert!(!grounded.knowledge_base.premises.is_empty());
}

#[test]
fn semi_naive_matches_naive_on_ground_system() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .ordinary_premise(Formula::prop("a"))
        .ordinary_premise(Formula::prop("b"))
        .defeasible_rule("r1", vec![Formula::prop("a")], Formula::prop("c"))
        .strict_rule("s1", vec![Formula::prop("b")], Formula::prop("d"))
        .build();

    let naive_result = NaiveGrounder.ground(&system).unwrap();
    let semi_result = SemiNaiveGrounder.ground(&system).unwrap();

    assert_eq!(
        naive_result.knowledge_base.premises.len(),
        semi_result.knowledge_base.premises.len()
    );
}

// ---------------------------------------------------------------------------
// Integration: optimised pipeline produces same results as classical
// ---------------------------------------------------------------------------

#[test]
#[cfg(feature = "sat")]
fn optimised_pipeline_matches_classical() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .ordinary_premise(Formula::prop("a"))
        .ordinary_premise(Formula::prop("b"))
        .ordinary_premise(Formula::neg_prop("b"))
        .with_classical_negation()
        .build();

    let ordering: Box<dyn ArgumentOrdering> = Box::new(LastLinkOrdering {
        rule_ordering: Box::new(NoPreference),
        premise_ordering: Box::new(NoPreference),
        lifting: LiftingStrategy::Elitist,
    });

    let classical = AspicPipeline::classical(system.clone(), ordering);
    let classical_result = classical.evaluate(Semantics::Stable).unwrap();

    let ordering2: Box<dyn ArgumentOrdering> = Box::new(LastLinkOrdering {
        rule_ordering: Box::new(NoPreference),
        premise_ordering: Box::new(NoPreference),
        lifting: LiftingStrategy::Elitist,
    });
    let optimised = AspicPipeline::optimised(system, ordering2);
    let optimised_result = optimised.evaluate(Semantics::Stable).unwrap();

    let mut classical_exts = classical_result.extensions;
    let mut optimised_exts = optimised_result.extensions;
    classical_exts.sort();
    optimised_exts.sort();

    assert_eq!(classical_exts, optimised_exts);
}
