sat-solvers 0.1.1

//! Tests for the correctness of available SAT solver executors
//!
//! These tests execute actual SAT solver binaries with simple DIMACS formulas
//! to verify that the executors can correctly identify satisfiable and unsatisfiable
//! problems, and handle timeouts correctly.
//!
//! The tests will run only if the corresponding feature flags for the solvers
//! are enabled. The solvers must be built and available in the expected paths.
#![cfg(any(
    feature = "cadical",
    feature = "glucose",
    feature = "lingeling",
    feature = "minisat",
    feature = "kissat"
))]

use std::time::Duration;

use sat_solvers::SATResult;
use sat_solvers::solvers::SolverExecutor;

/// Create a simple satisfiable DIMACS formula: (x1 OR NOT x2) AND (x2 OR x3)
/// This should be satisfiable with assignment like x1=true, x2=false, x3=true
fn create_simple_sat_dimacs() -> String {
    "p cnf 3 2\n1 -2 0\n2 3 0\n".to_string()
}

/// Create a simple unsatisfiable DIMACS formula: (x1) AND (NOT x1)
fn create_simple_unsat_dimacs() -> String {
    "p cnf 1 2\n1 0\n-1 0\n".to_string()
}

/// Test solver executors with actual solver binaries on satisfiable problems
#[test]
fn test_solver_integration_satisfiable() {
    let dimacs = create_simple_sat_dimacs();
    let timeout = Some(Duration::from_secs(10));

    #[cfg(feature = "cadical")]
    {
        let executor = sat_solvers::solvers::cadical::CaDiCaLExecutor;
        match executor.execute(&dimacs, timeout) {
            Ok(SATResult::Satisfiable(assignment)) => {
                assert!(
                    !assignment.is_empty(),
                    "Assignment should not be empty for SAT result"
                );
                println!(
                    "CaDiCaL found satisfying assignment with {} literals",
                    assignment.len()
                );
            }
            Ok(other) => panic!("Expected satisfiable result, got: {:?}", other),
            Err(e) => panic!("CaDiCaL execution failed: {:?}", e),
        }
    }

    #[cfg(feature = "glucose")]
    {
        let executor = sat_solvers::solvers::glucose::GlucoseExecutor;
        match executor.execute(&dimacs, timeout) {
            Ok(SATResult::Satisfiable(assignment)) => {
                assert!(
                    !assignment.is_empty(),
                    "Assignment should not be empty for SAT result"
                );
                println!(
                    "Glucose found satisfying assignment with {} literals",
                    assignment.len()
                );
            }
            Ok(other) => panic!("Expected satisfiable result, got: {:?}", other),
            Err(e) => panic!("Glucose execution failed: {:?}", e),
        }
    }

    #[cfg(feature = "lingeling")]
    {
        let executor = sat_solvers::solvers::lingeling::LingelingExecutor;
        match executor.execute(&dimacs, timeout) {
            Ok(SATResult::Satisfiable(assignment)) => {
                assert!(
                    !assignment.is_empty(),
                    "Assignment should not be empty for SAT result"
                );
                println!(
                    "Lingeling found satisfying assignment with {} literals",
                    assignment.len()
                );
            }
            Ok(other) => panic!("Expected satisfiable result, got: {:?}", other),
            Err(e) => panic!("Lingeling execution failed: {:?}", e),
        }
    }

    #[cfg(feature = "minisat")]
    {
        let executor = sat_solvers::solvers::minisat::MiniSatExecutor;
        match executor.execute(&dimacs, timeout) {
            Ok(SATResult::Satisfiable(assignment)) => {
                assert!(
                    !assignment.is_empty(),
                    "Assignment should not be empty for SAT result"
                );
                println!(
                    "MiniSat found satisfying assignment with {} literals",
                    assignment.len()
                );
            }
            Ok(other) => panic!("Expected satisfiable result, got: {:?}", other),
            Err(e) => panic!("MiniSat execution failed: {:?}", e),
        }
    }

    #[cfg(feature = "kissat")]
    {
        let executor = sat_solvers::solvers::kissat::KissatExecutor;
        match executor.execute(&dimacs, timeout) {
            Ok(SATResult::Satisfiable(assignment)) => {
                assert!(
                    !assignment.is_empty(),
                    "Assignment should not be empty for SAT result"
                );
                println!(
                    "Kissat found satisfying assignment with {} literals",
                    assignment.len()
                );
            }
            Ok(other) => panic!("Expected satisfiable result, got: {:?}", other),
            Err(e) => panic!("Kissat execution failed: {:?}", e),
        }
    }
}

/// Test solver executors with actual solver binaries on unsatisfiable problems
#[test]
fn test_solver_integration_unsatisfiable() {
    let dimacs = create_simple_unsat_dimacs();
    let timeout = Some(Duration::from_secs(10));

    #[cfg(feature = "cadical")]
    {
        let executor = sat_solvers::solvers::cadical::CaDiCaLExecutor;
        match executor.execute(&dimacs, timeout) {
            Ok(SATResult::Unsatisfiable) => {
                println!("CaDiCaL correctly identified unsatisfiable formula");
            }
            Ok(other) => panic!("Expected unsatisfiable result, got: {:?}", other),
            Err(e) => panic!("CaDiCaL execution failed: {:?}", e),
        }
    }

    #[cfg(feature = "glucose")]
    {
        let executor = sat_solvers::solvers::glucose::GlucoseExecutor;
        match executor.execute(&dimacs, timeout) {
            Ok(SATResult::Unsatisfiable) => {
                println!("Glucose correctly identified unsatisfiable formula");
            }
            Ok(other) => panic!("Expected unsatisfiable result, got: {:?}", other),
            Err(e) => panic!("Glucose execution failed: {:?}", e),
        }
    }

    #[cfg(feature = "lingeling")]
    {
        let executor = sat_solvers::solvers::lingeling::LingelingExecutor;
        match executor.execute(&dimacs, timeout) {
            Ok(SATResult::Unsatisfiable) => {
                println!("Lingeling correctly identified unsatisfiable formula");
            }
            Ok(other) => panic!("Expected unsatisfiable result, got: {:?}", other),
            Err(e) => panic!("Lingeling execution failed: {:?}", e),
        }
    }

    #[cfg(feature = "minisat")]
    {
        let executor = sat_solvers::solvers::minisat::MiniSatExecutor;
        match executor.execute(&dimacs, timeout) {
            Ok(SATResult::Unsatisfiable) => {
                println!("MiniSat correctly identified unsatisfiable formula");
            }
            Ok(other) => panic!("Expected unsatisfiable result, got: {:?}", other),
            Err(e) => panic!("MiniSat execution failed: {:?}", e),
        }
    }

    #[cfg(feature = "kissat")]
    {
        let executor = sat_solvers::solvers::kissat::KissatExecutor;
        match executor.execute(&dimacs, timeout) {
            Ok(SATResult::Unsatisfiable) => {
                println!("Kissat correctly identified unsatisfiable formula");
            }
            Ok(other) => panic!("Expected unsatisfiable result, got: {:?}", other),
            Err(e) => panic!("Kissat execution failed: {:?}", e),
        }
    }
}