import { readFile } from "node:fs/promises";
export function parseDimacsCnfText(input) {
    const clauses = [];
    let declaredVariables = 0;
    let currentClause = [];
    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) {
    return parseDimacsCnfText(await readFile(filePath, "utf8"));
}
export function parseUnitClauseAssignment(solution) {
    const assignment = new Map();
    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, assignment) {
    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) {
    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) {
    const assignment = new Map();
    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, literals) {
    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`;
}
