//! Tests for strict closure, direct consistency, and indirect consistency
//! (Definition 3.4, M&P 2014).

use std::collections::HashSet;

use pickaxe_rs::formula;
use pickaxe_rs::prelude::*;
use pickaxe_rs::system::consistency::{
    is_directly_consistent, is_indirectly_consistent, strict_closure,
};

// --- strict_closure ---

#[test]
fn strict_closure_basic() {
    let s: HashSet<Formula> = [formula!(p), formula!(q)].into_iter().collect();
    let rules = vec![StrictRule {
        id: RuleId("s1".into()),
        antecedents: vec![formula!(p), formula!(q)],
        consequent: formula!(r),
    }];
    let cl = strict_closure(&s, &rules);
    assert!(cl.contains(&formula!(p)));
    assert!(cl.contains(&formula!(q)));
    assert!(cl.contains(&formula!(r)));
    assert_eq!(cl.len(), 3);
}

#[test]
fn strict_closure_chained_rules() {
    let s: HashSet<Formula> = [formula!(p)].into_iter().collect();
    let rules = vec![
        StrictRule {
            id: RuleId("s1".into()),
            antecedents: vec![formula!(p)],
            consequent: formula!(q),
        },
        StrictRule {
            id: RuleId("s2".into()),
            antecedents: vec![formula!(q)],
            consequent: formula!(r),
        },
    ];
    let cl = strict_closure(&s, &rules);
    assert!(cl.contains(&formula!(p)));
    assert!(cl.contains(&formula!(q)));
    assert!(cl.contains(&formula!(r)));
    assert_eq!(cl.len(), 3);
}

#[test]
fn strict_closure_no_applicable_rules() {
    let s: HashSet<Formula> = [formula!(p)].into_iter().collect();
    let rules = vec![StrictRule {
        id: RuleId("s1".into()),
        antecedents: vec![formula!(q)],
        consequent: formula!(r),
    }];
    let cl = strict_closure(&s, &rules);
    assert_eq!(cl, s);
}

#[test]
fn strict_closure_empty_initial_set() {
    let s: HashSet<Formula> = HashSet::new();
    let rules = vec![StrictRule {
        id: RuleId("s1".into()),
        antecedents: vec![formula!(p)],
        consequent: formula!(q),
    }];
    let cl = strict_closure(&s, &rules);
    assert!(cl.is_empty());
}

#[test]
fn strict_closure_no_rules() {
    let s: HashSet<Formula> = [formula!(p), formula!(q)].into_iter().collect();
    let cl = strict_closure(&s, &[]);
    assert_eq!(cl, s);
}

#[test]
fn strict_closure_idempotence() {
    let s: HashSet<Formula> = [formula!(p), formula!(q)].into_iter().collect();
    let rules = vec![StrictRule {
        id: RuleId("s1".into()),
        antecedents: vec![formula!(p), formula!(q)],
        consequent: formula!(r),
    }];
    let cl1 = strict_closure(&s, &rules);
    let cl2 = strict_closure(&cl1, &rules);
    assert_eq!(cl1, cl2, "Cl(Cl(S)) must equal Cl(S)");
}

// --- is_directly_consistent ---

#[test]
fn directly_consistent_no_conflict() {
    let cf = ContrarinessFunction::new().with_classical_negation();
    let s: HashSet<Formula> = [formula!(p), formula!(q)].into_iter().collect();
    assert!(is_directly_consistent(&s, &cf));
}

#[test]
fn directly_inconsistent_classical_negation() {
    let cf = ContrarinessFunction::new().with_classical_negation();
    let s: HashSet<Formula> = [formula!(p), formula!(!p)].into_iter().collect();
    assert!(!is_directly_consistent(&s, &cf));
}

#[test]
fn directly_inconsistent_explicit_contrary() {
    let mut cf = ContrarinessFunction::new();
    cf.add_contrary(formula!(p), formula!(q));
    let s: HashSet<Formula> = [formula!(p), formula!(q)].into_iter().collect();
    assert!(!is_directly_consistent(&s, &cf));
}

#[test]
fn directly_consistent_empty_set() {
    let cf = ContrarinessFunction::new().with_classical_negation();
    let s: HashSet<Formula> = HashSet::new();
    assert!(is_directly_consistent(&s, &cf));
}

#[test]
fn directly_consistent_singleton() {
    let cf = ContrarinessFunction::new().with_classical_negation();
    let s: HashSet<Formula> = [formula!(p)].into_iter().collect();
    assert!(is_directly_consistent(&s, &cf));
}

// --- is_indirectly_consistent ---

#[test]
fn indirectly_inconsistent_via_strict_rule() {
    // {p, q} with strict rule p, q → ¬p under classical negation:
    // Cl({p,q}) = {p, q, ¬p} which is directly inconsistent.
    let cf = ContrarinessFunction::new().with_classical_negation();
    let s: HashSet<Formula> = [formula!(p), formula!(q)].into_iter().collect();
    let rules = vec![StrictRule {
        id: RuleId("s1".into()),
        antecedents: vec![formula!(p), formula!(q)],
        consequent: formula!(!p),
    }];
    assert!(!is_indirectly_consistent(&s, &rules, &cf));
}

#[test]
fn indirectly_and_directly_consistent() {
    let cf = ContrarinessFunction::new().with_classical_negation();
    let s: HashSet<Formula> = [formula!(p), formula!(q)].into_iter().collect();
    let rules = vec![StrictRule {
        id: RuleId("s1".into()),
        antecedents: vec![formula!(p), formula!(q)],
        consequent: formula!(r),
    }];
    assert!(is_directly_consistent(&s, &cf));
    assert!(is_indirectly_consistent(&s, &rules, &cf));
}

#[test]
fn directly_consistent_but_indirectly_inconsistent() {
    // {p} is directly consistent. Strict rule p → q, and explicit contrary q attacks p.
    // Cl({p}) = {p, q}, and q is contrary of p → directly inconsistent.
    let mut cf = ContrarinessFunction::new();
    cf.add_contrary(formula!(p), formula!(q));
    let s: HashSet<Formula> = [formula!(p)].into_iter().collect();
    let rules = vec![StrictRule {
        id: RuleId("s1".into()),
        antecedents: vec![formula!(p)],
        consequent: formula!(q),
    }];
    assert!(
        is_directly_consistent(&s, &cf),
        "directly consistent (only p, no q yet)"
    );
    assert!(
        !is_indirectly_consistent(&s, &rules, &cf),
        "indirectly inconsistent (closure adds q which attacks p)"
    );
}

#[test]
fn indirect_consistency_no_strict_rules_equals_direct() {
    let cf = ContrarinessFunction::new().with_classical_negation();
    let s: HashSet<Formula> = [formula!(p), formula!(q)].into_iter().collect();
    let direct = is_directly_consistent(&s, &cf);
    let indirect = is_indirectly_consistent(&s, &[], &cf);
    assert_eq!(direct, indirect, "with no strict rules, indirect = direct");
}
