/**
 * Deterministic first-order logic evaluation engine.
 *
 * Evaluates Imhotep logic formulas exhaustively over a finite geometry
 * world.  The engine supports:
 *
 *   - Universal quantification (forall) with short-circuit on first failure
 *   - Existential quantification (exists) with short-circuit on first success
 *   - Boolean connectives: And, Or, Not, Implies
 *   - Predicate calls against a registered predicate registry
 *
 * Invariants:
 *   1. Closed-world semantics: every domain is finite and enumerated.
 *   2. No silent defaults: missing facts produce indeterminate results.
 *   3. Rich diagnostics: every failing assignment is reported with proof ids
 *      and trace events.
 *   4. Deterministic vs sampled is explicit in the result mode.
 */

import { performance } from 'node:perf_hooks';
import type { DiagnosticCode } from 'imhotep-core'
import type {
  GeometryWorld,
  Proof,
  Witness,
  Diagnostic,
  TraceEvent,
} from './registry.js';

import type {
  PredicateEvaluator,
  PredicateResult,
  PredicateTruth,
} from './predicates.js';

import {
  getPredicateEvaluator,
  registerDefaultPredicates,
  PredicateRegistry,
  globalPredicateRegistry,
} from './predicates.js';

import {
  BindingEnv,
  type BindingEntry,
  type TupleBindingSpec,
  enumerateTuples,
  tupleToBindings,
} from './bindings.js';

import {
  createCartesianIterator,
  type JoinSpec,
} from './joins.js';

import type {
  FormulaNode,
  ForAllFormula,
  ExistsFormula,
  AndFormula,
  OrFormula,
  NotFormula,
  ImpliesFormula,
  PredicateCall,
  DomainRef,
  DomainValue,
} from 'imhotep-core';

// ---------------------------------------------------------------------------
// Evaluation Result Contract
// ---------------------------------------------------------------------------

export type EvaluationMode = 'scene-determinate' | 'scene-indeterminate';

export interface DeterministicSceneEvaluation {
  mode: EvaluationMode;
  sceneId: string;
  passed: boolean;
  formulaResults: FormulaResult[];
  proofs: Proof[];
  diagnostics: Diagnostic[];
  trace: TraceEvent[];
  /** Failing variable assignments for diagnostics. */
  failingAssignments?: Record<string, number>[];
}

export interface FormulaResult {
  formulaId: string;
  outcome: 'pass' | 'fail' | 'indeterminate';
  truth: 'determinate' | 'indeterminate';
  witness?: number[];
  metrics?: Record<string, number>;
}

// ---------------------------------------------------------------------------
// Domain Resolver
// ---------------------------------------------------------------------------

export interface DomainResolver {
  resolve(domain: DomainRef, env?: BindingEnv): DomainValue | undefined;
}

// ---------------------------------------------------------------------------
// Engine Options
// ---------------------------------------------------------------------------

export interface LogicEngineOptions {
  skipMissingPredicates?: boolean;
  maxDiagnostics?: number;
  predicateRegistry?: PredicateRegistry;
  /** Enable detailed trace logging. Default true. Disable for production speed. */
  trace?: boolean;
}

// ---------------------------------------------------------------------------
// Internal Evaluation State
// ---------------------------------------------------------------------------

interface EvalState {
  world: GeometryWorld;
  resolver: DomainResolver;
  options: LogicEngineOptions;
  diagnostics: Diagnostic[];
  trace: TraceEvent[];
  proofs: Proof[];
  proofCounter: number;
  formulaCounter: number;
  predicateRegistry: PredicateRegistry;
}

// ---------------------------------------------------------------------------
// Proof Generation
// ---------------------------------------------------------------------------

function nextProofId(state: EvalState): string {
  return `proof_${++state.proofCounter}`;
}

function nextFormulaId(state: EvalState): string {
  return `formula_${++state.formulaCounter}`;
}

function makeProof(
  state: EvalState,
  formulaId: string,
  outcome: 'pass' | 'fail' | 'indeterminate',
  truth: 'determinate' | 'indeterminate',
  witness?: number[],
  usedFacts: number[] = [],
): Proof {
  // Map indeterminate outcome to 'error' for ClauseStatus compatibility.
  const clauseOutcome = outcome === 'indeterminate' ? 'error' : outcome;
  return {
    proofId: nextProofId(state),
    clauseId: formulaId,
    outcome: clauseOutcome,
    truth,
    usedFacts,
    derivedFacts: [],
    witness: witness
      ? {
          subjectId: witness[0],
          referenceId: witness[1],
          snapshotId: state.world.snapshotId,
        }
      : undefined,
  };
}

function addTrace(
  state: EvalState,
  phase: string,
  clauseId?: string,
  payload?: Record<string, unknown>,
): void {
  if (state.options.trace === false) return;
  state.trace.push({
    traceEventId: `trace_${state.trace.length}`,
    phase,
    at: performance.now(),
    refs: clauseId ? { clauseId } : {},
    payload: payload ?? {},
  });
}

function addDiagnostic(
  state: EvalState,
  code: DiagnosticCode,
  severity: 'error' | 'warning' | 'info',
  message: string,
  clauseId?: string,
): void {
  const max = state.options.maxDiagnostics ?? 100;
  if (state.diagnostics.length >= max) {
    return;
  }
  state.diagnostics.push({
    code,
    severity,
    category: severity === 'error' ? 'contract-failure' : 'internal-error',
    message,
    clauseId,
  });
}

// ---------------------------------------------------------------------------
// Formula Evaluation
// ---------------------------------------------------------------------------

function evaluateFormula(
  formula: FormulaNode,
  env: BindingEnv,
  state: EvalState,
): FormulaResult {
  const formulaId = nextFormulaId(state);
  if (state.options.trace !== false) {
    addTrace(state, 'evaluate-formula', formulaId, {
      kind: formula.kind,
      bindings: env.toObject(),
    });
  }

  switch (formula.kind) {
    case 'forall':
      return evaluateForAll(formula as ForAllFormula, env, state, formulaId);
    case 'exists':
      return evaluateExists(formula as ExistsFormula, env, state, formulaId);
    case 'and':
      return evaluateAnd(formula as AndFormula, env, state, formulaId);
    case 'or':
      return evaluateOr(formula as OrFormula, env, state, formulaId);
    case 'not':
      return evaluateNot(formula as NotFormula, env, state, formulaId);
    case 'implies':
      return evaluateImplies(formula as ImpliesFormula, env, state, formulaId);
    case 'predicate':
      return evaluatePredicate(formula as PredicateCall, env, state, formulaId);
    default:
      addDiagnostic(
        state,
        'IMH_LOGIC_UNKNOWN_FORMULA_KIND',
        'error',
        `Unknown formula kind: ${(formula as FormulaNode).kind}`,
        formulaId,
      );
      return {
        formulaId,
        outcome: 'indeterminate',
        truth: 'indeterminate',
      };
  }
}

function evaluateForAll(
  formula: ForAllFormula,
  env: BindingEnv,
  state: EvalState,
  formulaId: string,
): FormulaResult {
  addTrace(state, 'evaluate-forall-start', formulaId);

  // Resolve domains and build join specs.
  const specs: JoinSpec[] = [];
  for (const binding of formula.bindings) {
    const domain = state.resolver.resolve(binding.domain, env);
    if (!domain) {
      addDiagnostic(
        state,
        'IMH_LOGIC_DOMAIN_UNRESOLVED',
        'error',
        `Domain ${binding.domain.domain} could not be resolved.`,
        formulaId,
      );
      const result: FormulaResult = {
        formulaId,
        outcome: 'indeterminate',
        truth: 'indeterminate',
      };
      state.proofs.push(makeProof(state, formulaId, 'indeterminate', 'indeterminate'));
      return result;
    }

    if (domain.subjectIds.length === 0) {
      // Empty domain: forall over empty set is vacuously true.
      // When ANY quantified variable has an empty domain, the entire
      // universal quantification is vacuously true (no tuples to check).
      addDiagnostic(
        state,
        'IMH_LOGIC_VACUOUS_FORALL',
        'info',
        `Forall over empty domain "${binding.domain.domain}" (selector: ${binding.domain.selector ?? 'none'}) is vacuously true.`,
        formulaId,
      );
      addTrace(state, 'evaluate-forall-empty-domain', formulaId, {
        domainId: domain.domainId,
      });
      const result: FormulaResult = {
        formulaId,
        outcome: 'pass',
        truth: 'determinate',
      };
      state.proofs.push(makeProof(state, formulaId, 'pass', 'determinate'));
      addTrace(state, 'evaluate-forall-vacuous', formulaId);
      return result;
    }

    for (const varName of binding.variables) {
      specs.push({
        variableName: varName,
        domain,
      });
    }
  }

  if (specs.length === 0) {
    // No variables or all domains empty: vacuously true.
    const result: FormulaResult = {
      formulaId,
      outcome: 'pass',
      truth: 'determinate',
    };
    state.proofs.push(makeProof(state, formulaId, 'pass', 'determinate'));
    addTrace(state, 'evaluate-forall-vacuous', formulaId);
    return result;
  }

  // Enumerate all tuples exhaustively.
  const iterator = createCartesianIterator(specs);
  let failed = false;
  let indeterminate = false;
  let failingTuple: Record<string, number> | undefined;
  let failingMetrics: Record<string, number> | undefined;

  iterator.forEach((tuple, indices) => {
    // Build extended environment.
    const entries: BindingEntry[] = [];
    for (let i = 0; i < specs.length; i++) {
      entries.push({
        variableName: specs[i].variableName,
        subjectId: tuple[i],
      });
    }
    const childEnv = env.bindTuple(entries);

    const bodyResult = evaluateFormula(formula.body, childEnv, state);

    if (bodyResult.outcome === 'indeterminate') {
      indeterminate = true;
      addTrace(state, 'evaluate-forall-indeterminate', formulaId, {
        tuple: Object.fromEntries(specs.map((s, i) => [s.variableName, tuple[i]])),
        bodyOutcome: bodyResult.outcome,
      });
      return false; // Short-circuit.
    }

    if (bodyResult.outcome === 'fail') {
      failed = true;
      failingTuple = {};
      failingMetrics = bodyResult.metrics;
      for (let i = 0; i < specs.length; i++) {
        failingTuple[specs[i].variableName] = tuple[i];
      }
      addTrace(state, 'evaluate-forall-failure', formulaId, {
        failingTuple,
        bodyOutcome: bodyResult.outcome,
      });
      return false; // Short-circuit.
    }

    return true;
  });

  let outcome: 'pass' | 'fail' | 'indeterminate';
  if (indeterminate) {
    outcome = 'indeterminate';
  } else if (failed) {
    outcome = 'fail';
  } else {
    outcome = 'pass';
  }

  const result: FormulaResult = {
    formulaId,
    outcome,
    truth: outcome === 'indeterminate' ? 'indeterminate' : 'determinate',
    metrics: failingMetrics,
  };

  state.proofs.push(makeProof(state, formulaId, outcome, 'determinate'));
  addTrace(state, 'evaluate-forall-end', formulaId, { outcome });

  return result;
}

function evaluateExists(
  formula: ExistsFormula,
  env: BindingEnv,
  state: EvalState,
  formulaId: string,
): FormulaResult {
  addTrace(state, 'evaluate-exists-start', formulaId);

  // Resolve domains and build join specs.
  const specs: JoinSpec[] = [];
  for (const binding of formula.bindings) {
    const domain = state.resolver.resolve(binding.domain, env);
    if (!domain) {
      addDiagnostic(
        state,
        'IMH_LOGIC_DOMAIN_UNRESOLVED',
        'error',
        `Domain ${binding.domain.domain} could not be resolved.`,
        formulaId,
      );
      const result: FormulaResult = {
        formulaId,
        outcome: 'indeterminate',
        truth: 'indeterminate',
      };
      state.proofs.push(makeProof(state, formulaId, 'indeterminate', 'indeterminate'));
      return result;
    }

    if (domain.subjectIds.length === 0) {
      // Empty domain: exists over empty set is false.
      // When ANY quantified variable has an empty domain, the entire
      // existential quantification is false (no witness possible).
      addDiagnostic(
        state,
        'IMH_LOGIC_EMPTY_DOMAIN_EXISTS',
        'info',
        `Exists over empty domain "${binding.domain.domain}" (selector: ${binding.domain.selector ?? 'none'}) is false.`,
        formulaId,
      );
      const result: FormulaResult = {
        formulaId,
        outcome: 'fail',
        truth: 'determinate',
      };
      state.proofs.push(makeProof(state, formulaId, 'fail', 'determinate'));
      addTrace(state, 'evaluate-exists-empty', formulaId);
      return result;
    }

    for (const varName of binding.variables) {
      specs.push({
        variableName: varName,
        domain,
      });
    }
  }

  if (specs.length === 0) {
    // No variables or all domains empty: exists is false.
    const result: FormulaResult = {
      formulaId,
      outcome: 'fail',
      truth: 'determinate',
    };
    state.proofs.push(makeProof(state, formulaId, 'fail', 'determinate'));
    addTrace(state, 'evaluate-exists-empty', formulaId);
    return result;
  }

  // Enumerate tuples looking for a witness.
  const iterator = createCartesianIterator(specs);
  let found = false;
  let indeterminate = false;
  let witnessTuple: Record<string, number> | undefined;

  iterator.forEach((tuple, indices) => {
    const entries: BindingEntry[] = [];
    for (let i = 0; i < specs.length; i++) {
      entries.push({
        variableName: specs[i].variableName,
        subjectId: tuple[i],
      });
    }
    const childEnv = env.bindTuple(entries);

    const bodyResult = evaluateFormula(formula.body, childEnv, state);

    if (bodyResult.outcome === 'pass') {
      found = true;
      witnessTuple = {};
      for (let i = 0; i < specs.length; i++) {
        witnessTuple[specs[i].variableName] = tuple[i];
      }
      addTrace(state, 'evaluate-exists-witness', formulaId, {
        witnessTuple,
      });
      return false; // Short-circuit.
    }

    if (bodyResult.outcome === 'indeterminate') {
      indeterminate = true;
    }

    return true;
  });

  let outcome: 'pass' | 'fail' | 'indeterminate';
  if (found) {
    outcome = 'pass';
  } else if (indeterminate) {
    outcome = 'indeterminate';
  } else {
    outcome = 'fail';
  }

  const result: FormulaResult = {
    formulaId,
    outcome,
    truth: outcome === 'indeterminate' ? 'indeterminate' : 'determinate',
    witness: witnessTuple
      ? Object.values(witnessTuple)
      : undefined,
  };

  state.proofs.push(makeProof(state, formulaId, outcome, 'determinate', result.witness));
  addTrace(state, 'evaluate-exists-end', formulaId, { outcome });

  return result;
}

function evaluateAnd(
  formula: AndFormula,
  env: BindingEnv,
  state: EvalState,
  formulaId: string,
): FormulaResult {
  addTrace(state, 'evaluate-and-start', formulaId);

  const leftResult = evaluateFormula(formula.left, env, state);
  if (leftResult.outcome === 'indeterminate') {
    const result: FormulaResult = {
      formulaId,
      outcome: 'indeterminate',
      truth: 'indeterminate',
    };
    state.proofs.push(makeProof(state, formulaId, 'indeterminate', 'indeterminate'));
    addTrace(state, 'evaluate-and-short-circuit', formulaId, { side: 'left', reason: 'indeterminate' });
    return result;
  }

  if (leftResult.outcome === 'fail') {
    const result: FormulaResult = {
      formulaId,
      outcome: 'fail',
      truth: 'determinate',
      metrics: leftResult.metrics,
    };
    state.proofs.push(makeProof(state, formulaId, 'fail', 'determinate'));
    addTrace(state, 'evaluate-and-short-circuit', formulaId, { side: 'left', reason: 'fail' });
    return result;
  }

  const rightResult = evaluateFormula(formula.right, env, state);
  let outcome: 'pass' | 'fail' | 'indeterminate';
  let truth: 'determinate' | 'indeterminate';
  let metrics: Record<string, number> | undefined;

  if (rightResult.outcome === 'pass') {
    outcome = 'pass';
    truth = 'determinate';
  } else if (rightResult.outcome === 'indeterminate') {
    outcome = 'indeterminate';
    truth = 'indeterminate';
    metrics = rightResult.metrics;
  } else {
    outcome = 'fail';
    truth = 'determinate';
    metrics = rightResult.metrics;
  }

  const result: FormulaResult = {
    formulaId,
    outcome,
    truth,
    metrics,
  };
  state.proofs.push(makeProof(state, formulaId, result.outcome, result.truth));
  addTrace(state, 'evaluate-and-end', formulaId, { outcome });
  return result;
}

function evaluateOr(
  formula: OrFormula,
  env: BindingEnv,
  state: EvalState,
  formulaId: string,
): FormulaResult {
  addTrace(state, 'evaluate-or-start', formulaId);

  const leftResult = evaluateFormula(formula.left, env, state);
  if (leftResult.outcome === 'pass') {
    const result: FormulaResult = {
      formulaId,
      outcome: 'pass',
      truth: 'determinate',
      metrics: leftResult.metrics,
    };
    state.proofs.push(makeProof(state, formulaId, 'pass', 'determinate'));
    addTrace(state, 'evaluate-or-short-circuit', formulaId, { side: 'left', reason: 'pass' });
    return result;
  }

  const rightResult = evaluateFormula(formula.right, env, state);
  let outcome: 'pass' | 'fail' | 'indeterminate';
  let truth: 'determinate' | 'indeterminate';
  let metrics: Record<string, number> | undefined;

  if (rightResult.outcome === 'pass') {
    outcome = 'pass';
    truth = 'determinate';
    metrics = rightResult.metrics;
  } else if (leftResult.outcome === 'indeterminate' || rightResult.outcome === 'indeterminate') {
    outcome = 'indeterminate';
    truth = 'indeterminate';
    metrics = rightResult.metrics ?? leftResult.metrics;
  } else {
    outcome = 'fail';
    truth = 'determinate';
    metrics = { ...leftResult.metrics, ...rightResult.metrics };
  }

  const result: FormulaResult = {
    formulaId,
    outcome,
    truth,
    metrics,
  };
  state.proofs.push(makeProof(state, formulaId, result.outcome, result.truth));
  addTrace(state, 'evaluate-or-end', formulaId, { outcome });
  return result;
}

function evaluateNot(
  formula: NotFormula,
  env: BindingEnv,
  state: EvalState,
  formulaId: string,
): FormulaResult {
  addTrace(state, 'evaluate-not-start', formulaId);

  // Capture diagnostic count before evaluating operand so we can
  // suppress inner diagnostics when the not inverts a failure into a pass.
  const diagnosticCountBefore = state.diagnostics.length;

  const operandResult = evaluateFormula(formula.operand, env, state);
  let outcome: 'pass' | 'fail' | 'indeterminate';
  let truth: 'determinate' | 'indeterminate';
  let metrics: Record<string, number> | undefined;

  if (operandResult.outcome === 'pass') {
    outcome = 'fail';
    truth = 'determinate';
    metrics = operandResult.metrics;
  } else if (operandResult.outcome === 'fail') {
    outcome = 'pass';
    truth = 'determinate';
    // The inner predicate failed, but not() inverts it to a pass.
    // Remove diagnostics produced by the inner evaluation since they
    // describe a condition that the user explicitly negated.
    state.diagnostics.splice(diagnosticCountBefore, state.diagnostics.length - diagnosticCountBefore);
  } else {
    outcome = 'indeterminate';
    truth = 'indeterminate';
    metrics = operandResult.metrics;
  }

  const result: FormulaResult = {
    formulaId,
    outcome,
    truth,
    metrics,
  };

  state.proofs.push(makeProof(state, formulaId, result.outcome, result.truth));
  addTrace(state, 'evaluate-not-end', formulaId, { outcome });
  return result;
}

function evaluateImplies(
  formula: ImpliesFormula,
  env: BindingEnv,
  state: EvalState,
  formulaId: string,
): FormulaResult {
  addTrace(state, 'evaluate-implies-start', formulaId);

  const antecedentResult = evaluateFormula(formula.antecedent, env, state);
  if (antecedentResult.outcome === 'indeterminate') {
    const result: FormulaResult = {
      formulaId,
      outcome: 'indeterminate',
      truth: 'indeterminate',
    };
    state.proofs.push(makeProof(state, formulaId, 'indeterminate', 'indeterminate'));
    addTrace(state, 'evaluate-implies-indeterminate', formulaId, { reason: 'antecedent' });
    return result;
  }

  if (antecedentResult.outcome === 'fail') {
    // Vacuously true.
    const result: FormulaResult = {
      formulaId,
      outcome: 'pass',
      truth: 'determinate',
    };
    state.proofs.push(makeProof(state, formulaId, 'pass', 'determinate'));
    addTrace(state, 'evaluate-implies-vacuous', formulaId);
    return result;
  }

  const consequentResult = evaluateFormula(formula.consequent, env, state);
  let outcome: 'pass' | 'fail' | 'indeterminate';
  let truth: 'determinate' | 'indeterminate';
  let metrics: Record<string, number> | undefined;

  if (consequentResult.outcome === 'pass') {
    outcome = 'pass';
    truth = 'determinate';
  } else if (consequentResult.outcome === 'indeterminate') {
    outcome = 'indeterminate';
    truth = 'indeterminate';
    metrics = consequentResult.metrics;
  } else {
    outcome = 'fail';
    truth = 'determinate';
    metrics = consequentResult.metrics;
  }

  const result: FormulaResult = {
    formulaId,
    outcome,
    truth,
    metrics,
  };
  state.proofs.push(makeProof(state, formulaId, result.outcome, result.truth));
  addTrace(state, 'evaluate-implies-end', formulaId, { outcome });
  return result;
}

function evaluatePredicate(
  formula: PredicateCall,
  env: BindingEnv,
  state: EvalState,
  formulaId: string,
): FormulaResult {
  addTrace(state, 'evaluate-predicate-start', formulaId, {
    predicate: formula.predicate,
  });

  const evaluator = state.predicateRegistry.get(formula.predicate);
  if (!evaluator) {
    const msg = `No predicate evaluator registered for: ${formula.predicate}`;
    addDiagnostic(
      state,
      'IMH_LOGIC_PREDICATE_MISSING',
      'error',
      msg,
      formulaId,
    );
    const result: FormulaResult = {
      formulaId,
      outcome: 'indeterminate',
      truth: 'indeterminate',
    };
    state.proofs.push(makeProof(state, formulaId, 'indeterminate', 'indeterminate'));
    return result;
  }

  // Resolve arguments from bindings.
  const tuple: number[] = [];
  for (const arg of formula.args) {
    switch (arg.type) {
      case 'VariableRef': {
        const subjectId = env.lookup(arg.name);
        if (subjectId === undefined) {
          addDiagnostic(
            state,
            'IMH_LOGIC_UNBOUND_VARIABLE',
            'error',
            `Variable ${arg.name} is not bound in the current scope.`,
            formulaId,
          );
          const result: FormulaResult = {
            formulaId,
            outcome: 'indeterminate',
            truth: 'indeterminate',
          };
          state.proofs.push(makeProof(state, formulaId, 'indeterminate', 'indeterminate'));
          return result;
        }
        tuple.push(subjectId);
        break;
      }
      case 'AccessorTerm': {
        const subjectId = env.lookup(arg.variable);
        if (subjectId === undefined) {
          addDiagnostic(
            state,
            'IMH_LOGIC_UNBOUND_VARIABLE',
            'error',
            `Variable ${arg.variable} is not bound in the current scope.`,
            formulaId,
          );
          const result: FormulaResult = {
            formulaId,
            outcome: 'indeterminate',
            truth: 'indeterminate',
          };
          state.proofs.push(makeProof(state, formulaId, 'indeterminate', 'indeterminate'));
          return result;
        }
        // For now, accessors evaluate to the subject id itself.
        // Property access (e.g., width, height) is handled by the predicate.
        tuple.push(subjectId);
        break;
      }
      default:
        addDiagnostic(
          state,
          'IMH_LOGIC_UNSUPPORTED_TERM',
          'error',
          `Unsupported term type: ${arg.type}`,
          formulaId,
        );
        const result: FormulaResult = {
          formulaId,
          outcome: 'indeterminate',
          truth: 'indeterminate',
        };
        state.proofs.push(makeProof(state, formulaId, 'indeterminate', 'indeterminate'));
        return result;
    }
  }

  const predicateResult = evaluator.evaluateTuple(state.world, tuple, (formula as any).options);

  // Propagate predicate-level diagnostics to engine state.
  if (predicateResult.diagnostics) {
    for (const d of predicateResult.diagnostics) {
      addDiagnostic(state, d.code, d.severity, d.message, formulaId);
    }
  }

  const outcome: 'pass' | 'fail' | 'indeterminate' =
    predicateResult.truth === 'true'
      ? 'pass'
      : predicateResult.truth === 'false'
        ? 'fail'
        : 'indeterminate';

  const result: FormulaResult = {
    formulaId,
    outcome,
    truth: outcome === 'indeterminate' ? 'indeterminate' : 'determinate',
    witness: predicateResult.witness?.subjectIds,
    metrics: predicateResult.metrics,
  };

  state.proofs.push(
    makeProof(
      state,
      formulaId,
      result.outcome,
      result.truth,
      result.witness,
    ),
  );
  addTrace(state, 'evaluate-predicate-end', formulaId, {
    predicate: formula.predicate,
    outcome,
  });

  return result;
}

// ---------------------------------------------------------------------------
// Public API
// ---------------------------------------------------------------------------

export interface LogicEngineInput {
  formula: FormulaNode;
  world: GeometryWorld;
  resolver: DomainResolver;
  options?: LogicEngineOptions;
}

/**
 * Evaluate a logic formula deterministically against a geometry world.
 *
 * This is the entry point for Stream 1 deterministic scene evaluation.
 */
export function evaluateLogic(input: LogicEngineInput): DeterministicSceneEvaluation {
  const { formula, world, resolver, options = {} } = input;

  const state: EvalState = {
    world,
    resolver,
    options,
    diagnostics: [],
    trace: [],
    proofs: [],
    proofCounter: 0,
    formulaCounter: 0,
    predicateRegistry: options.predicateRegistry ?? globalPredicateRegistry,
  };

  addTrace(state, 'evaluate-logic-start');

  const env = new BindingEnv();
  const formulaResult = evaluateFormula(formula, env, state);

  addTrace(state, 'evaluate-logic-end');

  const mode: EvaluationMode =
    formulaResult.outcome === 'indeterminate'
      ? 'scene-indeterminate'
      : 'scene-determinate';

  const failingAssignments: Record<string, number>[] = [];
  if (formulaResult.outcome === 'fail') {
    // Collect failing assignments from trace events.
    for (const event of state.trace) {
      if (event.payload && typeof event.payload === 'object' && 'failingTuple' in event.payload) {
        const ft = event.payload.failingTuple as Record<string, number>;
        failingAssignments.push(ft);
      }
    }
  }

  return {
    mode,
    sceneId: world.sceneId,
    passed: formulaResult.outcome === 'pass',
    formulaResults: [formulaResult],
    proofs: state.proofs,
    diagnostics: state.diagnostics,
    trace: state.trace,
    failingAssignments: failingAssignments.length > 0 ? failingAssignments : undefined,
  };
}

/**
 * Convenience: evaluate a formula with default predicates registered.
 */
export function evaluateLogicWithDefaults(input: LogicEngineInput): DeterministicSceneEvaluation {
  registerDefaultPredicates();
  return evaluateLogic(input);
}