sat-solvers 0.1.1

//! SAT solver executors and utilities.
//!
//! This module provides the [`SolverExecutor`] trait and implementations for
//! each supported SAT solver. It also includes utilities for executing solvers
//! with timeout support.
//!
//! # Available Executors
//!
//! Each solver has its own executor type (enabled via feature flags):
//!
//! - [`cadical::CaDiCaLExecutor`] - CaDiCaL solver (feature: `cadical`)
//! - [`minisat::MiniSatExecutor`] - MiniSat solver (feature: `minisat`)
//! - [`glucose::GlucoseExecutor`] - Glucose solver (feature: `glucose`)
//! - [`lingeling::LingelingExecutor`] - Lingeling solver (feature: `lingeling`)
//! - [`kissat::KissatExecutor`] - Kissat solver (feature: `kissat`)
//!
//! # Example
//!
//! ```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;
//!
//! let executor = CaDiCaLExecutor;
//! let dimacs = "p cnf 2 1\n1 2 0\n";
//!
//! match executor.execute(dimacs, Some(Duration::from_secs(60))) {
//!     Ok(SATResult::Satisfiable(assignment)) => {
//!         println!("SAT: {:?}", assignment);
//!     }
//!     Ok(SATResult::Unsatisfiable) => println!("UNSAT"),
//!     Ok(SATResult::Unknown) => println!("UNKNOWN"),
//!     Err(e) => eprintln!("Error: {}", e),
//! }
//! # }
//! # #[cfg(not(feature = "cadical"))]
//! # fn main() {}
//! ```

use thiserror::Error;

use std::{
    path::{Path, PathBuf},
    process::{Command, Stdio},
    thread,
    time::{Duration, Instant},
};

use super::SATResult;

#[cfg(feature = "cadical")]
pub mod cadical;
#[cfg(feature = "glucose")]
pub mod glucose;
#[cfg(feature = "kissat")]
pub mod kissat;
#[cfg(feature = "lingeling")]
pub mod lingeling;
#[cfg(feature = "minisat")]
pub mod minisat;

/// Errors that can occur during SAT solver execution.
///
/// This error type covers all failure modes when running a SAT solver,
/// including I/O errors, process failures, timeouts, and output parsing issues.
#[derive(Error, Debug)]
pub enum SATSolverError {
    /// An I/O error occurred (e.g., failed to spawn process or write temp file).
    #[error("I/O error: {0}")]
    Io(#[from] std::io::Error),

    /// The solver process crashed with a non-standard exit code.
    ///
    /// Standard exit codes (10 = SAT, 20 = UNSAT, 0 = success) are not errors.
    #[error("Process crashed with exit code: {code:?}")]
    ProcessCrashed {
        /// The exit code, or `None` if the process was terminated by a signal.
        code: Option<i32>,
    },

    /// The solver exceeded the specified timeout.
    ///
    /// When this occurs, the solver process is killed and this error is returned.
    #[error("Solver timed out after {timeout:?}")]
    Timeout {
        /// The timeout duration that was exceeded.
        timeout: Duration,
    },

    /// Failed to parse the solver's output.
    ///
    /// This can occur if the solver produces unexpected output format,
    /// or if there are inconsistencies in the output.
    #[error("Output parsing error: {0}")]
    OutputParseError(String),
}

/// Trait for SAT solver execution.
///
/// This trait provides a unified interface for executing different SAT solvers.
/// Each solver implementation handles its specific command-line interface and
/// output format.
///
/// # Implementors
///
/// - [`cadical::CaDiCaLExecutor`] (requires `cadical` feature)
/// - [`minisat::MiniSatExecutor`] (requires `minisat` feature)
/// - [`glucose::GlucoseExecutor`] (requires `glucose` feature)
/// - [`lingeling::LingelingExecutor`] (requires `lingeling` feature)
/// - [`kissat::KissatExecutor`] (requires `kissat` feature)
///
/// # Example
///
/// ```no_run
/// use sat_solvers::solvers::SolverExecutor;
/// use std::time::Duration;
///
/// # #[cfg(feature = "cadical")]
/// fn solve_with_any_executor(executor: &impl SolverExecutor, dimacs: &str) {
///     let result = executor.execute(dimacs, Some(Duration::from_secs(30)));
///     match result {
///         Ok(r) => println!("Result: {}", r),
///         Err(e) => eprintln!("Error: {}", e),
///     }
/// }
/// ```
pub trait SolverExecutor {
    /// Returns the path to the solver binary.
    ///
    /// The path is typically determined at build time and embedded in the binary.
    /// It can often be overridden via environment variables.
    fn get_solver_path(&self) -> PathBuf;

    /// Executes the SAT solver with the given DIMACS input.
    ///
    /// This is the main entry point for solving SAT problems. The input should
    /// be a valid DIMACS CNF formula.
    ///
    /// # Arguments
    ///
    /// * `dimacs` - The SAT problem in DIMACS CNF format
    /// * `timeout` - Optional timeout duration. If `None`, no timeout is applied.
    ///
    /// # Returns
    ///
    /// Returns a [`SATResult`] indicating whether the problem is satisfiable,
    /// unsatisfiable, or unknown (e.g., due to timeout).
    ///
    /// # Errors
    ///
    /// Returns [`SATSolverError`] if:
    /// - The solver process fails to start ([`SATSolverError::Io`])
    /// - The solver crashes ([`SATSolverError::ProcessCrashed`])
    /// - The timeout is exceeded ([`SATSolverError::Timeout`])
    /// - The output cannot be parsed ([`SATSolverError::OutputParseError`])
    fn execute(&self, dimacs: &str, timeout: Option<Duration>)
    -> Result<SATResult, SATSolverError>;

    /// Returns solver-specific command-line arguments.
    ///
    /// This method is used internally by [`execute`](SolverExecutor::execute)
    /// to construct the command line for the solver.
    ///
    /// # Arguments
    ///
    /// * `input_file` - Path to the temporary file containing the DIMACS input
    fn get_args(&self, input_file: &Path) -> Vec<String>;

    /// Parses the solver's output to extract the result.
    ///
    /// Each solver has its own output format. This method handles the
    /// solver-specific parsing logic.
    ///
    /// # Arguments
    ///
    /// * `stdout` - The solver's standard output
    /// * `stderr` - The solver's standard error
    ///
    /// # Errors
    ///
    /// Returns [`SATSolverError::OutputParseError`] if the output cannot be parsed.
    fn parse_output(&self, stdout: &str, stderr: &str) -> Result<SATResult, SATSolverError>;
}

/// Executes a command with an optional timeout.
///
/// This is a helper function used by solver executors to run the solver binary
/// with timeout support.
///
/// # Arguments
///
/// * `solver_path` - Path to the solver binary
/// * `args` - Command-line arguments for the solver
/// * `timeout` - Optional timeout duration. If `None`, the maximum possible
///   duration is used (effectively no timeout).
///
/// # Returns
///
/// Returns a tuple of `(stdout, stderr)` as strings.
///
/// # Errors
///
/// Returns [`SATSolverError`] if:
/// - The process fails to spawn ([`SATSolverError::Io`])
/// - The process crashes with a non-standard exit code ([`SATSolverError::ProcessCrashed`])
/// - The timeout is exceeded ([`SATSolverError::Timeout`])
///
/// # Exit Code Handling
///
/// The following exit codes are considered successful:
/// - `10`: SATISFIABLE (standard SAT solver convention)
/// - `20`: UNSATISFIABLE (standard SAT solver convention)
/// - `0`: General success
///
/// Any other exit code is treated as a crash.
pub fn execute_with_timeout(
    solver_path: &Path,
    args: &[String],
    timeout: Option<Duration>,
) -> Result<(String, String), SATSolverError> {
    let mut cmd = Command::new(solver_path);
    cmd.args(args).stdout(Stdio::piped()).stderr(Stdio::piped());

    let mut child = cmd.spawn()?;
    let timeout = timeout.unwrap_or(Duration::from_secs(u64::MAX));
    let start_time = Instant::now();

    // Wait for completion or timeout
    loop {
        match child.try_wait()? {
            Some(status) => {
                if let Some(code) = status.code() {
                    match code {
                        10 => break, // SATISFIABLE
                        20 => break, // UNSATISFIABLE
                        0 => break,  // SUCCESS
                        _ => {
                            return Err(SATSolverError::ProcessCrashed { code: Some(code) });
                        }
                    }
                }
                break;
            }
            None => {
                if start_time.elapsed() > timeout {
                    let _ = child.kill();
                    let _ = child.wait();
                    return Err(SATSolverError::Timeout { timeout });
                }
                thread::sleep(Duration::from_millis(100));
            }
        }
    }

    let output = child.wait_with_output()?;
    let stdout = String::from_utf8_lossy(&output.stdout).to_string();
    let stderr = String::from_utf8_lossy(&output.stderr).to_string();

    Ok((stdout, stderr))
}