/**
 * Builtin image `tfp-builtin/sat-assignment-check:1` — the `assignment_check`
 * stage of the @tfp/sat-assignment Contract (schemas/examples/
 * verifier-contract.sat.json).
 *
 * Contract semantics (statement_md): verified when the submitted
 * assignment, parsed as SAT-competition v-line format, assigns every
 * variable of the bound CNF instance and satisfies all of its clauses;
 * assignments mentioning variables outside the instance are rejected
 * (refuted). A file that cannot be parsed at all is inconclusive.
 *
 * Runs only against the fixed filesystem: /input/manifest.json,
 * /input/reference/instance/<file>, /input/artifacts/assignment/<file>;
 * writes /output/result.json and /output/evidence/summary.json.
 */

import type { SandboxFs } from '../sandbox.js';
import type { RunManifest } from '../../contracts.js';

export const SAT_IMAGE_REF = 'tfp-builtin/sat-assignment-check:1';

/** Work bounds: the instance slot is ≤10 MiB, so anything past these is not a real instance but a CPU attack. */
const MAX_VARS = 5_000_000;
const MAX_CLAUSES = 5_000_000;
interface Cnf { numVars: number; clauses: number[][] }

function parseDimacs(text: string): Cnf | string {
  let numVars = -1; let declared = -1;
  const clauses: number[][] = [];
  let current: number[] = [];
  for (const raw of text.split('\n')) {
    const line = raw.trim();
    if (!line || line.startsWith('c') || line.startsWith('%')) continue;
    if (line.startsWith('p')) {
      const m = line.match(/^p\s+cnf\s+(\d+)\s+(\d+)$/);
      if (!m) return `bad problem line: ${line.slice(0, 40)}`;
      numVars = Number(m[1]); declared = Number(m[2]);
      if (numVars > MAX_VARS || declared > MAX_CLAUSES) return `instance too large (limit ${MAX_VARS} variables, ${MAX_CLAUSES} clauses)`;
      continue;
    }
    for (const tok of line.split(/\s+/)) {
      if (!/^-?\d+$/.test(tok)) return `bad literal token: ${tok.slice(0, 20)}`;
      const lit = Number(tok);
      if (lit === 0) { clauses.push(current); current = []; } else current.push(lit);
    }
  }
  if (current.length) clauses.push(current);
  if (numVars < 0) return 'missing p cnf header';
  if (declared !== clauses.length) return `header declares ${declared} clauses; found ${clauses.length}`;
  for (const c of clauses) for (const l of c) if (Math.abs(l) > numVars) return `clause literal ${l} exceeds declared variable count ${numVars}`;
  return { numVars, clauses };
}

type Parsed = { ok: true; values: Map<number, boolean> } | { ok: false; malformed: string };

/** SAT-competition v-lines: `v` prefixed or bare, space-separated signed ints, terminated by 0. */
function parseAssignment(text: string): Parsed {
  const values = new Map<number, boolean>();
  let terminated = false;
  let sawLiteral = false;
  if (text.length > 4 * 1024 * 1024) return { ok: false, malformed: 'assignment text too large' };
  for (const raw of text.split('\n')) {
    let line = raw.trim();
    if (!line || line.startsWith('c') || line.startsWith('s ')) continue;
    if (line === 's SATISFIABLE') continue;
    if (/^v(\s|$)/.test(line)) line = line.slice(1).trim();
    if (terminated && line) return { ok: false, malformed: 'content after the terminating 0' };
    for (const tok of line.split(/\s+/)) {
      if (!tok) continue;
      if (!/^-?\d+$/.test(tok)) return { ok: false, malformed: `not a literal: ${tok.slice(0, 20)}` };
      const lit = Number(tok);
      if (!Number.isSafeInteger(lit)) return { ok: false, malformed: `literal out of range: ${tok.slice(0, 20)}` };
      if (lit === 0) { terminated = true; continue; }
      if (terminated) return { ok: false, malformed: 'literal after the terminating 0' };
      const v = Math.abs(lit);
      if (values.has(v) && values.get(v) !== lit > 0) return { ok: false, malformed: `variable ${v} assigned both polarities` };
      values.set(v, lit > 0);
      sawLiteral = true;
    }
  }
  if (!sawLiteral) return { ok: false, malformed: 'no literals found' };
  if (!terminated) return { ok: false, malformed: 'missing terminating 0' };
  return { ok: true, values };
}

const onlyFile = (fs: SandboxFs, dir: string): string | null => {
  const files = fs.list(dir);
  return files.length === 1 ? files[0]! : null;
};

export async function satAssignmentCheck(fs: SandboxFs): Promise<number> {
  const manifest = JSON.parse(fs.readText('/input/manifest.json')) as RunManifest;
  const finish = (result: 'verified' | 'refuted' | 'inconclusive', reason: string, evidence: Record<string, unknown>) => {
    fs.writeFile('/output/evidence/summary.json', JSON.stringify({ clauses_total: 0, clauses_satisfied: 0, ...evidence }));
    fs.writeFile('/output/result.json', JSON.stringify({ result, reason }));
    fs.log(`${result}: ${reason}`);
    return 0;
  };
  const instanceEntry = manifest.reference.find((r) => r.key === 'instance');
  const instancePath = instanceEntry?.path ?? onlyFile(fs, '/input/reference/instance');
  if (!instancePath) return finish('inconclusive', 'no bound instance', {});
  let cnfText: string;
  try { cnfText = fs.readText(instancePath); } catch { return finish('inconclusive', 'instance is not UTF-8 text', {}); }
  const cnf = parseDimacs(cnfText);
  if (typeof cnf === 'string') return finish('inconclusive', `instance is not valid DIMACS: ${cnf}`, {});
  fs.log(`instance: ${cnf.numVars} variables, ${cnf.clauses.length} clauses`);

  const assignmentEntry = manifest.artifacts.find((a) => a.role === 'assignment');
  const assignmentPath = assignmentEntry?.path ?? onlyFile(fs, '/input/artifacts/assignment');
  if (!assignmentPath) return finish('inconclusive', 'no assignment artifact', { clauses_total: cnf.clauses.length });
  let text: string;
  try { text = fs.readText(assignmentPath); } catch { return finish('inconclusive', 'assignment is not UTF-8 text', { clauses_total: cnf.clauses.length }); }
  const parsed = parseAssignment(text);
  if (!parsed.ok) return finish('inconclusive', `assignment could not be parsed as v-lines: ${parsed.malformed}`, { clauses_total: cnf.clauses.length });

  const outOfRange = [...parsed.values.keys()].filter((v) => v > cnf.numVars);
  if (outOfRange.length) {
    return finish('refuted', `assignment names ${outOfRange.length} variable(s) outside the instance (first: ${outOfRange[0]})`,
      { clauses_total: cnf.clauses.length, variables_total: cnf.numVars, variables_assigned: parsed.values.size, out_of_range_variables: outOfRange.length });
  }
  const missing: number[] = [];
  for (let v = 1; v <= cnf.numVars; v++) if (!parsed.values.has(v)) missing.push(v);
  let satisfied = 0;
  let firstFalse = -1;
  cnf.clauses.forEach((clause, i) => {
    const ok = clause.some((l) => parsed.values.get(Math.abs(l)) === l > 0);
    if (ok) satisfied += 1; else if (firstFalse < 0) firstFalse = i;
  });
  const evidence = { clauses_total: cnf.clauses.length, clauses_satisfied: satisfied, variables_total: cnf.numVars, variables_assigned: parsed.values.size, unassigned_variables: missing.length };
  if (missing.length) return finish('refuted', `assignment leaves ${missing.length} variable(s) unassigned (first: ${missing[0]})`, evidence);
  if (satisfied !== cnf.clauses.length) return finish('refuted', `clause ${firstFalse + 1} is not satisfied (${satisfied}/${cnf.clauses.length} satisfied)`, evidence);
  return finish('verified', `${satisfied}/${cnf.clauses.length} clauses satisfied by a complete assignment`, evidence);
}