import { spawn } from "node:child_process";
export function runCryptoMiniSat({ binaryPath, cnfPath, proofPath, timeoutMs = 60_000 }) {
    return new Promise((resolve, reject) => {
        const args = proofPath ? ["--verb", "0", cnfPath, proofPath] : ["--verb", "0", cnfPath];
        const child = spawn(binaryPath, args, {
            windowsHide: true
        });
        let stdout = "";
        let stderr = "";
        let settled = false;
        const timer = setTimeout(() => {
            if (settled) {
                return;
            }
            settled = true;
            child.kill();
            reject(new Error(`CryptoMiniSat timed out after ${timeoutMs}ms.`));
        }, timeoutMs);
        child.stdout.on("data", (chunk) => {
            stdout += chunk.toString();
        });
        child.stderr.on("data", (chunk) => {
            stderr += chunk.toString();
        });
        child.on("error", (err) => {
            if (settled) {
                return;
            }
            settled = true;
            clearTimeout(timer);
            reject(err);
        });
        child.on("close", (exitCode) => {
            if (settled) {
                return;
            }
            settled = true;
            clearTimeout(timer);
            const output = `${stdout}\n${stderr}`;
            const status = /\bs\s+SATISFIABLE\b|\bSATISFIABLE\b/.test(output)
                ? "SAT"
                : /\bs\s+UNSATISFIABLE\b|\bUNSATISFIABLE\b/.test(output)
                    ? "UNSAT"
                    : "UNKNOWN";
            resolve({ status, stdout, stderr, exitCode });
        });
    });
}
export function extractSatAssignment(result, variables) {
    const literals = [];
    const seen = new Set();
    const output = `${result.stdout}\n${result.stderr}`;
    for (const rawLine of output.split(/\r?\n/)) {
        const line = rawLine.trim();
        if (!line.startsWith("v")) {
            continue;
        }
        for (const token of line.slice(1).trim().split(/\s+/)) {
            if (!token || !/^-?\d+$/.test(token)) {
                continue;
            }
            const literal = Number(token);
            if (literal === 0) {
                continue;
            }
            const variable = Math.abs(literal);
            if (variable < 1 || variable > variables || seen.has(variable)) {
                continue;
            }
            seen.add(variable);
            literals.push(literal);
        }
    }
    if (literals.length === 0) {
        throw new Error("CryptoMiniSat returned SAT but did not print a model line.");
    }
    return literals.sort((left, right) => Math.abs(left) - Math.abs(right));
}
