/**
* ASP Validator
* Validates ASP programs for syntax and semantic correctness
*/
import { ASPProgram, ASPAnalysis, ASPConflict } from '../../types.js';
export class ASPValidator {
/**
* Validate ASP program
*/
validate(program: ASPProgram): ASPAnalysis {
const errors: string[] = [];
const conflicts: ASPConflict[] = [];
// Check for empty program
if (program.facts.length === 0 && program.rules.length === 0) {
errors.push('Program is empty');
}
// Validate facts
for (const fact of program.facts) {
if (!fact.predicate) {
errors.push('Fact missing predicate');
}
if (fact.negation !== 'none' && fact.negation !== undefined) {
errors.push(`Fact cannot be negated: ${fact.predicate}`);
}
}
// Validate rules
for (const rule of program.rules) {
if (!rule.head) {
errors.push('Rule missing head');
}
if (!rule.body) {
errors.push('Rule missing body');
}
// Check for unsafe variables (variables in head not in positive body)
const headVars = this.extractVariables(Array.isArray(rule.head) ? rule.head : [rule.head]);
const positiveBodyVars = this.extractVariablesFromBody(rule.body, false);
for (const headVar of headVars) {
if (!positiveBodyVars.includes(headVar)) {
errors.push(`Unsafe variable ${headVar} in rule head`);
}
}
}
// Check for contradictory constraints
const contradictions = this.findContradictions(program);
conflicts.push(...contradictions);
// Check for circular dependencies
const circularDeps = this.findCircularDependencies(program);
conflicts.push(...circularDeps);
const analysis: ASPAnalysis = {
hasAnswerSets: errors.length === 0,
answerSetCount: -1, // Unknown until solved
explanation: errors.length === 0
? 'Program is syntactically valid'
: `Program has ${errors.length} error(s): ${errors.join('; ')}`,
conflicts: conflicts.length > 0 ? conflicts : undefined
};
return analysis;
}
/**
* Extract variables from atoms
*/
private extractVariables(atoms: any[]): string[] {
const variables: string[] = [];
for (const atom of atoms) {
if (!atom || !atom.terms) continue;
for (const term of atom.terms) {
if (typeof term === 'string' && term.match(/^[A-Z]/)) {
// Variables start with uppercase in ASP
if (!variables.includes(term)) {
variables.push(term);
}
}
}
}
return variables;
}
/**
* Extract variables from body literals
*/
private extractVariablesFromBody(body: any[], onlyPositive: boolean = false): string[] {
const variables: string[] = [];
for (const literal of body) {
if (onlyPositive && literal.negation !== 'none') continue;
const atomVars = this.extractVariables([literal.atom]);
for (const v of atomVars) {
if (!variables.includes(v)) {
variables.push(v);
}
}
}
return variables;
}
/**
* Find contradictory constraints
*/
private findContradictions(program: ASPProgram): ASPConflict[] {
const conflicts: ASPConflict[] = [];
// Simple check: constraints that are always violated
for (const constraint of program.constraints) {
if (constraint.body.length === 0) {
conflicts.push({
type: 'contradiction',
involvedRules: [],
explanation: 'Empty constraint body - always violated',
location: 'constraint'
});
}
}
return conflicts;
}
/**
* Find circular dependencies
*/
private findCircularDependencies(program: ASPProgram): ASPConflict[] {
const conflicts: ASPConflict[] = [];
// Build dependency graph
const dependencies: Map<string, string[]> = new Map();
for (const rule of program.rules) {
const headPreds = Array.isArray(rule.head)
? rule.head.map(h => h.predicate)
: [rule.head.predicate];
for (const headPred of headPreds) {
if (!dependencies.has(headPred)) {
dependencies.set(headPred, []);
}
for (const bodyLit of rule.body) {
const bodyPred = bodyLit.atom.predicate;
if (!dependencies.get(headPred)!.includes(bodyPred)) {
dependencies.get(headPred)!.push(bodyPred);
}
}
}
}
// Detect cycles
const visited = new Set<string>();
const recStack = new Set<string>();
const detectCycle = (pred: string, path: string[]): boolean => {
visited.add(pred);
recStack.add(pred);
path.push(pred);
const deps = dependencies.get(pred) || [];
for (const dep of deps) {
if (!visited.has(dep)) {
if (detectCycle(dep, [...path])) {
return true;
}
} else if (recStack.has(dep)) {
// Cycle detected
conflicts.push({
type: 'circular_dependency',
involvedRules: [],
explanation: `Circular dependency: ${[...path, dep].join(' → ')}`,
location: 'rules'
});
return true;
}
}
recStack.delete(pred);
return false;
};
for (const pred of dependencies.keys()) {
if (!visited.has(pred)) {
detectCycle(pred, []);
}
}
return conflicts;
}
}
