use std::{ops::Deref, hash::Hasher};

use dimacs::{Clause, Lit, Var};

/// Clause wrapper with lex-order implementation
#[derive(Debug, Eq, PartialEq, Clone)]
pub(crate) struct ClauseKey(pub(crate) Clause);

impl Deref for ClauseKey {
    type Target = Clause;

    fn deref(&self) -> &Self::Target {
        &self.0
    }
}

impl PartialOrd for ClauseKey {
    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
        Some(self.cmp(other))
    }
}

impl Ord for ClauseKey {
    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
        let lhs_key = self.lits().iter().map(to_i64);
        let rhs_key = other.lits().iter().map(to_i64);
        lhs_key.cmp(rhs_key)
    }
}

impl std::hash::Hash for ClauseKey {
    fn hash<H: Hasher>(&self, state: &mut H) {
        self.0.lits().hash(state);
    }
}

/// Negate an input literal
pub fn negate(lit: &Lit) -> Lit {
    Lit::from_i64(-to_i64(lit))
}

/// Return a positive literal of an input variable
pub fn var_to_pos(var: &Var) -> Lit {
    Lit::from_i64(var.to_u64() as i64)
}

/// Return a negative literal of an input variable
pub fn var_to_neg(var: &Var) -> Lit {
    Lit::from_i64(-(var.to_u64() as i64))
}

/// Convert a literal to an integer; an inverse of `Lit::from_i64`
pub fn to_i64(lit: &Lit) -> i64 {
    lit.var().to_u64() as i64
        * match lit.sign() {
            dimacs::Sign::Pos => 1,
            dimacs::Sign::Neg => -1,
        }
}

pub fn resolve(lhs: &Clause, rhs: &Clause) -> Option<Clause> {
    // Find a literal to resolve upon
    let resolve_lit = lhs
        .lits()
        .iter()
        .filter(|lit| {
            rhs.lits()
                .iter()
                .any(|rhs_lit| rhs_lit.var() == lit.var() && rhs_lit.sign() != lit.sign())
        })
        .collect::<Vec<_>>();
    if let [resolve_lit] = resolve_lit[..] {
        // Merge the literals (except for the resolving one) and return
        let mut lits = lhs
            .lits()
            .iter()
            .filter(|lit| lit.var() != resolve_lit.var())
            .chain(
                rhs.lits()
                    .iter()
                    .filter(|lit| lit.var() != resolve_lit.var()),
            )
            .cloned()
            .collect::<Vec<_>>();
        lits.sort_by_key(|lit| lit.var().to_u64());
        lits.dedup();
        Some(Clause::from_vec(lits))
    } else {
        // If non-unique, return None
        None
    }
}

/// Computes a subset of clauses such that there is an optimal proof using only those clauses
pub(crate) fn frontier(clauses: &[Clause]) -> Vec<Clause> {
    // Remove dominated clauses
    let mut new_clauses = clauses.to_vec();
    new_clauses.retain(|clause| {
        clauses.iter().all(|sub_clause| {
            // Any clause in the formula must either be as long as `clause`
            // or have a literal not contained in `clause`
            sub_clause.len() >= clause.len()
                || sub_clause
                    .lits()
                    .iter()
                    .any(|sub_lit| !clause.lits().contains(sub_lit))
        })
    });
    // Sort the remaining clauses to ensure order independence
    new_clauses.sort_by_cached_key(|clause| clause.lits().iter().map(to_i64).collect::<Vec<_>>());
    new_clauses.dedup();
    new_clauses
}

#[cfg(test)]
mod resolution_tests {
    use super::*;
    use dimacs::Lit;

    #[test]
    fn resolve_single_lit_no_overlap() {
        let lhs = Clause::from_vec(vec![Lit::from_i64(1), Lit::from_i64(-2)]);
        let rhs = Clause::from_vec(vec![Lit::from_i64(2), Lit::from_i64(3)]);
        if let Some(resolved) = resolve(&lhs, &rhs) {
            assert_eq!(resolved.lits(), vec![Lit::from_i64(1), Lit::from_i64(3)]);
        } else {
            panic!();
        }
    }

    #[test]
    fn resolve_single_lit_overlap() {
        let lhs = Clause::from_vec(vec![Lit::from_i64(1), Lit::from_i64(-2)]);
        let rhs = Clause::from_vec(vec![Lit::from_i64(1), Lit::from_i64(2)]);
        if let Some(resolved) = resolve(&lhs, &rhs) {
            assert_eq!(resolved.lits(), vec![Lit::from_i64(1)]);
        } else {
            panic!();
        }
    }

    #[test]
    fn resolve_multiple_lits() {
        let lhs = Clause::from_vec(vec![Lit::from_i64(1), Lit::from_i64(-2), Lit::from_i64(3)]);
        let rhs = Clause::from_vec(vec![Lit::from_i64(1), Lit::from_i64(2), Lit::from_i64(-3)]);
        assert!(resolve(&lhs, &rhs).is_none())
    }

    #[test]
    fn resolve_no_lits() {
        let lhs = Clause::from_vec(vec![Lit::from_i64(1), Lit::from_i64(2), Lit::from_i64(3)]);
        let rhs = Clause::from_vec(vec![Lit::from_i64(1), Lit::from_i64(2), Lit::from_i64(3)]);
        assert!(resolve(&lhs, &rhs).is_none())
    }
}
