import {
SMTProblem,
SMTAnalysis,
SMTSolution
} from '../../types.js';
/**
* Validator for SMT problems
* Checks constraints for satisfiability and correctness
*/
export class SMTValidator {
/**
* Validate an SMT problem
* @param problem SMT problem to validate
* @returns Analysis result
*/
validate(problem: SMTProblem): SMTAnalysis {
// Check for empty constraints
if (problem.constraints.length === 0) {
return {
isSatisfiable: true,
explanation: 'No constraints provided - trivially satisfiable'
};
}
// Check for contradictory constraints
const contradiction = this.findContradiction(problem);
if (contradiction) {
return {
isSatisfiable: false,
explanation: `Unsatisfiable: ${contradiction}`,
counterexample: contradiction
};
}
// Check for obvious satisfiability
const trivialSat = this.checkTrivialSat(problem);
if (trivialSat) {
return {
isSatisfiable: true,
explanation: 'Constraints appear satisfiable',
solution: {
status: 'sat',
model: this.generateTrivialModel(problem)
}
};
}
// Default to unknown (would require actual Z3 solving)
return {
isSatisfiable: true,
explanation: 'Constraint validation requires SMT solver'
};
}
/**
* Find obvious contradictions in constraints
* @param problem SMT problem
* @returns Contradiction description or null
*/
private findContradiction(problem: SMTProblem): string | null {
const constraints = problem.constraints.map(c => c.expression.toLowerCase());
// Check for direct contradictions like "x > 10" and "x < 5"
for (const varName of problem.variables.map(v => v.name)) {
const upperBounds: number[] = [];
const lowerBounds: number[] = [];
for (const constraint of constraints) {
// Match patterns like "x < 5" or "x <= 5"
const upperMatch = constraint.match(new RegExp(`${varName}\\s*(<|<=)\\s*(\\d+)`));
if (upperMatch) {
const bound = parseInt(upperMatch[2]);
const inclusive = upperMatch[1] === '<=';
upperBounds.push(inclusive ? bound : bound - 1);
}
// Match patterns like "x > 10" or "x >= 10"
const lowerMatch = constraint.match(new RegExp(`${varName}\\s*(>|>=)\\s*(\\d+)`));
if (lowerMatch) {
const bound = parseInt(lowerMatch[2]);
const inclusive = lowerMatch[1] === '>=';
lowerBounds.push(inclusive ? bound : bound + 1);
}
}
// Check if lower bound exceeds upper bound
if (upperBounds.length > 0 && lowerBounds.length > 0) {
const maxLower = Math.max(...lowerBounds);
const minUpper = Math.min(...upperBounds);
if (maxLower > minUpper) {
return `Variable ${varName} must be > ${maxLower - 1} and < ${minUpper + 1}, which is impossible`;
}
}
}
// Check for explicit contradictions like "x == 5" and "x == 10"
for (const varName of problem.variables.map(v => v.name)) {
const equalities: number[] = [];
for (const constraint of constraints) {
const eqMatch = constraint.match(new RegExp(`${varName}\\s*==\\s*(\\d+)`));
if (eqMatch) {
equalities.push(parseInt(eqMatch[1]));
}
}
if (equalities.length > 1) {
const uniqueVals = [...new Set(equalities)];
if (uniqueVals.length > 1) {
return `Variable ${varName} cannot equal both ${uniqueVals[0]} and ${uniqueVals[1]}`;
}
}
}
return null;
}
/**
* Check if constraints are trivially satisfiable
* @param problem SMT problem
* @returns True if trivially satisfiable
*/
private checkTrivialSat(problem: SMTProblem): boolean {
// Check if all constraints are non-contradictory simple bounds
for (const constraint of problem.constraints) {
const expr = constraint.expression.toLowerCase();
// Complex constraints require solver
if (expr.includes('and') || expr.includes('or') || expr.includes('+') || expr.includes('*')) {
return false;
}
}
return true;
}
/**
* Generate a trivial model that might satisfy simple constraints
* @param problem SMT problem
* @returns Simple model
*/
private generateTrivialModel(problem: SMTProblem): { [variable: string]: string | number | boolean } {
const model: { [variable: string]: string | number | boolean } = {};
for (const variable of problem.variables) {
if (variable.type === 'Int') {
model[variable.name] = 0;
} else if (variable.type === 'Real') {
model[variable.name] = 0.0;
} else if (variable.type === 'Bool') {
model[variable.name] = false;
} else {
model[variable.name] = '';
}
}
return model;
}
/**
* Validate constraint syntax
* @param constraint Constraint expression
* @returns True if valid
*/
validateConstraintSyntax(constraint: string): boolean {
// Basic syntax validation
try {
// Check for balanced parentheses
let depth = 0;
for (const char of constraint) {
if (char === '(') depth++;
if (char === ')') depth--;
if (depth < 0) return false;
}
if (depth !== 0) return false;
// Check for valid operators
const validOperators = ['+', '-', '*', '/', '==', '!=', '<', '>', '<=', '>=', 'and', 'or', 'not'];
// TODO: More sophisticated syntax checking
return true;
} catch (e) {
return false;
}
}
}
