/**
* Clingo Integration
* Provides TypeScript interface to Clingo ASP solver via command-line subprocess
*
* This module manages communication with Clingo using the proven subprocess pattern
* from Z3 and ProbLog integrations. It spawns Clingo processes, sends ASP programs
* via stdin, and parses JSON results from stdout.
*/
import { spawn, ChildProcess } from 'child_process';
import {
ClingoOptions,
ClingoRequest,
ClingoResponse,
ClingoStatus,
ClingoStatistics,
StableModel,
ClingoJSONOutput,
ASPValidationResult
} from './types.js';
/**
* Configuration for ClingoSolver
*/
export interface ClingoSolverConfig {
clingoPath?: string; // Path to clingo executable (default: 'clingo')
defaultTimeout?: number; // Default timeout in ms (default: 10000)
defaultModels?: number; // Default number of models (default: 0 = all)
}
/**
* Clingo Solver integration class
* Manages subprocess spawning and communication with Clingo
*/
export class ClingoSolver {
private clingoPath: string;
private defaultTimeout: number;
private defaultModels: number;
/**
* Create a new Clingo solver instance
* @param config Configuration options
*/
constructor(config: ClingoSolverConfig = {}) {
this.clingoPath = config.clingoPath || 'clingo';
this.defaultTimeout = config.defaultTimeout || 10000; // 10 seconds
this.defaultModels = config.defaultModels || 0; // All models
}
/**
* Solve an ASP program and return stable models
* @param program ASP program text
* @param options Solver options
* @returns Clingo response with models and statistics
*/
async solve(program: string, options: ClingoOptions = {}): Promise<ClingoResponse> {
const request: ClingoRequest = { program, options };
return this.executeClingo(request);
}
/**
* Enumerate all stable models (or up to limit)
* @param program ASP program text
* @param limit Maximum number of models (0 = all)
* @param timeout Optional timeout override
* @returns All stable models found
*/
async enumerate(
program: string,
limit: number = 0,
timeout?: number
): Promise<StableModel[]> {
const options: ClingoOptions = {
models: limit,
timeout: timeout || this.defaultTimeout,
optimization: 'ignore' // Don't optimize, just enumerate
};
const response = await this.solve(program, options);
return response.models;
}
/**
* Find optimal stable model(s)
* @param program ASP program with optimization statements
* @param timeout Optional timeout override
* @returns Optimal stable model(s)
*/
async optimize(program: string, timeout?: number): Promise<ClingoResponse> {
const options: ClingoOptions = {
models: 0, // Find all optimal models
timeout: timeout || this.defaultTimeout,
optimization: 'on',
optMode: 'optN' // Find optimal models
};
return this.solve(program, options);
}
/**
* Check if program has any stable models (satisfiability check)
* @param program ASP program text
* @param timeout Optional timeout override
* @returns True if satisfiable, false otherwise
*/
async check(program: string, timeout?: number): Promise<boolean> {
const options: ClingoOptions = {
models: 1, // Just find one model
timeout: timeout || this.defaultTimeout,
optimization: 'ignore'
};
const response = await this.solve(program, options);
return response.status === 'SATISFIABLE' || response.status === 'OPTIMUM';
}
/**
* Validate ASP program syntax without solving
* @param program ASP program text
* @returns Validation result with errors/warnings
*/
async validate(program: string): Promise<ASPValidationResult> {
return new Promise((resolve) => {
const args = [
'--warn=all', // Show all warnings
'--verbose=0', // Minimal output
'-' // Read from stdin
];
const proc = spawn(this.clingoPath, args, {
stdio: ['pipe', 'pipe', 'pipe']
});
let stderr = '';
let exitCode: number | null = null;
// Collect stderr (errors and warnings)
proc.stderr.on('data', (data: Buffer) => {
stderr += data.toString();
});
// Write program to stdin
proc.stdin.write(program);
proc.stdin.end();
// Handle process completion
proc.on('close', (code: number | null) => {
exitCode = code;
const validation = this.parseValidationOutput(stderr, exitCode);
resolve(validation);
});
// Handle process error
proc.on('error', (error: Error) => {
resolve({
valid: false,
errors: [{
type: 'syntax',
message: `Failed to run clingo: ${error.message}`,
suggestion: 'Ensure clingo is installed and in PATH'
}]
});
});
// Set timeout for validation (shorter than solving)
setTimeout(() => {
proc.kill('SIGTERM');
resolve({
valid: false,
errors: [{
type: 'syntax',
message: 'Validation timeout',
suggestion: 'Program may have syntax errors'
}]
});
}, 5000);
});
}
/**
* Generate explanation/derivation for atoms in a model
* @param program ASP program text
* @param timeout Optional timeout override
* @returns Response with verbose derivation info
*/
async explain(program: string, timeout?: number): Promise<ClingoResponse> {
const options: ClingoOptions = {
models: 1, // Explain first model
timeout: timeout || this.defaultTimeout,
verbose: true // Enable verbose output
};
return this.solve(program, options);
}
/**
* Execute Clingo with given request
* @param request Clingo request with program and options
* @returns Clingo response
*/
private async executeClingo(request: ClingoRequest): Promise<ClingoResponse> {
const { program, options = {} } = request;
const timeout = options.timeout || this.defaultTimeout;
return new Promise((resolve, reject) => {
// Build Clingo command-line arguments
const args = this.buildClingoArgs(options);
// Spawn Clingo process
const proc: ChildProcess = spawn(this.clingoPath, args, {
stdio: ['pipe', 'pipe', 'pipe']
});
let stdout = '';
let stderr = '';
let timeoutHandle: NodeJS.Timeout;
// Set up timeout
timeoutHandle = setTimeout(() => {
proc.kill('SIGTERM');
// Give it a moment to terminate gracefully
setTimeout(() => {
if (proc.exitCode === null) {
proc.kill('SIGKILL');
}
}, 1000);
resolve(this.createTimeoutResponse(timeout));
}, timeout);
// Collect stdout (JSON results)
proc.stdout?.on('data', (data: Buffer) => {
stdout += data.toString();
});
// Collect stderr (errors and warnings)
proc.stderr?.on('data', (data: Buffer) => {
stderr += data.toString();
});
// Write program to stdin
try {
proc.stdin?.write(program);
proc.stdin?.end();
} catch (error) {
clearTimeout(timeoutHandle);
reject(new Error(`Failed to write to clingo: ${error}`));
return;
}
// Handle process completion
proc.on('close', (code: number | null) => {
clearTimeout(timeoutHandle);
// Clingo exit codes:
// 10 = SATISFIABLE (at least one model)
// 20 = UNSATISFIABLE (no models)
// 30 = OPTIMUM (optimal model found)
// 0 = UNKNOWN
// other = ERROR
if (code !== null && code !== 0 && code !== 10 && code !== 20 && code !== 30) {
resolve(this.createErrorResponse(code, stderr));
return;
}
// Parse JSON output
try {
const response = this.parseOutput(stdout, stderr, code);
resolve(response);
} catch (error) {
resolve({
status: 'ERROR',
models: [],
statistics: this.createEmptyStatistics(),
errors: [
`Failed to parse Clingo output: ${error}`,
`Stdout: ${stdout.substring(0, 500)}`,
`Stderr: ${stderr.substring(0, 500)}`
]
});
}
});
// Handle process error
proc.on('error', (error: Error) => {
clearTimeout(timeoutHandle);
reject(new Error(`Failed to spawn clingo: ${error.message}`));
});
});
}
/**
* Build Clingo command-line arguments from options
* @param options Solver options
* @returns Array of command-line arguments
*/
private buildClingoArgs(options: ClingoOptions): string[] {
const args: string[] = [];
// JSON output format
args.push('--outf=2'); // JSON output
// Number of models
const models = options.models !== undefined ? options.models : this.defaultModels;
args.push(`--models=${models}`);
// Optimization mode
if (options.optimization && options.optimization !== 'ignore') {
if (options.optMode) {
args.push(`--opt-mode=${options.optMode}`);
} else {
args.push('--opt-mode=optN'); // Find optimal models
}
if (options.optStrategy) {
args.push(`--opt-strategy=${options.optStrategy}`);
}
} else {
args.push('--opt-mode=ignore'); // Ignore optimization statements
}
// Threads
if (options.threads) {
args.push(`--parallel-mode=${options.threads}`);
}
// Verbose output
if (options.verbose) {
args.push('--verbose=3');
}
// Project solution (show only #show atoms)
// NOTE: Only enable projection if explicitly requested, otherwise show all atoms
if (options.projectSolution === true) {
args.push('--project');
}
// Suppress common warnings
args.push('--warn=no-atom-undefined');
// Constant definitions
if (options.constantDefinitions) {
for (const [name, value] of Object.entries(options.constantDefinitions)) {
args.push(`-c`, `${name}=${value}`);
}
}
// Read from stdin
args.push('-');
return args;
}
/**
* Parse Clingo JSON output
* @param stdout Standard output (JSON)
* @param stderr Standard error (warnings/errors)
* @param exitCode Process exit code
* @returns Parsed Clingo response
*/
private parseOutput(
stdout: string,
stderr: string,
exitCode: number | null
): ClingoResponse {
// Parse JSON output
const json: ClingoJSONOutput = JSON.parse(stdout);
// Extract models
const models: StableModel[] = [];
if (json.Call && json.Call[0] && json.Call[0].Witnesses) {
for (let i = 0; i < json.Call[0].Witnesses.length; i++) {
const witness = json.Call[0].Witnesses[i];
models.push({
atoms: witness.Value || [],
cost: witness.Costs,
optimal: witness.Optimum === 'yes',
number: i + 1
});
}
}
// Determine status from exit code and result
let status: ClingoStatus;
if (exitCode === 30 || json.Models?.Optimum === 'yes') {
status = 'OPTIMUM';
} else if (exitCode === 10 || json.Result === 'SATISFIABLE') {
status = 'SATISFIABLE';
} else if (exitCode === 20 || json.Result === 'UNSATISFIABLE') {
status = 'UNSATISFIABLE';
} else if (json.Result === 'UNKNOWN') {
status = 'UNKNOWN';
} else {
status = 'UNKNOWN';
}
// Extract statistics
const statistics: ClingoStatistics = {
time: {
total: json.Time?.Total || 0,
cpu: json.Time?.CPU || 0,
solve: json.Time?.Solve || 0
},
models: {
enumerated: json.Models?.Number || models.length,
optimal: json.Models?.Optimal || 0,
optimum: json.Models?.Optimum === 'yes'
},
calls: json.Calls || 1
};
// Parse warnings and errors from stderr
const { warnings, errors } = this.parseStderr(stderr);
return {
status,
models,
statistics,
warnings: warnings.length > 0 ? warnings : undefined,
errors: errors.length > 0 ? errors : undefined,
optimal: status === 'OPTIMUM',
satisfiable: status === 'SATISFIABLE' || status === 'OPTIMUM'
};
}
/**
* Parse stderr for errors and warnings
* @param stderr Standard error output
* @returns Parsed errors and warnings
*/
private parseStderr(stderr: string): { warnings: string[]; errors: string[] } {
const warnings: string[] = [];
const errors: string[] = [];
if (!stderr) {
return { warnings, errors };
}
const lines = stderr.split('\n');
for (const line of lines) {
const trimmed = line.trim();
if (!trimmed) continue;
if (trimmed.includes('*** ERROR:') || trimmed.includes('error:')) {
errors.push(trimmed);
} else if (trimmed.includes('*** WARNING:') || trimmed.includes('warning:')) {
warnings.push(trimmed);
}
}
return { warnings, errors };
}
/**
* Parse validation output from stderr
* @param stderr Standard error output
* @param exitCode Process exit code
* @returns Validation result
*/
private parseValidationOutput(
stderr: string,
exitCode: number | null
): ASPValidationResult {
const errors: ASPValidationResult['errors'] = [];
const warnings: ASPValidationResult['warnings'] = [];
if (exitCode !== 0 && exitCode !== 10 && exitCode !== 20 && exitCode !== 30 && exitCode !== null) {
// Parse error messages
const lines = stderr.split('\n');
for (const line of lines) {
if (line.includes('error:')) {
const errorType = this.classifyError(line);
errors.push({
type: errorType,
message: line.trim(),
suggestion: this.getSuggestionForError(line)
});
} else if (line.includes('warning:')) {
warnings.push({
type: 'undefined',
message: line.trim()
});
}
}
}
return {
valid: errors.length === 0,
errors: errors.length > 0 ? errors : undefined,
warnings: warnings.length > 0 ? warnings : undefined
};
}
/**
* Classify error type from error message
* @param errorMessage Error message
* @returns Error type
*/
private classifyError(errorMessage: string): 'syntax' | 'semantic' | 'safety' | 'grounding' {
if (errorMessage.includes('syntax error')) {
return 'syntax';
} else if (errorMessage.includes('unsafe variables')) {
return 'safety';
} else if (errorMessage.includes('undefined') || errorMessage.includes('not defined')) {
return 'semantic';
} else if (errorMessage.includes('grounding') || errorMessage.includes('instantiation')) {
return 'grounding';
}
return 'syntax';
}
/**
* Get suggestion for error
* @param errorMessage Error message
* @returns Helpful suggestion
*/
private getSuggestionForError(errorMessage: string): string {
if (errorMessage.includes('unsafe variables')) {
return 'Every variable must appear in at least one positive (non-negated) predicate in the rule body. Add domain predicates or use global predicates.';
} else if (errorMessage.includes('syntax error')) {
return 'Check for: 1) Missing periods at end of rules, 2) Unmatched parentheses, 3) Invalid operators. ASP uses :- for "if" and not for negation.';
} else if (errorMessage.includes('undefined')) {
return 'Define all predicates used in the program. Add facts or rules that define the predicate.';
}
return 'Check the ASP syntax and program structure.';
}
/**
* Create timeout response
* @param timeout Timeout value in ms
* @returns Timeout response
*/
private createTimeoutResponse(timeout: number): ClingoResponse {
return {
status: 'TIMEOUT',
models: [],
statistics: this.createEmptyStatistics(),
errors: [`Clingo process timeout after ${timeout}ms`]
};
}
/**
* Create error response
* @param exitCode Exit code
* @param stderr Standard error output
* @returns Error response
*/
private createErrorResponse(exitCode: number, stderr: string): ClingoResponse {
return {
status: 'ERROR',
models: [],
statistics: this.createEmptyStatistics(),
errors: [
`Clingo exited with code ${exitCode}`,
stderr || 'No error message available'
]
};
}
/**
* Create empty statistics object
* @returns Empty statistics
*/
private createEmptyStatistics(): ClingoStatistics {
return {
time: {
total: 0,
cpu: 0,
solve: 0
},
models: {
enumerated: 0,
optimal: 0,
optimum: false
},
calls: 0
};
}
/**
* Test Clingo installation
* @returns True if Clingo is available and working
*/
async testConnection(): Promise<boolean> {
try {
const program = 'test.';
const response = await this.solve(program, { models: 1, timeout: 2000 });
return response.status === 'SATISFIABLE' && response.models.length === 1;
} catch (error) {
return false;
}
}
/**
* Get Clingo version information
* @returns Version string or error message
*/
async getVersion(): Promise<string> {
return new Promise((resolve, reject) => {
const proc = spawn(this.clingoPath, ['--version']);
let output = '';
proc.stdout?.on('data', (data: Buffer) => {
output += data.toString();
});
proc.on('close', (code: number | null) => {
if (code === 0) {
// Extract version from output (first line usually)
const version = output.split('\n')[0].trim();
resolve(version);
} else {
reject(new Error('Failed to get Clingo version'));
}
});
proc.on('error', (error: Error) => {
reject(new Error(`Failed to check Clingo: ${error.message}`));
});
setTimeout(() => {
proc.kill();
reject(new Error('Timeout checking Clingo version'));
}, 2000);
});
}
}
/**
* Create a solver instance with default configuration
*/
export function createClingoSolver(config?: ClingoSolverConfig): ClingoSolver {
return new ClingoSolver(config);
}
/**
* Helper functions for building ASP programs
*/
/**
* Create a fact
*/
export function fact(atom: string): string {
return `${atom}.`;
}
/**
* Create a rule
*/
export function rule(head: string, body: string[]): string {
return `${head} :- ${body.join(', ')}.`;
}
/**
* Create a constraint (headless rule)
*/
export function constraint(body: string[]): string {
return `:- ${body.join(', ')}.`;
}
/**
* Create a choice rule
*/
export function choice(
elements: string[],
lower?: number,
upper?: number,
condition?: string
): string {
const bounds = lower !== undefined || upper !== undefined
? `${lower !== undefined ? lower : ''} `
: '';
const upperBound = upper !== undefined ? ` ${upper}` : '';
const cond = condition ? ` :- ${condition}` : '';
return `${bounds}{${elements.join('; ')}}${upperBound}${cond}.`;
}
/**
* Create a show directive
*/
export function show(predicate: string, arity?: number): string {
if (arity !== undefined) {
return `#show ${predicate}/${arity}.`;
}
return `#show ${predicate}.`;
}
/**
* Create a minimize statement
*/
export function minimize(terms: Array<{ weight: number; tuple: string[] }>, priority: number = 1): string {
const termStrs = terms.map(t => `${t.weight}@${priority},${t.tuple.join(',')}`);
return `#minimize { ${termStrs.join('; ')} }.`;
}
/**
* Create a maximize statement
*/
export function maximize(terms: Array<{ weight: number; tuple: string[] }>, priority: number = 1): string {
const termStrs = terms.map(t => `${t.weight}@${priority},${t.tuple.join(',')}`);
return `#maximize { ${termStrs.join('; ')} }.`;
}
/**
* Create a complete ASP program from parts
*/
export function buildProgram(parts: {
facts?: string[];
rules?: string[];
constraints?: string[];
choices?: string[];
optimization?: string[];
show?: string[];
}): string {
const sections: string[] = [];
if (parts.facts && parts.facts.length > 0) {
sections.push('% Facts');
sections.push(...parts.facts);
sections.push('');
}
if (parts.rules && parts.rules.length > 0) {
sections.push('% Rules');
sections.push(...parts.rules);
sections.push('');
}
if (parts.choices && parts.choices.length > 0) {
sections.push('% Choice Rules');
sections.push(...parts.choices);
sections.push('');
}
if (parts.constraints && parts.constraints.length > 0) {
sections.push('% Constraints');
sections.push(...parts.constraints);
sections.push('');
}
if (parts.optimization && parts.optimization.length > 0) {
sections.push('% Optimization');
sections.push(...parts.optimization);
sections.push('');
}
if (parts.show && parts.show.length > 0) {
sections.push('% Show Directives');
sections.push(...parts.show);
}
return sections.join('\n');
}
