import { SMTProblem, SMTVariable, SMTConstraint } from '../../../types.js';
/**
* Visualizer for SMT problems
* Generates visual representations of constraints and solutions
*/
export class SMTVisualizer {
/**
* Visualize an SMT problem
* @param problem SMT problem
* @returns ASCII art visualization
*/
visualize(problem: SMTProblem): string {
const sections: string[] = [];
// Title
sections.push(this.createTitle('SMT Problem Visualization'));
sections.push('');
// Variables section
sections.push(this.visualizeVariables(problem.variables));
sections.push('');
// Constraints section
sections.push(this.visualizeConstraints(problem.constraints));
sections.push('');
// Optimization section
if (problem.optimization) {
sections.push(this.visualizeOptimization(problem.optimization));
sections.push('');
}
// Constraint graph
sections.push(this.visualizeConstraintGraph(problem));
return sections.join('\n');
}
/**
* Create a title box
* @param title Title text
* @returns Boxed title
*/
private createTitle(title: string): string {
const width = title.length + 4;
const border = '═'.repeat(width);
return `╔${border}╗
║ ${title} ║
╚${border}╝`;
}
/**
* Visualize variables
* @param variables List of variables
* @returns Formatted variable list
*/
private visualizeVariables(variables: SMTVariable[]): string {
const lines: string[] = [];
lines.push('┌─────────────────────┐');
lines.push('│ Variables │');
lines.push('├─────────────────────┤');
for (const variable of variables) {
const typeStr = variable.bitWidth
? `${variable.type}[${variable.bitWidth}]`
: variable.type;
lines.push(`│ ${variable.name}: ${typeStr}`.padEnd(22) + '│');
}
lines.push('└─────────────────────┘');
return lines.join('\n');
}
/**
* Visualize constraints
* @param constraints List of constraints
* @returns Formatted constraint list
*/
private visualizeConstraints(constraints: SMTConstraint[]): string {
const lines: string[] = [];
lines.push('┌─────────────────────────────────────────────┐');
lines.push('│ Constraints │');
lines.push('├─────────────────────────────────────────────┤');
for (let i = 0; i < constraints.length; i++) {
const constraint = constraints[i];
const prefix = constraint.type === 'soft' ? '[SOFT]' : '[HARD]';
const weight = constraint.weight ? ` (w=${constraint.weight})` : '';
// Split long constraints
const maxLen = 37;
if (constraint.expression.length <= maxLen) {
lines.push(`│ ${i + 1}. ${prefix} ${constraint.expression}${weight}`.padEnd(46) + '│');
} else {
const parts = this.splitString(constraint.expression, maxLen);
lines.push(`│ ${i + 1}. ${prefix} ${parts[0]}`.padEnd(46) + '│');
for (let j = 1; j < parts.length; j++) {
lines.push(`│ ${parts[j]}`.padEnd(46) + '│');
}
if (weight) {
lines.push(`│ ${weight}`.padEnd(46) + '│');
}
}
}
lines.push('└─────────────────────────────────────────────┘');
return lines.join('\n');
}
/**
* Visualize optimization goal
* @param optimization Optimization goal
* @returns Formatted optimization
*/
private visualizeOptimization(optimization: any): string {
const lines: string[] = [];
const directive = optimization.direction === 'maximize' ? 'MAXIMIZE' : 'MINIMIZE';
lines.push('┌─────────────────────────────────────────────┐');
lines.push(`│ ${directive}`.padEnd(46) + '│');
lines.push('├─────────────────────────────────────────────┤');
lines.push(`│ ${optimization.objective}`.padEnd(46) + '│');
lines.push('└─────────────────────────────────────────────┘');
return lines.join('\n');
}
/**
* Visualize constraint dependency graph
* @param problem SMT problem
* @returns ASCII constraint graph
*/
private visualizeConstraintGraph(problem: SMTProblem): string {
const lines: string[] = [];
lines.push('┌─────────────────────────────────────────────┐');
lines.push('│ Constraint Graph │');
lines.push('├─────────────────────────────────────────────┤');
lines.push('│ │');
// Build variable dependency map
const varToConstraints = new Map<string, number[]>();
for (const variable of problem.variables) {
varToConstraints.set(variable.name, []);
}
for (let i = 0; i < problem.constraints.length; i++) {
const constraint = problem.constraints[i];
for (const variable of problem.variables) {
if (constraint.expression.includes(variable.name)) {
varToConstraints.get(variable.name)!.push(i + 1);
}
}
}
// Display connections
for (const [varName, constraintIds] of varToConstraints) {
if (constraintIds.length > 0) {
const constraintStr = constraintIds.join(', ');
const line = `│ ${varName} → C${constraintStr}`;
lines.push(line.padEnd(46) + '│');
}
}
lines.push('│ │');
lines.push('└─────────────────────────────────────────────┘');
return lines.join('\n');
}
/**
* Split a string into chunks of maximum length
* @param str String to split
* @param maxLen Maximum length per chunk
* @returns Array of chunks
*/
private splitString(str: string, maxLen: number): string[] {
const chunks: string[] = [];
let remaining = str;
while (remaining.length > 0) {
if (remaining.length <= maxLen) {
chunks.push(remaining);
break;
}
// Try to split at a space
let splitPos = remaining.lastIndexOf(' ', maxLen);
if (splitPos === -1 || splitPos === 0) {
splitPos = maxLen;
}
chunks.push(remaining.substring(0, splitPos));
remaining = remaining.substring(splitPos).trim();
}
return chunks;
}
/**
* Visualize a solution
* @param solution SMT solution
* @returns Formatted solution
*/
visualizeSolution(solution: any): string {
const lines: string[] = [];
lines.push('┌─────────────────────────────────────────────┐');
lines.push('│ Solution │');
lines.push('├─────────────────────────────────────────────┤');
lines.push(`│ Status: ${solution.status.toUpperCase()}`.padEnd(46) + '│');
if (solution.model) {
lines.push('│ │');
lines.push('│ Model: │');
for (const [varName, value] of Object.entries(solution.model)) {
lines.push(`│ ${varName} = ${value}`.padEnd(46) + '│');
}
}
if (solution.objectiveValue !== undefined) {
lines.push('│ │');
lines.push(`│ Objective: ${solution.objectiveValue}`.padEnd(46) + '│');
}
lines.push('└─────────────────────────────────────────────┘');
return lines.join('\n');
}
}
