mod common;
use common::*;

use pickaxe_rs::formula;
use pickaxe_rs::prelude::*;
use pickaxe_rs::system::ordering::democratic_strict;

// ---
// Ordering helpers specific to this file
// ---

/// Rule ordering for Examples 3.22/3.24: d4 < d2 < d5 (tiers most-preferred first).
fn example_rule_ordering() -> TieredOrdering<RuleId> {
    TieredOrdering::new(vec![
        vec![RuleId("d5".into())],
        vec![RuleId("d2".into())],
        vec![RuleId("d4".into())],
    ])
}

/// Premise ordering for Examples 3.22/3.24: u <' s, x <' s (s is more preferred).
fn example_premise_ordering() -> TieredOrdering<Formula> {
    TieredOrdering::new(vec![vec![formula!(s)], vec![formula!(u), formula!(x)]])
}

// ---
// Corrected set orderings (arXiv:1804.06763 Definition 19)
// ---

/// democratic_strict: ∀∃ quantifier structure with strict < (arXiv:1804.06763 Def 19).
#[test]
fn democratic_strict_forall_exists() {
    let is_lt = |a: &i32, b: &i32| a < b;

    // (a) σ = [2], σ' = [5]: ∀x in {2} ∃y in {5}: 2 < 5 → true
    assert!(democratic_strict(&[2], &[5], is_lt));

    // (b) σ = [4,5], σ' = [2]: ∀x in {4,5} ∃y in {2}: x < y
    //     4 < 2? no. → false (4 fails ∀)
    assert!(!democratic_strict(&[4, 5], &[2], is_lt));

    // (c) σ = [2,4], σ' = [5,3]: ∀x in {2,4} ∃y in {5,3}: x < y
    //     2 < 3 ✓. 4 < 5 ✓. → true
    assert!(democratic_strict(&[2, 4], &[5, 3], is_lt));

    // (d) σ = [2,6], σ' = [5,3]: 2 < 3 ✓, 6 < 5? no. 6 < 3? no. → false
    assert!(!democratic_strict(&[2, 6], &[5, 3], is_lt));

    // (e) Strict vs non-strict distinction: σ = [3], σ' = [3]: 3 < 3 → false
    //     (democratic_leq would return true here since 3 ≤ 3)
    assert!(!democratic_strict(&[3], &[3], is_lt));

    // (f) σ = [2,3], σ' = [3,4]: 2 < 3 ✓, 3 < 4 ✓ → true
    assert!(democratic_strict(&[2, 3], &[3, 4], is_lt));

    // (g) σ = [2,3], σ' = [3,3]: 2 < 3 ✓, 3 < 3? no → false
    assert!(!democratic_strict(&[2, 3], &[3, 3], is_lt));
}

/// democratic_strict: empty-set handling (same clauses 1–2 as all kernel functions).
#[test]
fn democratic_strict_empty_handling() {
    let empty: &[i32] = &[];
    let is_lt = |a: &i32, b: &i32| a < b;

    assert!(!democratic_strict(empty, empty, is_lt));
    assert!(!democratic_strict(empty, &[1], is_lt));
    assert!(democratic_strict(&[1], empty, is_lt));
    assert!(democratic_strict(&[1, 2, 3], empty, is_lt));
}

// ---
// Base orderings
// ---

/// Preference::is_leq() semantics.
#[test]
fn preference_is_leq() {
    assert!(Preference::StrictlyDispreferred.is_leq());
    assert!(Preference::Equal.is_leq());
    assert!(!Preference::StrictlyPreferred.is_leq());
    assert!(!Preference::Incomparable.is_leq());
}

/// TieredOrdering with example tiers [[d5],[d2],[d4]].
#[test]
fn tiered_ordering_example() {
    let ordering = example_rule_ordering();

    assert_eq!(
        ordering.compare(&RuleId("d2".into()), &RuleId("d5".into())),
        Preference::StrictlyDispreferred,
        "d2 < d5"
    );
    assert_eq!(
        ordering.compare(&RuleId("d4".into()), &RuleId("d2".into())),
        Preference::StrictlyDispreferred,
        "d4 < d2"
    );
    assert_eq!(
        ordering.compare(&RuleId("d2".into()), &RuleId("d2".into())),
        Preference::Equal,
        "d2 = d2"
    );
    assert_eq!(
        ordering.compare(&RuleId("d5".into()), &RuleId("d4".into())),
        Preference::StrictlyPreferred,
        "d5 > d4"
    );
}

/// TieredOrdering tiered-vs-untiered and untiered-vs-untiered.
#[test]
fn tiered_ordering_tiered_vs_untiered() {
    let ordering: TieredOrdering<RuleId> =
        TieredOrdering::new(vec![vec![RuleId("d1".into())], vec![RuleId("d2".into())]]);

    // Known vs unknown: incomparable (partial-order reading)
    assert_eq!(
        ordering.compare(&RuleId("d1".into()), &RuleId("d3".into())),
        Preference::Incomparable,
        "tiered d1 vs untiered d3: incomparable"
    );
    assert_eq!(
        ordering.compare(&RuleId("d3".into()), &RuleId("d1".into())),
        Preference::Incomparable,
        "untiered d3 vs tiered d1: incomparable"
    );
    // Unknown vs unknown: incomparable
    assert_eq!(
        ordering.compare(&RuleId("d3".into()), &RuleId("d4".into())),
        Preference::Incomparable,
        "two untiered rules are incomparable"
    );
}

/// TieredOrdering<Formula> as PremiseOrdering.
#[test]
fn tiered_ordering_formula_as_premise_ordering() {
    let ordering = example_premise_ordering();

    let s_prem = Premise {
        formula: formula!(s),
        kind: PremiseKind::Ordinary,
    };
    let u_prem = Premise {
        formula: formula!(u),
        kind: PremiseKind::Ordinary,
    };
    let x_prem = Premise {
        formula: formula!(x),
        kind: PremiseKind::Ordinary,
    };

    assert_eq!(
        PremiseOrdering::compare(&ordering, &u_prem, &s_prem),
        Preference::StrictlyDispreferred,
        "u <' s"
    );
    assert_eq!(
        PremiseOrdering::compare(&ordering, &s_prem, &u_prem),
        Preference::StrictlyPreferred,
        "s >' u"
    );
    assert_eq!(
        PremiseOrdering::compare(&ordering, &u_prem, &x_prem),
        Preference::Equal,
        "u =' x (same tier)"
    );
}

// ---
// Last-link ordering
// ---

/// Example 3.22 last-link comparisons at the ordering level.
///
/// C3 vs B1: LastDefRules(C3) = {d4}, LastDefRules(B1) = ∅.
///   {d4} ⊴ ∅ → C3 is weaker → StrictlyDispreferred.
/// D4 vs B2: LastDefRules(D4) = {d5}, LastDefRules(B2) = {d2}.
///   d2 < d5 → B2 weaker → D4 is StrictlyPreferred.
#[test]
fn last_link_example_3_22() {
    let (store, _) = running_example_store();
    let args = find_running_example_args(&store);

    let ordering = LastLinkOrdering {
        rule_ordering: Box::new(example_rule_ordering()),
        premise_ordering: Box::new(example_premise_ordering()),
        lifting: LiftingStrategy::Elitist,
    };

    assert_eq!(
        ordering.compare(args.c3, args.b1, &store),
        Preference::StrictlyDispreferred,
        "C3 < B1 under last-link (LastDefRules(C3)={{d4}} ⊴ ∅)"
    );

    assert_eq!(
        ordering.compare(args.d4, args.b2, &store),
        Preference::StrictlyPreferred,
        "D4 > B2 under last-link (d2 < d5)"
    );
}

/// Last-link premise fallback: both have empty LastDefRules.
///
/// B1 (premise s) vs C1 (premise u): both premise-only, falls through
/// to Elitist premise comparison. s > u → B1 preferred.
#[test]
fn last_link_premise_fallback() {
    let (store, _) = running_example_store();
    let args = find_running_example_args(&store);

    let ordering = LastLinkOrdering {
        rule_ordering: Box::new(example_rule_ordering()),
        premise_ordering: Box::new(example_premise_ordering()),
        lifting: LiftingStrategy::Elitist,
    };

    assert_eq!(
        ordering.compare(args.b1, args.c1, &store),
        Preference::StrictlyPreferred,
        "B1 > C1 (premise s > premise u under Elitist premise comparison)"
    );
    assert_eq!(
        ordering.compare(args.c1, args.b1, &store),
        Preference::StrictlyDispreferred,
        "C1 < B1"
    );
}

/// Example 3.25 last-link: A3 vs B2 in the library-access system.
///
/// LastDefRules(A3) = {d2}, LastDefRules(B2) = {d3}. d3 < d2 → B2 ≺ A3.
#[test]
fn last_link_example_3_25_library_access() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .ordinary_premise(formula!(Snores))
        .ordinary_premise(formula!(Professor))
        .named_defeasible_rule(
            "d1",
            formula!(d1),
            vec![formula!(Snores)],
            formula!(Misbehaves),
        )
        .named_defeasible_rule(
            "d2",
            formula!(d2),
            vec![formula!(Misbehaves)],
            formula!(AccessDenied),
        )
        .named_defeasible_rule(
            "d3",
            formula!(d3),
            vec![formula!(Professor)],
            formula!(!AccessDenied),
        )
        .build();

    let rule_ord = TieredOrdering::new(vec![
        vec![RuleId("d2".into())],
        vec![RuleId("d3".into())],
        vec![RuleId("d1".into())],
    ]);
    let premise_ord = TieredOrdering::new(vec![vec![formula!(Professor)], vec![formula!(Snores)]]);

    let ordering = LastLinkOrdering {
        rule_ordering: Box::new(rule_ord),
        premise_ordering: Box::new(premise_ord),
        lifting: LiftingStrategy::Elitist,
    };

    let grounder = NaiveGrounder;
    let grounded = grounder.ground(&system).expect("grounding should succeed");
    let constructor = ForwardChainingConstructor;
    let store = constructor.construct(&grounded);

    let a3 = find_arg_by_conclusion_and_rule(&store, &formula!(AccessDenied), "d2")
        .expect("A3: AccessDenied via d2");
    let b2 = find_arg_by_conclusion_and_rule(&store, &formula!(!AccessDenied), "d3")
        .expect("B2: ¬AccessDenied via d3");

    assert_eq!(
        ordering.compare(a3, b2, &store),
        Preference::StrictlyPreferred,
        "A3 > B2 under last-link (LastDefRules(A3)={{d2}} > LastDefRules(B2)={{d3}})"
    );
}

/// Last-link with missing argument ID → Incomparable.
#[test]
fn last_link_missing_argument_id() {
    let (store, _) = running_example_store();
    let args = find_running_example_args(&store);

    let ordering = LastLinkOrdering {
        rule_ordering: Box::new(example_rule_ordering()),
        premise_ordering: Box::new(example_premise_ordering()),
        lifting: LiftingStrategy::Elitist,
    };

    let invalid = ArgumentId(9999);
    assert_eq!(
        ordering.compare(args.a1, invalid, &store),
        Preference::Incomparable,
        "valid vs invalid → Incomparable"
    );
    assert_eq!(
        ordering.compare(invalid, args.a1, &store),
        Preference::Incomparable,
        "invalid vs valid → Incomparable"
    );
}

/// Democratic vs Elitist last-link produces different results.
///
/// To get multiple last defeasible rules, we need a strict rule combining two
/// independent defeasible branches:
///   d1: p ⇒ a   (defeasible, least preferred — tier 2)
///   d3: q ⇒ b   (defeasible, most preferred — tier 0)
///   s1: a, b → c (strict — combines both branches)
///   d2: r ⇒ ¬c  (defeasible, middle — tier 1)
///
/// Argument for c has LastDefRules = {d1, d3} (the topmost defeasible rules
/// in each branch, just below the strict rule s1).
/// Argument for ¬c has LastDefRules = {d2}.
///
/// Tiers: d3 (tier 0), d2 (tier 1), d1 (tier 2). So d1 < d2 < d3 in preference.
///
/// Comparing LastDefRules(c) vs LastDefRules(¬c), i.e. {d1,d3} vs {d2}:
///
/// Check {d1,d3} ◁ {d2} (c weaker?):
///   Elitist: ∃x∈{d1,d3}: x < d2? d1 < d2 → yes → true.
///   Democratic: ∀x∈{d1,d3}: x < d2? d1 < d2 yes, d3 < d2? no → false.
///
/// Check {d2} ◁ {d1,d3} (¬c weaker?):
///   Elitist: d2 < d1? no → false.
///   Democratic: d2 < d3? yes → true.
///
/// Elitist: c ◁ ¬c true, ¬c ◁ c false → c is StrictlyDispreferred.
/// Democratic: c ◁ ¬c false, ¬c ◁ c true → ¬c is StrictlyDispreferred (c preferred!).
#[test]
fn last_link_democratic_vs_elitist() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .axiom(formula!(p))
        .axiom(formula!(q))
        .axiom(formula!(r))
        .named_defeasible_rule("d1", formula!(d1), vec![formula!(p)], formula!(a))
        .named_defeasible_rule("d3", formula!(d3), vec![formula!(q)], formula!(b))
        .strict_rule("s1", vec![formula!(a), formula!(b)], formula!(c))
        .named_defeasible_rule("d2", formula!(d2), vec![formula!(r)], formula!(!c))
        .build();

    let rule_ord = TieredOrdering::new(vec![
        vec![RuleId("d3".into())],
        vec![RuleId("d2".into())],
        vec![RuleId("d1".into())],
    ]);

    let grounder = NaiveGrounder;
    let grounded = grounder.ground(&system).expect("grounding should succeed");
    let constructor = ForwardChainingConstructor;
    let store = constructor.construct(&grounded);

    let arg_c = store
        .all_arguments()
        .find(|(_, a)| *a.conclusion() == formula!(c))
        .map(|(id, _)| id)
        .expect("argument concluding c (via strict rule over d1 and d3 branches)");
    let arg_nc = store
        .all_arguments()
        .find(|(_, a)| *a.conclusion() == formula!(!c))
        .map(|(id, _)| id)
        .expect("argument concluding ¬c (via d2)");

    let elitist_ord = LastLinkOrdering {
        rule_ordering: Box::new(rule_ord.clone()),
        premise_ordering: Box::new(NoPreference),
        lifting: LiftingStrategy::Elitist,
    };
    let democratic_ord = LastLinkOrdering {
        rule_ordering: Box::new(rule_ord),
        premise_ordering: Box::new(NoPreference),
        lifting: LiftingStrategy::Democratic,
    };

    let elitist_result = elitist_ord.compare(arg_c, arg_nc, &store);
    let democratic_result = democratic_ord.compare(arg_c, arg_nc, &store);

    assert_ne!(
        elitist_result, democratic_result,
        "Elitist and democratic must produce different results for this case"
    );
    assert_eq!(
        elitist_result,
        Preference::StrictlyDispreferred,
        "Under elitist, c is weaker (d1 ∈ {{d1,d3}} satisfies d1 < d2)"
    );
    assert_eq!(
        democratic_result,
        Preference::StrictlyPreferred,
        "Under democratic, c is preferred (¬c's d2 < d3 makes ¬c weaker)"
    );
}

// ---
// Weakest-link ordering
// ---

/// Example 3.24 weakest-link comparisons at the ordering level.
///
/// C3 vs B1: C3 has ordinary premises {u}, defeasible rules {d4}.
///   B1 has premises {s}, no defeasible rules but B1 is not firm+strict
///   in the weakest-link sense... B1 is strict (no defeasible rules) but
///   not firm (ordinary premise). Falls through to case (3).
///   Prem_p(C3) = {u} ⊴ {s} = Prem_p(B1) and DefRules(C3) = {d4} ⊴ ∅ = DefRules(B1).
///   DefRules(B1) is empty → elitist_leq({d4}, ∅) = true, elitist_leq(∅, {d4}) = false.
///   Prem_p: elitist_leq({u}, {s}) → u ≤ s (u is dispreferred) → true.
///           elitist_leq({s}, {u}) → s ≤ u? no → false.
///   C3 ⊴ B1 in both dims → C3 StrictlyDispreferred.
///
/// D4 vs B2: Under weakest-link, D4 < B2 (opposite of last-link).
///   Prem_p(D4) = {u,x}, Prem_p(B2) = {s}.
///   DefRules(D4) = {d4,d5}, DefRules(B2) = {d2}.
///   elitist_leq({u,x}, {s}): ∃x in {u,x}: u ≤ s ✓ → true.
///   elitist_leq({s}, {u,x}): s ≤ u? no, s ≤ x? no → false.
///   elitist_leq({d4,d5}, {d2}): ∃r in {d4,d5}: d4 ≤ d2 ✓ → true.
///   elitist_leq({d2}, {d4,d5}): d2 ≤ d4? no, d2 ≤ d5? yes → true.
///   Wait — d2 ≤ d5? The ordering has d5 > d2 > d4, so d2 < d5,
///   meaning is_leq(d2, d5) = true.
///   So rules: a_leq_b = true, b_leq_a = true → Equal for rules.
///   But prems: a_leq_b = true, b_leq_a = false.
///   Combined: D4_leq_B2 = true && true = true.
///             B2_leq_D4 = false && true = false.
///   → D4 StrictlyDispreferred.
#[test]
fn weakest_link_example_3_24() {
    let (store, _) = running_example_store();
    let args = find_running_example_args(&store);

    let ordering = WeakestLinkOrdering {
        rule_ordering: Box::new(example_rule_ordering()),
        premise_ordering: Box::new(example_premise_ordering()),
        lifting: LiftingStrategy::Elitist,
    };

    assert_eq!(
        ordering.compare(args.c3, args.b1, &store),
        Preference::StrictlyDispreferred,
        "C3 < B1 under weakest-link"
    );

    assert_eq!(
        ordering.compare(args.d4, args.b2, &store),
        Preference::StrictlyDispreferred,
        "D4 < B2 under weakest-link (opposite of last-link)"
    );
}

/// Weakest-link firm+strict case (Definition 3.23 case 1).
///
/// Two axiom-only, strict-rule-only arguments → both firm AND strict.
/// Case 1 (both strict) applies: compare OrdPrems only.
/// Both are firm so OrdPrems = ∅ for both. elitist_leq(∅, ∅) = false
/// for both directions → Incomparable (functionally equivalent to Equal
/// for defeat — neither is StrictlyDispreferred).
#[test]
fn weakest_link_firm_strict_equal() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .axiom(formula!(a))
        .axiom(formula!(b))
        .strict_rule("s1", vec![formula!(a)], formula!(c))
        .strict_rule("s2", vec![formula!(b)], formula!(d))
        .build();

    let grounder = NaiveGrounder;
    let grounded = grounder.ground(&system).expect("grounding should succeed");
    let constructor = ForwardChainingConstructor;
    let store = constructor.construct(&grounded);

    let arg_c = store
        .all_arguments()
        .find(|(_, a)| *a.conclusion() == formula!(c))
        .map(|(id, _)| id)
        .expect("argument for c");
    let arg_d = store
        .all_arguments()
        .find(|(_, a)| *a.conclusion() == formula!(d))
        .map(|(id, _)| id)
        .expect("argument for d");

    let ordering = WeakestLinkOrdering {
        rule_ordering: Box::new(NoPreference),
        premise_ordering: Box::new(NoPreference),
        lifting: LiftingStrategy::Elitist,
    };

    assert_eq!(
        ordering.compare(arg_c, arg_d, &store),
        Preference::Equal,
        "two firm+strict arguments: OrdPrems both empty → Equal (corrected Definition 21)"
    );
}

/// Weakest-link firm+strict vs non-firm (Definition 3.23).
///
/// One argument is firm+strict, the other is not → firm+strict preferred.
#[test]
fn weakest_link_firm_strict_vs_nonfirm() {
    let (store, _) = running_example_store();
    let args = find_running_example_args(&store);

    let ordering = WeakestLinkOrdering {
        rule_ordering: Box::new(example_rule_ordering()),
        premise_ordering: Box::new(example_premise_ordering()),
        lifting: LiftingStrategy::Elitist,
    };

    // A1 is firm+strict (axiom p, no defeasible rules).
    // B2 is not strict (uses d2) and not firm (ordinary premise s).
    assert_eq!(
        ordering.compare(args.a1, args.b2, &store),
        Preference::StrictlyPreferred,
        "firm+strict A1 > non-firm B2 under weakest-link"
    );
    assert_eq!(
        ordering.compare(args.b2, args.a1, &store),
        Preference::StrictlyDispreferred,
        "non-firm B2 < firm+strict A1"
    );
}

/// Example 3.25 weakest-link: A3 vs B2 in the library-access system.
///
/// Under weakest-link, A3 ≺ B2 (opposite of last-link).
/// Prem_p(A3) = {Snores}, Prem_p(B2) = {Professor}. Snores < Professor.
/// DefRules(A3) = {d1,d2}, DefRules(B2) = {d3}.
/// elitist_leq({d1,d2}, {d3}): d1 ≤ d3? d1 is tier 2, d3 is tier 1 → yes. → true.
/// elitist_leq({d3}, {d1,d2}): d3 ≤ d1? d3 > d1 → no. d3 ≤ d2? d3 < d2 → yes. → true.
/// Rules: Equal. Prems: A3 weaker. → A3 StrictlyDispreferred.
#[test]
fn weakest_link_example_3_25_library_access() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .ordinary_premise(formula!(Snores))
        .ordinary_premise(formula!(Professor))
        .named_defeasible_rule(
            "d1",
            formula!(d1),
            vec![formula!(Snores)],
            formula!(Misbehaves),
        )
        .named_defeasible_rule(
            "d2",
            formula!(d2),
            vec![formula!(Misbehaves)],
            formula!(AccessDenied),
        )
        .named_defeasible_rule(
            "d3",
            formula!(d3),
            vec![formula!(Professor)],
            formula!(!AccessDenied),
        )
        .build();

    let rule_ord = TieredOrdering::new(vec![
        vec![RuleId("d2".into())],
        vec![RuleId("d3".into())],
        vec![RuleId("d1".into())],
    ]);
    let premise_ord = TieredOrdering::new(vec![vec![formula!(Professor)], vec![formula!(Snores)]]);

    let ordering = WeakestLinkOrdering {
        rule_ordering: Box::new(rule_ord),
        premise_ordering: Box::new(premise_ord),
        lifting: LiftingStrategy::Elitist,
    };

    let grounder = NaiveGrounder;
    let grounded = grounder.ground(&system).expect("grounding should succeed");
    let constructor = ForwardChainingConstructor;
    let store = constructor.construct(&grounded);

    let a3 = find_arg_by_conclusion_and_rule(&store, &formula!(AccessDenied), "d2")
        .expect("A3: AccessDenied via d2");
    let b2 = find_arg_by_conclusion_and_rule(&store, &formula!(!AccessDenied), "d3")
        .expect("B2: ¬AccessDenied via d3");

    assert_eq!(
        ordering.compare(a3, b2, &store),
        Preference::StrictlyDispreferred,
        "A3 < B2 under weakest-link (opposite of last-link)"
    );
}

/// Weakest-link strict-but-plausible (Definition 3.23 case 1).
///
/// Two strict-but-not-firm arguments (ordinary premises, strict rules only).
/// Case 1 (both strict) applies: compare OrdPrems only.
/// Prem_p(c) = {a}, Prem_p(d) = {b}. Premise ordering: a > b → c preferred.
#[test]
fn weakest_link_strict_but_plausible() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .ordinary_premise(formula!(a))
        .ordinary_premise(formula!(b))
        .strict_rule("s1", vec![formula!(a)], formula!(c))
        .strict_rule("s2", vec![formula!(b)], formula!(d))
        .build();

    let grounder = NaiveGrounder;
    let grounded = grounder.ground(&system).expect("grounding should succeed");
    let constructor = ForwardChainingConstructor;
    let store = constructor.construct(&grounded);

    let arg_c = store
        .all_arguments()
        .find(|(_, a)| *a.conclusion() == formula!(c))
        .map(|(id, _)| id)
        .expect("argument for c");
    let arg_d = store
        .all_arguments()
        .find(|(_, a)| *a.conclusion() == formula!(d))
        .map(|(id, _)| id)
        .expect("argument for d");

    let arg_c_obj = store.get(arg_c).unwrap();
    let arg_d_obj = store.get(arg_d).unwrap();
    assert!(arg_c_obj.is_strict(&store), "c is strict");
    assert!(
        !arg_c_obj.is_firm(&store),
        "c is NOT firm (ordinary premise)"
    );
    assert!(arg_d_obj.is_strict(&store), "d is strict");
    assert!(
        !arg_d_obj.is_firm(&store),
        "d is NOT firm (ordinary premise)"
    );

    let premise_ord = TieredOrdering::new(vec![vec![formula!(a)], vec![formula!(b)]]);
    let ordering = WeakestLinkOrdering {
        rule_ordering: Box::new(NoPreference),
        premise_ordering: Box::new(premise_ord),
        lifting: LiftingStrategy::Elitist,
    };

    let result = ordering.compare(arg_c, arg_d, &store);

    // Case 1 (Def 3.23 clause 1): both strict → compare OrdPrems only.
    // Prem_p(c) = {a}, Prem_p(d) = {b}. a > b → c StrictlyPreferred.
    assert_eq!(
        result,
        Preference::StrictlyPreferred,
        "strict-but-plausible: c preferred (premise a > b)"
    );
}

/// Weakest-link firm-but-defeasible (Definition 3.23 case 2).
///
/// Two firm-but-not-strict arguments (axiom premises, defeasible rules).
/// Case 2 (both firm) applies: compare DefRules only.
/// DefRules(e) = {d1}, DefRules(f) = {d2}. Rule ordering: d1 > d2 → e preferred.
#[test]
fn weakest_link_firm_but_defeasible() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .axiom(formula!(a))
        .axiom(formula!(b))
        .named_defeasible_rule("d1", formula!(d1), vec![formula!(a)], formula!(e))
        .named_defeasible_rule("d2", formula!(d2), vec![formula!(b)], formula!(f))
        .build();

    let grounder = NaiveGrounder;
    let grounded = grounder.ground(&system).expect("grounding should succeed");
    let constructor = ForwardChainingConstructor;
    let store = constructor.construct(&grounded);

    let arg_e = store
        .all_arguments()
        .find(|(_, a)| *a.conclusion() == formula!(e))
        .map(|(id, _)| id)
        .expect("argument for e");
    let arg_f = store
        .all_arguments()
        .find(|(_, a)| *a.conclusion() == formula!(f))
        .map(|(id, _)| id)
        .expect("argument for f");

    let arg_e_obj = store.get(arg_e).unwrap();
    let arg_f_obj = store.get(arg_f).unwrap();
    assert!(arg_e_obj.is_firm(&store), "e is firm (axiom premise)");
    assert!(
        !arg_e_obj.is_strict(&store),
        "e is NOT strict (defeasible rule)"
    );
    assert!(arg_f_obj.is_firm(&store), "f is firm (axiom premise)");
    assert!(
        !arg_f_obj.is_strict(&store),
        "f is NOT strict (defeasible rule)"
    );

    let rule_ord = TieredOrdering::new(vec![vec![RuleId("d1".into())], vec![RuleId("d2".into())]]);
    let ordering = WeakestLinkOrdering {
        rule_ordering: Box::new(rule_ord),
        premise_ordering: Box::new(NoPreference),
        lifting: LiftingStrategy::Elitist,
    };

    let result = ordering.compare(arg_e, arg_f, &store);

    // Case 2 (Def 3.23 clause 2): both firm → compare DefRules only.
    // DefRules(e) = {d1}, DefRules(f) = {d2}. d1 > d2 → e StrictlyPreferred.
    assert_eq!(
        result,
        Preference::StrictlyPreferred,
        "firm-but-defeasible: e preferred (rule d1 > d2)"
    );

    // Verify the reverse direction.
    assert_eq!(
        ordering.compare(arg_f, arg_e, &store),
        Preference::StrictlyDispreferred,
        "firm-but-defeasible: f dispreferred (rule d2 < d1)"
    );
}

/// Weakest-link with missing argument ID → Incomparable.
#[test]
fn weakest_link_missing_argument_id() {
    let (store, _) = running_example_store();
    let args = find_running_example_args(&store);

    let ordering = WeakestLinkOrdering {
        rule_ordering: Box::new(example_rule_ordering()),
        premise_ordering: Box::new(example_premise_ordering()),
        lifting: LiftingStrategy::Elitist,
    };

    let invalid = ArgumentId(9999);
    assert_eq!(
        ordering.compare(args.a1, invalid, &store),
        Preference::Incomparable,
    );
    assert_eq!(
        ordering.compare(invalid, args.a1, &store),
        Preference::Incomparable,
    );
}

/// Democratic vs Elitist weakest-link produces different results.
///
/// Uses the "both firm" case (clause 2) where only defeasible rules are compared.
/// Argument A has DefRules = {d1, d3}, Argument B has DefRules = {d2}.
/// Tiers: d3 (tier 0, most preferred), d2 (tier 1), d1 (tier 2, least preferred).
///
/// Check A ◁ B ({d1,d3} ◁ {d2}):
///   Elitist: ∃x∈{d1,d3}: ∀y∈{d2}: x < y? d1 < d2 → yes → true.
///   Democratic: ∀x∈{d1,d3}: ∃y∈{d2}: x < y? d1 < d2 yes, d3 < d2? no → false.
///
/// Check B ◁ A ({d2} ◁ {d1,d3}):
///   Elitist: ∃x∈{d2}: ∀y∈{d1,d3}: d2 < d1? no → false.
///   Democratic: ∀x∈{d2}: ∃y∈{d1,d3}: d2 < d3? yes → true.
///
/// Elitist: A ◁ B true, B ◁ A false → A dispreferred.
/// Democratic: A ◁ B false, B ◁ A true → B dispreferred.
#[test]
fn weakest_link_democratic_vs_elitist() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .axiom(formula!(p))
        .axiom(formula!(q))
        .named_defeasible_rule("d1", formula!(d1), vec![formula!(p)], formula!(a))
        .named_defeasible_rule("d3", formula!(d3), vec![formula!(a)], formula!(c))
        .named_defeasible_rule("d2", formula!(d2), vec![formula!(q)], formula!(!c))
        .build();

    let rule_ord = TieredOrdering::new(vec![
        vec![RuleId("d3".into())],
        vec![RuleId("d2".into())],
        vec![RuleId("d1".into())],
    ]);

    let grounder = NaiveGrounder;
    let grounded = grounder.ground(&system).expect("grounding should succeed");
    let constructor = ForwardChainingConstructor;
    let store = constructor.construct(&grounded);

    let arg_c = store
        .all_arguments()
        .find(|(_, a)| *a.conclusion() == formula!(c))
        .map(|(id, _)| id)
        .expect("argument concluding c (via d1 then d3, DefRules = {d1,d3})");
    let arg_nc = store
        .all_arguments()
        .find(|(_, a)| *a.conclusion() == formula!(!c))
        .map(|(id, _)| id)
        .expect("argument concluding ¬c (via d2, DefRules = {d2})");

    let elitist_ord = WeakestLinkOrdering {
        rule_ordering: Box::new(rule_ord.clone()),
        premise_ordering: Box::new(NoPreference),
        lifting: LiftingStrategy::Elitist,
    };
    let democratic_ord = WeakestLinkOrdering {
        rule_ordering: Box::new(rule_ord),
        premise_ordering: Box::new(NoPreference),
        lifting: LiftingStrategy::Democratic,
    };

    let elitist_result = elitist_ord.compare(arg_c, arg_nc, &store);
    let democratic_result = democratic_ord.compare(arg_c, arg_nc, &store);

    assert_ne!(
        elitist_result, democratic_result,
        "Elitist and democratic must produce different results for this case"
    );
}

// ---
// Defeat computation
// ---

/// Defeat under last-link ordering for Example 3.7.
///
/// (a) B3 undercut on A2 → succeeds (undercuts always succeed)
/// (b) C3 undermine on B1 → fails (C3 strictly dispreferred to B1)
/// (c) D4 rebut on B2 → succeeds (D4 preferred under last-link: d5 > d2)
/// (d) B2 rebut on D4 → fails (B2 strictly dispreferred: d2 < d5)
#[test]
fn defeat_last_link_example() {
    let ordering = LastLinkOrdering {
        rule_ordering: Box::new(example_rule_ordering()),
        premise_ordering: Box::new(example_premise_ordering()),
        lifting: LiftingStrategy::Elitist,
    };

    let pipeline = AspicPipeline::classical(running_example(), Box::new(ordering));
    let result = pipeline.evaluate(Semantics::Grounded).unwrap();
    let store = &result.store;
    let args = find_running_example_args(store);

    let ordering2 = LastLinkOrdering {
        rule_ordering: Box::new(example_rule_ordering()),
        premise_ordering: Box::new(example_premise_ordering()),
        lifting: LiftingStrategy::Elitist,
    };
    let defeats = compute_defeats(&result.attacks, store, &ordering2);

    // (a) B3 undercuts A2 → always succeeds
    assert!(
        defeat_exists(&defeats, args.b3, args.a2),
        "B3 undercut on A2 should succeed"
    );

    // (b) C3 undermines B1 → fails
    assert!(
        !defeat_exists(&defeats, args.c3, args.b1),
        "C3 undermine on B1 should fail (C3 strictly dispreferred)"
    );

    // (c) D4 rebuts B2 → succeeds (d5 > d2 under last-link)
    assert!(
        defeat_exists(&defeats, args.d4, args.b2),
        "D4 rebut on B2 should succeed (d5 > d2)"
    );

    // (d) B2 rebuts D4 → fails (d2 < d5 under last-link)
    assert!(
        !defeat_exists(&defeats, args.b2, args.d4),
        "B2 rebut on D4 should fail (d2 < d5)"
    );
}

/// Defeat under weakest-link ordering for Example 3.7.
///
/// Same attacks but opposite rebut results vs last-link:
/// (a) B3 undercut on A2 → succeeds
/// (b) C3 undermine on B1 → fails
/// (c) D4 rebut on B2 → fails (D4 dispreferred under weakest-link)
/// (d) B2 rebut on D4 → succeeds (B2 preferred under weakest-link)
#[test]
fn defeat_weakest_link_example() {
    let ordering = WeakestLinkOrdering {
        rule_ordering: Box::new(example_rule_ordering()),
        premise_ordering: Box::new(example_premise_ordering()),
        lifting: LiftingStrategy::Elitist,
    };

    let pipeline = AspicPipeline::classical(running_example(), Box::new(ordering));
    let result = pipeline.evaluate(Semantics::Grounded).unwrap();
    let store = &result.store;
    let args = find_running_example_args(store);

    let ordering2 = WeakestLinkOrdering {
        rule_ordering: Box::new(example_rule_ordering()),
        premise_ordering: Box::new(example_premise_ordering()),
        lifting: LiftingStrategy::Elitist,
    };
    let defeats = compute_defeats(&result.attacks, store, &ordering2);

    // (a) Undercut always succeeds
    assert!(
        defeat_exists(&defeats, args.b3, args.a2),
        "B3 undercut on A2 should succeed"
    );

    // (b) C3 undermine on B1 → still fails under weakest-link
    assert!(
        !defeat_exists(&defeats, args.c3, args.b1),
        "C3 undermine on B1 should fail"
    );

    // (c) D4 rebut on B2 → fails (D4 strictly dispreferred under weakest-link)
    assert!(
        !defeat_exists(&defeats, args.d4, args.b2),
        "D4 rebut on B2 should fail under weakest-link (D4 < B2)"
    );

    // (d) B2 rebuts D4 → succeeds (B2 preferred under weakest-link)
    assert!(
        defeat_exists(&defeats, args.b2, args.d4),
        "B2 rebut on D4 should succeed under weakest-link"
    );
}

/// Undercut always succeeds regardless of ordering.
///
/// Even with an ordering that returns StrictlyDispreferred for ALL comparisons,
/// undercuts still succeed as defeats.
#[test]
fn undercut_always_succeeds_regardless_of_ordering() {
    let pipeline = AspicPipeline::classical(running_example(), Box::new(EqualOrdering));
    let result = pipeline.evaluate(Semantics::Grounded).unwrap();
    let store = &result.store;
    let args = find_running_example_args(store);

    let defeats = compute_defeats(&result.attacks, store, &AlwaysDispreferredOrdering);

    // B3 undercuts A2 (and A3) → must succeed even with AlwaysDispreferred
    assert!(
        defeat_exists(&defeats, args.b3, args.a2),
        "undercut B3→A2 should succeed even with StrictlyDispreferred ordering"
    );
    assert!(
        defeat_exists(&defeats, args.b3, args.a3),
        "undercut B3→A3 should succeed even with StrictlyDispreferred ordering"
    );

    // All rebuts and undermines should fail with this ordering
    assert!(
        !defeat_exists(&defeats, args.d4, args.b2),
        "rebut D4→B2 should fail with StrictlyDispreferred ordering"
    );
}

/// Defeat comparison point is target_sub (not target).
///
/// For a rebut attack where attack.target ≠ attack.kind.target_sub,
/// the comparison must be made against target_sub, not the top-level target.
///
/// In the running example, D4 rebuts B3 on sub-arg B2 (target=B3, target_sub=B2).
/// We use an ordering where compare(D4, B3) = StrictlyDispreferred but
/// compare(D4, B2) = StrictlyPreferred. If the comparison is against target_sub (B2),
/// the defeat succeeds. If it were against target (B3), it would fail.
#[test]
fn defeat_comparison_point_is_target_sub() {
    let pipeline = AspicPipeline::classical(running_example(), Box::new(EqualOrdering));
    let result = pipeline.evaluate(Semantics::Grounded).unwrap();
    let store = &result.store;
    let args = find_running_example_args(store);

    /// Custom ordering: D4 > B2, D4 < B3, everything else Equal.
    #[derive(Debug)]
    struct TargetSubOrdering {
        d4: ArgumentId,
        b2: ArgumentId,
        b3: ArgumentId,
    }

    impl ArgumentOrdering for TargetSubOrdering {
        fn compare(&self, a: ArgumentId, b: ArgumentId, _store: &ArgumentStore) -> Preference {
            if a == self.d4 && b == self.b2 {
                Preference::StrictlyPreferred
            } else if (a == self.d4 && b == self.b3) || (a == self.b2 && b == self.d4) {
                Preference::StrictlyDispreferred
            } else if a == self.b3 && b == self.d4 {
                Preference::StrictlyPreferred
            } else {
                Preference::Equal
            }
        }
    }

    let ordering = TargetSubOrdering {
        d4: args.d4,
        b2: args.b2,
        b3: args.b3,
    };
    let defeats = compute_defeats(&result.attacks, store, &ordering);

    // D4 rebuts B3 on sub-arg B2. compare(D4, B2) = StrictlyPreferred → succeeds.
    assert!(
        defeat_exists(&defeats, args.d4, args.b3),
        "D4→B3 defeat should succeed (comparison point is B2, not B3)"
    );
}

// ---
// Power-set orderings
// ---

/// Elitist vs Democratic lifted set preference produces different
/// results on carefully chosen sets.
#[test]
fn elitist_vs_democratic_lifted_difference() {
    let store = ArgumentStore::new();
    let s1 = make_set(&[0, 3]);
    let s2 = make_set(&[1, 2]);

    let elitist = LiftedSetPreference {
        base: Box::new(IdBasedOrdering),
        lifting: LiftingStrategy::Elitist,
    };
    let democratic = LiftedSetPreference {
        base: Box::new(IdBasedOrdering),
        lifting: LiftingStrategy::Democratic,
    };

    let e_result = elitist.compare(&s1, &s2, &store);
    let d_result = democratic.compare(&s1, &s2, &store);

    assert_eq!(
        e_result,
        Preference::StrictlyDispreferred,
        "s1 is dispreferred under Elitist (weakest member 3 drags it down)"
    );
    assert_eq!(
        d_result,
        Preference::StrictlyPreferred,
        "s1 is preferred under Democratic (best member 0 lifts it up)"
    );
    assert_ne!(
        e_result, d_result,
        "Elitist and Democratic should differ on this input"
    );
}

// ---
// Dyrkolbotn counterexample — corrected Definition 19 (arXiv:1804.06763)
// ---

use pickaxe_rs::system::knowledge::Premise;

/// Premise ordering for the Dyrkolbotn counterexample:
/// p ≡ q (group 0), r ≡ s (group 1), cross-group = Incomparable.
#[derive(Debug)]
struct DyrkolbotnPremiseOrdering;

impl PremiseOrdering for DyrkolbotnPremiseOrdering {
    fn compare(&self, a: &Premise, b: &Premise) -> Preference {
        let group_of = |f: &pickaxe_rs::language::formula::Formula| -> Option<usize> {
            let s = format!("{f:?}");
            if s.contains("\"p\"") || s.contains("\"q\"") {
                Some(0)
            } else if s.contains("\"r\"") || s.contains("\"s\"") {
                Some(1)
            } else {
                None
            }
        };
        match (group_of(&a.formula), group_of(&b.formula)) {
            (Some(ga), Some(gb)) if ga == gb => Preference::Equal,
            _ => Preference::Incomparable,
        }
    }
}

/// Dyrkolbotn counterexample verifying the corrected Elitist
/// set comparison (arXiv:1804.06763 Definition 19, Eq. 3).
///
/// Setup: Kp = {p, q, r, s}. Strict rules r1: p,q,r → ¬s etc.
/// Ordering: p ≡ q, r ≡ s, cross-group Incomparable.
///
/// Under the **original** (uncorrected) Elitist: {p,q,r} ⊴ {s} because
/// r ≤ s (r ≡ s). So A1 ≺ S, and A1's undermine of S fails as defeat.
///
/// Under the **corrected** Elitist: {p,q,r} ◁ {s} requires r < s (strict),
/// which fails since r ≡ s. So A1 and S are Incomparable, and the
/// undermine succeeds as defeat (no argument is strictly dispreferred).
#[test]
fn dyrkolbotn_corrected_elitist_no_false_strict() {
    let (system, _) = AspicSystemBuilder::new()
        .with_classical_negation()
        .ordinary_premise(formula!(p))
        .ordinary_premise(formula!(q))
        .ordinary_premise(formula!(r))
        .ordinary_premise(formula!(s))
        .strict_rule(
            "r1",
            vec![formula!(p), formula!(q), formula!(r)],
            formula!(!s),
        )
        .strict_rule(
            "r2",
            vec![formula!(p), formula!(q), formula!(s)],
            formula!(!r),
        )
        .strict_rule(
            "r3",
            vec![formula!(s), formula!(q), formula!(r)],
            formula!(!p),
        )
        .strict_rule(
            "r4",
            vec![formula!(p), formula!(s), formula!(r)],
            formula!(!q),
        )
        .build();

    let grounder = NaiveGrounder;
    let grounded = grounder.ground(&system).expect("grounding");
    let constructor = ForwardChainingConstructor;
    let store = constructor.construct(&grounded);

    let arg_s = store
        .all_arguments()
        .find(|(_, a)| a.premises(&store).len() == 1 && *a.conclusion() == formula!(s))
        .map(|(id, _)| id)
        .expect("premise argument S = [s]");

    let arg_a1 = store
        .all_arguments()
        .find(|(_, a)| *a.conclusion() == formula!(!s) && a.premises(&store).len() > 1)
        .map(|(id, _)| id)
        .expect("argument A1 concluding ¬s");

    let ordering = WeakestLinkOrdering {
        rule_ordering: Box::new(NoPreference),
        premise_ordering: Box::new(DyrkolbotnPremiseOrdering),
        lifting: LiftingStrategy::Elitist,
    };

    let result = ordering.compare(arg_a1, arg_s, &store);

    assert_eq!(
        result,
        Preference::Incomparable,
        "Corrected Elitist: A1 and S should be Incomparable (not StrictlyDispreferred). \
         Under the original (uncorrected) definition, this would incorrectly be \
         StrictlyDispreferred because r ≤ s (r ≡ s) makes {{p,q,r}} ⊴ {{s}}."
    );
}

#[test]
fn deterministic_incomparable_ordering() {
    let (system, _) = AspicSystemBuilder::new()
        .ordinary_premise(formula!(p))
        .ordinary_premise(formula!(q))
        .defeasible_rule("d1", vec![formula!(p)], formula!(r))
        .defeasible_rule("d2", vec![formula!(q)], formula!(s))
        .build();
    let grounder = NaiveGrounder;
    let grounded = grounder.ground(&system).expect("grounding should succeed");
    let store = ForwardChainingConstructor.construct(&grounded);

    let arg_r = store
        .all_arguments()
        .find(|(_, a)| *a.conclusion() == formula!(r))
        .map(|(id, _)| id)
        .expect("argument concluding r");
    let arg_s = store
        .all_arguments()
        .find(|(_, a)| *a.conclusion() == formula!(s))
        .map(|(id, _)| id)
        .expect("argument concluding s");

    let ordering = WeakestLinkOrdering {
        rule_ordering: Box::new(NoPreference),
        premise_ordering: Box::new(NoPreference),
        lifting: LiftingStrategy::Elitist,
    };

    let first_result = ordering.compare(arg_r, arg_s, &store);
    for _ in 0..1000 {
        assert_eq!(
            ordering.compare(arg_r, arg_s, &store),
            first_result,
            "ordering comparison must be deterministic across repeated calls"
        );
    }
}

// ---
// TieredOrdering and NoPreference smoke tests
// ---

#[test]
fn tiered_rule_ordering() {
    let ordering = TieredOrdering::new(vec![
        vec![RuleId("r1".into())],
        vec![RuleId("r2".into()), RuleId("r3".into())],
        vec![RuleId("r4".into())],
    ]);

    assert_eq!(
        ordering.compare(&RuleId("r1".into()), &RuleId("r2".into())),
        Preference::StrictlyPreferred
    );
    assert_eq!(
        ordering.compare(&RuleId("r2".into()), &RuleId("r3".into())),
        Preference::Equal
    );
    assert_eq!(
        ordering.compare(&RuleId("r4".into()), &RuleId("r2".into())),
        Preference::StrictlyDispreferred
    );
    assert_eq!(
        ordering.compare(&RuleId("r5".into()), &RuleId("r6".into())),
        Preference::Incomparable
    );
    assert_eq!(
        ordering.compare(&RuleId("r1".into()), &RuleId("r99".into())),
        Preference::Incomparable
    );
}

#[test]
fn last_link_ordering_basic() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .ordinary_premise(formula!(a))
        .defeasible_rule("d1", vec![formula!(a)], formula!(b))
        .defeasible_rule("d2", vec![formula!(a)], formula!(!b))
        .build();

    let rule_ord = TieredOrdering::new(vec![vec![RuleId("d1".into())], vec![RuleId("d2".into())]]);

    let pipeline = AspicPipeline::classical(
        system,
        Box::new(LastLinkOrdering {
            rule_ordering: Box::new(rule_ord),
            premise_ordering: Box::new(NoPreference),
            lifting: LiftingStrategy::Elitist,
        }),
    );

    let result = pipeline.evaluate(Semantics::Grounded).unwrap();

    let grounded = &result.extensions[0];
    let conclusions: Vec<Formula> = grounded
        .iter()
        .filter_map(|id| result.store.get(*id))
        .map(|a| a.conclusion().clone())
        .collect();

    assert!(
        conclusions.contains(&formula!(b)),
        "b should be in grounded extension. Conclusions: {:?}",
        conclusions
    );
    assert!(
        !conclusions.contains(&formula!(!b)),
        "-b should not be in grounded extension"
    );
}

/// Under M&P Definition 3.19(3), {d1, d2} <=_Eli {d3} holds because d2
/// (which exists in {d1,d2}) is <= every element of {d3}. So the argument
/// with LastDefRules = {d3} is strictly preferred.
#[test]
fn last_link_ordering_mixed_last_rules() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .ordinary_premise(formula!(p))
        .ordinary_premise(formula!(r))
        .ordinary_premise(formula!(t))
        .defeasible_rule("d1", vec![formula!(p)], formula!(q))
        .defeasible_rule("d2", vec![formula!(r)], formula!(s))
        .strict_rule("s1", vec![formula!(q), formula!(s)], formula!(u))
        .defeasible_rule("d3", vec![formula!(t)], formula!(v))
        .build();

    let rule_ord = TieredOrdering::new(vec![
        vec![RuleId("d1".into())],
        vec![RuleId("d3".into())],
        vec![RuleId("d2".into())],
    ]);

    let ordering = LastLinkOrdering {
        rule_ordering: Box::new(rule_ord),
        premise_ordering: Box::new(NoPreference),
        lifting: LiftingStrategy::Elitist,
    };

    let grounder = NaiveGrounder;
    let grounded = grounder.ground(&system).expect("grounding should succeed");
    let constructor = ForwardChainingConstructor;
    let store = constructor.construct(&grounded);

    let arg_u = store
        .all_arguments()
        .find(|(_, a)| *a.conclusion() == formula!(u))
        .map(|(id, _)| id)
        .expect("should have argument for u");

    let arg_v = store
        .all_arguments()
        .find(|(_, a)| *a.conclusion() == formula!(v))
        .map(|(id, _)| id)
        .expect("should have argument for v");

    let result = ordering.compare(arg_u, arg_v, &store);
    assert_eq!(
        result,
        Preference::StrictlyDispreferred,
        "arg_v should be strictly preferred (arg_u dispreferred) under M&P Elitist"
    );
}

#[test]
fn no_preference_ordering() {
    let ordering = NoPreference;
    assert_eq!(
        RuleOrdering::compare(&ordering, &RuleId("a".into()), &RuleId("b".into())),
        Preference::Equal
    );
}
