//! Validation tests for the SAF → AF reduction and Dung AF property checks.
//!
//! **Reference**: Modgil & Prakken (2014) — Definitions 3.1, 3.12, 3.14, 3.16;
//! Examples 3.15, 3.18.
//!
//! These tests validate the existing implementation against the formal theory:
//! - Definition 3.12: defeat filtering (undercut always, rebut/undermine iff ⊀)
//! - Definition 3.16: AF = (A, D) constructed from SAF = ⟨A, C, ≤⟩
//! - Definition 3.1: conflict-freeness, defence, admissibility, completeness, stability

use pickaxe_rs::prelude::*;

mod common;
use common::*;

// ---
// Local helpers
// ---

fn build_store(n: usize) -> ArgumentStore {
    let mut store = ArgumentStore::new();
    for i in 0..n {
        store.add(Argument::Premise {
            id: ArgumentId(i),
            premise: Premise {
                formula: Formula::prop(format!("p{i}")),
                kind: PremiseKind::Ordinary,
            },
        });
    }
    store
}

/// Ordering controlled by a lookup table: maps (a, b) pairs to a Preference.
/// Returns Incomparable for any pair not in the table.
#[derive(Debug)]
struct TableOrdering {
    entries: Vec<(usize, usize, Preference)>,
}

impl ArgumentOrdering for TableOrdering {
    fn compare(&self, a: ArgumentId, b: ArgumentId, _store: &ArgumentStore) -> Preference {
        for (ea, eb, pref) in &self.entries {
            if a.0 == *ea && b.0 == *eb {
                return pref.clone();
            }
        }
        Preference::Incomparable
    }
}

// ---
// Defeat computation (Definition 3.12)
// ---

/// Undercuts always succeed, even when the ordering says StrictlyDispreferred.
#[test]
fn defeat_undercut_always_succeeds() {
    let store = build_store(2);
    let attacks = vec![Attack {
        attacker: ArgumentId(0),
        target: ArgumentId(1),
        kind: AttackKind::Undercut {
            target_sub: ArgumentId(1),
            rule_id: RuleId("r1".into()),
        },
    }];
    let defeats = compute_defeats(&attacks, &store, &AlwaysDispreferredOrdering);
    assert_eq!(defeats.len(), 1);
    assert!(defeat_exists(&defeats, ArgumentId(0), ArgumentId(1)));
}

/// A rebut is blocked when the attacker is strictly dispreffered to the target sub-argument.
#[test]
fn defeat_rebut_blocked_when_strictly_dispreffered() {
    let store = build_store(2);
    let attacks = vec![Attack {
        attacker: ArgumentId(0),
        target: ArgumentId(1),
        kind: AttackKind::Rebut {
            target_sub: ArgumentId(1),
            contrary: false,
        },
    }];
    let defeats = compute_defeats(&attacks, &store, &AlwaysDispreferredOrdering);
    assert!(
        defeats.is_empty(),
        "rebut should be blocked when strictly dispreffered"
    );
}

/// An undermine is blocked when the attacker is strictly dispreffered to the target premise.
#[test]
fn defeat_undermine_blocked_when_strictly_dispreffered() {
    let store = build_store(2);
    let attacks = vec![Attack {
        attacker: ArgumentId(0),
        target: ArgumentId(1),
        kind: AttackKind::Undermine {
            target_premise: ArgumentId(1),
            contrary: false,
        },
    }];
    let defeats = compute_defeats(&attacks, &store, &AlwaysDispreferredOrdering);
    assert!(
        defeats.is_empty(),
        "undermine should be blocked when strictly dispreffered"
    );
}

/// A rebut succeeds when the ordering returns Equal, StrictlyPreferred, or Incomparable.
#[test]
fn defeat_rebut_succeeds_when_equal_or_preferred() {
    let store = build_store(4);

    let make_rebut = |attacker: usize, target: usize| Attack {
        attacker: ArgumentId(attacker),
        target: ArgumentId(target),
        kind: AttackKind::Rebut {
            target_sub: ArgumentId(target),
            contrary: false,
        },
    };

    let attacks = vec![make_rebut(0, 1), make_rebut(1, 2), make_rebut(2, 3)];

    let ordering = TableOrdering {
        entries: vec![
            (0, 1, Preference::Equal),
            (1, 2, Preference::StrictlyPreferred),
            (2, 3, Preference::Incomparable),
        ],
    };

    let defeats = compute_defeats(&attacks, &store, &ordering);
    assert_eq!(defeats.len(), 3, "all three rebuts should succeed");
    assert!(defeat_exists(&defeats, ArgumentId(0), ArgumentId(1)));
    assert!(defeat_exists(&defeats, ArgumentId(1), ArgumentId(2)));
    assert!(defeat_exists(&defeats, ArgumentId(2), ArgumentId(3)));
}

/// With an equal ordering, all attack types succeed as defeats.
#[test]
fn defeat_all_attacks_succeed_with_no_preference() {
    let store = build_store(4);

    let attacks = vec![
        Attack {
            attacker: ArgumentId(0),
            target: ArgumentId(1),
            kind: AttackKind::Undercut {
                target_sub: ArgumentId(1),
                rule_id: RuleId("r1".into()),
            },
        },
        Attack {
            attacker: ArgumentId(1),
            target: ArgumentId(2),
            kind: AttackKind::Rebut {
                target_sub: ArgumentId(2),
                contrary: false,
            },
        },
        Attack {
            attacker: ArgumentId(2),
            target: ArgumentId(3),
            kind: AttackKind::Undermine {
                target_premise: ArgumentId(3),
                contrary: false,
            },
        },
    ];

    let defeats = compute_defeats(&attacks, &store, &EqualOrdering);
    assert_eq!(
        defeats.len(),
        3,
        "all attacks should succeed with EqualOrdering"
    );
}

// ---
// AF construction with deduplication
// ---

/// The AF's argument set matches the store exactly.
#[test]
fn af_arguments_match_store() {
    let af = build_af(5, &[]);
    assert_eq!(af.arguments.len(), 5);
    for i in 0..5 {
        assert!(af.arguments.contains(&ArgumentId(i)));
    }
}

/// Duplicate defeat pairs are deduplicated in the AF.
#[test]
fn af_deduplicates_defeat_pairs() {
    let store = build_store(2);
    let defeats = vec![
        Defeat {
            attacker: ArgumentId(0),
            target: ArgumentId(1),
            kind: AttackKind::Rebut {
                target_sub: ArgumentId(1),
                contrary: false,
            },
        },
        Defeat {
            attacker: ArgumentId(0),
            target: ArgumentId(1),
            kind: AttackKind::Undermine {
                target_premise: ArgumentId(1),
                contrary: false,
            },
        },
        Defeat {
            attacker: ArgumentId(0),
            target: ArgumentId(1),
            kind: AttackKind::Undercut {
                target_sub: ArgumentId(1),
                rule_id: RuleId("r1".into()),
            },
        },
    ];

    let af = AbstractFramework::from_defeats(&store, &defeats);
    assert_eq!(
        af.defeats.len(),
        1,
        "three defeats with same (attacker, target) should deduplicate to 1"
    );
    assert_eq!(af.defeats[0], (ArgumentId(0), ArgumentId(1)));
}

/// attackers_of returns the correct set of attackers.
#[test]
fn af_attackers_of_returns_correct_set() {
    let af = build_af(3, &[(0, 1), (2, 1), (0, 2)]);

    let mut att1 = af.attackers_of(ArgumentId(1)).to_vec();
    att1.sort();
    assert_eq!(att1, vec![ArgumentId(0), ArgumentId(2)]);

    let att2 = af.attackers_of(ArgumentId(2));
    assert_eq!(att2, &[ArgumentId(0)]);

    let att0 = af.attackers_of(ArgumentId(0));
    assert!(att0.is_empty());
}

/// attacked_by returns the correct set of targets.
#[test]
fn af_attacked_by_returns_correct_set() {
    let af = build_af(3, &[(0, 1), (2, 1), (0, 2)]);

    let mut targets0 = af.attacked_by(ArgumentId(0)).to_vec();
    targets0.sort();
    assert_eq!(targets0, vec![ArgumentId(1), ArgumentId(2)]);

    let targets2 = af.attacked_by(ArgumentId(2));
    assert_eq!(targets2, &[ArgumentId(1)]);

    let targets1 = af.attacked_by(ArgumentId(1));
    assert!(targets1.is_empty());
}

/// An empty store produces an empty framework.
#[test]
fn af_empty_store_produces_empty_framework() {
    let af = build_af(0, &[]);
    assert!(af.arguments.is_empty());
    assert!(af.defeats.is_empty());
}

// ---
// AF property checks (Definition 3.1)
// ---

/// Conflict-freeness basic cases.
#[test]
fn conflict_free_basic() {
    let af = build_af(3, &[(0, 1)]);

    assert!(
        af.is_conflict_free(&make_set(&[0, 2])),
        "{{0,2}} has no internal defeats"
    );
    assert!(
        !af.is_conflict_free(&make_set(&[0, 1])),
        "{{0,1}} contains defeat (0→1)"
    );
    assert!(
        af.is_conflict_free(&make_set(&[])),
        "empty set is trivially conflict-free"
    );
}

/// A self-attacking argument is not conflict-free.
#[test]
fn conflict_free_self_attack() {
    let af = build_af(1, &[(0, 0)]);
    assert!(
        !af.is_conflict_free(&make_set(&[0])),
        "{{0}} with 0→0 is not conflict-free"
    );
}

/// Defence is vacuously true when the argument has no attackers.
#[test]
fn defends_vacuous_no_attackers() {
    let af = build_af(3, &[(0, 1)]);
    assert!(
        af.defends(&make_set(&[]), ArgumentId(0)),
        "0 has no attackers, so ∅ defends 0"
    );
    assert!(
        af.defends(&make_set(&[]), ArgumentId(2)),
        "2 has no attackers, so ∅ defends 2"
    );
}

/// Defence requires a counter-attack against every attacker.
#[test]
fn defends_requires_counter() {
    let af_no_counter = build_af(3, &[(1, 0)]);
    assert!(
        !af_no_counter.defends(&make_set(&[]), ArgumentId(0)),
        "∅ cannot defend 0 against attacker 1"
    );
    assert!(
        !af_no_counter.defends(&make_set(&[2]), ArgumentId(0)),
        "{{2}} does not defeat 1"
    );

    let af_with_counter = build_af(3, &[(1, 0), (2, 1)]);
    assert!(
        af_with_counter.defends(&make_set(&[2]), ArgumentId(0)),
        "{{2}} defeats 1 who attacks 0"
    );
}

/// The empty set is admissible in any AF.
#[test]
fn admissible_empty_set() {
    let af = build_af(3, &[(0, 1), (1, 2)]);
    assert!(af.is_admissible(&make_set(&[])), "∅ is always admissible");
}

/// Admissibility requires conflict-freeness and self-defence.
#[test]
fn admissible_defends_all_members() {
    let af = build_af(2, &[(1, 0), (0, 1)]);
    assert!(
        af.is_admissible(&make_set(&[0])),
        "{{0}} is conflict-free and defends itself (0 defeats its attacker 1)"
    );
    assert!(
        !af.is_admissible(&make_set(&[0, 1])),
        "{{0,1}} is not conflict-free"
    );
}

/// Completeness requires the set to contain all arguments it defends.
#[test]
fn complete_fixed_point() {
    let af = build_af(3, &[(1, 0), (0, 1)]);
    assert!(
        !af.is_complete(&make_set(&[0])),
        "{{0}} is admissible but doesn't contain 2 (which it defends), so not complete"
    );
    assert!(
        af.is_complete(&make_set(&[0, 2])),
        "{{0,2}} is admissible and contains everything it defends"
    );
}

/// Stability requires defeating all non-members.
#[test]
fn stable_attacks_all_outsiders() {
    let af = build_af(3, &[(0, 1), (0, 2)]);
    assert!(
        af.is_stable(&make_set(&[0])),
        "{{0}} is conflict-free and defeats both non-members 1 and 2"
    );
}

/// Stability fails if the set is not conflict-free.
#[test]
fn stable_not_conflict_free_fails() {
    let af = build_af(3, &[(0, 1), (1, 0), (0, 2), (1, 2)]);
    assert!(
        !af.is_stable(&make_set(&[0, 1])),
        "{{0,1}} defeats 2 but is not conflict-free (mutual defeat)"
    );
}

// ---
// Pipeline integration via ClassicalEvaluator
// ---

fn running_example_store_and_attacks() -> (ArgumentStore, Vec<Attack>) {
    let system = running_example();
    let grounder = NaiveGrounder;
    let grounded = grounder.ground(&system).expect("grounding should succeed");
    let constructor = ForwardChainingConstructor;
    let store = constructor.construct(&grounded);
    let contrariness = grounded.contrariness.clone();
    let attack_computer = PairwiseAttackComputer;
    let attacks = attack_computer.compute(&store, &contrariness);
    (store, attacks)
}

/// ClassicalEvaluator wires defeats → AF → solver correctly.
#[test]
fn classical_evaluator_produces_correct_af() {
    let (store, attacks) = running_example_store_and_attacks();
    let evaluator = ClassicalEvaluator {
        semantics_solver: Box::new(NaiveEnumerationSolver),
    };
    let pref = PreferenceConfig::ArgumentOrdering(Box::new(EqualOrdering));
    let result = evaluator
        .evaluate(&store, &attacks, Semantics::Grounded, &pref)
        .unwrap();
    assert_eq!(
        result.extensions.len(),
        1,
        "grounded semantics yields exactly one extension"
    );
    assert!(
        !result.extensions[0].is_empty(),
        "grounded extension should be non-empty for the running example"
    );
}

/// Different orderings produce different defeat sets.
#[test]
fn different_orderings_produce_different_afs() {
    let (store, attacks) = running_example_store_and_attacks();

    let defeats_equal = compute_defeats(&attacks, &store, &EqualOrdering);
    let defeats_dispreffered = compute_defeats(&attacks, &store, &AlwaysDispreferredOrdering);

    assert!(
        defeats_equal.len() > defeats_dispreffered.len(),
        "NoPreference should admit more defeats than AlwaysDispreferred \
         (which blocks all rebuts/undermines). Equal: {}, Dispreffered: {}",
        defeats_equal.len(),
        defeats_dispreffered.len()
    );
}

// ---
// Example 3.18 — defeat under different orderings
// ---

/// Ordering for Example 3.18 that compares arguments by ID using a lookup of
/// which arguments are "strictly preferred". Pairs not in the table get Equal.
#[derive(Debug)]
struct Example318Ordering {
    strictly_preferred: Vec<(ArgumentId, ArgumentId)>,
}

impl ArgumentOrdering for Example318Ordering {
    fn compare(&self, a: ArgumentId, b: ArgumentId, _store: &ArgumentStore) -> Preference {
        if a == b {
            return Preference::Equal;
        }
        for &(pref, disp) in &self.strictly_preferred {
            if a == pref && b == disp {
                return Preference::StrictlyPreferred;
            }
            if a == disp && b == pref {
                return Preference::StrictlyDispreferred;
            }
        }
        Preference::Equal
    }
}

/// Example 3.18 Case 1 — D₄ strictly preferred over B₂.
/// B₂→D₄ should NOT succeed as a defeat. D₄→B₂ and D₄→B₃ should succeed.
#[test]
fn example_3_18_case_1_d4_strictly_preferred() {
    let (store, attacks) = running_example_store_and_attacks();
    let args = find_running_example_args(&store);

    let ordering = Example318Ordering {
        strictly_preferred: vec![(args.d4, args.b2)],
    };

    let defeats = compute_defeats(&attacks, &store, &ordering);

    assert!(
        defeat_exists(&defeats, args.b3, args.a2),
        "B₃→A₂ should be a defeat (undercut, always succeeds)"
    );
    assert!(
        defeat_exists(&defeats, args.b3, args.a3),
        "B₃→A₃ should be a defeat (undercut, always succeeds)"
    );
    assert!(
        defeat_exists(&defeats, args.d4, args.b2),
        "D₄→B₂ should succeed (D₄ is not strictly dispreffered to the rebut comparison point)"
    );
    assert!(
        !defeat_exists(&defeats, args.b2, args.d4),
        "B₂→D₄ should NOT succeed (B₂ is strictly dispreffered to D₄)"
    );
}

/// Example 3.18 Case 2 — B₂ strictly preferred over D₄.
/// D₄→B₂ should NOT succeed. B₂→D₄ should succeed.
#[test]
fn example_3_18_case_2_b2_strictly_preferred() {
    let (store, attacks) = running_example_store_and_attacks();
    let args = find_running_example_args(&store);

    let ordering = Example318Ordering {
        strictly_preferred: vec![(args.b2, args.d4)],
    };

    let defeats = compute_defeats(&attacks, &store, &ordering);

    assert!(
        defeat_exists(&defeats, args.b2, args.d4),
        "B₂→D₄ should succeed (B₂ is strictly preferred)"
    );
    assert!(
        !defeat_exists(&defeats, args.d4, args.b2),
        "D₄→B₂ should NOT succeed (D₄ is strictly dispreffered to B₂)"
    );
}

/// Example 3.18 Case 3 — B₂ and D₄ are equally preferred (mutual defeat).
#[test]
fn example_3_18_case_3_mutual_defeat() {
    let (store, attacks) = running_example_store_and_attacks();
    let args = find_running_example_args(&store);

    let ordering = Example318Ordering {
        strictly_preferred: vec![],
    };

    let defeats = compute_defeats(&attacks, &store, &ordering);

    assert!(
        defeat_exists(&defeats, args.b2, args.d4),
        "B₂→D₄ should succeed (neither is strictly dispreffered)"
    );
    assert!(
        defeat_exists(&defeats, args.d4, args.b2),
        "D₄→B₂ should succeed (neither is strictly dispreffered)"
    );
}

// ---
// Edge cases
// ---

/// With no defeats, every non-empty subset is conflict-free.
#[test]
fn af_no_attacks_all_conflict_free() {
    let af = build_af(3, &[]);
    assert!(af.is_conflict_free(&make_set(&[0])));
    assert!(af.is_conflict_free(&make_set(&[1])));
    assert!(af.is_conflict_free(&make_set(&[2])));
    assert!(af.is_conflict_free(&make_set(&[0, 1])));
    assert!(af.is_conflict_free(&make_set(&[0, 2])));
    assert!(af.is_conflict_free(&make_set(&[1, 2])));
    assert!(af.is_conflict_free(&make_set(&[0, 1, 2])));
}

/// All undercut attacks become defeats, even with StrictlyDispreferred ordering.
#[test]
fn af_all_undercut_attacks_become_defeats() {
    let store = build_store(3);
    let attacks = vec![
        Attack {
            attacker: ArgumentId(0),
            target: ArgumentId(1),
            kind: AttackKind::Undercut {
                target_sub: ArgumentId(1),
                rule_id: RuleId("r1".into()),
            },
        },
        Attack {
            attacker: ArgumentId(1),
            target: ArgumentId(2),
            kind: AttackKind::Undercut {
                target_sub: ArgumentId(2),
                rule_id: RuleId("r2".into()),
            },
        },
        Attack {
            attacker: ArgumentId(2),
            target: ArgumentId(0),
            kind: AttackKind::Undercut {
                target_sub: ArgumentId(0),
                rule_id: RuleId("r3".into()),
            },
        },
    ];

    let defeats = compute_defeats(&attacks, &store, &AlwaysDispreferredOrdering);
    assert_eq!(
        defeats.len(),
        3,
        "all three undercuts should succeed despite AlwaysDispreferred"
    );
}
