852 lines
27 KiB
TypeScript
852 lines
27 KiB
TypeScript
|
/**
|
||
|
|
* 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): 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');
|
||
|
|
});
|
||
|
|
});
|