use std::collections::BTreeSet;

use dimacs::Clause;
use itertools::Itertools;
use log::info;

use crate::propositional::frontier;

const PREPROCESS_SUBSUMPTION_MAXLEN: usize = 2_000;

pub fn preprocess(clauses: &[Clause]) -> Vec<Clause> {
    let nontrivial_clauses = clauses
        .iter()
        .filter(|clause| {
            let mut visited_vars = BTreeSet::<u64>::default();
            for lit in clause.lits() {
                let var = lit.var().0;
                if visited_vars.contains(&var) {
                    return false;
                }
                visited_vars.insert(var);
            }
            true
        })
        .cloned()
        .collect_vec();
    if nontrivial_clauses.len() < clauses.len() {
        info!(
            "Eliminated {} trivial clauses from the input, proceeding with {} clauses",
            clauses.len() - nontrivial_clauses.len(),
            nontrivial_clauses.len()
        );
    }
    if nontrivial_clauses.len() < PREPROCESS_SUBSUMPTION_MAXLEN {
        let frontier_clauses = frontier(nontrivial_clauses.as_slice());
        if frontier_clauses.len() < nontrivial_clauses.len() {
            info!(
            "Eliminated {} non-frontier clauses from the input, proceeding with {} frontier clauses",
            nontrivial_clauses.len() - frontier_clauses.len(),
            frontier_clauses.len()
        );
        }
        frontier_clauses
    } else {
        nontrivial_clauses
    }
}
