import { PropositionalFormula, PropositionalArgument, PropositionalOperator } from '../../../types.js';
/**
* Gate types for logic circuits
*/
type GateType = 'AND' | 'OR' | 'NOT' | 'NAND' | 'NOR' | 'XOR' | 'XNOR' | 'BUFFER';
/**
* Node structure for circuit visualization
*/
interface CircuitNode {
id: string;
type: 'input' | 'gate' | 'output';
gateType?: GateType;
label: string;
x: number;
y: number;
inputs: CircuitNode[];
outputs: CircuitNode[];
}
/**
* Logic circuit visualizer for propositional formulas
*/
export class LogicCircuitVisualizer {
private width: number = 800;
private height: number = 600;
private nodeSize: number = 40;
private nodeSpacing: number = 100;
private nodeCounter: number = 0;
/**
* Generate a logic circuit visualization for a propositional formula
* @param input Formula or argument to visualize
* @param format Output format
* @returns Circuit visualization string
*/
visualize(
input: PropositionalFormula | PropositionalArgument,
format: 'html' | 'svg' | 'text' = 'svg'
): string {
let rootFormula: PropositionalFormula;
if ('premises' in input) {
// For arguments, combine premises with implication to conclusion
const combinedPremises = this.combinePremises(input.premises);
rootFormula = {
type: 'binary',
operator: 'implies',
left: combinedPremises,
right: input.conclusion
};
} else {
rootFormula = input;
}
switch (format) {
case 'html':
return this.generateHTML(rootFormula);
case 'svg':
return this.generateSVG(rootFormula);
case 'text':
return this.generateText(rootFormula);
default:
return this.generateSVG(rootFormula);
}
}
/**
* Combine multiple premises into a single formula using AND operations
* @param premises Array of formulas
* @returns Combined formula
*/
private combinePremises(premises: PropositionalFormula[]): PropositionalFormula {
if (premises.length === 0) {
throw new Error('No premises provided');
}
if (premises.length === 1) {
return premises[0];
}
let result = premises[0];
for (let i = 1; i < premises.length; i++) {
result = {
type: 'binary',
operator: 'and',
left: result,
right: premises[i]
};
}
return result;
}
/**
* Generate HTML visualization with interactive circuit
* @param formula Formula to visualize
* @returns HTML string
*/
private generateHTML(formula: PropositionalFormula): string {
const circuit = this.buildCircuit(formula);
const svg = this.generateSVGContent(circuit);
return `
<div class="logic-circuit-container">
<style>
.logic-circuit-container {
font-family: Arial, sans-serif;
padding: 20px;
background-color: #f8f9fa;
border-radius: 10px;
box-shadow: 0 2px 4px rgba(0,0,0,0.1);
}
.circuit-svg {
background-color: white;
border: 1px solid #dee2e6;
border-radius: 5px;
cursor: default;
}
.gate {
cursor: pointer;
transition: opacity 0.3s;
}
.gate:hover {
opacity: 0.8;
}
.wire {
transition: stroke-width 0.3s;
}
.wire:hover {
stroke-width: 3;
}
.circuit-controls {
margin-top: 20px;
padding: 10px;
background-color: #e9ecef;
border-radius: 5px;
}
.control-button {
padding: 5px 10px;
margin-right: 10px;
background-color: #007bff;
color: white;
border: none;
border-radius: 3px;
cursor: pointer;
}
.control-button:hover {
background-color: #0056b3;
}
</style>
<h3>Logic Circuit Visualization</h3>
${svg}
<div class="circuit-controls">
<button class="control-button" onclick="switchToCanonicalForm()">Canonical Form</button>
<button class="control-button" onclick="simplifyCircuit()">Simplify</button>
<button class="control-button" onclick="showTruthTable()">Truth Table</button>
</div>
<script>
function switchToCanonicalForm() {
alert('Canonical form conversion coming soon!');
}
function simplifyCircuit() {
alert('Circuit simplification coming soon!');
}
function showTruthTable() {
alert('Truth table generation coming soon!');
}
</script>
</div>
`;
}
/**
* Generate SVG visualization of the circuit
* @param formula Formula to visualize
* @returns SVG string
*/
private generateSVG(formula: PropositionalFormula): string {
const circuit = this.buildCircuit(formula);
return `<svg width="${this.width}" height="${this.height}" xmlns="http://www.w3.org/2000/svg" class="circuit-svg">
${this.generateSVGContent(circuit)}
</svg>`;
}
/**
* Generate SVG content for the circuit
* @param circuit Root node of the circuit
* @returns SVG content string
*/
private generateSVGContent(circuit: CircuitNode): string {
let svg = '';
// Background
svg += `<rect x="0" y="0" width="100%" height="100%" fill="white" />\n`;
// Draw wires first (so they're behind gates)
svg += '<g class="wires">\n';
svg += this.drawWires(circuit);
svg += '</g>\n';
// Draw gates and labels
svg += '<g class="gates">\n';
svg += this.drawGates(circuit);
svg += '</g>\n';
return svg;
}
/**
* Build circuit structure from formula
* @param formula Formula to convert
* @returns Root circuit node
*/
private buildCircuit(formula: PropositionalFormula): CircuitNode {
// Extract variables
const variables = this.extractVariables(formula);
const inputNodes = new Map<string, CircuitNode>();
// Create input nodes
variables.forEach((variable, index) => {
const node: CircuitNode = {
id: `input_${this.nodeCounter++}`,
type: 'input',
label: variable,
x: 50,
y: 100 + index * this.nodeSpacing,
inputs: [],
outputs: []
};
inputNodes.set(variable, node);
});
// Build circuit from formula
const resultNode = this.buildFormulaCircuit(formula, inputNodes);
// Create a separate output node and connect the result to it
const outputNode: CircuitNode = {
id: 'output',
type: 'output',
label: 'Output',
x: 0, // Will be positioned by layout
y: 0, // Will be positioned by layout
inputs: [resultNode],
outputs: []
};
// Add output to result node's outputs
resultNode.outputs.push(outputNode);
// Adjust layout
this.layoutCircuit(outputNode);
return outputNode;
}
/**
* Build circuit for a formula recursively
* @param formula Formula to process
* @param inputNodes Map of variable names to input nodes
* @returns Circuit node representing the formula
*/
private buildFormulaCircuit(
formula: PropositionalFormula,
inputNodes: Map<string, CircuitNode>
): CircuitNode {
switch (formula.type) {
case 'variable':
const inputNode = inputNodes.get(formula.name);
if (!inputNode) {
throw new Error(`Variable ${formula.name} not found in input nodes`);
}
return inputNode;
case 'unary':
const operandNode = this.buildFormulaCircuit(formula.operand, inputNodes);
const notGate: CircuitNode = {
id: `not_${this.nodeCounter++}`,
type: 'gate',
gateType: this.getGateType(formula.operator),
label: this.getGateLabel(formula.operator),
x: operandNode.x + this.nodeSpacing,
y: operandNode.y,
inputs: [operandNode],
outputs: []
};
operandNode.outputs.push(notGate);
return notGate;
case 'binary':
const leftNode = this.buildFormulaCircuit(formula.left, inputNodes);
const rightNode = this.buildFormulaCircuit(formula.right, inputNodes);
const binaryGate: CircuitNode = {
id: `${formula.operator}_${this.nodeCounter++}`,
type: 'gate',
gateType: this.getGateType(formula.operator),
label: this.getGateLabel(formula.operator),
x: Math.max(leftNode.x, rightNode.x) + this.nodeSpacing,
y: (leftNode.y + rightNode.y) / 2,
inputs: [leftNode, rightNode],
outputs: []
};
leftNode.outputs.push(binaryGate);
rightNode.outputs.push(binaryGate);
return binaryGate;
}
throw new Error(`Unknown formula type: ${(formula as any).type}`);
}
/**
* Get gate type for operator
* @param operator Propositional operator
* @returns Gate type
*/
private getGateType(operator: PropositionalOperator): GateType {
switch (operator) {
case 'and':
case '∧':
return 'AND';
case 'or':
case '∨':
return 'OR';
case 'not':
case '¬':
return 'NOT';
case 'implies':
case '→':
// A → B is equivalent to ¬A ∨ B
return 'OR';
case 'iff':
case '↔':
return 'XNOR';
case 'xor':
case '⊕':
return 'XOR';
default:
return 'BUFFER';
}
}
/**
* Get gate label for operator
* @param operator Propositional operator
* @returns Gate label
*/
private getGateLabel(operator: PropositionalOperator): string {
switch (operator) {
case 'and':
case '∧':
return 'AND';
case 'or':
case '∨':
return 'OR';
case 'not':
case '¬':
return 'NOT';
case 'implies':
case '→':
return 'IMP';
case 'iff':
case '↔':
return 'IFF';
case 'xor':
case '⊕':
return 'XOR';
default:
return operator;
}
}
/**
* Extract all variables from formula
* @param formula Formula to analyze
* @returns Array of unique variable names
*/
private extractVariables(formula: PropositionalFormula): string[] {
const variables = new Set<string>();
const extract = (f: PropositionalFormula): void => {
if (f.type === 'variable') {
variables.add(f.name);
} else if (f.type === 'unary') {
extract(f.operand);
} else if (f.type === 'binary') {
extract(f.left);
extract(f.right);
}
};
extract(formula);
return Array.from(variables).sort();
}
/**
* Layout circuit nodes for optimal visualization
* @param root Root node of the circuit
*/
private layoutCircuit(root: CircuitNode): void {
// Simple left-to-right layout algorithm
const layers = this.calculateLayers(root);
const maxLayer = Math.max(...layers.keys());
// Calculate positions for each layer
layers.forEach((nodes, layer) => {
const x = 50 + layer * (this.nodeSpacing * 1.5);
const startY = (this.height - (nodes.length - 1) * this.nodeSpacing) / 2;
nodes.forEach((node, index) => {
if (node.type !== 'input') {
node.x = x;
node.y = startY + index * this.nodeSpacing;
}
});
});
// Position the output node at the rightmost position
if (root.type === 'output') {
root.x = 50 + (maxLayer + 1) * (this.nodeSpacing * 1.5);
}
}
/**
* Calculate layer depth for each node
* @param root Root node
* @returns Map of layer to nodes
*/
private calculateLayers(root: CircuitNode): Map<number, CircuitNode[]> {
const layers = new Map<number, CircuitNode[]>();
const visited = new Set<string>();
const traverse = (node: CircuitNode, layer: number): void => {
if (visited.has(node.id)) return;
visited.add(node.id);
if (!layers.has(layer)) {
layers.set(layer, []);
}
layers.get(layer)!.push(node);
node.inputs.forEach(input => {
traverse(input, layer - 1);
});
};
traverse(root, 0);
// Normalize layer numbers to start from 0
const minLayer = Math.min(...layers.keys());
const normalizedLayers = new Map<number, CircuitNode[]>();
layers.forEach((nodes, layer) => {
normalizedLayers.set(layer - minLayer, nodes);
});
return normalizedLayers;
}
/**
* Draw gates on the SVG
* @param root Root node of the circuit
* @returns SVG string
*/
private drawGates(root: CircuitNode): string {
let svg = '';
const visited = new Set<string>();
const traverse = (node: CircuitNode): void => {
if (visited.has(node.id)) return;
visited.add(node.id);
// Draw the node
svg += this.drawNode(node);
// Traverse input nodes
node.inputs.forEach(input => traverse(input));
};
traverse(root);
return svg;
}
/**
* Draw a single node
* @param node Node to draw
* @returns SVG string
*/
private drawNode(node: CircuitNode): string {
let svg = '';
switch (node.type) {
case 'input':
svg += `<circle cx="${node.x}" cy="${node.y}" r="${this.nodeSize/3}" fill="#28a745" stroke="#218838" stroke-width="2" />\n`;
svg += `<text x="${node.x}" y="${node.y - 25}" text-anchor="middle" font-family="Arial" font-size="14" font-weight="bold">${node.label}</text>\n`;
break;
case 'output':
svg += `<circle cx="${node.x}" cy="${node.y}" r="${this.nodeSize/3}" fill="#dc3545" stroke="#c82333" stroke-width="2" />\n`;
svg += `<text x="${node.x}" y="${node.y - 25}" text-anchor="middle" font-family="Arial" font-size="14" font-weight="bold">${node.label}</text>\n`;
break;
case 'gate':
svg += this.drawGate(node);
break;
}
return svg;
}
/**
* Draw a logic gate
* @param node Gate node
* @returns SVG string
*/
private drawGate(node: CircuitNode): string {
let svg = '';
const gateWidth = this.nodeSize;
const gateHeight = this.nodeSize * 0.8;
switch (node.gateType) {
case 'AND':
// Draw AND gate shape (D-shaped)
svg += `<path d="M ${node.x - gateWidth/2} ${node.y - gateHeight/2}
L ${node.x} ${node.y - gateHeight/2}
A ${gateWidth/2} ${gateHeight/2} 0 0 1 ${node.x} ${node.y + gateHeight/2}
L ${node.x - gateWidth/2} ${node.y + gateHeight/2} Z"
fill="#3498db" stroke="#2980b9" stroke-width="2" />\n`;
break;
case 'OR':
// Draw OR gate shape (convex)
svg += `<path d="M ${node.x - gateWidth/2} ${node.y - gateHeight/2}
Q ${node.x - gateWidth/4} ${node.y} ${node.x - gateWidth/2} ${node.y + gateHeight/2}
Q ${node.x} ${node.y} ${node.x + gateWidth/2} ${node.y - gateHeight/4}
Q ${node.x} ${node.y} ${node.x + gateWidth/2} ${node.y + gateHeight/4}
Q ${node.x} ${node.y} ${node.x - gateWidth/2} ${node.y + gateHeight/2} Z"
fill="#e74c3c" stroke="#c0392b" stroke-width="2" />\n`;
break;
case 'NOT':
// Draw NOT gate shape (triangle with circle)
svg += `<path d="M ${node.x - gateWidth/2} ${node.y - gateHeight/2}
L ${node.x + gateWidth/2 - 8} ${node.y}
L ${node.x - gateWidth/2} ${node.y + gateHeight/2} Z"
fill="#9b59b6" stroke="#8e44ad" stroke-width="2" />\n`;
svg += `<circle cx="${node.x + gateWidth/2 - 4}" cy="${node.y}" r="4" fill="#9b59b6" stroke="#8e44ad" stroke-width="2" />\n`;
break;
case 'XOR':
// Draw XOR gate shape (OR with extra line)
svg += `<path d="M ${node.x - gateWidth/2 - 4} ${node.y - gateHeight/2}
Q ${node.x - gateWidth/4 - 4} ${node.y} ${node.x - gateWidth/2 - 4} ${node.y + gateHeight/2}"
fill="none" stroke="#f39c12" stroke-width="2" />\n`;
svg += `<path d="M ${node.x - gateWidth/2} ${node.y - gateHeight/2}
Q ${node.x - gateWidth/4} ${node.y} ${node.x - gateWidth/2} ${node.y + gateHeight/2}
Q ${node.x} ${node.y} ${node.x + gateWidth/2} ${node.y - gateHeight/4}
Q ${node.x} ${node.y} ${node.x + gateWidth/2} ${node.y + gateHeight/4}
Q ${node.x} ${node.y} ${node.x - gateWidth/2} ${node.y + gateHeight/2} Z"
fill="#f39c12" stroke="#d35400" stroke-width="2" />\n`;
break;
case 'NAND':
// Draw NAND gate shape (AND with circle)
svg += `<path d="M ${node.x - gateWidth/2} ${node.y - gateHeight/2}
L ${node.x - 8} ${node.y - gateHeight/2}
A ${gateWidth/2 - 8} ${gateHeight/2} 0 0 1 ${node.x - 8} ${node.y + gateHeight/2}
L ${node.x - gateWidth/2} ${node.y + gateHeight/2} Z"
fill="#3498db" stroke="#2980b9" stroke-width="2" />\n`;
svg += `<circle cx="${node.x + gateWidth/2 - 4}" cy="${node.y}" r="4" fill="#3498db" stroke="#2980b9" stroke-width="2" />\n`;
break;
case 'NOR':
// Draw NOR gate shape (OR with circle)
svg += `<path d="M ${node.x - gateWidth/2} ${node.y - gateHeight/2}
Q ${node.x - gateWidth/4} ${node.y} ${node.x - gateWidth/2} ${node.y + gateHeight/2}
Q ${node.x} ${node.y} ${node.x + gateWidth/2 - 8} ${node.y - gateHeight/4}
Q ${node.x} ${node.y} ${node.x + gateWidth/2 - 8} ${node.y + gateHeight/4}
Q ${node.x} ${node.y} ${node.x - gateWidth/2} ${node.y + gateHeight/2} Z"
fill="#e74c3c" stroke="#c0392b" stroke-width="2" />\n`;
svg += `<circle cx="${node.x + gateWidth/2 - 4}" cy="${node.y}" r="4" fill="#e74c3c" stroke="#c0392b" stroke-width="2" />\n`;
break;
case 'XNOR':
// Draw XNOR gate shape (XOR with circle)
svg += `<path d="M ${node.x - gateWidth/2 - 4} ${node.y - gateHeight/2}
Q ${node.x - gateWidth/4 - 4} ${node.y} ${node.x - gateWidth/2 - 4} ${node.y + gateHeight/2}"
fill="none" stroke="#f39c12" stroke-width="2" />\n`;
svg += `<path d="M ${node.x - gateWidth/2} ${node.y - gateHeight/2}
Q ${node.x - gateWidth/4} ${node.y} ${node.x - gateWidth/2} ${node.y + gateHeight/2}
Q ${node.x} ${node.y} ${node.x + gateWidth/2 - 8} ${node.y - gateHeight/4}
Q ${node.x} ${node.y} ${node.x + gateWidth/2 - 8} ${node.y + gateHeight/4}
Q ${node.x} ${node.y} ${node.x - gateWidth/2} ${node.y + gateHeight/2} Z"
fill="#f39c12" stroke="#d35400" stroke-width="2" />\n`;
svg += `<circle cx="${node.x + gateWidth/2 - 4}" cy="${node.y}" r="4" fill="#f39c12" stroke="#d35400" stroke-width="2" />\n`;
break;
default:
// Default rectangle gate
svg += `<rect x="${node.x - gateWidth/2}" y="${node.y - gateHeight/2}"
width="${gateWidth}" height="${gateHeight}"
fill="#95a5a6" stroke="#7f8c8d" stroke-width="2" rx="5" />\n`;
}
// Add label
svg += `<text x="${node.x}" y="${node.y + 5}" text-anchor="middle" font-family="Arial"
font-size="12" font-weight="bold" fill="white">${node.label}</text>\n`;
return svg;
}
/**
* Draw wires connecting gates
* @param root Root node of the circuit
* @returns SVG string
*/
private drawWires(root: CircuitNode): string {
let svg = '';
const visited = new Set<string>();
const traverse = (node: CircuitNode): void => {
if (visited.has(node.id)) return;
visited.add(node.id);
// Draw wires to input nodes
node.inputs.forEach(input => {
svg += this.drawWire(input, node);
traverse(input);
});
};
traverse(root);
return svg;
}
/**
* Draw a wire between two nodes
* @param from Source node
* @param to Target node
* @returns SVG string
*/
private drawWire(from: CircuitNode, to: CircuitNode): string {
let fromX = from.x;
let fromY = from.y;
let toX = to.x;
let toY = to.y;
// Adjust connection points based on node type
if (from.type === 'gate') {
fromX += this.nodeSize / 2;
} else {
fromX += this.nodeSize / 3;
}
if (to.type === 'gate') {
toX -= this.nodeSize / 2;
} else {
toX -= this.nodeSize / 3;
}
// Use a curved path for better visibility
const controlPointX = (fromX + toX) / 2;
const controlPointY = (fromY + toY) / 2;
const path = `M ${fromX} ${fromY} Q ${controlPointX} ${fromY} ${controlPointX} ${controlPointY}
T ${toX} ${toY}`;
return `<path d="${path}" fill="none" stroke="#34495e" stroke-width="2" class="wire" />\n`;
}
/**
* Generate text visualization of the circuit
* @param formula Formula to visualize
* @returns Text string
*/
private generateText(formula: PropositionalFormula): string {
let text = 'Logic Circuit Structure\n';
text += '=====================\n\n';
const circuit = this.buildCircuit(formula);
const components = this.analyzeCircuit(circuit);
text += `Total components: ${components.totalGates + components.inputs.length + components.outputs.length}\n`;
text += `Inputs: ${components.inputs.length} (${components.inputs.join(', ')})\n`;
text += `Gates: ${components.totalGates}\n`;
text += ' - ' + components.gateBreakdown.map(g => `${g.type}: ${g.count}`).join('\n - ') + '\n';
text += `Outputs: ${components.outputs.length} (${components.outputs.join(', ')})\n\n`;
text += 'Circuit Structure:\n';
text += this.generateCircuitDescription(circuit, 0);
return text;
}
/**
* Analyze circuit structure for statistics
* @param root Root node
* @returns Circuit analysis
*/
private analyzeCircuit(root: CircuitNode): {
inputs: string[];
outputs: string[];
gateBreakdown: Array<{ type: GateType; count: number }>;
totalGates: number;
} {
const inputs: string[] = [];
const outputs: string[] = [];
const gates = new Map<GateType, number>();
const visited = new Set<string>();
const traverse = (node: CircuitNode): void => {
if (visited.has(node.id)) return;
visited.add(node.id);
if (node.type === 'input') {
inputs.push(node.label);
} else if (node.type === 'output') {
outputs.push(node.label);
} else if (node.type === 'gate' && node.gateType) {
gates.set(node.gateType, (gates.get(node.gateType) || 0) + 1);
}
node.inputs.forEach(input => traverse(input));
};
traverse(root);
const gateBreakdown = Array.from(gates.entries()).map(([type, count]) => ({ type, count }));
const totalGates = gateBreakdown.reduce((sum, g) => sum + g.count, 0);
return {
inputs,
outputs,
gateBreakdown,
totalGates
};
}
/**
* Generate text description of circuit structure
* @param node Current node
* @param depth Indentation depth
* @returns Text description
*/
private generateCircuitDescription(node: CircuitNode, depth: number): string {
const indent = ' '.repeat(depth);
let text = '';
text += `${indent}${node.type.toUpperCase()}: ${node.label}`;
if (node.type === 'gate') {
text += ` (${node.gateType})`;
}
text += '\n';
if (node.inputs.length > 0) {
text += `${indent} Inputs:\n`;
node.inputs.forEach(input => {
text += this.generateCircuitDescription(input, depth + 2);
});
}
return text;
}
}
