//! Direct and indirect consistency checks for sets of formulae.
//!
//! Implements Definition 3.4 from Modgil & Prakken (2014): strict closure Cl(S),
//! direct consistency, and indirect consistency. These are standalone utility
//! functions that operate on sets of formulae relative to an argumentation
//! system's strict rules and contrariness function.

use std::collections::HashSet;

use crate::error::{AspicError, SolverError};
use crate::language::formula::Formula;
use crate::system::contrariness::ContrarinessFunction;
use crate::system::rules::StrictRule;

const POWERSET_LIMIT: usize = 64;

/// Compute the strict closure Cl(S) of a set of formulae under the given strict rules.
///
/// Returns the smallest set containing `initial` and the consequent of every
/// strict rule whose antecedents are all in the closure.
///
/// # References
///
/// Definition 3.4 in Modgil & Prakken (2014): "the closure of S under strict
/// rules, denoted Cl(S), \[is\] the smallest set containing S and the consequent
/// of any strict rule in `R_s` whose antecedents are in Cl(S)."
///
/// # Examples
///
/// ```
/// use std::collections::HashSet;
/// use pickaxe_rs::formula;
/// use pickaxe_rs::prelude::*;
/// use pickaxe_rs::system::consistency::strict_closure;
///
/// 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!(r)));
/// ```
pub fn strict_closure(initial: &HashSet<Formula>, strict_rules: &[StrictRule]) -> HashSet<Formula> {
    let mut result = initial.clone();
    loop {
        let mut changed = false;
        for rule in strict_rules {
            if rule.antecedents.iter().all(|a| result.contains(a))
                && result.insert(rule.consequent.clone())
            {
                changed = true;
            }
        }
        if !changed {
            break;
        }
    }
    result
}

/// Check whether a set of formulae is directly consistent.
///
/// A set S is directly consistent iff there do not exist ψ, ϕ ∈ S such that
/// ψ ∈ ϕ̄ (i.e., `contrariness.is_contrary(ϕ, ψ)` returns true for some
/// ordered pair).
///
/// # References
///
/// Definition 3.4 in Modgil & Prakken (2014), generalised per §5: "a set S is
/// directly consistent iff ∄ψ, ϕ ∈ S such that ψ ∈ ϕ̄."
///
/// # Examples
///
/// ```
/// use std::collections::HashSet;
/// use pickaxe_rs::formula;
/// use pickaxe_rs::prelude::*;
/// use pickaxe_rs::system::consistency::is_directly_consistent;
///
/// let cf = ContrarinessFunction::new().with_classical_negation();
/// let consistent: HashSet<Formula> = [formula!(p), formula!(q)].into_iter().collect();
/// assert!(is_directly_consistent(&consistent, &cf));
///
/// let inconsistent: HashSet<Formula> = [formula!(p), formula!(!p)].into_iter().collect();
/// assert!(!is_directly_consistent(&inconsistent, &cf));
/// ```
pub fn is_directly_consistent(
    formulas: &HashSet<Formula>,
    contrariness: &ContrarinessFunction,
) -> bool {
    let items: Vec<&Formula> = formulas.iter().collect();
    for (i, target) in items.iter().enumerate() {
        for (j, attacker) in items.iter().enumerate() {
            if i != j && contrariness.is_contrary(target, attacker) {
                return false;
            }
        }
    }
    true
}

/// Check whether a set of formulae is indirectly consistent.
///
/// A set S is indirectly consistent iff Cl(S) is directly consistent, where
/// Cl(S) is the strict closure of S.
///
/// # References
///
/// Definition 3.4 in Modgil & Prakken (2014): "indirectly consistent iff Cl(S)
/// is directly consistent."
///
/// # Examples
///
/// ```
/// use std::collections::HashSet;
/// use pickaxe_rs::formula;
/// use pickaxe_rs::prelude::*;
/// use pickaxe_rs::system::consistency::is_indirectly_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!(!p),
/// }];
/// assert!(!is_indirectly_consistent(&s, &rules, &cf));
/// ```
pub fn is_indirectly_consistent(
    formulas: &HashSet<Formula>,
    strict_rules: &[StrictRule],
    contrariness: &ContrarinessFunction,
) -> bool {
    let closure = strict_closure(formulas, strict_rules);
    is_directly_consistent(&closure, contrariness)
}

/// Check closure under contraposition (Definition 4.3): for all S ⊆ L,
/// s ∈ S, and φ, if S ⊢ φ (φ properly derived via strict rules, i.e.,
/// φ ∈ Cl(S) \ S) then S\{s} ∪ {¬φ} ⊢ ¬s.
///
/// Only formulae properly derived by at least one strict rule application
/// are checked, consistent with the proof that closure under transposition
/// implies closure under contraposition (Modgil & Prakken 2013, Prop. 3.18).
///
/// This is exponential in the size of `language` (O(2^|L| × |L|² × |Rs|)),
/// so it is practical only for small languages (|L| ≤ ~15).
///
/// # References
///
/// Definition 4.3 in Modgil & Prakken (2014): "AT is closed under
/// contraposition iff for all S ⊆ L, s ∈ S and φ, if S ⊢ φ, then
/// S\{s} ∪ {¬φ} ⊢ ¬s."
///
/// # Errors
///
/// Returns [`AspicError`] if the language exceeds the powerset limit
/// (currently 64 formulae).
pub fn check_contraposition_closure(
    language: &HashSet<Formula>,
    strict_rules: &[StrictRule],
    _contrariness: &ContrarinessFunction,
) -> Result<bool, AspicError> {
    let lang_vec: Vec<&Formula> = language.iter().collect();
    let n = lang_vec.len();

    if n >= POWERSET_LIMIT {
        return Err(SolverError::PowersetLimitExceeded {
            count: n,
            limit: POWERSET_LIMIT,
        }
        .into());
    }

    for mask in 1u64..(1u64 << n) {
        let s: HashSet<Formula> = (0..n)
            .filter(|i| mask & (1u64 << i) != 0)
            .map(|i| lang_vec[i].clone())
            .collect();

        let closure = strict_closure(&s, strict_rules);

        for phi in closure.difference(&s) {
            for s_elem in &s {
                let neg_phi = phi.classical_negation();
                let neg_s = s_elem.classical_negation();

                let mut contraposed: HashSet<Formula> = s.clone();
                contraposed.remove(s_elem);
                contraposed.insert(neg_phi);

                let contraposed_closure = strict_closure(&contraposed, strict_rules);

                if !contraposed_closure.contains(&neg_s) {
                    return Ok(false);
                }
            }
        }
    }
    Ok(true)
}
