/**
* Z3 Integration Tests
* Tests Z3 solver integration via Python subprocess
*/
import { Z3Solver, intVar, realVar, boolVar, constraint, maximize, minimize } from './z3Integration.js';
import { Z3Variable, Z3Constraint } from './types.js';
// Skip tests if Z3 is not installed
const Z3_AVAILABLE = process.env.SKIP_Z3_TESTS !== 'true';
describe('Z3Solver', () => {
let solver: Z3Solver;
beforeEach(() => {
solver = new Z3Solver({ timeout: 5000 });
});
// Test connection to Z3
if (Z3_AVAILABLE) {
test('testConnection should verify Z3 is available', async () => {
const available = await solver.testConnection();
expect(available).toBe(true);
}, 10000);
test('getVersion should return Z3 version string', async () => {
const version = await solver.getVersion();
expect(version).toMatch(/\d+\.\d+\.\d+/);
}, 5000);
}
// Test simple constraint solving
test('solve simple constraint: x + y = 10, x > 5', async () => {
const variables: Z3Variable[] = [intVar('x'), intVar('y')];
const constraints: Z3Constraint[] = [
constraint('x + y == 10'),
constraint('x > 5')
];
const response = await solver.solve(variables, constraints);
expect(response.status).toBe('sat');
expect(response.model).toBeDefined();
if (response.model) {
expect(response.model.x).toBeGreaterThan(5);
expect(Number(response.model.x) + Number(response.model.y)).toBe(10);
}
}, 10000);
// Test unsat case
test('detect unsatisfiable constraints: x > 10 and x < 5', async () => {
const variables: Z3Variable[] = [intVar('x')];
const constraints: Z3Constraint[] = [
constraint('x > 10'),
constraint('x < 5')
];
const response = await solver.solve(variables, constraints);
expect(response.status).toBe('unsat');
expect(response.model).toBeUndefined();
}, 10000);
// Test optimization
test('optimize: maximize 2*x + 3*y subject to x + y <= 10', async () => {
const variables: Z3Variable[] = [intVar('x'), intVar('y')];
const constraints: Z3Constraint[] = [
constraint('x >= 0'),
constraint('y >= 0'),
constraint('x + y <= 10')
];
const objective = maximize('2*x + 3*y');
const response = await solver.optimize(variables, constraints, objective);
expect(response.status).toBe('sat');
expect(response.model).toBeDefined();
expect(response.objectiveValue).toBeDefined();
// Optimal solution should be x=0, y=10 (gives 30)
if (response.model) {
expect(response.objectiveValue).toBe(30);
}
}, 10000);
// Test real arithmetic
test('solve with real numbers: x^2 = 2', async () => {
const variables: Z3Variable[] = [realVar('x')];
const constraints: Z3Constraint[] = [
constraint('x * x == 2'),
constraint('x > 0')
];
const response = await solver.solve(variables, constraints);
expect(response.status).toBe('sat');
expect(response.model).toBeDefined();
if (response.model) {
const x = parseFloat(response.model.x as string);
expect(Math.abs(x * x - 2)).toBeLessThan(0.01); // Approximately sqrt(2)
}
}, 10000);
// Test boolean satisfiability
test('solve boolean SAT: (p OR q) AND (NOT p OR r) AND (NOT q OR NOT r)', async () => {
const variables: Z3Variable[] = [boolVar('p'), boolVar('q'), boolVar('r')];
const constraints: Z3Constraint[] = [
constraint('Or(p, q)'),
constraint('Or(Not(p), r)'),
constraint('Or(Not(q), Not(r))')
];
const response = await solver.solve(variables, constraints);
expect(response.status).toBe('sat');
expect(response.model).toBeDefined();
}, 10000);
// Test checkSat method
test('checkSat returns only status', async () => {
const variables: Z3Variable[] = [intVar('x')];
const constraints: Z3Constraint[] = [constraint('x > 0')];
const status = await solver.checkSat(variables, constraints);
expect(status).toBe('sat');
}, 10000);
// Test getModel method
test('getModel returns solution model', async () => {
const variables: Z3Variable[] = [intVar('x'), intVar('y')];
const constraints: Z3Constraint[] = [
constraint('x == 5'),
constraint('y == 3')
];
const model = await solver.getModel(variables, constraints);
expect(model).not.toBeNull();
if (model) {
expect(model.x).toBe(5);
expect(model.y).toBe(3);
}
}, 10000);
// Test timeout handling
test('timeout should be handled gracefully', async () => {
const variables: Z3Variable[] = [intVar('x'), intVar('y')];
const constraints: Z3Constraint[] = [
constraint('x > 0'),
constraint('y > 0')
];
// Use very short timeout
const shortTimeoutSolver = new Z3Solver({ timeout: 1 });
await expect(
shortTimeoutSolver.solve(variables, constraints)
).rejects.toThrow(/timeout/i);
}, 10000);
// Test error handling for invalid constraints
test('invalid constraint should return error status', async () => {
const variables: Z3Variable[] = [intVar('x')];
const constraints: Z3Constraint[] = [
constraint('this is not valid syntax')
];
const response = await solver.solve(variables, constraints);
expect(response.status).toBe('error');
expect(response.reason).toBeDefined();
}, 10000);
// Test solution enumeration
test('enumerateSolutions finds multiple solutions', async () => {
const variables: Z3Variable[] = [intVar('x'), intVar('y')];
const constraints: Z3Constraint[] = [
constraint('x >= 1'),
constraint('x <= 3'),
constraint('y >= 1'),
constraint('y <= 3'),
constraint('x + y <= 4')
];
const solutions = await solver.enumerateSolutions(variables, constraints, 10);
expect(solutions.length).toBeGreaterThan(1);
expect(solutions.length).toBeLessThanOrEqual(10);
// Verify all solutions satisfy constraints
for (const solution of solutions) {
const x = solution.x as number;
const y = solution.y as number;
expect(x).toBeGreaterThanOrEqual(1);
expect(x).toBeLessThanOrEqual(3);
expect(y).toBeGreaterThanOrEqual(1);
expect(y).toBeLessThanOrEqual(3);
expect(x + y).toBeLessThanOrEqual(4);
}
}, 15000);
// Test minimize objective
test('minimize objective function', async () => {
const variables: Z3Variable[] = [intVar('x'), intVar('y')];
const constraints: Z3Constraint[] = [
constraint('x >= 0'),
constraint('y >= 0'),
constraint('x + y >= 10')
];
const objective = minimize('x + y');
const response = await solver.optimize(variables, constraints, objective);
expect(response.status).toBe('sat');
expect(response.objectiveValue).toBe(10);
}, 10000);
// Test getUnsatCore
test('getUnsatCore identifies conflicting constraints', async () => {
const variables: Z3Variable[] = [intVar('x')];
const constraints: Z3Constraint[] = [
constraint('x > 10'), // Constraint 0
constraint('x < 20'), // Constraint 1
constraint('x < 5') // Constraint 2 - conflicts with 0
];
const unsatCore = await solver.getUnsatCore(variables, constraints);
expect(unsatCore).toBeDefined();
if (unsatCore) {
// Core should include constraints 0 and 2
expect(unsatCore.constraints).toContain(0);
expect(unsatCore.constraints).toContain(2);
}
}, 10000);
});
// Integration tests with more complex scenarios
describe('Z3Solver - Complex Scenarios', () => {
let solver: Z3Solver;
beforeEach(() => {
solver = new Z3Solver({ timeout: 10000 });
});
test('solve system of linear equations', async () => {
const variables: Z3Variable[] = [realVar('x'), realVar('y'), realVar('z')];
const constraints: Z3Constraint[] = [
constraint('x + y + z == 6'),
constraint('2*x - y + z == 1'),
constraint('x + 2*y - z == 3')
];
const response = await solver.solve(variables, constraints);
expect(response.status).toBe('sat');
expect(response.model).toBeDefined();
// Verify solution
if (response.model) {
const x = parseFloat(response.model.x as string);
const y = parseFloat(response.model.y as string);
const z = parseFloat(response.model.z as string);
expect(Math.abs(x + y + z - 6)).toBeLessThan(0.01);
expect(Math.abs(2*x - y + z - 1)).toBeLessThan(0.01);
expect(Math.abs(x + 2*y - z - 3)).toBeLessThan(0.01);
}
}, 15000);
test('solve scheduling problem', async () => {
// Schedule 3 tasks with dependencies
// Task A: duration 2, starts at time >= 0
// Task B: duration 3, starts after A finishes
// Task C: duration 1, starts after B finishes
const variables: Z3Variable[] = [
intVar('start_A'),
intVar('start_B'),
intVar('start_C'),
intVar('makespan')
];
const constraints: Z3Constraint[] = [
constraint('start_A >= 0'),
constraint('start_B >= start_A + 2'), // B starts after A finishes
constraint('start_C >= start_B + 3'), // C starts after B finishes
constraint('makespan >= start_C + 1') // Total time includes C
];
const objective = minimize('makespan');
const response = await solver.optimize(variables, constraints, objective);
expect(response.status).toBe('sat');
expect(response.objectiveValue).toBe(6); // 2 + 3 + 1 = 6
}, 15000);
test('solve logic puzzle (Zebra-style)', async () => {
// Simplified logic puzzle: 3 houses, 3 colors, determine arrangement
// House 1 is red, blue house is next to green house
const variables: Z3Variable[] = [
intVar('red'), // Position of red house (1-3)
intVar('blue'), // Position of blue house
intVar('green') // Position of green house
];
const constraints: Z3Constraint[] = [
constraint('red == 1'),
constraint('blue >= 1'),
constraint('blue <= 3'),
constraint('green >= 1'),
constraint('green <= 3'),
constraint('Distinct(red, blue, green)'),
// Blue is next to green (adjacent positions)
constraint('Or(blue == green + 1, blue == green - 1)')
];
const response = await solver.solve(variables, constraints);
expect(response.status).toBe('sat');
if (response.model) {
const red = response.model.red as number;
const blue = response.model.blue as number;
const green = response.model.green as number;
expect(red).toBe(1);
expect(Math.abs(blue - green)).toBe(1); // Adjacent
}
}, 15000);
});
// Helper function tests
describe('Helper Functions', () => {
test('intVar creates integer variable', () => {
const v = intVar('x');
expect(v.name).toBe('x');
expect(v.type).toBe('Int');
});
test('realVar creates real variable', () => {
const v = realVar('y');
expect(v.name).toBe('y');
expect(v.type).toBe('Real');
});
test('boolVar creates boolean variable', () => {
const v = boolVar('p');
expect(v.name).toBe('p');
expect(v.type).toBe('Bool');
});
test('constraint creates constraint object', () => {
const c = constraint('x > 0', 'x is positive');
expect(c.expression).toBe('x > 0');
expect(c.description).toBe('x is positive');
});
test('maximize creates maximize objective', () => {
const obj = maximize('x + y');
expect(obj.expression).toBe('x + y');
expect(obj.direction).toBe('maximize');
});
test('minimize creates minimize objective', () => {
const obj = minimize('x + y');
expect(obj.expression).toBe('x + y');
expect(obj.direction).toBe('minimize');
});
});
