import { PropositionalFormula } from '../../../types.js';
/**
* Parse Tree Visualizer for propositional logic formulas
* Creates SVG visualizations of formula structure as a tree
*/
export class ParseTreeVisualizer {
// SVG dimensions and spacing
private width = 800;
private height = 600;
private nodeRadius = 25;
private levelHeight = 80;
private horizontalSpacing = 50;
private margin = 40;
/**
* Generate a parse tree visualization for a propositional formula
* @param formula The formula to visualize
* @returns SVG string representation of the parse tree
*/
generateParseTree(formula: PropositionalFormula): 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(400, 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: PropositionalFormula): number {
if (formula.type === 'variable') {
return 1;
} else if (formula.type === 'unary') {
return 1 + this.calculateTreeDepth(formula.operand);
} else if (formula.type === 'binary') {
return 1 + Math.max(
this.calculateTreeDepth(formula.left),
this.calculateTreeDepth(formula.right)
);
}
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: PropositionalFormula): number {
if (formula.type === 'variable') {
return 1;
} else if (formula.type === 'unary') {
return this.calculateTreeWidth(formula.operand);
} else if (formula.type === 'binary') {
return this.calculateTreeWidth(formula.left) + this.calculateTreeWidth(formula.right);
}
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: PropositionalFormula,
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 = '';
if (formula.type === 'variable') {
// Variable node
nodeContent = formula.name;
nodeFill = '#d1e7dd'; // Light green for variables
} else if (formula.type === 'unary') {
// Unary operator node (negation)
nodeContent = formula.operator === 'not' ? '¬' : formula.operator;
nodeFill = '#f8d7da'; // Light red for negation
// Create child node (operand)
const childY = y + this.levelHeight;
const childX = x; // Unary operators have one child directly below
const childResult = this.createTreeElements(
formula.operand,
childX,
childY,
level + 1,
nextNodeId,
nodeMap
);
nodes.push(...childResult.nodes);
links.push(...childResult.links);
// Add link to child
const childNodeId = nextNodeId;
const childPos = nodeMap.get(childNodeId);
if (childPos) {
links.push(this.createLink(x, y, childPos.x, childPos.y));
}
nextNodeId = childResult.nextNodeId;
totalWidth = childResult.width;
} else if (formula.type === 'binary') {
// Binary operator node
const binaryFormula = formula; // Create a constant to help TypeScript narrow the type
switch (binaryFormula.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;
case 'xor':
case '⊕':
nodeContent = '⊕';
nodeFill = '#f3d9e2'; // Light pink for XOR
break;
default:
nodeContent = binaryFormula.operator as string;
nodeFill = '#f0f0f0'; // Light gray for unknown operators
}
// Calculate child positions
const leftWidth = this.calculateTreeWidth(binaryFormula.left);
const rightWidth = this.calculateTreeWidth(binaryFormula.right);
totalWidth = leftWidth + rightWidth;
// Calculate horizontal spacing based on the tree width
const spacing = this.horizontalSpacing * Math.max(3, Math.min(10, totalWidth));
// Create left child
const leftX = x - spacing / 2;
const leftY = y + this.levelHeight;
const leftResult = this.createTreeElements(
binaryFormula.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 + spacing / 2;
const rightY = y + this.levelHeight;
const rightResult = this.createTreeElements(
binaryFormula.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;
}
// 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="18" 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 itemWidth = 120;
const itemSpacing = 5;
// Legend items: [content, fill color, description]
const items: [string, string, string][] = [
['p', '#d1e7dd', 'Variable'],
['¬', '#f8d7da', 'Negation'],
['∧', '#cfe2ff', 'AND'],
['∨', '#fff3cd', 'OR'],
['→', '#e2d9f3', 'IMPLIES'],
['↔', '#d9f3e2', 'IFF'],
['⊕', '#f3d9e2', 'XOR']
];
// Calculate legend dimensions
const legendWidth = items.length * (itemWidth + itemSpacing);
const legendHeight = itemHeight + 10;
let legend = `
<rect x="${legendX}" y="${legendY - legendHeight}"
width="${legendWidth}" height="${legendHeight}"
fill="white" stroke="#ccc" stroke-width="1" rx="5" ry="5" />
<text x="${legendX + 10}" y="${legendY - legendHeight + 15}"
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 + 70 + index * (itemWidth + itemSpacing);
const y = legendY - legendHeight/2;
legend += `
<circle cx="${x - 50}" cy="${y}" r="10" fill="${fill}" stroke="#333" stroke-width="1" />
<text x="${x - 50}" 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 propositional formula as a string
* @param formula The formula to format
* @returns Formatted string representation
*/
private formatFormula(formula: PropositionalFormula): string {
switch (formula.type) {
case 'variable':
return formula.name;
case 'unary':
const unaryOpSymbol = formula.operator === 'not' ? '¬' : formula.operator;
const operand = this.formatFormula(formula.operand);
// Add parentheses if the operand is not a variable or another negation
if (formula.operand.type === 'binary') {
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;
case 'xor': binaryOpSymbol = '⊕'; break;
default: binaryOpSymbol = formula.operator;
}
// Add parentheses around left operand if needed
const leftStr = (formula.left.type === 'binary' &&
this.getOperatorPrecedence(formula.left.operator) <
this.getOperatorPrecedence(formula.operator))
? `(${left})`
: left;
// Add parentheses around right operand if needed
const rightStr = (formula.right.type === 'binary' &&
this.getOperatorPrecedence(formula.right.operator) <=
this.getOperatorPrecedence(formula.operator))
? `(${right})`
: right;
return `${leftStr} ${binaryOpSymbol} ${rightStr}`;
}
throw new Error(`Unknown formula type`);
}
/**
* Get the precedence level of an operator
* Higher numbers indicate higher precedence
* @param operator The operator
* @returns Precedence level (number)
*/
private getOperatorPrecedence(operator: string): number {
switch (operator) {
case 'not':
case '¬':
return 4;
case 'and':
case '∧':
return 3;
case 'or':
case '∨':
return 2;
case 'implies':
case '→':
return 1;
case 'iff':
case '↔':
case 'xor':
case '⊕':
return 0;
default:
return 0;
}
}
}
