//! # rustsat-cadical - Interface to the CaDiCaL SAT Solver for RustSAT
//!
//! Armin Biere's SAT solver [CaDiCaL](https://github.com/arminbiere/cadical) to be used with the [RustSAT](https://github.com/chrjabs/rustsat) library.
//!
//! **Note**: at the moment this crate is known to not work on Windows since CaDiCaL is non-trivial to get to work on Windows.
//!
//! ## Features
//!
//! - `debug`: if this feature is enables, the C++ library will be built with debug and check functionality if the Rust project is built in debug mode
//! - `safe`: disable writing through 'popen' for more safe usage of the library in applications
//! - `quiet`: exclude message and profiling code (logging too)
//! - `logging`: include logging code (but disabled by default)
//!
//! ## CaDiCaL Versions
//!
//! CaDiCaL versions can be selected via cargo crate features.
//! All CaDiCaL versions up to [Version 1.9.4](https://github.com/arminbiere/cadical/releases/tag/rel-1.9.4) are available.
//! For the full list of versions and the changelog see [the CaDiCaL releases](https://github.com/arminbiere/cadical/releases).
//!
//! Without any features selected, the newest version will be used.
//! If conflicting CaDiCaL versions are requested, the newest requested version will be selected.

#![warn(missing_docs)]

use core::ffi::{c_int, c_void, CStr};
use std::{cmp::Ordering, ffi::CString, fmt};

use cpu_time::ProcessTime;
use ffi::CaDiCaLHandle;
use rustsat::solvers::{
    ControlSignal, FreezeVar, GetInternalStats, Interrupt, InterruptSolver, Learn, LimitConflicts,
    LimitDecisions, PhaseLit, Solve, SolveIncremental, SolveStats, SolverResult, SolverState,
    SolverStats, StateError, Terminate,
};
use rustsat::types::{Clause, Lit, TernaryVal, Var};
use thiserror::Error;

const OUT_OF_MEM: c_int = 50;

macro_rules! handle_oom {
    ($val:expr) => {{
        let val = $val;
        if val == crate::OUT_OF_MEM {
            return anyhow::Context::context(
                Err(rustsat::OutOfMemory::ExternalApi),
                "cadical out of memory",
            );
        }
        val
    }};
    ($val:expr, noanyhow) => {{
        let val = $val;
        if val == crate::OUT_OF_MEM {
            return Err(rustsat::OutOfMemory::ExternalApi);
        }
        val
    }};
}
pub(crate) use handle_oom;

/// Fatal error returned if the CaDiCaL API returns an invalid value
#[derive(Error, Clone, Copy, PartialEq, Eq, Debug)]
#[error("cadical c-api returned an invalid value: {api_call} -> {value}")]
pub struct InvalidApiReturn {
    api_call: &'static str,
    value: c_int,
}

#[derive(Debug, PartialEq, Eq, Default)]
enum InternalSolverState {
    #[default]
    Configuring,
    Input,
    Sat,
    Unsat(Vec<Lit>),
}

impl InternalSolverState {
    fn to_external(&self) -> SolverState {
        match self {
            InternalSolverState::Configuring => SolverState::Configuring,
            InternalSolverState::Input => SolverState::Input,
            InternalSolverState::Sat => SolverState::Sat,
            InternalSolverState::Unsat(_) => SolverState::Unsat,
        }
    }
}

type TermCallbackPtr<'a> = Box<dyn FnMut() -> ControlSignal + 'a>;
type LearnCallbackPtr<'a> = Box<dyn FnMut(Clause) + 'a>;
type LratCallbackPtr<'a> = Box<dyn FnMut(u64, Clause, &[u64]) + 'a>;
/// Double boxing is necessary to get thin pointers for casting
type OptTermCallbackStore<'a> = Option<Box<TermCallbackPtr<'a>>>;
/// Double boxing is necessary to get thin pointers for casting
type OptLearnCallbackStore<'a> = Option<Box<LearnCallbackPtr<'a>>>;
type LratCallbackStore<'a> = Option<Box<LratCallbackPtr<'a>>>;

/// The CaDiCaL solver type
pub struct CaDiCaL<'term, 'learn, 'lrat> {
    handle: *mut CaDiCaLHandle,
    state: InternalSolverState,
    terminate_cb: OptTermCallbackStore<'term>,
    learner_cb: OptLearnCallbackStore<'learn>,
    lrat_cb: LratCallbackStore<'lrat>,
    stats: SolverStats,
}

unsafe impl Send for CaDiCaL<'_, '_, '_> {}

impl Default for CaDiCaL<'_, '_, '_> {
    fn default() -> Self {
        let handle = unsafe { ffi::ccadical_init() };
        if handle.is_null() {
            panic!("not enough memory to initialize CaDiCaL solver")
        }
        let solver = Self {
            handle: unsafe { ffi::ccadical_init() },
            state: Default::default(),
            terminate_cb: Default::default(),
            learner_cb: Default::default(),
            lrat_cb: Default::default(),
            stats: Default::default(),
        };
        let quiet = CString::new("quiet").unwrap();
        unsafe { ffi::ccadical_set_option_ret(solver.handle, quiet.as_ptr(), 1) };
        solver
    }
}

impl CaDiCaL<'_, '_, '_> {
    fn get_core_assumps(&self, assumps: &[Lit]) -> Result<Vec<Lit>, InvalidApiReturn> {
        let mut core = Vec::new();
        for a in assumps {
            match unsafe { ffi::ccadical_failed(self.handle, a.to_ipasir()) } {
                0 => (),
                1 => core.push(!*a),
                value => {
                    return Err(InvalidApiReturn {
                        api_call: "ccadical_failed",
                        value,
                    })
                }
            }
        }
        Ok(core)
    }

    /// Adds a clause that only exists for the next solver call. Only one such
    /// clause can exist, a new new clause replaces the old one.
    ///
    /// _Note_: If this is used, in addition to [`SolveIncremental::core`],
    /// [`CaDiCaL::tmp_clause_in_core`] needs to be checked to determine if the
    /// temporary clause is part of the core.
    pub fn add_tmp_clause(&mut self, clause: Clause) -> Result<(), rustsat::OutOfMemory> {
        // Update wrapper-internal state
        self.stats.n_clauses += 1;
        self.stats.avg_clause_len =
            (self.stats.avg_clause_len * ((self.stats.n_clauses - 1) as f32) + clause.len() as f32)
                / self.stats.n_clauses as f32;
        self.state = InternalSolverState::Input;
        // Call CaDiCaL backend
        for lit in &clause {
            handle_oom!(
                unsafe { ffi::ccadical_constrain_mem(self.handle, lit.to_ipasir()) },
                noanyhow
            );
        }
        handle_oom!(
            unsafe { ffi::ccadical_constrain_mem(self.handle, 0) },
            noanyhow
        );
        Ok(())
    }

    /// Checks whether the temporary clause is part of the core if in
    /// unsatisfiable state. This needs to always be checked in addition to
    /// [`SolveIncremental::core`] if a [`CaDiCaL::add_tmp_clause`] is used.
    pub fn tmp_clause_in_core(&mut self) -> anyhow::Result<bool> {
        match &self.state {
            InternalSolverState::Unsat(_) => unsafe {
                Ok(ffi::ccadical_constraint_failed(self.handle) != 0)
            },
            state => Err(StateError {
                required_state: SolverState::Unsat,
                actual_state: state.to_external(),
            }
            .into()),
        }
    }

    /// Sets a pre-defined configuration for CaDiCaL's internal options
    pub fn set_configuration(&mut self, config: Config) -> anyhow::Result<()> {
        if self.state == InternalSolverState::Configuring {
            let config_name = match config {
                Config::Default => CString::new("default").unwrap(),
                Config::Plain => CString::new("plain").unwrap(),
                Config::SAT => CString::new("sat").unwrap(),
                Config::UNSAT => CString::new("unsat").unwrap(),
            };
            let ret = unsafe { ffi::ccadical_configure(self.handle, config_name.as_ptr()) };
            if ret {
                Ok(())
            } else {
                Err(InvalidApiReturn {
                    api_call: "ccadical_configure",
                    value: 0,
                }
                .into())
            }
        } else {
            Err(StateError {
                required_state: SolverState::Configuring,
                actual_state: self.state.to_external(),
            }
            .into())
        }
    }

    /// Sets the value of a CaDiCaL option. For possible options, check CaDiCaL with `cadical --help`.
    /// Requires state [`SolverState::Configuring`].
    ///
    /// # CaDiCaL Documentation
    ///
    /// Explicit version of setting an option.  If the option `<name>` exists
    /// and `<val>` can be parsed then 'true' is returned.  If the option value
    /// is out of range the actual value is computed as the closest (minimum or
    /// maximum) value possible, but still `true` is returned.
    pub fn set_option(&mut self, name: &str, value: c_int) -> anyhow::Result<()> {
        let c_name = CString::new(name)?;
        if unsafe { ffi::ccadical_set_option_ret(self.handle, c_name.as_ptr(), value) } {
            Ok(())
        } else {
            Err(InvalidApiReturn {
                api_call: "ccadical_set_option_ret",
                value: 0,
            }
            .into())
        }
    }

    /// Gets the value of a CaDiCaL option. For possible options, check CaDiCaL with `cadical --help`.
    ///
    /// # CaDiCaL Documentation
    ///
    /// Get the current value of the option `name`.  If `name` is invalid then
    /// zero is returned.
    pub fn get_option(&self, name: &str) -> anyhow::Result<c_int> {
        let c_name = CString::new(name)?;
        Ok(unsafe { ffi::ccadical_get_option(self.handle, c_name.as_ptr()) })
    }

    /// Sets an internal limit for CaDiCaL
    ///
    /// # CaDiCaL Documentation
    ///
    /// Specify search limits, where currently `name` can be "conflicts",
    /// "decisions", "preprocessing", or "localsearch".  The first two limits
    /// are unbounded by default.  Thus using a negative limit for conflicts or
    /// decisions switches back to the default of unlimited search (for that
    /// particular limit).  The preprocessing limit determines the number of
    /// preprocessing rounds, which is zero by default.  Similarly, the local
    /// search limit determines the number of local search rounds (also zero by
    /// default).  As with `set`, the return value denotes whether the limit
    /// `name` is valid.  These limits are only valid for the next `solve` or
    /// `simplify` call and reset to their default after `solve` returns (as
    /// well as overwritten and reset during calls to `simplify` and
    /// `lookahead`).  We actually also have an internal "terminate" limit
    /// which however should only be used for testing and debugging.
    pub fn set_limit(&mut self, limit: Limit) -> anyhow::Result<()> {
        let (name, val) = match limit {
            Limit::Terminate(val) => (CString::new("terminate").unwrap(), val),
            Limit::Conflicts(val) => (CString::new("conflicts").unwrap(), val),
            Limit::Decisions(val) => (CString::new("decisions").unwrap(), val),
            Limit::Preprocessing(val) => (CString::new("preprocessing").unwrap(), val),
            Limit::LocalSearch(val) => (CString::new("localsearch").unwrap(), val),
        };
        if unsafe { ffi::ccadical_limit_ret(self.handle, name.as_ptr(), val) } {
            Ok(())
        } else {
            Err(InvalidApiReturn {
                api_call: "ccadical_limit_ret",
                value: 0,
            }
            .into())
        }
    }

    /// Gets the number of active variables
    pub fn get_active(&self) -> i64 {
        unsafe { ffi::ccadical_active(self.handle) }
    }

    /// Gets the number of active irredundant clauses
    pub fn get_irredundant(&self) -> i64 {
        unsafe { ffi::ccadical_irredundant(self.handle) }
    }

    /// Gets the number of active redundant clauses
    pub fn get_redundant(&self) -> i64 {
        unsafe { ffi::ccadical_redundant(self.handle) }
    }

    /// Gets the current literal value at the root level
    pub fn current_lit_val(&self, lit: Lit) -> TernaryVal {
        let int_val = unsafe { ffi::ccadical_fixed(self.handle, lit.to_ipasir()) };
        match int_val.cmp(&0) {
            Ordering::Greater => TernaryVal::True,
            Ordering::Less => TernaryVal::False,
            Ordering::Equal => TernaryVal::DontCare,
        }
    }

    /// Prints the solver statistics from the CaDiCaL backend
    pub fn print_stats(&self) {
        unsafe { ffi::ccadical_print_statistics(self.handle) }
    }

    /// Executes the given number of preprocessing rounds
    ///
    /// # CaDiCaL Documentation
    ///
    /// This function executes the given number of preprocessing rounds. It is
    /// similar to 'solve' with 'limits ("preprocessing", rounds)' except that
    /// no CDCL nor local search, nor lucky phases are executed.  The result
    /// values are also the same: 0=UNKNOWN, 10=SATISFIABLE, 20=UNSATISFIABLE.
    /// As 'solve' it resets current assumptions and limits before returning.
    /// The numbers of rounds should not be negative.  If the number of rounds
    /// is zero only clauses are restored (if necessary) and top level unit
    /// propagation is performed, which both take some time.
    pub fn simplify(&mut self, rounds: u32) -> anyhow::Result<SolverResult> {
        // If already solved, return state
        if let InternalSolverState::Sat = self.state {
            return Ok(SolverResult::Sat);
        }
        if let InternalSolverState::Unsat(_) = self.state {
            return Ok(SolverResult::Unsat);
        }
        let rounds: c_int = rounds.try_into()?;
        // Simplify with CaDiCaL backend
        match unsafe { ffi::ccadical_simplify_rounds(self.handle, rounds) } {
            0 => {
                self.state = InternalSolverState::Input;
                Ok(SolverResult::Interrupted)
            }
            10 => {
                self.state = InternalSolverState::Sat;
                Ok(SolverResult::Sat)
            }
            20 => {
                self.state = InternalSolverState::Unsat(vec![]);
                Ok(SolverResult::Unsat)
            }
            value => Err(InvalidApiReturn {
                api_call: "ccadical_simplify",
                value,
            }
            .into()),
        }
    }

    /// Executes the given number of preprocessing rounds under assumptions
    ///
    /// # CaDiCaL Documentation
    ///
    /// This function executes the given number of preprocessing rounds. It is
    /// similar to 'solve' with 'limits ("preprocessing", rounds)' except that
    /// no CDCL nor local search, nor lucky phases are executed.  The result
    /// values are also the same: 0=UNKNOWN, 10=SATISFIABLE, 20=UNSATISFIABLE.
    /// As 'solve' it resets current assumptions and limits before returning.
    /// The numbers of rounds should not be negative.  If the number of rounds
    /// is zero only clauses are restored (if necessary) and top level unit
    /// propagation is performed, which both take some time.
    pub fn simplify_assumps(
        &mut self,
        assumps: Vec<Lit>,
        rounds: u32,
    ) -> anyhow::Result<SolverResult> {
        // If already solved, return state
        if let InternalSolverState::Sat = self.state {
            return Ok(SolverResult::Sat);
        }
        if let InternalSolverState::Unsat(_) = self.state {
            return Ok(SolverResult::Unsat);
        }
        let rounds: c_int = rounds.try_into()?;
        // Simplify with CaDiCaL backend under assumptions
        for a in &assumps {
            handle_oom!(unsafe { ffi::ccadical_assume_mem(self.handle, a.to_ipasir()) });
        }
        match unsafe { ffi::ccadical_simplify_rounds(self.handle, rounds) } {
            0 => {
                self.state = InternalSolverState::Input;
                Ok(SolverResult::Interrupted)
            }
            10 => {
                self.state = InternalSolverState::Sat;
                Ok(SolverResult::Sat)
            }
            20 => {
                self.state = InternalSolverState::Unsat(vec![]);
                Ok(SolverResult::Unsat)
            }
            value => Err(InvalidApiReturn {
                api_call: "ccadical_simplify",
                value,
            }
            .into()),
        }
    }
}

impl Extend<Clause> for CaDiCaL<'_, '_, '_> {
    fn extend<T: IntoIterator<Item = Clause>>(&mut self, iter: T) {
        iter.into_iter()
            .for_each(|cl| self.add_clause(cl).expect("Error adding clause in extend"))
    }
}

impl<'a> Extend<&'a Clause> for CaDiCaL<'_, '_, '_> {
    fn extend<T: IntoIterator<Item = &'a Clause>>(&mut self, iter: T) {
        iter.into_iter().for_each(|cl| {
            self.add_clause_ref(cl)
                .expect("Error adding clause in extend")
        })
    }
}

impl Solve for CaDiCaL<'_, '_, '_> {
    fn signature(&self) -> &'static str {
        let c_chars = unsafe { ffi::ccadical_signature() };
        let c_str = unsafe { CStr::from_ptr(c_chars) };
        c_str
            .to_str()
            .expect("CaDiCaL signature returned invalid UTF-8.")
    }

    fn reserve(&mut self, max_var: Var) -> anyhow::Result<()> {
        self.state = InternalSolverState::Input;
        handle_oom!(unsafe { ffi::ccadical_reserve(self.handle, max_var.to_ipasir()) });
        Ok(())
    }

    fn solve(&mut self) -> anyhow::Result<SolverResult> {
        // If already solved, return state
        if let InternalSolverState::Sat = self.state {
            return Ok(SolverResult::Sat);
        }
        if let InternalSolverState::Unsat(core) = &self.state {
            if core.is_empty() {
                return Ok(SolverResult::Unsat);
            }
        }
        let start = ProcessTime::now();
        // Solve with CaDiCaL backend
        let res = handle_oom!(unsafe { ffi::ccadical_solve_mem(self.handle) });
        self.stats.cpu_solve_time += start.elapsed();
        match res {
            0 => {
                self.stats.n_terminated += 1;
                self.state = InternalSolverState::Input;
                Ok(SolverResult::Interrupted)
            }
            10 => {
                self.stats.n_sat += 1;
                self.state = InternalSolverState::Sat;
                Ok(SolverResult::Sat)
            }
            20 => {
                self.stats.n_unsat += 1;
                self.state = InternalSolverState::Unsat(vec![]);
                Ok(SolverResult::Unsat)
            }
            value => Err(InvalidApiReturn {
                api_call: "ccadical_solve",
                value,
            }
            .into()),
        }
    }

    fn lit_val(&self, lit: Lit) -> anyhow::Result<TernaryVal> {
        if self.state != InternalSolverState::Sat {
            return Err(StateError {
                required_state: SolverState::Sat,
                actual_state: self.state.to_external(),
            }
            .into());
        }
        let lit = lit.to_ipasir();
        match unsafe { ffi::ccadical_val(self.handle, lit) } {
            0 => Ok(TernaryVal::DontCare),
            p if p == lit => Ok(TernaryVal::True),
            n if n == -lit => Ok(TernaryVal::False),
            // CaDiCaL returns -1 if variable is higher than max var
            dc if dc == -1 => Ok(TernaryVal::DontCare),
            value => Err(InvalidApiReturn {
                api_call: "ccadical_val",
                value,
            }
            .into()),
        }
    }

    fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> {
        // Update wrapper-internal state
        self.stats.n_clauses += 1;
        self.stats.avg_clause_len =
            (self.stats.avg_clause_len * ((self.stats.n_clauses - 1) as f32) + clause.len() as f32)
                / self.stats.n_clauses as f32;
        self.state = InternalSolverState::Input;
        // Call CaDiCaL backend
        for &l in clause {
            handle_oom!(unsafe { ffi::ccadical_add_mem(self.handle, l.to_ipasir()) });
        }
        handle_oom!(unsafe { ffi::ccadical_add_mem(self.handle, 0) });
        Ok(())
    }
}

impl SolveIncremental for CaDiCaL<'_, '_, '_> {
    fn solve_assumps(&mut self, assumps: &[Lit]) -> anyhow::Result<SolverResult> {
        let start = ProcessTime::now();
        // Solve with CaDiCaL backend
        for a in assumps {
            handle_oom!(unsafe { ffi::ccadical_assume_mem(self.handle, a.to_ipasir()) });
        }
        let res = handle_oom!(unsafe { ffi::ccadical_solve_mem(self.handle) });
        self.stats.cpu_solve_time += start.elapsed();
        match res {
            0 => {
                self.stats.n_terminated += 1;
                self.state = InternalSolverState::Input;
                Ok(SolverResult::Interrupted)
            }
            10 => {
                self.stats.n_sat += 1;
                self.state = InternalSolverState::Sat;
                Ok(SolverResult::Sat)
            }
            20 => {
                self.stats.n_unsat += 1;
                self.state = InternalSolverState::Unsat(self.get_core_assumps(assumps)?);
                Ok(SolverResult::Unsat)
            }
            value => Err(InvalidApiReturn {
                api_call: "ccadical_solve",
                value,
            }
            .into()),
        }
    }

    fn core(&mut self) -> anyhow::Result<Vec<Lit>> {
        match &self.state {
            InternalSolverState::Unsat(core) => Ok(core.clone()),
            other => Err(StateError {
                required_state: SolverState::Unsat,
                actual_state: other.to_external(),
            }
            .into()),
        }
    }
}

impl<'term> Terminate<'term> for CaDiCaL<'term, '_, '_> {
    /// Sets a terminator callback that is regularly called during solving.
    ///
    /// # Examples
    ///
    /// Terminate solver after 10 callback calls.
    ///
    /// ```
    /// use rustsat::solvers::{ControlSignal, Solve, SolverResult, Terminate};
    /// use rustsat_cadical::CaDiCaL;
    ///
    /// let mut solver = CaDiCaL::default();
    ///
    /// // Load instance
    ///
    /// let mut cnt = 1;
    /// solver.attach_terminator(move || {
    ///     if cnt > 10 {
    ///         ControlSignal::Terminate
    ///     } else {
    ///         cnt += 1;
    ///         ControlSignal::Continue
    ///     }
    /// });
    ///
    /// let ret = solver.solve().unwrap();
    ///
    /// // Assuming an instance is actually loaded and runs long enough
    /// // assert_eq!(ret, SolverResult::Interrupted);
    /// ```
    fn attach_terminator<CB>(&mut self, cb: CB)
    where
        CB: FnMut() -> ControlSignal + 'term,
    {
        self.terminate_cb = Some(Box::new(Box::new(cb)));
        let cb_ptr = self.terminate_cb.as_mut().unwrap().as_mut() as *const _ as *const c_void;
        unsafe {
            ffi::ccadical_set_terminate(self.handle, cb_ptr, Some(ffi::ccadical_terminate_cb))
        }
    }

    fn detach_terminator(&mut self) {
        self.terminate_cb = None;
        unsafe { ffi::ccadical_set_terminate(self.handle, std::ptr::null(), None) }
    }
}

impl<'learn> Learn<'learn> for CaDiCaL<'_, 'learn, '_> {
    /// Sets a learner callback that gets passed clauses up to a certain length learned by the solver.
    ///
    /// The callback goes out of scope with the solver, afterwards captured variables become accessible.
    ///
    /// # Examples
    ///
    /// Count number of learned clauses up to length 10.
    ///
    /// ```
    /// use rustsat::solvers::{Solve, SolverResult, Learn};
    /// use rustsat_cadical::CaDiCaL;
    ///
    /// let mut cnt = 0;
    ///
    /// {
    ///     let mut solver = CaDiCaL::default();
    ///     // Load instance
    ///
    ///     solver.attach_learner(|_| cnt += 1, 10);
    ///
    ///     solver.solve().unwrap();
    /// }
    ///
    /// // cnt variable can be accessed from here on
    /// ```
    fn attach_learner<CB>(&mut self, cb: CB, max_len: usize)
    where
        CB: FnMut(Clause) + 'learn,
    {
        self.learner_cb = Some(Box::new(Box::new(cb)));
        let cb_ptr = self.learner_cb.as_mut().unwrap().as_mut() as *const _ as *const c_void;
        unsafe {
            ffi::ccadical_set_learn(
                self.handle,
                cb_ptr,
                max_len.try_into().unwrap(),
                Some(ffi::ccadical_learn_cb),
            )
        }
    }

    fn detach_learner(&mut self) {
        self.terminate_cb = None;
        unsafe { ffi::ccadical_set_learn(self.handle, std::ptr::null(), 0, None) }
    }
}

/// A trait for a non-canonical functionality of invoking a callback
/// on every LRAT derivation step
pub trait Lrat<'a> {
    /// Connects the callback `cb` to CaDiCaL as an LRAT callback
    fn attach_lrat_callback<CB>(&mut self, cb: CB)
    where
        CB: FnMut(u64, Clause, &[u64]) + 'a;
}

impl<'lrat> Lrat<'lrat> for CaDiCaL<'_, '_, 'lrat> {
    fn attach_lrat_callback<CB>(&mut self, cb: CB)
    where
        CB: FnMut(u64, Clause, &[u64]) + 'lrat,
    {
        self.lrat_cb = Some(Box::new(Box::new(cb)));
        let cb_ptr = self.lrat_cb.as_mut().unwrap().as_mut() as *const _ as *const c_void;
        unsafe { ffi::ccadical_trace_proof_callback(self.handle, cb_ptr, ffi::ccadical_lrat_cb) };
    }
}

impl Interrupt for CaDiCaL<'_, '_, '_> {
    type Interrupter = Interrupter;
    fn interrupter(&mut self) -> Self::Interrupter {
        Interrupter {
            handle: self.handle,
        }
    }
}

/// An Interrupter for the CaDiCaL solver
pub struct Interrupter {
    /// The C API handle
    handle: *mut CaDiCaLHandle,
}

unsafe impl Send for Interrupter {}
unsafe impl Sync for Interrupter {}

impl InterruptSolver for Interrupter {
    fn interrupt(&self) {
        unsafe { ffi::ccadical_terminate(self.handle) }
    }
}

impl PhaseLit for CaDiCaL<'_, '_, '_> {
    /// Forces the default decision phase of a variable to a certain value
    fn phase_lit(&mut self, lit: Lit) -> anyhow::Result<()> {
        unsafe { ffi::ccadical_phase(self.handle, lit.to_ipasir()) };
        Ok(())
    }

    /// Undoes the effect of a call to [`CaDiCaL::phase_lit`]
    fn unphase_var(&mut self, var: Var) -> anyhow::Result<()> {
        unsafe { ffi::ccadical_unphase(self.handle, var.to_ipasir()) };
        Ok(())
    }
}

impl FreezeVar for CaDiCaL<'_, '_, '_> {
    fn freeze_var(&mut self, var: Var) -> anyhow::Result<()> {
        unsafe { ffi::ccadical_freeze(self.handle, var.to_ipasir()) };
        Ok(())
    }

    fn melt_var(&mut self, var: Var) -> anyhow::Result<()> {
        unsafe { ffi::ccadical_melt(self.handle, var.to_ipasir()) };
        Ok(())
    }

    fn is_frozen(&mut self, var: Var) -> anyhow::Result<bool> {
        Ok(unsafe { ffi::ccadical_frozen(self.handle, var.to_ipasir()) } != 0)
    }
}

// >= v1.5.4
#[cfg(all(
    not(feature = "v1-5-3"),
    not(feature = "v1-5-2"),
    not(feature = "v1-5-1"),
    not(feature = "v1-5-0")
))]
impl rustsat::solvers::FlipLit for CaDiCaL<'_, '_, '_> {
    fn flip_lit(&mut self, lit: Lit) -> anyhow::Result<bool> {
        if self.state != InternalSolverState::Sat {
            return Err(StateError {
                required_state: SolverState::Sat,
                actual_state: self.state.to_external(),
            }
            .into());
        }
        Ok(unsafe { ffi::ccadical_flip(self.handle, lit.to_ipasir()) })
    }

    fn is_flippable(&mut self, lit: Lit) -> anyhow::Result<bool> {
        if self.state != InternalSolverState::Sat {
            return Err(StateError {
                required_state: SolverState::Sat,
                actual_state: self.state.to_external(),
            }
            .into());
        }
        Ok(unsafe { ffi::ccadical_flippable(self.handle, lit.to_ipasir()) })
    }
}

impl LimitConflicts for CaDiCaL<'_, '_, '_> {
    fn limit_conflicts(&mut self, limit: Option<u32>) -> anyhow::Result<()> {
        self.set_limit(Limit::Conflicts(if let Some(limit) = limit {
            limit as c_int
        } else {
            -1
        }))
    }
}

impl LimitDecisions for CaDiCaL<'_, '_, '_> {
    fn limit_decisions(&mut self, limit: Option<u32>) -> anyhow::Result<()> {
        self.set_limit(Limit::Decisions(if let Some(limit) = limit {
            limit as c_int
        } else {
            -1
        }))
    }
}

impl GetInternalStats for CaDiCaL<'_, '_, '_> {
    fn propagations(&self) -> usize {
        unsafe { ffi::ccadical_propagations(self.handle) }
            .try_into()
            .unwrap()
    }

    fn decisions(&self) -> usize {
        unsafe { ffi::ccadical_decisions(self.handle) }
            .try_into()
            .unwrap()
    }

    fn conflicts(&self) -> usize {
        unsafe { ffi::ccadical_conflicts(self.handle) }
            .try_into()
            .unwrap()
    }
}

impl SolveStats for CaDiCaL<'_, '_, '_> {
    fn stats(&self) -> SolverStats {
        let max_var_idx = unsafe { ffi::ccadical_vars(self.handle) };
        let max_var = if max_var_idx > 0 {
            Some(Var::new((max_var_idx - 1) as u32))
        } else {
            None
        };
        let mut stats = self.stats.clone();
        stats.max_var = max_var;
        stats
    }

    fn max_var(&self) -> Option<Var> {
        let max_var_idx = unsafe { ffi::ccadical_vars(self.handle) };
        if max_var_idx > 0 {
            Some(Var::new((max_var_idx - 1) as u32))
        } else {
            None
        }
    }
}

impl Drop for CaDiCaL<'_, '_, '_> {
    fn drop(&mut self) {
        unsafe { ffi::ccadical_release(self.handle) }
    }
}

/// Possible CaDiCaL configurations
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum Config {
    /// Set default advanced internal options
    Default,
    /// Disable all internal preprocessing options
    Plain,
    /// Set internal options to target satisfiable instances
    SAT,
    /// Set internal options to target unsatisfiable instances
    UNSAT,
}

impl fmt::Display for Config {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Config::Default => write!(f, "default"),
            Config::Plain => write!(f, "plain"),
            Config::SAT => write!(f, "sat"),
            Config::UNSAT => write!(f, "unsat"),
        }
    }
}

/// Possible CaDiCaL limits
#[derive(Debug)]
pub enum Limit {
    /// The number of calls to [`InterruptSolver::interrupt()`] before CaDiCaL terminates
    Terminate(c_int),
    /// A limit on the number of conflicts
    Conflicts(c_int),
    /// A limit on the number of decisions
    Decisions(c_int),
    /// A limit on the rounds of internal preprocessing
    Preprocessing(c_int),
    /// A limit on the internal local search
    LocalSearch(c_int),
}

impl fmt::Display for Limit {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Limit::Terminate(val) => write!(f, "terminate ({})", val),
            Limit::Conflicts(val) => write!(f, "conflicts ({})", val),
            Limit::Decisions(val) => write!(f, "decisions ({})", val),
            Limit::Preprocessing(val) => write!(f, "preprocessing ({})", val),
            Limit::LocalSearch(val) => write!(f, "localsearch ({})", val),
        }
    }
}

#[cfg(test)]
mod test {
    use super::{CaDiCaL, Config, Limit};
    use rustsat::{
        lit,
        solvers::{Solve, SolverState, StateError},
        types::TernaryVal,
        var,
    };

    rustsat_solvertests::basic_unittests!(CaDiCaL);
    rustsat_solvertests::termination_unittests!(CaDiCaL);
    rustsat_solvertests::learner_unittests!(CaDiCaL);
    rustsat_solvertests::freezing_unittests!(CaDiCaL);

    #[test]
    fn configure() {
        let mut solver = CaDiCaL::default();
        solver.set_configuration(Config::Default).unwrap();
        solver.set_configuration(Config::Plain).unwrap();
        solver.set_configuration(Config::SAT).unwrap();
        solver.set_configuration(Config::UNSAT).unwrap();
        solver.add_unit(lit![0]).unwrap();
        assert!(solver.set_configuration(Config::Default).is_err_and(|e| e
            .downcast::<StateError>()
            .unwrap()
            == StateError {
                required_state: SolverState::Configuring,
                actual_state: SolverState::Input
            }));
    }

    #[test]
    fn options() {
        let mut solver = CaDiCaL::default();
        assert_eq!(solver.get_option("arena").unwrap(), 1);
        solver.set_option("arena", 0).unwrap();
        assert_eq!(solver.get_option("arena").unwrap(), 0);
    }

    #[test]
    fn limit() {
        let mut solver = CaDiCaL::default();
        solver.set_limit(Limit::Conflicts(100)).unwrap();
    }

    #[test]
    fn backend_stats() {
        let mut solver = CaDiCaL::default();
        solver.add_binary(lit![0], !lit![1]).unwrap();
        solver.add_binary(lit![1], !lit![2]).unwrap();
        solver.add_binary(lit![2], !lit![3]).unwrap();
        solver.add_binary(lit![3], !lit![4]).unwrap();
        solver.add_binary(lit![4], !lit![5]).unwrap();
        solver.add_binary(lit![5], !lit![6]).unwrap();
        solver.add_binary(lit![6], !lit![7]).unwrap();
        solver.add_binary(lit![7], !lit![8]).unwrap();
        solver.add_binary(lit![8], !lit![9]).unwrap();

        assert_eq!(solver.get_active(), 10);
        assert_eq!(solver.get_irredundant(), 9);
        assert_eq!(solver.get_redundant(), 0);
        assert_eq!(solver.current_lit_val(lit![0]), TernaryVal::DontCare);
    }
}

mod ffi {
    use core::ffi::{c_char, c_int, c_void};
    use rustsat::{solvers::ControlSignal, types::Lit};
    use std::slice;

    use super::{LearnCallbackPtr, LratCallbackPtr, TermCallbackPtr};

    #[repr(C)]
    pub struct CaDiCaLHandle {
        _private: [u8; 0],
    }

    #[link(name = "cadical", kind = "static")]
    extern "C" {
        // Redefinitions of CaDiCaL C API
        pub fn ccadical_signature() -> *const c_char;
        pub fn ccadical_init() -> *mut CaDiCaLHandle;
        pub fn ccadical_release(solver: *mut CaDiCaLHandle);
        pub fn ccadical_add_mem(solver: *mut CaDiCaLHandle, lit_or_zero: c_int) -> c_int;
        pub fn ccadical_assume_mem(solver: *mut CaDiCaLHandle, lit: c_int) -> c_int;
        pub fn ccadical_solve_mem(solver: *mut CaDiCaLHandle) -> c_int;
        pub fn ccadical_val(solver: *mut CaDiCaLHandle, lit: c_int) -> c_int;
        pub fn ccadical_failed(solver: *mut CaDiCaLHandle, lit: c_int) -> c_int;
        pub fn ccadical_set_terminate(
            solver: *mut CaDiCaLHandle,
            state: *const c_void,
            terminate: Option<extern "C" fn(state: *const c_void) -> c_int>,
        );
        pub fn ccadical_set_learn(
            solver: *mut CaDiCaLHandle,
            state: *const c_void,
            max_length: c_int,
            learn: Option<extern "C" fn(state: *const c_void, clause: *const c_int)>,
        );
        pub fn ccadical_trace_proof_callback(
            solver: *mut CaDiCaLHandle,
            state: *const c_void,
            // callback: extern "C" fn(u64, *const i32, u64, *const u64, u64),
            callback: extern "C" fn(
                state: *const c_void,
                id: u64,
                clause: *const c_int,
                clause_len: usize,
                resolvents: *const u64,
                resolvents_len: usize,
            ),
        ) -> c_int;
        pub fn ccadical_constrain_mem(solver: *mut CaDiCaLHandle, lit: c_int) -> c_int;
        pub fn ccadical_constraint_failed(solver: *mut CaDiCaLHandle) -> c_int;
        pub fn ccadical_set_option_ret(
            solver: *mut CaDiCaLHandle,
            name: *const c_char,
            val: c_int,
        ) -> bool;
        pub fn ccadical_get_option(solver: *mut CaDiCaLHandle, name: *const c_char) -> c_int;
        pub fn ccadical_limit_ret(
            solver: *mut CaDiCaLHandle,
            name: *const c_char,
            limit: c_int,
        ) -> bool;
        pub fn ccadical_print_statistics(solver: *mut CaDiCaLHandle);
        pub fn ccadical_active(solver: *mut CaDiCaLHandle) -> i64;
        pub fn ccadical_irredundant(solver: *mut CaDiCaLHandle) -> i64;
        pub fn ccadical_redundant(solver: *mut CaDiCaLHandle) -> i64;
        pub fn ccadical_fixed(solver: *mut CaDiCaLHandle, lit: c_int) -> c_int;
        pub fn ccadical_terminate(solver: *mut CaDiCaLHandle);
        pub fn ccadical_freeze(solver: *mut CaDiCaLHandle, lit: c_int);
        pub fn ccadical_frozen(solver: *mut CaDiCaLHandle, lit: c_int) -> c_int;
        pub fn ccadical_melt(solver: *mut CaDiCaLHandle, lit: c_int);
        pub fn ccadical_simplify_rounds(solver: *mut CaDiCaLHandle, rounds: c_int) -> c_int;
        pub fn ccadical_configure(solver: *mut CaDiCaLHandle, name: *const c_char) -> bool;
        pub fn ccadical_phase(solver: *mut CaDiCaLHandle, lit: c_int);
        pub fn ccadical_unphase(solver: *mut CaDiCaLHandle, lit: c_int);
        pub fn ccadical_vars(solver: *mut CaDiCaLHandle) -> c_int;
        pub fn ccadical_reserve(solver: *mut CaDiCaLHandle, min_max_var: c_int) -> c_int;
        pub fn ccadical_propagations(solver: *mut CaDiCaLHandle) -> i64;
        pub fn ccadical_decisions(solver: *mut CaDiCaLHandle) -> i64;
        pub fn ccadical_conflicts(solver: *mut CaDiCaLHandle) -> i64;
    }

    // >= v1.5.4
    #[cfg(all(
        not(feature = "v1-5-3"),
        not(feature = "v1-5-2"),
        not(feature = "v1-5-1"),
        not(feature = "v1-5-0")
    ))]
    #[link(name = "cadical", kind = "static")]
    extern "C" {
        pub fn ccadical_flip(solver: *mut CaDiCaLHandle, lit: c_int) -> bool;
        pub fn ccadical_flippable(solver: *mut CaDiCaLHandle, lit: c_int) -> bool;
    }

    // Raw callbacks forwarding to user callbacks
    pub extern "C" fn ccadical_terminate_cb(ptr: *const c_void) -> c_int {
        let cb = unsafe { &mut *(ptr as *mut TermCallbackPtr<'_>) };
        match cb() {
            ControlSignal::Continue => 0,
            ControlSignal::Terminate => 1,
        }
    }

    pub extern "C" fn ccadical_learn_cb(ptr: *const c_void, clause: *const c_int) {
        let cb = unsafe { &mut *(ptr as *mut LearnCallbackPtr<'_>) };

        let mut cnt = 0;
        for n in 0.. {
            if unsafe { *clause.offset(n) } != 0 {
                cnt += 1;
            }
        }
        let int_slice = unsafe { slice::from_raw_parts(clause, cnt) };
        let clause = int_slice
            .iter()
            .map(|il| {
                Lit::from_ipasir(*il).expect("Invalid literal in learned clause from CaDiCaL")
            })
            .collect();
        cb(clause)
    }

    pub extern "C" fn ccadical_lrat_cb(
        ptr: *const c_void,
        clause_id: u64,
        clause: *const c_int,
        clause_len: usize,
        resolvents: *const u64,
        resolvents_len: usize,
    ) {
        let cb = unsafe { &mut *(ptr as *mut LratCallbackPtr<'_>) };
        let clause_slice = unsafe { slice::from_raw_parts(clause, clause_len) };
        let clause = clause_slice
            .iter()
            .map(|il| {
                Lit::from_ipasir(*il).expect("Invalid literal in learned clause from CaDiCaL")
            })
            .collect();
        let resolvents_slice = unsafe { slice::from_raw_parts(resolvents, resolvents_len) };
        cb(clause_id, clause, resolvents_slice)
    }
}
