sat-solvers 0.1.1

//! # SAT Solvers
//!
//! A unified Rust interface to multiple SAT solvers with automatic source compilation.
//!
//! This crate provides a simple way to use popular SAT solvers (CaDiCaL, MiniSat, Glucose,
//! Lingeling, Kissat) without requiring pre-installed binaries. The solvers are compiled
//! from source during `cargo build`, ensuring reproducible builds across different systems.
//!
//! ## Features
//!
//! - **Self-contained**: Solvers are built from bundled source code during compilation
//! - **Unified interface**: All solvers implement the [`SolverExecutor`] trait
//! - **Feature-gated**: Only compile the solvers you need
//! - **Timeout support**: Built-in timeout handling for long-running problems
//! - **DIMACS format**: Standard CNF input format supported by all solvers
//!
//! ## Quick Start
//!
//! Add `sat-solvers` to your `Cargo.toml`:
//!
//! ```toml
//! [dependencies]
//! sat-solvers = "0.1"
//! ```
//!
//! By default, CaDiCaL and MiniSat are enabled. To use other solvers, enable their features:
//!
//! ```toml
//! [dependencies]
//! sat-solvers = { version = "0.1", features = ["cadical", "glucose", "kissat"] }
//! ```
//!
//! ## Example
//!
//! Solve a simple SAT problem using CaDiCaL:
//!
//! ```no_run
//! use sat_solvers::solvers::SolverExecutor;
//! use sat_solvers::SATResult;
//! use std::time::Duration;
//!
//! # #[cfg(feature = "cadical")]
//! # fn main() {
//! use sat_solvers::solvers::cadical::CaDiCaLExecutor;
//!
//! // Define a simple CNF formula in DIMACS format:
//! // (x1 OR NOT x2) AND (x2 OR x3)
//! let dimacs = "p cnf 3 2\n1 -2 0\n2 3 0\n";
//!
//! let executor = CaDiCaLExecutor;
//! let result = executor.execute(dimacs, Some(Duration::from_secs(30))).unwrap();
//!
//! match result {
//!     SATResult::Satisfiable(assignment) => {
//!         println!("Satisfiable! Assignment: {:?}", assignment);
//!     }
//!     SATResult::Unsatisfiable => {
//!         println!("Unsatisfiable");
//!     }
//!     SATResult::Unknown => {
//!         println!("Unknown (timeout or resource limit)");
//!     }
//! }
//! # }
//! # #[cfg(not(feature = "cadical"))]
//! # fn main() {}
//! ```
//!
//! ## Available Solvers
//!
//! | Feature     | Solver    | Description                                      |
//! |-------------|-----------|--------------------------------------------------|
//! | `cadical`   | CaDiCaL   | State-of-the-art CDCL solver, SAT Competition winner |
//! | `minisat`   | MiniSat   | Classic, widely-used SAT solver                  |
//! | `glucose`   | Glucose   | MiniSat derivative with improved learning        |
//! | `lingeling` | Lingeling | High-performance solver by Armin Biere           |
//! | `kissat`    | Kissat    | Successor to CaDiCaL, SAT Competition 2020+ winner |
//!
//! ## Build Requirements
//!
//! Since solvers are compiled from source, you need:
//!
//! - A C++ compiler (g++ or clang++)
//! - `make`
//! - `cmake` (for Glucose)
//!
//! ## DIMACS CNF Format
//!
//! The solvers accept input in DIMACS CNF format:
//!
//! ```text
//! p cnf <num_variables> <num_clauses>
//! <literal1> <literal2> ... 0
//! <literal1> <literal2> ... 0
//! ...
//! ```
//!
//! - Variables are positive integers (1, 2, 3, ...)
//! - Negative literals represent negation (-1 means NOT x1)
//! - Each clause ends with 0

#![warn(missing_docs)]
#![deny(rustdoc::broken_intra_doc_links)]

use thiserror::Error;

use std::fmt;
use std::path::PathBuf;
#[cfg(any(
    feature = "minisat",
    feature = "glucose",
    feature = "cadical",
    feature = "kissat",
    feature = "lingeling"
))]
use std::process::Command;
use std::process::Output;

pub mod solvers;
pub use solvers::SolverExecutor;

/// Identifies which SAT solver to use.
///
/// Each variant corresponds to a different SAT solver implementation.
/// The availability of each solver depends on the enabled feature flags.
///
/// # Example
///
/// ```
/// use sat_solvers::SATSolverKind;
///
/// let solver = SATSolverKind::CaDiCaL;
/// println!("Using solver: {}", solver);
/// ```
#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, serde::Serialize, serde::Deserialize)]
pub enum SATSolverKind {
    /// CaDiCaL - State-of-the-art CDCL SAT solver by Armin Biere.
    /// Winner of multiple SAT Competitions.
    CaDiCaL,
    /// MiniSat - A minimalistic, open-source SAT solver.
    /// One of the most widely used and studied SAT solvers.
    MiniSat,
    /// Glucose - A CDCL SAT solver based on MiniSat with improved clause learning.
    Glucose,
    /// Lingeling - A high-performance SAT solver by Armin Biere.
    Lingeling,
    /// Kissat - Successor to CaDiCaL, winner of SAT Competition 2020 and later.
    Kissat,
}

impl fmt::Display for SATSolverKind {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            SATSolverKind::CaDiCaL => write!(f, "CaDiCaL"),
            SATSolverKind::MiniSat => write!(f, "MiniSat"),
            SATSolverKind::Glucose => write!(f, "Glucose"),
            SATSolverKind::Lingeling => write!(f, "Lingeling"),
            SATSolverKind::Kissat => write!(f, "Kissat"),
        }
    }
}

/// The result of a SAT solver execution.
///
/// A SAT problem can have three possible outcomes:
/// - [`Satisfiable`](SATResult::Satisfiable): A satisfying assignment exists
/// - [`Unsatisfiable`](SATResult::Unsatisfiable): No satisfying assignment exists
/// - [`Unknown`](SATResult::Unknown): The solver couldn't determine satisfiability
///   (e.g., due to timeout or resource limits)
///
/// # Example
///
/// ```
/// use sat_solvers::SATResult;
///
/// let result = SATResult::Satisfiable(vec![1, -2, 3]);
///
/// if result.is_satisfiable() {
///     if let SATResult::Satisfiable(assignment) = result {
///         // assignment contains the satisfying variable assignments
///         // Positive values mean the variable is true, negative means false
///         assert!(assignment.contains(&1));  // x1 = true
///         assert!(assignment.contains(&-2)); // x2 = false
///     }
/// }
/// ```
#[derive(Debug, PartialEq, Eq, Clone)]
pub enum SATResult {
    /// The formula is satisfiable. Contains the satisfying assignment as a
    /// vector of literals. Positive values indicate the variable is true,
    /// negative values indicate the variable is false.
    Satisfiable(Vec<i32>),
    /// The formula is unsatisfiable (no satisfying assignment exists).
    Unsatisfiable,
    /// The solver could not determine satisfiability (e.g., timeout).
    Unknown,
}

impl SATResult {
    /// Returns `true` if the result is [`Satisfiable`](SATResult::Satisfiable).
    ///
    /// # Example
    ///
    /// ```
    /// use sat_solvers::SATResult;
    ///
    /// let sat = SATResult::Satisfiable(vec![1, -2]);
    /// let unsat = SATResult::Unsatisfiable;
    ///
    /// assert!(sat.is_satisfiable());
    /// assert!(!unsat.is_satisfiable());
    /// ```
    pub fn is_satisfiable(&self) -> bool {
        matches!(self, SATResult::Satisfiable(_))
    }

    /// Returns `true` if the result is [`Unsatisfiable`](SATResult::Unsatisfiable).
    ///
    /// # Example
    ///
    /// ```
    /// use sat_solvers::SATResult;
    ///
    /// let unsat = SATResult::Unsatisfiable;
    /// assert!(unsat.is_unsatisfiable());
    /// ```
    pub fn is_unsatisfiable(&self) -> bool {
        matches!(self, SATResult::Unsatisfiable)
    }

    /// Returns `true` if the result is [`Unknown`](SATResult::Unknown).
    ///
    /// # Example
    ///
    /// ```
    /// use sat_solvers::SATResult;
    ///
    /// let unknown = SATResult::Unknown;
    /// assert!(unknown.is_unknown());
    /// ```
    pub fn is_unknown(&self) -> bool {
        matches!(self, SATResult::Unknown)
    }
}

impl fmt::Display for SATResult {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            SATResult::Satisfiable(model) => write!(f, "SATISFIABLE with model: {:?}", model),
            SATResult::Unsatisfiable => write!(f, "UNSATISFIABLE"),
            SATResult::Unknown => write!(f, "UNKNOWN"),
        }
    }
}

/// Errors that can occur when working with SAT solvers.
///
/// This enum represents all possible errors that can be returned by
/// the crate's public API.
#[derive(Debug, Error)]
pub enum SATSolversError {
    /// The requested solver is not available in this build.
    ///
    /// This occurs when trying to use a solver whose feature flag
    /// was not enabled at compile time.
    #[error("Solver '{0}' is not available in this build.")]
    SolverNotAvailable(String),

    /// The solver binary was not found at the expected path.
    ///
    /// This typically indicates a build issue where the solver
    /// failed to compile or the binary was moved/deleted.
    #[error("Solver binary not found at path: {0}")]
    SolverBinaryNotFound(PathBuf),

    /// An I/O error occurred while executing the solver.
    #[error("I/O Error: {0}")]
    IoError(#[from] std::io::Error),
}

type Result<T> = std::result::Result<T, SATSolversError>;

/// Returns the path to the MiniSat binary.
///
/// The path can be overridden by setting the `MINISAT_BINARY_PATH` environment variable.
/// Otherwise, the path determined at build time is used.
///
/// # Panics
///
/// Panics if the `minisat` feature is not enabled.
#[cfg(feature = "minisat")]
pub fn minisat_path() -> PathBuf {
    std::env::var("MINISAT_BINARY_PATH")
        .unwrap_or_else(|_| env!("MINISAT_BINARY_PATH").to_string())
        .into()
}

/// Returns the path to the Glucose binary.
///
/// The path can be overridden by setting the `GLUCOSE_BINARY_PATH` environment variable.
/// Otherwise, the path determined at build time is used.
///
/// # Panics
///
/// Panics if the `glucose` feature is not enabled.
#[cfg(feature = "glucose")]
pub fn glucose_path() -> PathBuf {
    std::env::var("GLUCOSE_BINARY_PATH")
        .unwrap_or_else(|_| env!("GLUCOSE_BINARY_PATH").to_string())
        .into()
}

/// Returns the path to the CaDiCaL binary.
///
/// The path can be overridden by setting the `CADICAL_BINARY_PATH` environment variable.
/// Otherwise, the path determined at build time is used.
///
/// # Panics
///
/// Panics if the `cadical` feature is not enabled.
#[cfg(feature = "cadical")]
pub fn cadical_path() -> PathBuf {
    std::env::var("CADICAL_BINARY_PATH")
        .unwrap_or_else(|_| env!("CADICAL_BINARY_PATH").to_string())
        .into()
}

/// Returns the path to the Kissat binary.
///
/// The path can be overridden by setting the `KISSAT_BINARY_PATH` environment variable.
/// Otherwise, the path determined at build time is used.
///
/// # Panics
///
/// Panics if the `kissat` feature is not enabled.
#[cfg(feature = "kissat")]
pub fn kissat_path() -> PathBuf {
    std::env::var("KISSAT_BINARY_PATH")
        .unwrap_or_else(|_| env!("KISSAT_BINARY_PATH").to_string())
        .into()
}

/// Returns the path to the Lingeling binary.
///
/// The path can be overridden by setting the `LINGELING_BINARY_PATH` environment variable.
/// Otherwise, the path determined at build time is used.
///
/// # Panics
///
/// Panics if the `lingeling` feature is not enabled.
#[cfg(feature = "lingeling")]
pub fn lingeling_path() -> PathBuf {
    std::env::var("LINGELING_BINARY_PATH")
        .unwrap_or_else(|_| env!("LINGELING_BINARY_PATH").to_string())
        .into()
}

/// Returns the path to the specified solver's binary.
///
/// # Arguments
///
/// * `solver` - The name of the solver (case-insensitive). Valid values are:
///   `"minisat"`, `"glucose"`, `"cadical"`, `"kissat"`, `"lingeling"`
///
/// # Errors
///
/// Returns [`SATSolversError::SolverNotAvailable`] if the solver is not
/// enabled via feature flags or if the solver name is not recognized.
///
/// # Example
///
/// ```no_run
/// use sat_solvers::solver_path;
///
/// # #[cfg(feature = "cadical")]
/// let path = solver_path("cadical").unwrap();
/// ```
pub fn solver_path(solver: &str) -> Result<PathBuf> {
    match solver.to_ascii_lowercase() {
        #[cfg(feature = "minisat")]
        ref s if s == "minisat" => Ok(minisat_path()),
        #[cfg(feature = "glucose")]
        ref s if s == "glucose" => Ok(glucose_path()),
        #[cfg(feature = "cadical")]
        ref s if s == "cadical" => Ok(cadical_path()),
        #[cfg(feature = "kissat")]
        ref s if s == "kissat" => Ok(kissat_path()),
        #[cfg(feature = "lingeling")]
        ref s if s == "lingeling" => Ok(lingeling_path()),
        _ => Err(SATSolversError::SolverNotAvailable(solver.to_string())),
    }
}

/// Runs the specified solver with the given command-line arguments.
///
/// This is a low-level function that executes the solver binary directly.
/// For most use cases, prefer using the [`SolverExecutor`] trait instead.
///
/// # Arguments
///
/// * `solver` - The name of the solver (case-insensitive)
/// * `args` - Command-line arguments to pass to the solver
///
/// # Errors
///
/// Returns [`SATSolversError::SolverNotAvailable`] if the solver is not enabled,
/// or [`SATSolversError::IoError`] if execution fails.
///
/// # Example
///
/// ```no_run
/// use sat_solvers::run_solver;
///
/// # #[cfg(feature = "cadical")]
/// let output = run_solver("cadical", &["--help"]).unwrap();
/// ```
#[allow(unused_variables)]
pub fn run_solver(solver: &str, args: &[&str]) -> Result<Output> {
    match solver.to_ascii_lowercase() {
        #[cfg(feature = "minisat")]
        ref s if s == "minisat" => Ok(Command::new(minisat_path()).args(args).output()?),
        #[cfg(feature = "glucose")]
        ref s if s == "glucose" => Ok(Command::new(glucose_path()).args(args).output()?),
        #[cfg(feature = "cadical")]
        ref s if s == "cadical" => Ok(Command::new(cadical_path()).args(args).output()?),
        #[cfg(feature = "kissat")]
        ref s if s == "kissat" => Ok(Command::new(kissat_path()).args(args).output()?),
        #[cfg(feature = "lingeling")]
        ref s if s == "lingeling" => Ok(Command::new(lingeling_path()).args(args).output()?),
        _ => Err(SATSolversError::SolverNotAvailable(solver.to_string())),
    }
}

/// Ensures that the specified solver binary exists at its expected path.
///
/// # Arguments
///
/// * `solver` - The name of the solver (case-insensitive)
///
/// # Errors
///
/// Returns [`SATSolversError::SolverNotAvailable`] if the solver is not enabled,
/// or [`SATSolversError::SolverBinaryNotFound`] if the binary doesn't exist.
///
/// # Example
///
/// ```no_run
/// use sat_solvers::ensure_solver_exists;
///
/// # #[cfg(feature = "cadical")]
/// match ensure_solver_exists("cadical") {
///     Ok(path) => println!("CaDiCaL found at: {}", path.display()),
///     Err(e) => eprintln!("Error: {}", e),
/// }
/// ```
pub fn ensure_solver_exists(solver: &str) -> Result<PathBuf> {
    let p = solver_path(solver);
    match p {
        Ok(path) => {
            if path.exists() {
                Ok(path)
            } else {
                Err(SATSolversError::SolverBinaryNotFound(path))
            }
        }
        Err(e) => Err(e),
    }
}