/**
 * Edge case tests for Imhotep's First-Order Logic implementation.
 *
 * Covers:
 *   1. Empty domains (vacuous truth)
 *   2. Variable shadowing in nested quantifiers
 *   3. Free/unbound variables
 *   4. Quantifier over single element
 *   5. Deep nesting (5+ levels)
 *   6. Circular/tautological formulas
 *   7. Contradictions
 *   8. Mixed coordinate spaces in quantified formulas
 */

import { describe, it, beforeEach } from 'node:test';
import assert from 'node:assert';

import type {
  DomainValue,
} from 'imhotep-core';

import type {
  GeometryWorld,
} from './registry.js';

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

import {
  clearPredicateRegistry,
  registerDefaultPredicates,
} from './predicates.js';

import {
  evaluateLogic,
  type LogicEngineInput,
  type DomainResolver,
} from './logic-engine.js';

// ---------------------------------------------------------------------------
// Mock World Helpers
// ---------------------------------------------------------------------------

function makeWorld(overrides?: Partial<GeometryWorld>): GeometryWorld {
  return {
    sceneId: 'scene_1',
    snapshotId: 'snap_1',
    env: {
      viewportWidth: 1280,
      viewportHeight: 800,
      deviceScaleFactor: 1,
      colorScheme: 'light',
      pointer: 'fine',
      hover: false,
      reducedMotion: false,
      locale: 'en',
      writingMode: 'horizontal-tb',
    },
    strings: { values: [] },
    subjects: {
      ids: [1, 2, 3],
      domNodeId: [10, 20, 30],
      subjectKind: [1, 1, 1],
      primaryBoxId: [100, 200, 300],
      firstFragmentId: [0, 0, 0],
      fragmentCount: [0, 0, 0],
    },
    dom: {
      nodeId: [10, 20, 30],
      parentNodeId: [0, 0, 0],
      childCount: [0, 0, 0],
      tagNameStringId: [0, 0, 0],
    },
    boxes: {
      boxId: [100, 200, 300],
      subjectId: [1, 2, 3],
      frameId: [1, 1, 1],
      borderLeft: [0, 110, 220],
      borderTop: [0, 50, 100],
      borderRight: [100, 210, 320],
      borderBottom: [40, 90, 140],
      paddingLeft: [0, 0, 0],
      paddingTop: [0, 0, 0],
      paddingRight: [0, 0, 0],
      paddingBottom: [0, 0, 0],
      contentLeft: [0, 0, 0],
      contentTop: [0, 0, 0],
      contentRight: [0, 0, 0],
      contentBottom: [0, 0, 0],
    },
    visualBoxes: {
      boxId: [], subjectId: [], frameId: [],
      borderLeft: [], borderTop: [], borderRight: [], borderBottom: [],
      paddingLeft: [], paddingTop: [], paddingRight: [], paddingBottom: [],
      contentLeft: [], contentTop: [], contentRight: [], contentBottom: [],
    },
    transforms: {
      transformId: [], subjectId: [], matrixStart: [], matrixLength: [],
      originX: [], originY: [],
    },
    matrices: { values: [] },
    rects: {
      rectId: [],
      left: [],
      top: [],
      right: [],
      bottom: [],
    },
    topology: {
      containingBlockOf: [0, 0, 0],
      nearestPositionedAncestorOf: [0, 0, 0],
      scrollContainerOf: [0, 0, 0],
      stackingContextOf: [0, 0, 0],
      formattingContextOf: [0, 0, 0],
      clippingRootOf: [0, 0, 0],
      paintOrderBucket: [0, 0, 0],
      paintOrderIndex: [0, 0, 0],
    },
    scroll: {
      containerId: [],
      scrollLeft: [],
      scrollTop: [],
      scrollWidth: [],
      scrollHeight: [],
      clientWidth: [],
      clientHeight: [],
    },
    clipping: {
      clipNodeId: [],
      subjectId: [],
      clipKind: [],
      clipLeft: [],
      clipTop: [],
      clipRight: [],
      clipBottom: [],
      parentClipNodeId: [],
    },
    visibility: {
      subjectId: [],
      isRendered: [],
      isVisible: [],
      visibleArea: [],
      clippedArea: [],
    },
    ...overrides,
  };
}

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

function makeResolver(domains: Map<string, DomainValue>): DomainResolver {
  return {
    resolve(domain: DomainRef, _env?): DomainValue | undefined {
      const key = domain.selector ?? domain.domain;
      return domains.get(key);
    },
  };
}

// ---------------------------------------------------------------------------
// Formula Helpers
// ---------------------------------------------------------------------------

function predicate(name: string, args: TermNode[]): PredicateCall {
  return {
    type: 'FormulaNode',
    kind: 'predicate',
    predicate: name,
    args,
  };
}

function varRef(name: string): TermNode {
  return { type: 'VariableRef', name };
}

function domainRef(domain: string, selector?: string, parentVar?: string): DomainRef {
  return { type: 'DomainRef', domain, selector, parentVar };
}

function forall(bindings: { vars: string[]; domain: DomainRef }[], body: FormulaNode): ForAllFormula {
  return {
    type: 'FormulaNode',
    kind: 'forall',
    bindings: bindings.map((b) => ({
      type: 'TupleBinding',
      variables: b.vars,
      domain: b.domain,
    })),
    body,
  };
}

function exists(bindings: { vars: string[]; domain: DomainRef }[], body: FormulaNode): ExistsFormula {
  return {
    type: 'FormulaNode',
    kind: 'exists',
    bindings: bindings.map((b) => ({
      type: 'TupleBinding',
      variables: b.vars,
      domain: b.domain,
    })),
    body,
  };
}

function and(left: FormulaNode, right: FormulaNode): AndFormula {
  return { type: 'FormulaNode', kind: 'and', left, right };
}

function or(left: FormulaNode, right: FormulaNode): OrFormula {
  return { type: 'FormulaNode', kind: 'or', left, right };
}

function not(operand: FormulaNode): NotFormula {
  return { type: 'FormulaNode', kind: 'not', operand };
}

// ---------------------------------------------------------------------------
// Setup
// ---------------------------------------------------------------------------

beforeEach(() => {
  clearPredicateRegistry();
  registerDefaultPredicates();
});

// ---------------------------------------------------------------------------
// Edge Case 1: Empty domains
// ---------------------------------------------------------------------------

describe('Edge Case 1: Empty domains', () => {
  it('forall over empty domain passes vacuously with diagnostic', () => {
    const world = makeWorld();
    const formula = predicate('leftOf', [varRef('x'), varRef('y')]);
    const domains = new Map<string, DomainValue>([
      ['.nonexistent', {
        domainId: 'dom_empty',
        subjectIds: new Uint32Array([]),
        provenance: 'elements(.nonexistent)',
        closed: true,
      }],
      ['.something', {
        domainId: 'dom_something',
        subjectIds: new Uint32Array([2]),
        provenance: 'elements(.something)',
        closed: true,
      }],
    ]);

    const input: LogicEngineInput = {
      formula: forall([
        { vars: ['x'], domain: domainRef('elements', '.nonexistent') },
        { vars: ['y'], domain: domainRef('elements', '.something') },
      ], formula),
      world,
      resolver: makeResolver(domains),
    };

    const result = evaluateLogic(input);
    // FIXED: When one of multiple domains is empty, forall is vacuously true.
    // Previously the engine skipped empty domains and left variables unbound,
    // causing indeterminate. Fixed in logic-engine.ts:283-296.
    assert.strictEqual(result.passed, true, 'forall over empty domain should be vacuously true');
    assert.strictEqual(result.formulaResults[0].outcome, 'pass');
    assert.ok(
      result.diagnostics.some((d) => d.code === 'IMH_LOGIC_VACUOUS_FORALL'),
      'Should emit vacuous forall diagnostic'
    );
  });

  it('exists over empty domain fails with diagnostic', () => {
    const world = makeWorld();
    const formula = predicate('leftOf', [varRef('x'), varRef('y')]);
    const domains = new Map<string, DomainValue>([
      ['.nonexistent', {
        domainId: 'dom_empty',
        subjectIds: new Uint32Array([]),
        provenance: 'elements(.nonexistent)',
        closed: true,
      }],
      ['.something', {
        domainId: 'dom_something',
        subjectIds: new Uint32Array([2]),
        provenance: 'elements(.something)',
        closed: true,
      }],
    ]);

    const input: LogicEngineInput = {
      formula: exists([
        { vars: ['x'], domain: domainRef('elements', '.nonexistent') },
        { vars: ['y'], domain: domainRef('elements', '.something') },
      ], formula),
      world,
      resolver: makeResolver(domains),
    };

    const result = evaluateLogic(input);
    // FIXED: When one of multiple domains is empty, exists is false.
    // Previously the engine skipped empty domains and left variables unbound,
    // causing indeterminate. Fixed in logic-engine.ts:424-433.
    assert.strictEqual(result.passed, false, 'exists over empty domain should be false');
    assert.strictEqual(result.formulaResults[0].outcome, 'fail');
    assert.ok(
      result.diagnostics.some((d) => d.code === 'IMH_LOGIC_EMPTY_DOMAIN_EXISTS'),
      'Should emit empty domain exists diagnostic'
    );
  });
});

// ---------------------------------------------------------------------------
// Edge Case 2: Variable shadowing
// ---------------------------------------------------------------------------

describe('Edge Case 2: Variable shadowing', () => {
  it('nested forall with same variable name uses inner binding', () => {
    const world = makeWorld();
    // Subject 1 [0,0,100,40] is leftOf subject 2 [110,50,210,90] (gap 10).
    // Subject 2 [110,50,210,90] is leftOf subject 3 [220,100,320,140] (gap 10).
    // Inner $x should bind to .b domain (subject 2), not outer .a domain (subject 1).
    const innerBody = predicate('leftOf', [varRef('x'), varRef('c')]);
    const innerForall = forall([
      { vars: ['x'], domain: domainRef('elements', '.b') },
      { vars: ['c'], domain: domainRef('elements', '.c') },
    ], innerBody);
    const outerForall = forall([
      { vars: ['x'], domain: domainRef('elements', '.a') },
    ], innerForall);

    const domains = new Map<string, DomainValue>([
      ['.a', {
        domainId: 'dom_a',
        subjectIds: new Uint32Array([1]),
        provenance: 'elements(.a)',
        closed: true,
      }],
      ['.b', {
        domainId: 'dom_b',
        subjectIds: new Uint32Array([2]),
        provenance: 'elements(.b)',
        closed: true,
      }],
      ['.c', {
        domainId: 'dom_c',
        subjectIds: new Uint32Array([3]),
        provenance: 'elements(.c)',
        closed: true,
      }],
    ]);

    const input: LogicEngineInput = {
      formula: outerForall,
      world,
      resolver: makeResolver(domains),
    };

    const result = evaluateLogic(input);
    // Inner $x binds to subject 2, which is leftOf subject 3 (gap 10).
    assert.strictEqual(result.passed, true, 'Inner binding should shadow outer; subject 2 is leftOf subject 3');
    assert.strictEqual(result.formulaResults[0].outcome, 'pass');
  });

  it('nested forall with same variable name fails when inner binding violates predicate', () => {
    const world = makeWorld();
    // Subject 2 [110,50,210,90] is NOT leftOf subject 1 [0,0,100,40].
    const innerBody = predicate('leftOf', [varRef('x'), varRef('c')]);
    const innerForall = forall([
      { vars: ['x'], domain: domainRef('elements', '.b') },
      { vars: ['c'], domain: domainRef('elements', '.c') },
    ], innerBody);
    const outerForall = forall([
      { vars: ['x'], domain: domainRef('elements', '.a') },
    ], innerForall);

    const domains = new Map<string, DomainValue>([
      ['.a', {
        domainId: 'dom_a',
        subjectIds: new Uint32Array([1]),
        provenance: 'elements(.a)',
        closed: true,
      }],
      ['.b', {
        domainId: 'dom_b',
        subjectIds: new Uint32Array([2]),
        provenance: 'elements(.b)',
        closed: true,
      }],
      ['.c', {
        domainId: 'dom_c',
        subjectIds: new Uint32Array([1]),
        provenance: 'elements(.c)',
        closed: true,
      }],
    ]);

    const input: LogicEngineInput = {
      formula: outerForall,
      world,
      resolver: makeResolver(domains),
    };

    const result = evaluateLogic(input);
    // Inner $x binds to subject 2, which is NOT leftOf subject 1.
    assert.strictEqual(result.passed, false, 'Inner binding should shadow outer; subject 2 is NOT leftOf subject 1');
    assert.strictEqual(result.formulaResults[0].outcome, 'fail');
  });
});

// ---------------------------------------------------------------------------
// Edge Case 3: Free variables
// ---------------------------------------------------------------------------

describe('Edge Case 3: Free variables', () => {
  it('unbound variable produces IMH_LOGIC_UNBOUND_VARIABLE and indeterminate', () => {
    const world = makeWorld();
    // $y is not bound by any quantifier.
    const formula = predicate('leftOf', [varRef('x'), varRef('y')]);
    const domains = new Map<string, DomainValue>([
      ['.a', {
        domainId: 'dom_a',
        subjectIds: new Uint32Array([1]),
        provenance: 'elements(.a)',
        closed: true,
      }],
    ]);

    const input: LogicEngineInput = {
      formula: forall([
        { vars: ['x'], domain: domainRef('elements', '.a') },
      ], formula),
      world,
      resolver: makeResolver(domains),
    };

    const result = evaluateLogic(input);
    assert.strictEqual(result.passed, false, 'Unbound variable should cause indeterminate/failure');
    assert.strictEqual(result.formulaResults[0].outcome, 'indeterminate');
    assert.ok(
      result.diagnostics.some((d) => d.code === 'IMH_LOGIC_UNBOUND_VARIABLE'),
      'Should emit IMH_LOGIC_UNBOUND_VARIABLE diagnostic'
    );
    assert.ok(
      result.diagnostics.some((d) => d.message.includes('y')),
      'Diagnostic should mention the unbound variable name y'
    );
  });
});

// ---------------------------------------------------------------------------
// Edge Case 4: Quantifier over single element
// ---------------------------------------------------------------------------

describe('Edge Case 4: Quantifier over single element', () => {
  it('forall over single element produces same result as non-quantified version', () => {
    const world = makeWorld();
    // Subject 1 is leftOf subject 2.
    const quantifiedFormula = forall([
      { vars: ['x'], domain: domainRef('elements', '.a') },
      { vars: ['y'], domain: domainRef('elements', '.b') },
    ], predicate('leftOf', [varRef('x'), varRef('y')]));

    const nonQuantifiedFormula = predicate('leftOf', [varRef('x'), varRef('y')]);

    const domains = new Map<string, DomainValue>([
      ['.a', {
        domainId: 'dom_a',
        subjectIds: new Uint32Array([1]),
        provenance: 'elements(.a)',
        closed: true,
      }],
      ['.b', {
        domainId: 'dom_b',
        subjectIds: new Uint32Array([2]),
        provenance: 'elements(.b)',
        closed: true,
      }],
    ]);

    const quantifiedInput: LogicEngineInput = {
      formula: quantifiedFormula,
      world,
      resolver: makeResolver(domains),
    };

    const quantifiedResult = evaluateLogic(quantifiedInput);

    assert.strictEqual(quantifiedResult.passed, true, 'Quantified single element should pass');
    assert.strictEqual(quantifiedResult.formulaResults[0].outcome, 'pass');
  });

  it('forall over single failing element produces same failure as non-quantified', () => {
    const world = makeWorld();
    // Subject 2 is NOT leftOf subject 1.
    const quantifiedFormula = forall([
      { vars: ['x'], domain: domainRef('elements', '.b') },
      { vars: ['y'], domain: domainRef('elements', '.a') },
    ], predicate('leftOf', [varRef('x'), varRef('y')]));

    const domains = new Map<string, DomainValue>([
      ['.a', {
        domainId: 'dom_a',
        subjectIds: new Uint32Array([1]),
        provenance: 'elements(.a)',
        closed: true,
      }],
      ['.b', {
        domainId: 'dom_b',
        subjectIds: new Uint32Array([2]),
        provenance: 'elements(.b)',
        closed: true,
      }],
    ]);

    const input: LogicEngineInput = {
      formula: quantifiedFormula,
      world,
      resolver: makeResolver(domains),
    };

    const result = evaluateLogic(input);
    assert.strictEqual(result.passed, false, 'Quantified single element should fail when predicate is false');
    assert.strictEqual(result.formulaResults[0].outcome, 'fail');
  });
});

// ---------------------------------------------------------------------------
// Edge Case 5: Deep nesting (5+ levels)
// ---------------------------------------------------------------------------

describe('Edge Case 5: Deep nesting (5+ levels)', () => {
  it('deeply nested and(5+) evaluates without stack overflow', () => {
    const world = makeWorld();
    // Build a deeply nested and tree: and(A, and(B, and(C, and(D, and(E, F)))))
    // All predicates are true: leftOf(1,2), leftOf(1,3), leftOf(2,3), etc.
    const p1 = predicate('leftOf', [varRef('a'), varRef('b')]);
    const p2 = predicate('leftOf', [varRef('a'), varRef('c')]);
    const p3 = predicate('leftOf', [varRef('b'), varRef('c')]);
    const p4 = predicate('above', [varRef('a'), varRef('b')]);
    const p5 = predicate('above', [varRef('a'), varRef('c')]);
    const p6 = predicate('above', [varRef('b'), varRef('c')]);

    let body = and(p5, p6);
    body = and(p4, body);
    body = and(p3, body);
    body = and(p2, body);
    body = and(p1, body);

    const domains = new Map<string, DomainValue>([
      ['.a', {
        domainId: 'dom_a',
        subjectIds: new Uint32Array([1]),
        provenance: 'elements(.a)',
        closed: true,
      }],
      ['.b', {
        domainId: 'dom_b',
        subjectIds: new Uint32Array([2]),
        provenance: 'elements(.b)',
        closed: true,
      }],
      ['.c', {
        domainId: 'dom_c',
        subjectIds: new Uint32Array([3]),
        provenance: 'elements(.c)',
        closed: true,
      }],
    ]);

    const input: LogicEngineInput = {
      formula: forall([
        { vars: ['a'], domain: domainRef('elements', '.a') },
        { vars: ['b'], domain: domainRef('elements', '.b') },
        { vars: ['c'], domain: domainRef('elements', '.c') },
      ], body),
      world,
      resolver: makeResolver(domains),
    };

    const result = evaluateLogic(input);
    assert.strictEqual(result.passed, true, 'Deep nesting should not overflow and should pass');
    assert.strictEqual(result.formulaResults[0].outcome, 'pass');
  });

  it('deeply nested or(5+) short-circuits correctly', () => {
    const world = makeWorld();
    // First predicate is true, rest are false - should short-circuit.
    const p1 = predicate('leftOf', [varRef('a'), varRef('b')]);
    const p2 = predicate('inside', [varRef('a'), varRef('b')]);
    const p3 = predicate('inside', [varRef('b'), varRef('a')]);
    const p4 = predicate('inside', [varRef('a'), varRef('c')]);
    const p5 = predicate('inside', [varRef('c'), varRef('a')]);
    const p6 = predicate('inside', [varRef('b'), varRef('c')]);

    let body = or(p5, p6);
    body = or(p4, body);
    body = or(p3, body);
    body = or(p2, body);
    body = or(p1, body);

    const domains = new Map<string, DomainValue>([
      ['.a', {
        domainId: 'dom_a',
        subjectIds: new Uint32Array([1]),
        provenance: 'elements(.a)',
        closed: true,
      }],
      ['.b', {
        domainId: 'dom_b',
        subjectIds: new Uint32Array([2]),
        provenance: 'elements(.b)',
        closed: true,
      }],
      ['.c', {
        domainId: 'dom_c',
        subjectIds: new Uint32Array([3]),
        provenance: 'elements(.c)',
        closed: true,
      }],
    ]);

    const input: LogicEngineInput = {
      formula: forall([
        { vars: ['a'], domain: domainRef('elements', '.a') },
        { vars: ['b'], domain: domainRef('elements', '.b') },
        { vars: ['c'], domain: domainRef('elements', '.c') },
      ], body),
      world,
      resolver: makeResolver(domains),
    };

    const result = evaluateLogic(input);
    assert.strictEqual(result.passed, true, 'Deep or should short-circuit on first true');
    assert.strictEqual(result.formulaResults[0].outcome, 'pass');
    assert.ok(
      result.trace.some((t) => t.phase === 'evaluate-or-short-circuit'),
      'Should show short-circuit trace'
    );
  });
});

// ---------------------------------------------------------------------------
// Edge Case 6: Circular/tautological formulas
// ---------------------------------------------------------------------------

describe('Edge Case 6: Circular/tautological formulas', () => {
  it('or(P, not(P)) is always a tautology', () => {
    const world = makeWorld();
    // leftOf(1,2) is true, so or(leftOf, not(leftOf)) is true.
    // Even if leftOf were false, not(leftOf) would be true.
    const p = predicate('leftOf', [varRef('a'), varRef('b')]);
    const tautology = or(p, not(p));

    const domains = new Map<string, DomainValue>([
      ['.a', {
        domainId: 'dom_a',
        subjectIds: new Uint32Array([1]),
        provenance: 'elements(.a)',
        closed: true,
      }],
      ['.b', {
        domainId: 'dom_b',
        subjectIds: new Uint32Array([2]),
        provenance: 'elements(.b)',
        closed: true,
      }],
    ]);

    const input: LogicEngineInput = {
      formula: forall([
        { vars: ['a'], domain: domainRef('elements', '.a') },
        { vars: ['b'], domain: domainRef('elements', '.b') },
      ], tautology),
      world,
      resolver: makeResolver(domains),
    };

    const result = evaluateLogic(input);
    assert.strictEqual(result.passed, true, 'Tautology or(P, not(P)) should always pass');
    assert.strictEqual(result.formulaResults[0].outcome, 'pass');
  });

  it('or(inside, not(inside)) passes even when inside is false', () => {
    const world = makeWorld();
    // inside(1,2) is false, so not(inside) is true.
    const p = predicate('inside', [varRef('a'), varRef('b')]);
    const tautology = or(p, not(p));

    const domains = new Map<string, DomainValue>([
      ['.a', {
        domainId: 'dom_a',
        subjectIds: new Uint32Array([1]),
        provenance: 'elements(.a)',
        closed: true,
      }],
      ['.b', {
        domainId: 'dom_b',
        subjectIds: new Uint32Array([2]),
        provenance: 'elements(.b)',
        closed: true,
      }],
    ]);

    const input: LogicEngineInput = {
      formula: forall([
        { vars: ['a'], domain: domainRef('elements', '.a') },
        { vars: ['b'], domain: domainRef('elements', '.b') },
      ], tautology),
      world,
      resolver: makeResolver(domains),
    };

    const result = evaluateLogic(input);
    assert.strictEqual(result.passed, true, 'Tautology should pass even when predicate is false');
    assert.strictEqual(result.formulaResults[0].outcome, 'pass');
  });
});

// ---------------------------------------------------------------------------
// Edge Case 7: Contradictions
// ---------------------------------------------------------------------------

describe('Edge Case 7: Contradictions', () => {
  it('and(P, not(P)) is always a contradiction', () => {
    const world = makeWorld();
    // leftOf(1,2) is true, so not(leftOf) is false, and(true, false) = false.
    const p = predicate('leftOf', [varRef('a'), varRef('b')]);
    const contradiction = and(p, not(p));

    const domains = new Map<string, DomainValue>([
      ['.a', {
        domainId: 'dom_a',
        subjectIds: new Uint32Array([1]),
        provenance: 'elements(.a)',
        closed: true,
      }],
      ['.b', {
        domainId: 'dom_b',
        subjectIds: new Uint32Array([2]),
        provenance: 'elements(.b)',
        closed: true,
      }],
    ]);

    const input: LogicEngineInput = {
      formula: forall([
        { vars: ['a'], domain: domainRef('elements', '.a') },
        { vars: ['b'], domain: domainRef('elements', '.b') },
      ], contradiction),
      world,
      resolver: makeResolver(domains),
    };

    const result = evaluateLogic(input);
    assert.strictEqual(result.passed, false, 'Contradiction and(P, not(P)) should always fail');
    assert.strictEqual(result.formulaResults[0].outcome, 'fail');
  });

  it('and(inside, not(inside)) fails even when both are evaluated', () => {
    const world = makeWorld();
    // inside(1,2) is false, not(inside) is true, and(false, true) = false.
    const p = predicate('inside', [varRef('a'), varRef('b')]);
    const contradiction = and(p, not(p));

    const domains = new Map<string, DomainValue>([
      ['.a', {
        domainId: 'dom_a',
        subjectIds: new Uint32Array([1]),
        provenance: 'elements(.a)',
        closed: true,
      }],
      ['.b', {
        domainId: 'dom_b',
        subjectIds: new Uint32Array([2]),
        provenance: 'elements(.b)',
        closed: true,
      }],
    ]);

    const input: LogicEngineInput = {
      formula: forall([
        { vars: ['a'], domain: domainRef('elements', '.a') },
        { vars: ['b'], domain: domainRef('elements', '.b') },
      ], contradiction),
      world,
      resolver: makeResolver(domains),
    };

    const result = evaluateLogic(input);
    assert.strictEqual(result.passed, false, 'Contradiction should always fail');
    assert.strictEqual(result.formulaResults[0].outcome, 'fail');
  });
});

// ---------------------------------------------------------------------------
// Edge Case 8: Mixed coordinate spaces in quantified formulas
// ---------------------------------------------------------------------------

describe('Edge Case 8: Mixed coordinate spaces in quantified formulas', () => {
  it('forall with layout space option uses layout space for all evaluations', () => {
    const world = makeWorld();
    // The leftOf predicate with space: 'layout' should be evaluated in layout space.
    // For this test, we just verify the formula compiles and evaluates without error.
    // The actual layout vs visual difference would require transformed elements.
    const formula = predicate('leftOf', [varRef('x'), varRef('y')]);
    (formula as any).options = { space: 'layout' };

    const domains = new Map<string, DomainValue>([
      ['.transformed', {
        domainId: 'dom_transformed',
        subjectIds: new Uint32Array([1]),
        provenance: 'elements(.transformed)',
        closed: true,
      }],
      ['.anchor', {
        domainId: 'dom_anchor',
        subjectIds: new Uint32Array([2]),
        provenance: 'elements(.anchor)',
        closed: true,
      }],
    ]);

    const input: LogicEngineInput = {
      formula: forall([
        { vars: ['x'], domain: domainRef('elements', '.transformed') },
        { vars: ['y'], domain: domainRef('elements', '.anchor') },
      ], formula),
      world,
      resolver: makeResolver(domains),
    };

    const result = evaluateLogic(input);
    // Should evaluate without error; pass/fail depends on geometry.
    assert.ok(
      result.formulaResults[0].outcome === 'pass' || result.formulaResults[0].outcome === 'fail',
      'Layout space option should not cause indeterminate'
    );
    assert.strictEqual(result.formulaResults[0].truth, 'determinate');
  });
});