import {
SMTProblem,
SMTVariable,
SMTConstraint,
SMTOptimization
} from '../../types.js';
/**
* Translator from SMT problems to Z3 Python API code
* Generates executable Z3 Python code from CSDL problems
*/
export class Z3Translator {
/**
* Translate SMT problem to Z3 Python code
* @param problem SMT problem
* @returns Z3 Python code
*/
translate(problem: SMTProblem): string {
const lines: string[] = [];
// Add imports
lines.push('from z3 import *');
lines.push('import json');
lines.push('import sys');
lines.push('');
// Declare variables
lines.push('# Declare variables');
lines.push(...this.translateVariables(problem.variables));
lines.push('');
// Create solver or optimizer
if (problem.optimization) {
lines.push('# Create optimizer');
lines.push('solver = Optimize()');
} else {
lines.push('# Create solver');
lines.push('solver = Solver()');
}
lines.push('');
// Add constraints
if (problem.constraints.length > 0) {
lines.push('# Add constraints');
lines.push(...this.translateConstraints(problem.constraints, problem.variables));
lines.push('');
}
// Add optimization
if (problem.optimization) {
lines.push('# Add optimization objective');
lines.push(...this.translateOptimization(problem.optimization, problem.variables));
lines.push('');
}
// Check satisfiability
lines.push('# Check satisfiability');
lines.push('result = solver.check()');
lines.push('');
// Handle result
lines.push('# Output result');
lines.push('if result == sat:');
lines.push(' model = solver.model()');
lines.push(' solution = {}');
for (const variable of problem.variables) {
lines.push(` solution['${variable.name}'] = str(model[${variable.name}])`);
}
lines.push(' output = {');
lines.push(" 'status': 'sat',");
lines.push(" 'model': solution");
lines.push(' }');
if (problem.optimization) {
lines.push(` output['objective_value'] = str(model.evaluate(${problem.optimization.objective}))`);
}
lines.push(' print(json.dumps(output))');
lines.push('elif result == unsat:');
lines.push(' output = {');
lines.push(" 'status': 'unsat',");
lines.push(" 'message': 'No solution exists'");
lines.push(' }');
lines.push(' print(json.dumps(output))');
lines.push('else:');
lines.push(' output = {');
lines.push(" 'status': 'unknown',");
lines.push(" 'reason': solver.reason_unknown()");
lines.push(' }');
lines.push(' print(json.dumps(output))');
return lines.join('\n');
}
/**
* Translate variable declarations
* @param variables List of variables
* @returns Python code lines
*/
private translateVariables(variables: SMTVariable[]): string[] {
const lines: string[] = [];
const groupedByType = new Map<string, string[]>();
// Group variables by type
for (const variable of variables) {
const typeKey = variable.type + (variable.bitWidth ? `_${variable.bitWidth}` : '');
if (!groupedByType.has(typeKey)) {
groupedByType.set(typeKey, []);
}
groupedByType.get(typeKey)!.push(variable.name);
}
// Generate declarations for each type
for (const [typeKey, varNames] of groupedByType) {
const variable = variables.find(v =>
(v.type + (v.bitWidth ? `_${v.bitWidth}` : '')) === typeKey
)!;
if (varNames.length === 1) {
lines.push(this.declareSingleVariable(variable));
} else {
lines.push(this.declareMultipleVariables(variable.type, varNames, variable.bitWidth));
}
}
return lines;
}
/**
* Declare a single variable
* @param variable Variable to declare
* @returns Python code line
*/
private declareSingleVariable(variable: SMTVariable): string {
const z3Type = this.getZ3Type(variable.type, variable.bitWidth);
return `${variable.name} = ${z3Type}('${variable.name}')`;
}
/**
* Declare multiple variables of the same type
* @param type Variable type
* @param names Variable names
* @param bitWidth Bit width for BitVec
* @returns Python code line
*/
private declareMultipleVariables(type: string, names: string[], bitWidth?: number): string {
const z3TypePlural = this.getZ3TypePlural(type, bitWidth);
const nameList = names.join(' ');
const varList = names.join(', ');
return `${varList} = ${z3TypePlural}('${nameList}')`;
}
/**
* Get Z3 type constructor
* @param type Variable type
* @param bitWidth Bit width for BitVec
* @returns Z3 type constructor
*/
private getZ3Type(type: string, bitWidth?: number): string {
switch (type) {
case 'Int': return 'Int';
case 'Real': return 'Real';
case 'Bool': return 'Bool';
case 'String': return 'String';
case 'BitVec': return `BitVec(${bitWidth || 32})`;
case 'Array': return 'Array';
default: return 'Int';
}
}
/**
* Get Z3 plural type constructor
* @param type Variable type
* @param bitWidth Bit width for BitVec
* @returns Z3 plural type constructor
*/
private getZ3TypePlural(type: string, bitWidth?: number): string {
switch (type) {
case 'Int': return 'Ints';
case 'Real': return 'Reals';
case 'Bool': return 'Bools';
case 'BitVec': return `[BitVec('v', ${bitWidth || 32}) for v in ...]`;
default: return 'Ints';
}
}
/**
* Translate constraints
* @param constraints List of constraints
* @param variables List of variables
* @returns Python code lines
*/
private translateConstraints(constraints: SMTConstraint[], variables: SMTVariable[]): string[] {
const lines: string[] = [];
for (const constraint of constraints) {
const z3Expr = this.translateExpression(constraint.expression, variables);
if (constraint.type === 'soft' && constraint.weight) {
lines.push(`solver.add_soft(${z3Expr}, weight=${constraint.weight})`);
} else {
lines.push(`solver.add(${z3Expr})`);
}
}
return lines;
}
/**
* Translate an expression to Z3 syntax
* @param expr Expression string
* @param variables List of variables
* @returns Z3 expression
*/
private translateExpression(expr: string, variables: SMTVariable[]): string {
let z3Expr = expr.trim();
// Replace operators
z3Expr = z3Expr.replace(/\b(and|AND)\b/g, 'And');
z3Expr = z3Expr.replace(/\b(or|OR)\b/g, 'Or');
z3Expr = z3Expr.replace(/\b(not|NOT)\b/g, 'Not');
z3Expr = z3Expr.replace(/\b(implies|IMPLIES)\b/g, 'Implies');
// Handle comparison operators (Z3 uses == not =)
z3Expr = z3Expr.replace(/\s*==\s*/g, ' == ');
z3Expr = z3Expr.replace(/\s*!=\s*/g, ' != ');
z3Expr = z3Expr.replace(/\s*<=\s*/g, ' <= ');
z3Expr = z3Expr.replace(/\s*>=\s*/g, ' >= ');
z3Expr = z3Expr.replace(/\s*<\s*/g, ' < ');
z3Expr = z3Expr.replace(/\s*>\s*/g, ' > ');
// Handle power operator
z3Expr = z3Expr.replace(/\*\*/g, '**');
return z3Expr;
}
/**
* Translate optimization
* @param optimization Optimization goal
* @param variables List of variables
* @returns Python code lines
*/
private translateOptimization(optimization: SMTOptimization, variables: SMTVariable[]): string[] {
const lines: string[] = [];
const objective = this.translateExpression(optimization.objective, variables);
if (optimization.direction === 'maximize') {
lines.push(`solver.maximize(${objective})`);
} else {
lines.push(`solver.minimize(${objective})`);
}
return lines;
}
/**
* Generate complete Python script that can be executed
* @param problem SMT problem
* @returns Complete Python script
*/
generateScript(problem: SMTProblem): string {
const code = this.translate(problem);
return `#!/usr/bin/env python3
"""
Auto-generated Z3 solver script
Generated by logic-thinking MCP server
"""
${code}
`;
}
}
