/**
* Clingo Solver Wrapper
* Interface to the Clingo ASP solver via child process
*/
import { spawn } from 'child_process';
import { ASPSolution, AnswerSet, ASPAtom } from '../../types.js';
import { Loggers } from '../../utils/logger.js';
const logger = Loggers.manager;
export interface ClingoOptions {
maxModels?: number; // 0 = all models
cautious?: boolean; // Cautious reasoning
brave?: boolean; // Brave reasoning
optimization?: boolean; // Find optimal models
timeout?: number; // Timeout in seconds
}
export class ClingoSolver {
private clingoPath: string;
constructor(clingoPath: string = 'clingo') {
this.clingoPath = clingoPath;
}
/**
* Solve ASP program using Clingo
*/
async solve(program: string, options: ClingoOptions = {}): Promise<ASPSolution> {
const startTime = Date.now();
try {
const output = await this.runClingo(program, options);
const solution = this.parseOutput(output);
solution.computationTime = Date.now() - startTime;
return solution;
} catch (error) {
logger.error('Clingo solver error', { error });
return {
answerSets: [],
totalModels: 0,
optimal: false,
computationTime: Date.now() - startTime,
satisfiable: false
};
}
}
/**
* Run Clingo as child process
*/
private runClingo(program: string, options: ClingoOptions): Promise<string> {
return new Promise((resolve, reject) => {
const args = this.buildArgs(options);
logger.debug('Running Clingo', { args, programLength: program.length });
const clingo = spawn(this.clingoPath, args);
let stdout = '';
let stderr = '';
// Write program to stdin
clingo.stdin.write(program);
clingo.stdin.end();
// Collect output
clingo.stdout.on('data', (data) => {
stdout += data.toString();
});
clingo.stderr.on('data', (data) => {
stderr += data.toString();
});
// Handle completion
clingo.on('close', (code) => {
if (code === 0 || code === 30) {
// 0 = success, 30 = unsatisfiable (which is not an error)
// NOTE: Clingo with --outf=2 outputs JSON to BOTH stdout and stderr
// Prefer stdout, but fall back to stderr if stdout is empty
const output = stdout.trim() || stderr.trim();
resolve(output);
} else {
logger.error('Clingo exited with error', { code, stderr });
reject(new Error(`Clingo exited with code ${code}: ${stderr}`));
}
});
// Handle errors
clingo.on('error', (err) => {
if (err.message.includes('ENOENT')) {
reject(new Error(
'Clingo not found. Please install Clingo: ' +
'brew install clingo (macOS) or apt-get install gringo (Linux)'
));
} else {
reject(err);
}
});
});
}
/**
* Build Clingo command-line arguments
*/
private buildArgs(options: ClingoOptions): string[] {
const args: string[] = [];
// Number of models
if (options.maxModels !== undefined) {
args.push(options.maxModels.toString());
} else {
args.push('0'); // All models
}
// Cautious/brave reasoning
if (options.cautious) {
args.push('--cautious');
}
if (options.brave) {
args.push('--brave');
}
// Optimization
if (options.optimization) {
args.push('--opt-mode=optN'); // Find all optimal models
}
// Timeout
if (options.timeout) {
args.push(`--time-limit=${options.timeout}`);
}
// Output format
args.push('--outf=2'); // JSON output format
return args;
}
/**
* Parse Clingo output to ASPSolution
*/
private parseOutput(output: string): ASPSolution {
const solution: ASPSolution = {
answerSets: [],
totalModels: 0,
optimal: false,
computationTime: 0,
satisfiable: false
};
try {
// Try to parse as JSON (--outf=2)
const json = JSON.parse(output);
if (json.Result === 'UNSATISFIABLE') {
solution.satisfiable = false;
return solution;
}
solution.satisfiable = true;
// Parse witnesses (answer sets)
if (json.Call && json.Call[0] && json.Call[0].Witnesses) {
const witnesses = json.Call[0].Witnesses;
for (let i = 0; i < witnesses.length; i++) {
const witness = witnesses[i];
const answerSet: AnswerSet = {
id: i + 1,
atoms: this.parseAtoms(witness.Value || []),
isOptimal: witness.Optimum !== undefined
};
// Parse optimization costs
if (witness.Costs) {
answerSet.cost = witness.Costs;
}
solution.answerSets.push(answerSet);
}
solution.totalModels = witnesses.length;
solution.optimal = witnesses.some((w: any) => w.Optimum !== undefined);
}
} catch (e) {
// Fallback to text parsing
logger.debug('JSON parse failed, trying text parsing', { error: e });
return this.parseTextOutput(output);
}
return solution;
}
/**
* Parse atoms from Clingo witness value
*/
private parseAtoms(value: string[]): ASPAtom[] {
const atoms: ASPAtom[] = [];
for (const atomStr of value) {
const atom = this.parseAtomString(atomStr);
if (atom) {
atoms.push(atom);
}
}
return atoms;
}
/**
* Parse single atom string
*/
private parseAtomString(atomStr: string): ASPAtom | null {
// Handle negation
let negation: 'classical' | 'default' | 'none' = 'none';
let cleanStr = atomStr.trim();
if (cleanStr.startsWith('not ')) {
negation = 'default';
cleanStr = cleanStr.substring(4);
} else if (cleanStr.startsWith('-')) {
negation = 'classical';
cleanStr = cleanStr.substring(1);
}
// Parse predicate(terms) format
const match = cleanStr.match(/^(\w+)(?:\(([^)]*)\))?$/);
if (!match) return null;
const [, predicate, termsStr] = match;
const terms = termsStr
? termsStr.split(',').map(t => {
const trimmed = t.trim();
const num = parseInt(trimmed);
return isNaN(num) ? trimmed : num;
})
: [];
return {
predicate,
terms,
negation
};
}
/**
* Fallback text output parser (for older Clingo versions)
*/
private parseTextOutput(output: string): ASPSolution {
const solution: ASPSolution = {
answerSets: [],
totalModels: 0,
optimal: false,
computationTime: 0,
satisfiable: false
};
const lines = output.split('\n');
let currentAnswerSet: AnswerSet | null = null;
let answerSetId = 0;
for (const line of lines) {
const trimmed = line.trim();
if (trimmed.startsWith('Answer:')) {
// Start new answer set
answerSetId++;
currentAnswerSet = {
id: answerSetId,
atoms: [],
isOptimal: false
};
} else if (currentAnswerSet && trimmed && !trimmed.startsWith('SATISFIABLE') && !trimmed.startsWith('UNSATISFIABLE') && !trimmed.startsWith('Optimization')) {
// Parse atoms in answer set
const atomStrings = trimmed.split(/\s+/);
for (const atomStr of atomStrings) {
const atom = this.parseAtomString(atomStr);
if (atom) {
currentAnswerSet.atoms.push(atom);
}
}
// Save answer set
if (!solution.answerSets.find(as => as.id === currentAnswerSet!.id)) {
solution.answerSets.push(currentAnswerSet);
}
} else if (trimmed.startsWith('SATISFIABLE')) {
solution.satisfiable = true;
} else if (trimmed.startsWith('UNSATISFIABLE')) {
solution.satisfiable = false;
} else if (trimmed.startsWith('Optimization:')) {
solution.optimal = true;
if (currentAnswerSet) {
currentAnswerSet.isOptimal = true;
}
}
}
solution.totalModels = solution.answerSets.length;
return solution;
}
/**
* Check if Clingo is available
*/
async checkAvailability(): Promise<boolean> {
try {
await this.runClingo('', { maxModels: 0 });
return true;
} catch (error) {
return false;
}
}
}
