sat-solvers 0.1.1

#[cfg(any(
    feature = "minisat",
    feature = "glucose",
    feature = "cadical",
    feature = "lingeling",
    feature = "kissat",
))]
use std::{
    fs,
    path::{Path, PathBuf},
    process::Command,
    sync::Arc,
};

#[cfg(feature = "minisat")]
const MINISAT_VERSION: &str = "2.2.0";
#[cfg(feature = "glucose")]
const GLUCOSE_VERSION: &str = "4.2.1";
#[cfg(feature = "cadical")]
const CADICAL_VERSION: &str = "2.1.3";
#[cfg(feature = "lingeling")]
const LINGELING_VERSION: &str = "1.0.0";
#[cfg(feature = "kissat")]
const KISSAT_VERSION: &str = "4.0.4";

#[cfg(feature = "minisat")]
const MINISAT_SOURCE: &str = "lib/minisat";
#[cfg(feature = "glucose")]
const GLUCOSE_SOURCE: &str = "lib/glucose";
#[cfg(feature = "cadical")]
const CADICAL_SOURCE: &str = "lib/cadical";
#[cfg(feature = "lingeling")]
const LINGELING_SOURCE: &str = "lib/lingeling";
#[cfg(feature = "kissat")]
const KISSAT_SOURCE: &str = "lib/kissat";

fn main() {
    set_version_env_vars();

    if !check_enabled_features() {
        println!("cargo:warning=No SAT solver features enabled");
        #[allow(clippy::needless_return)]
        return;
    }

    #[cfg(any(
        feature = "minisat",
        feature = "glucose",
        feature = "cadical",
        feature = "lingeling",
        feature = "kissat",
    ))]
    {
        build_all().unwrap_or_else(|e| {
            panic!("Failed to build SAT solvers: {}", e);
        });
    }
}

/// Sets environment variables for the versions of the SAT solvers.
fn set_version_env_vars() {
    #[cfg(feature = "minisat")]
    println!("cargo:rustc-env=MINISAT_VERSION={}", MINISAT_VERSION);
    #[cfg(feature = "glucose")]
    println!("cargo:rustc-env=GLUCOSE_VERSION={}", GLUCOSE_VERSION);
    #[cfg(feature = "cadical")]
    println!("cargo:rustc-env=CADICAL_VERSION={}", CADICAL_VERSION);
    #[cfg(feature = "lingeling")]
    println!("cargo:rustc-env=LINGELING_VERSION={}", LINGELING_VERSION);
    #[cfg(feature = "kissat")]
    println!("cargo:rustc-env=KISSAT_VERSION={}", KISSAT_VERSION);
}

/// Checks if any SAT solver features are enabled.
fn check_enabled_features() -> bool {
    [
        cfg!(feature = "minisat"),
        cfg!(feature = "glucose"),
        cfg!(feature = "cadical"),
        cfg!(feature = "lingeling"),
        cfg!(feature = "kissat"),
    ]
    .iter()
    .any(|&x| x)
}

#[cfg(any(
    feature = "minisat",
    feature = "glucose",
    feature = "cadical",
    feature = "lingeling",
    feature = "kissat"
))]
fn build_all() -> Result<(), String> {
    use std::thread;

    let build_dir = utils::build_dir();
    fs::create_dir_all(&build_dir)
        .map_err(|e| format!("Failed to create build directory: {}", e))?;

    let build_dir = Arc::new(build_dir.to_path_buf());
    let mut handles: Vec<(String, thread::JoinHandle<()>)> = Vec::new();

    #[cfg(feature = "minisat")]
    {
        let build_dir_clone = Arc::clone(&build_dir);
        let handle = thread::spawn(move || {
            build_minisat(&build_dir_clone).expect("Failed to build MiniSAT");
        });
        handles.push(("MiniSAT".to_string(), handle));
    }

    #[cfg(feature = "glucose")]
    {
        let build_dir_clone = Arc::clone(&build_dir);
        let handle = thread::spawn(move || {
            build_glucose(&build_dir_clone).expect("Failed to build Glucose SAT solver");
        });
        handles.push(("Glucose".to_string(), handle));
    }

    #[cfg(feature = "cadical")]
    {
        let build_dir_clone = Arc::clone(&build_dir);
        let handle = thread::spawn(move || {
            build_cadical(&build_dir_clone).expect("Failed to build CaDiCaL SAT solver");
        });
        handles.push(("CaDiCaL".to_string(), handle));
    }

    #[cfg(feature = "lingeling")]
    {
        let build_dir_clone = Arc::clone(&build_dir);
        let handle = thread::spawn(move || {
            build_lingeling(&build_dir_clone).expect("Failed to build Lingeling SAT solver");
        });
        handles.push(("Lingeling".to_string(), handle));
    }

    #[cfg(feature = "kissat")]
    {
        let build_dir_clone = Arc::clone(&build_dir);
        let handle = thread::spawn(move || {
            build_kissat(&build_dir_clone).expect("Failed to build Kissat SAT solver");
        });
        handles.push(("Kissat".to_string(), handle));
    }

    // Wait for all builds to complete
    println!(
        "Starting concurrent builds for {} solver(s)...",
        handles.len()
    );

    // Collect results from all threads
    let mut errors = Vec::new();
    for (solver_name, handle) in handles {
        match handle.join() {
            Ok(_) => println!("{} build completed successfully", solver_name),
            Err(_) => {
                let error_message = format!("{} build failed", solver_name);
                println!("cargo:warning={}", error_message);
                errors.push(error_message);
            }
        }
    }

    // Check if any errors occurred during the builds
    if !errors.is_empty() {
        Err(format!("Build errors: {}", errors.join(", ")))
    } else {
        println!("All solver builds completed successfully");
        Ok(())
    }
}

#[cfg(feature = "minisat")]
fn build_minisat(build_dir: &Path) -> Result<PathBuf, String> {
    // Check if the MiniSAT source directory exists
    println!("cargo:rerun-if-changed={}", MINISAT_SOURCE);
    let minisat_src = Path::new(MINISAT_SOURCE);
    utils::verify_src_exists(minisat_src, "MiniSAT")?;

    // Start building the MiniSAT binary
    println!("Building MiniSAT v{} binary...", MINISAT_VERSION);

    // Copy the source directory to the build directory
    let minisat_build_dir = utils::copy_src_dir(minisat_src, build_dir, "minisat")
        .map_err(|e| format!("Failed to copy MiniSAT source directory: {}", e))?;

    // Create the `make` command
    // Note: MiniSat has C++ compatibility issues with macOS clang.
    // On macOS, you may need to install GCC via homebrew and set CXX=g++-14
    let mut make_cmd = Command::new("make");
    make_cmd
        .current_dir(&minisat_build_dir)
        .arg("r")
        .arg(format!("-j{}", utils::num_jobs()))
        .env("BUILD_DIR", build_dir.join("minisat"))
        .env("CXXFLAGS", "-fpermissive -Wno-literal-suffix -std=c++98");

    // Run the `make` command
    utils::run_command(make_cmd, "Failed to build MiniSAT with make")?;

    // Verify the binary was created
    let bin_path = build_dir
        .join("minisat")
        .join("release")
        .join("bin")
        .join("minisat");
    utils::verify_binary_exists(&bin_path, "MiniSAT")?;

    // Set the environment variable for the MiniSAT binary path
    println!("cargo:rustc-env=MINISAT_BINARY_PATH={}", bin_path.display());

    // Return the path to the built binary
    Ok(bin_path)
}

#[cfg(feature = "glucose")]
fn build_glucose(build_dir: &Path) -> Result<PathBuf, String> {
    // Check if the Glucose source directory exists
    println!("cargo:rerun-if-changed={}", GLUCOSE_SOURCE);
    let glucose_source = Path::new(GLUCOSE_SOURCE);
    utils::verify_src_exists(glucose_source, "Glucose")?;

    // Start building the Glucose binary
    println!("Building Glucose SAT solver...");

    // Copy the source directory to the build directory
    let glucose_build_dir = utils::copy_src_dir(glucose_source, build_dir, "glucose")
        .map_err(|e| format!("Failed to copy Glucose source directory: {}", e))?;

    // Create the CMake build directory
    let cmake_build_dir = glucose_build_dir.join("build");
    fs::create_dir_all(&cmake_build_dir).expect("Failed to create CMake build directory");

    // Create the CMake configuration command
    let mut cmake_configure = Command::new("cmake");
    cmake_configure
        .current_dir(&cmake_build_dir)
        .arg("..")
        .arg("-DCMAKE_BUILD_TYPE=Release")
        .arg("-DBUILD_SHARED_LIBS=OFF")
        .arg("-DCMAKE_POLICY_VERSION_MINIMUM=3.5");

    // Run the CMake configuration command
    utils::run_command(cmake_configure, "Failed to configure Glucose with cmake")?;

    // Create the CMake build command
    let mut cmake_build = Command::new("cmake");
    cmake_build
        .current_dir(&cmake_build_dir)
        .arg("--build")
        .arg(".")
        .arg("--config")
        .arg("Release")
        .arg("--parallel")
        .arg(utils::num_jobs());

    // Run the CMake build command
    utils::run_command(cmake_build, "Failed to build Glucose with cmake")?;

    // Create paths for each possible binary
    let glucose_simp_binary = cmake_build_dir.join("glucose-simp");
    let glucose_parallel_binary = cmake_build_dir.join("glucose-syrup");

    // Prefer the simplified version as the primary binary
    let primary_binary = if glucose_simp_binary.exists() {
        &glucose_simp_binary
    } else if glucose_parallel_binary.exists() {
        &glucose_parallel_binary
    } else {
        return Err("No Glucose binary found".to_string());
    };

    // Verify the primary binary exists
    utils::verify_binary_exists(primary_binary, "Glucose")?;

    // Set the environment variable for the primary binary path
    println!(
        "cargo:rustc-env=GLUCOSE_BINARY_PATH={}",
        primary_binary.display()
    );

    // Set additional binary paths if they exist
    if glucose_simp_binary.exists() {
        println!(
            "cargo:rustc-env=GLUCOSE_SIMP_BINARY_PATH={}",
            glucose_simp_binary.display()
        );
    }

    if glucose_parallel_binary.exists() {
        println!(
            "cargo:rustc-env=GLUCOSE_SYRUP_BINARY_PATH={}",
            glucose_parallel_binary.display()
        );
    }

    // Return the path to the primary binary
    Ok(primary_binary.clone())
}

#[cfg(feature = "cadical")]
fn build_cadical(build_dir: &Path) -> Result<PathBuf, String> {
    // Check if the CaDiCaL source directory exists
    println!("cargo:rerun-if-changed={}", CADICAL_SOURCE);
    let cadical_source = Path::new(CADICAL_SOURCE);
    utils::verify_src_exists(cadical_source, "CaDiCaL")?;

    // Start building the CaDiCaL binary
    println!("Building CaDiCaL SAT solver...");

    // Copy the source directory to the build directory
    let cadical_build_dir = utils::copy_src_dir(cadical_source, build_dir, "cadical")
        .map_err(|e| format!("Failed to copy CaDiCaL source directory: {}", e))?;

    // Create the `./configure` command
    let mut configure_cmd = Command::new("./configure");
    configure_cmd
        .current_dir(&cadical_build_dir)
        .arg("--quiet")
        .arg("--no-contracts")
        .arg("--no-tracing");

    // Run the `./configure` command
    utils::run_command(configure_cmd, "Failed to configure CaDiCaL")?;

    // Create the `make` command
    let mut make_cmd = Command::new("make");
    make_cmd
        .current_dir(&cadical_build_dir)
        .arg("cadical")
        .arg(format!("-j{}", utils::num_jobs()));

    // Run the `make` command
    utils::run_command(make_cmd, "Failed to build CaDiCaL with make")?;

    // Verify the binary was created
    let built_binary = cadical_build_dir.join("build").join("cadical");
    utils::verify_binary_exists(&built_binary, "CaDiCaL")?;

    // Set the environment variable for the CaDiCaL binary path
    println!(
        "cargo:rustc-env=CADICAL_BINARY_PATH={}",
        built_binary.display()
    );

    // Also expose the library path if needed
    let built_library = cadical_build_dir.join("build").join("libcadical.a");
    if built_library.exists() {
        println!(
            "cargo:rustc-env=CADICAL_LIBRARY_PATH={}",
            built_library.display()
        );
    }

    // Return the path to the built binary
    Ok(built_binary)
}

#[cfg(feature = "lingeling")]
fn build_lingeling(build_dir: &Path) -> Result<PathBuf, String> {
    // Check if the Lingeling source directory exists
    println!("cargo:rerun-if-changed={}", LINGELING_SOURCE);
    let lingeling_source = Path::new(LINGELING_SOURCE);
    utils::verify_src_exists(lingeling_source, "Lingeling")?;

    // Start building the Lingeling binary
    println!("Building Lingeling SAT solver...");

    // Copy the source directory to the build directory
    let lingeling_build_dir = utils::copy_src_dir(lingeling_source, build_dir, "lingeling")
        .map_err(|e| format!("Failed to copy Lingeling source directory: {}", e))?;

    // Create the `./configure.sh` command
    let mut configure_cmd = Command::new("./configure.sh");
    configure_cmd
        .current_dir(&lingeling_build_dir)
        .arg("--no-aiger")
        .arg("--no-yalsat")
        .arg("--no-druplig");

    // Run the `./configure.sh` command
    utils::run_command(configure_cmd, "Failed to configure Lingeling")?;

    // Create the `make` command
    let mut make_cmd = Command::new("make");
    make_cmd
        .current_dir(&lingeling_build_dir)
        .arg("lingeling")
        .arg(format!("-j{}", utils::num_jobs()));

    // Run the `make` command
    utils::run_command(make_cmd, "Failed to build Lingeling with make")?;

    // Verify the binary was created
    let built_binary = lingeling_build_dir.join("lingeling");
    utils::verify_binary_exists(&built_binary, "Lingeling")?;

    // Set the environment variable for the Lingeling binary path
    println!(
        "cargo:rustc-env=LINGELING_BINARY_PATH={}",
        built_binary.display()
    );

    // Also expose the library path if needed
    let built_library = lingeling_build_dir.join("liblgl.a");
    if built_library.exists() {
        println!(
            "cargo:rustc-env=LINGELING_LIBRARY_PATH={}",
            built_library.display()
        );
    }

    // Return the path to the built binary
    Ok(built_binary)
}

#[cfg(feature = "kissat")]
fn build_kissat(build_dir: &Path) -> Result<PathBuf, String> {
    // Check if the Kissat source directory exists
    println!("cargo:rerun-if-changed={}", KISSAT_SOURCE);
    let kissat_source = Path::new(KISSAT_SOURCE);
    utils::verify_src_exists(kissat_source, "Kissat")?;

    // Start building the Kissat binary
    println!("Building Kissat SAT solver...");

    // Copy the source directory to the build directory
    let kissat_build_dir = utils::copy_src_dir(kissat_source, build_dir, "kissat")
        .map_err(|e| format!("Failed to copy Kissat source directory: {}", e))?;

    // Create the `configure` command
    let mut configure_cmd = Command::new("./configure");
    configure_cmd.current_dir(&kissat_build_dir).arg("--quiet");

    // Run the `configure` command
    utils::run_command(configure_cmd, "Failed to configure Kissat")?;

    println!("Configured Kissat successfully.");
    // Create the `make test` command
    let mut make_cmd = Command::new("make");
    make_cmd.current_dir(&kissat_build_dir).arg("test");

    // Run the `make test` command
    utils::run_command(make_cmd, "Failed to build Kissat with make")?;
    println!("Built Kissat successfully.");

    // Verify the binary was created
    let built_binary = kissat_build_dir.join("build/kissat");
    println!("Kissat binary expected at: {}", built_binary.display());
    utils::verify_binary_exists(&built_binary, "Kissat")?;
    println!("Verified Kissat binary exists.");

    // Set the environment variable for the Kissat binary path
    println!(
        "cargo:rustc-env=KISSAT_BINARY_PATH={}",
        built_binary.display()
    );

    // Return the path to the built binary
    Ok(built_binary)
}

#[cfg(any(
    feature = "minisat",
    feature = "glucose",
    feature = "cadical",
    feature = "lingeling",
    feature = "kissat",
))]
mod utils {
    use std::{env, fs, io, path, process};

    /// Recursively copies the source directory to the destination directory.
    pub fn copy_dir(src: &path::Path, dst: &path::Path) -> io::Result<()> {
        fs::create_dir_all(dst)?;

        for entry in fs::read_dir(src)? {
            let entry = entry?;
            let path = entry.path();
            let dest_path = dst.join(entry.file_name());

            if path.is_dir() {
                copy_dir(&path, &dest_path)?;
            } else if let Err(e) = fs::copy(&path, &dest_path) {
                println!(
                    "cargo:warning=Failed to copy {:?} to {:?}: {}",
                    path, dest_path, e
                );
            }
        }
        Ok(())
    }

    /// Copies the source directory to the build directory for the specified solver.
    pub fn copy_src_dir(
        src: &path::Path,
        build: &path::Path,
        solver: &str,
    ) -> Result<path::PathBuf, io::Error> {
        let solver_build_dir = build.join(solver);

        // Remove existing build directory if it exists
        if solver_build_dir.exists() {
            fs::remove_dir_all(&solver_build_dir)?;
        }

        // Copy source to build directory
        copy_dir(src, &solver_build_dir)?;

        Ok(solver_build_dir)
    }

    /// Runs a command and checks its output for success.
    #[cfg(any(
        feature = "minisat",
        feature = "glucose",
        feature = "cadical",
        feature = "lingeling",
        feature = "kissat"
    ))]
    pub fn run_command(mut cmd: process::Command, ctx: &str) -> Result<(), String> {
        let output = cmd
            .output()
            .map_err(|e| format!("Failed to execute command: {}", e))?;

        if !output.status.success() {
            let stderr = String::from_utf8_lossy(&output.stderr);
            Err(format!("{}: {}", ctx, stderr))
        } else {
            Ok(())
        }
    }

    #[cfg(any(
        feature = "minisat",
        feature = "glucose",
        feature = "cadical",
        feature = "lingeling",
        // not used in kissat build
    ))]
    /// Gets the number of jobs to use for building the solvers.
    pub fn num_jobs() -> String {
        use std::thread;

        // Try to get from CARGO_MAKEFLAGS or NUM_JOBS environment variable first
        if let Ok(makeflags) = env::var("CARGO_MAKEFLAGS")
            && let Some(jobs) = _find_jobs_flag(&makeflags)
        {
            return jobs;
        }

        if let Ok(num_jobs) = env::var("NUM_JOBS") {
            return num_jobs;
        }

        // Fall back to number of logical CPUs
        match thread::available_parallelism() {
            Ok(parallelism) => parallelism.get().to_string(),
            Err(_) => "4".to_string(), // Reasonable default
        }
    }

    /// Gets the cargo build target directory.
    pub fn build_dir() -> path::PathBuf {
        let out_dir = env::var("OUT_DIR").expect("OUT_DIR not set");
        println!("Building in: {}", out_dir);
        path::Path::new(&out_dir).into()
    }

    /// Verifies if the source path exists for the specified solver.
    #[cfg(any(
        feature = "minisat",
        feature = "glucose",
        feature = "cadical",
        feature = "lingeling",
        feature = "kissat"
    ))]
    pub fn verify_src_exists(path: &path::Path, solver: &str) -> Result<(), String> {
        if path.exists() {
            println!("{} source found at: {}", solver, path.display());
            Ok(())
        } else {
            Err(format!(
                "{} source not found at: {}",
                solver,
                path.display()
            ))
        }
    }

    /// Verifies if the binary exists at the specified path.
    #[cfg(any(
        feature = "minisat",
        feature = "glucose",
        feature = "cadical",
        feature = "lingeling",
        feature = "kissat"
    ))]
    pub fn verify_binary_exists(path: &path::Path, solver: &str) -> Result<(), String> {
        if path.exists() {
            println!("{} binary available at: {}", solver, path.display());
            Ok(())
        } else {
            Err(format!(
                "{} binary not found at: {}",
                solver,
                path.display()
            ))
        }
    }

    fn _find_jobs_flag(makeflags: &str) -> Option<String> {
        // Look for -j followed by a number in CARGO_MAKEFLAGS
        for part in makeflags.split_whitespace() {
            if let Some(jobs_str) = part.strip_prefix("-j")
                && !jobs_str.is_empty()
                && jobs_str.chars().all(|c| c.is_ascii_digit())
            {
                return Some(jobs_str.to_string());
            }
        }
        None
    }
}