import { SMTLogic } from './smt.js';
import { SMTProblem } from '../types.js';
describe('SMTLogic', () => {
let smtLogic: SMTLogic;
beforeEach(() => {
smtLogic = new SMTLogic();
});
describe('Natural Language Parsing', () => {
test('should extract variables from natural language', () => {
const input = 'Find x and y where x + y = 10';
const result = smtLogic.process('formalize', input, 'natural');
expect(result.status).toBe('success');
expect(result.details.formalizedInput).toContain('x');
expect(result.details.formalizedInput).toContain('y');
});
test('should detect integer variables', () => {
const input = 'Find integers x and y where x > 0 and y > 0';
const result = smtLogic.process('formalize', input, 'natural');
expect(result.status).toBe('success');
expect(result.details.formalizedInput).toContain('Int');
});
test('should parse constraints from natural language', () => {
const input = 'Find x where x is greater than 5 and x is less than 10';
const result = smtLogic.process('formalize', input, 'natural');
expect(result.status).toBe('success');
expect(result.details.formalizedInput).toMatch(/x\s*>\s*5/);
expect(result.details.formalizedInput).toMatch(/x\s*<\s*10/);
});
test('should extract optimization goals', () => {
const input = 'Maximize x + y where x >= 0 and y >= 0 and x + y <= 10';
const result = smtLogic.process('formalize', input, 'natural');
expect(result.status).toBe('success');
expect(result.details.formalizedInput).toContain('maximize');
});
});
describe('Validation', () => {
test('should validate satisfiable constraints', () => {
const problem: SMTProblem = {
variables: [
{ name: 'x', type: 'Int' },
{ name: 'y', type: 'Int' }
],
constraints: [
{ type: 'constraint', expression: 'x > 0' },
{ type: 'constraint', expression: 'y > 0' },
{ type: 'constraint', expression: 'x + y == 10' }
]
};
const result = smtLogic.process('validate', problem, 'symbolic');
expect(result.status).toBe('success');
expect(result.details.analysis?.isValid).toBe(true);
});
test('should detect unsatisfiable constraints', () => {
const problem: SMTProblem = {
variables: [
{ name: 'x', type: 'Int' }
],
constraints: [
{ type: 'constraint', expression: 'x > 10' },
{ type: 'constraint', expression: 'x < 5' }
]
};
const result = smtLogic.process('validate', problem, 'symbolic');
expect(result.status).toBe('success');
expect(result.details.analysis?.isValid).toBe(false);
expect(result.details.analysis?.explanation).toContain('Unsatisfiable');
});
test('should handle empty constraints', () => {
const problem: SMTProblem = {
variables: [
{ name: 'x', type: 'Int' }
],
constraints: []
};
const result = smtLogic.process('validate', problem, 'symbolic');
expect(result.status).toBe('success');
expect(result.details.analysis?.isValid).toBe(true);
});
});
describe('Formalization', () => {
test('should formalize problem to CSDL', () => {
const problem: SMTProblem = {
variables: [
{ name: 'x', type: 'Int' },
{ name: 'y', type: 'Real' }
],
constraints: [
{ type: 'constraint', expression: 'x > 0' },
{ type: 'constraint', expression: 'y >= 0.5' }
]
};
const result = smtLogic.process('formalize', problem, 'symbolic');
expect(result.status).toBe('success');
expect(result.details.formalizedInput).toContain('var x: Int');
expect(result.details.formalizedInput).toContain('var y: Real');
expect(result.details.formalizedInput).toContain('assert: x > 0');
});
test('should generate Z3 Python code', () => {
const problem: SMTProblem = {
variables: [
{ name: 'x', type: 'Int' },
{ name: 'y', type: 'Int' }
],
constraints: [
{ type: 'constraint', expression: 'x + y == 10' }
]
};
const result = smtLogic.process('formalize', problem, 'symbolic');
expect(result.status).toBe('success');
expect(result.details.formalizedInput).toContain('from z3 import *');
expect(result.details.formalizedInput).toContain('x, y = Ints');
expect(result.details.formalizedInput).toContain('solver.add(x + y == 10)');
});
test('should handle optimization problems', () => {
const problem: SMTProblem = {
variables: [
{ name: 'x', type: 'Real' },
{ name: 'y', type: 'Real' }
],
constraints: [
{ type: 'constraint', expression: 'x >= 0' },
{ type: 'constraint', expression: 'y >= 0' },
{ type: 'constraint', expression: 'x + y <= 10' }
],
optimization: {
direction: 'maximize',
objective: '2*x + 3*y'
}
};
const result = smtLogic.process('formalize', problem, 'symbolic');
expect(result.status).toBe('success');
expect(result.details.formalizedInput).toContain('Optimize()');
expect(result.details.formalizedInput).toContain('solver.maximize(2*x + 3*y)');
});
});
describe('Visualization', () => {
test('should visualize problem structure', () => {
const problem: SMTProblem = {
variables: [
{ name: 'x', type: 'Int' },
{ name: 'y', type: 'Int' }
],
constraints: [
{ type: 'constraint', expression: 'x > 0' },
{ type: 'constraint', expression: 'y > 0' },
{ type: 'constraint', expression: 'x + y == 10' }
]
};
const result = smtLogic.process('visualize', problem, 'symbolic');
expect(result.status).toBe('success');
expect(result.details.visualization).toContain('Variables');
expect(result.details.visualization).toContain('Constraints');
expect(result.details.visualization).toContain('x: Int');
expect(result.details.visualization).toContain('y: Int');
});
test('should show constraint dependencies', () => {
const problem: SMTProblem = {
variables: [
{ name: 'x', type: 'Int' },
{ name: 'y', type: 'Int' }
],
constraints: [
{ type: 'constraint', expression: 'x + y == 10' }
]
};
const result = smtLogic.process('visualize', problem, 'symbolic');
expect(result.status).toBe('success');
expect(result.details.visualization).toContain('Constraint Graph');
});
test('should visualize optimization problems', () => {
const problem: SMTProblem = {
variables: [
{ name: 'x', type: 'Real' }
],
constraints: [
{ type: 'constraint', expression: 'x >= 0' }
],
optimization: {
direction: 'maximize',
objective: 'x'
}
};
const result = smtLogic.process('visualize', problem, 'symbolic');
expect(result.status).toBe('success');
expect(result.details.visualization).toContain('MAXIMIZE');
});
});
describe('Solving', () => {
test('should return error when Z3 not installed', () => {
const problem: SMTProblem = {
variables: [
{ name: 'x', type: 'Int' }
],
constraints: [
{ type: 'constraint', expression: 'x == 5' }
]
};
const result = smtLogic.process('solve', problem, 'symbolic');
expect(result.status).toBe('error');
expect(result.message).toContain('Z3 solver not installed');
expect(result.details.solution).toBeDefined();
expect(result.details.solution?.steps).toBeDefined();
expect(result.details.formalizedInput).toContain('Problem recognized');
});
test('should return error for system of equations', () => {
const input = 'Solve: x + y = 10, x - y = 2';
const result = smtLogic.process('solve', input, 'natural');
expect(result.status).toBe('error');
expect(result.message).toContain('Z3 solver not installed');
expect(result.details.solution).toBeDefined();
});
test('should provide installation instructions', () => {
const problem: SMTProblem = {
variables: [
{ name: 'x', type: 'Int' },
{ name: 'y', type: 'Int' }
],
constraints: [
{ type: 'constraint', expression: 'x > 0' },
{ type: 'constraint', expression: 'y > 0' },
{ type: 'constraint', expression: 'x + y == 10' }
]
};
const result = smtLogic.process('solve', problem, 'symbolic');
expect(result.status).toBe('error');
expect(result.message).toContain('pip install z3-solver');
expect(result.details.solution?.conclusion).toContain('Cannot solve without Z3 installed');
});
});
describe('Error Handling', () => {
test('should handle invalid input format', () => {
const result = smtLogic.process('solve', '{invalid json', 'symbolic');
expect(result.status).toBe('error');
expect(result.message).toContain('Failed to parse');
});
test('should handle unsupported operation', () => {
const problem: SMTProblem = {
variables: [{ name: 'x', type: 'Int' }],
constraints: []
};
const result = smtLogic.process('unsupported' as any, problem, 'symbolic');
expect(result.status).toBe('error');
expect(result.message).toContain('Unsupported operation');
});
test('should handle empty input gracefully', () => {
const result = smtLogic.process('solve', '', 'natural');
expect(result.status).toBe('error');
expect(result.message).toBeDefined();
expect(result.message).toContain('Z3 solver not installed');
});
});
describe('Integration Tests', () => {
test('should handle complete workflow: natural language → solve', () => {
const input = 'Find x where x + 5 = 10';
const result = smtLogic.process('solve', input, 'natural');
expect(result.status).toBe('error');
expect(result.message).toContain('Z3 solver not installed');
expect(result.details.solution).toBeDefined();
});
test('should handle optimization workflow', () => {
const input = 'Maximize x + y where x + y <= 10 and x >= 0 and y >= 0';
const result = smtLogic.process('solve', input, 'natural');
expect(result.status).toBe('error');
expect(result.message).toContain('Z3 solver not installed');
});
test('should process all four operations (solve returns error without Z3)', () => {
const problem: SMTProblem = {
variables: [
{ name: 'x', type: 'Int' },
{ name: 'y', type: 'Int' }
],
constraints: [
{ type: 'constraint', expression: 'x > 0' },
{ type: 'constraint', expression: 'y > 0' },
{ type: 'constraint', expression: 'x + y == 10' }
]
};
const validateResult = smtLogic.process('validate', problem, 'symbolic');
const formalizeResult = smtLogic.process('formalize', problem, 'symbolic');
const visualizeResult = smtLogic.process('visualize', problem, 'symbolic');
const solveResult = smtLogic.process('solve', problem, 'symbolic');
expect(validateResult.status).toBe('success');
expect(formalizeResult.status).toBe('success');
expect(visualizeResult.status).toBe('success');
expect(solveResult.status).toBe('error');
expect(solveResult.message).toContain('Z3 solver not installed');
});
});
describe('Variable Type Inference', () => {
test('should infer integer types from context', () => {
const input = 'Find integer x where x > 5';
const result = smtLogic.process('formalize', input, 'natural');
expect(result.status).toBe('success');
expect(result.details.formalizedInput).toContain('Int');
});
test('should infer real types from context', () => {
const input = 'Find real number x where x > 5.5';
const result = smtLogic.process('formalize', input, 'natural');
expect(result.status).toBe('success');
expect(result.details.formalizedInput).toContain('Real');
});
test('should default to Int for ambiguous cases', () => {
const input = 'Find x where x > 5';
const result = smtLogic.process('formalize', input, 'natural');
expect(result.status).toBe('success');
expect(result.details.formalizedInput).toContain('Int');
});
});
});
