import { readFile } from "node:fs/promises";

export interface ParsedCnf {
  variables: number;
  clauses: number[][];
}

export interface AssignmentCheck {
  ok: boolean;
  assignment: Map<number, boolean>;
  reason?: string;
}

export function parseDimacsCnfText(input: string): ParsedCnf {
  const clauses: number[][] = [];
  let declaredVariables = 0;
  let currentClause: number[] = [];

  for (const rawLine of input.split(/\r?\n/)) {
    const line = rawLine.trim();
    if (!line || line.startsWith("c")) {
      continue;
    }
    if (line.startsWith("%")) {
      break;
    }
    if (line.startsWith("p")) {
      const parts = line.split(/\s+/);
      if (parts.length < 4 || parts[1]?.toLowerCase() !== "cnf") {
        throw new Error("DIMACS header must be p cnf <variables> <clauses>.");
      }
      declaredVariables = Number(parts[2]);
      if (!Number.isInteger(declaredVariables) || declaredVariables <= 0) {
        throw new Error("DIMACS variable count is invalid.");
      }
      continue;
    }

    for (const token of line.split(/\s+/)) {
      if (!/^-?\d+$/.test(token)) {
        throw new Error(`Invalid DIMACS token: ${token}`);
      }
      const literal = Number(token);
      if (literal === 0) {
        if (currentClause.length > 0) {
          clauses.push(currentClause);
          currentClause = [];
        }
      } else {
        currentClause.push(literal);
      }
    }
  }

  if (currentClause.length > 0) {
    clauses.push(currentClause);
  }
  if (clauses.length === 0) {
    throw new Error("DIMACS file contains no clauses.");
  }

  const maxVariable = Math.max(...clauses.flat().map((literal) => Math.abs(literal)));
  return {
    variables: Math.max(declaredVariables, maxVariable),
    clauses
  };
}

export async function parseDimacsCnfFile(filePath: string) {
  return parseDimacsCnfText(await readFile(filePath, "utf8"));
}

export function parseUnitClauseAssignment(solution: ParsedCnf): AssignmentCheck {
  const assignment = new Map<number, boolean>();
  for (const clause of solution.clauses) {
    if (clause.length !== 1) {
      return {
        ok: false,
        assignment,
        reason: "Solution CNF must contain only unit clauses in MVP assignment mode."
      };
    }
    const literal = clause[0];
    const variable = Math.abs(literal);
    const value = literal > 0;
    const previous = assignment.get(variable);
    if (previous !== undefined && previous !== value) {
      return {
        ok: false,
        assignment,
        reason: `Conflicting assignment for variable ${variable}.`
      };
    }
    assignment.set(variable, value);
  }
  return { ok: true, assignment };
}

export function assignmentSatisfies(instance: ParsedCnf, assignment: Map<number, boolean>) {
  for (let index = 0; index < instance.clauses.length; index += 1) {
    const clause = instance.clauses[index];
    const satisfied = clause.some((literal) => {
      const value = assignment.get(Math.abs(literal));
      return value !== undefined && (literal > 0 ? value : !value);
    });
    if (!satisfied) {
      return {
        ok: false,
        reason: `Instance clause ${index + 1} is not satisfied by the submitted assignment.`
      };
    }
  }
  return { ok: true };
}

export function dimacsCnfText(instance: ParsedCnf) {
  const lines = [
    `p cnf ${instance.variables} ${instance.clauses.length}`,
    ...instance.clauses.map((clause) => `${clause.join(" ")} 0`)
  ];
  return `${lines.join("\n")}\n`;
}
export function assignmentFromLiterals(literals: number[]) {
  const assignment = new Map<number, boolean>();
  for (const literal of literals) {
    const variable = Math.abs(literal);
    const value = literal > 0;
    const previous = assignment.get(variable);
    if (previous !== undefined && previous !== value) {
      throw new Error(`Conflicting solver model for variable ${variable}.`);
    }
    assignment.set(variable, value);
  }
  return assignment;
}

export function unitClauseCnfText(variables: number, literals: number[]) {
  const lines = [
    "c 3SAT Network MVP solution artifact",
    "c This file is a unit-CNF assignment generated by the solver client.",
    `p cnf ${variables} ${literals.length}`,
    ...literals.map((literal) => `${literal} 0`)
  ];
  return `${lines.join("\n")}\n`;
}
