//! Tests for the generalised contrariness function: contrary/contradictory
//! relations, contraries_of queries, and classical negation mode
//! (Definition 5.1, M&P 2014).

use pickaxe_rs::formula;
use pickaxe_rs::prelude::*;

// --- add_contrary() asymmetry ---

#[test]
fn contrary_is_asymmetric() {
    let mut cf = ContrarinessFunction::new();
    let target = formula!(p);
    let attacker = formula!(q);
    cf.add_contrary(target.clone(), attacker.clone());

    assert!(
        cf.is_contrary(&target, &attacker),
        "attacker should attack target"
    );
    assert!(
        !cf.is_contrary(&attacker, &target),
        "target should NOT attack attacker"
    );
}

// --- add_contradictory() symmetry ---

#[test]
fn contradictory_is_symmetric() {
    let mut cf = ContrarinessFunction::new();
    let a = formula!(p);
    let b = formula!(q);
    cf.add_contradictory(a.clone(), b.clone());

    assert!(cf.is_contrary(&a, &b), "b should attack a");
    assert!(cf.is_contrary(&b, &a), "a should attack b");
}

#[test]
fn contradictory_entries_have_contradictory_relation() {
    let mut cf = ContrarinessFunction::new();
    let a = formula!(p);
    let b = formula!(q);
    cf.add_contradictory(a.clone(), b.clone());

    let entries_a = cf.entries().get(&a).unwrap();
    assert!(entries_a
        .iter()
        .any(|(f, r)| f == &b && *r == ContrarinessRelation::Contradictory));

    let entries_b = cf.entries().get(&b).unwrap();
    assert!(entries_b
        .iter()
        .any(|(f, r)| f == &a && *r == ContrarinessRelation::Contradictory));
}

// --- contraries_of() completeness ---

#[test]
fn contraries_of_returns_explicit_entries() {
    let mut cf = ContrarinessFunction::new();
    let target = formula!(p);
    let attacker1 = formula!(q);
    let attacker2 = formula!(r);
    cf.add_contrary(target.clone(), attacker1.clone());
    cf.add_contradictory(target.clone(), attacker2.clone());

    let result = cf.contraries_of(&target);
    assert!(result.contains(&attacker1));
    assert!(result.contains(&attacker2));
}

#[test]
fn contraries_of_returns_no_duplicates_with_classical_negation() {
    let mut cf = ContrarinessFunction::new().with_classical_negation();
    let p = formula!(p);
    let neg_p = formula!(!p);
    cf.add_contradictory(p.clone(), neg_p.clone());

    let result = cf.contraries_of(&p);
    let neg_count = result.iter().filter(|f| **f == neg_p).count();
    assert_eq!(
        neg_count, 1,
        "¬p should appear exactly once even with classical negation overlap"
    );
}

// --- Classical negation mode ---

#[test]
fn classical_negation_makes_p_and_neg_p_contraries() {
    let cf = ContrarinessFunction::new().with_classical_negation();
    let p = formula!(p);
    let neg_p = formula!(!p);

    assert!(
        cf.is_contrary(&p, &neg_p),
        "¬p should attack p under classical negation"
    );
    assert!(
        cf.is_contrary(&neg_p, &p),
        "p should attack ¬p under classical negation"
    );
}

#[test]
fn classical_negation_disabled_by_default() {
    let cf = ContrarinessFunction::new();
    let p = formula!(p);
    let neg_p = formula!(!p);

    assert!(
        !cf.is_contrary(&p, &neg_p),
        "no automatic contrariness without classical negation"
    );
    assert!(
        !cf.is_contrary(&neg_p, &p),
        "no automatic contrariness without classical negation"
    );
}

// --- contraries_of with explicit + classical negation ---

#[test]
fn contraries_of_union_of_explicit_and_classical() {
    let mut cf = ContrarinessFunction::new().with_classical_negation();
    let p = formula!(p);
    let q = formula!(q);
    let neg_p = formula!(!p);
    cf.add_contrary(p.clone(), q.clone());

    let result = cf.contraries_of(&p);
    assert!(result.contains(&q), "explicit contrary q should be present");
    assert!(
        result.contains(&neg_p),
        "classical negation ¬p should be present"
    );
}

#[test]
fn classical_negation_with_predicate_atom() {
    let cf = ContrarinessFunction::new().with_classical_negation();
    let flies = formula!(flies(tweety));
    let not_flies = formula!(!flies(tweety));

    assert!(cf.is_contrary(&flies, &not_flies));
    assert!(cf.is_contrary(&not_flies, &flies));
}
