/// Module `solver` provides the top-level API as a SAT solver.
/// API to instantiate
mod build;
/// Module 'conflict' handles conflicts.
mod conflict;
/// Module `restart` provides restart heuristics.
pub mod restart;
/// CDCL search engine
mod search;
/// Stage manger (was Stabilizer)
mod stage;
/// Module `validate` implements a model checker.
mod validate;

pub use self::{
    build::SatSolverIF,
    restart::{RestartIF, RestartManager},
    search::SolveIF,
    stage::StageManager,
    validate::ValidateIF,
};

use crate::{assign::AssignStack, cdb::ClauseDB, state::*, types::*};

/// Normal results returned by Solver.
#[derive(Debug, Eq, PartialEq)]
pub enum Certificate {
    /// It is satisfiable; `vec` is such an assignment sorted by var order.
    SAT(Vec<i32>),
    /// It is unsatisfiable.
    UNSAT,
}

/// The return type of `Solver::solve`.
/// This captures the following three cases:
/// * `Certificate::SAT` -- solved with a satisfiable assignment set,
/// * `Certificate::UNSAT` -- proved that it's an unsatisfiable problem, and
/// * `SolverError::*` -- caused by a bug
pub type SolverResult = Result<Certificate, SolverError>;

/// define sub-modules' responsibilities
#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub enum SolverEvent {
    /// asserting a var.
    Assert(VarId),
    /// conflict by unit propagation.
    Conflict,
    /// eliminating a var.
    Eliminate(VarId),
    /// Not in use
    Instantiate,
    /// increment the number of vars.
    NewVar,
    /// re-initialization for incremental solving.
    Reinitialize,
    /// restart
    Restart,
    /// start a new stage of Luby stabilization. It holds new scale.
    Stage(usize),

    #[cfg(feature = "clause_vivification")]
    /// Vivification: `true` for start, `false` for end.
    Vivify(bool),
}

/// The SAT solver object consisting of 6 sub modules.
/// ```
/// use crate::splr::*;
/// use crate::splr::{assign::{AssignIF, VarManipulateIF}, state::{State, StateIF}, types::*};
/// use std::path::Path;
///
/// let mut s = Solver::try_from(Path::new("cnfs/sample.cnf")).expect("can't load");
/// assert_eq!(s.asg.derefer(assign::property::Tusize::NumVar), 250);
/// assert_eq!(s.asg.derefer(assign::property::Tusize::NumUnassertedVar), 250);
/// if let Ok(Certificate::SAT(v)) = s.solve() {
///     assert_eq!(v.len(), 250);
///     // But don't expect `s.asg.var_stats().3 == 0` at this point.
///     // It returns the number of vars which were assigned at decision level 0.
/// } else {
///     panic!("It should be satisfied!");
/// }
/// assert_eq!(Solver::try_from(Path::new("cnfs/unsat.cnf")).expect("can't load").solve(), Ok(Certificate::UNSAT));
/// ```
#[derive(Clone, Debug, Default)]
pub struct Solver {
    /// assignment management
    pub asg: AssignStack,
    /// clause container
    pub cdb: ClauseDB,
    /// misc data holder
    pub state: State,
}

/// Example
///```
/// use crate::splr::*;
///
/// let v: Vec<Vec<i32>> = vec![];
/// assert!(matches!(
///     Certificate::try_from(v),
///     Ok(Certificate::SAT(_))
/// ));
/// assert!(matches!(
///     Certificate::try_from(vec![vec![0_i32]]),
///     Err(SolverError::InvalidLiteral)
/// ));
///
/// // `Solver` has another interface.
/// assert!(matches!(
///     Solver::try_from((Config::default(), vec![vec![0_i32]].as_ref())),
///     Err(Err(SolverError::InvalidLiteral))
/// ));
///```
impl<V: AsRef<[i32]>> TryFrom<Vec<V>> for Certificate {
    type Error = SolverError;
    fn try_from(vec: Vec<V>) -> SolverResult {
        Solver::try_from((Config::default(), vec.as_ref())).map_or_else(
            |e: SolverResult| match e {
                Ok(cert) => Ok(cert),
                Err(SolverError::EmptyClause) => Ok(Certificate::UNSAT),
                Err(e) => Err(e),
            },
            |mut solver| solver.solve(),
        )
    }
}

/// Iterator for Solver
/// * takes `&mut Solver`
/// * returns `Option<Vec<i32>>`
///    * `Some(Vec<i32>)` -- satisfiable assignment
///    * `None` -- unsatisfiable anymore
/// * Some internal error causes panic.
#[cfg(feature = "incremental_solver")]
pub struct SolverIter<'a> {
    solver: &'a mut Solver,
    refute: Option<Vec<i32>>,
}

#[cfg(feature = "incremental_solver")]
impl Solver {
    /// return an iterator on Solver. **Requires 'incremental_solver' feature**
    ///```ignore
    ///use splr::Solver;
    ///use std::path::Path;
    ///
    ///for v in Solver::try_from(Path::new("cnfs/sample.cnf")).expect("panic").iter() {
    ///    println!(" - answer: {:?}", v);
    ///}
    ///```
    pub fn iter(&mut self) -> SolverIter {
        SolverIter {
            solver: self,
            refute: None,
        }
    }
}

#[cfg(feature = "incremental_solver")]
impl<'a> Iterator for SolverIter<'a> {
    type Item = Vec<i32>;
    fn next(&mut self) -> Option<Self::Item> {
        if let Some(ref v) = self.refute {
            debug_assert!(1 < v.len());
            match self.solver.add_clause(v) {
                Err(SolverError::Inconsistent) => return None,
                Err(SolverError::EmptyClause) => return None,
                Err(e) => panic!("s UNKNOWN: {:?} by adding {:?}", e, v),
                Ok(_) => self.solver.reset(),
            }
            self.refute = None;
        }
        match self.solver.solve() {
            Ok(Certificate::SAT(ans)) => {
                let rft: Vec<i32> = ans.iter().map(|i| -i).collect::<Vec<i32>>();
                self.refute = Some(rft);
                Some(ans)
            }
            Ok(Certificate::UNSAT) => None,
            e => panic!("s UNKNOWN: {:?}", e),
        }
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::assign;

    #[cfg_attr(not(feature = "no_IO"), test)]
    fn test_solver() {
        let config = Config::from("cnfs/sample.cnf");
        if let Ok(s) = Solver::build(&config) {
            assert_eq!(s.asg.derefer(assign::property::Tusize::NumVar), 250);
            assert_eq!(
                s.asg.derefer(assign::property::Tusize::NumUnassertedVar),
                250
            );
        } else {
            panic!("failed to build a solver for cnfs/sample.cnf");
        }
    }

    macro_rules! run {
        ($vec: expr) => {
            println!(
                "{:>46} =| {:?}",
                format!("{:?}", $vec),
                match Solver::try_from((Config::default(), $vec.as_ref())).map(|mut s| s.solve()) {
                    Err(e) => e,
                    Ok(Ok(u @ Certificate::UNSAT)) => Ok(u),
                    Ok(s) => s,
                }
            );
        };
    }

    macro_rules! sat {
        ($vec: expr, $should_be: pat) => {
            println!("{:>46} =| ", format!("{:?}", $vec));
            let result = Certificate::try_from($vec);
            println!("{:?}", result);
            assert!(matches!(result, $should_be));
        };
        ($vec: expr) => {
            println!(
                "{:>46} =| {:?}",
                format!("{:?}", $vec),
                Certificate::try_from($vec)
            );
        };
    }

    #[test]
    fn test_on_memory_solving() {
        let mut v: Vec<Vec<i32>> = Vec::new();
        run!(v);
        v.push(Vec::new());
        run!(v);
        run!(vec![vec![1]]);
        run!(vec![vec![1], vec![-1]]);
        run!(vec![vec![1, 2], vec![-1, 3], vec![1, -3], vec![-1, 2]]);
        run!(vec![
            vec![1, 2],
            vec![-1, 3],
            vec![1, -3],
            vec![-1, -2],
            vec![-2, -3]
        ]);
        run!(vec![
            vec![1, 2],
            vec![-1, 3],
            vec![-1, -3],
            vec![-1, -2],
            vec![1, -2]
        ]);

        // auto conversion via `as_ref`
        let (v1, v2, v3, v4, v5) = (vec![1, 2], vec![-1, 3], vec![1, -3], vec![-1, 2], vec![-3]);
        run!(vec![&v1, &v2, &v3, &v4, &v5]); // : Vec<&[i32]>
        run!([&v1, &v2, &v3, &v4, &v5]); // [&[i32]; 5]

        // let v: Vec<Vec<i32>> = vec![vec![1, 2], vec![-1, 3], vec![1, -3], vec![-1, 2]];
        // let s = Solver::try_from((Config::default(), v.as_ref()));
        // match s.map_or_else(|e| e, |mut solver| solver.solve()) {
        //     Ok(Certificate::SAT(ans)) => println!("s SATISFIABLE: {:?}", ans),
        //     Ok(Certificate::UNSAT) => println!("s UNSATISFIABLE"),
        //     Err(e) => panic!("{}", e),
        // }
        let v0: Vec<Vec<i32>> = vec![];
        sat!(v0, Ok(Certificate::SAT(_)));
        let v1: Vec<Vec<i32>> = vec![vec![]];
        sat!(v1, Ok(Certificate::UNSAT));
        sat!(vec![vec![1i32]], Ok(Certificate::SAT(_)));
        sat!(vec![vec![1i32], vec![-1]], Ok(Certificate::UNSAT));
        sat!(vec![vec![1i32, 2], vec![-1, 3], vec![1, -3], vec![-1, 2]]);
        sat!(vec![
            vec![1i32, 2],
            vec![-1, 3],
            vec![1, -3],
            vec![-1, -2],
            vec![-2, -3]
        ]);
        sat!(vec![
            vec![1i32, 2],
            vec![-1, 3],
            vec![-1, -3],
            vec![-1, -2],
            vec![1, -2]
        ]);
        let (v1, v2, v3, v4, v5) = (
            vec![1i32, 2],
            vec![-1i32, 3],
            vec![1i32, -3],
            vec![-1i32, 2],
            vec![-3i32],
        );
        sat!(vec![&v1, &v2, &v3, &v4, &v5]); // : Vec<&[i32]>
    }

    #[cfg(feature = "incremental_solver")]
    #[test]
    fn test_solver_iter() {
        let mut slv = Solver::instantiate(
            &Config::default(),
            &CNFDescription {
                num_of_variables: 8,
                ..CNFDescription::default()
            },
        );
        assert_eq!(slv.iter().count(), 256);
    }
    #[cfg(feature = "incremental_solver")]
    #[test]
    fn test_add_var_on_incremental_solver() {
        let mut slv = Solver::instantiate(
            &Config::default(),
            &CNFDescription {
                num_of_variables: 4,
                ..CNFDescription::default()
            },
        );
        assert!(slv.add_clause(vec![-1, -2]).is_ok());
        assert!(slv.add_clause(vec![-3, -4]).is_ok());
        assert!(slv.add_assignment(-2).is_ok());
        let a = slv.add_var() as i32;
        assert!(slv.add_clause(vec![1, 3, 4, -a]).is_ok());
        assert!(slv.add_clause(vec![1, -3, -4, -a]).is_ok());
        assert!(slv.add_clause(vec![-1, 3, -4, -a]).is_ok());
        assert!(slv.add_clause(vec![-1, -3, 4, -a]).is_ok());
        assert!(slv.add_clause(vec![-1, -3, -4, a]).is_ok());
        assert!(slv.add_clause(vec![-1, 3, 4, a]).is_ok());
        assert!(slv.add_clause(vec![1, -3, 4, a]).is_ok());
        assert!(slv.add_clause(vec![1, 3, -4, a]).is_ok());
        let b = slv.add_var() as i32;
        assert!(slv.add_clause(vec![1, 3, -b]).is_ok());
        assert!(slv.add_clause(vec![1, 4, -b]).is_ok());
        assert!(slv.add_clause(vec![3, 4, -b]).is_ok());
        assert!(slv.add_clause(vec![-1, -3, b]).is_ok());
        assert!(slv.add_clause(vec![-1, -4, b]).is_ok());
        assert!(slv.add_clause(vec![-3, -4, b]).is_ok());
        assert!(slv.add_clause(vec![-1, -b]).is_ok());
        assert!(slv.add_clause(vec![-a, -b]).is_ok());
        // let solns: Vec<Vec<i32>> = slv.iter().collect();
        // Use the result of
        // cargo run --features incremental_solver --example all-solutions -- cnfs/isseu-182.cnf
        assert_eq!(slv.iter().count(), 4);
    }
    #[cfg(feature = "incremental_solver")]
    #[test]
    // There was an inconsistency in AssignStack::var_order.
    fn test_add_var_and_add_assignment() {
        let mut slv = Solver::instantiate(
            &Config::default(),
            &CNFDescription {
                num_of_variables: 3 as usize,
                ..CNFDescription::default()
            },
        );

        slv.add_var();
        assert!(slv.add_clause(vec![-1, 4]).is_ok());
        slv.add_var();
        assert!(slv.add_clause(vec![-2, 5]).is_ok());
        slv.add_var();
        assert!(slv.add_clause(vec![-1, -2, 6]).is_ok());
        slv.add_var();
        assert!(slv.add_clause(vec![-5, 7]).is_ok());
        slv.add_var();
        assert!(slv.add_clause(vec![-6, 8]).is_ok());
        slv.add_var();
        assert!(slv.add_clause(vec![-4, 9]).is_ok());
        slv.add_var();
        assert!(slv.add_clause(vec![-3, 10]).is_ok());
        slv.add_var();
        assert!(slv.add_clause(vec![-5, -3, 11]).is_ok());
        assert!(slv.add_clause(vec![-6, -3, 11]).is_ok());
        slv.add_var();
        assert!(slv.add_clause(vec![-4, -3, 12]).is_ok());
        assert!(slv.add_assignment(-11).is_ok());
        assert!(slv.solve().is_ok());
    }
}