import { PredicateFormula } from '../../../types.js';
/**
* Parse Tree Visualizer for predicate logic formulas
* Creates SVG visualizations of formula structure as a tree
*/
export class PredicateParseTreeVisualizer {
// SVG dimensions and spacing
private width = 900;
private height = 700;
private nodeRadius = 25;
private levelHeight = 80;
private horizontalSpacing = 50;
private margin = 40;
/**
* Generate a parse tree visualization for a predicate formula
* @param formula The formula to visualize
* @returns SVG string representation of the parse tree
*/
generateParseTree(formula: PredicateFormula): string {
// Calculate tree dimensions
const treeDepth = this.calculateTreeDepth(formula);
const treeWidth = this.calculateTreeWidth(formula);
// Adjust SVG size based on tree dimensions
this.height = treeDepth * this.levelHeight + 2 * this.margin;
this.width = Math.max(500, treeWidth * this.horizontalSpacing + 2 * this.margin);
// Start SVG content
let svg = `<svg width="${this.width}" height="${this.height}" xmlns="http://www.w3.org/2000/svg">`;
// Add background
svg += `<rect x="0" y="0" width="${this.width}" height="${this.height}" fill="#f8f8f8" />`;
// Add title
svg += `
<text x="${this.width / 2}" y="${this.margin / 2}"
text-anchor="middle" font-family="Arial" font-size="16" font-weight="bold">
Parse Tree for: ${this.formatFormula(formula)}
</text>
`;
// Calculate node positions and draw the tree
const rootX = this.width / 2;
const rootY = this.margin + this.nodeRadius;
// Create node IDs for links
let nextNodeId = 0;
// Add tree elements (nodes and links)
const nodeMap = new Map<number, { x: number; y: number }>();
const { nodes, links } = this.createTreeElements(formula, rootX, rootY, 0, nextNodeId, nodeMap);
// Add links first (so they appear behind nodes)
links.forEach(link => {
svg += link;
});
// Add nodes
nodes.forEach(node => {
svg += node;
});
// Add legend
svg += this.createLegend();
// Close SVG
svg += '</svg>';
return svg;
}
/**
* Calculate the depth of the parse tree
* @param formula The formula to analyze
* @returns Depth of the tree (number of levels)
*/
private calculateTreeDepth(formula: PredicateFormula): number {
switch (formula.type) {
case 'variable':
case 'constant':
return 1;
case 'function':
case 'predicate':
// Find the max depth of arguments plus 1 for this node
return 1 + Math.max(
0,
...formula.args.map(arg => this.calculateTreeDepth(arg))
);
case 'unary':
return 1 + this.calculateTreeDepth(formula.operand);
case 'binary':
return 1 + Math.max(
this.calculateTreeDepth(formula.left),
this.calculateTreeDepth(formula.right)
);
case 'quantified':
return 1 + this.calculateTreeDepth(formula.formula);
default:
return 1; // Fallback
}
}
/**
* Calculate the width of the parse tree
* @param formula The formula to analyze
* @returns Width of the tree (approximate number of leaf nodes)
*/
private calculateTreeWidth(formula: PredicateFormula): number {
switch (formula.type) {
case 'variable':
case 'constant':
return 1;
case 'function':
case 'predicate':
// Sum up widths of all arguments
return Math.max(
1,
formula.args.reduce((sum, arg) => sum + this.calculateTreeWidth(arg), 0)
);
case 'unary':
return this.calculateTreeWidth(formula.operand);
case 'binary':
return this.calculateTreeWidth(formula.left) + this.calculateTreeWidth(formula.right);
case 'quantified':
return this.calculateTreeWidth(formula.formula);
default:
return 1; // Fallback
}
}
/**
* Create tree elements (nodes and links) for SVG visualization
* @param formula The formula node to render
* @param x X-coordinate of this node
* @param y Y-coordinate of this node
* @param level Current tree level (depth)
* @param nodeId Unique ID for this node
* @param nodeMap Map of node IDs to coordinates
* @returns Object containing arrays of node and link SVG elements
*/
private createTreeElements(
formula: PredicateFormula,
x: number,
y: number,
level: number,
nodeId: number,
nodeMap: Map<number, { x: number; y: number }>
): {
nodes: string[];
links: string[];
nextNodeId: number;
width: number;
} {
const nodes: string[] = [];
const links: string[] = [];
let currentNodeId = nodeId;
let nextNodeId = nodeId + 1;
let totalWidth = 1;
// Store node position for links
nodeMap.set(currentNodeId, { x, y });
// Create node based on formula type
let nodeContent = '';
let nodeFill = '';
switch (formula.type) {
case 'variable':
// Variable node
nodeContent = formula.name;
nodeFill = '#d1e7dd'; // Light green for variables
break;
case 'constant':
// Constant node
nodeContent = formula.name;
nodeFill = '#e7d1dd'; // Light pink for constants
break;
case 'function':
// Function node
nodeContent = formula.name;
nodeFill = '#ddd1e7'; // Light purple for functions
// Create child nodes (arguments)
const fnArgWidth = this.calculateTreeWidth(formula);
const fnChildY = y + this.levelHeight;
totalWidth = fnArgWidth;
if (formula.args.length === 0) {
// Function with no arguments (constant function)
break;
}
// Calculate spacing for children
const fnSpacing = this.horizontalSpacing * Math.max(3, Math.min(10, fnArgWidth));
let fnChildX = x - (fnSpacing / 2) * (formula.args.length - 1) / 2;
// Create a node for each argument
for (const arg of formula.args) {
const argResult = this.createTreeElements(
arg,
fnChildX,
fnChildY,
level + 1,
nextNodeId,
nodeMap
);
nodes.push(...argResult.nodes);
links.push(...argResult.links);
// Add link to this argument
const argNodeId = nextNodeId;
const argPos = nodeMap.get(argNodeId);
if (argPos) {
links.push(this.createLink(x, y, argPos.x, argPos.y));
}
nextNodeId = argResult.nextNodeId;
fnChildX += fnSpacing / 2;
}
break;
case 'predicate':
// Predicate node
nodeContent = formula.name;
nodeFill = '#ffe6cc'; // Light orange for predicates
// Create child nodes (arguments) - similar to function case
const predArgWidth = this.calculateTreeWidth(formula);
const predChildY = y + this.levelHeight;
totalWidth = predArgWidth;
if (formula.args.length === 0) {
// Predicate with no arguments (proposition)
break;
}
// Calculate spacing for children
const predSpacing = this.horizontalSpacing * Math.max(3, Math.min(10, predArgWidth));
let predChildX = x - (predSpacing / 2) * (formula.args.length - 1) / 2;
// Create a node for each argument
for (const arg of formula.args) {
const argResult = this.createTreeElements(
arg,
predChildX,
predChildY,
level + 1,
nextNodeId,
nodeMap
);
nodes.push(...argResult.nodes);
links.push(...argResult.links);
// Add link to this argument
const argNodeId = nextNodeId;
const argPos = nodeMap.get(argNodeId);
if (argPos) {
links.push(this.createLink(x, y, argPos.x, argPos.y));
}
nextNodeId = argResult.nextNodeId;
predChildX += predSpacing / 2;
}
break;
case 'unary':
// Unary operator node (negation)
nodeContent = formula.operator === 'not' ? '¬' : formula.operator;
nodeFill = '#f8d7da'; // Light red for negation
// Create child node (operand)
const unaryChildY = y + this.levelHeight;
const unaryChildX = x; // Unary operators have one child directly below
const unaryChildResult = this.createTreeElements(
formula.operand,
unaryChildX,
unaryChildY,
level + 1,
nextNodeId,
nodeMap
);
nodes.push(...unaryChildResult.nodes);
links.push(...unaryChildResult.links);
// Add link to child
const unaryChildNodeId = nextNodeId;
const unaryChildPos = nodeMap.get(unaryChildNodeId);
if (unaryChildPos) {
links.push(this.createLink(x, y, unaryChildPos.x, unaryChildPos.y));
}
nextNodeId = unaryChildResult.nextNodeId;
totalWidth = unaryChildResult.width;
break;
case 'binary':
// Binary operator node
switch (formula.operator) {
case 'and':
case '∧':
nodeContent = '∧';
nodeFill = '#cfe2ff'; // Light blue for AND
break;
case 'or':
case '∨':
nodeContent = '∨';
nodeFill = '#fff3cd'; // Light yellow for OR
break;
case 'implies':
case '→':
nodeContent = '→';
nodeFill = '#e2d9f3'; // Light purple for IMPLIES
break;
case 'iff':
case '↔':
nodeContent = '↔';
nodeFill = '#d9f3e2'; // Light teal for IFF
break;
default:
nodeContent = formula.operator;
nodeFill = '#f0f0f0'; // Light gray for unknown operators
}
// Calculate child positions
const leftWidth = this.calculateTreeWidth(formula.left);
const rightWidth = this.calculateTreeWidth(formula.right);
totalWidth = leftWidth + rightWidth;
// Calculate horizontal spacing based on the tree width
const binarySpacing = this.horizontalSpacing * Math.max(3, Math.min(10, totalWidth));
// Create left child
const leftX = x - binarySpacing / 2;
const leftY = y + this.levelHeight;
const leftResult = this.createTreeElements(
formula.left,
leftX,
leftY,
level + 1,
nextNodeId,
nodeMap
);
nodes.push(...leftResult.nodes);
links.push(...leftResult.links);
// Add link to left child
const leftNodeId = nextNodeId;
const leftPos = nodeMap.get(leftNodeId);
if (leftPos) {
links.push(this.createLink(x, y, leftPos.x, leftPos.y));
}
nextNodeId = leftResult.nextNodeId;
// Create right child
const rightX = x + binarySpacing / 2;
const rightY = y + this.levelHeight;
const rightResult = this.createTreeElements(
formula.right,
rightX,
rightY,
level + 1,
nextNodeId,
nodeMap
);
nodes.push(...rightResult.nodes);
links.push(...rightResult.links);
// Add link to right child
const rightNodeId = nextNodeId;
const rightPos = nodeMap.get(rightNodeId);
if (rightPos) {
links.push(this.createLink(x, y, rightPos.x, rightPos.y));
}
nextNodeId = rightResult.nextNodeId;
break;
case 'quantified':
// Quantifier node
switch (formula.quantifier) {
case 'forall':
case '∀':
nodeContent = `∀${formula.variable}`;
nodeFill = '#d4edda'; // Light green for universal quantifier
break;
case 'exists':
case '∃':
nodeContent = `∃${formula.variable}`;
nodeFill = '#d1ecf1'; // Light blue for existential quantifier
break;
default:
nodeContent = `${formula.quantifier}${formula.variable}`;
nodeFill = '#f5f5f5'; // Light gray for unknown quantifiers
}
// Create child node (formula)
const quantChildY = y + this.levelHeight;
const quantChildX = x;
const quantChildResult = this.createTreeElements(
formula.formula,
quantChildX,
quantChildY,
level + 1,
nextNodeId,
nodeMap
);
nodes.push(...quantChildResult.nodes);
links.push(...quantChildResult.links);
// Add link to child
const quantChildNodeId = nextNodeId;
const quantChildPos = nodeMap.get(quantChildNodeId);
if (quantChildPos) {
links.push(this.createLink(x, y, quantChildPos.x, quantChildPos.y));
}
nextNodeId = quantChildResult.nextNodeId;
totalWidth = quantChildResult.width;
break;
}
// Create node SVG
nodes.push(this.createNode(x, y, nodeContent, nodeFill));
return {
nodes,
links,
nextNodeId,
width: totalWidth
};
}
/**
* Create an SVG node element
* @param x X-coordinate
* @param y Y-coordinate
* @param content Text content for the node
* @param fill Fill color
* @returns SVG string for the node
*/
private createNode(x: number, y: number, content: string, fill: string): string {
return `
<g class="node">
<circle cx="${x}" cy="${y}" r="${this.nodeRadius}"
fill="${fill}" stroke="#333" stroke-width="2" />
<text x="${x}" y="${y}"
text-anchor="middle" dominant-baseline="middle"
font-family="Arial" font-size="16" font-weight="bold">${content}</text>
</g>
`;
}
/**
* Create an SVG link between nodes
* @param x1 Starting X-coordinate
* @param y1 Starting Y-coordinate
* @param x2 Ending X-coordinate
* @param y2 Ending Y-coordinate
* @returns SVG string for the link
*/
private createLink(x1: number, y1: number, x2: number, y2: number): string {
// Adjust connection points to be at the edge of the circles
const angle = Math.atan2(y2 - y1, x2 - x1);
const startX = x1 + this.nodeRadius * Math.cos(angle);
const startY = y1 + this.nodeRadius * Math.sin(angle);
const endX = x2 - this.nodeRadius * Math.cos(angle);
const endY = y2 - this.nodeRadius * Math.sin(angle);
return `
<line x1="${startX}" y1="${startY}" x2="${endX}" y2="${endY}"
stroke="#333" stroke-width="2" />
`;
}
/**
* Create a legend explaining node colors
* @returns SVG string for the legend
*/
private createLegend(): string {
const legendX = this.margin;
const legendY = this.height - this.margin;
const itemHeight = 25;
const itemSpacing = 5;
// Legend items: [content, fill color, description]
const items: [string, string, string][] = [
['x', '#d1e7dd', 'Variable'],
['a', '#e7d1dd', 'Constant'],
['f', '#ddd1e7', 'Function'],
['P', '#ffe6cc', 'Predicate'],
['¬', '#f8d7da', 'Negation'],
['∧', '#cfe2ff', 'AND'],
['∨', '#fff3cd', 'OR'],
['→', '#e2d9f3', 'IMPLIES'],
['∀x', '#d4edda', 'Universal'],
['∃x', '#d1ecf1', 'Existential']
];
// Calculate legend dimensions
const legendWidth = items.length * 100 + itemSpacing * (items.length - 1);
const legendHeight = itemHeight + 10;
// Create legend background
let legend = `
<rect x="${legendX}" y="${legendY - legendHeight - 40}"
width="${legendWidth}" height="${legendHeight + 30}"
fill="white" stroke="#ccc" stroke-width="1" rx="5" ry="5" />
<text x="${legendX + 10}" y="${legendY - legendHeight - 20}"
font-family="Arial" font-size="12" font-weight="bold">Legend:</text>
`;
// Add legend items
items.forEach((item, index) => {
const [content, fill, description] = item;
const x = legendX + 50 + index * 100;
const y = legendY - legendHeight;
legend += `
<circle cx="${x - 35}" cy="${y}" r="10" fill="${fill}" stroke="#333" stroke-width="1" />
<text x="${x - 35}" y="${y}" text-anchor="middle" dominant-baseline="middle"
font-family="Arial" font-size="12" font-weight="bold">${content}</text>
<text x="${x}" y="${y}" text-anchor="start" dominant-baseline="middle"
font-family="Arial" font-size="12">${description}</text>
`;
});
return legend;
}
/**
* Format a predicate formula as a string
* @param formula The formula to format
* @returns Formatted string representation
*/
private formatFormula(formula: PredicateFormula): string {
switch (formula.type) {
case 'variable':
return formula.name;
case 'constant':
return formula.name;
case 'function':
if (formula.args.length === 0) {
return formula.name;
} else {
const args = formula.args.map(arg => this.formatFormula(arg)).join(', ');
return `${formula.name}(${args})`;
}
case 'predicate':
if (formula.args.length === 0) {
return formula.name;
} else {
const args = formula.args.map(arg => this.formatFormula(arg)).join(', ');
return `${formula.name}(${args})`;
}
case 'unary':
const unaryOpSymbol = formula.operator === 'not' ? '¬' : formula.operator;
const operand = this.formatFormula(formula.operand);
// Add parentheses if the operand is not a variable, constant, function, or predicate
if (
formula.operand.type !== 'variable' &&
formula.operand.type !== 'constant' &&
formula.operand.type !== 'function' &&
formula.operand.type !== 'predicate'
) {
return `${unaryOpSymbol}(${operand})`;
} else {
return `${unaryOpSymbol}${operand}`;
}
case 'binary':
const left = this.formatFormula(formula.left);
const right = this.formatFormula(formula.right);
// Convert operator to symbol if needed
let binaryOpSymbol: string;
switch (formula.operator) {
case 'and': binaryOpSymbol = '∧'; break;
case 'or': binaryOpSymbol = '∨'; break;
case 'implies': binaryOpSymbol = '→'; break;
case 'iff': binaryOpSymbol = '↔'; break;
default: binaryOpSymbol = formula.operator;
}
// Add parentheses around left operand if needed
const leftStr = (
formula.left.type === 'binary' ||
formula.left.type === 'quantified'
) ? `(${left})` : left;
// Add parentheses around right operand if needed
const rightStr = (
formula.right.type === 'binary' ||
formula.right.type === 'quantified'
) ? `(${right})` : right;
return `${leftStr} ${binaryOpSymbol} ${rightStr}`;
case 'quantified':
const quantSymbol = formula.quantifier === 'forall' ? '∀' :
formula.quantifier === 'exists' ? '∃' :
formula.quantifier;
const subformula = this.formatFormula(formula.formula);
// Add parentheses if the subformula is a binary operation
const formulaStr = formula.formula.type === 'binary' ? `(${subformula})` : subformula;
return `${quantSymbol}${formula.variable}.${formulaStr}`;
default:
return 'Unknown formula type';
}
}
}
