//! Property-based tests for ordering reasonableness.
//!
//! Verifies that the built-in last-link and weakest-link orderings satisfy the
//! three conditions for being reasonable orderings (Modgil & Prakken 2013,
//! Theorem 4.13; Modgil & Prakken 2014, §4.2):
//!
//! (a) Strict+firm arguments are strictly preferred over non-strict-or-non-firm.
//! (b) The ordering is determined solely by defeasible rules and ordinary premises.
//! (c) The strict preference relation is acyclic.

use pickaxe_rs::language::formula::{Atom, Formula, Literal};
use pickaxe_rs::prelude::*;

use proptest::prelude::*;

// --- Helpers ---

fn make_atom(i: usize) -> Formula {
    Formula::Lit(Literal::Pos(Atom {
        predicate: format!("a{i}"),
        terms: vec![],
    }))
}

/// Generate a random AT for ordering tests (does not require well-definedness).
fn arb_at_for_ordering() -> impl Strategy<Value = (AspicSystem, Vec<RuleId>)> {
    let n_atoms = 3..=5usize;
    let n_ordinary = 1..=3usize;
    let n_defeasible = 2..=4usize;

    (n_atoms, n_ordinary, n_defeasible)
        .prop_flat_map(|(na, no, nd)| {
            let atoms: Vec<Formula> = (0..na).map(make_atom).collect();
            let all: Vec<Formula> = atoms
                .iter()
                .flat_map(|a| vec![a.clone(), a.classical_negation()])
                .collect();
            let n_all = all.len();

            let axiom_idx =
                proptest::sample::subsequence((0..na).collect::<Vec<_>>(), 1..=1usize.min(na));

            let ord_idx =
                proptest::sample::subsequence((0..na).collect::<Vec<_>>(), 1..=no.min(na));

            let def_rules = proptest::collection::vec(
                (
                    proptest::sample::subsequence((0..n_all).collect::<Vec<_>>(), 1..=2),
                    (0..n_all),
                ),
                2..=nd,
            );

            (Just(atoms), Just(all), axiom_idx, ord_idx, def_rules)
        })
        .prop_filter_map(
            "valid AT for ordering",
            |(atoms, all, ax_idx, ord_idx, def_raw)| {
                let mut builder = AspicSystemBuilder::new().with_classical_negation();

                for &i in &ax_idx {
                    builder = builder.axiom(atoms[i].clone());
                }
                for &i in &ord_idx {
                    builder = builder.ordinary_premise(atoms[i].clone());
                }

                let mut rule_ids = Vec::new();
                let mut def_id = 0u32;
                for (ante_idx, cons_idx) in &def_raw {
                    let antes: Vec<Formula> = ante_idx.iter().map(|&i| all[i].clone()).collect();
                    if let Some(cons) = all.get(*cons_idx) {
                        if antes.contains(cons) {
                            continue;
                        }
                        let id = format!("d{def_id}");
                        let name = Formula::Lit(Literal::Pos(Atom {
                            predicate: id.clone(),
                            terms: vec![],
                        }));
                        builder = builder.named_defeasible_rule(&id, name, antes, cons.clone());
                        rule_ids.push(RuleId(id));
                        def_id += 1;
                    }
                }

                if rule_ids.len() < 2 {
                    return None;
                }

                let (system, _) = builder.build();
                Some((system, rule_ids))
            },
        )
}

proptest! {
    #![proptest_config(ProptestConfig::with_cases(64))]

    /// Condition (a): Strict+firm arguments are strictly preferred over
    /// non-strict-or-non-firm arguments.
    ///
    /// The WeakestLinkOrdering explicitly handles this case (Definition 3.23
    /// in Modgil & Prakken 2014). The LastLinkOrdering achieves reasonableness
    /// through the combined system (ordering + defeat + well-formedness),
    /// not the ordering comparison alone — so we only test WeakestLink here.
    ///
    /// Reference: Modgil & Prakken (2013), Theorem 4.13 condition (i).
    #[test]
    fn strict_firm_preferred(
        (system, rule_ids) in arb_at_for_ordering()
    ) {
        let pipeline = AspicPipeline::classical(
            system.clone(),
            Box::new(WeakestLinkOrdering {
                rule_ordering: Box::new(NoPreference),
                premise_ordering: Box::new(NoPreference),
                lifting: LiftingStrategy::Elitist,
            }),
        );
        let result = pipeline.evaluate(Semantics::Grounded).unwrap();
        let store = &result.store;

        let strict_firm: Vec<ArgumentId> = store
            .all_arguments()
            .filter(|(_, a)| a.is_strict(store) && a.is_firm(store))
            .map(|(id, _)| id)
            .collect();

        let fallible: Vec<ArgumentId> = store
            .all_arguments()
            .filter(|(_, a)| !a.is_strict(store) || !a.is_firm(store))
            .map(|(id, _)| id)
            .collect();

        let wl = WeakestLinkOrdering {
            rule_ordering: Box::new(TieredOrdering::new(
                rule_ids.iter().map(|r| vec![r.clone()]).collect(),
            )),
            premise_ordering: Box::new(NoPreference),
            lifting: LiftingStrategy::Elitist,
        };

        for &sf in &strict_firm {
            for &fb in &fallible {
                let pref = wl.compare(sf, fb, store);
                prop_assert!(
                    matches!(pref, Preference::StrictlyPreferred),
                    "weakest-link: strict+firm {sf:?} should be strictly preferred over {fb:?}, got {pref:?}"
                );
            }
        }
    }

    /// Condition (c): The strict preference relation is acyclic.
    ///
    /// For the set of all constructed arguments, the strict-preference graph
    /// must contain no cycles.
    ///
    /// Reference: Modgil & Prakken (2013), Theorem 4.13 condition (iii).
    #[test]
    fn ordering_acyclicity(
        (system, rule_ids) in arb_at_for_ordering()
    ) {
        let pipeline = AspicPipeline::classical(
            system.clone(),
            Box::new(LastLinkOrdering {
                rule_ordering: Box::new(NoPreference),
                premise_ordering: Box::new(NoPreference),
                lifting: LiftingStrategy::Elitist,
            }),
        );
        let result = pipeline.evaluate(Semantics::Grounded).unwrap();
        let store = &result.store;

        let all_ids: Vec<ArgumentId> = store.all_arguments().map(|(id, _)| id).collect();

        // Check last-link acyclicity via DFS cycle detection
        let ll = LastLinkOrdering {
            rule_ordering: Box::new(TieredOrdering::new(
                rule_ids.iter().map(|r| vec![r.clone()]).collect(),
            )),
            premise_ordering: Box::new(NoPreference),
            lifting: LiftingStrategy::Elitist,
        };

        prop_assert!(
            !has_cycle(&all_ids, |a, b| ll.compare(a, b, store)),
            "last-link ordering has a cycle"
        );

        // Check weakest-link acyclicity
        let wl = WeakestLinkOrdering {
            rule_ordering: Box::new(TieredOrdering::new(
                rule_ids.iter().map(|r| vec![r.clone()]).collect(),
            )),
            premise_ordering: Box::new(NoPreference),
            lifting: LiftingStrategy::Elitist,
        };

        prop_assert!(
            !has_cycle(&all_ids, |a, b| wl.compare(a, b, store)),
            "weakest-link ordering has a cycle"
        );
    }
}

/// DFS-based cycle detection in the strict-preference graph.
fn has_cycle(ids: &[ArgumentId], compare: impl Fn(ArgumentId, ArgumentId) -> Preference) -> bool {
    let n = ids.len();
    if n == 0 {
        return false;
    }

    // Build adjacency: edge from i → j if ids[i] is strictly preferred over ids[j]
    let mut adj: Vec<Vec<usize>> = vec![Vec::new(); n];
    for i in 0..n {
        for j in 0..n {
            if i != j && matches!(compare(ids[i], ids[j]), Preference::StrictlyPreferred) {
                adj[i].push(j);
            }
        }
    }

    // Standard DFS cycle detection: 0 = unvisited, 1 = in-stack, 2 = done
    let mut state = vec![0u8; n];

    fn dfs(node: usize, adj: &[Vec<usize>], state: &mut [u8]) -> bool {
        state[node] = 1;
        for &next in &adj[node] {
            if state[next] == 1 {
                return true;
            }
            if state[next] == 0 && dfs(next, adj, state) {
                return true;
            }
        }
        state[node] = 2;
        false
    }

    for i in 0..n {
        if state[i] == 0 && dfs(i, &adj, &mut state) {
            return true;
        }
    }
    false
}
