import {
LogicalSystem,
Operation,
InputFormat,
LogicResult,
SMTProblem,
SMTSolution,
SMTVariable,
SMTConstraint,
SMTOptimization
} from '../types.js';
// Import validators, formatters, and translators
import { SMTValidator } from './smt/smtValidator.js';
import { SMTFormatter } from './smt/smtFormatter.js';
import { Z3Translator } from './smt/z3Translator.js';
import { SMTVisualizer } from './visualization/smt/smtVisualizer.js';
import { Z3Solver } from './smt/z3Integration.js';
import { Loggers } from '../utils/logger.js';
const logger = Loggers.manager;
/**
* SMT (Satisfiability Modulo Theories) Logic System
* Handles constraint solving via Z3 theorem prover
*/
export class SMTLogic {
private validator: SMTValidator;
private formatter: SMTFormatter;
private translator: Z3Translator;
private visualizer: SMTVisualizer;
private z3Solver: Z3Solver;
constructor() {
this.validator = new SMTValidator();
this.formatter = new SMTFormatter();
this.translator = new Z3Translator();
this.visualizer = new SMTVisualizer();
this.z3Solver = new Z3Solver();
}
/**
* Main entry point for SMT logic operations
* @param operation The operation to perform
* @param input Input text or structured data
* @param format Input format
* @returns Operation result
*/
async process(
operation: Operation,
input: string | SMTProblem,
format: InputFormat = 'natural'
): Promise<LogicResult> {
try {
logger.info('Processing SMT operation', { operation, format });
// Parse the input if it's a string
const problem = typeof input === 'string'
? this.parseInput(input, format)
: input;
// Perform the requested operation
switch (operation) {
case 'validate':
return this.validate(problem);
case 'formalize':
return this.formalize(problem);
case 'visualize':
return this.visualize(problem);
case 'solve':
return await this.solve(problem);
default:
throw new Error(`Unsupported operation: ${operation}`);
}
} catch (error) {
logger.error('SMT processing error', { error });
return {
status: 'error',
message: error instanceof Error ? error.message : 'Unknown error',
details: {
system: 'smt' as LogicalSystem
}
};
}
}
/**
* Parse input text into structured SMT problem
* @param input Input text
* @param format Input format
* @returns Parsed SMT problem
*/
private parseInput(input: string, format: InputFormat): SMTProblem {
logger.debug('Parsing SMT input', { format, inputLength: input.length });
if (format === 'natural') {
// Natural language to CSDL/SMT conversion
return this.naturalLanguageToSMT(input);
} else if (format === 'symbolic') {
// Parse symbolic CSDL format
return this.symbolicToSMT(input);
} else {
// Mixed format - try natural first, fallback to symbolic
try {
return this.naturalLanguageToSMT(input);
} catch (e) {
return this.symbolicToSMT(input);
}
}
}
/**
* Convert natural language to SMT problem
* @param input Natural language input
* @returns SMT problem
*/
private naturalLanguageToSMT(input: string): SMTProblem {
const lowerInput = input.toLowerCase();
// Extract variables
const allVariables = this.extractVariables(input);
// Extract constraints
const constraints = this.extractConstraints(input, allVariables);
// Extract optimization goal if present
const optimization = this.extractOptimization(input, allVariables);
// Filter variables to only those used in constraints or optimization
const usedVarNames = new Set<string>();
for (const constraint of constraints) {
const expr = constraint.expression;
for (const v of allVariables) {
if (new RegExp(`\\b${v.name}\\b`).test(expr)) {
usedVarNames.add(v.name);
}
}
}
if (optimization) {
const expr = optimization.objective;
for (const v of allVariables) {
if (new RegExp(`\\b${v.name}\\b`).test(expr)) {
usedVarNames.add(v.name);
}
}
}
const variables = allVariables.filter(v => usedVarNames.has(v.name));
return {
variables,
constraints,
optimization
};
}
/**
* Extract variables from natural language
* @param input Input text
* @returns List of SMT variables
*/
private extractVariables(input: string): SMTVariable[] {
const variables: SMTVariable[] = [];
const lowerInput = input.toLowerCase();
// Match patterns like "x and y", "variables x, y, z", "integers x and y"
const varPatterns = [
/(?:variables?|find|let)\s+([a-z](?:\s*,\s*[a-z]|\s+and\s+[a-z])*)/gi,
/(?:integers?|reals?|numbers?)\s+([a-z])\s+(?:and|,)\s+([a-z])/gi,
/\b([a-z])\s+(?:is|=|>|<|>=|<=|!=)/gi,
/\b([a-z])\s*\+\s*([a-z])/gi
];
const varSet = new Set<string>();
for (const pattern of varPatterns) {
const matches = input.matchAll(pattern);
for (const match of matches) {
// Skip the full match (index 0), process captured groups
for (let i = 1; i < match.length; i++) {
if (match[i]) {
// Extract individual variable names
const varNames = match[i].split(/[\s,]+/).filter(v => v && v !== 'and' && /^[a-z]$/i.test(v));
varNames.forEach(name => varSet.add(name.toLowerCase()));
}
}
}
}
// Determine variable types from context
for (const varName of varSet) {
const type = this.inferVariableType(input, varName);
variables.push({
name: varName,
type
});
}
// If no variables found, look for implicit variables in expressions
if (variables.length === 0) {
// Match single letters that appear in mathematical contexts
const implicitVars = input.match(/\b[a-z]\b/gi);
if (implicitVars) {
const uniqueVars = [...new Set(implicitVars.map(v => v.toLowerCase()))];
for (const varName of uniqueVars) {
variables.push({
name: varName,
type: this.inferVariableType(input, varName)
});
}
}
}
return variables;
}
/**
* Infer variable type from context
* @param input Input text
* @param varName Variable name
* @returns Variable type
*/
private inferVariableType(input: string, varName: string): 'Int' | 'Real' | 'Bool' {
const lowerInput = input.toLowerCase();
// Check for explicit type keywords
if (lowerInput.includes(`${varName} is a boolean`) ||
lowerInput.includes(`${varName} is true`) ||
lowerInput.includes(`${varName} is false`)) {
return 'Bool';
}
if (lowerInput.includes('real') || lowerInput.includes('decimal') ||
lowerInput.includes('float') || input.includes(`${varName}`) && input.includes('.')) {
return 'Real';
}
if (lowerInput.includes('integer') || lowerInput.includes('whole number')) {
return 'Int';
}
// Default to Int for numeric contexts
return 'Int';
}
/**
* Extract constraints from natural language
* @param input Input text
* @param variables Known variables
* @returns List of constraints
*/
private extractConstraints(input: string, variables: SMTVariable[]): SMTConstraint[] {
const constraints: SMTConstraint[] = [];
// Extract "such that" clause if present
const suchThatMatch = input.match(/such\s+that\s+(.+?)(?:$|\.)/i);
let constraintText = suchThatMatch ? suchThatMatch[1] : input;
// Split by "and" but only when it separates equations/constraints
// Look for patterns like "x + y = 10 and x - y = 4"
const parts = constraintText.split(/\s+and\s+(?=[a-z]\s*[+\-*/]|[a-z]\s*[<>=])/i);
for (const part of parts) {
const trimmed = part.trim();
if (!trimmed || trimmed.length < 3) continue;
try {
const expr = this.sentenceToExpression(trimmed, variables);
if (expr) {
constraints.push({
type: 'constraint',
expression: expr
});
}
} catch (e) {
logger.debug('Failed to parse sentence as constraint', { sentence: trimmed });
}
}
return constraints;
}
/**
* Convert a sentence to a mathematical expression
* @param sentence Input sentence
* @param variables Known variables
* @returns Expression string or null
*/
private sentenceToExpression(sentence: string, variables: SMTVariable[]): string | null {
let expr = sentence.toLowerCase().trim();
// Skip meta sentences
if (expr.includes('find') || expr.includes('solve') || expr.includes('maximize') ||
expr.includes('minimize') || expr.includes('subject to')) {
return null;
}
// Remove "such that" phrases
expr = expr.replace(/\b(?:such\s+that|where|given\s+that)\b/gi, '');
// Replace natural language operators
const replacements: Array<[RegExp, string]> = [
[/\bis greater than or equal to\b/g, '>='],
[/\bis less than or equal to\b/g, '<='],
[/\bis greater than\b/g, '>'],
[/\bis less than\b/g, '<'],
[/\bequals\b/g, '=='],
[/\bis equal to\b/g, '=='],
[/\bplus\b/g, '+'],
[/\bminus\b/g, '-'],
[/\btimes\b/g, '*'],
[/\bmultiplied by\b/g, '*'],
[/\bdivided by\b/g, '/'],
[/\bsquared\b/g, '**2'],
[/\bat most\b/g, '<='],
[/\bat least\b/g, '>='],
[/\bmore than\b/g, '>'],
[/\bless than\b/g, '<']
];
for (const [pattern, replacement] of replacements) {
expr = expr.replace(pattern, replacement);
}
// Clean up whitespace around operators
expr = expr.replace(/\s+/g, ' ');
expr = expr.replace(/\s*([+\-*/<>=!]+)\s*/g, ' $1 ');
// Convert single = to == for equality (but not for already-double ==)
expr = expr.replace(/\s*=\s*/g, ' == ');
// Fix any === that might have been created
expr = expr.replace(/===+/g, '==');
return expr.trim() || null;
}
/**
* Extract optimization goal from natural language
* @param input Input text
* @param variables Known variables
* @returns Optimization goal or undefined
*/
private extractOptimization(input: string, variables: SMTVariable[]): SMTOptimization | undefined {
const lowerInput = input.toLowerCase();
// Check for maximize
const maxMatch = lowerInput.match(/maximize\s+(.+?)(?:\s+subject|\s+where|$)/i);
if (maxMatch) {
return {
direction: 'maximize',
objective: this.sentenceToExpression(maxMatch[1], variables) || maxMatch[1]
};
}
// Check for minimize
const minMatch = lowerInput.match(/minimize\s+(.+?)(?:\s+subject|\s+where|$)/i);
if (minMatch) {
return {
direction: 'minimize',
objective: this.sentenceToExpression(minMatch[1], variables) || minMatch[1]
};
}
return undefined;
}
/**
* Parse symbolic CSDL format
* @param input Symbolic input
* @returns SMT problem
*/
private symbolicToSMT(input: string): SMTProblem {
// Simple JSON parsing for now
// In a full implementation, this would use the CSDL parser
try {
return JSON.parse(input) as SMTProblem;
} catch (e) {
throw new Error('Failed to parse symbolic input. Expected JSON format.');
}
}
/**
* Validate SMT problem for satisfiability
* @param problem SMT problem
* @returns Validation result
*/
private validate(problem: SMTProblem): LogicResult {
try {
const smtAnalysis = this.validator.validate(problem);
// Convert SMT analysis to LogicalAnalysis format
const analysis = {
isValid: smtAnalysis.isSatisfiable,
fallacies: [],
explanation: smtAnalysis.explanation,
counterexample: smtAnalysis.counterexample
};
return {
status: 'success',
message: smtAnalysis.isSatisfiable
? 'The constraints are satisfiable.'
: 'The constraints are unsatisfiable.',
details: {
system: 'smt' as LogicalSystem,
analysis
}
};
} catch (error) {
return {
status: 'error',
message: error instanceof Error ? error.message : 'Validation failed',
details: {
system: 'smt' as LogicalSystem
}
};
}
}
/**
* Formalize SMT problem to Z3 Python code
* @param problem SMT problem
* @returns Formalization result
*/
private formalize(problem: SMTProblem): LogicResult {
try {
const formatted = this.formatter.formatProblem(problem);
const z3Code = this.translator.translate(problem);
return {
status: 'success',
message: 'Problem formalized successfully.',
details: {
system: 'smt' as LogicalSystem,
formalizedInput: `CSDL Format:\n${formatted}\n\nZ3 Python Code:\n${z3Code}`
}
};
} catch (error) {
return {
status: 'error',
message: error instanceof Error ? error.message : 'Formalization failed',
details: {
system: 'smt' as LogicalSystem
}
};
}
}
/**
* Visualize SMT problem
* @param problem SMT problem
* @returns Visualization result
*/
private visualize(problem: SMTProblem): LogicResult {
try {
const visualization = this.visualizer.visualize(problem);
return {
status: 'success',
message: 'Visualization generated successfully.',
details: {
system: 'smt' as LogicalSystem,
visualization
}
};
} catch (error) {
return {
status: 'error',
message: error instanceof Error ? error.message : 'Visualization failed',
details: {
system: 'smt' as LogicalSystem
}
};
}
}
/**
* Solve SMT problem using Z3
* @param problem SMT problem
* @returns Solution result
*/
private async solve(problem: SMTProblem): Promise<LogicResult> {
try {
// Convert SMTProblem to Z3 format
const z3Variables = problem.variables.map(v => ({
name: v.name,
type: v.type
}));
const z3Constraints = problem.constraints.map(c => ({
expression: c.expression
}));
// Call Z3 solver
const response = await this.z3Solver.solve(z3Variables, z3Constraints);
if (response.status === 'sat' && response.model) {
// Build solution steps
const steps = [];
let index = 1;
// Show the problem
const formatted = this.formatter.formatProblem(problem);
steps.push({
index: index++,
statement: `Problem:\n${formatted}`,
rule: 'Given',
justification: 'Constraint satisfaction problem'
});
// Show each variable solution
for (const [varName, value] of Object.entries(response.model)) {
steps.push({
index: index++,
statement: `${varName} = ${value}`,
rule: 'Z3 Solution',
justification: `Satisfies all constraints`
});
}
// Build conclusion
const solutionStr = Object.entries(response.model)
.map(([name, value]) => `${name} = ${value}`)
.join(', ');
return {
status: 'success',
message: 'Solution found successfully.',
details: {
system: 'smt' as LogicalSystem,
formalizedInput: formatted,
solution: {
steps,
conclusion: `Solution: ${solutionStr}`
}
}
};
} else if (response.status === 'unsat') {
return {
status: 'error',
message: 'The constraints are unsatisfiable (no solution exists).',
details: {
system: 'smt' as LogicalSystem,
formalizedInput: this.formatter.formatProblem(problem),
solution: {
steps: [{
index: 1,
statement: 'Constraints are unsatisfiable',
rule: 'Z3 Analysis',
justification: response.reason || 'The given constraints cannot all be true simultaneously'
}],
conclusion: 'No solution exists'
}
}
};
} else {
// Unknown or timeout
return {
status: 'error',
message: `Z3 returned status: ${response.status}`,
details: {
system: 'smt' as LogicalSystem,
formalizedInput: this.formatter.formatProblem(problem)
}
};
}
} catch (error) {
// Z3 not available or other error
const formatted = this.formatter.formatProblem(problem);
const z3Code = this.translator.translate(problem);
return {
status: 'error',
message: error instanceof Error ? error.message : 'Solving failed',
details: {
system: 'smt' as LogicalSystem,
formalizedInput: `Problem recognized:\n\n${formatted}\n\nZ3 Python code:\n${z3Code}\n\n⚠️ ${error instanceof Error ? error.message : 'Unknown error'}`
}
};
}
}
}
