import { spawn } from "node:child_process";

export interface CryptoMiniSatResult {
  status: "SAT" | "UNSAT" | "UNKNOWN";
  stdout: string;
  stderr: string;
  exitCode: number | null;
}

export function runCryptoMiniSat({
  binaryPath,
  cnfPath,
  proofPath,
  timeoutMs = 60_000
}: {
  binaryPath: string;
  cnfPath: string;
  proofPath?: string;
  timeoutMs?: number;
}): Promise<CryptoMiniSatResult> {
  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: CryptoMiniSatResult, variables: number) {
  const literals: number[] = [];
  const seen = new Set<number>();
  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));
}
