ipasir-loading 0.1.0

#![doc = include_str!("../README.md")]

use anyhow::{anyhow, Result};
use core::slice;
use libloading::{Library, Symbol};
use std::{
    ffi::{CStr, OsStr},
    ops::{Deref, DerefMut},
    os::raw::{c_char, c_void},
    rc::Rc,
};

/// A structure used to load a shared library and build new SAT solvers from it.
///
/// This structure takes as entry point a path to a shared library containing a SAT solver that conform to the IPASIR specification.
/// An [`IpasirSolverLoader`] is built by passing this path to the [`from_path`](Self::from_path) function.
/// This object can be used to create new solvers with the [`new_solver`](Self::new_solver) function.
///
/// The IPASIR interface provides two functions that take a function pointer as parameter.
/// To use them on solvers created by this object,
/// these functions must be enabled by calling [`enable_set_terminate`](Self::enable_set_terminate)
/// and [`enable_set_learn`](Self::enable_set_learn) before creating the SAT solvers.
///
/// # Example
///
/// ```no_run
/// # use ipasir_loading::IpasirSolverLoader;
/// let mut loader = IpasirSolverLoader::from_path("path/to/lib.so").unwrap();
/// loader.enable_set_terminate(true); // activate ipasir_set_terminate
/// loader.enable_set_learn(Some(8)); // activate ipasir_set_learn for clause of sizes at most 8
/// let sat_solver = loader.new_solver().unwrap(); // create the solver
/// ```
pub struct IpasirSolverLoader {
    library: Rc<Library>,
    enable_set_terminate: bool,
    enable_set_learn: Option<i32>,
}

impl IpasirSolverLoader {
    /// Builds a new [`IpasirSolverLoader`] given a path to a shared library containing a SAT solver that conform to the IPASIR specification.
    ///
    /// # Errors
    ///
    /// This function returns an error if the library cannot be loaded,
    /// e.g. if the path does not point to a shared library.
    pub fn from_path<P: AsRef<OsStr>>(path: P) -> Result<Self> {
        let library = unsafe { Library::new(path)? };
        Ok(Self {
            library: Rc::new(library),
            enable_set_terminate: false,
            enable_set_learn: None,
        })
    }

    /// Returns a string describing the name and the version of the library solver.
    ///
    /// # Errors
    ///
    /// This function returns an error if the library does not include the corresponding IPASIR function,
    /// or if an error occurs when calling it.
    pub fn ipasir_signature(&self) -> Result<String> {
        let c_str_signature = unsafe {
            let function: Symbol<unsafe extern "C" fn() -> *const c_char> =
                self.library.get(b"ipasir_signature")?;
            CStr::from_ptr(function())
        };
        Ok(c_str_signature.to_str()?.to_string())
    }

    /// Builds a new SAT solver from the shared library.
    ///
    /// The returned solver can accept callback functions on termination or when learning a clause
    /// only if the appropriate activation functions ([`enable_set_terminate`](IpasirSolverLoader::enable_set_terminate) or [`enable_set_learn`](IpasirSolverLoader::enable_set_learn)) have been called before calling this function.
    ///
    /// # Errors
    ///
    /// This function returns an error if the library does not contain the `ipasir_init` function,
    /// or if an error occurs when calling it.
    /// In case some callback functions are enabled,
    /// this function will also return an error if the corresponding IPASIR callback function (`ipasir_set_terminate` or `ipasir_set_learn`) is missing from the library or if an error occurs when calling it.
    pub fn new_solver(&self) -> Result<IpasirSolverWrapper> {
        let solver_ptr = unsafe {
            let init_function: Symbol<unsafe extern "C" fn() -> *const c_void> =
                self.library.get(b"ipasir_init")?;
            init_function()
        };
        let mut ipasir_solver_box = Box::new(IpasirSolver {
            library: Rc::clone(&self.library),
            solver: solver_ptr,
            enable_set_terminate: self.enable_set_terminate,
            set_terminate_callbacks: vec![],
            enable_set_learn: self.enable_set_learn,
            set_learn_callbacks: vec![],
            state: SolverState::Input,
        });
        if self.enable_set_terminate {
            Self::enable_set_terminate_for_solver(self, solver_ptr, &mut ipasir_solver_box)?;
        }
        if let Some(bound) = self.enable_set_learn {
            Self::enable_set_learn_for_solver(self, solver_ptr, &mut ipasir_solver_box, bound)?;
        }
        Ok(IpasirSolverWrapper(ipasir_solver_box))
    }

    /// Enables or disables the [`ipasir_set_terminate`](IpasirSolver::ipasir_set_terminate) for the solvers created after the call to this function.
    pub fn enable_set_terminate(&mut self, v: bool) {
        self.enable_set_terminate = v;
    }

    fn enable_set_terminate_for_solver(
        loader: &IpasirSolverLoader,
        solver_ptr: *const c_void,
        ipasir_solver_box: &mut IpasirSolver,
    ) -> Result<()> {
        unsafe {
            let set_terminate_function: Symbol<
                unsafe extern "C" fn(
                    *const c_void,
                    *const c_void,
                    *const fn(*const c_void) -> isize,
                ),
            > = loader.library.get(b"ipasir_set_terminate")?;
            set_terminate_function(
                solver_ptr,
                std::ptr::addr_of_mut!(*ipasir_solver_box) as *const _,
                ipasir_set_terminate_callback as *const _,
            );
        }
        Ok(())
    }

    /// Enables or disables the [`ipasir_set_learn`](IpasirSolver::ipasir_set_learn) for the solvers created after the call to this function.
    ///
    /// To enable the function, pass `Some(n)` where `n` is the maximum length of the learned clauses you are interested in.
    /// To disable the function, pass `None`.
    pub fn enable_set_learn(&mut self, bound: Option<i32>) {
        self.enable_set_learn = bound;
    }

    fn enable_set_learn_for_solver(
        loader: &IpasirSolverLoader,
        solver_ptr: *const c_void,
        ipasir_solver_box: &mut IpasirSolver,
        max_length: i32,
    ) -> Result<()> {
        unsafe {
            let set_learn_function: Symbol<
                unsafe extern "C" fn(
                    *const c_void,
                    *const c_void,
                    i32,
                    *const fn(*const c_void, *const i32),
                ),
            > = loader.library.get(b"ipasir_set_learn")?;
            set_learn_function(
                solver_ptr,
                std::ptr::addr_of_mut!(*ipasir_solver_box) as *const _,
                max_length,
                ipasir_set_learn_callback as *const _,
            );
        }
        Ok(())
    }
}

impl AsRef<Library> for IpasirSolverLoader {
    fn as_ref(&self) -> &Library {
        &self.library
    }
}

extern "C" fn ipasir_set_terminate_callback(solver_ptr: *const IpasirSolver) -> isize {
    let must_terminate = unsafe {
        (*solver_ptr)
            .set_terminate_callbacks
            .iter()
            .any(|callback| callback())
    };
    isize::from(must_terminate)
}

extern "C" fn ipasir_set_learn_callback(solver_ptr: *const IpasirSolver, clause_ptr: *const i32) {
    let clause = unsafe {
        let mut p = clause_ptr;
        while *p != 0 {
            p = p.add(1);
        }
        slice::from_raw_parts(clause_ptr, p.offset_from(clause_ptr).unsigned_abs())
    };
    unsafe {
        (*solver_ptr)
            .set_learn_callbacks
            .iter()
            .for_each(|callback| callback(clause));
    };
}

/// A wrapper around [`IpasirSolver`].
pub struct IpasirSolverWrapper(Box<IpasirSolver>);

impl Deref for IpasirSolverWrapper {
    type Target = IpasirSolver;

    fn deref(&self) -> &Self::Target {
        &self.0
    }
}

impl DerefMut for IpasirSolverWrapper {
    fn deref_mut(&mut self) -> &mut Self::Target {
        &mut self.0
    }
}

type SetLearnCallbackType = Box<dyn Fn(&[i32])>;

type SetTerminateCallbackType = Box<dyn Fn() -> bool>;

#[derive(Debug, Copy, Clone, PartialEq)]
enum SolverState {
    Input,
    Sat,
    Unsat,
}

impl SolverState {
    fn expect_status(self, expected: Self) -> Result<()> {
        if self == expected {
            Ok(())
        } else {
            Err(anyhow!("expected status {expected:?}, was {self:?}"))
        }
    }

    fn update_from_status(&mut self, status: isize) {
        *self = match status {
            0 => *self,
            10 => SolverState::Sat,
            20 => SolverState::Unsat,
            _ => unreachable!(),
        }
    }
}

/// A SAT solver conforming to the IPASIR specification.
///
/// All of the functions below, except the callback functions, are just safe interfaces to the IPASIR functions of the same name.
/// For the two functions where the behavior differs from the specification, this is indicated in the function documentation.
///
/// When the [`IpasirSolver`] is dropped, the underlying data is automatically released by calling the `ipasir_release` function from the loaded library.
/// Note that an error encountered in this function can lead to a panic.
///
/// ```no_run
/// # use ipasir_loading::IpasirSolverLoader;
/// // load the IPASIR library
/// let loader = IpasirSolverLoader::from_path("path/to/lib.so").unwrap();
///
/// // create a solver from the library and populate it
/// let mut solver = loader.new_solver().unwrap();
/// solver.ipasir_add(-1).unwrap();
/// solver.ipasir_add(-2).unwrap();
/// solver.ipasir_add(0).unwrap();
/// solver.ipasir_add(1).unwrap();
/// solver.ipasir_add(2).unwrap();
/// solver.ipasir_add(0).unwrap();
///
/// // check satisfiability and get back the model
/// assert!(solver.ipasir_solve().unwrap().unwrap());
/// let model = vec![solver.ipasir_val(1).unwrap(), solver.ipasir_val(2).unwrap()];
/// let expected_1 = vec![Some(true), Some(false)];
/// let expected_2 = vec![Some(false), Some(true)];
/// assert!(model == expected_1 || model == expected_2);
/// ```
pub struct IpasirSolver {
    library: Rc<Library>,
    solver: *const c_void,
    enable_set_terminate: bool,
    set_terminate_callbacks: Vec<SetTerminateCallbackType>,
    enable_set_learn: Option<i32>,
    set_learn_callbacks: Vec<SetLearnCallbackType>,
    state: SolverState,
}

impl IpasirSolver {
    /// Add the given literal into the currently added clause or finalize the clause with a 0.
    ///
    /// # Errors
    ///
    /// This function returns an error if the library does not include the corresponding IPASIR function,
    /// or if an error occurs when calling it.
    pub fn ipasir_add(&mut self, lit: i32) -> Result<()> {
        unsafe {
            let function: Symbol<unsafe extern "C" fn(*const c_void, i32)> =
                self.library.get(b"ipasir_add")?;
            function(self.solver, lit);
        }
        self.state = SolverState::Input;
        Ok(())
    }

    /// Solve the formula with specified clauses under the specified assumptions.
    ///
    /// The solver returns an `Option` containing `true` (resp. `false`) if the formula is satisfiable,
    /// or `None` if the search was stopped before deciding the satisfiability.
    ///
    /// # Errors
    ///
    /// This function returns an error if the library does not include the corresponding IPASIR function,
    /// or if an error occurs when calling it.
    pub fn ipasir_solve(&mut self) -> Result<Option<bool>> {
        let status = unsafe {
            let function: Symbol<unsafe extern "C" fn(*const c_void) -> isize> =
                self.library.get(b"ipasir_solve")?;
            function(self.solver)
        };
        self.state.update_from_status(status);
        match status {
            0 => Ok(None),
            10 => Ok(Some(true)),
            20 => Ok(Some(false)),
            _ => Err(anyhow!(
                "ipasir_solve returned an unexpected value: {status}"
            )),
        }
    }

    /// Get the truth value of the given literal in the found satisfying assignment.
    /// This function must not be called if the formula changed since the last time `ipasir_solve` found a model.
    ///
    /// This function returns an `Option` containing `true` (resp. `false`) if the variable was set to `true` (resp. `false`) in the last satisfying assignment.
    /// In case the solver detected both polarities of the literal would lead to a model, `None` may be returned.
    ///
    /// # Errors
    ///
    /// This function returns an error if the library does not include the corresponding IPASIR function,
    /// or if an error occurs when calling it.
    pub fn ipasir_val(&mut self, lit: i32) -> Result<Option<bool>> {
        self.state.expect_status(SolverState::Sat)?;
        let value = unsafe {
            let function: Symbol<unsafe extern "C" fn(*const c_void, i32) -> i32> =
                self.library.get(b"ipasir_val")?;
            function(self.solver, lit)
        };
        match value {
            0 => Ok(None),
            n if n == lit.abs() => Ok(Some(true)),
            n if n == -lit.abs() => Ok(Some(false)),
            _ => Err(anyhow!("ipasir_val returned an unexpected value: {value}")),
        }
    }

    /// Add an assumption for the next SAT search (the next call of [`ipasir_solve`](Self::ipasir_solve)).
    /// After calling [`ipasir_solve`](Self::ipasir_solve) all the previously added assumptions are cleared.
    ///
    /// # Errors
    ///
    /// This function returns an error if the library does not include the corresponding IPASIR function,
    /// or if an error occurs when calling it.
    pub fn ipasir_assume(&mut self, lit: i32) -> Result<()> {
        unsafe {
            let function: Symbol<unsafe extern "C" fn(*const c_void, i32)> =
                self.library.get(b"ipasir_assume")?;
            function(self.solver, lit);
        }
        self.state = SolverState::Input;
        Ok(())
    }

    /// Check if the given assumption literal was used to prove the unsatisfiability of the formula under the assumptions used for the last SAT search.
    /// This function must not be called if the formula changed since the last time `ipasir_solve` proved the unsatisfiability of the formula.
    /// Return `true` if so, `false` otherwise.
    ///
    /// # Errors
    ///
    /// This function returns an error if the library does not include the corresponding IPASIR function,
    /// or if an error occurs when calling it.
    pub fn ipasir_failed(&mut self, lit: i32) -> Result<bool> {
        self.state.expect_status(SolverState::Unsat)?;
        let value = unsafe {
            let function: Symbol<unsafe extern "C" fn(*const c_void, i32) -> isize> =
                self.library.get(b"ipasir_failed")?;
            function(self.solver, lit)
        };
        match value {
            0 => Ok(false),
            1 => Ok(true),
            _ => Err(anyhow!(
                "ipasir_failed returned an unexpected value: {value}"
            )),
        }
    }

    /// Add a callback function used to indicate a termination requirement to the solver.
    /// The [`IpasirSolverLoader`] that created this solver must have enabled such callbacks with [`enable_set_terminate`](IpasirSolverLoader::enable_set_terminate).
    ///
    /// The solver will periodically call the callback function and check its return value during the search.
    /// If the function returns `true`, the solver should terminate.
    ///
    /// Contrary to the IPASIR specification, more than one callback function can be set in this way.
    ///
    /// # Errors
    ///
    /// This function will return an error if the correct type of callback function has not been enabled prior to the creation of the solver.
    pub fn ipasir_set_terminate(&mut self, callback: SetTerminateCallbackType) -> Result<()> {
        if self.enable_set_terminate {
            self.set_terminate_callbacks.push(callback);
            Ok(())
        } else {
            Err(anyhow!("ipasir_set_terminate is not enabled; see ipasir-loading documentation for more information"))
        }
    }

    /// Add a callback function to be called when a clause is learned by the solver.
    /// The [`IpasirSolverLoader`] that created this solver must have enabled such callbacks with [`enable_set_learn`](IpasirSolverLoader::enable_set_learn).
    ///
    /// Contrary to the IPASIR specification, more than one callback function can be set in this way.
    /// The maximum length of the clauses passed to the callbacks is defined when enabling the callbacks in [`IpasirSolverLoader`].
    ///
    /// # Errors
    ///
    /// This function will return an error if the correct type of callback function has not been enabled prior to the creation of the solver.
    pub fn ipasir_set_learn(&mut self, callback: SetLearnCallbackType) -> Result<()> {
        if self.enable_set_learn.is_some() {
            self.set_learn_callbacks.push(callback);
            Ok(())
        } else {
            Err(anyhow!("ipasir_set_learn is not enabled; see ipasir-loading documentation for more information"))
        }
    }
}

impl Drop for IpasirSolver {
    fn drop(&mut self) {
        unsafe {
            let function: Symbol<unsafe extern "C" fn(*const c_void)> = self
                .library
                .get(b"ipasir_release")
                .expect("cannot get function ipafair_release from IPSAIR solver library");
            function(self.solver);
        }
    }
}

#[cfg(test)]
#[allow(dead_code, unused_imports)]
mod tests {
    use super::*;
    use std::{cell::RefCell, rc::Rc};

    macro_rules! solver_loader_or_return {
        () => {
            if let Ok(path) = std::env::var("IPASIR_SOLVER") {
                IpasirSolverLoader::from_path(path).unwrap()
            } else {
                return;
            }
        };
    }

    #[test]
    fn test_signature() {
        let loader = solver_loader_or_return!();
        let signature = loader.ipasir_signature().unwrap();
        assert!(!signature.is_empty());
    }

    #[test]
    fn test_sat() {
        let loader = solver_loader_or_return!();
        let mut solver = loader.new_solver().unwrap();
        solver.ipasir_add(1).unwrap();
        solver.ipasir_add(0).unwrap();
        assert!(solver.ipasir_solve().unwrap().unwrap());
        assert!(solver.ipasir_val(1).unwrap().unwrap());
        assert!(!solver.ipasir_val(-1).unwrap().unwrap());
    }

    #[test]
    fn test_sat_neg_lit() {
        let loader = solver_loader_or_return!();
        let mut solver = loader.new_solver().unwrap();
        solver.ipasir_add(-1).unwrap();
        solver.ipasir_add(0).unwrap();
        assert!(solver.ipasir_solve().unwrap().unwrap());
        assert!(!solver.ipasir_val(1).unwrap().unwrap());
        assert!(solver.ipasir_val(-1).unwrap().unwrap());
    }

    #[test]
    fn test_unsat() {
        let loader = solver_loader_or_return!();
        let mut solver = loader.new_solver().unwrap();
        solver.ipasir_add(1).unwrap();
        solver.ipasir_add(0).unwrap();
        solver.ipasir_add(-1).unwrap();
        solver.ipasir_add(0).unwrap();
        assert!(!solver.ipasir_solve().unwrap().unwrap());
    }

    #[test]
    fn test_sat_then_unsat() {
        let loader = solver_loader_or_return!();
        let mut solver = loader.new_solver().unwrap();
        solver.ipasir_add(1).unwrap();
        solver.ipasir_add(0).unwrap();
        assert!(solver.ipasir_solve().unwrap().unwrap());
        assert!(solver.ipasir_val(1).unwrap().unwrap());
        solver.ipasir_add(-1).unwrap();
        solver.ipasir_add(0).unwrap();
        assert!(!solver.ipasir_solve().unwrap().unwrap());
    }

    #[test]
    fn test_assume() {
        let loader = solver_loader_or_return!();
        let mut solver = loader.new_solver().unwrap();
        solver.ipasir_assume(1).unwrap();
        assert!(solver.ipasir_solve().unwrap().unwrap());
        assert!(solver.ipasir_val(1).unwrap().unwrap());
        solver.ipasir_assume(-1).unwrap();
        assert!(solver.ipasir_solve().unwrap().unwrap());
        assert!(!solver.ipasir_val(1).unwrap().unwrap());
        solver.ipasir_assume(1).unwrap();
        solver.ipasir_assume(-1).unwrap();
        assert!(!solver.ipasir_solve().unwrap().unwrap());
    }

    #[test]
    fn test_failed() {
        let loader = solver_loader_or_return!();
        let mut solver = loader.new_solver().unwrap();
        solver.ipasir_add(-1).unwrap();
        solver.ipasir_add(0).unwrap();
        solver.ipasir_assume(1).unwrap();
        solver.ipasir_assume(2).unwrap();
        assert!(!solver.ipasir_solve().unwrap().unwrap());
        assert!(solver.ipasir_failed(1).unwrap());
        assert!(!solver.ipasir_failed(2).unwrap());
    }

    #[allow(clippy::cast_possible_truncation, clippy::cast_possible_wrap)]
    fn encode_php(solver: &mut IpasirSolver, n: usize) {
        let n = n as i32;
        let mut add_clause = |lits: &[i32]| {
            for lit in lits {
                solver.ipasir_add(*lit).unwrap();
            }
            solver.ipasir_add(0).unwrap();
        };
        for var0 in 1..=n {
            let mut lit0 = -var0;
            for i in 0..n {
                let mut lit1 = lit0 - n;
                for _ in 0..(n - i) {
                    add_clause(&[lit0, lit1]);
                    lit1 -= n;
                }
                lit0 -= n;
            }
        }
        (0..=n)
            .map(|i| (i * n + 1..=(i + 1) * n))
            .for_each(|r| add_clause(&r.collect::<Vec<_>>()));
    }

    #[test]
    fn test_set_terminate() {
        let mut loader = solver_loader_or_return!();
        loader.enable_set_terminate(true);
        let mut solver = loader.new_solver().unwrap();
        encode_php(&mut solver, 20);
        let called = Rc::new(RefCell::new(false));
        let called_cl = Rc::clone(&called);
        let callback = Box::new(move || {
            *called_cl.borrow_mut() = true;
            true
        });
        solver.ipasir_set_terminate(callback).unwrap();
        assert!(solver.ipasir_solve().unwrap().is_none());
        assert!(*called.borrow());
    }

    #[test]
    fn test_set_learn() {
        let mut loader = solver_loader_or_return!();
        loader.enable_set_learn(Some(i32::MAX));
        let mut solver = loader.new_solver().unwrap();
        encode_php(&mut solver, 3);
        let n_lits = Rc::new(RefCell::new(0));
        let n_lits_cl = Rc::clone(&n_lits);
        let callback = Box::new(move |clause: &[i32]| {
            *n_lits_cl.borrow_mut() += clause.len();
        });
        solver.ipasir_set_learn(callback).unwrap();
        assert!(!solver.ipasir_solve().unwrap().unwrap());
        assert_ne!(*n_lits.borrow(), 0);
    }

    #[test]
    fn test_set_terminate_is_disabled() {
        let loader = solver_loader_or_return!();
        let mut solver = loader.new_solver().unwrap();
        solver.ipasir_set_terminate(Box::new(|| true)).unwrap_err();
    }

    #[test]
    fn test_set_learn_is_disabled() {
        let loader = solver_loader_or_return!();
        let mut solver = loader.new_solver().unwrap();
        solver.ipasir_set_learn(Box::new(|_| {})).unwrap_err();
    }

    #[test]
    fn test_forbidden_functions_on_input_state() {
        let loader = solver_loader_or_return!();
        let mut solver = loader.new_solver().unwrap();
        solver.ipasir_add(-1).unwrap();
        solver.ipasir_add(0).unwrap();
        solver.ipasir_assume(1).unwrap();
        solver.ipasir_val(1).unwrap_err();
        solver.ipasir_failed(1).unwrap_err();
    }

    #[test]
    fn test_forbidden_functions_on_sat_state() {
        let loader = solver_loader_or_return!();
        let mut solver = loader.new_solver().unwrap();
        solver.ipasir_add(-1).unwrap();
        solver.ipasir_add(0).unwrap();
        assert!(solver.ipasir_solve().unwrap().unwrap());
        solver.ipasir_failed(1).unwrap_err();
    }

    #[test]
    fn test_forbidden_functions_on_unsat_state() {
        let loader = solver_loader_or_return!();
        let mut solver = loader.new_solver().unwrap();
        solver.ipasir_add(-1).unwrap();
        solver.ipasir_add(0).unwrap();
        solver.ipasir_add(1).unwrap();
        solver.ipasir_add(0).unwrap();
        assert!(!solver.ipasir_solve().unwrap().unwrap());
        solver.ipasir_val(1).unwrap_err();
    }

    #[test]
    fn test_xor() {
        let loader = solver_loader_or_return!();
        let mut solver = loader.new_solver().unwrap();
        solver.ipasir_add(-1).unwrap();
        solver.ipasir_add(-2).unwrap();
        solver.ipasir_add(0).unwrap();
        solver.ipasir_add(1).unwrap();
        solver.ipasir_add(2).unwrap();
        solver.ipasir_add(0).unwrap();
        assert!(solver.ipasir_solve().unwrap().unwrap());
        let model = vec![solver.ipasir_val(1).unwrap(), solver.ipasir_val(2).unwrap()];
        let expected_1 = vec![Some(true), Some(false)];
        let expected_2 = vec![Some(false), Some(true)];
        assert!(model == expected_1 || model == expected_2);
    }
}