pub mod bnb;
pub mod forqes;
pub mod ifelse;
pub mod trivial;

use std::{io::Write, time::Instant};

use dimacs::Clause;

use crate::{mus::trivial::TrivialBounder, propositional::to_i64};

pub trait MusEngine {
    /// Report the lower and upper bounds on the smallest MUS cardinality
    /// before the deadline, if any provided, or until the computational
    /// budget defined by the implementation is exhausted
    fn optimize_with_deadline(
        &mut self,
        formula: &[Clause],
        mandatory: &[Clause],
        deadline: Option<Instant>,
    ) -> MusStatus;

    /// A convenience method that leaves the termination decision to the implementation
    fn optimize(&mut self, formula: &[Clause], mandatory: &[Clause]) -> MusStatus {
        self.optimize_with_deadline(formula, mandatory, None)
    }

    /// Report the internal statistics of the solver
    fn report(&self) {}
}

#[derive(Debug, Clone)]
pub struct MusStatus {
    /// The smallest discovered UNSAT subset of clauses.
    pub smallest_subset: Vec<Clause>,
    /// Lowest cardinality that a MUS could still have.
    ///
    /// Equivalent claim: any subset of size less than `lower_bound` is SAT.
    pub lower_bound: usize,
}

impl MusStatus {
    pub fn upper_bound(&self) -> usize {
        self.smallest_subset.len()
    }

    pub fn is_optimal(&self) -> bool {
        self.lower_bound == self.upper_bound()
    }

    pub fn write_dimacs(&self, mut writer: impl Write) -> std::io::Result<()> {
        writeln!(writer, "c >= {}", self.lower_bound)?;
        let n_variables = self
            .smallest_subset
            .iter()
            .flat_map(|clause| clause.lits().iter().map(|lit| lit.var().0))
            .max()
            .unwrap_or(0);
        let n_clauses = self.smallest_subset.len();
        writeln!(writer, "p cnf {n_variables} {n_clauses}")?;
        for clause in &self.smallest_subset {
            for lit in clause.lits() {
                write!(writer, "{} ", to_i64(lit))?;
            }
            writeln!(writer, "0")?;
        }
        Ok(())
    }
}
