/**
* Tests for Clingo ASP Solver Integration
*
* These tests verify the Clingo subprocess integration following
* the patterns from Z3 and ProbLog integrations.
*/
import { ClingoSolver, buildProgram, fact, rule, constraint, choice, show, minimize } from './clingoIntegration.js';
import { StableModel } from './types.js';
describe('Clingo Integration', () => {
let solver: ClingoSolver;
beforeAll(async () => {
solver = new ClingoSolver({ defaultTimeout: 5000 });
// Check if Clingo is installed
const available = await solver.testConnection();
if (!available) {
console.warn('Clingo not available - some tests may fail');
}
});
describe('Basic Operations', () => {
test('should solve simple satisfiable program', async () => {
const program = buildProgram({
facts: ['a.', 'b.', 'c.']
});
const response = await solver.solve(program, { models: 1 });
expect(response.status).toBe('SATISFIABLE');
expect(response.models.length).toBeGreaterThan(0);
expect(response.models[0].atoms).toContain('a');
expect(response.models[0].atoms).toContain('b');
expect(response.models[0].atoms).toContain('c');
});
test('should handle unsatisfiable program', async () => {
const program = buildProgram({
facts: ['a.'],
constraints: [':- a.']
});
const response = await solver.solve(program);
expect(response.status).toBe('UNSATISFIABLE');
expect(response.models.length).toBe(0);
});
test('should enumerate multiple models', async () => {
const program = buildProgram({
choices: ['{a; b; c}.']
});
const response = await solver.solve(program, { models: 0 }); // All models
expect(response.status).toBe('SATISFIABLE');
expect(response.models.length).toBe(8); // 2^3 = 8 subsets
});
test('should limit number of models', async () => {
const program = buildProgram({
choices: ['{a; b; c; d}.']
});
const response = await solver.solve(program, { models: 5 });
expect(response.status).toBe('SATISFIABLE');
expect(response.models.length).toBeLessThanOrEqual(5);
});
test('should check satisfiability', async () => {
const satisfiableProgram = 'a. b.';
const unsatisfiableProgram = 'a. :- a.';
const isSat = await solver.check(satisfiableProgram);
const isUnsat = await solver.check(unsatisfiableProgram);
expect(isSat).toBe(true);
expect(isUnsat).toBe(false);
});
});
describe('Graph Coloring', () => {
test('should solve 3-coloring of cycle graph', async () => {
const program = `
% 5-node cycle graph: 1-2-3-4-5-1
vertex(1..5).
edge(1,2). edge(2,3). edge(3,4). edge(4,5). edge(5,1).
% Define colors
color(red; blue; green).
% Assign exactly one color to each vertex
1 {assign(X, C) : color(C)} 1 :- vertex(X).
% Adjacent vertices must have different colors
:- assign(X, C), assign(Y, C), edge(X, Y).
#show assign/2.
`;
const response = await solver.solve(program, { models: 1 });
expect(response.status).toBe('SATISFIABLE');
expect(response.models.length).toBeGreaterThan(0);
const model = response.models[0];
expect(model.atoms.length).toBe(5); // 5 vertices, each with one color
// Verify no adjacent vertices have same color
const assignments = new Map<number, string>();
for (const atom of model.atoms) {
const match = atom.match(/assign\((\d+),(\w+)\)/);
if (match) {
assignments.set(parseInt(match[1]), match[2]);
}
}
expect(assignments.get(1)).not.toBe(assignments.get(2));
expect(assignments.get(2)).not.toBe(assignments.get(3));
expect(assignments.get(3)).not.toBe(assignments.get(4));
expect(assignments.get(4)).not.toBe(assignments.get(5));
expect(assignments.get(5)).not.toBe(assignments.get(1));
});
test('should enumerate all colorings', async () => {
const program = `
% Triangle graph
vertex(1..3).
edge(1,2). edge(2,3). edge(3,1).
color(red; blue).
1 {assign(X, C) : color(C)} 1 :- vertex(X).
:- assign(X, C), assign(Y, C), edge(X, Y).
#show assign/2.
`;
const models = await solver.enumerate(program);
expect(models.length).toBe(6); // 3! / 2 = 6 valid 2-colorings
});
});
describe('N-Queens Problem', () => {
test('should solve 4-Queens', async () => {
const N = 4;
const program = `
% Board size
#const n=${N}.
row(1..n).
col(1..n).
% Place exactly one queen per row
1 {queen(R, C) : col(C)} 1 :- row(R).
% No two queens in same column
:- queen(R1, C), queen(R2, C), R1 != R2.
% No two queens on same diagonal (/)
:- queen(R1, C1), queen(R2, C2), R1 != R2, C1 - R1 == C2 - R2.
% No two queens on same diagonal (\\)
:- queen(R1, C1), queen(R2, C2), R1 != R2, C1 + R1 == C2 + R2.
#show queen/2.
`;
const response = await solver.solve(program, { models: 2 });
expect(response.status).toBe('SATISFIABLE');
expect(response.models.length).toBeGreaterThan(0);
const model = response.models[0];
expect(model.atoms.length).toBe(N); // N queens
});
test('should find all solutions for 4-Queens', async () => {
const program = `
#const n=4.
row(1..n). col(1..n).
1 {queen(R, C) : col(C)} 1 :- row(R).
:- queen(R1, C), queen(R2, C), R1 != R2.
:- queen(R1, C1), queen(R2, C2), R1 != R2, C1 - R1 == C2 - R2.
:- queen(R1, C1), queen(R2, C2), R1 != R2, C1 + R1 == C2 + R2.
#show queen/2.
`;
const models = await solver.enumerate(program);
expect(models.length).toBe(2); // 4-Queens has exactly 2 solutions
});
});
describe('Optimization', () => {
test('should minimize selection', async () => {
const program = `
% Choose subset of items
item(1..5).
{selected(X) : item(X)}.
% Minimize number of selected items
#minimize {1, X : selected(X)}.
#show selected/1.
`;
const response = await solver.optimize(program);
expect(response.status).toBe('OPTIMUM');
expect(response.optimal).toBe(true);
expect(response.models.length).toBeGreaterThan(0);
const optimalModel = response.models[response.models.length - 1];
expect(optimalModel.optimal).toBe(true);
expect(optimalModel.atoms.length).toBe(0); // Empty set is optimal
});
test('should maximize with constraints', async () => {
const program = `
% Knapsack-like problem
item(1..3).
weight(1, 2). weight(2, 3). weight(3, 4).
value(1, 10). value(2, 15). value(3, 20).
% Select items
{selected(X) : item(X)}.
% Capacity constraint
:- #sum{W, X : selected(X), weight(X, W)} > 6.
% Maximize value
#maximize {V@1, X : selected(X), value(X, V)}.
#show selected/1.
`;
const response = await solver.optimize(program);
expect(response.status).toBe('OPTIMUM');
expect(response.optimal).toBe(true);
const optimalModel = response.models[response.models.length - 1];
expect(optimalModel.cost).toBeDefined();
expect(optimalModel.optimal).toBe(true);
});
test('should handle multi-level optimization', async () => {
const program = `
% Select numbers
num(1..5).
{select(X) : num(X)}.
% First priority: maximize count
#maximize {1@2, X : select(X)}.
% Second priority: minimize sum
#minimize {X@1, X : select(X)}.
#show select/1.
`;
const response = await solver.optimize(program);
expect(response.status).toBe('OPTIMUM');
expect(response.optimal).toBe(true);
const optimalModel = response.models[response.models.length - 1];
expect(optimalModel.cost).toBeDefined();
expect(optimalModel.cost!.length).toBe(2); // Two priority levels
});
});
describe('Aggregates and Constraints', () => {
test('should handle count aggregates', async () => {
const program = `
item(1..10).
{selected(X) : item(X)}.
% Select exactly 3 items
:- #count{X : selected(X)} != 3.
#show selected/1.
`;
const models = await solver.enumerate(program, 5);
expect(models.length).toBeGreaterThan(0);
for (const model of models) {
expect(model.atoms.length).toBe(3);
}
});
test('should handle sum aggregates', async () => {
const program = `
num(1..5).
{choose(X) : num(X)}.
% Sum must be between 5 and 8
:- #sum{X : choose(X)} < 5.
:- #sum{X : choose(X)} > 8.
#show choose/1.
`;
const response = await solver.solve(program, { models: 5 });
expect(response.status).toBe('SATISFIABLE');
expect(response.models.length).toBeGreaterThan(0);
for (const model of response.models) {
const sum = model.atoms
.map(a => {
const match = a.match(/choose\((\d+)\)/);
return match ? parseInt(match[1]) : 0;
})
.reduce((a, b) => a + b, 0);
expect(sum).toBeGreaterThanOrEqual(5);
expect(sum).toBeLessThanOrEqual(8);
}
});
test('should handle conditional literals in aggregates', async () => {
const program = `
person(alice; bob; charlie).
age(alice, 25). age(bob, 30). age(charlie, 20).
{invited(P) : person(P)}.
% At least 2 people over 22 must be invited
:- #count{P : invited(P), age(P, A), A > 22} < 2.
#show invited/1.
`;
const models = await solver.enumerate(program, 3);
expect(models.length).toBeGreaterThan(0);
for (const model of models) {
// Should include at least alice and bob (both > 22)
const hasAlice = model.atoms.some(a => a.includes('alice'));
const hasBob = model.atoms.some(a => a.includes('bob'));
expect(hasAlice || hasBob).toBe(true);
}
});
});
describe('Default Logic', () => {
test('should handle default negation', async () => {
const program = `
bird(tweety).
bird(penguin).
penguin(penguin).
% Birds fly by default, unless they are penguins
flies(X) :- bird(X), not penguin(X).
#show flies/1.
`;
const response = await solver.solve(program, { models: 1 });
expect(response.status).toBe('SATISFIABLE');
expect(response.models[0].atoms).toContain('flies(tweety)');
expect(response.models[0].atoms).not.toContain('flies(penguin)');
});
test('should handle multiple defaults', async () => {
const program = `
vehicle(car). vehicle(bike).
motorized(car).
% Vehicles are eco-friendly by default if not motorized
eco(X) :- vehicle(X), not motorized(X).
#show eco/1.
`;
const response = await solver.solve(program, { models: 1 });
expect(response.status).toBe('SATISFIABLE');
expect(response.models[0].atoms).toContain('eco(bike)');
expect(response.models[0].atoms).not.toContain('eco(car)');
});
});
describe('Error Handling', () => {
test('should detect syntax errors', async () => {
const program = 'a :- b % Missing period';
const validation = await solver.validate(program);
expect(validation.valid).toBe(false);
expect(validation.errors).toBeDefined();
expect(validation.errors!.length).toBeGreaterThan(0);
});
test('should detect unsafe variables', async () => {
const program = `
edge(1, 2).
% Unsafe: X and Y appear only in negative literal
path(X, Y) :- not blocked(X, Y).
`;
const validation = await solver.validate(program);
expect(validation.valid).toBe(false);
if (validation.errors) {
const hasUnsafeError = validation.errors.some(e =>
e.message.includes('unsafe') || e.type === 'safety'
);
expect(hasUnsafeError).toBe(true);
}
});
test('should handle timeout', async () => {
// Create a program that's difficult to solve
const program = `
num(1..100).
{select(X) : num(X)}.
% Force specific sum (computationally intensive)
:- #sum{X : select(X)} != 1234.
#show select/1.
`;
const response = await solver.solve(program, { timeout: 500 });
// Should either timeout or solve quickly
expect(['SATISFIABLE', 'UNSATISFIABLE', 'TIMEOUT', 'UNKNOWN']).toContain(response.status);
}, 10000);
test('should handle empty program', async () => {
const program = '';
const response = await solver.solve(program, { models: 1 });
// Empty program has one empty model
expect(response.status).toBe('SATISFIABLE');
expect(response.models.length).toBe(1);
expect(response.models[0].atoms.length).toBe(0);
});
});
describe('Helper Functions', () => {
test('should build program from parts', () => {
const program = buildProgram({
facts: ['a.', 'b.'],
rules: ['c :- a, b.'],
constraints: [':- c, d.'],
show: ['#show c/0.']
});
expect(program).toContain('a.');
expect(program).toContain('b.');
expect(program).toContain('c :- a, b.');
expect(program).toContain(':- c, d.');
expect(program).toContain('#show c/0.');
});
test('should create fact', () => {
expect(fact('a')).toBe('a.');
expect(fact('node(1)')).toBe('node(1).');
});
test('should create rule', () => {
expect(rule('c', ['a', 'b'])).toBe('c :- a, b.');
});
test('should create constraint', () => {
expect(constraint(['a', 'b'])).toBe(':- a, b.');
});
test('should create choice rule', () => {
expect(choice(['a', 'b', 'c'])).toBe('{a; b; c}.');
expect(choice(['a', 'b'], 1, 1)).toBe('1 {a; b} 1.');
expect(choice(['a', 'b'], 0, 2, 'condition')).toBe('0 {a; b} 2 :- condition.');
});
test('should create show directive', () => {
expect(show('atom')).toBe('#show atom.');
expect(show('pred', 2)).toBe('#show pred/2.');
});
test('should create minimize statement', () => {
const result = minimize([
{ weight: 1, tuple: ['X'] },
{ weight: 2, tuple: ['Y'] }
]);
expect(result).toContain('#minimize');
expect(result).toContain('1@1');
expect(result).toContain('2@1');
});
});
describe('Statistics', () => {
test('should return timing statistics', async () => {
const program = `
vertex(1..10).
{color(X, red); color(X, blue)} :- vertex(X).
1 {color(X, C)} 1 :- vertex(X).
#show color/2.
`;
const response = await solver.solve(program, { models: 1 });
expect(response.statistics).toBeDefined();
expect(response.statistics.time.total).toBeGreaterThan(0);
expect(response.statistics.models.enumerated).toBeGreaterThanOrEqual(1);
});
test('should report model counts correctly', async () => {
const program = '{a; b}.';
const response = await solver.solve(program, { models: 0 });
expect(response.statistics.models.enumerated).toBe(4); // 2^2 = 4
expect(response.models.length).toBe(4);
});
});
describe('Complex Problems', () => {
test('should solve Hamiltonian path', async () => {
const program = `
% Complete graph K4
node(1..4).
edge(X, Y) :- node(X), node(Y), X != Y.
% Start at node 1
path(1, Y, 1) :- edge(1, Y).
% Continue path
path(X, Y, T+1) :- path(_, X, T), edge(X, Y), not visited(Y, T), T < 4.
% Mark visited
visited(X, T) :- path(_, X, T).
visited(1, 0).
% Must visit all 4 nodes
:- #count{X : visited(X, T)} != 4.
#show path/3.
`;
const response = await solver.solve(program, { models: 1, timeout: 5000 });
// Hamiltonian path should exist in complete graph
expect(['SATISFIABLE', 'UNSATISFIABLE']).toContain(response.status);
});
test('should solve scheduling problem', async () => {
const program = `
% Employees and shifts
employee(alice; bob; charlie).
shift(morning; afternoon; evening).
% Each employee gets exactly one shift
1 {assign(E, S) : shift(S)} 1 :- employee(E).
% Each shift needs at least 1 person
:- shift(S), not assigned_to(S).
assigned_to(S) :- assign(_, S).
% Alice can't work evening
:- assign(alice, evening).
#show assign/2.
`;
const response = await solver.solve(program, { models: 5 });
expect(response.status).toBe('SATISFIABLE');
expect(response.models.length).toBeGreaterThan(0);
for (const model of response.models) {
// Verify Alice not in evening
const aliceInEvening = model.atoms.some(a => a === 'assign(alice,evening)');
expect(aliceInEvening).toBe(false);
// Verify each employee has one shift
const aliceAssignments = model.atoms.filter(a => a.includes('alice')).length;
expect(aliceAssignments).toBe(1);
}
});
});
describe('Connection Tests', () => {
test('should test connection successfully', async () => {
const available = await solver.testConnection();
expect(typeof available).toBe('boolean');
});
test('should get version information', async () => {
try {
const version = await solver.getVersion();
expect(version).toBeDefined();
expect(version.length).toBeGreaterThan(0);
} catch (error) {
// Version check may fail if clingo not installed
console.log('Version check skipped - clingo may not be installed');
}
});
});
});
