use itertools::Itertools;
use log::trace;

use crate::propositional::to_i64;

use super::MusEngine;

#[derive(Default, Clone)]
pub struct TrivialBounder {
    pub use_cover_bound: bool,
}

impl MusEngine for TrivialBounder {
    fn optimize_with_deadline(
        &mut self,
        formula: &[dimacs::Clause],
        mandatory: &[dimacs::Clause],
        _deadline: Option<std::time::Instant>,
    ) -> super::MusStatus {
        let mut lower_bound = mandatory.len();
        if self.use_cover_bound {
            let mut mandatory_lens = mandatory.iter().map(|x| x.len()).collect_vec();
            mandatory_lens.sort();
            let mut partial_sum = 0.0;
            for len in mandatory_lens {
                partial_sum += (-(len as f64)).exp2();
                if partial_sum >= 1.0 {
                    break;
                }
            }
            if partial_sum < 1.0 {
                let mut clause_lens = formula
                    .iter()
                    .filter(|x| !mandatory.contains(x))
                    .map(|x| x.len())
                    .collect_vec();
                clause_lens.sort();
                for len in clause_lens {
                    partial_sum += (-(len as f64)).exp2();
                    lower_bound += 1;
                    if partial_sum >= 1.0 {
                        break;
                    }
                }
            }
        }
        super::MusStatus {
            smallest_subset: vec![],
            lower_bound,
        }
    }
}
