rustsat-cadical 0.7.5

//! # CaDiCaL Proof Tracing Functionality

use std::ffi::{c_int, c_void};

use rustsat::{
    solvers::SolverResult,
    types::{Assignment, Clause, Lit},
    utils::from_raw_parts_maybe_null,
};

use crate::ffi;

/// The ID of a clause internal to CaDiCaL
#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
#[repr(transparent)]
pub struct ClauseId(pub i64);

/// A conclusion for an incremental proof
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum Conclusion {
    /// The solver found a conflict of the input clauses
    Conflict,
    /// The solver found the input clauses to be unsatisfiable with the assumptions
    Assumptions,
    /// The solver found the input clauses to be unsatisfiable with the temporary constraint
    Constraint,
}

/// Trait that must be implement for a type that can be used to trace a proof generated by CaDiCaL
///
/// This is the equivalent to the proof tracer Cpp-API of CaDiCaL
///
/// Rather than passing [`Clause`] to the tracer, we use [`CaDiCaLClause`], which
/// lazily converts IPASIR literals to [`Lit`] to not perform any work if the clause is not actually
/// used
#[allow(unused_variables)]
pub trait TraceProof {
    /// Notify the tracer that a original clause has been added.
    ///
    /// Includes ID and whether the clause is redundant or irredundant
    fn add_original_clause(
        &mut self,
        id: ClauseId,
        redundant: bool,
        clause: &CaDiCaLClause,
        restored: bool,
    ) {
    }

    /// Notify the observer that a new clause has been derived.
    ///
    /// Includes ID and whether the clause is redundant or irredundant
    /// If antecedents are derived they will be included here.
    fn add_derived_clause(
        &mut self,
        id: ClauseId,
        redundant: bool,
        clause: &CaDiCaLClause,
        antecedents: &[ClauseId],
    ) {
    }

    /// Notify the observer that a clause is deleted.
    ///
    /// Includes ID and redundant/irredundant
    fn delete_clause(&mut self, id: ClauseId, redundant: bool, clause: &CaDiCaLClause) {}

    /// Notify the observer to remember that the clause might be restored later
    fn weaken_minus(&mut self, id: ClauseId, clause: &CaDiCaLClause) {}

    /// Notify the observer that a clause is strengthened
    fn strengthen(&mut self, id: ClauseId) {}

    /// Notify the observer that the solve call ends with status [`SolverResult`]
    /// If the status is UNSAT and an empty clause has been derived, the second
    /// argument will contain its id.
    /// Note that the empty clause is already added through [`TraceProof::add_derived_clause`]
    /// and finalized with [`TraceProof::finalize_clause`]
    fn report_status(&mut self, status: SolverResult, id: ClauseId) {}

    /// Notify the observer that a clause is finalized.
    fn finalize_clause(&mut self, id: ClauseId, clause: &CaDiCaLClause) {}

    /// Notify the observer that the proof begins with a set of reserved ids
    /// for original clauses. Given ID is the first derived clause ID.
    fn begin_proof(&mut self, id: ClauseId) {}

    /// Notify the observer that an assumption has been added
    fn solve_query(&mut self) {}

    /// Notify the observer that an assumption has been added
    fn add_assumption(&mut self, assumption: Lit) {}

    /// Notify the observer that a constraint has been added
    // Arguments: Data, length, constraint_clause
    fn add_constraint(&mut self, constraint: &CaDiCaLClause) {}

    /// Notify the observer that assumptions and constraints are reset
    fn reset_assumptions(&mut self) {}

    /// Notify the observer that this clause could be derived, which
    /// is the negation of a core of failing assumptions/constraints.
    /// If antecedents are derived they will be included here.
    fn add_assumption_clause(
        &mut self,
        id: ClauseId,
        clause: &CaDiCaLClause,
        antecedents: &[ClauseId],
    ) {
    }

    /// Notify the observer that conclude unsat was requested.
    /// will give either the id of the empty clause, the id of a failing
    /// assumption clause or the ids of the failing constrain clauses
    fn conclude_unsat(&mut self, conclusion: Conclusion, failing: &[ClauseId]) {}

    /// Notify the observer that conclude sat was requested.
    /// will give the complete model as a vector.
    fn conclude_sat(&mut self, solution: &CaDiCaLAssignment) {}

    /// Notify the observer that conclude unknown was requested.
    /// will give the current trail as a vector.
    fn conclude_unknown(&mut self, solution: &CaDiCaLAssignment) {}

    /// Notify the observer that two literals are equivalent
    ///
    /// You receive literals, not variables. You can also get notified
    /// multiple times. You can also get notified of BVA variables, aka
    /// variables you did not declare.
    fn notify_equivalence(&mut self, first: Lit, second: Lit) {}
}

/// A handle to an attached proof tracer in order to be able to detach it again
///
/// This is intentionally not [`Clone`] or [`Copy`] so that it cannot be used after the tracer has
/// been disconnected from the solver
#[derive(Debug)]
pub struct ProofTracerHandle<PT> {
    c_class: *mut ffi::CCaDiCaLTracer,
    tracer: *mut PT,
    trait_ptr: *mut *mut dyn TraceProof,
}

impl<PT> Drop for ProofTracerHandle<PT> {
    fn drop(&mut self) {
        let trait_ptr = unsafe { Box::from_raw(self.trait_ptr) };
        drop(trait_ptr);
        let tracer = unsafe { Box::from_raw(self.tracer) };
        drop(tracer);
    }
}

/// Error stating that a provided proof tracer was not connected to the solver
#[derive(Clone, Copy, Debug, thiserror::Error)]
#[error("the provided proof tracer handle is not connected to the solver")]
pub struct ProofTracerNotConnected;

impl super::CaDiCaL<'_, '_> {
    /// Connects a proof tracer to the solver
    ///
    /// **Note**: in order to not leak memory, dropping the [`ProofTracerHandle`] will drop the
    /// proof tracer. Ensure therefore that the handle is not dropped before the solver is not used
    /// anymore, or call [`Self::disconnect_proof_tracer`], if you do not need the proof tracer
    /// anymore.
    pub fn connect_proof_tracer<PT>(
        &mut self,
        tracer: PT,
        antecedents: bool,
    ) -> ProofTracerHandle<PT>
    where
        PT: TraceProof + 'static,
    {
        let tracer = Box::new(tracer);
        let tracer = Box::into_raw(tracer);
        let trait_ptr = Box::new(tracer as *mut dyn TraceProof);
        let trait_ptr = Box::into_raw(trait_ptr);
        let ptr = unsafe {
            ffi::ccadical_connect_proof_tracer(
                self.handle,
                trait_ptr.cast::<c_void>(),
                ffi::prooftracer::DISPATCH_CALLBACKS,
                antecedents,
            )
        };
        ProofTracerHandle {
            c_class: ptr,
            tracer,
            trait_ptr,
        }
    }

    /// Disconnects a proof tracer from the solver
    ///
    /// # Errors
    ///
    /// If the handle is not connected to the given solver, returns [`ProofTracerNotConnected`]
    // We intentionally pass the handle by value here so that it cannot be used afterwards, since
    // it is not Clone of Copy
    #[allow(clippy::needless_pass_by_value)]
    pub fn disconnect_proof_tracer<PT>(
        &mut self,
        handle: ProofTracerHandle<PT>,
    ) -> Result<PT, ProofTracerNotConnected>
    where
        PT: TraceProof + 'static,
    {
        if !unsafe { ffi::ccadical_disconnect_proof_tracer(self.handle, handle.c_class) } {
            return Err(ProofTracerNotConnected);
        }
        let trait_ptr = unsafe { Box::from_raw(handle.trait_ptr) };
        drop(trait_ptr);
        let tracer = unsafe { Box::from_raw(handle.tracer) };
        // avoid dropping tracer in drop implementation
        let _ = std::mem::ManuallyDrop::new(handle);
        Ok(*tracer)
    }

    /// Gets a mutable reference to a connected proof tracer
    // We are intentionally taking self, since the solver "owns" the tracer, even though the
    // compiler doesn't know this
    #[allow(clippy::unused_self)]
    // The handle can only have originated from connect_proof_tracer, the pointer can therefore
    // never be null
    #[allow(clippy::missing_panics_doc)]
    pub fn proof_tracer_mut<PT>(&mut self, handle: &ProofTracerHandle<PT>) -> &mut PT
    where
        PT: TraceProof + 'static,
    {
        unsafe { handle.tracer.as_mut() }.expect("unexpected null ptr")
    }
}

/// A clause passed from CaDiCaL
///
/// This performs lazy conversion to [`Lit`] in order to avoid unnecessary memory allocations and
/// work
#[derive(Debug)]
pub struct CaDiCaLClause<'slf> {
    lits: &'slf [c_int],
}

impl CaDiCaLClause<'_> {
    pub(crate) fn new(cl_len: usize, cl_data: *const c_int) -> Self {
        Self {
            lits: unsafe { from_raw_parts_maybe_null(cl_data, cl_len) },
        }
    }

    /// Gets an iterator over the literals in the clause
    ///
    /// # Panics
    ///
    /// If CaDiCaL passes an invalid IPASIR literal
    pub fn iter(&self) -> impl Iterator<Item = Lit> + '_ {
        self.lits
            .iter()
            .map(|&lit| Lit::from_ipasir(lit).expect("got invalid literal from CaDiCaL"))
    }

    /// Gets the length of the clause
    #[inline]
    #[must_use]
    pub fn len(&self) -> usize {
        self.lits.len()
    }

    /// Checks if the clause is empty
    #[inline]
    #[must_use]
    pub fn is_empty(&self) -> bool {
        self.lits.is_empty()
    }

    /// Converts the clause into an owned [`Clause`]
    ///
    /// This is costly because of IPASIR to [`Lit`] conversion and memory allocation
    #[must_use]
    pub fn to_owned(&self) -> Clause {
        self.iter().collect()
    }
}

#[cfg(feature = "pigeons")]
impl pigeons::ConstraintLike<rustsat::types::Var> for CaDiCaLClause<'_> {
    fn rhs(&self) -> isize {
        1
    }

    fn sum_iter(&self) -> impl Iterator<Item = (isize, pigeons::Axiom<rustsat::types::Var>)> {
        self.iter().map(|l| (1, pigeons::Axiom::from(l)))
    }
}

/// An assignment passed from CaDiCaL
///
/// This performs lazy conversion to [`Lit`] in order to avoid unnecessary memory allocations and
/// work
#[derive(Debug)]
pub struct CaDiCaLAssignment<'slf> {
    lits: &'slf [c_int],
}

impl CaDiCaLAssignment<'_> {
    pub(crate) fn new(assign_len: usize, assign_data: *const c_int) -> Self {
        Self {
            lits: unsafe { from_raw_parts_maybe_null(assign_data, assign_len) },
        }
    }

    /// Gets an iterator over the literals in the assignment
    ///
    /// # Panics
    ///
    /// If CaDiCaL passes an invalid IPASIR literal
    pub fn iter(&self) -> impl Iterator<Item = Lit> + '_ {
        self.lits
            .iter()
            .map(|&lit| Lit::from_ipasir(lit).expect("got invalid literal from CaDiCaL"))
    }

    /// Gets the length of the clause
    #[inline]
    #[must_use]
    pub fn len(&self) -> usize {
        self.lits.len()
    }

    /// Checks if the clause is empty
    #[inline]
    #[must_use]
    pub fn is_empty(&self) -> bool {
        self.lits.is_empty()
    }

    /// Converts the clause into an owned [`rustsat::types::Assignment`]
    ///
    /// This is costly because of IPASIR to [`Lit`] conversion and memory allocation
    #[must_use]
    pub fn to_owned(&self) -> Assignment {
        self.iter().collect()
    }
}

#[cfg(test)]
mod test {
    use crate::CaDiCaL;

    struct Tracer;

    impl super::TraceProof for Tracer {}

    #[test]
    fn connect_tracer() {
        let mut slv = CaDiCaL::default();
        let handle = slv.connect_proof_tracer(Tracer, false);
        let _ = slv.disconnect_proof_tracer(handle).unwrap();
    }
}