/**
* Z3 SMT Solver Integration
* Provides TypeScript interface to Z3 theorem prover via Python subprocess
*/
import { spawn, ChildProcess } from 'child_process';
import { resolve, dirname } from 'path';
import { fileURLToPath } from 'url';
import {
Z3Request,
Z3Response,
Z3Variable,
Z3Constraint,
Z3Objective,
Z3Model,
Z3Status
} from './types.js';
// Get directory name in ES modules
const __z3filename = fileURLToPath(import.meta.url);
const __z3dirname = dirname(__z3filename);
/**
* Configuration options for Z3 solver
*/
export interface Z3SolverConfig {
timeout?: number; // Timeout in milliseconds (default: 5000)
pythonPath?: string; // Path to Python interpreter (default: 'python3')
maxSolutions?: number; // Maximum solutions for enumeration (default: 100)
}
/**
* Z3 Solver integration class
* Manages communication with Python Z3 subprocess
*/
export class Z3Solver {
private pythonPath: string;
private scriptPath: string;
private defaultTimeout: number;
private maxSolutions: number;
/**
* Create a new Z3 solver instance
* @param config Configuration options
*/
constructor(config: Z3SolverConfig = {}) {
// Use pyenv Python if available, fallback to system python3
const pyenvPython = '/Users/russellsmith/.pyenv/shims/python3';
this.pythonPath = config.pythonPath || pyenvPython;
this.scriptPath = resolve(__z3dirname, 'z3Solver.py');
this.defaultTimeout = config.timeout || 5000;
this.maxSolutions = config.maxSolutions || 100;
}
/**
* Solve constraint satisfaction problem
* @param variables Variable definitions
* @param constraints Constraint expressions
* @param timeout Optional timeout override
* @returns Solution model or error
*/
async solve(
variables: Z3Variable[],
constraints: Z3Constraint[],
timeout?: number
): Promise<Z3Response> {
const request: Z3Request = {
variables,
constraints,
timeout: timeout || this.defaultTimeout
};
return this.callZ3(request);
}
/**
* Solve optimization problem
* @param variables Variable definitions
* @param constraints Constraint expressions
* @param objective Optimization objective
* @param timeout Optional timeout override
* @returns Optimal solution or error
*/
async optimize(
variables: Z3Variable[],
constraints: Z3Constraint[],
objective: Z3Objective,
timeout?: number
): Promise<Z3Response> {
const request: Z3Request = {
variables,
constraints,
objective,
timeout: timeout || this.defaultTimeout
};
return this.callZ3(request);
}
/**
* Check satisfiability only (without model)
* @param variables Variable definitions
* @param constraints Constraint expressions
* @param timeout Optional timeout override
* @returns Satisfiability status
*/
async checkSat(
variables: Z3Variable[],
constraints: Z3Constraint[],
timeout?: number
): Promise<Z3Status> {
const response = await this.solve(variables, constraints, timeout);
return response.status;
}
/**
* Get satisfying model
* @param variables Variable definitions
* @param constraints Constraint expressions
* @param timeout Optional timeout override
* @returns Solution model or null if unsat
*/
async getModel(
variables: Z3Variable[],
constraints: Z3Constraint[],
timeout?: number
): Promise<Z3Model | null> {
const response = await this.solve(variables, constraints, timeout);
return response.model || null;
}
/**
* Get unsat core (minimal unsatisfiable subset)
* @param variables Variable definitions
* @param constraints Constraint expressions
* @param timeout Optional timeout override
* @returns Unsat core or null if satisfiable
*/
async getUnsatCore(
variables: Z3Variable[],
constraints: Z3Constraint[],
timeout?: number
): Promise<{ constraints: number[]; explanation: string } | null> {
const response = await this.solve(variables, constraints, timeout);
return response.unsatCore || null;
}
/**
* Enumerate all solutions
* @param variables Variable definitions
* @param constraints Constraint expressions
* @param maxSolutions Maximum number of solutions to find
* @param timeout Optional timeout override
* @returns Array of solution models
*/
async enumerateSolutions(
variables: Z3Variable[],
constraints: Z3Constraint[],
maxSolutions?: number,
timeout?: number
): Promise<Z3Model[]> {
const request: Z3Request = {
variables,
constraints,
findAll: true,
maxSolutions: maxSolutions || this.maxSolutions,
timeout: timeout || this.defaultTimeout
};
const response = await this.callZ3(request);
return response.models || (response.model ? [response.model] : []);
}
/**
* Call Z3 solver via Python subprocess
* @param request Z3 request object
* @returns Z3 response object
*/
private async callZ3(request: Z3Request): Promise<Z3Response> {
return new Promise((resolve, reject) => {
// Spawn Python process
const python: ChildProcess = spawn(this.pythonPath, [this.scriptPath]);
let stdout = '';
let stderr = '';
let processTimeout: NodeJS.Timeout;
// Set up timeout
const timeoutMs = request.timeout || this.defaultTimeout;
processTimeout = setTimeout(() => {
python.kill('SIGTERM');
reject(new Error(`Z3 process timeout after ${timeoutMs}ms`));
}, timeoutMs + 1000); // Add 1s buffer for cleanup
// Collect stdout
python.stdout?.on('data', (data: Buffer) => {
stdout += data.toString();
});
// Collect stderr
python.stderr?.on('data', (data: Buffer) => {
stderr += data.toString();
});
// Handle process exit
python.on('close', (code: number | null) => {
clearTimeout(processTimeout);
if (code !== 0 && code !== null) {
reject(new Error(`Z3 process exited with code ${code}: ${stderr}`));
return;
}
// Parse JSON response
try {
const response: Z3Response = JSON.parse(stdout);
resolve(response);
} catch (e) {
reject(new Error(`Failed to parse Z3 output: ${stdout}\nError: ${e}`));
}
});
// Handle process errors
python.on('error', (error: Error) => {
clearTimeout(processTimeout);
reject(new Error(`Failed to spawn Python process: ${error.message}`));
});
// Send request as JSON to stdin
try {
const requestJson = JSON.stringify(request);
python.stdin?.write(requestJson);
python.stdin?.end();
} catch (e) {
clearTimeout(processTimeout);
python.kill();
reject(new Error(`Failed to write to Python process: ${e}`));
}
});
}
/**
* Test Z3 installation and Python script availability
* @returns true if Z3 is available, false otherwise
*/
async testConnection(): Promise<boolean> {
try {
const variables: Z3Variable[] = [{ name: 'x', type: 'Int' }];
const constraints: Z3Constraint[] = [{ expression: 'x > 0' }];
const response = await this.solve(variables, constraints, 1000);
return response.status === 'sat';
} catch (error) {
return false;
}
}
/**
* Get Z3 version information
* @returns Version string or error message
*/
async getVersion(): Promise<string> {
return new Promise((resolve, reject) => {
const python = spawn(this.pythonPath, [
'-c',
'from z3 import get_version_string; print(get_version_string())'
]);
let output = '';
python.stdout?.on('data', (data: Buffer) => {
output += data.toString();
});
python.on('close', (code: number | null) => {
if (code === 0) {
resolve(output.trim());
} else {
reject(new Error('Failed to get Z3 version'));
}
});
python.on('error', (error: Error) => {
reject(new Error(`Failed to check Z3: ${error.message}`));
});
setTimeout(() => {
python.kill();
reject(new Error('Timeout checking Z3 version'));
}, 2000);
});
}
}
/**
* Create a solver instance with default configuration
*/
export function createZ3Solver(config?: Z3SolverConfig): Z3Solver {
return new Z3Solver(config);
}
/**
* Helper function to create integer variable
*/
export function intVar(name: string): Z3Variable {
return { name, type: 'Int' };
}
/**
* Helper function to create real variable
*/
export function realVar(name: string): Z3Variable {
return { name, type: 'Real' };
}
/**
* Helper function to create boolean variable
*/
export function boolVar(name: string): Z3Variable {
return { name, type: 'Bool' };
}
/**
* Helper function to create constraint
*/
export function constraint(expression: string, description?: string): Z3Constraint {
return { expression, description };
}
/**
* Helper function to create maximize objective
*/
export function maximize(expression: string): Z3Objective {
return { expression, direction: 'maximize' };
}
/**
* Helper function to create minimize objective
*/
export function minimize(expression: string): Z3Objective {
return { expression, direction: 'minimize' };
}
